public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-233] [Ada] Proof of System.Val_Int at gold level
@ 2022-05-10 8:21 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-10 8:21 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:336ea8f2d6ef528db37212ac7517330274a4793a
commit r13-233-g336ea8f2d6ef528db37212ac7517330274a4793a
Author: Claire Dross <dross@adacore.com>
Date: Thu Jan 20 09:15:28 2022 +0100
[Ada] Proof of System.Val_Int at gold level
gcc/ada/
* libgnat/s-valint.ads: Add SPARK_Mode and pragma to ignore
assertions in instance and add additional ghost parameters to
the instance of Value_I.
* libgnat/s-vallli.ads: Idem.
* libgnat/s-valllli.ads: Idem.
* libgnat/s-valuei.ads, libgnat/s-valuei.adb: New generic
parameters for ghost functions from System.Valueu. Add
functional contracts.
Diff:
---
gcc/ada/libgnat/s-valint.ads | 27 ++++++-
gcc/ada/libgnat/s-vallli.ads | 31 ++++++--
gcc/ada/libgnat/s-valllli.ads | 31 ++++++--
gcc/ada/libgnat/s-valuei.adb | 55 ++++++++++++--
gcc/ada/libgnat/s-valuei.ads | 167 +++++++++++++++++++++++++++++++++++++++++-
5 files changed, 289 insertions(+), 22 deletions(-)
diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads
index 4fef265e9cf..c0d47aa1ce7 100644
--- a/gcc/ada/libgnat/s-valint.ads
+++ b/gcc/ada/libgnat/s-valint.ads
@@ -32,16 +32,39 @@
-- This package contains routines for scanning signed Integer values for use
-- in Text_IO.Integer_IO, and the Value attribute.
+-- 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.Unsigned_Types;
with System.Val_Uns;
with System.Value_I;
-package System.Val_Int is
+package System.Val_Int with SPARK_Mode is
pragma Preelaborate;
subtype Unsigned is Unsigned_Types.Unsigned;
- package Impl is new Value_I (Integer, Unsigned, Val_Uns.Scan_Raw_Unsigned);
+ package Impl is new Value_I
+ (Int => Integer,
+ Uns => Unsigned,
+ Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned,
+ Is_Raw_Unsigned_Format_Ghost =>
+ Val_Uns.Impl.Is_Raw_Unsigned_Format_Ghost,
+ Raw_Unsigned_Overflows_Ghost =>
+ Val_Uns.Impl.Raw_Unsigned_Overflows_Ghost,
+ Scan_Raw_Unsigned_Ghost =>
+ Val_Uns.Impl.Scan_Raw_Unsigned_Ghost,
+ Raw_Unsigned_Last_Ghost =>
+ Val_Uns.Impl.Raw_Unsigned_Last_Ghost);
procedure Scan_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads
index ce1d9ee1340..dfb1729e41c 100644
--- a/gcc/ada/libgnat/s-vallli.ads
+++ b/gcc/ada/libgnat/s-vallli.ads
@@ -32,19 +32,40 @@
-- This package contains routines for scanning signed Long_Long_Integer
-- values for use in Text_IO.Integer_IO, and the Value attribute.
+-- 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.Unsigned_Types;
with System.Val_LLU;
with System.Value_I;
-package System.Val_LLI is
+package System.Val_LLI with SPARK_Mode is
pragma Preelaborate;
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
- package Impl is new
- Value_I (Long_Long_Integer,
- Long_Long_Unsigned,
- Val_LLU.Scan_Raw_Long_Long_Unsigned);
+ package Impl is new Value_I
+ (Int => Long_Long_Integer,
+ Uns => Long_Long_Unsigned,
+ Scan_Raw_Unsigned =>
+ Val_LLU.Scan_Raw_Long_Long_Unsigned,
+ Is_Raw_Unsigned_Format_Ghost =>
+ Val_LLU.Impl.Is_Raw_Unsigned_Format_Ghost,
+ Raw_Unsigned_Overflows_Ghost =>
+ Val_LLU.Impl.Raw_Unsigned_Overflows_Ghost,
+ Scan_Raw_Unsigned_Ghost =>
+ Val_LLU.Impl.Scan_Raw_Unsigned_Ghost,
+ Raw_Unsigned_Last_Ghost =>
+ Val_LLU.Impl.Raw_Unsigned_Last_Ghost);
procedure Scan_Long_Long_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads
index 176000a4060..84bca5878ed 100644
--- a/gcc/ada/libgnat/s-valllli.ads
+++ b/gcc/ada/libgnat/s-valllli.ads
@@ -32,19 +32,40 @@
-- This package contains routines for scanning signed Long_Long_Long_Integer
-- values for use in Text_IO.Integer_IO, and the Value attribute.
+-- 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.Unsigned_Types;
with System.Val_LLLU;
with System.Value_I;
-package System.Val_LLLI is
+package System.Val_LLLI with SPARK_Mode is
pragma Preelaborate;
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
- package Impl is new
- Value_I (Long_Long_Long_Integer,
- Long_Long_Long_Unsigned,
- Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned);
+ package Impl is new Value_I
+ (Int => Long_Long_Long_Integer,
+ Uns => Long_Long_Long_Unsigned,
+ Scan_Raw_Unsigned =>
+ Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned,
+ Is_Raw_Unsigned_Format_Ghost =>
+ Val_LLLU.Impl.Is_Raw_Unsigned_Format_Ghost,
+ Raw_Unsigned_Overflows_Ghost =>
+ Val_LLLU.Impl.Raw_Unsigned_Overflows_Ghost,
+ Scan_Raw_Unsigned_Ghost =>
+ Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost,
+ Raw_Unsigned_Last_Ghost =>
+ Val_LLLU.Impl.Raw_Unsigned_Last_Ghost);
procedure Scan_Long_Long_Long_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index 83828d34dd7..faf57915c78 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -29,10 +29,18 @@
-- --
------------------------------------------------------------------------------
-with System.Val_Util; use System.Val_Util;
-
package body System.Value_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,
+ Subprogram_Variant => Ignore);
+
------------------
-- Scan_Integer --
------------------
@@ -46,26 +54,35 @@ package body System.Value_I is
Uval : Uns;
-- Unsigned result
- Minus : Boolean := False;
+ Minus : Boolean;
-- Set to True if minus sign is present, otherwise to False
- Start : Positive;
+ Unused_Start : Positive;
-- Saves location of first non-blank (not used in this case)
+ Non_Blank : constant Positive :=
+ First_Non_Space_Ghost (Str, Ptr.all, Max)
+ with Ghost;
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+ else Non_Blank)
+ with Ghost;
+
begin
- Scan_Sign (Str, Ptr, Max, Minus, Start);
+ Scan_Sign (Str, Ptr, Max, Minus, Unused_Start);
if Str (Ptr.all) not in '0' .. '9' then
- Ptr.all := Start;
+ Ptr.all := Unused_Start;
Bad_Value (Str);
end if;
Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
+ pragma Assert (Uval = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
-- Deal with overflow cases, and also with largest negative number
if Uval > Uns (Int'Last) then
- if Minus and then Uval = Uns (-(Int'First)) then
+ if Minus and then Uval = Uns (Int'Last) + 1 then
Res := Int'First;
else
Bad_Value (Str);
@@ -106,9 +123,31 @@ package body System.Value_I is
declare
V : Int;
P : aliased Integer := Str'First;
+
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last)
+ with Ghost;
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+ else Non_Blank)
+ with Ghost;
begin
- Scan_Integer (Str, P'Access, Str'Last, V);
+ pragma Assert
+ (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+
+ declare
+ P_Acc : constant not null access Integer := P'Access;
+ begin
+ Scan_Integer (Str, P_Acc, Str'Last, V);
+ end;
+
+ pragma Assert
+ (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+
Scan_Trailing_Blanks (Str, P);
+
+ pragma Assert
+ (Is_Value_Integer_Ghost (Slide_If_Necessary (Str), V));
return V;
end;
end if;
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index e0a34d9465c..d6a78fda540 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -32,6 +32,16 @@
-- This package contains routines for scanning signed integer values for use
-- in Text_IO.Integer_IO, and the Value attribute.
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+pragma Warnings (Off, "postcondition does not mention function result");
+-- True postconditions are used to avoid inlining for GNATprove
+
+with System.Val_Util; use System.Val_Util;
+
generic
type Int is range <>;
@@ -44,14 +54,86 @@ generic
Max : Integer;
Res : out Uns);
+ -- Additional parameters for ghost subprograms used inside contracts
+
+ with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean;
+ with function Raw_Unsigned_Overflows_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Boolean;
+ with function Scan_Raw_Unsigned_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Uns;
+ with function Raw_Unsigned_Last_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Positive;
+
package System.Value_I is
pragma Preelaborate;
+ function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
+ (if Minus then Uval <= Uns (Int'Last) + 1
+ else Uval <= Uns (Int'Last))
+ with Ghost,
+ Post => True;
+ -- Return True if Uval (or -Uval when Minus is True) is a valid number of
+ -- type Int.
+
+ function Is_Int_Of_Uns
+ (Minus : Boolean;
+ Uval : Uns;
+ Val : Int)
+ return Boolean
+ is
+ (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
+ elsif Minus then Val = -(Int (Uval))
+ else Val = Int (Uval))
+ with Ghost,
+ Pre => Uns_Is_Valid_Int (Minus, Uval),
+ Post => True;
+ -- Return True if Uval (or -Uval when Minus is True) is equal to Val
+
procedure Scan_Integer
(Str : String;
Ptr : not null access Integer;
Max : Integer;
- Res : out Int);
+ Res : out Int)
+ with
+ Pre =>
+ Str'Last /= Positive'Last
+ -- Ptr.all .. Max is either an empty range, or a valid range in Str
+ and then (Ptr.all > Max
+ or else (Ptr.all >= Str'First and then Max <= Str'Last))
+ and then not Only_Space_Ghost (Str, Ptr.all, Max)
+ and then
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Ptr.all, Max);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+ else Non_Blank);
+ begin
+ Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
+ and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
+ and then Uns_Is_Valid_Int
+ (Minus => Str (Non_Blank) = '-',
+ Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))),
+ Post =>
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Ptr.all'Old, Max);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+ else Non_Blank);
+ Uval : constant Uns :=
+ Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
+ begin
+ Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+ Uval => Uval,
+ Val => Res)
+ and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
-- This procedure scans the string starting at Str (Ptr.all) for a valid
-- integer according to the syntax described in (RM 3.5(43)). The substring
-- scanned extends no further than Str (Max). There are three cases for the
@@ -77,10 +159,91 @@ package System.Value_I is
-- special case of an all-blank string, and Ptr is unchanged, and hence
-- is greater than Max as required in this case.
- function Value_Integer (Str : String) return Int;
+ function Slide_To_1 (Str : String) return String
+ with Ghost,
+ Post =>
+ Only_Space_Ghost (Str, Str'First, Str'Last) =
+ (for all J in Str'First .. Str'Last =>
+ Slide_To_1'Result (J - Str'First + 1) = ' ');
+ -- Slides Str so that it starts at 1
+
+ function Slide_If_Necessary (Str : String) return String is
+ (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
+ with Ghost,
+ Post =>
+ Only_Space_Ghost (Str, Str'First, Str'Last) =
+ Only_Space_Ghost (Slide_If_Necessary'Result,
+ Slide_If_Necessary'Result'First,
+ Slide_If_Necessary'Result'Last);
+ -- If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+ function Is_Integer_Ghost (Str : String) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
+ begin
+ Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+ and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
+ and then
+ Uns_Is_Valid_Int
+ (Minus => Str (Non_Blank) = '-',
+ Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
+ and then Only_Space_Ghost
+ (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
+ with Ghost,
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last,
+ Post => True;
+ -- Ghost function that determines if Str has the correct format for a
+ -- signed number, consisting in some blank characters, an optional
+ -- sign, a raw unsigned number which does not overflow and then some
+ -- more blank characters.
+
+ function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
+ Uval : constant Uns :=
+ Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
+ begin
+ Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+ Uval => Uval,
+ Val => Val))
+ with Ghost,
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last
+ and then Is_Integer_Ghost (Str),
+ Post => True;
+ -- Ghost function that returns True if Val is the value corresponding to
+ -- the signed number represented by Str.
+
+ function Value_Integer (Str : String) return Int
+ with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Length /= Positive'Last
+ and then Is_Integer_Ghost (Slide_If_Necessary (Str)),
+ Post =>
+ Is_Value_Integer_Ghost
+ (Slide_If_Necessary (Str), Value_Integer'Result),
+ Subprogram_Variant => (Decreases => Str'First);
-- Used in computing X'Value (Str) where X is a signed integer type whose
-- base range does not exceed the base range of Integer. Str is the string
-- argument of the attribute. Constraint_Error is raised if the string is
-- malformed, or if the value is out of range.
+private
+
+ ----------------
+ -- Slide_To_1 --
+ ----------------
+
+ function Slide_To_1 (Str : String) return String is
+ (declare
+ Res : constant String (1 .. Str'Length) := Str;
+ begin
+ Res);
+
end System.Value_I;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-10 8:21 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-10 8:21 [gcc r13-233] [Ada] Proof of System.Val_Int at gold level 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).