public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-6226] [Ada] Rename parameter-dependent constants in generic unit
@ 2022-01-05 11:33 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-01-05 11:33 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:1a056c2788630270b37066a1ac76d1e64ac6e194
commit r12-6226-g1a056c2788630270b37066a1ac76d1e64ac6e194
Author: Yannick Moy <moy@adacore.com>
Date: Mon Nov 29 17:52:56 2021 +0100
[Ada] Rename parameter-dependent constants in generic unit
gcc/ada/
* libgnat/s-aridou.adb: Apply replacement.
Diff:
---
gcc/ada/libgnat/s-aridou.adb | 365 +++++++++++++++++++++++--------------------
1 file changed, 194 insertions(+), 171 deletions(-)
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 57d427b147e..c93636a309f 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -64,10 +64,7 @@ is
when others => raise Program_Error)
with Ghost;
- -- Power-of-two constants. Use the names Big_2xx32, Big_2xx63 and Big_2xx64
- -- even if Single_Size might not be 32 and Double_Size might not be 64, as
- -- this facilitates code and proof understanding, compared to more generic
- -- names.
+ -- Power-of-two constants
pragma Warnings
(Off, "non-preelaborable call not allowed in preelaborated unit",
@@ -78,13 +75,13 @@ is
Big_0 : constant Big_Integer :=
Big (Double_Uns'(0))
with Ghost;
- Big_2xx32 : constant Big_Integer :=
+ Big_2xxSingle : constant Big_Integer :=
Big (Double_Int'(2 ** Single_Size))
with Ghost;
- Big_2xx63 : constant Big_Integer :=
+ Big_2xxDouble_Minus_1 : constant Big_Integer :=
Big (Double_Uns'(2 ** (Double_Size - 1)))
with Ghost;
- Big_2xx64 : constant Big_Integer :=
+ Big_2xxDouble : constant Big_Integer :=
Big (Double_Uns'(2 ** Double_Size - 1)) + 1
with Ghost;
pragma Warnings
@@ -137,8 +134,9 @@ is
-- 2**N as a big integer
function Big3 (X1, X2, X3 : Single_Uns) return Big_Integer is
- (Big_2xx32 * Big_2xx32 * Big (Double_Uns (X1))
- + Big_2xx32 * Big (Double_Uns (X2)) + Big (Double_Uns (X3)))
+ (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (X1))
+ + Big_2xxSingle * Big (Double_Uns (X2))
+ + Big (Double_Uns (X3)))
with Ghost;
-- X1&X2&X3 as a big integer
@@ -353,8 +351,8 @@ is
with
Ghost,
Pre => Xhi = Hi (Xu) and Xlo = Lo (Xu),
- Post =>
- Big (Xu) = Big_2xx32 * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo));
+ Post => Big (Xu) =
+ Big_2xxSingle * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo));
procedure Lemma_Hi_Lo_3 (Xu : Double_Uns; Xhi, Xlo : Single_Uns)
with
@@ -365,7 +363,7 @@ is
procedure Lemma_Lo_Is_Ident (X : Double_Uns)
with
Ghost,
- Pre => Big (X) < Big_2xx32,
+ Pre => Big (X) < Big_2xxSingle,
Post => Double_Uns (Lo (X)) = X;
procedure Lemma_Lt_Commutation (A, B : Double_Uns)
@@ -396,7 +394,7 @@ is
procedure Lemma_Mult_Commutation (X, Y, Z : Double_Uns)
with
Ghost,
- Pre => Big (X) * Big (Y) < Big_2xx64 and then Z = X * Y,
+ Pre => Big (X) * Big (Y) < Big_2xxDouble and then Z = X * Y,
Post => Big (X) * Big (Y) = Big (Z);
procedure Lemma_Mult_Decomposition
@@ -411,9 +409,9 @@ is
and then Yhi = Hi (Yu)
and then Ylo = Lo (Yu),
Post => Mult =
- Big_2xx32 * Big_2xx32 * (Big (Double_Uns'(Xhi * Yhi)))
- + Big_2xx32 * (Big (Double_Uns'(Xhi * Ylo)))
- + Big_2xx32 * (Big (Double_Uns'(Xlo * Yhi)))
+ Big_2xxSingle * Big_2xxSingle * (Big (Double_Uns'(Xhi * Yhi)))
+ + Big_2xxSingle * (Big (Double_Uns'(Xhi * Ylo)))
+ + Big_2xxSingle * (Big (Double_Uns'(Xlo * Yhi)))
+ (Big (Double_Uns'(Xlo * Ylo)));
procedure Lemma_Mult_Distribution (X, Y, Z : Big_Integer)
@@ -435,8 +433,8 @@ is
procedure Lemma_Not_In_Range_Big2xx64
with
- Post => not In_Double_Int_Range (Big_2xx64)
- and then not In_Double_Int_Range (-Big_2xx64);
+ Post => not In_Double_Int_Range (Big_2xxDouble)
+ and then not In_Double_Int_Range (-Big_2xxDouble);
procedure Lemma_Powers_Of_2 (M, N : Natural)
with
@@ -446,7 +444,7 @@ is
and then M + N <= Double_Size,
Post =>
Big_2xx (M) * Big_2xx (N) =
- (if M + N = Double_Size then Big_2xx64 else Big_2xx (M + N));
+ (if M + N = Double_Size then Big_2xxDouble else Big_2xx (M + N));
procedure Lemma_Powers_Of_2_Commutation (M : Natural)
with
@@ -454,7 +452,7 @@ is
Subprogram_Variant => (Decreases => M),
Pre => M <= Double_Size,
Post => Big (Double_Uns'(2))**M =
- (if M < Double_Size then Big_2xx (M) else Big_2xx64);
+ (if M < Double_Size then Big_2xx (M) else Big_2xxDouble);
procedure Lemma_Powers_Of_2_Increasing (M, N : Natural)
with
@@ -541,7 +539,7 @@ is
procedure Lemma_Word_Commutation (X : Single_Uns)
with
Ghost,
- Post => Big_2xx32 * Big (Double_Uns (X))
+ Post => Big_2xxSingle * Big (Double_Uns (X))
= Big (2**Single_Size * Double_Uns (X));
-----------------------------
@@ -772,9 +770,11 @@ is
procedure Prove_Quotient_Zero
with
Ghost,
- Pre => Mult >= Big_2xx64
+ Pre => Mult >= Big_2xxDouble
and then
- not (Mult = Big_2xx64 and then X = Double_Int'First and then Round)
+ not (Mult = Big_2xxDouble
+ and then X = Double_Int'First
+ and then Round)
and then Q = 0
and then R = X,
Post => Big (R) = Big (X) rem (Big (Y) * Big (Z))
@@ -790,7 +790,7 @@ is
procedure Prove_Round_To_One
with
Ghost,
- Pre => Mult = Big_2xx64
+ Pre => Mult = Big_2xxDouble
and then X = Double_Int'First
and then Q = (if Den_Pos then -1 else 1)
and then R = X
@@ -944,28 +944,32 @@ is
pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo))
+ Big (Double_Uns'(Ylo * Zhi)));
- Lemma_Mult_Distribution (Big_2xx32, Big (Double_Uns'(Yhi * Zlo)),
- Big (Double_Uns'(Ylo * Zhi)));
- pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (T1));
+ Lemma_Mult_Distribution (Big_2xxSingle,
+ Big (Double_Uns'(Yhi * Zlo)),
+ Big (Double_Uns'(Ylo * Zhi)));
+ pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1));
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
pragma Assert
- (Mult = Big_2xx32 * Big (T2)
- + Big_2xx32 * Big (Double_Uns (Hi (T1)))
- + Big (Double_Uns (Lo (T1))));
- Lemma_Mult_Distribution (Big_2xx32, Big (T2),
- Big (Double_Uns (Hi (T1))));
+ (Mult = Big_2xxSingle * Big (T2)
+ + Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ + Big (Double_Uns (Lo (T1))));
+ Lemma_Mult_Distribution (Big_2xxSingle,
+ Big (T2),
+ Big (Double_Uns (Hi (T1))));
Lemma_Add_Commutation (T2, Hi (T1));
T2 := T2 + Hi (T1);
- pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1))));
+ pragma Assert
+ (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1))));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
- Lemma_Mult_Distribution (Big_2xx32, Big (Double_Uns (Hi (T2))),
- Big (Double_Uns (Lo (T2))));
+ Lemma_Mult_Distribution (Big_2xxSingle,
+ Big (Double_Uns (Hi (T2))),
+ Big (Double_Uns (Lo (T2))));
pragma Assert
- (Mult = Big_2xx64 * Big (Double_Uns (Hi (T2)))
- + Big_2xx32 * Big (Double_Uns (Lo (T2)))
- + Big (Double_Uns (Lo (T1))));
+ (Mult = Big_2xxDouble * Big (Double_Uns (Hi (T2)))
+ + Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+ + Big (Double_Uns (Lo (T1))));
if Hi (T2) /= 0 then
R := X;
@@ -988,7 +992,7 @@ is
pragma Assert (Big (Double_Uns (Hi (T2))) >= 1);
pragma Assert (Big (Double_Uns (Lo (T2))) >= 0);
pragma Assert (Big (Double_Uns (Lo (T1))) >= 0);
- pragma Assert (Mult >= Big_2xx64);
+ pragma Assert (Mult >= Big_2xxDouble);
if Hi (T2) > 1 then
pragma Assert (Big (Double_Uns (Hi (T2))) > 1);
elsif Lo (T2) > 0 then
@@ -1195,22 +1199,24 @@ is
Lemma_Hi_Lo (Yu, Yhi, Ylo);
pragma Assert
- (Mult = (Big_2xx32 * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo))) *
- (Big_2xx32 * Big (Double_Uns (Yhi)) + Big (Double_Uns (Ylo))));
+ (Mult =
+ (Big_2xxSingle * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo))) *
+ (Big_2xxSingle * Big (Double_Uns (Yhi)) + Big (Double_Uns (Ylo))));
pragma Assert (Mult =
- Big_2xx32 * Big_2xx32 * Big (Double_Uns (Xhi)) * Big (Double_Uns (Yhi))
- + Big_2xx32 * Big (Double_Uns (Xhi)) * Big (Double_Uns (Ylo))
- + Big_2xx32 * Big (Double_Uns (Xlo)) * Big (Double_Uns (Yhi))
- + Big (Double_Uns (Xlo)) * Big (Double_Uns (Ylo)));
- Lemma_Deep_Mult_Commutation (Big_2xx32 * Big_2xx32, Xhi, Yhi);
- Lemma_Deep_Mult_Commutation (Big_2xx32, Xhi, Ylo);
- Lemma_Deep_Mult_Commutation (Big_2xx32, Xlo, Yhi);
+ Big_2xxSingle
+ * Big_2xxSingle * Big (Double_Uns (Xhi)) * Big (Double_Uns (Yhi))
+ + Big_2xxSingle * Big (Double_Uns (Xhi)) * Big (Double_Uns (Ylo))
+ + Big_2xxSingle * Big (Double_Uns (Xlo)) * Big (Double_Uns (Yhi))
+ + Big (Double_Uns (Xlo)) * Big (Double_Uns (Ylo)));
+ Lemma_Deep_Mult_Commutation (Big_2xxSingle * Big_2xxSingle, Xhi, Yhi);
+ Lemma_Deep_Mult_Commutation (Big_2xxSingle, Xhi, Ylo);
+ Lemma_Deep_Mult_Commutation (Big_2xxSingle, Xlo, Yhi);
Lemma_Mult_Commutation (Xlo, Ylo);
pragma Assert (Mult =
- Big_2xx32 * Big_2xx32 * Big (Double_Uns'(Xhi * Yhi))
- + Big_2xx32 * Big (Double_Uns'(Xhi * Ylo))
- + Big_2xx32 * Big (Double_Uns'(Xlo * Yhi))
- + Big (Double_Uns'(Xlo * Ylo)));
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns'(Xhi * Yhi))
+ + Big_2xxSingle * Big (Double_Uns'(Xhi * Ylo))
+ + Big_2xxSingle * Big (Double_Uns'(Xlo * Yhi))
+ + Big (Double_Uns'(Xlo * Ylo)));
end Lemma_Mult_Decomposition;
-------------------
@@ -1383,9 +1389,9 @@ is
Pre => Xhi /= 0
and then Yhi /= 0
and then Mult =
- Big_2xx32 * Big_2xx32 * (Big (Double_Uns'(Xhi * Yhi)))
- + Big_2xx32 * (Big (Double_Uns'(Xhi * Ylo)))
- + Big_2xx32 * (Big (Double_Uns'(Xlo * Yhi)))
+ Big_2xxSingle * Big_2xxSingle * (Big (Double_Uns'(Xhi * Yhi)))
+ + Big_2xxSingle * (Big (Double_Uns'(Xhi * Ylo)))
+ + Big_2xxSingle * (Big (Double_Uns'(Xlo * Yhi)))
+ (Big (Double_Uns'(Xlo * Ylo))),
Post => not In_Double_Int_Range (Big (X) * Big (Y));
@@ -1393,7 +1399,7 @@ is
with
Ghost,
Pre => In_Double_Int_Range (Big (X) * Big (Y))
- and then Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1)))
+ and then Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))
and then Hi (T2) = 0,
Post => Mult = Big (Lo (T2) & Lo (T1));
@@ -1416,14 +1422,14 @@ is
procedure Prove_Result_Too_Large
with
Ghost,
- Pre => Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1)))
+ Pre => Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))
and then Hi (T2) /= 0,
Post => not In_Double_Int_Range (Big (X) * Big (Y));
procedure Prove_Too_Large
with
Ghost,
- Pre => abs (Big (X) * Big (Y)) >= Big_2xx64,
+ Pre => abs (Big (X) * Big (Y)) >= Big_2xxDouble,
Post => not In_Double_Int_Range (Big (X) * Big (Y));
--------------------------
@@ -1432,10 +1438,10 @@ is
procedure Prove_Both_Too_Large is
begin
- pragma Assert
- (Mult >= Big_2xx32 * Big_2xx32 * Big (Double_Uns'(Xhi * Yhi)));
+ pragma Assert (Mult >=
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns'(Xhi * Yhi)));
pragma Assert (Double_Uns (Xhi) * Double_Uns (Yhi) >= 1);
- pragma Assert (Mult >= Big_2xx32 * Big_2xx32);
+ pragma Assert (Mult >= Big_2xxSingle * Big_2xxSingle);
Prove_Too_Large;
end Prove_Both_Too_Large;
@@ -1446,9 +1452,9 @@ is
procedure Prove_Final_Decomposition is
begin
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
- pragma Assert (Mult = Big_2xx32 * Big (Double_Uns (Lo (T2)))
- + Big (Double_Uns (Lo (T1))));
- pragma Assert (Mult <= Big_2xx63);
+ pragma Assert (Mult = Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+ + Big (Double_Uns (Lo (T1))));
+ pragma Assert (Mult <= Big_2xxDouble_Minus_1);
Lemma_Mult_Commutation (X, Y);
pragma Assert (Mult = abs (Big (X * Y)));
Lemma_Word_Commutation (Lo (T2));
@@ -1490,12 +1496,12 @@ is
procedure Prove_Result_Too_Large is
begin
- pragma Assert (Mult >= Big_2xx32 * Big (T2));
+ pragma Assert (Mult >= Big_2xxSingle * Big (T2));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
- pragma Assert
- (Mult >= Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T2))));
+ pragma Assert (Mult >=
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))));
pragma Assert (Double_Uns (Hi (T2)) >= 1);
- pragma Assert (Mult >= Big_2xx32 * Big_2xx32);
+ pragma Assert (Mult >= Big_2xxSingle * Big_2xxSingle);
Prove_Too_Large;
end Prove_Result_Too_Large;
@@ -1532,9 +1538,9 @@ is
pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo))
+ Big (Double_Uns'(Xlo * Yhi)));
- Lemma_Mult_Distribution (Big_2xx32, Big (Double_Uns'(Xhi * Ylo)),
+ Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Xhi * Ylo)),
Big (Double_Uns'(Xlo * Yhi)));
- pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (T1));
+ pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1));
Lemma_Add_Commutation (T2, Hi (T1));
pragma Assert
(Big (T2 + Hi (T1)) = Big (T2) + Big (Double_Uns (Hi (T1))));
@@ -1542,7 +1548,8 @@ is
T2 := T2 + Hi (T1);
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
- pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1))));
+ pragma Assert
+ (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1))));
if Hi (T2) /= 0 then
Prove_Result_Too_Large;
@@ -1656,19 +1663,21 @@ is
Pre => D'Initialized
and then Scale <= Single_Size
and then Mult =
- Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1)))
- + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
+ Big_2xxSingle
+ * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4)))
- and then Big (D (1) & D (2)) * Big_2xx (Scale) < Big_2xx64
+ and then Big (D (1) & D (2)) * Big_2xx (Scale) < Big_2xxDouble
and then T1 = Shift_Left (D (1) & D (2), Scale)
and then T2 = Shift_Left (Double_Uns (D (3)), Scale)
and then T3 = Shift_Left (Double_Uns (D (4)), Scale),
Post => Mult * Big_2xx (Scale) =
- Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T1)))
- + Big_2xx32 * Big_2xx32 * Big (Double_Uns (Lo (T1) or
+ Big_2xxSingle
+ * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1) or
Hi (T2)))
- + Big_2xx32 * Big (Double_Uns (Lo (T2) or
+ + Big_2xxSingle * Big (Double_Uns (Lo (T2) or
Hi (T3)))
+ Big (Double_Uns (Lo (T3)));
-- Proves the scaling of the 4-digit dividend actually multiplies it by
@@ -1712,7 +1721,8 @@ is
procedure Prove_Overflow
with
Ghost,
- Pre => Z /= 0 and then Mult >= Big_2xx64 * Big (Double_Uns'(abs Z)),
+ Pre => Z /= 0
+ and then Mult >= Big_2xxDouble * Big (Double_Uns'(abs Z)),
Post => not In_Double_Int_Range (Big (X) * Big (Y) / Big (Z))
and then not In_Double_Int_Range
(Round_Quotient (Big (X) * Big (Y), Big (Z),
@@ -1762,7 +1772,7 @@ is
with
Ghost,
Pre => In_Double_Int_Range (Big_Q)
- and then abs Big_Q = Big_2xx64,
+ and then abs Big_Q = Big_2xxDouble,
Post => False;
-- Proves the inconsistency when Q is equal to Big_2xx64
@@ -1833,9 +1843,10 @@ is
and then D'Initialized
and then Hi (abs Z) = 0
and then Lo (abs Z) = Zlo
- and then Mult = Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4)))
+ and then Mult =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4)))
and then D (2) < Zlo
and then Quot = (Big (X) * Big (Y)) / Big (Z)
and then Big_R = (Big (X) * Big (Y)) rem Big (Z)
@@ -1855,14 +1866,15 @@ is
begin
Lemma_Hi_Lo (D (1) & D (2), D (1), D (2));
pragma Assert (Mult * Big_2xx (Scale) =
- Big_2xx32 * Big_2xx32 * Big_2xx (Scale) * Big (D (1) & D (2))
- + Big_2xx32 * Big_2xx (Scale) * Big (Double_Uns (D (3)))
- + Big_2xx (Scale) * Big (Double_Uns (D (4))));
+ Big_2xxSingle
+ * Big_2xxSingle * Big_2xx (Scale) * Big (D (1) & D (2))
+ + Big_2xxSingle * Big_2xx (Scale) * Big (Double_Uns (D (3)))
+ + Big_2xx (Scale) * Big (Double_Uns (D (4))));
pragma Assert (Big_2xx (Scale) > 0);
- Lemma_Lt_Mult (Big (Double_Uns (D (3))), Big_2xx32,
- Big_2xx (Scale), Big_2xx64);
- Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xx32,
- Big_2xx (Scale), Big_2xx64);
+ Lemma_Lt_Mult (Big (Double_Uns (D (3))), Big_2xxSingle,
+ Big_2xx (Scale), Big_2xxDouble);
+ Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xxSingle,
+ Big_2xx (Scale), Big_2xxDouble);
Lemma_Mult_Commutation (2 ** Scale, D (1) & D (2), T1);
declare
Big_D12 : constant Big_Integer :=
@@ -1870,8 +1882,8 @@ is
Big_T1 : constant Big_Integer := Big (T1);
begin
pragma Assert (Big_D12 = Big_T1);
- pragma Assert (Big_2xx32 * Big_2xx32 * Big_D12
- = Big_2xx32 * Big_2xx32 * Big_T1);
+ pragma Assert (Big_2xxSingle * Big_2xxSingle * Big_D12
+ = Big_2xxSingle * Big_2xxSingle * Big_T1);
end;
Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (3)), T2);
declare
@@ -1880,7 +1892,7 @@ is
Big_T2 : constant Big_Integer := Big (T2);
begin
pragma Assert (Big_D3 = Big_T2);
- pragma Assert (Big_2xx32 * Big_D3 = Big_2xx32 * Big_T2);
+ pragma Assert (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2);
end;
Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (4)), T3);
declare
@@ -1891,7 +1903,9 @@ is
pragma Assert (Big_D4 = Big_T3);
end;
pragma Assert (Mult * Big_2xx (Scale) =
- Big_2xx32 * Big_2xx32 * Big (T1) + Big_2xx32 * Big (T2) + Big (T3));
+ Big_2xxSingle * Big_2xxSingle * Big (T1)
+ + Big_2xxSingle * Big (T2)
+ + Big (T3));
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
Lemma_Hi_Lo (T3, Hi (T3), Lo (T3));
@@ -1912,10 +1926,10 @@ is
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
Lemma_Hi_Lo (T3, Hi (T3), S2);
pragma Assert (Big (Double_Uns (Q)) * Big (Zu) =
- Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T2)))
- + Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T3)))
- + Big_2xx32 * Big (Double_Uns (S2))
- + Big (Double_Uns (S3)));
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3)))
+ + Big_2xxSingle * Big (Double_Uns (S2))
+ + Big (Double_Uns (S3)));
pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1));
Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2));
pragma Assert
@@ -1938,7 +1952,7 @@ is
procedure Prove_Overflow is
begin
- Lemma_Div_Ge (Mult, Big_2xx64, Big (Double_Uns'(abs Z)));
+ Lemma_Div_Ge (Mult, Big_2xxDouble, Big (Double_Uns'(abs Z)));
Lemma_Abs_Commutation (Z);
Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
end Prove_Overflow;
@@ -1962,9 +1976,9 @@ is
Lemma_Lt_Commutation (Double_Uns (D (J)), Double_Uns (Zhi));
Lemma_Gt_Mult (Big (Double_Uns (Zhi)),
Big (Double_Uns (D (J))) + 1,
- Big_2xx32, Big (D (J) & D (J + 1)));
+ Big_2xxSingle, Big (D (J) & D (J + 1)));
Lemma_Div_Lt
- (Big (D (J) & D (J + 1)), Big_2xx32, Big (Double_Uns (Zhi)));
+ (Big (D (J) & D (J + 1)), Big_2xxSingle, Big (Double_Uns (Zhi)));
Lemma_Div_Commutation (D (J) & D (J + 1), Double_Uns (Zhi));
Lemma_Lo_Is_Ident ((D (J) & D (J + 1)) / Zhi);
Lemma_Div_Definition (D (J) & D (J + 1), Zhi, Double_Uns (Qd (J)),
@@ -1973,10 +1987,10 @@ is
((D (J) & D (J + 1)) rem Zhi, Double_Uns (Zhi));
Lemma_Gt_Mult
((Big (Double_Uns (Qd (J))) + 1) * Big (Double_Uns (Zhi)),
- Big (D (J) & D (J + 1)) + 1, Big_2xx32,
+ Big (D (J) & D (J + 1)) + 1, Big_2xxSingle,
Big3 (D (J), D (J + 1), D (J + 2)));
Lemma_Hi_Lo (Zu, Zhi, Lo (Zu));
- Lemma_Gt_Mult (Big (Zu), Big_2xx32 * Big (Double_Uns (Zhi)),
+ Lemma_Gt_Mult (Big (Zu), Big_2xxSingle * Big (Double_Uns (Zhi)),
Big (Double_Uns (Qd (J))) + 1,
Big3 (D (J), D (J + 1), D (J + 2)));
Lemma_Div_Lt (Big3 (D (J), D (J + 1), D (J + 2)),
@@ -1989,7 +2003,7 @@ is
procedure Prove_Q_Too_Big is
begin
- pragma Assert (Big_Q = Big_2xx64 or Big_Q = -Big_2xx64);
+ pragma Assert (Big_Q = Big_2xxDouble or Big_Q = -Big_2xxDouble);
Lemma_Not_In_Range_Big2xx64;
end Prove_Q_Too_Big;
@@ -2055,16 +2069,16 @@ is
Lemma_Div_Definition (T2, Zlo, T2 / Zlo, Ru);
pragma Assert
(Mult = Big (Double_Uns (Zlo)) *
- (Big_2xx32 * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru));
- Lemma_Div_Lt (Big (T1), Big_2xx32, Big (Double_Uns (Zlo)));
+ (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru));
+ Lemma_Div_Lt (Big (T1), Big_2xxSingle, Big (Double_Uns (Zlo)));
Lemma_Div_Commutation (T1, Double_Uns (Zlo));
Lemma_Lo_Is_Ident (T1 / Zlo);
- Lemma_Div_Lt (Big (T2), Big_2xx32, Big (Double_Uns (Zlo)));
+ Lemma_Div_Lt (Big (T2), Big_2xxSingle, Big (Double_Uns (Zlo)));
Lemma_Div_Commutation (T2, Double_Uns (Zlo));
Lemma_Lo_Is_Ident (T2 / Zlo);
Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / Zlo));
Lemma_Substitution (Mult, Big (Double_Uns (Zlo)),
- Big_2xx32 * Big (T1 / Zlo) + Big (T2 / Zlo),
+ Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo),
Big (Qu), Big (Ru));
Lemma_Lt_Commutation (Ru, Double_Uns (Zlo));
Lemma_Rev_Div_Definition
@@ -2110,7 +2124,7 @@ is
T2 := D (3) + Lo (T1);
- Lemma_Mult_Distribution (Big_2xx32,
+ Lemma_Mult_Distribution (Big_2xxSingle,
Big (Double_Uns (D (3))),
Big (Double_Uns (Lo (T1))));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
@@ -2159,9 +2173,10 @@ is
Big (Double_Uns (D (1))));
pragma Assert (Mult =
- Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1)))
- + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
+ Big_2xxSingle
+ * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4))));
else
@@ -2169,9 +2184,10 @@ is
end if;
pragma Assert (Mult =
- Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1)))
- + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
+ Big_2xxSingle
+ * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4))));
else
@@ -2182,7 +2198,7 @@ is
T2 := D (3) + Lo (T1);
- Lemma_Mult_Distribution (Big_2xx32,
+ Lemma_Mult_Distribution (Big_2xxSingle,
Big (Double_Uns (D (3))),
Big (Double_Uns (Lo (T1))));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
@@ -2196,27 +2212,28 @@ is
pragma Assert
(Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) =
Big (Double_Uns (D (2))));
- pragma Assert
- (Mult = Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
+ pragma Assert (Mult =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4))));
else
D (2) := 0;
- pragma Assert
- (Mult = Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
+ pragma Assert (Mult =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4))));
end if;
D (1) := 0;
end if;
- pragma Assert
- (Mult = Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1)))
- + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4))));
+ pragma Assert (Mult =
+ Big_2xxSingle
+ * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4))));
-- Now it is time for the dreaded multiple precision division. First an
-- easy case, check for the simple case of a one digit divisor.
@@ -2225,14 +2242,14 @@ is
if D (1) /= 0 or else D (2) >= Zlo then
if D (1) > 0 then
pragma Assert
- (Mult >= Big_2xx32 * Big_2xx32 * Big_2xx32
+ (Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
* Big (Double_Uns (D (1))));
- pragma Assert (Mult >= Big_2xx64 * Big_2xx32);
+ pragma Assert (Mult >= Big_2xxDouble * Big_2xxSingle);
Lemma_Ge_Commutation (2 ** Single_Size, Zu);
- pragma Assert (Mult >= Big_2xx64 * Big (Zu));
+ pragma Assert (Mult >= Big_2xxDouble * Big (Zu));
else
Lemma_Ge_Commutation (Double_Uns (D (2)), Zu);
- pragma Assert (Mult >= Big_2xx64 * Big (Zu));
+ pragma Assert (Mult >= Big_2xxDouble * Big (Zu));
end if;
Prove_Overflow;
@@ -2387,7 +2404,7 @@ is
Lemma_Lt_Commutation (D (1) & D (2), abs Z);
Lemma_Lt_Mult (Big (D (1) & D (2)),
Big (Double_Uns'(abs Z)), Big_2xx (Scale),
- Big_2xx64);
+ Big_2xxDouble);
T1 := Shift_Left (D (1) & D (2), Scale);
T2 := Shift_Left (Double_Uns (D (3)), Scale);
@@ -2401,21 +2418,23 @@ is
D (4) := Lo (T3);
pragma Assert (Mult * Big_2xx (Scale) =
- Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1)))
- + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2)))
- + Big_2xx32 * Big (Double_Uns (D (3)))
+ Big_2xxSingle
+ * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4))));
- Lemma_Substitution (Big_2xx64 * Big (Zu), Big_2xx64, Big (Zu),
+ Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu),
Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0);
- Lemma_Lt_Mult (Mult, Big_2xx64 * Big (Double_Uns'(abs Z)),
- Big_2xx (Scale), Big_2xx64 * Big (Zu));
- Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xx64);
- Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xx32,
- Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1)))
- + Big_2xx32 * Big (Double_Uns (D (2)))
- + Big (Double_Uns (D (3))),
- Big3 (D (1), D (2), D (3)),
- Big (Double_Uns (D (4))));
+ Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)),
+ Big_2xx (Scale), Big_2xxDouble * Big (Zu));
+ Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xxDouble);
+ Lemma_Substitution
+ (Mult * Big_2xx (Scale), Big_2xxSingle,
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
+ + Big_2xxSingle * Big (Double_Uns (D (2)))
+ + Big (Double_Uns (D (3))),
+ Big3 (D (1), D (2), D (3)),
+ Big (Double_Uns (D (4))));
-- Loop to compute quotient digits, runs twice for Qd (1) and Qd (2)
@@ -2427,7 +2446,7 @@ is
Ghost,
Pre => X1 = 0,
Post =>
- Big_2xx32 * Big3 (X1, X2, X3) + Big (Double_Uns (X4))
+ Big_2xxSingle * Big3 (X1, X2, X3) + Big (Double_Uns (X4))
= Big3 (X2, X3, X4);
---------------------------
@@ -2463,10 +2482,11 @@ is
Qd (J) := Single_Uns'Last;
Lemma_Gt_Mult (Big (Zu), Big (D (J) & D (J + 1)) + 1,
- Big_2xx32,
+ Big_2xxSingle,
Big3 (D (J), D (J + 1), D (J + 2)));
Lemma_Div_Lt
- (Big3 (D (J), D (J + 1), D (J + 2)), Big_2xx32, Big (Zu));
+ (Big3 (D (J), D (J + 1), D (J + 2)),
+ Big_2xxSingle, Big (Zu));
else
Qd (J) := Lo ((D (J) & D (J + 1)) / Zhi);
@@ -2548,50 +2568,52 @@ is
pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
if D (J) > 0 then
- pragma Assert (Big_2xx32 * Big_2xx32 = Big_2xx64);
+ pragma Assert
+ (Big_2xxSingle * Big_2xxSingle = Big_2xxDouble);
pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) =
- Big_2xx32 * Big_2xx32
- * Big (Double_Uns (D (J)))
- + Big_2xx32 * Big (Double_Uns (D (J + 1)))
- + Big (Double_Uns (D (J + 2))));
+ Big_2xxSingle
+ * Big_2xxSingle * Big (Double_Uns (D (J)))
+ + Big_2xxSingle * Big (Double_Uns (D (J + 1)))
+ + Big (Double_Uns (D (J + 2))));
pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) =
- Big_2xx64 * Big (Double_Uns (D (J)))
- + Big_2xx32 * Big (Double_Uns (D (J + 1)))
- + Big (Double_Uns (D (J + 2))));
+ Big_2xxDouble * Big (Double_Uns (D (J)))
+ + Big_2xxSingle * Big (Double_Uns (D (J + 1)))
+ + Big (Double_Uns (D (J + 2))));
pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) >=
- Big_2xx64 * Big (Double_Uns (D (J))));
+ Big_2xxDouble * Big (Double_Uns (D (J))));
Lemma_Ge_Commutation (Double_Uns (D (J)), Double_Uns'(1));
pragma Assert
- (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xx64);
+ (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xxDouble);
pragma Assert (False);
end if;
if J = 1 then
Qd1 := Qd (1);
Lemma_Substitution
- (Mult * Big_2xx (Scale), Big_2xx32, D123,
+ (Mult * Big_2xx (Scale), Big_2xxSingle, D123,
Big3 (D (1), D (2), D (3)) + Big3 (S1, S2, S3),
Big (Double_Uns (D (4))));
Prove_First_Iteration (D (1), D (2), D (3), D (4));
- Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xx32,
+ Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xxSingle,
Big3 (S1, S2, S3),
Big (Double_Uns (Qd1)) * Big (Zu),
Big3 (D (2), D (3), D (4)));
else
pragma Assert (Qd1 = Qd (1));
pragma Assert
- (Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) = 0);
+ (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ = 0);
pragma Assert
(Mult * Big_2xx (Scale) =
- Big_2xx32 * Big (Double_Uns (Qd (1))) * Big (Zu)
+ Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ Big3 (S1, S2, S3)
+ Big3 (D (2), D (3), D (4)));
pragma Assert
(Mult * Big_2xx (Scale) =
- Big_2xx32 * Big (Double_Uns (Qd (1))) * Big (Zu)
- + Big (Double_Uns (Qd (2))) * Big (Zu)
- + Big_2xx32 * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4))));
+ Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ + Big (Double_Uns (Qd (2))) * Big (Zu)
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4))));
end if;
end loop;
end;
@@ -2608,15 +2630,16 @@ is
pragma Assert
(Mult * Big_2xx (Scale) =
- Big_2xx32 * Big (Double_Uns (Qd (1))) * Big (Zu)
- + Big (Double_Uns (Qd (2))) * Big (Zu)
- + Big_2xx32 * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4))));
+ Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ + Big (Double_Uns (Qd (2))) * Big (Zu)
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4))));
Lemma_Hi_Lo (Qu, Qd (1), Qd (2));
Lemma_Hi_Lo (Ru, D (3), D (4));
Lemma_Substitution
(Mult * Big_2xx (Scale), Big (Zu),
- Big_2xx32 * Big (Double_Uns (Qd (1))) + Big (Double_Uns (Qd (2))),
+ Big_2xxSingle * Big (Double_Uns (Qd (1)))
+ + Big (Double_Uns (Qd (2))),
Big (Qu), Big (Ru));
Prove_Rescaling;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-01-05 11:33 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-01-05 11:33 [gcc r12-6226] [Ada] Rename parameter-dependent constants in generic unit Pierre-Marie de Rodat
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).