[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.

10 files changed, 253 insertions, 23 deletions

diff --git a/gcc/ada/libgnat/s-widint.ads b/gcc/ada/libgnat/s-widint.ads
index f9b5eda..fb71618 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 708dbdc..07ff8bf 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 82a7e3d..af35616 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 10a0c9c..fd6534f 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 7eaf966..ce01285 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 2f2d5e0..55a94ec 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 37865b89..44e448d 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 79a0074..0be44ff 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 7b71119..c70d7ae 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 713532e..f694470 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;