gcc/ada/libgnat/s-imagei.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                       S Y S T E M . I M A G E _ I                        --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
  33 use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
  34
  35 with System.Val_Spec;
  36
  37 package body System.Image_I is
  38
  39    --  Ghost code, loop invariants and assertions in this unit are meant for
  40    --  analysis only, not for run-time checking, as it would be too costly
  41    --  otherwise. This is enforced by setting the assertion policy to Ignore.
  42
  43    pragma Assertion_Policy (Ghost              => Ignore,
  44                             Loop_Invariant     => Ignore,
  45                             Assert             => Ignore,
  46                             Assert_And_Cut     => Ignore,
  47                             Pre                => Ignore,
  48                             Post               => Ignore,
  49                             Subprogram_Variant => Ignore);
  50
  51    subtype Non_Positive is Int range Int'First .. 0;
  52
  53    function Uns_Of_Non_Positive (T : Non_Positive) return Uns is
  54      (if T = Int'First then Uns (Int'Last) + 1 else Uns (-T));
  55
  56    procedure Set_Digits
  57      (T : Non_Positive;
  58       S : in out String;
  59       P : in out Natural)
  60    with
  61      Pre  => P < Integer'Last
  62        and then S'Last < Integer'Last
  63        and then S'First <= P + 1
  64        and then S'First <= S'Last
  65        and then P <= S'Last - Unsigned_Width_Ghost + 1,
  66      Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
  67        and then P in P'Old + 1 .. S'Last
  68        and then UP.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
  69        and then UP.Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
  70          = UP.Wrap_Option (Uns_Of_Non_Positive (T));
  71    --  Set digits of absolute value of T, which is zero or negative. We work
  72    --  with the negative of the value so that the largest negative number is
  73    --  not a special case.
  74
  75    package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
  76
  77    function Big (Arg : Uns) return Big_Integer renames
  78      Unsigned_Conversion.To_Big_Integer;
  79
  80    function From_Big (Arg : Big_Integer) return Uns renames
  81      Unsigned_Conversion.From_Big_Integer;
  82
  83    Big_10 : constant Big_Integer := Big (10) with Ghost;
  84
  85    ------------------
  86    -- Local Lemmas --
  87    ------------------
  88
  89    procedure Lemma_Non_Zero (X : Uns)
  90    with
  91      Ghost,
  92      Pre  => X /= 0,
  93      Post => Big (X) /= 0;
  94
  95    procedure Lemma_Div_Commutation (X, Y : Uns)
  96    with
  97      Ghost,
  98      Pre  => Y /= 0,
  99      Post => Big (X) / Big (Y) = Big (X / Y);
 100
 101    procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive)
 102    with
 103      Ghost,
 104      Post => X / Y / Z = X / (Y * Z);
 105
 106    ---------------------------
 107    -- Lemma_Div_Commutation --
 108    ---------------------------
 109
 110    procedure Lemma_Non_Zero (X : Uns) is null;
 111    procedure Lemma_Div_Commutation (X, Y : Uns) is null;
 112
 113    ---------------------
 114    -- Lemma_Div_Twice --
 115    ---------------------
 116
 117    procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is
 118       XY  : constant Big_Natural := X / Y;
 119       YZ  : constant Big_Natural := Y * Z;
 120       XYZ : constant Big_Natural := X / Y / Z;
 121       R   : constant Big_Natural := (XY rem Z) * Y + (X rem Y);
 122    begin
 123       pragma Assert (X = XY * Y + (X rem Y));
 124       pragma Assert (XY = XY / Z * Z + (XY rem Z));
 125       pragma Assert (X = XYZ * YZ + R);
 126       pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y);
 127       pragma Assert (R <= YZ - 1);
 128       pragma Assert (X / YZ = (XYZ * YZ + R) / YZ);
 129       pragma Assert (X / YZ = XYZ + R / YZ);
 130    end Lemma_Div_Twice;
 131
 132    -------------------
 133    -- Image_Integer --
 134    -------------------
 135
 136    procedure Image_Integer
 137      (V : Int;
 138       S : in out String;
 139       P : out Natural)
 140    is
 141       pragma Assert (S'First = 1);
 142
 143       procedure Prove_Value_Integer
 144       with
 145         Ghost,
 146         Pre => S'First = 1
 147           and then S'Last < Integer'Last
 148           and then P in 2 .. S'Last
 149           and then S (1) in ' ' | '-'
 150           and then (S (1) = '-') = (V < 0)
 151           and then UP.Only_Decimal_Ghost (S, From => 2, To => P)
 152           and then UP.Scan_Based_Number_Ghost (S, From => 2, To => P)
 153             = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)),
 154         Post => not System.Val_Spec.Only_Space_Ghost (S, 1, P)
 155           and then IP.Is_Integer_Ghost (S (1 .. P))
 156           and then IP.Is_Value_Integer_Ghost (S (1 .. P), V);
 157       --  Ghost lemma to prove the value of Value_Integer from the value of
 158       --  Scan_Based_Number_Ghost and the sign on a decimal string.
 159
 160       -------------------------
 161       -- Prove_Value_Integer --
 162       -------------------------
 163
 164       procedure Prove_Value_Integer is
 165          Str : constant String := S (1 .. P);
 166       begin
 167          pragma Assert (Str'First = 1);
 168          pragma Assert (Str (2) /= ' ');
 169          pragma Assert
 170            (UP.Only_Decimal_Ghost (Str, From => 2, To => P));
 171          UP.Prove_Scan_Based_Number_Ghost_Eq (S, Str, From => 2, To => P);
 172          pragma Assert
 173            (UP.Scan_Based_Number_Ghost (Str, From => 2, To => P)
 174             = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)));
 175          IP.Prove_Scan_Only_Decimal_Ghost (Str, V);
 176       end Prove_Value_Integer;
 177
 178    --  Start of processing for Image_Integer
 179
 180    begin
 181       if V >= 0 then
 182          pragma Annotate (CodePeer, False_Positive, "test always false",
 183                           "V can be positive");
 184          S (1) := ' ';
 185          P := 1;
 186          pragma Assert (P < S'Last);
 187
 188       else
 189          P := 0;
 190          pragma Assert (P < S'Last - 1);
 191       end if;
 192
 193       declare
 194          P_Prev : constant Integer := P with Ghost;
 195          Offset : constant Positive := (if V >= 0 then 1 else 2) with Ghost;
 196       begin
 197          Set_Image_Integer (V, S, P);
 198
 199          pragma Assert (P_Prev + Offset = 2);
 200       end;
 201       pragma Assert (if V >= 0 then S (1) = ' ');
 202       pragma Assert (S (1) in ' ' | '-');
 203
 204       Prove_Value_Integer;
 205    end Image_Integer;
 206
 207    ----------------
 208    -- Set_Digits --
 209    ----------------
 210
 211    procedure Set_Digits
 212      (T : Non_Positive;
 213       S : in out String;
 214       P : in out Natural)
 215    is
 216       Nb_Digits : Natural := 0;
 217       Value     : Non_Positive := T;
 218
 219       --  Local ghost variables
 220
 221       Pow        : Big_Positive := 1 with Ghost;
 222       S_Init     : constant String := S with Ghost;
 223       Uns_T      : constant Uns := Uns_Of_Non_Positive (T) with Ghost;
 224       Uns_Value  : Uns := Uns_Of_Non_Positive (Value) with Ghost;
 225       Prev_Value : Uns with Ghost;
 226       Prev_S     : String := S with Ghost;
 227
 228       --  Local ghost lemmas
 229
 230       procedure Prove_Character_Val (RU : Uns; RI : Non_Positive)
 231       with
 232         Ghost,
 233         Post => RU rem 10 in 0 .. 9
 234           and then -(RI rem 10) in 0 .. 9
 235           and then Character'Val (48 + RU rem 10) in '0' .. '9'
 236           and then Character'Val (48 - RI rem 10) in '0' .. '9';
 237       --  Ghost lemma to prove the value of a character corresponding to the
 238       --  next figure.
 239
 240       procedure Prove_Euclidian (Val, Quot, Rest : Uns)
 241       with
 242         Ghost,
 243         Pre  => Quot = Val / 10
 244           and then Rest = Val rem 10,
 245         Post => Uns'Last - Rest >= 10 * Quot and then Val = 10 * Quot + Rest;
 246       --  Ghost lemma to prove the relation between the quotient/remainder of
 247       --  division by 10 and the initial value.
 248
 249       procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int)
 250       with
 251         Ghost,
 252         Pre  => RU in 0 .. 9
 253           and then RI in 0 .. 9,
 254         Post => UP.Hexa_To_Unsigned_Ghost
 255             (Character'Val (48 + RU)) = RU
 256           and then UP.Hexa_To_Unsigned_Ghost
 257             (Character'Val (48 + RI)) = Uns (RI);
 258       --  Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source
 259       --  figure when applied to the corresponding character.
 260
 261       procedure Prove_Scan_Iter
 262         (S, Prev_S      : String;
 263          V, Prev_V, Res : Uns;
 264          P, Max         : Natural)
 265         with
 266           Ghost,
 267           Pre =>
 268             S'First = Prev_S'First and then S'Last = Prev_S'Last
 269             and then S'Last < Natural'Last and then
 270             Max in S'Range and then P in S'First .. Max and then
 271             (for all I in P + 1 .. Max => Prev_S (I) in '0' .. '9')
 272             and then (for all I in P + 1 .. Max => Prev_S (I) = S (I))
 273             and then S (P) in '0' .. '9'
 274             and then V <= Uns'Last / 10
 275             and then Uns'Last - UP.Hexa_To_Unsigned_Ghost (S (P))
 276               >= 10 * V
 277             and then Prev_V =
 278               V * 10 + UP.Hexa_To_Unsigned_Ghost (S (P))
 279             and then
 280               (if P = Max then Prev_V = Res
 281                else UP.Scan_Based_Number_Ghost
 282                  (Str  => Prev_S,
 283                   From => P + 1,
 284                   To   => Max,
 285                   Base => 10,
 286                   Acc  => Prev_V) = UP.Wrap_Option (Res)),
 287           Post =>
 288             (for all I in P .. Max => S (I) in '0' .. '9')
 289             and then UP.Scan_Based_Number_Ghost
 290               (Str  => S,
 291                From => P,
 292                To   => Max,
 293                Base => 10,
 294                Acc  => V) = UP.Wrap_Option (Res);
 295       --  Ghost lemma to prove that Scan_Based_Number_Ghost is preserved
 296       --  through an iteration of the loop.
 297
 298       procedure Prove_Uns_Of_Non_Positive_Value
 299       with
 300         Ghost,
 301         Pre  => Uns_Value = Uns_Of_Non_Positive (Value),
 302         Post => Uns_Value / 10 = Uns_Of_Non_Positive (Value / 10)
 303           and then Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10);
 304       --  Ghost lemma to prove that the relation between Value and its unsigned
 305       --  version is preserved.
 306
 307       -----------------------------
 308       -- Local lemma null bodies --
 309       -----------------------------
 310
 311       procedure Prove_Character_Val (RU : Uns; RI : Non_Positive) is null;
 312       procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null;
 313       procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) is null;
 314       procedure Prove_Uns_Of_Non_Positive_Value is null;
 315
 316       ---------------------
 317       -- Prove_Scan_Iter --
 318       ---------------------
 319
 320       procedure Prove_Scan_Iter
 321         (S, Prev_S      : String;
 322          V, Prev_V, Res : Uns;
 323          P, Max         : Natural)
 324       is
 325          pragma Unreferenced (Res);
 326       begin
 327          UP.Lemma_Scan_Based_Number_Ghost_Step
 328            (Str  => S,
 329             From => P,
 330             To   => Max,
 331             Base => 10,
 332             Acc  => V);
 333          if P < Max then
 334             UP.Prove_Scan_Based_Number_Ghost_Eq
 335               (Prev_S, S, P + 1, Max, 10, Prev_V);
 336          else
 337             UP.Lemma_Scan_Based_Number_Ghost_Base
 338               (Str  => S,
 339                From => P + 1,
 340                To   => Max,
 341                Base => 10,
 342                Acc  => Prev_V);
 343          end if;
 344       end Prove_Scan_Iter;
 345
 346    --  Start of processing for Set_Digits
 347
 348    begin
 349       pragma Assert (P >= S'First - 1 and P < S'Last);
 350       --  No check is done since, as documented in the Set_Image_Integer
 351       --  specification, the caller guarantees that S is long enough to
 352       --  hold the result.
 353
 354       --  First we compute the number of characters needed for representing
 355       --  the number.
 356       loop
 357          Lemma_Div_Commutation (Uns_Of_Non_Positive (Value), 10);
 358          Lemma_Div_Twice (Big (Uns_Of_Non_Positive (T)),
 359                           Big_10 ** Nb_Digits, Big_10);
 360          Prove_Uns_Of_Non_Positive_Value;
 361
 362          Value := Value / 10;
 363          Nb_Digits := Nb_Digits + 1;
 364
 365          Uns_Value := Uns_Value / 10;
 366          Pow := Pow * 10;
 367
 368          pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value));
 369          pragma Loop_Invariant (Nb_Digits in 1 .. Unsigned_Width_Ghost - 1);
 370          pragma Loop_Invariant (Pow = Big_10 ** Nb_Digits);
 371          pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow);
 372          pragma Loop_Variant (Increases => Value);
 373
 374          exit when Value = 0;
 375
 376          Lemma_Non_Zero (Uns_Value);
 377          pragma Assert (Pow <= Big (Uns'Last));
 378       end loop;
 379
 380       Value := T;
 381       Uns_Value := Uns_Of_Non_Positive (T);
 382       Pow := 1;
 383
 384       pragma Assert (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** 0));
 385
 386       --  We now populate digits from the end of the string to the beginning
 387       for J in reverse  1 .. Nb_Digits loop
 388          Lemma_Div_Commutation (Uns_Value, 10);
 389          Lemma_Div_Twice (Big (Uns_T), Big_10 ** (Nb_Digits - J), Big_10);
 390          Prove_Character_Val (Uns_Value, Value);
 391          Prove_Hexa_To_Unsigned_Ghost (Uns_Value rem 10, -(Value rem 10));
 392          Prove_Uns_Of_Non_Positive_Value;
 393
 394          Prev_Value := Uns_Value;
 395          Prev_S := S;
 396          Pow := Pow * 10;
 397          Uns_Value := Uns_Value / 10;
 398
 399          S (P + J) := Character'Val (48 - (Value rem 10));
 400          Value := Value / 10;
 401
 402          Prove_Euclidian
 403            (Val  => Prev_Value,
 404             Quot => Uns_Value,
 405             Rest => UP.Hexa_To_Unsigned_Ghost (S (P + J)));
 406
 407          Prove_Scan_Iter
 408            (S, Prev_S, Uns_Value, Prev_Value, Uns_T, P + J, P + Nb_Digits);
 409
 410          pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value));
 411          pragma Loop_Invariant (Uns_Value <= Uns'Last / 10);
 412          pragma Loop_Invariant
 413            (for all K in S'First .. P => S (K) = S_Init (K));
 414          pragma Loop_Invariant
 415            (UP.Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
 416          pragma Loop_Invariant
 417            (for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9');
 418          pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1));
 419          pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow);
 420          pragma Loop_Invariant
 421            (UP.Scan_Based_Number_Ghost
 422               (Str  => S,
 423                From => P + J,
 424                To   => P + Nb_Digits,
 425                Base => 10,
 426                Acc  => Uns_Value)
 427               = UP.Wrap_Option (Uns_T));
 428       end loop;
 429
 430       pragma Assert (Big (Uns_Value) = Big (Uns_T) / Big_10 ** (Nb_Digits));
 431       pragma Assert (Uns_Value = 0);
 432       pragma Assert
 433         (UP.Scan_Based_Number_Ghost
 434            (Str  => S,
 435             From => P + 1,
 436             To   => P + Nb_Digits,
 437             Base => 10,
 438             Acc  => Uns_Value)
 439          = UP.Wrap_Option (Uns_T));
 440
 441       P := P + Nb_Digits;
 442    end Set_Digits;
 443
 444    -----------------------
 445    -- Set_Image_Integer --
 446    -----------------------
 447
 448    procedure Set_Image_Integer
 449      (V : Int;
 450       S : in out String;
 451       P : in out Natural)
 452    is
 453    begin
 454       if V >= 0 then
 455          Set_Digits (-V, S, P);
 456
 457       else
 458          pragma Assert (P >= S'First - 1 and P < S'Last);
 459          --  No check is done since, as documented in the specification,
 460          --  the caller guarantees that S is long enough to hold the result.
 461          P := P + 1;
 462          S (P) := '-';
 463          Set_Digits (V, S, P);
 464       end if;
 465    end Set_Image_Integer;
 466
 467 end System.Image_I;