From 8ebdd4431829c61228ec92f906cb9f7a2141325f Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 23 Jan 2023 17:09:40 +0000 Subject: ada: Update proof of runtime units 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. --- 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); -- cgit v1.2.1