From: Yannick Moy Date: Tue, 30 Nov 2021 14:11:32 +0000 (+0100) Subject: [Ada] Proof of runtime units for integer exponentiation (checks on) X-Git-Tag: upstream/12.2.0~2461 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=3814652309edac1154ee3c7e40ff65ff861d17f3;p=platform%2Fupstream%2Fgcc.git [Ada] Proof of runtime units for integer exponentiation (checks on) gcc/ada/ * libgnat/s-expint.ads: Mark in SPARK. Adapt to change to package. * libgnat/s-explli.ads: Likewise. * libgnat/s-expllli.ads: Likewise. * libgnat/s-expont.adb: Add lemmas and ghost code. * libgnat/s-expont.ads: Add functional contract. --- diff --git a/gcc/ada/libgnat/s-expint.ads b/gcc/ada/libgnat/s-expint.ads index f41b6fa..b44cae5 100644 --- a/gcc/ada/libgnat/s-expint.ads +++ b/gcc/ada/libgnat/s-expint.ads @@ -31,11 +31,26 @@ -- Integer exponentiation (checks on) +-- Preconditions, postconditions, ghost code, loop invariants and assertions +-- in this unit are meant for analysis only, not for run-time checking, as it +-- would be too costly otherwise. This is enforced by setting the assertion +-- policy to Ignore. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + with System.Expont; -package System.Exp_Int is +package System.Exp_Int + with SPARK_Mode +is + + package Expont_Integer is new Expont (Integer); - function Exp_Integer is new Expont (Integer); - pragma Pure_Function (Exp_Integer); + function Exp_Integer (Left : Integer; Right : Natural) return Integer + renames Expont_Integer.Expon; end System.Exp_Int; diff --git a/gcc/ada/libgnat/s-explli.ads b/gcc/ada/libgnat/s-explli.ads index d9c8544..ebf5794 100644 --- a/gcc/ada/libgnat/s-explli.ads +++ b/gcc/ada/libgnat/s-explli.ads @@ -31,11 +31,27 @@ -- Long_Long_Integer exponentiation (checks on) +-- Preconditions, postconditions, ghost code, loop invariants and assertions +-- in this unit are meant for analysis only, not for run-time checking, as it +-- would be too costly otherwise. This is enforced by setting the assertion +-- policy to Ignore. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + with System.Expont; -package System.Exp_LLI is +package System.Exp_LLI + with SPARK_Mode +is + + package Expont_Integer is new Expont (Long_Long_Integer); - function Exp_Long_Long_Integer is new Expont (Long_Long_Integer); - pragma Pure_Function (Exp_Long_Long_Integer); + function Exp_Long_Long_Integer + (Left : Long_Long_Integer; Right : Natural) return Long_Long_Integer + renames Expont_Integer.Expon; end System.Exp_LLI; diff --git a/gcc/ada/libgnat/s-expllli.ads b/gcc/ada/libgnat/s-expllli.ads index 1ee278d..3c009bc 100644 --- a/gcc/ada/libgnat/s-expllli.ads +++ b/gcc/ada/libgnat/s-expllli.ads @@ -31,11 +31,28 @@ -- Long_Long_Long_Integer exponentiation (checks on) +-- Preconditions, postconditions, ghost code, loop invariants and assertions +-- in this unit are meant for analysis only, not for run-time checking, as it +-- would be too costly otherwise. This is enforced by setting the assertion +-- policy to Ignore. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + with System.Expont; -package System.Exp_LLLI is +package System.Exp_LLLI + with SPARK_Mode +is + + package Expont_Integer is new Expont (Long_Long_Long_Integer); - function Exp_Long_Long_Long_Integer is new Expont (Long_Long_Long_Integer); - pragma Pure_Function (Exp_Long_Long_Long_Integer); + function Exp_Long_Long_Long_Integer + (Left : Long_Long_Long_Integer; Right : Natural) + return Long_Long_Long_Integer + renames Expont_Integer.Expon; end System.Exp_LLLI; diff --git a/gcc/ada/libgnat/s-expont.adb b/gcc/ada/libgnat/s-expont.adb index 3c259cf..dc1586b 100644 --- a/gcc/ada/libgnat/s-expont.adb +++ b/gcc/ada/libgnat/s-expont.adb @@ -29,44 +29,198 @@ -- -- ------------------------------------------------------------------------------ -function System.Expont (Left : Int; Right : Natural) return Int is +package body System.Expont + with SPARK_Mode +is - -- Note that negative exponents get a constraint error because the - -- subtype of the Right argument (the exponent) is Natural. + -- Preconditions, postconditions, ghost code, loop invariants and + -- assertions in this unit are meant for analysis only, not for run-time + -- checking, as it would be too costly otherwise. This is enforced by + -- setting the assertion policy to Ignore. - Result : Int := 1; - Factor : Int := Left; - Exp : Natural := Right; + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); -begin - -- We use the standard logarithmic approach, Exp gets shifted right - -- testing successive low order bits and Factor is the value of the - -- base raised to the next power of 2. + -- Local lemmas - -- Note: it is not worth special casing base values -1, 0, +1 since - -- the expander does this when the base is a literal, and other cases - -- will be extremely rare. + procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) + with + Ghost, + Pre => A /= 0, + Post => + (if Exp rem 2 = 0 then + A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) + else + A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A); + + procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive) + with + Ghost, + Pre => In_Int_Range (A ** Exp * A ** Exp), + Post => In_Int_Range (A * A); + + procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural) + with + Ghost, + Pre => A /= 0, + Post => A ** Exp /= 0; + + procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural) + with + Ghost, + Pre => A /= 0 + and then Exp rem 2 = 0, + Post => A ** Exp > 0; + + procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer) + with + Ghost, + Pre => Y /= 0 + and then not (X = -Big (Int'First) and Y = -1) + and then X * Y = Z + and then In_Int_Range (Z), + Post => In_Int_Range (X); + + ----------------------------- + -- Local lemma null bodies -- + ----------------------------- + + procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural) is null; + procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer) is null; + + ----------- + -- Expon -- + ----------- + + function Expon (Left : Int; Right : Natural) return Int is + + -- Note that negative exponents get a constraint error because the + -- subtype of the Right argument (the exponent) is Natural. + + Result : Int := 1; + Factor : Int := Left; + Exp : Natural := Right; + + Rest : Big_Integer with Ghost; + -- Ghost variable to hold Factor**Exp between Exp and Factor updates + + begin + -- We use the standard logarithmic approach, Exp gets shifted right + -- testing successive low order bits and Factor is the value of the + -- base raised to the next power of 2. + + -- Note: for compilation only, it is not worth special casing base + -- values -1, 0, +1 since the expander does this when the base is a + -- literal, and other cases will be extremely rare. But for proof, + -- special casing zero in both positions makes ghost code and lemmas + -- simpler, so we do it. + + if Right = 0 then + return 1; + elsif Left = 0 then + return 0; + end if; - if Exp /= 0 then loop + pragma Loop_Invariant (Exp > 0); + pragma Loop_Invariant (Factor /= 0); + pragma Loop_Invariant + (Big (Result) * Big (Factor) ** Exp = Big (Left) ** Right); + pragma Loop_Variant (Decreases => Exp); + pragma Annotate + (CodePeer, False_Positive, + "validity check", "confusion on generated code"); + if Exp rem 2 /= 0 then declare pragma Unsuppress (Overflow_Check); begin + pragma Assert + (Big (Factor) ** Exp + = Big (Factor) * Big (Factor) ** (Exp - 1)); + Lemma_Exp_Positive (Big (Factor), Exp - 1); + Lemma_Mult_In_Range (Big (Result) * Big (Factor), + Big (Factor) ** (Exp - 1), + Big (Left) ** Right); + Result := Result * Factor; end; end if; + Lemma_Exp_Expand (Big (Factor), Exp); + Exp := Exp / 2; exit when Exp = 0; + Rest := Big (Factor) ** Exp; + pragma Assert + (Big (Result) * (Rest * Rest) = Big (Left) ** Right); + declare pragma Unsuppress (Overflow_Check); begin + Lemma_Mult_In_Range (Rest * Rest, + Big (Result), + Big (Left) ** Right); + Lemma_Exp_In_Range (Big (Factor), Exp); + Factor := Factor * Factor; end; + + pragma Assert (Big (Factor) ** Exp = Rest * Rest); end loop; - end if; - return Result; + pragma Assert (Big (Result) = Big (Left) ** Right); + + return Result; + end Expon; + + ---------------------- + -- Lemma_Exp_Expand -- + ---------------------- + + procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is + begin + if Exp rem 2 = 0 then + pragma Assert (Exp = Exp / 2 + Exp / 2); + else + pragma Assert (Exp = Exp / 2 + Exp / 2 + 1); + pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1)); + pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A); + pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A); + end if; + end Lemma_Exp_Expand; + + ------------------------ + -- Lemma_Exp_In_Range -- + ------------------------ + + procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive) is + begin + if A /= 0 and Exp /= 1 then + pragma Assert (A ** Exp = A * A ** (Exp - 1)); + Lemma_Mult_In_Range + (A * A, A ** (Exp - 1) * A ** (Exp - 1), A ** Exp * A ** Exp); + end if; + end Lemma_Exp_In_Range; + + ------------------------ + -- Lemma_Exp_Positive -- + ------------------------ + + procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural) is + begin + if Exp = 0 then + pragma Assert (A ** Exp = 1); + else + pragma Assert (Exp = 2 * (Exp / 2)); + pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2)); + pragma Assert (A ** Exp = (A ** (Exp / 2)) ** 2); + Lemma_Exp_Not_Zero (A, Exp / 2); + end if; + end Lemma_Exp_Positive; + end System.Expont; diff --git a/gcc/ada/libgnat/s-expont.ads b/gcc/ada/libgnat/s-expont.ads index 022cb64..4a62b18 100644 --- a/gcc/ada/libgnat/s-expont.ads +++ b/gcc/ada/libgnat/s-expont.ads @@ -31,8 +31,41 @@ -- Signed integer exponentiation (checks on) +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; + generic type Int is range <>; -function System.Expont (Left : Int; Right : Natural) return Int; +package System.Expont + with Pure, SPARK_Mode +is + + -- Preconditions in this unit are meant for analysis only, not for run-time + -- checking, so that the expected exceptions are raised. This is enforced + -- by setting the corresponding assertion policy to Ignore. Postconditions + -- and contract cases should not be executed at runtime as well, in order + -- not to slow down the execution of these functions. + + pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); + + package Signed_Conversion is new Signed_Conversions (Int => Int); + + function Big (Arg : Int) return Big_Integer is + (Signed_Conversion.To_Big_Integer (Arg)) + with Ghost; + + function In_Int_Range (Arg : Big_Integer) return Boolean is + (In_Range (Arg, Big (Int'First), Big (Int'Last))) + with Ghost; + + function Expon (Left : Int; Right : Natural) return Int + with + Pre => In_Int_Range (Big (Left) ** Right), + Post => Expon'Result = Left ** Right; + +end System.Expont;