public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-5740] [Ada] Proof of support units for 'Width on signed integers
@ 2021-12-02 16:29 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-12-02 16:29 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:3a54dfa801a1cfb387c8c43e7610b11905db505c
commit r12-5740-g3a54dfa801a1cfb387c8c43e7610b11905db505c
Author: Yannick Moy <moy@adacore.com>
Date: Wed Nov 24 17:20:59 2021 +0100
[Ada] Proof of support units for 'Width on signed integers
gcc/ada/
* libgnat/s-widint.ads: Mark in SPARK.
* libgnat/s-widlli.ads: Likewise.
* libgnat/s-widllli.ads: Likewise.
* libgnat/s-widlllu.ads: Likewise.
* libgnat/s-widllu.ads: Disable ghost/contract.
* libgnat/s-widthi.adb: Replicate and adapt the proof from
s-widthu.adb.
* libgnat/s-widthi.ads: Add minimal postcondition.
* libgnat/s-widthu.adb: Fix comments in the modular case.
* libgnat/s-widthu.ads: Add minimal postcondition.
* libgnat/s-widuns.ads: Disable ghost/contract.
Diff:
---
gcc/ada/libgnat/s-widint.ads | 15 ++++-
gcc/ada/libgnat/s-widlli.ads | 15 ++++-
gcc/ada/libgnat/s-widllli.ads | 15 ++++-
gcc/ada/libgnat/s-widlllu.ads | 11 ++++
gcc/ada/libgnat/s-widllu.ads | 11 ++++
gcc/ada/libgnat/s-widthi.adb | 130 ++++++++++++++++++++++++++++++++++++++++++
gcc/ada/libgnat/s-widthi.ads | 7 ++-
gcc/ada/libgnat/s-widthu.adb | 54 ++++++++++++------
gcc/ada/libgnat/s-widthu.ads | 7 ++-
gcc/ada/libgnat/s-widuns.ads | 11 ++++
10 files changed, 253 insertions(+), 23 deletions(-)
diff --git a/gcc/ada/libgnat/s-widint.ads b/gcc/ada/libgnat/s-widint.ads
index f9b5eda24be..fb716183f11 100644
--- a/gcc/ada/libgnat/s-widint.ads
+++ b/gcc/ada/libgnat/s-widint.ads
@@ -31,9 +31,22 @@
-- Width attribute for signed integers up to Integer
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
with System.Width_I;
-package System.Wid_Int is
+package System.Wid_Int
+ with SPARK_Mode
+is
function Width_Integer is new Width_I (Integer);
pragma Pure_Function (Width_Integer);
diff --git a/gcc/ada/libgnat/s-widlli.ads b/gcc/ada/libgnat/s-widlli.ads
index 708dbdc6e48..07ff8bf5354 100644
--- a/gcc/ada/libgnat/s-widlli.ads
+++ b/gcc/ada/libgnat/s-widlli.ads
@@ -31,9 +31,22 @@
-- Width attribute for signed integers larger than Integer
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
with System.Width_I;
-package System.Wid_LLI is
+package System.Wid_LLI
+ with SPARK_Mode
+is
function Width_Long_Long_Integer is new Width_I (Long_Long_Integer);
pragma Pure_Function (Width_Long_Long_Integer);
diff --git a/gcc/ada/libgnat/s-widllli.ads b/gcc/ada/libgnat/s-widllli.ads
index 82a7e3d46b0..af3561622ea 100644
--- a/gcc/ada/libgnat/s-widllli.ads
+++ b/gcc/ada/libgnat/s-widllli.ads
@@ -31,9 +31,22 @@
-- Width attribute for signed integers larger than Long_Long_Integer
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
with System.Width_I;
-package System.Wid_LLLI is
+package System.Wid_LLLI
+ with SPARK_Mode
+is
function Width_Long_Long_Long_Integer is
new Width_I (Long_Long_Long_Integer);
diff --git a/gcc/ada/libgnat/s-widlllu.ads b/gcc/ada/libgnat/s-widlllu.ads
index 10a0c9c7f9b..fd6534f92e3 100644
--- a/gcc/ada/libgnat/s-widlllu.ads
+++ b/gcc/ada/libgnat/s-widlllu.ads
@@ -31,6 +31,17 @@
-- Width attribute for modular integers larger than Long_Long_Integer
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
with System.Width_U;
with System.Unsigned_Types;
diff --git a/gcc/ada/libgnat/s-widllu.ads b/gcc/ada/libgnat/s-widllu.ads
index 7eaf966cbb7..ce01285c3a0 100644
--- a/gcc/ada/libgnat/s-widllu.ads
+++ b/gcc/ada/libgnat/s-widllu.ads
@@ -31,6 +31,17 @@
-- Width attribute for modular integers larger than Integer
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
with System.Width_U;
with System.Unsigned_Types;
diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb
index 2f2d5e05d74..55a94ecfc10 100644
--- a/gcc/ada/libgnat/s-widthi.adb
+++ b/gcc/ada/libgnat/s-widthi.adb
@@ -29,10 +29,109 @@
-- --
------------------------------------------------------------------------------
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+
function System.Width_I (Lo, Hi : Int) return Natural is
+
+ -- Ghost code, loop invariants and assertions in this unit are meant for
+ -- analysis only, not for run-time checking, as it would be too costly
+ -- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+ pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ package Signed_Conversion is new Signed_Conversions (Int => Int);
+
+ function Big (Arg : Int) return Big_Integer renames
+ Signed_Conversion.To_Big_Integer;
+
+ -- Maximum value of exponent for 10 that fits in Uns'Base
+ function Max_Log10 return Natural is
+ (case Int'Base'Size is
+ when 8 => 2,
+ when 16 => 4,
+ when 32 => 9,
+ when 64 => 19,
+ when 128 => 38,
+ when others => raise Program_Error)
+ with Ghost;
+
+ ------------------
+ -- Local Lemmas --
+ ------------------
+
+ procedure Lemma_Lower_Mult (A, B, C : Big_Natural)
+ with
+ Ghost,
+ Pre => A <= B,
+ Post => A * C <= B * C;
+
+ procedure Lemma_Div_Commutation (X, Y : Int)
+ with
+ Ghost,
+ Pre => X >= 0 and Y > 0,
+ Post => Big (X) / Big (Y) = Big (X / Y);
+
+ procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive)
+ with
+ Ghost,
+ Post => X / Y / Z = X / (Y * Z);
+
+ ----------------------
+ -- Lemma_Lower_Mult --
+ ----------------------
+
+ procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null;
+
+ ---------------------------
+ -- Lemma_Div_Commutation --
+ ---------------------------
+
+ procedure Lemma_Div_Commutation (X, Y : Int) is null;
+
+ ---------------------
+ -- Lemma_Div_Twice --
+ ---------------------
+
+ procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is
+ XY : constant Big_Natural := X / Y;
+ YZ : constant Big_Natural := Y * Z;
+ XYZ : constant Big_Natural := X / Y / Z;
+ R : constant Big_Natural := (XY rem Z) * Y + (X rem Y);
+ begin
+ pragma Assert (X = XY * Y + (X rem Y));
+ pragma Assert (XY = XY / Z * Z + (XY rem Z));
+ pragma Assert (X = XYZ * YZ + R);
+ pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y);
+ pragma Assert (R <= YZ - 1);
+ pragma Assert (X / YZ = (XYZ * YZ + R) / YZ);
+ pragma Assert (X / YZ = XYZ + R / YZ);
+ end Lemma_Div_Twice;
+
+ -- Local variables
+
W : Natural;
T : Int;
+ -- Local ghost variables
+
+ Max_W : constant Natural := Max_Log10 with Ghost;
+ Big_10 : constant Big_Integer := Big (10) with Ghost;
+
+ Pow : Big_Integer := 1 with Ghost;
+ T_Init : constant Int :=
+ Int'Max (abs (Int'Max (Lo, Int'First + 1)),
+ abs (Int'Max (Hi, Int'First + 1)))
+ with Ghost;
+
+-- Start of processing for System.Width_I
+
begin
if Lo > Hi then
return 0;
@@ -52,10 +151,41 @@ begin
-- Increase value if more digits required
while T >= 10 loop
+ Lemma_Div_Commutation (T, 10);
+ Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10);
+
T := T / 10;
W := W + 1;
+ Pow := Pow * 10;
+
+ pragma Loop_Invariant (T >= 0);
+ pragma Loop_Invariant (W in 3 .. Max_W + 3);
+ pragma Loop_Invariant (Pow = Big_10 ** (W - 2));
+ pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow);
+ pragma Loop_Variant (Decreases => T);
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;
+ begin
+ pragma Assert (Q < Big_10);
+ pragma Assert (Big (T_Init) = Q * F + R);
+ Lemma_Lower_Mult (Q, Big (9), F);
+ pragma Assert (Big (T_Init) <= Big (9) * F + F - 1);
+ pragma Assert (Big (T_Init) < Big_10 * F);
+ pragma Assert (Big_10 * F = Big_10 ** (W - 1));
+ end;
+
+ -- This is an expression of the functional postcondition for Width_I,
+ -- which cannot be expressed readily as a postcondition as this would
+ -- require making the instantiation Signed_Conversion and function Big
+ -- available from the spec.
+
+ pragma Assert (Big (Int'Max (Lo, Int'First + 1)) < Big_10 ** (W - 1));
+ pragma Assert (Big (Int'Max (Hi, Int'First + 1)) < Big_10 ** (W - 1));
+
return W;
end if;
diff --git a/gcc/ada/libgnat/s-widthi.ads b/gcc/ada/libgnat/s-widthi.ads
index 37865b8957d..44e448dfb28 100644
--- a/gcc/ada/libgnat/s-widthi.ads
+++ b/gcc/ada/libgnat/s-widthi.ads
@@ -36,4 +36,9 @@ generic
type Int is range <>;
-function System.Width_I (Lo, Hi : Int) return Natural;
+function System.Width_I (Lo, Hi : Int) return Natural
+with
+ Post => (if Lo > Hi then
+ System.Width_I'Result = 0
+ else
+ System.Width_I'Result > 0);
diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb
index 79a0074214d..0be44ffe6b9 100644
--- a/gcc/ada/libgnat/s-widthu.adb
+++ b/gcc/ada/libgnat/s-widthu.adb
@@ -42,14 +42,14 @@ function System.Width_U (Lo, Hi : Uns) return Natural is
Loop_Invariant => Ignore,
Assert => Ignore);
- W : Natural;
- T : Uns;
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
- function Big (Arg : Uns) return Big_Integer is
- (Unsigned_Conversion.To_Big_Integer (Arg))
- with Ghost;
+ function Big (Arg : Uns) return Big_Integer renames
+ Unsigned_Conversion.To_Big_Integer;
-- Maximum value of exponent for 10 that fits in Uns'Base
function Max_Log10 return Natural is
@@ -62,8 +62,9 @@ function System.Width_U (Lo, Hi : Uns) return Natural is
when others => raise Program_Error)
with Ghost;
- Max_W : constant Natural := Max_Log10 with Ghost;
- Big_10 : constant Big_Integer := Big (10) with Ghost;
+ ------------------
+ -- Local Lemmas --
+ ------------------
procedure Lemma_Lower_Mult (A, B, C : Big_Natural)
with
@@ -82,15 +83,21 @@ function System.Width_U (Lo, Hi : Uns) return Natural is
Ghost,
Post => X / Y / Z = X / (Y * Z);
- procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is
- begin
- null;
- end Lemma_Lower_Mult;
+ ----------------------
+ -- Lemma_Lower_Mult --
+ ----------------------
- procedure Lemma_Div_Commutation (X, Y : Uns) is
- begin
- null;
- end Lemma_Div_Commutation;
+ procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null;
+
+ ---------------------------
+ -- Lemma_Div_Commutation --
+ ---------------------------
+
+ procedure Lemma_Div_Commutation (X, Y : Uns) is null;
+
+ ---------------------
+ -- Lemma_Div_Twice --
+ ---------------------
procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is
XY : constant Big_Natural := X / Y;
@@ -107,20 +114,31 @@ function System.Width_U (Lo, Hi : Uns) return Natural is
pragma Assert (X / YZ = XYZ + R / YZ);
end Lemma_Div_Twice;
+ -- Local variables
+
+ W : Natural;
+ T : Uns;
+
+ -- Local ghost variables
+
+ Max_W : constant Natural := Max_Log10 with Ghost;
+ Big_10 : constant Big_Integer := Big (10) with Ghost;
+
Pow : Big_Integer := 1 with Ghost;
T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost;
+-- Start of processing for System.Width_U
+
begin
if Lo > Hi then
return 0;
else
- -- Minimum value is 2, one for sign, one for digit
+ -- Minimum value is 2, one for space, one for digit
W := 2;
- -- Get max of absolute values, but avoid bomb if we have the maximum
- -- negative number (note that First + 1 has same digits as First)
+ -- Get max of absolute values
T := Uns'Max (Lo, Hi);
diff --git a/gcc/ada/libgnat/s-widthu.ads b/gcc/ada/libgnat/s-widthu.ads
index 7b711190242..c70d7ae25e2 100644
--- a/gcc/ada/libgnat/s-widthu.ads
+++ b/gcc/ada/libgnat/s-widthu.ads
@@ -36,4 +36,9 @@ generic
type Uns is mod <>;
-function System.Width_U (Lo, Hi : Uns) return Natural;
+function System.Width_U (Lo, Hi : Uns) return Natural
+with
+ Post => (if Lo > Hi then
+ System.Width_U'Result = 0
+ else
+ System.Width_U'Result > 0);
diff --git a/gcc/ada/libgnat/s-widuns.ads b/gcc/ada/libgnat/s-widuns.ads
index 713532ed6d7..f694470f396 100644
--- a/gcc/ada/libgnat/s-widuns.ads
+++ b/gcc/ada/libgnat/s-widuns.ads
@@ -31,6 +31,17 @@
-- Width attribute for modular integers up to Integer
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
with System.Width_U;
with System.Unsigned_Types;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-12-02 16:29 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-12-02 16:29 [gcc r12-5740] [Ada] Proof of support units for 'Width on signed integers 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).