diff mbox series

[COMMITTED] ada: Adapt proof of runtime units

Message ID 20240507080017.37354-1-poulhies@adacore.com
State New
Headers show
Series [COMMITTED] ada: Adapt proof of runtime units | expand

Commit Message

Marc Poulhiès May 7, 2024, 8 a.m. UTC 
From: Yannick Moy <moy@adacore.com>

Restore proof of runtime units after changes in SPARK.

gcc/ada/

	* libgnat/a-strsea.adb (Index): Add assertions.
	* libgnat/a-strsup.ads ("="): Remove useless precondition.
	* libgnat/s-aridou.adb (Prove_Rounding_Case): Add assertions.
	(Lemma_Shift_Right): Add call to lemma.
	* libgnat/s-arit32.adb (Prove_Rounding_Case): Add assertion.
	(Prove_ Signs): Add assertions.
	(Scaled_Divide32): Add assertions.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-strsea.adb |  2 ++
 gcc/ada/libgnat/a-strsup.ads |  1 -
 gcc/ada/libgnat/s-aridou.adb |  9 +++++++--
 gcc/ada/libgnat/s-arit32.adb | 17 +++++++++++++++--
 4 files changed, 24 insertions(+), 5 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb
index 1dad3be4f4a..54f12199fcc 100644
--- a/gcc/ada/libgnat/a-strsea.adb
+++ b/gcc/ada/libgnat/a-strsea.adb
@@ -623,6 +623,7 @@  package body Ada.Strings.Search with SPARK_Mode is
            (if (for some J in From .. Source'Last - PL1 =>
                  Match (Source, Pattern, Mapping, J))
             then Result in From .. Source'Last - PL1
+              and then Match (Source, Pattern, Mapping, Result)
             else Result = 0);
 
       else
@@ -636,6 +637,7 @@  package body Ada.Strings.Search with SPARK_Mode is
            (if (for some J in Source'First .. From - PL1 =>
                   Match (Source, Pattern, Mapping, J))
             then Result in Source'First .. From - PL1
+              and then Match (Source, Pattern, Mapping, Result)
             else Result = 0);
       end if;
 
diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads
index cb1dcc9a076..6c360f1982b 100644
--- a/gcc/ada/libgnat/a-strsup.ads
+++ b/gcc/ada/libgnat/a-strsup.ads
@@ -689,7 +689,6 @@  is
      (Left  : Super_String;
       Right : Super_String) return Boolean
    with
-     Pre    => Left.Max_Length = Right.Max_Length,
      Post   => "="'Result = (Super_To_String (Left) = Super_To_String (Right)),
      Global => null;
 
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index ac25e6a9183..6f27487db37 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -971,7 +971,7 @@  is
       procedure Prove_Rounding_Case is
       begin
          if Same_Sign (Big (X), Big (Y) * Big (Z)) then
-            null;
+            pragma Assert (abs Big_Q = Big (Qu));
          end if;
       end Prove_Rounding_Case;
 
@@ -1603,6 +1603,7 @@  is
          pragma Loop_Invariant (XX = Shift_Right (X, J));
          pragma Loop_Invariant (XX = X / Double_Uns'(2) ** J);
       end loop;
+      Lemma_Div_Commutation (X, Double_Uns'(2) ** Shift);
    end Lemma_Shift_Right;
 
    ------------------------------
@@ -2441,7 +2442,11 @@  is
       procedure Prove_Rounding_Case is
       begin
          if Same_Sign (Big (X) * Big (Y), Big (Z)) then
-            null;
+            pragma Assert
+              (abs Big_Q =
+                 (if Ru > (Zu - Double_Uns'(1)) / Double_Uns'(2)
+                  then abs Quot + 1
+                  else abs Quot));
          end if;
       end Prove_Rounding_Case;
 
diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
index 59a6db08199..221ef1e635e 100644
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -415,7 +415,11 @@  is
       procedure Prove_Rounding_Case is
       begin
          if Same_Sign (Big (X) * Big (Y), Big (Z)) then
-            null;
+            pragma Assert
+              (abs Big_Q =
+                 (if Ru > (Zu - Uns32'(1)) / Uns32'(2)
+                  then abs Quot + 1
+                  else abs Quot));
          end if;
       end Prove_Rounding_Case;
 
@@ -432,7 +436,14 @@  is
       -- Prove_Signs --
       -----------------
 
-      procedure Prove_Signs is null;
+      procedure Prove_Signs is
+      begin
+         if (X >= 0) = (Y >= 0) then
+            pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q);
+         else
+            pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q);
+         end if;
+      end Prove_Signs;
 
    --  Start of processing for Scaled_Divide32
 
@@ -483,6 +494,8 @@  is
       Lemma_Div_Commutation (D, Uns64 (Zu));
       Lemma_Rem_Commutation (D, Uns64 (Zu));
 
+      pragma Assert (Uns64 (Qu) = D / Uns64 (Zu));
+      pragma Assert (Uns64 (Ru) = D rem Uns64 (Zu));
       pragma Assert (Big (Ru) = abs Big_R);
       pragma Assert (Big (Qu) = abs Quot);
       pragma Assert (Big (Zu) = Big (Uns32'(abs Z)));