From: Yannick Moy Date: Tue, 30 Nov 2021 10:43:40 +0000 (+0100) Subject: [Ada] Add contracts for the proof of System.Arith_128 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=bfcc4dd71b5e17488c85a42db86aef433ac712fd;p=test_jj.git [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 --git a/gcc/ada/libgnat/s-arit128.adb b/gcc/ada/libgnat/s-arit128.adb index 951e357..d5f6c3d 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 6213cfb..e712c3c 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