From: Yannick Moy <moy@adacore.com>
Date: Wed, 2 Feb 2022 11:52:36 +0000 (+0100)
Subject: [Ada] Adapt proof of System.Arith_Double after update of Z3
X-Git-Tag: basepoints/gcc-14~6902
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=4c533da21d6298cdf9eb11df7353b8c8684c7756;p=thirdparty%2Fgcc.git

[Ada] Adapt proof of System.Arith_Double after update of Z3

Update to version 4.8.14 of prover Z3 requires minor adjustments of the
ghost code to add necessary intermediate assertions that drive the
automatic proof.

gcc/ada/

	* libgnat/s-aridou.adb (Double_Divide, Scaled_Divide): Add
	intermediate assertions.
---

diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 0fefb6bd945..ffb6f4ca269 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -924,6 +924,8 @@ is
             else
                Q := 0;
 
+               pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Yhi));
+               pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Zhi));
                pragma Assert (Big (Double_Uns'(Yhi * Zhi)) >= 1);
                if Yhi > 1 or else Zhi > 1 then
                   pragma Assert (Big (Double_Uns'(Yhi * Zhi)) > 1);
@@ -938,10 +940,12 @@ is
             return;
          else
             T2 := Yhi * Zlo;
+            pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo)));
          end if;
 
       else
          T2 := Ylo * Zhi;
+         pragma Assert (Big (T2) = Big (Double_Uns'(Ylo * Zhi)));
       end if;
 
       T1 := Ylo * Zlo;
@@ -1527,10 +1531,14 @@ is
             Raise_Error;
          else
             T2 := Xhi * Ylo;
+            pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo))
+                                    + Big (Double_Uns'(Xlo * Yhi)));
          end if;
 
       elsif Yhi /= 0 then
          T2 := Xlo * Yhi;
+         pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo))
+                                 + Big (Double_Uns'(Xlo * Yhi)));
 
       else -- Yhi = Xhi = 0
          T2 := 0;
@@ -1544,7 +1552,7 @@ is
       pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo))
                               + Big (Double_Uns'(Xlo * Yhi)));
       Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Xhi * Ylo)),
-                                          Big (Double_Uns'(Xlo * Yhi)));
+                                              Big (Double_Uns'(Xlo * Yhi)));
       pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1));
       Lemma_Add_Commutation (T2, Hi (T1));
       pragma Assert
@@ -2575,7 +2583,13 @@ is
                                       Big (Double_Uns (Qd (J))) - 1,
                                       Big (Double_Uns (Qd (J) - 1)), 0);
 
-                  Qd (J) := Qd (J) - 1;
+                  declare
+                     Prev : constant Single_Uns := Qd (J) - 1 with Ghost;
+                  begin
+                     Qd (J) := Qd (J) - 1;
+
+                     pragma Assert (Qd (J) = Prev);
+                  end;
 
                   pragma Assert
                     (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));