diff options
Diffstat (limited to 'gcc/ada/libgnat/s-vauspe.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-vauspe.ads | 629 |
1 files changed, 0 insertions, 629 deletions
diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads deleted file mode 100644 index 5dbb57d..0000000 --- a/gcc/ada/libgnat/s-vauspe.ads +++ /dev/null @@ -1,629 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- S Y S T E M . V A L U E _ U _ S P E C -- --- -- --- S p e c -- --- -- --- Copyright (C) 2022-2025, Free Software Foundation, Inc. -- --- -- --- GNAT is free software; you can redistribute it and/or modify it under -- --- terms of the GNU General Public License as published by the Free Soft- -- --- ware Foundation; either version 3, or (at your option) any later ver- -- --- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- --- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- --- or FITNESS FOR A PARTICULAR PURPOSE. -- --- -- --- As a special exception under Section 7 of GPL version 3, you are granted -- --- additional permissions described in the GCC Runtime Library Exception, -- --- version 3.1, as published by the Free Software Foundation. -- --- -- --- You should have received a copy of the GNU General Public License and -- --- a copy of the GCC Runtime Library Exception along with this program; -- --- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- --- <http://www.gnu.org/licenses/>. -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This package is part of a set of Ghost code packages used to proof the --- implementations of the Image and Value attributes. It provides the --- specification entities using for the formal verification of the routines --- for scanning modular unsigned integer values. - --- 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_Spec; use System.Val_Spec; - -generic - - type Uns is mod <>; - -package System.Value_U_Spec with - Ghost, - SPARK_Mode, - Always_Terminates -is - pragma Preelaborate; - - -- Maximum value of exponent for 10 that fits in Uns'Base - function Max_Log10 return Natural is - (case Uns'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; - - pragma Annotate (Gnatcheck, Exempt_On, "Discriminated_Records", - "variant record only used in proof code"); - type Uns_Option (Overflow : Boolean := False) is record - case Overflow is - when True => - null; - when False => - Value : Uns := 0; - end case; - end record; - pragma Annotate (Gnatcheck, Exempt_Off, "Discriminated_Records"); - - function Wrap_Option (Value : Uns) return Uns_Option is - (Overflow => False, Value => Value); - - function Only_Decimal_Ghost - (Str : String; - From, To : Integer) - return Boolean - is - (for all J in From .. To => Str (J) in '0' .. '9') - with - Pre => From > To or else (From >= Str'First and then To <= Str'Last); - -- Ghost function that returns True if S has only decimal characters - -- from index From to index To. - - function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean - is - (for all J in From .. To => - Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_') - with - Pre => From > To or else (From >= Str'First and then To <= Str'Last); - -- Ghost function that returns True if S has only hexadecimal characters - -- from index From to index To. - - function Last_Hexa_Ghost (Str : String) return Positive - with - Pre => Str /= "" - and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F', - Post => Last_Hexa_Ghost'Result in Str'Range - and then (if Last_Hexa_Ghost'Result < Str'Last then - Str (Last_Hexa_Ghost'Result + 1) not in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_') - and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result); - -- Ghost function that returns the index of the last character in S that - -- is either an hexadecimal digit or an underscore, which necessarily - -- exists given the precondition on Str. - - function Is_Based_Format_Ghost (Str : String) return Boolean - is - (Str /= "" - and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' - and then - (declare - L : constant Positive := Last_Hexa_Ghost (Str); - begin - Str (L) /= '_' - and then (for all J in Str'First .. L => - (if Str (J) = '_' then Str (J + 1) /= '_')))); - -- Ghost function that determines if Str has the correct format for a - -- based number, consisting in a sequence of hexadecimal digits possibly - -- separated by single underscores. It may be followed by other characters. - - function Hexa_To_Unsigned_Ghost (X : Character) return Uns is - (case X is - when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'), - when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10, - when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10, - when others => raise Program_Error) - with - Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; - -- Ghost function that computes the value corresponding to an hexadecimal - -- digit. - - function Scan_Overflows_Ghost - (Digit : Uns; - Base : Uns; - Acc : Uns) return Boolean - is - (Digit >= Base - or else Acc > Uns'Last / Base - or else Uns'Last - Digit < Base * Acc); - -- Ghost function which returns True if Digit + Base * Acc overflows or - -- Digit is greater than Base, as this is used by the algorithm for the - -- test of overflow. - - function Scan_Based_Number_Ghost - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) return Uns_Option - with - Subprogram_Variant => (Increases => From), - Pre => Str'Last /= Positive'Last - and then - (From > To or else (From >= Str'First and then To <= Str'Last)) - and then Only_Hexa_Ghost (Str, From, To); - -- Ghost function that recursively computes the based number in Str, - -- assuming Acc has been scanned already and scanning continues at index - -- From. - - -- Lemmas unfolding the recursive definition of Scan_Based_Number_Ghost - - procedure Lemma_Scan_Based_Number_Ghost_Base - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Global => null, - Pre => Str'Last /= Positive'Last - and then - (From > To or else (From >= Str'First and then To <= Str'Last)) - and then Only_Hexa_Ghost (Str, From, To), - Post => - (if From > To - then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = - (Overflow => False, Value => Acc)); - -- Base case: Scan_Based_Number_Ghost returns Acc if From is bigger than To - - procedure Lemma_Scan_Based_Number_Ghost_Underscore - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Global => null, - Pre => Str'Last /= Positive'Last - and then - (From > To or else (From >= Str'First and then To <= Str'Last)) - and then Only_Hexa_Ghost (Str, From, To), - Post => - (if From <= To and then Str (From) = '_' - then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = - Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)); - -- Underscore case: underscores are ignored while scanning - - procedure Lemma_Scan_Based_Number_Ghost_Overflow - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Global => null, - Pre => Str'Last /= Positive'Last - and then - (From > To or else (From >= Str'First and then To <= Str'Last)) - and then Only_Hexa_Ghost (Str, From, To), - Post => - (if From <= To - and then Str (From) /= '_' - and then Scan_Overflows_Ghost - (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) - then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = - (Overflow => True)); - -- Overflow case: scanning a digit which causes an overflow - - procedure Lemma_Scan_Based_Number_Ghost_Step - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Global => null, - Pre => Str'Last /= Positive'Last - and then - (From > To or else (From >= Str'First and then To <= Str'Last)) - and then Only_Hexa_Ghost (Str, From, To), - Post => - (if From <= To - and then Str (From) /= '_' - and then not Scan_Overflows_Ghost - (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) - then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = - Scan_Based_Number_Ghost - (Str, From + 1, To, Base, - Base * Acc + Hexa_To_Unsigned_Ghost (Str (From)))); - -- Normal case: scanning a digit without overflows - - function Exponent_Unsigned_Ghost - (Value : Uns; - Exp : Natural; - Base : Uns := 10) return Uns_Option - with - Subprogram_Variant => (Decreases => Exp); - -- Ghost function that recursively computes Value * Base ** Exp - - -- Lemmas unfolding the recursive definition of Exponent_Unsigned_Ghost - - procedure Lemma_Exponent_Unsigned_Ghost_Base - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - with - Post => - (if Exp = 0 or Value = 0 - then Exponent_Unsigned_Ghost (Value, Exp, Base) = - (Overflow => False, Value => Value)); - -- Base case: Exponent_Unsigned_Ghost returns 0 if Value or Exp is 0 - - procedure Lemma_Exponent_Unsigned_Ghost_Overflow - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - with - Post => - (if Exp /= 0 - and then Value /= 0 - and then Scan_Overflows_Ghost (0, Base, Value) - then Exponent_Unsigned_Ghost (Value, Exp, Base) = (Overflow => True)); - -- Overflow case: the next multiplication overflows - - procedure Lemma_Exponent_Unsigned_Ghost_Step - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - with - Post => - (if Exp /= 0 - and then Value /= 0 - and then not Scan_Overflows_Ghost (0, Base, Value) - then Exponent_Unsigned_Ghost (Value, Exp, Base) = - Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base)); - -- Normal case: exponentiation without overflows - - function Raw_Unsigned_Starts_As_Based_Ghost - (Str : String; - Last_Num_Init, To : Integer) - return Boolean - is - (Last_Num_Init < To - 1 - and then Str (Last_Num_Init + 1) in '#' | ':' - and then Str (Last_Num_Init + 2) in - '0' .. '9' | 'a' .. 'f' | 'A' .. 'F') - with Ghost, - Pre => Last_Num_Init in Str'Range - and then To in Str'Range; - -- Return True if Str starts as a based number - - function Raw_Unsigned_Is_Based_Ghost - (Str : String; - Last_Num_Init : Integer; - Last_Num_Based : Integer; - To : Integer) - return Boolean - is - (Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To) - and then Last_Num_Based < To - and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)) - with Ghost, - Pre => Last_Num_Init in Str'Range - and then Last_Num_Based in Last_Num_Init .. Str'Last - and then To in Str'Range; - -- Return True if Str is a based number - - function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is - (Is_Natural_Format_Ghost (Str) - and then - (declare - Last_Num_Init : constant Integer := Last_Number_Ghost (Str); - Starts_As_Based : constant Boolean := - Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Str'Last); - Last_Num_Based : constant Integer := - (if Starts_As_Based - then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) - else Last_Num_Init); - Is_Based : constant Boolean := - Raw_Unsigned_Is_Based_Ghost - (Str, Last_Num_Init, Last_Num_Based, Str'Last); - First_Exp : constant Integer := - (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); - begin - (if Starts_As_Based then - Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) - and then Last_Num_Based < Str'Last) - and then Is_Opt_Exponent_Format_Ghost - (Str (First_Exp .. Str'Last)))) - with - Pre => Str'Last /= Positive'Last; - -- Ghost function that determines if Str has the correct format for an - -- unsigned number without a sign character. - -- It is a natural number in base 10, optionally followed by a based - -- number surrounded by delimiters # or :, optionally followed by an - -- exponent part. - - type Split_Value_Ghost is record - Value : Uns; - Base : Uns; - Expon : Natural; - end record; - - function Scan_Split_No_Overflow_Ghost - (Str : String; - From, To : Integer) - return Boolean - is - (declare - Last_Num_Init : constant Integer := - Last_Number_Ghost (Str (From .. To)); - Init_Val : constant Uns_Option := - Scan_Based_Number_Ghost (Str, From, Last_Num_Init); - Starts_As_Based : constant Boolean := - Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); - Last_Num_Based : constant Integer := - (if Starts_As_Based - then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) - else Last_Num_Init); - Based_Val : constant Uns_Option := - (if Starts_As_Based and then not Init_Val.Overflow - then Scan_Based_Number_Ghost - (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) - else Init_Val); - begin - not Init_Val.Overflow - and then - (Last_Num_Init >= To - 1 - or else Str (Last_Num_Init + 1) not in '#' | ':' - or else Init_Val.Value in 2 .. 16) - and then - (not Starts_As_Based - or else not Based_Val.Overflow)) - with - Pre => Str'Last /= Positive'Last - and then From in Str'Range - and then To in From .. Str'Last - and then Str (From) in '0' .. '9'; - -- Ghost function that determines if an overflow might occur while scanning - -- the representation of an unsigned number. The computation overflows if - -- either: - -- * The computation of the decimal part overflows, - -- * The decimal part is followed by a valid delimiter for a based - -- part, and the number corresponding to the base is not a valid base, - -- or - -- * The computation of the based part overflows. - - pragma Warnings (Off, "constant * is not referenced"); - function Scan_Split_Value_Ghost - (Str : String; - From, To : Integer) - return Split_Value_Ghost - is - (declare - Last_Num_Init : constant Integer := - Last_Number_Ghost (Str (From .. To)); - Init_Val : constant Uns_Option := - Scan_Based_Number_Ghost (Str, From, Last_Num_Init); - Starts_As_Based : constant Boolean := - Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); - Last_Num_Based : constant Integer := - (if Starts_As_Based - then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) - else Last_Num_Init); - Is_Based : constant Boolean := - Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To); - Based_Val : constant Uns_Option := - (if Starts_As_Based and then not Init_Val.Overflow - then Scan_Based_Number_Ghost - (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) - else Init_Val); - First_Exp : constant Integer := - (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); - Expon : constant Natural := - (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) - then Scan_Exponent_Ghost (Str (First_Exp .. To)) - else 0); - Base : constant Uns := - (if Is_Based then Init_Val.Value else 10); - Value : constant Uns := - (if Is_Based then Based_Val.Value else Init_Val.Value); - begin - (Value => Value, Base => Base, Expon => Expon)) - with - Pre => Str'Last /= Positive'Last - and then From in Str'Range - and then To in From .. Str'Last - and then Str (From) in '0' .. '9' - and then Scan_Split_No_Overflow_Ghost (Str, From, To); - -- Ghost function that scans an unsigned number without a sign character - -- and return a record containing the values scanned for its value, its - -- base, and its exponent. - pragma Warnings (On, "constant * is not referenced"); - - function Raw_Unsigned_No_Overflow_Ghost - (Str : String; - From, To : Integer) - return Boolean - is - (Scan_Split_No_Overflow_Ghost (Str, From, To) - and then - (declare - Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost - (Str, From, To); - begin - not Exponent_Unsigned_Ghost - (Val.Value, Val.Expon, Val.Base).Overflow)) - with - Pre => Str'Last /= Positive'Last - and then From in Str'Range - and then To in From .. Str'Last - and then Str (From) in '0' .. '9'; - -- Ghost function that determines if the computation of the unsigned number - -- represented by Str will overflow. The computation overflows if either: - -- * The scan of the string overflows, or - -- * The computation of the exponentiation overflows. - - function Scan_Raw_Unsigned_Ghost - (Str : String; - From, To : Integer) - return Uns - is - (declare - Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost - (Str, From, To); - begin - Exponent_Unsigned_Ghost (Val.Value, Val.Expon, Val.Base).Value) - with - Pre => Str'Last /= Positive'Last - and then From in Str'Range - and then To in From .. Str'Last - and then Str (From) in '0' .. '9' - and then Raw_Unsigned_No_Overflow_Ghost (Str, From, To); - -- Ghost function that scans an unsigned number without a sign character - - function Raw_Unsigned_Last_Ghost - (Str : String; - From, To : Integer) - return Positive - is - (declare - Last_Num_Init : constant Integer := - Last_Number_Ghost (Str (From .. To)); - Starts_As_Based : constant Boolean := - Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, To); - Last_Num_Based : constant Integer := - (if Starts_As_Based - then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) - else Last_Num_Init); - Is_Based : constant Boolean := - Raw_Unsigned_Is_Based_Ghost (Str, Last_Num_Init, Last_Num_Based, To); - First_Exp : constant Integer := - (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); - begin - (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) - then First_Exp - elsif Str (First_Exp + 1) in '-' | '+' then - Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1 - else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1)) - with - Pre => Str'Last /= Positive'Last - and then From in Str'Range - and then To in From .. Str'Last - and then Str (From) in '0' .. '9', - Post => Raw_Unsigned_Last_Ghost'Result >= From; - -- Ghost function that returns the position of the cursor once an unsigned - -- number has been seen. - - function Slide_To_1 (Str : String) return String - with - 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); - -- If Str'Last = Positive'Last then slides Str so that it starts at 1 - - function Is_Unsigned_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) = '+' then Non_Blank + 1 else Non_Blank); - begin - Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)) - and then Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last) - and then Only_Space_Ghost - (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)) - with - Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) - and then Str'Last /= Positive'Last; - -- Ghost function that determines if Str has the correct format for an - -- unsigned 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_Unsigned_Ghost (Str : String; Val : Uns) 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) = '+' then Non_Blank + 1 else Non_Blank); - begin - Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last)) - with - Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) - and then Str'Last /= Positive'Last - and then Is_Unsigned_Ghost (Str); - -- Ghost function that returns True if Val is the value corresponding to - -- the unsigned number represented by Str. - - procedure Prove_Scan_Based_Number_Ghost_Eq - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Subprogram_Variant => (Increases => From), - Pre => Str1'Last /= Positive'Last - and then Str2'Last /= Positive'Last - and then - (From > To or else (From >= Str1'First and then To <= Str1'Last)) - and then - (From > To or else (From >= Str2'First and then To <= Str2'Last)) - and then Only_Hexa_Ghost (Str1, From, To) - 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); - -- Scan_Based_Number_Ghost returns the same value on two slices which are - -- equal. - - procedure Prove_Scan_Only_Decimal_Ghost - (Str : String; - Val : Uns) - with - Pre => Str'Last /= Positive'Last - and then Str'Length >= 2 - and then Str (Str'First) = ' ' - 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 (Val), - Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str)) - and then - Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), Val); - -- Ghost lemma used in the proof of 'Image implementation, to prove that - -- the result of Value_Unsigned on a decimal string is the same as the - -- result of Scan_Based_Number_Ghost. - - -- Bundle Uns 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. - -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_U_Spec; |