OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Proof of 'Image support for signed integers 

Prove System.Image_I, similarly to the proof done for System.Image_U.
The contracts make the connection between the result of Image_Integer,
the available space computed with System.Width_U and the result of
'Value as computed by Value_Integer.

I/O units that now depend on non-pure units are also marked not Pure
anymore.

gcc/ada/

	* libgnat/s-imagef.adb: Adapt to new signature of Image_I, by
	providing ghost imported subprograms. For now, no contract is
	used on these subprograms, as System.Image_F is not proved.
	* libgnat/s-imagef.ads: Add modular type Uns as formal
	parameter, to use in defining Int_Params for instantiating
	Image_I.
	* libgnat/s-imagei.adb: Add contracts and ghost code.
	* libgnat/s-imagei.ads: Replace Int formal parameter by package
	Int_Params, which bundles type Int and Uns with ghost
	subprograms.  Add contracts.
	* libgnat/s-imfi128.ads: Adapt to new formal of Image_F.
	* libgnat/s-imfi32.ads: Adapt to new formal of Image_F.
	* libgnat/s-imfi64.ads: Adapt to new formal of Image_F.
	* libgnat/s-imgint.ads: Adapt to new formals of Image_I.
	* libgnat/s-imglli.ads: Adapt to new formals of Image_I.
	* libgnat/s-imgllli.ads: Adapt to new formals of Image_I.
	* libgnat/s-valint.ads: Adapt to new formals of Value_I.
	* libgnat/s-vallli.ads: Adapt to new formals of Value_I.
	* libgnat/s-valllli.ads: Adapt to new formals of Value_I.
	* libgnat/s-valuei.adb (Prove_Scan_Only_Decimal_Ghost): New
	ghost lemma.
	* libgnat/s-valuei.ads: New formal parameters to prove the new
	lemma.
	* libgnat/s-valuti.ads (Int_Params): Define a generic package to
	be used as a trait-like formal parameter in Image_I and other
	generics that need to instantiate Image_I.
	* libgnat/s-widthu.ads (Big_10): Qualify the 10 literal.
This commit is contained in:
Yannick Moy 2022-02-04 15:20:20 +01:00 committed by Pierre-Marie de Rodat
parent a4f6f9f176
commit 91d6876941
17 changed files with 786 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

80
gcc/ada/libgnat/s-imagef.adb
View File

@ -31,9 +31,24 @@
with System.Image_I;
with System.Img_Util; use System.Img_Util;
with System.Val_Util;
package body System.Image_F is
-- Contracts, 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 (Assert => Ignore,
Assert_And_Cut => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore,
Loop_Invariant => Ignore,
Pre => Ignore,
Post => Ignore,
Subprogram_Variant => Ignore);
Maxdigs : constant Natural := Int'Width - 2;
-- Maximum number of decimal digits that can be represented in an Int.
-- The "-2" accounts for the sign and one extra digit, since we need the
@ -54,7 +69,70 @@ package body System.Image_F is
-- if the small is larger than 1, and smaller than 2**(Int'Size - 1) / 10
-- if the small is smaller than 1.
package Image_I is new System.Image_I (Int);
-- Define ghost subprograms without implementation (marked as Import) to
-- create a suitable package Int_Params for type Int, as instantiations
-- of System.Image_F use for this type one of the derived integer types
-- defined in Interfaces, instead of the standard signed integer types
-- which are used to define System.Img_*.Int_Params.
type Uns_Option (Overflow : Boolean := False) is record
case Overflow is
when True =>
null;
when False =>
Value : Uns := 0;
end case;
end record;
Unsigned_Width_Ghost : constant Natural := Int'Width;
function Wrap_Option (Value : Uns) return Uns_Option
with Ghost, Import;
function Only_Decimal_Ghost
(Str : String;
From, To : Integer)
return Boolean
with Ghost, Import;
function Hexa_To_Unsigned_Ghost (X : Character) return Uns
with Ghost, Import;
function Scan_Based_Number_Ghost
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
return Uns_Option
with Ghost, Import;
function Is_Integer_Ghost (Str : String) return Boolean
with Ghost, Import;
procedure Prove_Iter_Scan_Based_Number_Ghost
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
with Ghost, Import;
procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
with Ghost, Import;
function Abs_Uns_Of_Int (Val : Int) return Uns
with Ghost, Import;
function Value_Integer (Str : String) return Int
with Ghost, Import;
package Int_Params is new Val_Util.Int_Params
(Int => Int,
Uns => Uns,
Uns_Option => Uns_Option,
Unsigned_Width_Ghost => Unsigned_Width_Ghost,
Wrap_Option => Wrap_Option,
Only_Decimal_Ghost => Only_Decimal_Ghost,
Hexa_To_Unsigned_Ghost => Hexa_To_Unsigned_Ghost,
Scan_Based_Number_Ghost => Scan_Based_Number_Ghost,
Is_Integer_Ghost => Is_Integer_Ghost,
Prove_Iter_Scan_Based_Number_Ghost => Prove_Iter_Scan_Based_Number_Ghost,
Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost,
Abs_Uns_Of_Int => Abs_Uns_Of_Int,
Value_Integer => Value_Integer);
package Image_I is new System.Image_I (Int_Params);
procedure Set_Image_Integer
(V : Int;

1
gcc/ada/libgnat/s-imagef.ads
View File

@ -36,6 +36,7 @@
generic
type Int is range <>;
type Uns is mod <>;
with procedure Scaled_Divide
(X, Y, Z : Int;

365
gcc/ada/libgnat/s-imagei.adb
View File

@ -29,18 +29,140 @@
-- --
------------------------------------------------------------------------------
with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
package body System.Image_I 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,
Assert_And_Cut => Ignore,
Pre => Ignore,
Post => Ignore,
Subprogram_Variant => Ignore);
-- As a use_clause for Int_Params cannot be used for instances of this
-- generic in System specs, rename all constants and subprograms.
Unsigned_Width_Ghost : constant Natural := Int_Params.Unsigned_Width_Ghost;
function Wrap_Option (Value : Uns) return Uns_Option
renames Int_Params.Wrap_Option;
function Only_Decimal_Ghost
(Str : String;
From, To : Integer)
return Boolean
renames Int_Params.Only_Decimal_Ghost;
function Hexa_To_Unsigned_Ghost (X : Character) return Uns
renames Int_Params.Hexa_To_Unsigned_Ghost;
function Scan_Based_Number_Ghost
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
return Uns_Option
renames Int_Params.Scan_Based_Number_Ghost;
function Is_Integer_Ghost (Str : String) return Boolean
renames Int_Params.Is_Integer_Ghost;
procedure Prove_Iter_Scan_Based_Number_Ghost
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
renames Int_Params.Prove_Iter_Scan_Based_Number_Ghost;
procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
renames Int_Params.Prove_Scan_Only_Decimal_Ghost;
function Abs_Uns_Of_Int (Val : Int) return Uns
renames Int_Params.Abs_Uns_Of_Int;
function Value_Integer (Str : String) return Int
renames Int_Params.Value_Integer;
subtype Non_Positive is Int range Int'First .. 0;
function Uns_Of_Non_Positive (T : Non_Positive) return Uns is
(if T = Int'First then Uns (Int'Last) + 1 else Uns (-T));
procedure Set_Digits
(T : Non_Positive;
S : in out String;
P : in out Natural);
P : in out Natural)
with
Pre => P < Integer'Last
and then S'Last < Integer'Last
and then S'First <= P + 1
and then S'First <= S'Last
and then P <= S'Last - Unsigned_Width_Ghost + 1,
Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
and then P in P'Old + 1 .. S'Last
and then Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
= Wrap_Option (Uns_Of_Non_Positive (T));
-- Set digits of absolute value of T, which is zero or negative. We work
-- with the negative of the value so that the largest negative number is
-- not a special case.
package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
function Big (Arg : Uns) return Big_Integer renames
Unsigned_Conversion.To_Big_Integer;
function From_Big (Arg : Big_Integer) return Uns renames
Unsigned_Conversion.From_Big_Integer;
Big_10 : constant Big_Integer := Big (10) with Ghost;
------------------
-- Local Lemmas --
------------------
procedure Lemma_Non_Zero (X : Uns)
with
Ghost,
Pre => X /= 0,
Post => Big (X) /= 0;
procedure Lemma_Div_Commutation (X, Y : Uns)
with
Ghost,
Pre => 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_Div_Commutation --
---------------------------
procedure Lemma_Non_Zero (X : Uns) is null;
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;
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;
-------------------
-- Image_Integer --
-------------------
@ -52,6 +174,39 @@ package body System.Image_I is
is
pragma Assert (S'First = 1);
procedure Prove_Value_Integer
with
Ghost,
Pre => S'First = 1
and then S'Last < Integer'Last
and then P in 2 .. S'Last
and then S (1) in ' ' | '-'
and then (S (1) = '-') = (V < 0)
and then Only_Decimal_Ghost (S, From => 2, To => P)
and then Scan_Based_Number_Ghost (S, From => 2, To => P)
= Wrap_Option (Abs_Uns_Of_Int (V)),
Post => Is_Integer_Ghost (S (1 .. P))
and then Value_Integer (S (1 .. P)) = V;
-- Ghost lemma to prove the value of Value_Integer from the value of
-- Scan_Based_Number_Ghost and the sign on a decimal string.
-------------------------
-- Prove_Value_Integer --
-------------------------
procedure Prove_Value_Integer is
Str : constant String := S (1 .. P);
begin
pragma Assert (Str'First = 1);
pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P));
Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P);
pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P)
= Wrap_Option (Abs_Uns_Of_Int (V)));
Prove_Scan_Only_Decimal_Ghost (Str, V);
end Prove_Value_Integer;
-- Start of processing for Image_Integer
begin
if V >= 0 then
S (1) := ' ';
@ -63,7 +218,16 @@ package body System.Image_I is
pragma Assert (P < S'Last - 1);
end if;
Set_Image_Integer (V, S, P);
declare
P_Prev : constant Integer := P with Ghost;
Offset : constant Positive := (if V >= 0 then 1 else 2) with Ghost;
begin
Set_Image_Integer (V, S, P);
pragma Assert (P_Prev + Offset = 2);
end;
Prove_Value_Integer;
end Image_Integer;
----------------
@ -77,6 +241,106 @@ package body System.Image_I is
is
Nb_Digits : Natural := 0;
Value : Non_Positive := T;
-- Local ghost variables
Pow : Big_Positive := 1 with Ghost;
S_Init : constant String := S with Ghost;
Uns_T : constant Uns := Uns_Of_Non_Positive (T) with Ghost;
Uns_Value : Uns := Uns_Of_Non_Positive (Value) with Ghost;
Prev, Cur : Uns_Option with Ghost;
Prev_Value : Uns with Ghost;
Prev_S : String := S with Ghost;
-- Local ghost lemmas
procedure Prove_Character_Val (RU : Uns; RI : Int)
with
Ghost,
Pre => RU in 0 .. 9
and then RI in 0 .. 9,
Post => Character'Val (48 + RU) in '0' .. '9'
and then Character'Val (48 + RI) in '0' .. '9';
-- Ghost lemma to prove the value of a character corresponding to the
-- next figure.
procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int)
with
Ghost,
Pre => RU in 0 .. 9
and then RI in 0 .. 9,
Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + RU)) = RU
and then Hexa_To_Unsigned_Ghost (Character'Val (48 + RI)) = Uns (RI);
-- Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source
-- figure when applied to the corresponding character.
procedure Prove_Unchanged
with
Ghost,
Pre => P <= S'Last
and then S_Init'First = S'First
and then S_Init'Last = S'Last
and then (for all K in S'First .. P => S (K) = S_Init (K)),
Post => S (S'First .. P) = S_Init (S'First .. P);
-- Ghost lemma to prove that the part of string S before P has not been
-- modified.
procedure Prove_Uns_Of_Non_Positive_Value
with
Ghost,
Pre => Uns_Value = Uns_Of_Non_Positive (Value),
Post => Uns_Value / 10 = Uns_Of_Non_Positive (Value / 10)
and then Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10);
-- Ghost lemma to prove that the relation between Value and its unsigned
-- version is preserved.
procedure Prove_Iter_Scan
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
with
Ghost,
Pre => Str1'Last /= Positive'Last
and then
(From > To or else (From >= Str1'First and then To <= Str1'Last))
and then Only_Decimal_Ghost (Str1, From, To)
and then Str1'First = Str2'First
and then Str1'Last = Str2'Last
and then (for all J in From .. To => Str1 (J) = Str2 (J)),
Post =>
Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
= Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
-- Ghost lemma to prove that the result of Scan_Based_Number_Ghost only
-- depends on the value of the argument string in the (From .. To) range
-- of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost
-- so that we can call it here on ghost arguments.
-----------------------------
-- Local lemma null bodies --
-----------------------------
procedure Prove_Character_Val (RU : Uns; RI : Int) is null;
procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) is null;
procedure Prove_Unchanged is null;
procedure Prove_Uns_Of_Non_Positive_Value is null;
---------------------
-- Prove_Iter_Scan --
---------------------
procedure Prove_Iter_Scan
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
is
begin
Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc);
end Prove_Iter_Scan;
-- Start of processing for Set_Digits
begin
pragma Assert (P >= S'First - 1 and P < S'Last);
-- No check is done since, as documented in the Set_Image_Integer
@ -86,19 +350,116 @@ package body System.Image_I is
-- First we compute the number of characters needed for representing
-- the number.
loop
Lemma_Div_Commutation (Uns_Of_Non_Positive (Value), 10);
Lemma_Div_Twice (Big (Uns_Of_Non_Positive (T)),
Big_10 ** Nb_Digits, Big_10);
Prove_Uns_Of_Non_Positive_Value;
Value := Value / 10;
Nb_Digits := Nb_Digits + 1;
Uns_Value := Uns_Value / 10;
Pow := Pow * 10;
pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value));
pragma Loop_Invariant (Nb_Digits in 1 .. Unsigned_Width_Ghost - 1);
pragma Loop_Invariant (Pow = Big_10 ** Nb_Digits);
pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow);
pragma Loop_Variant (Increases => Value);
exit when Value = 0;
Lemma_Non_Zero (Uns_Value);
pragma Assert (Pow <= Big (Uns'Last));
end loop;
Value := T;
Uns_Value := Uns_Of_Non_Positive (T);
Pow := 1;
pragma Assert (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** 0));
-- We now populate digits from the end of the string to the beginning
for J in reverse 1 .. Nb_Digits loop
Lemma_Div_Commutation (Uns_Value, 10);
Lemma_Div_Twice (Big (Uns_T), Big_10 ** (Nb_Digits - J), Big_10);
Prove_Character_Val (Uns_Value rem 10, -(Value rem 10));
Prove_Hexa_To_Unsigned_Ghost (Uns_Value rem 10, -(Value rem 10));
Prove_Uns_Of_Non_Positive_Value;
pragma Assert (Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10));
pragma Assert (Uns_Value rem 10 = Uns (-(Value rem 10)));
Prev_Value := Uns_Value;
Prev_S := S;
Pow := Pow * 10;
Uns_Value := Uns_Value / 10;
S (P + J) := Character'Val (48 - (Value rem 10));
Value := Value / 10;
pragma Assert (S (P + J) in '0' .. '9');
pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) =
From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)) rem 10);
pragma Assert
(for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9');
Prev := Scan_Based_Number_Ghost
(Str => S,
From => P + J + 1,
To => P + Nb_Digits,
Base => 10,
Acc => Prev_Value);
Cur := Scan_Based_Number_Ghost
(Str => S,
From => P + J,
To => P + Nb_Digits,
Base => 10,
Acc => Uns_Value);
pragma Assert (Prev_Value = 10 * Uns_Value + (Prev_Value rem 10));
pragma Assert
(Prev_Value rem 10 = Hexa_To_Unsigned_Ghost (S (P + J)));
pragma Assert
(Prev_Value = 10 * Uns_Value + Hexa_To_Unsigned_Ghost (S (P + J)));
if J /= Nb_Digits then
Prove_Iter_Scan
(Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value);
end if;
pragma Assert (Prev = Cur);
pragma Assert (Prev = Wrap_Option (Uns_T));
pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value));
pragma Loop_Invariant (Uns_Value <= Uns'Last / 10);
pragma Loop_Invariant
(for all K in S'First .. P => S (K) = S_Init (K));
pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
pragma Loop_Invariant
(for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9');
pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1));
pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow);
pragma Loop_Invariant
(Scan_Based_Number_Ghost
(Str => S,
From => P + J,
To => P + Nb_Digits,
Base => 10,
Acc => Uns_Value)
= Wrap_Option (Uns_T));
end loop;
pragma Assert (Big (Uns_Value) = Big (Uns_T) / Big_10 ** (Nb_Digits));
pragma Assert (Uns_Value = 0);
Prove_Unchanged;
pragma Assert
(Scan_Based_Number_Ghost
(Str => S,
From => P + 1,
To => P + Nb_Digits,
Base => 10,
Acc => Uns_Value)
= Wrap_Option (Uns_T));
P := P + Nb_Digits;
end Set_Digits;

60
gcc/ada/libgnat/s-imagei.ads
View File

@ -33,17 +33,45 @@
-- signed integer types, and also for conversion operations required in
-- Text_IO.Integer_IO for such types.
-- 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,
Subprogram_Variant => Ignore);
with System.Val_Util;
generic
type Int is range <>;
with package Int_Params is new System.Val_Util.Int_Params (<>);
package System.Image_I is
pragma Pure;
subtype Int is Int_Params.Int;
use type Int_Params.Int;
subtype Uns is Int_Params.Uns;
use type Int_Params.Uns;
subtype Uns_Option is Int_Params.Uns_Option;
use type Int_Params.Uns_Option;
procedure Image_Integer
(V : Int;
S : in out String;
P : out Natural);
P : out Natural)
with
Pre => S'First = 1
and then S'Last < Integer'Last
and then S'Last >= Int_Params.Unsigned_Width_Ghost,
Post => P in S'Range
and then Int_Params.Value_Integer (S (1 .. P)) = V;
-- Computes Int'Image (V) and stores the result in S (1 .. P)
-- setting the resulting value of P. The caller guarantees that S
-- is long enough to hold the result, and that S'First is 1.
@ -51,7 +79,31 @@ package System.Image_I is
procedure Set_Image_Integer
(V : Int;
S : in out String;
P : in out Natural);
P : in out Natural)
with
Pre => P < Integer'Last
and then S'Last < Integer'Last
and then S'First <= P + 1
and then S'First <= S'Last
and then
(if V >= 0 then
P <= S'Last - Int_Params.Unsigned_Width_Ghost + 1
else
P <= S'Last - Int_Params.Unsigned_Width_Ghost),
Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
and then
(declare
Minus : constant Boolean := S (P'Old + 1) = '-';
Offset : constant Positive := (if V >= 0 then 1 else 2);
Abs_V : constant Uns := Int_Params.Abs_Uns_Of_Int (V);
begin
Minus = (V < 0)
and then P in P'Old + Offset .. S'Last
and then Int_Params.Only_Decimal_Ghost
(S, From => P'Old + Offset, To => P)
and then Int_Params.Scan_Based_Number_Ghost
(S, From => P'Old + Offset, To => P)
= Int_Params.Wrap_Option (Abs_V));
-- Stores the image of V in S starting at S (P + 1), P is updated to point
-- to the last character stored. The value stored is identical to the value
-- of Int'Image (V) except that no leading space is stored when V is

3
gcc/ada/libgnat/s-imfi128.ads
View File

@ -39,8 +39,9 @@ with System.Image_F;
package System.Img_Fixed_128 is
subtype Int128 is Interfaces.Integer_128;
subtype Uns128 is Interfaces.Unsigned_128;
package Impl is new Image_F (Int128, Arith_128.Scaled_Divide128);
package Impl is new Image_F (Int128, Uns128, Arith_128.Scaled_Divide128);
procedure Image_Fixed128
(V : Int128;

3
gcc/ada/libgnat/s-imfi32.ads
View File

@ -39,8 +39,9 @@ with System.Image_F;
package System.Img_Fixed_32 is
subtype Int32 is Interfaces.Integer_32;
subtype Uns32 is Interfaces.Unsigned_32;
package Impl is new Image_F (Int32, Arith_32.Scaled_Divide32);
package Impl is new Image_F (Int32, Uns32, Arith_32.Scaled_Divide32);
procedure Image_Fixed32
(V : Int32;

3
gcc/ada/libgnat/s-imfi64.ads
View File

@ -39,8 +39,9 @@ with System.Image_F;
package System.Img_Fixed_64 is
subtype Int64 is Interfaces.Integer_64;
subtype Uns64 is Interfaces.Unsigned_64;
package Impl is new Image_F (Int64, Arith_64.Scaled_Divide64);
package Impl is new Image_F (Int64, Uns64, Arith_64.Scaled_Divide64);
procedure Image_Fixed64
(V : Int64;

45
gcc/ada/libgnat/s-imgint.ads
View File

@ -33,12 +33,51 @@
-- signed integer types up to Integer, and also for conversion operations
-- required in Text_IO.Integer_IO for such types.
-- 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,
Subprogram_Variant => Ignore);
with System.Image_I;
with System.Unsigned_Types;
with System.Val_Int;
with System.Val_Uns;
with System.Val_Util;
with System.Wid_Uns;
package System.Img_Int is
pragma Pure;
package System.Img_Int
with SPARK_Mode
is
subtype Unsigned is Unsigned_Types.Unsigned;
package Impl is new Image_I (Integer);
package Int_Params is new Val_Util.Int_Params
(Int => Integer,
Uns => Unsigned,
Uns_Option => Val_Uns.Impl.Uns_Option,
Unsigned_Width_Ghost =>
Wid_Uns.Width_Unsigned (0, Unsigned'Last),
Only_Decimal_Ghost => Val_Uns.Impl.Only_Decimal_Ghost,
Hexa_To_Unsigned_Ghost =>
Val_Uns.Impl.Hexa_To_Unsigned_Ghost,
Wrap_Option => Val_Uns.Impl.Wrap_Option,
Scan_Based_Number_Ghost =>
Val_Uns.Impl.Scan_Based_Number_Ghost,
Prove_Iter_Scan_Based_Number_Ghost =>
Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost,
Is_Integer_Ghost => Val_Int.Impl.Is_Integer_Ghost,
Prove_Scan_Only_Decimal_Ghost =>
Val_Int.Impl.Prove_Scan_Only_Decimal_Ghost,
Abs_Uns_Of_Int => Val_Int.Impl.Abs_Uns_Of_Int,
Value_Integer => Val_Int.Impl.Value_Integer);
package Impl is new Image_I (Int_Params);
procedure Image_Integer
(V : Integer;

45
gcc/ada/libgnat/s-imglli.ads
View File

@ -33,12 +33,51 @@
-- signed integer types larger than Integer, and also for conversion
-- operations required in Text_IO.Integer_IO for such types.
-- 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,
Subprogram_Variant => Ignore);
with System.Image_I;
with System.Unsigned_Types;
with System.Val_LLI;
with System.Val_LLU;
with System.Val_Util;
with System.Wid_LLU;
package System.Img_LLI is
pragma Pure;
package System.Img_LLI
with SPARK_Mode
is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
package Impl is new Image_I (Long_Long_Integer);
package Int_Params is new Val_Util.Int_Params
(Int => Long_Long_Integer,
Uns => Long_Long_Unsigned,
Uns_Option => Val_LLU.Impl.Uns_Option,
Unsigned_Width_Ghost =>
Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last),
Only_Decimal_Ghost => Val_LLU.Impl.Only_Decimal_Ghost,
Hexa_To_Unsigned_Ghost =>
Val_LLU.Impl.Hexa_To_Unsigned_Ghost,
Wrap_Option => Val_LLU.Impl.Wrap_Option,
Scan_Based_Number_Ghost =>
Val_LLU.Impl.Scan_Based_Number_Ghost,
Prove_Iter_Scan_Based_Number_Ghost =>
Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
Is_Integer_Ghost => Val_LLI.Impl.Is_Integer_Ghost,
Prove_Scan_Only_Decimal_Ghost =>
Val_LLI.Impl.Prove_Scan_Only_Decimal_Ghost,
Abs_Uns_Of_Int => Val_LLI.Impl.Abs_Uns_Of_Int,
Value_Integer => Val_LLI.Impl.Value_Integer);
package Impl is new Image_I (Int_Params);
procedure Image_Long_Long_Integer
(V : Long_Long_Integer;

46
gcc/ada/libgnat/s-imgllli.ads
View File

@ -33,12 +33,52 @@
-- signed integer types larger than Long_Long_Integer, and also for conversion
-- operations required in Text_IO.Integer_IO for such types.
-- 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,
Subprogram_Variant => Ignore);
with System.Image_I;
with System.Unsigned_Types;
with System.Val_LLLI;
with System.Val_LLLU;
with System.Val_Util;
with System.Wid_LLLU;
package System.Img_LLLI is
pragma Pure;
package System.Img_LLLI
with SPARK_Mode
is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
package Impl is new Image_I (Long_Long_Long_Integer);
package Int_Params is new Val_Util.Int_Params
(Int => Long_Long_Long_Integer,
Uns => Long_Long_Long_Unsigned,
Uns_Option => Val_LLLU.Impl.Uns_Option,
Unsigned_Width_Ghost =>
Wid_LLLU.Width_Long_Long_Long_Unsigned
(0, Long_Long_Long_Unsigned'Last),
Only_Decimal_Ghost => Val_LLLU.Impl.Only_Decimal_Ghost,
Hexa_To_Unsigned_Ghost =>
Val_LLLU.Impl.Hexa_To_Unsigned_Ghost,
Wrap_Option => Val_LLLU.Impl.Wrap_Option,
Scan_Based_Number_Ghost =>
Val_LLLU.Impl.Scan_Based_Number_Ghost,
Prove_Iter_Scan_Based_Number_Ghost =>
Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
Is_Integer_Ghost => Val_LLLI.Impl.Is_Integer_Ghost,
Prove_Scan_Only_Decimal_Ghost =>
Val_LLLI.Impl.Prove_Scan_Only_Decimal_Ghost,
Abs_Uns_Of_Int => Val_LLLI.Impl.Abs_Uns_Of_Int,
Value_Integer => Val_LLLI.Impl.Value_Integer);
package Impl is new Image_I (Int_Params);
procedure Image_Long_Long_Long_Integer
(V : Long_Long_Long_Integer;

8
gcc/ada/libgnat/s-valint.ads
View File

@ -57,6 +57,8 @@ package System.Val_Int with SPARK_Mode is
(Int => Integer,
Uns => Unsigned,
Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned,
Uns_Option => Val_Uns.Impl.Uns_Option,
Wrap_Option => Val_Uns.Impl.Wrap_Option,
Is_Raw_Unsigned_Format_Ghost =>
Val_Uns.Impl.Is_Raw_Unsigned_Format_Ghost,
Raw_Unsigned_Overflows_Ghost =>
@ -64,7 +66,11 @@ package System.Val_Int with SPARK_Mode is
Scan_Raw_Unsigned_Ghost =>
Val_Uns.Impl.Scan_Raw_Unsigned_Ghost,
Raw_Unsigned_Last_Ghost =>
Val_Uns.Impl.Raw_Unsigned_Last_Ghost);
Val_Uns.Impl.Raw_Unsigned_Last_Ghost,
Only_Decimal_Ghost =>
Val_Uns.Impl.Only_Decimal_Ghost,
Scan_Based_Number_Ghost =>
Val_Uns.Impl.Scan_Based_Number_Ghost);
procedure Scan_Integer
(Str : String;

8
gcc/ada/libgnat/s-vallli.ads
View File

@ -58,6 +58,8 @@ package System.Val_LLI with SPARK_Mode is
Uns => Long_Long_Unsigned,
Scan_Raw_Unsigned =>
Val_LLU.Scan_Raw_Long_Long_Unsigned,
Uns_Option => Val_LLU.Impl.Uns_Option,
Wrap_Option => Val_LLU.Impl.Wrap_Option,
Is_Raw_Unsigned_Format_Ghost =>
Val_LLU.Impl.Is_Raw_Unsigned_Format_Ghost,
Raw_Unsigned_Overflows_Ghost =>
@ -65,7 +67,11 @@ package System.Val_LLI with SPARK_Mode is
Scan_Raw_Unsigned_Ghost =>
Val_LLU.Impl.Scan_Raw_Unsigned_Ghost,
Raw_Unsigned_Last_Ghost =>
Val_LLU.Impl.Raw_Unsigned_Last_Ghost);
Val_LLU.Impl.Raw_Unsigned_Last_Ghost,
Only_Decimal_Ghost =>
Val_LLU.Impl.Only_Decimal_Ghost,
Scan_Based_Number_Ghost =>
Val_LLU.Impl.Scan_Based_Number_Ghost);
procedure Scan_Long_Long_Integer
(Str : String;

8
gcc/ada/libgnat/s-valllli.ads
View File

@ -58,6 +58,8 @@ package System.Val_LLLI with SPARK_Mode is
Uns => Long_Long_Long_Unsigned,
Scan_Raw_Unsigned =>
Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned,
Uns_Option => Val_LLLU.Impl.Uns_Option,
Wrap_Option => Val_LLLU.Impl.Wrap_Option,
Is_Raw_Unsigned_Format_Ghost =>
Val_LLLU.Impl.Is_Raw_Unsigned_Format_Ghost,
Raw_Unsigned_Overflows_Ghost =>
@ -65,7 +67,11 @@ package System.Val_LLLI with SPARK_Mode is
Scan_Raw_Unsigned_Ghost =>
Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost,
Raw_Unsigned_Last_Ghost =>
Val_LLLU.Impl.Raw_Unsigned_Last_Ghost);
Val_LLLU.Impl.Raw_Unsigned_Last_Ghost,
Only_Decimal_Ghost =>
Val_LLLU.Impl.Only_Decimal_Ghost,
Scan_Based_Number_Ghost =>
Val_LLLU.Impl.Scan_Based_Number_Ghost);
procedure Scan_Long_Long_Long_Integer
(Str : String;

53
gcc/ada/libgnat/s-valuei.adb
View File

@ -41,6 +41,59 @@ package body System.Value_I is
Assert_And_Cut => Ignore,
Subprogram_Variant => Ignore);
-----------------------------------
-- Prove_Scan_Only_Decimal_Ghost --
-----------------------------------
procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is
Non_Blank : constant Positive := First_Non_Space_Ghost
(Str, Str'First, Str'Last);
pragma Assert
(if Val < 0 then Non_Blank = Str'First
else
Only_Space_Ghost (Str, Str'First, Str'First)
and then Non_Blank = Str'First + 1);
Minus : constant Boolean := Str (Non_Blank) = '-';
Fst_Num : constant Positive :=
(if Minus then Non_Blank + 1 else Non_Blank);
pragma Assert (Fst_Num = Str'First + 1);
Uval : constant Uns :=
Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
procedure Unique_Int_Of_Uns (Val1, Val2 : Int)
with
Pre => Uns_Is_Valid_Int (Minus, Uval)
and then Is_Int_Of_Uns (Minus, Uval, Val1)
and then Is_Int_Of_Uns (Minus, Uval, Val2),
Post => Val1 = Val2;
-- Local proof of the unicity of the signed representation
procedure Unique_Int_Of_Uns (Val1, Val2 : Int) is null;
-- Start of processing for Prove_Scan_Only_Decimal_Ghost
begin
pragma Assert (Minus = (Val < 0));
pragma Assert (Uval = Abs_Uns_Of_Int (Val));
pragma Assert (if Minus then Uval <= Uns (Int'Last) + 1
else Uval <= Uns (Int'Last));
pragma Assert (Uns_Is_Valid_Int (Minus, Uval));
pragma Assert
(if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
elsif Minus then Val = -(Int (Uval))
else Val = Int (Uval));
pragma Assert (Is_Int_Of_Uns (Minus, Uval, Val));
pragma Assert
(Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
pragma Assert
(not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last));
pragma Assert (Only_Space_Ghost
(Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last));
pragma Assert (Is_Integer_Ghost (Str));
pragma Assert (Is_Value_Integer_Ghost (Str, Val));
Unique_Int_Of_Uns (Val, Value_Integer (Str));
end Prove_Scan_Only_Decimal_Ghost;
------------------
-- Scan_Integer --
------------------

53
gcc/ada/libgnat/s-valuei.ads
View File

@ -56,19 +56,31 @@ generic
-- Additional parameters for ghost subprograms used inside contracts
type Uns_Option is private;
with function Wrap_Option (Value : Uns) return Uns_Option;
with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean;
with function Raw_Unsigned_Overflows_Ghost
(Str : String;
From, To : Integer)
return Boolean;
(Str : String;
From, To : Integer)
return Boolean;
with function Scan_Raw_Unsigned_Ghost
(Str : String;
From, To : Integer)
return Uns;
(Str : String;
From, To : Integer)
return Uns;
with function Raw_Unsigned_Last_Ghost
(Str : String;
From, To : Integer)
return Positive;
(Str : String;
From, To : Integer)
return Positive;
with function Only_Decimal_Ghost
(Str : String;
From, To : Integer)
return Boolean;
with function Scan_Based_Number_Ghost
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
return Uns_Option;
package System.Value_I is
pragma Preelaborate;
@ -96,6 +108,13 @@ package System.Value_I is
Post => True;
-- Return True if Uval (or -Uval when Minus is True) is equal to Val
function Abs_Uns_Of_Int (Val : Int) return Uns is
(if Val = Int'First then Uns (Int'Last) + 1
elsif Val < 0 then Uns (-Val)
else Uns (Val))
with Ghost;
-- Return the unsigned absolute value of Val
procedure Scan_Integer
(Str : String;
Ptr : not null access Integer;
@ -238,6 +257,22 @@ package System.Value_I is
-- argument of the attribute. Constraint_Error is raised if the string is
-- malformed, or if the value is out of range.
procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
with
Ghost,
Pre => Str'Last /= Positive'Last
and then Str'Length >= 2
and then Str (Str'First) in ' ' | '-'
and then (Str (Str'First) = '-') = (Val < 0)
and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
= Wrap_Option (Abs_Uns_Of_Int (Val)),
Post => Is_Integer_Ghost (Slide_If_Necessary (Str))
and then Value_Integer (Str) = Val;
-- Ghost lemma used in the proof of 'Image implementation, to prove that
-- the result of Value_Integer on a decimal string is the same as the
-- signing the result of Scan_Based_Number_Ghost.
private
----------------

35
gcc/ada/libgnat/s-valuti.ads
View File

@ -376,6 +376,41 @@ is
-- no check for this case, the caller must ensure this condition is met.
pragma Warnings (GNATprove, On, """Ptr"" is not modified");
-- Bundle Int type with other types, constants and subprograms used in
-- ghost code, so that this package can be instantiated once and used
-- multiple times as generic formal for a given Int type.
generic
type Int is range <>;
type Uns is mod <>;
type Uns_Option is private;
Unsigned_Width_Ghost : Natural;
with function Wrap_Option (Value : Uns) return Uns_Option;
with function Only_Decimal_Ghost
(Str : String;
From, To : Integer)
return Boolean;
with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
with function Scan_Based_Number_Ghost
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
return Uns_Option;
with function Is_Integer_Ghost (Str : String) return Boolean;
with procedure Prove_Iter_Scan_Based_Number_Ghost
(Str1, Str2 : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0);
with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int);
with function Abs_Uns_Of_Int (Val : Int) return Uns;
with function Value_Integer (Str : String) return Int;
package Int_Params is
end Int_Params;
private
------------------------

2
gcc/ada/libgnat/s-widthu.ads
View File

@ -59,7 +59,7 @@ is
function Big (Arg : Uns) return Big_Integer renames
Unsigned_Conversion.To_Big_Integer;
Big_10 : constant Big_Integer := Big (10) with Ghost;
Big_10 : constant Big_Integer := Big (Uns'(10)) with Ghost;
-- Maximum value of exponent for 10 that fits in Uns'Base
function Max_Log10 return Natural is