From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 3AAE8385842C; Wed, 5 Jan 2022 11:34:23 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 3AAE8385842C MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r12-6236] [Ada] Proof of runtime units for integer exponentiation (checks on) X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: 1702fb6bf95de5461f896cf69832edc0e2e40cc5 X-Git-Newrev: 3814652309edac1154ee3c7e40ff65ff861d17f3 Message-Id: <20220105113423.3AAE8385842C@sourceware.org> Date: Wed, 5 Jan 2022 11:34:23 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 05 Jan 2022 11:34:23 -0000 https://gcc.gnu.org/g:3814652309edac1154ee3c7e40ff65ff861d17f3 commit r12-6236-g3814652309edac1154ee3c7e40ff65ff861d17f3 Author: Yannick Moy Date: Tue Nov 30 15:11:32 2021 +0100 [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: --- gcc/ada/libgnat/s-expint.ads | 21 ++++- gcc/ada/libgnat/s-explli.ads | 22 ++++- gcc/ada/libgnat/s-expllli.ads | 23 +++++- gcc/ada/libgnat/s-expont.adb | 186 ++++++++++++++++++++++++++++++++++++++---- gcc/ada/libgnat/s-expont.ads | 35 +++++++- 5 files changed, 261 insertions(+), 26 deletions(-) diff --git a/gcc/ada/libgnat/s-expint.ads b/gcc/ada/libgnat/s-expint.ads index f41b6faabe5..b44cae5535d 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 d9c8544e2a8..ebf579473e3 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 1ee278d8b82..3c009bcac94 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 3c259cfc2e9..dc1586b4c23 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 022cb64eb91..4a62b186af1 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;