From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 670173881D2B for ; Tue, 16 May 2023 08:41:24 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 670173881D2B Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-wr1-x42b.google.com with SMTP id ffacd0b85a97d-307c040797bso4511901f8f.3 for ; Tue, 16 May 2023 01:41:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1684226483; x=1686818483; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=RiImX8CIC7rQhpvJUkP0QWeF/CTarMDqy3gop9edjgM=; b=OFhNCuxPs/Z88zkHazhkoYnWwgVhAQZAPwiSigl7GbBOqCT8YykzRPbVklQEqsjKrv KCLu0s8+WE3rg4KRCd9oTC95sQAFkzUVArFO8nZ5aqu/GK/jKhiMmbRDW3DK2TNWOIqk V+3ZarPl1B4wUiWTR8Fr/OphwAFxSg6paejqHAKF9M2umE3T7tn/7zIVt1yQqZ24m52n Lw80LcpyC4N79+DP3Spa8Ahj19SpLjOcq8HbU/Ccc551x9DSOOYDBFjzgUgzOQrkOoJM 3lKiXNf3oA0ys8Rvh4XRhfgTqvBse2FBUQ1nHGp/eodDUuPcxDroitgN53/XdvfgIT4L ra1w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684226483; x=1686818483; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=RiImX8CIC7rQhpvJUkP0QWeF/CTarMDqy3gop9edjgM=; b=XCP1q/TbsLp26Nv5xqVYxE1gfMXKChDclAUj0PDqDhf5lCK1T4Pet9XyWnkiLnQCST DyKFZDm8MPo/5eEzG59O/Mv6ten5C1+twf8qs/nSgcmfqDK3OFz/ALOZEVwWm0ogfG1u RnbeejG9LSH8QIf6gy+qnWzr/vwhPsUx0TV9Eo4kqbGRA66Jv1kKG77F9ZmIkrZmKuUF gwoQ9YqU5XB71J8BUqHgO9ZeLii6p/JD3pqBBqDX4L31FwYR9m0Dr/PyzW94p0ZgO0p3 xLbXnlD2rjoKuc0YungkCFL86Q8w+mkgUsO12tcoQUArDJVCZ+Hcp22SuoKUCTSsUUnl Os8g== X-Gm-Message-State: AC+VfDw01gNzNcZTmlVYFdBjES4h4jH3QgxyJ3wvd1i5gmLVN9yO17v5 L3cFPzVlgl6wWG5XIaW0MApOzy0t69ajXL2M4IdlXw== X-Google-Smtp-Source: ACHHUZ6dqwQATVSP+TihfVrUanMQL8G3JV8ChkFM5QDbsVpVRtzA08QAiJNnMskdpDgtzwWGUdqDYw== X-Received: by 2002:a5d:4578:0:b0:306:31e0:958 with SMTP id a24-20020a5d4578000000b0030631e00958mr26133138wrc.15.1684226483036; Tue, 16 May 2023 01:41:23 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id i15-20020a5d630f000000b0030771c6e443sm1781740wru.42.2023.05.16.01.41.22 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 16 May 2023 01:41:22 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Update proof of runtime units Date: Tue, 16 May 2023 10:41:20 +0200 Message-Id: <20230516084120.1502199-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Status: No, score=-13.1 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,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org List-Id: From: Yannick Moy Following changes in GNATprove, proofs need to be amended. gcc/ada/ * libgnat/s-aridou.adb (Lemma_Div_Pow2): Add assertion. * libgnat/s-arit32.adb (Lemma_Abs_Div_Commutation): Simplify. * libgnat/s-expmod.adb (Lemma_Exp_Mod): Add assertions. (Lemma_Euclidean_Mod): Add body to lemma. (Lemma_Mult_Mod): Add assertion. * libgnat/s-valueu.adb (Scan_Raw_Unsigned): Modify assertion. * libgnat/s-vauspe.ads (Raw_Unsigned_Last_Ghost): Add postcondition. * libgnat/s-widthi.adb: Use more precise types. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/s-aridou.adb | 2 +- gcc/ada/libgnat/s-arit32.adb | 33 +-------------------------------- gcc/ada/libgnat/s-expmod.adb | 20 ++++++++++++++++++-- gcc/ada/libgnat/s-valueu.adb | 12 ++++++------ gcc/ada/libgnat/s-vauspe.ads | 3 ++- gcc/ada/libgnat/s-widthi.adb | 6 +++--- 6 files changed, 31 insertions(+), 45 deletions(-) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index dbf0f42cd49..041478538a7 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -1543,7 +1543,7 @@ is Div2 : constant Double_Uns := Double_Uns'(2); Left : constant Double_Uns := X / Div1 / Div2; R2 : constant Double_Uns := X / Div1 - Left * Div2; - pragma Assert (R2 < Div2); + pragma Assert (R2 <= Div2 - 1); R1 : constant Double_Uns := X - X / Div1 * Div1; pragma Assert (R1 < Div1); begin diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index bd316c1bc20..219523b00f2 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -195,12 +195,6 @@ is or else (X >= Big_0 and then Y <= Big_0), Post => X * Y <= Big_0; - procedure Lemma_Neg_Div (X, Y : Big_Integer) - with - Ghost, - Pre => Y /= 0, - Post => X / Y = (-X) / (-Y); - procedure Lemma_Neg_Rem (X, Y : Big_Integer) with Ghost, @@ -223,6 +217,7 @@ is ----------------------------- procedure Lemma_Abs_Commutation (X : Int32) is null; + procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is null; procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null; procedure Lemma_Div_Commutation (X, Y : Uns64) is null; procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null; @@ -234,22 +229,6 @@ is procedure Lemma_Not_In_Range_Big2xx32 is null; procedure Lemma_Rem_Commutation (X, Y : Uns64) is null; - ------------------------------- - -- Lemma_Abs_Div_Commutation -- - ------------------------------- - - procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is - begin - if Y < 0 then - if X < 0 then - pragma Assert (abs (X / Y) = abs (X / (-Y))); - else - Lemma_Neg_Div (X, Y); - pragma Assert (abs (X / Y) = abs ((-X) / (-Y))); - end if; - end if; - end Lemma_Abs_Div_Commutation; - ------------------------------- -- Lemma_Abs_Rem_Commutation -- ------------------------------- @@ -277,16 +256,6 @@ is pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32); end Lemma_Hi_Lo; - ------------------- - -- Lemma_Neg_Div -- - ------------------- - - procedure Lemma_Neg_Div (X, Y : Big_Integer) is - begin - pragma Assert ((-X) / (-Y) = -(X / (-Y))); - pragma Assert (X / (-Y) = -(X / Y)); - end Lemma_Neg_Div; - ----------------- -- Raise_Error -- ----------------- diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb index 0682589d352..aa6e9b4c361 100644 --- a/gcc/ada/libgnat/s-expmod.adb +++ b/gcc/ada/libgnat/s-expmod.adb @@ -109,9 +109,21 @@ is procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) with Pre => F /= 0, - Post => (Q * F + R) mod F = R mod F; + Post => (Q * F + R) mod F = R mod F, + Subprogram_Variant => (Decreases => Q); - procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is null; + ------------------------- + -- Lemma_Euclidean_Mod -- + ------------------------- + + procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is + begin + if Q > 0 then + Lemma_Euclidean_Mod (Q - 1, F, R); + end if; + end Lemma_Euclidean_Mod; + + -- Local variables Left : constant Big_Natural := (X + Y) mod B; Right : constant Big_Natural := ((X mod B) + (Y mod B)) mod B; @@ -164,6 +176,9 @@ is Lemma_Mod_Mod (A, B); Lemma_Exp_Mod (A, Exp - 1, B); Lemma_Mult_Mod (A, A ** (Exp - 1), B); + pragma Assert + ((A mod B) * (A mod B) ** (Exp - 1) = (A mod B) ** Exp); + pragma Assert (A * A ** (Exp - 1) = A ** Exp); pragma Assert (Left = Right); end; end if; @@ -190,6 +205,7 @@ is pragma Assert (Left = Right); else pragma Assert (Y mod B = 0); + pragma Assert (Y / B * B = Y); pragma Assert ((X * Y) mod B = (X * Y) - (X * Y) / B * B); pragma Assert ((X * Y) mod B = (X * Y) - (X * (Y / B) * B) / B * B); diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index bc6ed1ca669..062ad33b1e9 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -483,12 +483,12 @@ package body System.Value_U is pragma Assert (By (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max), - (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max)) - then Ptr.all = First_Exp - elsif Str (First_Exp + 1) in '-' | '+' then - Ptr.all = Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1 - else Ptr.all = - Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1))); + Ptr.all = + (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max)) + then First_Exp + elsif Str (First_Exp + 1) in '-' | '+' then + Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1 + else Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1))); pragma Assert (if not Overflow then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) = diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads index 25a095b57a0..117769d20cb 100644 --- a/gcc/ada/libgnat/s-vauspe.ads +++ b/gcc/ada/libgnat/s-vauspe.ads @@ -492,7 +492,8 @@ is Pre => Str'Last /= Positive'Last and then From in Str'Range and then To in From .. Str'Last - and then Str (From) in '0' .. '9'; + and then Str (From) in '0' .. '9', + Post => Raw_Unsigned_Last_Ghost'Result >= From; -- Ghost function that returns the position of the cursor once an unsigned -- number has been seen. diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb index bdd1bfb303e..7f04e22ae7f 100644 --- a/gcc/ada/libgnat/s-widthi.adb +++ b/gcc/ada/libgnat/s-widthi.adb @@ -166,9 +166,9 @@ begin end loop; declare - F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; - Q : constant Big_Integer := Big (T_Init) / F with Ghost; - R : constant Big_Integer := Big (T_Init) rem F with Ghost; + F : constant Big_Positive := Big_10 ** (W - 2) with Ghost; + Q : constant Big_Natural := Big (T_Init) / F with Ghost; + R : constant Big_Natural := Big (T_Init) rem F with Ghost; begin pragma Assert (Q < Big_10); pragma Assert (Big (T_Init) = Q * F + R); -- 2.40.0