gcc/ada/libgnat/s-expont.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                        S Y S T E M . E X P O N T                         --
   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 package body System.Expont
  33   with SPARK_Mode
  34 is
  35
  36    --  Preconditions, postconditions, ghost code, loop invariants and
  37    --  assertions in this unit are meant for analysis only, not for run-time
  38    --  checking, as it would be too costly otherwise. This is enforced by
  39    --  setting the assertion policy to Ignore.
  40
  41    pragma Assertion_Policy (Pre            => Ignore,
  42                             Post           => Ignore,
  43                             Ghost          => Ignore,
  44                             Loop_Invariant => Ignore,
  45                             Assert         => Ignore);
  46
  47    --  Local lemmas
  48
  49    procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural)
  50    with
  51      Ghost,
  52      Pre  => A /= 0,
  53      Post =>
  54        (if Exp rem 2 = 0 then
  55           A ** Exp = A ** (Exp / 2) * A ** (Exp / 2)
  56         else
  57           A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
  58
  59    procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive)
  60    with
  61      Ghost,
  62      Pre  => In_Int_Range (A ** Exp * A ** Exp),
  63      Post => In_Int_Range (A * A);
  64
  65    procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural)
  66    with
  67      Ghost,
  68      Pre  => A /= 0,
  69      Post => A ** Exp /= 0;
  70
  71    procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural)
  72    with
  73      Ghost,
  74      Pre  => A /= 0
  75        and then Exp rem 2 = 0,
  76      Post => A ** Exp > 0;
  77
  78    procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer)
  79    with
  80      Ghost,
  81      Pre  => Y /= 0
  82        and then not (X = -Big (Int'First) and Y = -1)
  83        and then X * Y = Z
  84        and then In_Int_Range (Z),
  85      Post => In_Int_Range (X);
  86
  87    -----------------------------
  88    -- Local lemma null bodies --
  89    -----------------------------
  90
  91    procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural) is null;
  92    procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer) is null;
  93
  94    -----------
  95    -- Expon --
  96    -----------
  97
  98    function Expon (Left : Int; Right : Natural) return Int is
  99
 100       --  Note that negative exponents get a constraint error because the
 101       --  subtype of the Right argument (the exponent) is Natural.
 102
 103       Result : Int     := 1;
 104       Factor : Int     := Left;
 105       Exp    : Natural := Right;
 106
 107       Rest : Big_Integer with Ghost;
 108       --  Ghost variable to hold Factor**Exp between Exp and Factor updates
 109
 110    begin
 111       pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
 112                        "early returns for performance");
 113
 114       --  We use the standard logarithmic approach, Exp gets shifted right
 115       --  testing successive low order bits and Factor is the value of the
 116       --  base raised to the next power of 2.
 117
 118       --  Note: for compilation only, it is not worth special casing base
 119       --  values -1, 0, +1 since the expander does this when the base is a
 120       --  literal, and other cases will be extremely rare. But for proof,
 121       --  special casing zero in both positions makes ghost code and lemmas
 122       --  simpler, so we do it.
 123
 124       if Right = 0 then
 125          return 1;
 126       elsif Left = 0 then
 127          return 0;
 128       end if;
 129
 130       loop
 131          pragma Loop_Invariant (Exp > 0);
 132          pragma Loop_Invariant (Factor /= 0);
 133          pragma Loop_Invariant
 134            (Big (Result) * Big (Factor) ** Exp = Big (Left) ** Right);
 135          pragma Loop_Variant (Decreases => Exp);
 136
 137          if Exp rem 2 /= 0 then
 138             declare
 139                pragma Unsuppress (Overflow_Check);
 140             begin
 141                pragma Assert
 142                  (Big (Factor) ** Exp
 143                   = Big (Factor) * Big (Factor) ** (Exp - 1));
 144                Lemma_Exp_Positive (Big (Factor), Exp - 1);
 145                Lemma_Mult_In_Range (Big (Result) * Big (Factor),
 146                                     Big (Factor) ** (Exp - 1),
 147                                     Big (Left) ** Right);
 148
 149                Result := Result * Factor;
 150             end;
 151          end if;
 152
 153          Lemma_Exp_Expand (Big (Factor), Exp);
 154
 155          Exp := Exp / 2;
 156          exit when Exp = 0;
 157
 158          Rest := Big (Factor) ** Exp;
 159          pragma Assert
 160            (Big (Result) * (Rest * Rest) = Big (Left) ** Right);
 161
 162          declare
 163             pragma Unsuppress (Overflow_Check);
 164          begin
 165             Lemma_Mult_In_Range (Rest * Rest,
 166                                  Big (Result),
 167                                  Big (Left) ** Right);
 168             Lemma_Exp_In_Range (Big (Factor), Exp);
 169
 170             Factor := Factor * Factor;
 171          end;
 172
 173          pragma Assert (Big (Factor) ** Exp = Rest * Rest);
 174       end loop;
 175
 176       pragma Assert (Big (Result) = Big (Left) ** Right);
 177
 178       return Result;
 179
 180       pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
 181    end Expon;
 182
 183    ----------------------
 184    -- Lemma_Exp_Expand --
 185    ----------------------
 186
 187    procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
 188    begin
 189       if Exp rem 2 = 0 then
 190          pragma Assert (Exp = Exp / 2 + Exp / 2);
 191       else
 192          pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
 193          pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
 194          pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
 195          pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
 196       end if;
 197    end Lemma_Exp_Expand;
 198
 199    ------------------------
 200    -- Lemma_Exp_In_Range --
 201    ------------------------
 202
 203    procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive) is
 204    begin
 205       if A /= 0 and Exp /= 1 then
 206          pragma Assert (A ** Exp = A * A ** (Exp - 1));
 207          Lemma_Mult_In_Range
 208            (A * A, A ** (Exp - 1) * A ** (Exp - 1), A ** Exp * A ** Exp);
 209       end if;
 210    end Lemma_Exp_In_Range;
 211
 212    ------------------------
 213    -- Lemma_Exp_Positive --
 214    ------------------------
 215
 216    procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural) is
 217    begin
 218       if Exp = 0 then
 219          pragma Assert (A ** Exp = 1);
 220       else
 221          pragma Assert (Exp = 2 * (Exp / 2));
 222          pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2));
 223          pragma Assert (A ** Exp = (A ** (Exp / 2)) ** 2);
 224          Lemma_Exp_Not_Zero (A, Exp / 2);
 225       end if;
 226    end Lemma_Exp_Positive;
 227
 228 end System.Expont;