* [COMMITTED] ada: Update proof of runtime units
@ 2023-05-16 8:41 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-05-16 8:41 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
From: Yannick Moy <moy@adacore.com>
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-05-16 8:41 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-05-16 8:41 [COMMITTED] ada: Update proof of runtime units Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).