| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT RUN-TIME COMPONENTS -- |
| -- -- |
| -- S Y S T E M . W I D T H _ U -- |
| -- -- |
| -- B o d y -- |
| -- -- |
| -- Copyright (C) 1992-2021, 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 Ada.Numerics.Big_Numbers.Big_Integers; |
| use Ada.Numerics.Big_Numbers.Big_Integers; |
| |
| function System.Width_U (Lo, Hi : Uns) return Natural 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); |
| |
| W : Natural; |
| T : Uns; |
| |
| package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); |
| |
| function Big (Arg : Uns) return Big_Integer is |
| (Unsigned_Conversion.To_Big_Integer (Arg)) |
| with Ghost; |
| |
| -- Maximum value of exponent for 10 that fits in Uns'Base |
| function Max_Log10 return Natural is |
| (case Uns'Base'Size is |
| when 8 => 2, |
| when 16 => 4, |
| when 32 => 9, |
| when 64 => 19, |
| when 128 => 38, |
| when others => raise Program_Error) |
| with Ghost; |
| |
| Max_W : constant Natural := Max_Log10 with Ghost; |
| Big_10 : constant Big_Integer := Big (10) with Ghost; |
| |
| procedure Lemma_Lower_Mult (A, B, C : Big_Natural) |
| with |
| Ghost, |
| Pre => A <= B, |
| Post => A * C <= B * C; |
| |
| procedure Lemma_Div_Commutation (X, Y : Uns) |
| with |
| Ghost, |
| Pre => Y /= 0, |
| Post => Big (X) / Big (Y) = Big (X / Y); |
| |
| procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) |
| with |
| Ghost, |
| Post => X / Y / Z = X / (Y * Z); |
| |
| procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is |
| begin |
| null; |
| end Lemma_Lower_Mult; |
| |
| procedure Lemma_Div_Commutation (X, Y : Uns) is |
| begin |
| null; |
| end Lemma_Div_Commutation; |
| |
| procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is |
| XY : constant Big_Natural := X / Y; |
| YZ : constant Big_Natural := Y * Z; |
| XYZ : constant Big_Natural := X / Y / Z; |
| R : constant Big_Natural := (XY rem Z) * Y + (X rem Y); |
| begin |
| pragma Assert (X = XY * Y + (X rem Y)); |
| pragma Assert (XY = XY / Z * Z + (XY rem Z)); |
| pragma Assert (X = XYZ * YZ + R); |
| pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y); |
| pragma Assert (R <= YZ - 1); |
| pragma Assert (X / YZ = (XYZ * YZ + R) / YZ); |
| pragma Assert (X / YZ = XYZ + R / YZ); |
| end Lemma_Div_Twice; |
| |
| Pow : Big_Integer := 1 with Ghost; |
| T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; |
| |
| begin |
| if Lo > Hi then |
| return 0; |
| |
| else |
| -- Minimum value is 2, one for sign, one for digit |
| |
| W := 2; |
| |
| -- Get max of absolute values, but avoid bomb if we have the maximum |
| -- negative number (note that First + 1 has same digits as First) |
| |
| T := Uns'Max (Lo, Hi); |
| |
| -- Increase value if more digits required |
| |
| while T >= 10 loop |
| Lemma_Div_Commutation (T, 10); |
| Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); |
| |
| T := T / 10; |
| W := W + 1; |
| Pow := Pow * 10; |
| |
| pragma Loop_Invariant (W in 3 .. Max_W + 3); |
| pragma Loop_Invariant (Pow = Big_10 ** (W - 2)); |
| pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow); |
| pragma Loop_Variant (Decreases => T); |
| pragma Annotate |
| (CodePeer, False_Positive, |
| "validity check", "confusion on generated code"); |
| end loop; |
| |
| declare |
| F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; |
| Q : constant Big_Integer := Big (T_Init) / F with Ghost; |
| R : constant Big_Integer := Big (T_Init) rem F with Ghost; |
| begin |
| pragma Assert (Q < Big_10); |
| pragma Assert (Big (T_Init) = Q * F + R); |
| Lemma_Lower_Mult (Q, Big (9), F); |
| pragma Assert (Big (T_Init) <= Big (9) * F + F - 1); |
| pragma Assert (Big (T_Init) < Big_10 * F); |
| pragma Assert (Big_10 * F = Big_10 ** (W - 1)); |
| end; |
| |
| -- This is an expression of the functional postcondition for Width_U, |
| -- which cannot be expressed readily as a postcondition as this would |
| -- require making the instantiation Unsigned_Conversion and function |
| -- Big available from the spec. |
| |
| pragma Assert (Big (Lo) < Big_10 ** (W - 1)); |
| pragma Assert (Big (Hi) < Big_10 ** (W - 1)); |
| |
| return W; |
| end if; |
| |
| end System.Width_U; |
