------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--                       S Y S T E M . V A L U E _ U                        --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
--          Copyright (C) 1992-2024, 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.      --
--                                                                          --
------------------------------------------------------------------------------

with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations;
with System.Val_Util;             use System.Val_Util;

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 :=
        Spec.Raw_Unsigned_Starts_As_Based_Ghost (Str, Last_Num_Init, Max)
      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 :=
        Spec.Raw_Unsigned_Is_Based_Ghost
          (Str, Last_Num_Init, Last_Num_Based, Max)
      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');
      pragma Assert (Str (P) in '0' .. '9');
      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
               pragma Assert
                 (By
                    (Str (P) in '0' .. '9',
                     By
                       (Character'Pos (Str (P)) >= Character'Pos ('0'),
                        Uns '(Character'Pos (Str (P))) >=
                            Character'Pos ('0'))));
               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
                  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
        (By
           (P = Last_Num_Init + 1,
            P > Max or else Str (P) not in '_' | '0' .. '9')
         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
                  pragma Assert
                    (By
                       (Spec.Only_Hexa_Ghost (Str, P, Last_Num_Based),
                        P > Last_Num_Init + 1
                        and Spec.Only_Hexa_Ghost
                          (Str, Last_Num_Init + 2, Last_Num_Based)));
                  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 By
                       (P = Last_Num_Based + 1,
                        P <= Last_Num_Based + 1
                        and Str (P) not in
                        '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_'));
                  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
                    (By
                       (Is_Based,
                        So
                          (Starts_As_Based,
                           So
                             (Last_Num_Based < Max,
                              Str (Last_Num_Based + 1) = Base_Char
                              and Base_Char = Str (Last_Num_Init + 1)))));
                  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) not in '_' | Base_Char);
               end if;

               Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max);
               pragma Assert (Str (P) not in '_' | 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
           (By
              (Overflow /= Spec.Scan_Split_No_Overflow_Ghost
                   (Str, Ptr_Old, Max),
               So
                 (Last_Num_Init < Max - 1
                  and then Str (Last_Num_Init + 1) in '#' | ':',
                  Overflow =
                    (Init_Val.Overflow
                     or else Init_Val.Value not in 2 .. 16
                     or else (Starts_As_Based and Based_Val.Overflow)))));
      end if;

      pragma Assert_And_Cut
        (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)
         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))
         and then
           (if not Overflow then
                (if Is_Based then Uval = Based_Val.Value
                 else Uval = Init_Val.Value)));

      --  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
        (By
           (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max),
            Ptr.all =
              (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
               then First_Exp
               elsif Str (First_Exp + 1) in '-' | '+' then
                 Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1
               else Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1)));
      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;