[gcc r12-6238] [Ada] Add contracts for the proof of System.Arith_128

[gcc r12-6238] [Ada] Add contracts for the proof of System.Arith_128

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:bfcc4dd71b5e17488c85a42db86aef433ac712fd

commit r12-6238-gbfcc4dd71b5e17488c85a42db86aef433ac712fd
Author: Yannick Moy <moy@adacore.com>
Date:   Tue Nov 30 11:43:40 2021 +0100

    [Ada] Add contracts for the proof of System.Arith_128
    
    gcc/ada/
    
            * libgnat/s-arit128.adb: Mark in SPARK.
            * libgnat/s-arit128.ads: Add functional contracts.

Diff:
---
 gcc/ada/libgnat/s-arit128.adb |   4 +-
 gcc/ada/libgnat/s-arit128.ads | 100 +++++++++++++++++++++++++++++++++++++++---
 2 files changed, 96 insertions(+), 8 deletions(-)

diff --git a/gcc/ada/libgnat/s-arit128.adb b/gcc/ada/libgnat/s-arit128.adb
index 951e357e1b3..d5f6c3d64cd 100644
--- a/gcc/ada/libgnat/s-arit128.adb
+++ b/gcc/ada/libgnat/s-arit128.adb
@@ -31,7 +31,9 @@
 
 with System.Arith_Double;
 
-package body System.Arith_128 is
+package body System.Arith_128
+  with SPARK_Mode
+is
 
    subtype Uns128 is Interfaces.Unsigned_128;
    subtype Uns64  is Interfaces.Unsigned_64;
diff --git a/gcc/ada/libgnat/s-arit128.ads b/gcc/ada/libgnat/s-arit128.ads
index 6213cfb569a..e712c3c9d62 100644
--- a/gcc/ada/libgnat/s-arit128.ads
+++ b/gcc/ada/libgnat/s-arit128.ads
@@ -36,31 +36,102 @@
 pragma Restrictions (No_Elaboration_Code);
 --  Allow direct call from gigi generated code
 
+--  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 Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 with Interfaces;
 
-package System.Arith_128 is
-   pragma Pure;
+package System.Arith_128
+  with Pure, SPARK_Mode
+is
+   use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer;
+   use type Interfaces.Integer_128;
 
    subtype Int128 is Interfaces.Integer_128;
 
-   function Add_With_Ovflo_Check128 (X, Y : Int128) return Int128;
+   subtype Big_Integer is
+     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer
+   with Ghost;
+
+   package Signed_Conversion is new
+     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Signed_Conversions
+     (Int => Int128);
+
+   function Big (Arg : Int128) return Big_Integer is
+     (Signed_Conversion.To_Big_Integer (Arg))
+   with Ghost;
+
+   function In_Int128_Range (Arg : Big_Integer) return Boolean is
+     (Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range
+       (Arg, Big (Int128'First), Big (Int128'Last)))
+   with Ghost;
+
+   function Add_With_Ovflo_Check128 (X, Y : Int128) return Int128
+   with
+     Pre  => In_Int128_Range (Big (X) + Big (Y)),
+     Post => Add_With_Ovflo_Check128'Result = X + Y;
    --  Raises Constraint_Error if sum of operands overflows 128 bits,
    --  otherwise returns the 128-bit signed integer sum.
 
-   function Subtract_With_Ovflo_Check128 (X, Y : Int128) return Int128;
+   function Subtract_With_Ovflo_Check128 (X, Y : Int128) return Int128
+   with
+     Pre  => In_Int128_Range (Big (X) - Big (Y)),
+     Post => Subtract_With_Ovflo_Check128'Result = X - Y;
    --  Raises Constraint_Error if difference of operands overflows 128
    --  bits, otherwise returns the 128-bit signed integer difference.
 
-   function Multiply_With_Ovflo_Check128 (X, Y : Int128) return Int128;
+   function Multiply_With_Ovflo_Check128 (X, Y : Int128) return Int128
+   with
+     Pre  => In_Int128_Range (Big (X) * Big (Y)),
+     Post => Multiply_With_Ovflo_Check128'Result = X * Y;
    pragma Export (C, Multiply_With_Ovflo_Check128, "__gnat_mulv128");
    --  Raises Constraint_Error if product of operands overflows 128
    --  bits, otherwise returns the 128-bit signed integer product.
    --  Gigi may also call this routine directly.
 
+   function Same_Sign (X, Y : Big_Integer) return Boolean is
+     (X = Big (Int128'(0))
+        or else Y = Big (Int128'(0))
+        or else (X < Big (Int128'(0))) = (Y < Big (Int128'(0))))
+   with Ghost;
+
+   function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
+     (if abs R > (abs Y - Big (Int128'(1))) / Big (Int128'(2)) then
+       (if Same_Sign (X, Y) then Q + Big (Int128'(1))
+        else Q - Big (Int128'(1)))
+      else
+        Q)
+   with
+     Ghost,
+     Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
+
    procedure Scaled_Divide128
      (X, Y, Z : Int128;
       Q, R    : out Int128;
-      Round   : Boolean);
+      Round   : Boolean)
+   with
+     Pre  => Z /= 0
+       and then In_Int128_Range
+         (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                        Big (X) * Big (Y) / Big (Z),
+                                        Big (X) * Big (Y) rem Big (Z))
+          else Big (X) * Big (Y) / Big (Z)),
+     Post => Big (R) = Big (X) * Big (Y) rem Big (Z)
+       and then
+         (if Round then
+            Big (Q) = Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                      Big (X) * Big (Y) / Big (Z), Big (R))
+          else
+            Big (Q) = Big (X) * Big (Y) / Big (Z));
    --  Performs the division of (X * Y) / Z, storing the quotient in Q
    --  and the remainder in R. Constraint_Error is raised if Z is zero,
    --  or if the quotient does not fit in 128 bits. Round indicates if
@@ -72,7 +143,22 @@ package System.Arith_128 is
    procedure Double_Divide128
      (X, Y, Z : Int128;
       Q, R    : out Int128;
-      Round   : Boolean);
+      Round   : Boolean)
+   with
+     Pre  => Y /= 0
+       and then Z /= 0
+       and then In_Int128_Range
+         (if Round then Round_Quotient (Big (X), Big (Y) * Big (Z),
+                                        Big (X) / (Big (Y) * Big (Z)),
+                                        Big (X) rem (Big (Y) * Big (Z)))
+          else Big (X) / (Big (Y) * Big (Z))),
+     Post => Big (R) = Big (X) rem (Big (Y) * Big (Z))
+       and then
+         (if Round then
+            Big (Q) = Round_Quotient (Big (X), Big (Y) * Big (Z),
+                                      Big (X) / (Big (Y) * Big (Z)), Big (R))
+          else
+            Big (Q) = Big (X) / (Big (Y) * Big (Z)));
    --  Performs the division X / (Y * Z), storing the quotient in Q and
    --  the remainder in R. Constraint_Error is raised if Y or Z is zero,
    --  or if the quotient does not fit in 128 bits. Round indicates if the