------------------------------------------------------------------------------ | |

-- -- | |

-- GNAT RUN-TIME COMPONENTS -- | |

-- -- | |

-- S Y S T E M . W I D T H _ I -- | |

-- -- | |

-- B o d y -- | |

-- -- | |

-- Copyright (C) 1992-2022, 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_Ghost; | |

use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; | |

function System.Width_I (Lo, Hi : Int) 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); | |

----------------------- | |

-- Local Subprograms -- | |

----------------------- | |

package Signed_Conversion is new Signed_Conversions (Int => Int); | |

function Big (Arg : Int) return Big_Integer renames | |

Signed_Conversion.To_Big_Integer; | |

-- Maximum value of exponent for 10 that fits in Uns'Base | |

function Max_Log10 return Natural is | |

(case Int'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; | |

------------------ | |

-- Local Lemmas -- | |

------------------ | |

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 : Int) | |

with | |

Ghost, | |

Pre => X >= 0 and 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); | |

---------------------- | |

-- Lemma_Lower_Mult -- | |

---------------------- | |

procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null; | |

--------------------------- | |

-- Lemma_Div_Commutation -- | |

--------------------------- | |

procedure Lemma_Div_Commutation (X, Y : Int) is null; | |

--------------------- | |

-- Lemma_Div_Twice -- | |

--------------------- | |

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; | |

-- Local variables | |

W : Natural; | |

T : Int; | |

-- Local ghost variables | |

Max_W : constant Natural := Max_Log10 with Ghost; | |

Big_10 : constant Big_Integer := Big (10) with Ghost; | |

Pow : Big_Integer := 1 with Ghost; | |

T_Init : constant Int := | |

Int'Max (abs (Int'Max (Lo, Int'First + 1)), | |

abs (Int'Max (Hi, Int'First + 1))) | |

with Ghost; | |

-- Start of processing for System.Width_I | |

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 := Int'Max ( | |

abs (Int'Max (Lo, Int'First + 1)), | |

abs (Int'Max (Hi, Int'First + 1))); | |

-- 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 (T >= 0); | |

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); | |

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_I, | |

-- which cannot be expressed readily as a postcondition as this would | |

-- require making the instantiation Signed_Conversion and function Big | |

-- available from the spec. | |

pragma Assert (Big (Int'Max (Lo, Int'First + 1)) < Big_10 ** (W - 1)); | |

pragma Assert (Big (Int'Max (Hi, Int'First + 1)) < Big_10 ** (W - 1)); | |

return W; | |

end if; | |

end System.Width_I; |