gcc/ada/libgnat/s-arit32.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                      S Y S T E M . A R I T H _ 3 2                       --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --            Copyright (C) 2020-2024, 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 --  Preconditions, postconditions, ghost code, loop invariants and assertions
  33 --  in this unit are meant for analysis only, not for run-time checking, as it
  34 --  would be too costly otherwise. This is enforced by setting the assertion
  35 --  policy to Ignore.
  36
  37 pragma Assertion_Policy (Pre            => Ignore,
  38                          Post           => Ignore,
  39                          Ghost          => Ignore,
  40                          Loop_Invariant => Ignore,
  41                          Assert         => Ignore);
  42
  43 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
  44 use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
  45 with Ada.Unchecked_Conversion;
  46
  47 package body System.Arith_32
  48   with SPARK_Mode
  49 is
  50
  51    pragma Suppress (Overflow_Check);
  52    pragma Suppress (Range_Check);
  53
  54    subtype Uns32 is Interfaces.Unsigned_32;
  55    subtype Uns64 is Interfaces.Unsigned_64;
  56
  57    use Interfaces;
  58
  59    function To_Int is new Ada.Unchecked_Conversion (Uns32, Int32);
  60
  61    package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns32);
  62
  63    function Big (Arg : Uns32) return Big_Integer is
  64      (Unsigned_Conversion.To_Big_Integer (Arg))
  65    with Ghost;
  66
  67    package Unsigned_Conversion_64 is new Unsigned_Conversions (Int => Uns64);
  68
  69    function Big (Arg : Uns64) return Big_Integer is
  70      (Unsigned_Conversion_64.To_Big_Integer (Arg))
  71    with Ghost;
  72
  73    pragma Warnings
  74      (Off, "non-preelaborable call not allowed in preelaborated unit",
  75       Reason => "Ghost code is not compiled");
  76    Big_0 : constant Big_Integer :=
  77      Big (Uns32'(0))
  78    with Ghost;
  79    Big_2xx32 : constant Big_Integer :=
  80      Big (Uns32'(2 ** 32 - 1)) + 1
  81    with Ghost;
  82    Big_2xx64 : constant Big_Integer :=
  83      Big (Uns64'(2 ** 64 - 1)) + 1
  84    with Ghost;
  85    pragma Warnings
  86      (On, "non-preelaborable call not allowed in preelaborated unit");
  87
  88    -----------------------
  89    -- Local Subprograms --
  90    -----------------------
  91
  92    function "abs" (X : Int32) return Uns32 is
  93      (if X = Int32'First
  94       then Uns32'(2**31)
  95       else Uns32 (Int32'(abs X)));
  96    --  Convert absolute value of X to unsigned. Note that we can't just use
  97    --  the expression of the Else since it overflows for X = Int32'First.
  98
  99    function Lo (A : Uns64) return Uns32 is (Uns32 (A and (2 ** 32 - 1)));
 100    --  Low order half of 64-bit value
 101
 102    function Hi (A : Uns64) return Uns32 is (Uns32 (Shift_Right (A, 32)));
 103    --  High order half of 64-bit value
 104
 105    function To_Neg_Int (A : Uns32) return Int32
 106    with
 107      Pre  => In_Int32_Range (-Big (A)),
 108      Post => Big (To_Neg_Int'Result) = -Big (A);
 109    --  Convert to negative integer equivalent. If the input is in the range
 110    --  0 .. 2**31, then the corresponding nonpositive signed integer (obtained
 111    --  by negating the given value) is returned, otherwise constraint error is
 112    --  raised.
 113
 114    function To_Pos_Int (A : Uns32) return Int32
 115    with
 116      Pre  => In_Int32_Range (Big (A)),
 117      Post => Big (To_Pos_Int'Result) = Big (A);
 118    --  Convert to positive integer equivalent. If the input is in the range
 119    --  0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
 120    --  returned, otherwise constraint error is raised.
 121
 122    procedure Raise_Error;
 123    pragma No_Return (Raise_Error);
 124    --  Raise constraint error with appropriate message
 125
 126    ------------------
 127    -- Local Lemmas --
 128    ------------------
 129
 130    procedure Lemma_Abs_Commutation (X : Int32)
 131    with
 132      Ghost,
 133      Post => abs (Big (X)) = Big (Uns32'(abs X));
 134
 135    procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer)
 136    with
 137      Ghost,
 138      Pre  => Y /= 0,
 139      Post => abs (X / Y) = abs X / abs Y;
 140
 141    procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer)
 142    with
 143      Ghost,
 144      Post => abs (X * Y) = abs X * abs Y;
 145
 146    procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer)
 147    with
 148      Ghost,
 149      Pre  => Y /= 0,
 150      Post => abs (X rem Y) = (abs X) rem (abs Y);
 151
 152    procedure Lemma_Div_Commutation (X, Y : Uns64)
 153    with
 154      Ghost,
 155      Pre  => Y /= 0,
 156      Post => Big (X) / Big (Y) = Big (X / Y);
 157
 158    procedure Lemma_Div_Ge (X, Y, Z : Big_Integer)
 159    with
 160      Ghost,
 161      Pre  => Z > 0 and then X >= Y * Z,
 162      Post => X / Z >= Y;
 163
 164    procedure Lemma_Ge_Commutation (A, B : Uns32)
 165    with
 166      Ghost,
 167      Pre  => A >= B,
 168      Post => Big (A) >= Big (B);
 169
 170    procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32)
 171    with
 172      Ghost,
 173      Pre  => Xhi = Hi (Xu) and Xlo = Lo (Xu),
 174      Post => Big (Xu) = Big_2xx32 * Big (Xhi) + Big (Xlo);
 175
 176    procedure Lemma_Mult_Commutation (X, Y, Z : Uns64)
 177    with
 178      Ghost,
 179      Pre  => Big (X) * Big (Y) < Big_2xx64 and then Z = X * Y,
 180      Post => Big (X) * Big (Y) = Big (Z);
 181
 182    procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer)
 183    with
 184      Ghost,
 185      Pre  => (X >= Big_0 and then Y >= Big_0)
 186        or else (X <= Big_0 and then Y <= Big_0),
 187      Post => X * Y >= Big_0;
 188
 189    procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer)
 190    with
 191      Ghost,
 192      Pre  => (X <= Big_0 and then Y >= Big_0)
 193        or else (X >= Big_0 and then Y <= Big_0),
 194      Post => X * Y <= Big_0;
 195
 196    procedure Lemma_Neg_Rem (X, Y : Big_Integer)
 197    with
 198      Ghost,
 199      Pre  => Y /= 0,
 200      Post => X rem Y = X rem (-Y);
 201
 202    procedure Lemma_Not_In_Range_Big2xx32
 203    with
 204      Post => not In_Int32_Range (Big_2xx32)
 205        and then not In_Int32_Range (-Big_2xx32);
 206
 207    procedure Lemma_Rem_Commutation (X, Y : Uns64)
 208    with
 209      Ghost,
 210      Pre  => Y /= 0,
 211      Post => Big (X) rem Big (Y) = Big (X rem Y);
 212
 213    -----------------------------
 214    -- Local lemma null bodies --
 215    -----------------------------
 216
 217    procedure Lemma_Abs_Commutation (X : Int32) is null;
 218    procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is null;
 219    procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null;
 220    procedure Lemma_Div_Commutation (X, Y : Uns64) is null;
 221    procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null;
 222    procedure Lemma_Ge_Commutation (A, B : Uns32) is null;
 223    procedure Lemma_Mult_Commutation (X, Y, Z : Uns64) is null;
 224    procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) is null;
 225    procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) is null;
 226    procedure Lemma_Neg_Rem (X, Y : Big_Integer) is null;
 227    procedure Lemma_Not_In_Range_Big2xx32 is null;
 228    procedure Lemma_Rem_Commutation (X, Y : Uns64) is null;
 229
 230    -------------------------------
 231    -- Lemma_Abs_Rem_Commutation --
 232    -------------------------------
 233
 234    procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer) is
 235    begin
 236       if Y < 0 then
 237          Lemma_Neg_Rem (X, Y);
 238          if X < 0 then
 239             pragma Assert (X rem Y = -((-X) rem (-Y)));
 240             pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
 241          else
 242             pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
 243          end if;
 244       end if;
 245    end Lemma_Abs_Rem_Commutation;
 246
 247    -----------------
 248    -- Lemma_Hi_Lo --
 249    -----------------
 250
 251    procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32) is
 252    begin
 253       pragma Assert (Uns64 (Xhi) = Xu / Uns64'(2 ** 32));
 254       pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32);
 255    end Lemma_Hi_Lo;
 256
 257    -----------------
 258    -- Raise_Error --
 259    -----------------
 260
 261    procedure Raise_Error is
 262    begin
 263       raise Constraint_Error with "32-bit arithmetic overflow";
 264       pragma Annotate
 265         (GNATprove, Intentional, "exception might be raised",
 266          "Procedure Raise_Error is called to signal input errors");
 267    end Raise_Error;
 268
 269    -------------------
 270    -- Scaled_Divide --
 271    -------------------
 272
 273    procedure Scaled_Divide32
 274      (X, Y, Z : Int32;
 275       Q, R    : out Int32;
 276       Round   : Boolean)
 277    is
 278       Xu  : constant Uns32 := abs X;
 279       Yu  : constant Uns32 := abs Y;
 280       Zu  : constant Uns32 := abs Z;
 281
 282       D   : Uns64;
 283       --  The dividend
 284
 285       Qu : Uns32;
 286       Ru : Uns32;
 287       --  Unsigned quotient and remainder
 288
 289       --  Local ghost variables
 290
 291       Mult  : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost;
 292       Quot  : Big_Integer with Ghost;
 293       Big_R : Big_Integer with Ghost;
 294       Big_Q : Big_Integer with Ghost;
 295
 296       --  Local lemmas
 297
 298       procedure Prove_Negative_Dividend
 299       with
 300         Ghost,
 301         Pre  => Z /= 0
 302           and then ((X >= 0 and Y < 0) or (X < 0 and Y >= 0))
 303           and then Big_Q =
 304             (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
 305                                            Big (X) * Big (Y) / Big (Z),
 306                                            Big (X) * Big (Y) rem Big (Z))
 307              else Big (X) * Big (Y) / Big (Z)),
 308          Post =>
 309            (if Z > 0 then Big_Q <= Big_0 else Big_Q >= Big_0);
 310       --  Proves the sign of rounded quotient when dividend is non-positive
 311
 312       procedure Prove_Overflow
 313       with
 314         Ghost,
 315         Pre  => Z /= 0 and then Mult >= Big_2xx32 * Big (Uns32'(abs Z)),
 316         Post => not In_Int32_Range (Big (X) * Big (Y) / Big (Z))
 317           and then not In_Int32_Range
 318             (Round_Quotient (Big (X) * Big (Y), Big (Z),
 319                              Big (X) * Big (Y) / Big (Z),
 320                              Big (X) * Big (Y) rem Big (Z)));
 321       --  Proves overflow case
 322
 323       procedure Prove_Positive_Dividend
 324       with
 325         Ghost,
 326         Pre  => Z /= 0
 327           and then ((X >= 0 and Y >= 0) or (X < 0 and Y < 0))
 328           and then Big_Q =
 329             (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
 330                                            Big (X) * Big (Y) / Big (Z),
 331                                            Big (X) * Big (Y) rem Big (Z))
 332              else Big (X) * Big (Y) / Big (Z)),
 333          Post =>
 334            (if Z > 0 then Big_Q >= Big_0 else Big_Q <= Big_0);
 335       --  Proves the sign of rounded quotient when dividend is non-negative
 336
 337       procedure Prove_Rounding_Case
 338       with
 339         Ghost,
 340         Pre  => Z /= 0
 341           and then Quot = Big (X) * Big (Y) / Big (Z)
 342           and then Big_R = Big (X) * Big (Y) rem Big (Z)
 343           and then Big_Q =
 344             Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
 345           and then Big (Ru) = abs Big_R
 346           and then Big (Zu) = Big (Uns32'(abs Z)),
 347         Post => abs Big_Q =
 348           (if Ru > (Zu - Uns32'(1)) / Uns32'(2)
 349            then abs Quot + 1
 350            else abs Quot);
 351       --  Proves correctness of the rounding of the unsigned quotient
 352
 353       procedure Prove_Sign_R
 354       with
 355         Ghost,
 356         Pre  => Z /= 0 and then Big_R = Big (X) * Big (Y) rem Big (Z),
 357         Post => In_Int32_Range (Big_R);
 358
 359       procedure Prove_Signs
 360       with
 361         Ghost,
 362         Pre  => Z /= 0
 363           and then Quot = Big (X) * Big (Y) / Big (Z)
 364           and then Big_R = Big (X) * Big (Y) rem Big (Z)
 365           and then Big_Q =
 366             (if Round then
 367                Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
 368              else Quot)
 369           and then Big (Ru) = abs Big_R
 370           and then Big (Qu) = abs Big_Q
 371           and then In_Int32_Range (Big_Q)
 372           and then In_Int32_Range (Big_R)
 373           and then R =
 374             (if (X >= 0) = (Y >= 0) then To_Pos_Int (Ru) else To_Neg_Int (Ru))
 375           and then Q =
 376             (if ((X >= 0) = (Y >= 0)) = (Z >= 0) then To_Pos_Int (Qu)
 377              else To_Neg_Int (Qu)),  --  need to ensure To_Pos_Int precondition
 378         Post => Big (R) = Big_R and then Big (Q) = Big_Q;
 379       --  Proves final signs match the intended result after the unsigned
 380       --  division is done.
 381
 382       -----------------------------
 383       -- Prove_Negative_Dividend --
 384       -----------------------------
 385
 386       procedure Prove_Negative_Dividend is
 387       begin
 388          Lemma_Mult_Non_Positive (Big (X), Big (Y));
 389       end Prove_Negative_Dividend;
 390
 391       --------------------
 392       -- Prove_Overflow --
 393       --------------------
 394
 395       procedure Prove_Overflow is
 396       begin
 397          Lemma_Div_Ge (Mult, Big_2xx32, Big (Uns32'(abs Z)));
 398          Lemma_Abs_Commutation (Z);
 399          Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
 400       end Prove_Overflow;
 401
 402       -----------------------------
 403       -- Prove_Positive_Dividend --
 404       -----------------------------
 405
 406       procedure Prove_Positive_Dividend is
 407       begin
 408          Lemma_Mult_Non_Negative (Big (X), Big (Y));
 409       end Prove_Positive_Dividend;
 410
 411       -------------------------
 412       -- Prove_Rounding_Case --
 413       -------------------------
 414
 415       procedure Prove_Rounding_Case is
 416       begin
 417          if Same_Sign (Big (X) * Big (Y), Big (Z)) then
 418             pragma Assert
 419               (abs Big_Q =
 420                  (if Ru > (Zu - Uns32'(1)) / Uns32'(2)
 421                   then abs Quot + 1
 422                   else abs Quot));
 423          end if;
 424       end Prove_Rounding_Case;
 425
 426       ------------------
 427       -- Prove_Sign_R --
 428       ------------------
 429
 430       procedure Prove_Sign_R is
 431       begin
 432          pragma Assert (In_Int32_Range (Big (Z)));
 433       end Prove_Sign_R;
 434
 435       -----------------
 436       -- Prove_Signs --
 437       -----------------
 438
 439       procedure Prove_Signs is
 440       begin
 441          if (X >= 0) = (Y >= 0) then
 442             pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q);
 443          else
 444             pragma Assert (Big (R) = Big_R and then Big (Q) = Big_Q);
 445          end if;
 446       end Prove_Signs;
 447
 448    --  Start of processing for Scaled_Divide32
 449
 450    begin
 451       --  First do the 64-bit multiplication
 452
 453       D := Uns64 (Xu) * Uns64 (Yu);
 454
 455       Lemma_Abs_Mult_Commutation (Big (X), Big (Y));
 456       pragma Assert (Mult = Big (D));
 457       Lemma_Hi_Lo (D, Hi (D), Lo (D));
 458       pragma Assert (Mult = Big_2xx32 * Big (Hi (D)) + Big (Lo (D)));
 459
 460       --  If divisor is zero, raise error
 461
 462       if Z = 0 then
 463          Raise_Error;
 464       end if;
 465
 466       Quot := Big (X) * Big (Y) / Big (Z);
 467       Big_R := Big (X) * Big (Y) rem Big (Z);
 468       if Round then
 469          Big_Q := Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R);
 470       else
 471          Big_Q := Quot;
 472       end if;
 473
 474       --  If dividend is too large, raise error
 475
 476       if Hi (D) >= Zu then
 477          Lemma_Ge_Commutation (Hi (D), Zu);
 478          pragma Assert (Mult >= Big_2xx32 * Big (Zu));
 479          Prove_Overflow;
 480          Raise_Error;
 481       end if;
 482
 483       --  Then do the 64-bit division
 484
 485       Qu := Uns32 (D / Uns64 (Zu));
 486       Ru := Uns32 (D rem Uns64 (Zu));
 487
 488       Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
 489       Lemma_Abs_Rem_Commutation (Big (X) * Big (Y), Big (Z));
 490       Lemma_Abs_Commutation (X);
 491       Lemma_Abs_Commutation (Y);
 492       Lemma_Abs_Commutation (Z);
 493       Lemma_Mult_Commutation (Uns64 (Xu), Uns64 (Yu), D);
 494       Lemma_Div_Commutation (D, Uns64 (Zu));
 495       Lemma_Rem_Commutation (D, Uns64 (Zu));
 496
 497       pragma Assert (Uns64 (Qu) = D / Uns64 (Zu));
 498       pragma Assert (Uns64 (Ru) = D rem Uns64 (Zu));
 499       pragma Assert (Big (Ru) = abs Big_R);
 500       pragma Assert (Big (Qu) = abs Quot);
 501       pragma Assert (Big (Zu) = Big (Uns32'(abs Z)));
 502
 503       --  Deal with rounding case
 504
 505       if Round then
 506          Prove_Rounding_Case;
 507
 508          if Ru > (Zu - Uns32'(1)) / Uns32'(2) then
 509             pragma Assert (abs Big_Q = Big (Qu) + 1);
 510
 511             --  Protect against wrapping around when rounding, by signaling
 512             --  an overflow when the quotient is too large.
 513
 514             if Qu = Uns32'Last then
 515                pragma Assert (abs Big_Q = Big_2xx32);
 516                Lemma_Not_In_Range_Big2xx32;
 517                Raise_Error;
 518             end if;
 519
 520             Qu := Qu + Uns32'(1);
 521          end if;
 522       end if;
 523
 524       pragma Assert (In_Int32_Range (Big_Q));
 525       pragma Assert (Big (Qu) = abs Big_Q);
 526       pragma Assert (Big (Ru) = abs Big_R);
 527       Prove_Sign_R;
 528
 529       --  Set final signs (RM 4.5.5(27-30))
 530
 531       --  Case of dividend (X * Y) sign positive
 532
 533       if (X >= 0 and then Y >= 0) or else (X < 0 and then Y < 0) then
 534          Prove_Positive_Dividend;
 535
 536          R := To_Pos_Int (Ru);
 537          Q := (if Z > 0 then To_Pos_Int (Qu) else To_Neg_Int (Qu));
 538
 539       --  Case of dividend (X * Y) sign negative
 540
 541       else
 542          Prove_Negative_Dividend;
 543
 544          R := To_Neg_Int (Ru);
 545          Q := (if Z > 0 then To_Neg_Int (Qu) else To_Pos_Int (Qu));
 546       end if;
 547
 548       Prove_Signs;
 549    end Scaled_Divide32;
 550
 551    ----------------
 552    -- To_Neg_Int --
 553    ----------------
 554
 555    function To_Neg_Int (A : Uns32) return Int32 is
 556       R : constant Int32 :=
 557         (if A = 2**31 then Int32'First else -To_Int (A));
 558       --  Note that we can't just use the expression of the Else, because it
 559       --  overflows for A = 2**31.
 560    begin
 561       if R <= 0 then
 562          return R;
 563       else
 564          Raise_Error;
 565       end if;
 566    end To_Neg_Int;
 567
 568    ----------------
 569    -- To_Pos_Int --
 570    ----------------
 571
 572    function To_Pos_Int (A : Uns32) return Int32 is
 573       R : constant Int32 := To_Int (A);
 574    begin
 575       if R >= 0 then
 576          return R;
 577       else
 578          Raise_Error;
 579       end if;
 580    end To_Pos_Int;
 581
 582 end System.Arith_32;