gcc/ada/libgnat/s-widthu.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                       S Y S T E M . W I D T H _ U                        --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-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 package body System.Width_U is
  33
  34    --  Ghost code, loop invariants and assertions in this unit are meant for
  35    --  analysis only, not for run-time checking, as it would be too costly
  36    --  otherwise. This is enforced by setting the assertion policy to Ignore.
  37
  38    pragma Assertion_Policy (Ghost              => Ignore,
  39                             Loop_Invariant     => Ignore,
  40                             Assert             => Ignore,
  41                             Assert_And_Cut     => Ignore,
  42                             Subprogram_Variant => Ignore);
  43
  44    function Width (Lo, Hi : Uns) return Natural is
  45
  46       --  Ghost code, loop invariants and assertions in this unit are meant for
  47       --  analysis only, not for run-time checking, as it would be too costly
  48       --  otherwise. This is enforced by setting the assertion policy to
  49       --  Ignore.
  50
  51       pragma Assertion_Policy (Ghost          => Ignore,
  52                                Loop_Invariant => Ignore,
  53                                Assert         => Ignore);
  54
  55       ------------------
  56       -- Local Lemmas --
  57       ------------------
  58
  59       procedure Lemma_Lower_Mult (A, B, C : Big_Natural)
  60       with
  61         Ghost,
  62         Pre  => A <= B,
  63         Post => A * C <= B * C;
  64
  65       procedure Lemma_Div_Commutation (X, Y : Uns)
  66       with
  67         Ghost,
  68         Pre  => Y /= 0,
  69         Post => Big (X) / Big (Y) = Big (X / Y);
  70
  71       procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive)
  72       with
  73         Ghost,
  74         Post => X / Y / Z = X / (Y * Z);
  75
  76       procedure Lemma_Euclidian (V, Q, F, R : Big_Integer)
  77       with
  78         Ghost,
  79         Pre  => F > 0 and then Q = V / F and then R = V rem F,
  80         Post => V = Q * F + R;
  81       --  Ghost lemma to prove the relation between the quotient/remainder of
  82       --  division by F and the value V.
  83
  84       ----------------------
  85       -- Lemma_Lower_Mult --
  86       ----------------------
  87
  88       procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null;
  89
  90       ---------------------------
  91       -- Lemma_Div_Commutation --
  92       ---------------------------
  93
  94       procedure Lemma_Div_Commutation (X, Y : Uns) is null;
  95
  96       ---------------------
  97       -- Lemma_Div_Twice --
  98       ---------------------
  99
 100       procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is
 101          XY  : constant Big_Natural := X / Y;
 102          YZ  : constant Big_Natural := Y * Z;
 103          XYZ : constant Big_Natural := X / Y / Z;
 104          R   : constant Big_Natural := (XY rem Z) * Y + (X rem Y);
 105       begin
 106          pragma Assert (X = XY * Y + (X rem Y));
 107          pragma Assert (XY = XY / Z * Z + (XY rem Z));
 108          pragma Assert (X = XYZ * YZ + R);
 109          pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y);
 110          pragma Assert (R <= YZ - 1);
 111          pragma Assert (X / YZ = (XYZ * YZ + R) / YZ);
 112          pragma Assert (X / YZ = XYZ + R / YZ);
 113       end Lemma_Div_Twice;
 114
 115       ---------------------
 116       -- Lemma_Euclidian --
 117       ---------------------
 118
 119       procedure Lemma_Euclidian (V, Q, F, R : Big_Integer) is null;
 120
 121       --  Local variables
 122
 123       W : Natural;
 124       T : Uns;
 125
 126       --  Local ghost variables
 127
 128       Max_W  : constant Natural := Max_Log10 with Ghost;
 129       Pow    : Big_Integer := 1 with Ghost;
 130       T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost;
 131
 132    --  Start of processing for System.Width_U
 133
 134    begin
 135       if Lo > Hi then
 136          return 0;
 137
 138       else
 139          --  Minimum value is 2, one for space, one for digit
 140
 141          W := 2;
 142
 143          --  Get max of absolute values
 144
 145          T := Uns'Max (Lo, Hi);
 146
 147          --  Increase value if more digits required
 148
 149          while T >= 10 loop
 150             Lemma_Div_Commutation (T, 10);
 151             Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10);
 152
 153             T := T / 10;
 154             W := W + 1;
 155             Pow := Pow * 10;
 156
 157             pragma Loop_Invariant (W in 3 .. Max_W + 2);
 158             pragma Loop_Invariant (Pow = Big_10 ** (W - 2));
 159             pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow);
 160             pragma Loop_Variant (Decreases => T);
 161          end loop;
 162
 163          declare
 164             F : constant Big_Integer := Big_10 ** (W - 2) with Ghost;
 165             Q : constant Big_Integer := Big (T_Init) / F with Ghost;
 166             R : constant Big_Integer := Big (T_Init) rem F with Ghost;
 167          begin
 168             pragma Assert (Q < Big_10);
 169             Lemma_Euclidian (Big (T_Init), Q, F, R);
 170             Lemma_Lower_Mult (Q, Big (9), F);
 171             pragma Assert (Big (T_Init) <= Big (9) * F + F - 1);
 172             pragma Assert (Big (T_Init) < Big_10 * F);
 173             pragma Assert (Big_10 * F = Big_10 ** (W - 1));
 174          end;
 175
 176          return W;
 177       end if;
 178    end Width;
 179
 180 end System.Width_U;