------------------------------------------------------------------------------ -- -- -- GNAT COMPILER COMPONENTS -- -- -- -- S Y S T E M . V A L U E _ U -- -- -- -- B o d y -- -- -- -- Copyright (C) 1992-2022, 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 -- -- . -- -- -- -- GNAT was originally developed by the GNAT team at New York University. -- -- Extensive contributions were provided by Ada Core Technologies Inc. -- -- -- ------------------------------------------------------------------------------ package body System.Value_U 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); use type Spec.Uns_Option; use type Spec.Split_Value_Ghost; -- Local lemmas procedure Lemma_Digit_Not_Last (Str : String; P : Integer; From : Integer; To : Integer) with Ghost, 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' | 'a' .. 'f' | 'A' .. 'F' and then P in From .. To and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1 and then Spec.Is_Based_Format_Ghost (Str (From .. To)), Post => (if Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' then P <= Spec.Last_Hexa_Ghost (Str (From .. To))); procedure Lemma_Underscore_Not_Last (Str : String; P : Integer; From : Integer; To : Integer) with Ghost, 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' | 'a' .. 'f' | 'A' .. 'F' and then P in From .. To and then Str (P) = '_' and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1 and then Spec.Is_Based_Format_Ghost (Str (From .. To)), Post => P + 1 <= Spec.Last_Hexa_Ghost (Str (From .. To)) and then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; ----------------------------- -- Local lemma null bodies -- ----------------------------- procedure Lemma_Digit_Not_Last (Str : String; P : Integer; From : Integer; To : Integer) is null; procedure Lemma_Underscore_Not_Last (Str : String; P : Integer; From : Integer; To : Integer) is null; ----------------------- -- Scan_Raw_Unsigned -- ----------------------- procedure Scan_Raw_Unsigned (Str : String; Ptr : not null access Integer; Max : Integer; Res : out Uns) is P : Integer; -- Local copy of the pointer Uval : Uns; -- Accumulated unsigned integer result Expon : Integer; -- Exponent value Overflow : Boolean := False; -- Set True if overflow is detected at any point Base_Char : Character; -- Base character (# or :) in based case Base : Uns := 10; -- Base value (reset in based case) Digit : Uns; -- Digit value Ptr_Old : constant Integer := Ptr.all with Ghost; Last_Num_Init : constant Integer := Last_Number_Ghost (Str (Ptr.all .. Max)) with Ghost; Init_Val : constant Spec.Uns_Option := Spec.Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init) with Ghost; Starts_As_Based : constant Boolean := Last_Num_Init < Max - 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; Last_Num_Based : constant Integer := (if Starts_As_Based then Spec.Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max)) else Last_Num_Init) with Ghost; Is_Based : constant Boolean := Starts_As_Based and then Last_Num_Based < Max and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1) with Ghost; Based_Val : constant Spec.Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow then Spec.Scan_Based_Number_Ghost (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) else Init_Val) with Ghost; First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1) with Ghost; begin -- We do not tolerate strings with Str'Last = Positive'Last if Str'Last = Positive'Last then raise Program_Error with "string upper bound is Positive'Last, not supported"; end if; P := Ptr.all; Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init); Uval := Character'Pos (Str (P)) - Character'Pos ('0'); P := P + 1; -- Scan out digits of what is either the number or the base. -- In either case, we are definitely scanning out in base 10. declare Umax : constant Uns := (Uns'Last - 9) / 10; -- Max value which cannot overflow on accumulating next digit Umax10 : constant Uns := Uns'Last / 10; -- Numbers bigger than Umax10 overflow if multiplied by 10 begin -- Loop through decimal digits loop pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Init + 1); pragma Loop_Invariant (if Overflow then Init_Val.Overflow); pragma Loop_Invariant (if not Overflow then Init_Val = Spec.Scan_Based_Number_Ghost (Str, P, Last_Num_Init, Acc => Uval)); exit when P > Max; Digit := Character'Pos (Str (P)) - Character'Pos ('0'); -- Non-digit encountered if Digit > 9 then if Str (P) = '_' then Spec.Lemma_Scan_Based_Number_Ghost_Underscore (Str, P, Last_Num_Init, Acc => Uval); Scan_Underscore (Str, P, Ptr, Max, False); else exit; end if; -- Accumulate result, checking for overflow else Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init, Acc => Uval); Spec.Lemma_Scan_Based_Number_Ghost_Overflow (Str, P, Last_Num_Init, Acc => Uval); if Uval <= Umax then pragma Assert (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit); Uval := 10 * Uval + Digit; pragma Assert (if not Overflow then Init_Val = Spec.Scan_Based_Number_Ghost (Str, P + 1, Last_Num_Init, Acc => Uval)); elsif Uval > Umax10 then Overflow := True; else Uval := 10 * Uval + Digit; if Uval < Umax10 then Overflow := True; end if; pragma Assert (if not Overflow then Init_Val = Spec.Scan_Based_Number_Ghost (Str, P + 1, Last_Num_Init, Acc => Uval)); end if; P := P + 1; end if; end loop; Spec.Lemma_Scan_Based_Number_Ghost_Base (Str, P, Last_Num_Init, Acc => Uval); end; pragma Assert_And_Cut (P = Last_Num_Init + 1 and then Overflow = Init_Val.Overflow and then (if not Overflow then Init_Val.Value = Uval)); Ptr.all := P; -- Deal with based case. We recognize either the standard '#' or the -- allowed alternative replacement ':' (see RM J.2(3)). if P < Max and then (Str (P) = '#' or else Str (P) = ':') then Base_Char := Str (P); P := P + 1; Base := Uval; Uval := 0; -- Check base value. Overflow is set True if we find a bad base, or -- a digit that is out of range of the base. That way, we scan out -- the numeral that is still syntactically correct, though illegal. -- We use a safe base of 16 for this scan, to avoid zero divide. if Base not in 2 .. 16 then Overflow := True; Base := 16; end if; -- Scan out based integer declare Umax : constant Uns := (Uns'Last - Base + 1) / Base; -- Max value which cannot overflow on accumulating next digit UmaxB : constant Uns := Uns'Last / Base; -- Numbers bigger than UmaxB overflow if multiplied by base begin pragma Assert (if Str (P) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f' then Spec.Is_Based_Format_Ghost (Str (P .. Max))); -- Loop to scan out based integer value loop -- We require a digit at this stage if Str (P) in '0' .. '9' then Digit := Character'Pos (Str (P)) - Character'Pos ('0'); elsif Str (P) in 'A' .. 'F' then Digit := Character'Pos (Str (P)) - (Character'Pos ('A') - 10); elsif Str (P) in 'a' .. 'f' then Digit := Character'Pos (Str (P)) - (Character'Pos ('a') - 10); -- If we don't have a digit, then this is not a based number -- after all, so we use the value we scanned out as the base -- (now in Base), and the pointer to the base character was -- already stored in Ptr.all. else Spec.Lemma_Scan_Based_Number_Ghost_Base (Str, P, Last_Num_Based, Base, Uval); Uval := Base; Base := 10; pragma Assert (Ptr.all = Last_Num_Init + 1); pragma Assert (if Starts_As_Based then P = Last_Num_Based + 1); pragma Assert (not Is_Based); pragma Assert (if not Overflow then Uval = Init_Val.Value); exit; end if; pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Based); pragma Loop_Invariant (Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' and then Digit = Spec.Hexa_To_Unsigned_Ghost (Str (P))); pragma Loop_Invariant (if Overflow'Loop_Entry then Overflow); pragma Loop_Invariant (if Overflow then (Overflow'Loop_Entry or else Based_Val.Overflow)); pragma Loop_Invariant (if not Overflow then Based_Val = Spec.Scan_Based_Number_Ghost (Str, P, Last_Num_Based, Base, Uval)); pragma Loop_Invariant (Ptr.all = Last_Num_Init + 1); Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Based, Base, Uval); Spec.Lemma_Scan_Based_Number_Ghost_Overflow (Str, P, Last_Num_Based, Base, Uval); -- If digit is too large, just signal overflow and continue. -- The idea here is to keep scanning as long as the input is -- syntactically valid, even if we have detected overflow if Digit >= Base then Overflow := True; -- Here we accumulate the value, checking overflow elsif Uval <= Umax then Uval := Base * Uval + Digit; pragma Assert (if not Overflow then Based_Val = Spec.Scan_Based_Number_Ghost (Str, P + 1, Last_Num_Based, Base, Uval)); elsif Uval > UmaxB then Overflow := True; else Uval := Base * Uval + Digit; if Uval < UmaxB then Overflow := True; end if; pragma Assert (if not Overflow then Based_Val = Spec.Scan_Based_Number_Ghost (Str, P + 1, Last_Num_Based, Base, Uval)); end if; -- If at end of string with no base char, not a based number -- but we signal Constraint_Error and set the pointer past -- the end of the field, since this is what the ACVC tests -- seem to require, see CE3704N, line 204. P := P + 1; if P > Max then Ptr.all := P; Bad_Value (Str); end if; -- If terminating base character, we are done with loop if Str (P) = Base_Char then Ptr.all := P + 1; pragma Assert (P = Last_Num_Based + 1); pragma Assert (Ptr.all = Last_Num_Based + 2); pragma Assert (Starts_As_Based); pragma Assert (Last_Num_Based < Max); pragma Assert (Str (Last_Num_Based + 1) = Base_Char); pragma Assert (Base_Char = Str (Last_Num_Init + 1)); pragma Assert (Is_Based); Spec.Lemma_Scan_Based_Number_Ghost_Base (Str, P, Last_Num_Based, Base, Uval); exit; -- Deal with underscore elsif Str (P) = '_' then Lemma_Underscore_Not_Last (Str, P, Last_Num_Init + 2, Max); Spec.Lemma_Scan_Based_Number_Ghost_Underscore (Str, P, Last_Num_Based, Base, Uval); Scan_Underscore (Str, P, Ptr, Max, True); pragma Assert (if not Overflow then Based_Val = Spec.Scan_Based_Number_Ghost (Str, P, Last_Num_Based, Base, Uval)); pragma Assert (Str (P) /= '_'); pragma Assert (Str (P) /= Base_Char); end if; Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max); pragma Assert (Str (P) /= '_'); pragma Assert (Str (P) /= Base_Char); end loop; end; pragma Assert (if Starts_As_Based then P = Last_Num_Based + 1 else P = Last_Num_Init + 2); pragma Assert (Last_Num_Init < Max - 1 and then Str (Last_Num_Init + 1) in '#' | ':'); pragma Assert (Overflow = (Init_Val.Overflow or else Init_Val.Value not in 2 .. 16 or else (Starts_As_Based and then Based_Val.Overflow))); pragma Assert (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)); end if; pragma Assert_And_Cut (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max) and then (if not Overflow then (if Is_Based then Uval = Based_Val.Value else Uval = Init_Val.Value)) and then Ptr.all = First_Exp and then Base in 2 .. 16 and then (if not Overflow then (if Is_Based then Base = Init_Val.Value else Base = 10))); -- Come here with scanned unsigned value in Uval. The only remaining -- required step is to deal with exponent if one is present. Scan_Exponent (Str, Ptr, Max, Expon); pragma Assert (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max)); pragma Assert (if not Overflow then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) = (Uval, Base, Expon)); if Expon /= 0 and then Uval /= 0 then -- For non-zero value, scale by exponent value. No need to do this -- efficiently, since use of exponent in integer literals is rare, -- and in any case the exponent cannot be very large. declare UmaxB : constant Uns := Uns'Last / Base; -- Numbers bigger than UmaxB overflow if multiplied by base Res_Val : constant Spec.Uns_Option := Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base) with Ghost; begin for J in 1 .. Expon loop pragma Loop_Invariant (if Overflow'Loop_Entry then Overflow); pragma Loop_Invariant (if Overflow then Overflow'Loop_Entry or else Res_Val.Overflow); pragma Loop_Invariant (Uval /= 0); pragma Loop_Invariant (if not Overflow then Res_Val = Spec.Exponent_Unsigned_Ghost (Uval, Expon - J + 1, Base)); pragma Assert ((Uval > UmaxB) = Spec.Scan_Overflows_Ghost (0, Base, Uval)); if Uval > UmaxB then Spec.Lemma_Exponent_Unsigned_Ghost_Overflow (Uval, Expon - J + 1, Base); Overflow := True; exit; end if; Spec.Lemma_Exponent_Unsigned_Ghost_Step (Uval, Expon - J + 1, Base); Uval := Uval * Base; end loop; Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, Base); pragma Assert (Overflow /= Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max)); pragma Assert (if not Overflow then Res_Val = (False, Uval)); end; end if; Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, Expon, Base); pragma Assert (if Expon = 0 or else Uval = 0 then Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval)); pragma Assert (Overflow /= Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max)); pragma Assert (if not Overflow then Uval = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max)); -- Return result, dealing with overflow if Overflow then Bad_Value (Str); pragma Annotate (GNATprove, Intentional, "call to nonreturning subprogram might be executed", "it is expected that Constraint_Error is raised in case of" & " overflow"); else Res := Uval; end if; end Scan_Raw_Unsigned; ------------------- -- Scan_Unsigned -- ------------------- procedure Scan_Unsigned (Str : String; Ptr : not null access Integer; Max : Integer; Res : out Uns) is Start : Positive; -- Save location of first non-blank character begin pragma Warnings (Off, """Start"" is set by ""Scan_Plus_Sign"" but not used after the call"); Scan_Plus_Sign (Str, Ptr, Max, Start); pragma Warnings (On, """Start"" is set by ""Scan_Plus_Sign"" but not used after the call"); if Str (Ptr.all) not in '0' .. '9' then Ptr.all := Start; Bad_Value (Str); end if; Scan_Raw_Unsigned (Str, Ptr, Max, Res); end Scan_Unsigned; -------------------- -- Value_Unsigned -- -------------------- function Value_Unsigned (Str : String) return Uns is begin -- We have to special case Str'Last = Positive'Last because the normal -- circuit ends up setting P to Str'Last + 1 which is out of bounds. We -- deal with this by converting to a subtype which fixes the bounds. if Str'Last = Positive'Last then declare subtype NT is String (1 .. Str'Length); procedure Prove_Is_Unsigned_Ghost with Ghost, Pre => Str'Length < Natural'Last and then not Only_Space_Ghost (Str, Str'First, Str'Last) and then Spec.Is_Unsigned_Ghost (Spec.Slide_To_1 (Str)), Post => Spec.Is_Unsigned_Ghost (NT (Str)); procedure Prove_Is_Unsigned_Ghost is null; begin Prove_Is_Unsigned_Ghost; return Value_Unsigned (NT (Str)); end; -- Normal case where Str'Last < Positive'Last else declare V : Uns; 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) = '+' then Non_Blank + 1 else Non_Blank) with Ghost; begin declare P_Acc : constant not null access Integer := P'Access; begin Scan_Unsigned (Str, P_Acc, Str'Last, V); end; pragma Assert (P = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last)); pragma Assert (V = Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last)); Scan_Trailing_Blanks (Str, P); pragma Assert (Spec.Is_Value_Unsigned_Ghost (Spec.Slide_If_Necessary (Str), V)); return V; end; end if; end Value_Unsigned; end System.Value_U;