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