From patchwork Wed Jan 5 11:33:31 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 49560 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id C687C3858438 for ; Wed, 5 Jan 2022 11:42:54 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org C687C3858438 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1641382974; bh=Y0GpekvwlsQXSAMRM2X4t17051r9tirwNFuAei7cgYI=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=Xjy4ifr1iGJ3tkevWdUnHmzRqspzSQBQlcEad3Pib6nZ9Tmum4jsAtO565wSyu4/+ oDzoJKlAiJWHxkHnJI5Am/7QTpYVts8/5PT48DLq8jzqqEbkUuXg6j0oc28ac5Hnvq RyK79dQROz+qb3Q7aSbrngft6yYxUcF2oE8j0rBE= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x42b.google.com (mail-wr1-x42b.google.com [IPv6:2a00:1450:4864:20::42b]) by sourceware.org (Postfix) with ESMTPS id 1FB1B385842C for ; Wed, 5 Jan 2022 11:33:33 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 1FB1B385842C Received: by mail-wr1-x42b.google.com with SMTP id v6so20637009wra.8 for ; Wed, 05 Jan 2022 03:33:33 -0800 (PST) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=Y0GpekvwlsQXSAMRM2X4t17051r9tirwNFuAei7cgYI=; b=xcb1b9UXrk6gxrZSoNA9/NFnLMRWEdiUlFzwIoKfIv5RyFQGVQrf+WUdqxr0Peu8Zq pHGTHz3YmYH4NH7FEa9x1dRuA8fmvkML17U0yVKXIhAOM8+6WIswGdBh3ns7FFg14/Ql poHUxoEDVtYXo+cTQjKW+jE7JquNCjX/dYNwYqZlJZJ8bPpWVLrGswyV6Yai+Hd5ajSG OfFUXxocrQtTolJ6UJ302rYu4epO2DwKC/8Uvct9D3TBaIu74f8w7gKwak6orOhK1EZ4 wnpg9vehvChEZGniDSTGylIqw8kjDy7oIthYlbsMsBn429ii8n1tq4iElapAhS/AbTK6 AQew== X-Gm-Message-State: AOAM532Op9XQy1VK1o6nTVuqvlMJPFfkm0wmXjnhtJcjewoftkjxINj5 n6UYv8Mm+T9VfVlj5R7u1F9jjhVI3yKtJQ== X-Google-Smtp-Source: ABdhPJxV+4D5j4/NMwfXbEqfNMsxDvmppV5wiCKnrgKc3Qdcd2oD0/nics5f33IBZ7G8AFFX7kmBog== X-Received: by 2002:adf:f4ca:: with SMTP id h10mr46675164wrp.512.1641382412196; Wed, 05 Jan 2022 03:33:32 -0800 (PST) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id b2sm44945944wrd.35.2022.01.05.03.33.31 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 05 Jan 2022 03:33:31 -0800 (PST) Date: Wed, 5 Jan 2022 11:33:31 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Proof of runtime units for integer exponentiation (checks off) Message-ID: <20220105113331.GA2713264@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.7 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" This proves the generic unit System.Exponn instanciated for Integer, Long_Long_Integer and Long_Long_Long_Integer. In order to be able to add a suitable contract to the generic function, it is changed into a generic package which contains the function. Instantiations are adapted. GNATprove is called with switch --level=2. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-exnint.ads: Mark in SPARK. Adapt to change to package. * libgnat/s-exnlli.ads: Likewise. * libgnat/s-exnllli.ads: Likewise. * libgnat/s-exponn.adb: Add lemmas and ghost code. Secial case value zero as Left or Right to simplify proof. * libgnat/s-exponn.ads: Transform the generic function into a generic package with a function inside. Add a functional contract. diff --git a/gcc/ada/libgnat/s-exnint.ads b/gcc/ada/libgnat/s-exnint.ads --- a/gcc/ada/libgnat/s-exnint.ads +++ b/gcc/ada/libgnat/s-exnint.ads @@ -31,11 +31,26 @@ -- Integer exponentiation (checks off) +-- 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.Exponn; -package System.Exn_Int is +package System.Exn_Int + with SPARK_Mode +is + + package Exponn_Integer is new Exponn (Integer); - function Exn_Integer is new Exponn (Integer); - pragma Pure_Function (Exn_Integer); + function Exn_Integer (Left : Integer; Right : Natural) return Integer + renames Exponn_Integer.Expon; end System.Exn_Int; diff --git a/gcc/ada/libgnat/s-exnlli.ads b/gcc/ada/libgnat/s-exnlli.ads --- a/gcc/ada/libgnat/s-exnlli.ads +++ b/gcc/ada/libgnat/s-exnlli.ads @@ -31,11 +31,27 @@ -- Long_Long_Integer exponentiation (checks off) +-- 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.Exponn; -package System.Exn_LLI is +package System.Exn_LLI + with SPARK_Mode +is + + package Exponn_Integer is new Exponn (Long_Long_Integer); - function Exn_Long_Long_Integer is new Exponn (Long_Long_Integer); - pragma Pure_Function (Exn_Long_Long_Integer); + function Exn_Long_Long_Integer + (Left : Long_Long_Integer; Right : Natural) return Long_Long_Integer + renames Exponn_Integer.Expon; end System.Exn_LLI; diff --git a/gcc/ada/libgnat/s-exnllli.ads b/gcc/ada/libgnat/s-exnllli.ads --- a/gcc/ada/libgnat/s-exnllli.ads +++ b/gcc/ada/libgnat/s-exnllli.ads @@ -31,11 +31,28 @@ -- Long_Long_Long_Integer exponentiation (checks off) +-- 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.Exponn; -package System.Exn_LLLI is +package System.Exn_LLLI + with SPARK_Mode +is + + package Exponn_Integer is new Exponn (Long_Long_Long_Integer); - function Exn_Long_Long_Long_Integer is new Exponn (Long_Long_Long_Integer); - pragma Pure_Function (Exn_Long_Long_Long_Integer); + function Exn_Long_Long_Long_Integer + (Left : Long_Long_Long_Integer; Right : Natural) + return Long_Long_Long_Integer + renames Exponn_Integer.Expon; end System.Exn_LLLI; diff --git a/gcc/ada/libgnat/s-exponn.adb b/gcc/ada/libgnat/s-exponn.adb --- a/gcc/ada/libgnat/s-exponn.adb +++ b/gcc/ada/libgnat/s-exponn.adb @@ -29,44 +29,198 @@ -- -- ------------------------------------------------------------------------------ -function System.Exponn (Left : Int; Right : Natural) return Int is +package body System.Exponn + 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 Suppress (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 Suppress (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.Exponn; diff --git a/gcc/ada/libgnat/s-exponn.ads b/gcc/ada/libgnat/s-exponn.ads --- a/gcc/ada/libgnat/s-exponn.ads +++ b/gcc/ada/libgnat/s-exponn.ads @@ -31,8 +31,41 @@ -- Signed integer exponentiation (checks off) +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; + generic type Int is range <>; -function System.Exponn (Left : Int; Right : Natural) return Int; +package System.Exponn + 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.Exponn;