From patchwork Wed Jan 5 11:33:37 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: 49565 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 F2F233858434 for ; Wed, 5 Jan 2022 11:47:50 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org F2F233858434 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1641383271; bh=QMsKkDuSKQgUe/znN421DjydZ/LWhwbuYTYKvDyx9d8=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=K7cdH5lmH3Ibcse+uoj7GcydQQLbJN5Heb7VSe1QgdbwifFT/f7DmJjCYxyydu2pG 9tglEPgWZaeVkWG0vwdhJfNjluJFirIvaJlxye3e+EXJdKGUqu4WDoJGKIpUDckXcn fG4zxIFDGWm2siO91/pCQPQGQEIMrZ/jyt4xhwF0= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x434.google.com (mail-wr1-x434.google.com [IPv6:2a00:1450:4864:20::434]) by sourceware.org (Postfix) with ESMTPS id 1D80C385843D for ; Wed, 5 Jan 2022 11:33:39 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 1D80C385843D Received: by mail-wr1-x434.google.com with SMTP id w20so73329723wra.9 for ; Wed, 05 Jan 2022 03:33:39 -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=QMsKkDuSKQgUe/znN421DjydZ/LWhwbuYTYKvDyx9d8=; b=Mw9Zl0rGD+Sbi1I0zV+QvOfP9QSG27YTMr0KTjYq8+dZ2RA6n2MgFT8OC4uoXqB5Je H3FaxJEKGrV0HcW8B6yNRYlR2e0nf8JBmdbbUd0QifKK55/7HUamhV9p0yRVD1pi60Ja LrBUugt2VkYYorhQq+aFstJ5ap/C4EtWT5IPEhzuOkuycmegm6JFwg9j8qhW5rvp02NN fqy8Ts1Q1y4p7F+ztVCGEmYDyG9haPoU3CRIeB2eUQBq8/SaDbxK2whZuEjda7MAmne5 iWmxy7rPYJ0kOhZomKjUTZCMWMwCzaazKK9MUWW93NBJDCuHgv0ZCdEx5GP65C9wbzyv DH5g== X-Gm-Message-State: AOAM532rQLHuVH52HvXscQATFhAwZ2MotkzOuEdvTf70v51B1G+8LGhZ 19Y73us7tfeDbV9c/+q7+F32Y5a283AIxQ== X-Google-Smtp-Source: ABdhPJwaBzQ+BNk5tOR8p2Aa5OZ/8WTelc0emmbOQfo0JG/iPBUtpvZFOVmi8PNpYa8w7ZasZH9/ZA== X-Received: by 2002:a05:6000:1c1d:: with SMTP id ba29mr2086388wrb.235.1641382418154; Wed, 05 Jan 2022 03:33:38 -0800 (PST) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id e12sm44914884wrg.110.2022.01.05.03.33.37 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 05 Jan 2022 03:33:37 -0800 (PST) Date: Wed, 5 Jan 2022 11:33:37 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Proof of runtime units for integer exponentiation (checks on) Message-ID: <20220105113337.GA2714352@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.Expont instantiated for Integer, Long_Long_Integer and Long_Long_Long_Integer. The proof is similar to the one done for the same units with checks off. In this case too, the generic function is changed into a generic package. GNATprove is called with switch --level=2. Tested on x86_64-pc-linux-gnu, committed on trunk 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 --- 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 --- 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 --- 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 --- 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 --- 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;