diff mbox series

[COMMITTED] ada: Remove dynamic frame in System.Image_D and document it in System.Image_F

Message ID 20240513083642.166158-1-poulhies@adacore.com
State New
Headers show
Series [COMMITTED] ada: Remove dynamic frame in System.Image_D and document it in System.Image_F | expand

Commit Message

Marc Poulhiès May 13, 2024, 8:36 a.m. UTC
From: Eric Botcazou <ebotcazou@adacore.com>

The former can easily be removed while the latter cannot.

gcc/ada/

	* libgnat/s-imaged.ads (System.Image_D): Add Uns formal parameter.
	* libgnat/s-imaged.adb: Add with clauses for System.Image_I,
	System.Value_I_Spec and System.Value_U_Spec.
	(Uns_Spec): New instance of System.Value_U_Spec.
	(Int_Spec): New instance of System.Value_I_Spec.
	(Image_I): New instance of System.Image_I.
	(Set_Image_Integer): New renaming.
	(Set_Image_Decimal): Replace 'Image with call to Set_Image_Integer.
	* libgnat/s-imde32.ads (Uns32): New subtype.
	(Impl): Pass Uns32 as second actual paramter to Image_D.
	* libgnat/s-imde64.ads (Uns64): New subtype.
	(Impl): Pass Uns64 as second actual paramter to Image_D.
	* libgnat/s-imde128.ads (Uns128): New subtype.
	(Impl): Pass Uns128 as second actual paramter to Image_D.
	* libgnat/s-imagef.adb (Set_Image_Fixed): Document bounds for the
	A, D and AF local constants.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/s-imaged.adb  | 55 +++++++++++++++++++++++++++++++++--
 gcc/ada/libgnat/s-imaged.ads  |  5 ++--
 gcc/ada/libgnat/s-imagef.adb  |  9 ++++++
 gcc/ada/libgnat/s-imde128.ads |  3 +-
 gcc/ada/libgnat/s-imde32.ads  |  3 +-
 gcc/ada/libgnat/s-imde64.ads  |  3 +-
 6 files changed, 70 insertions(+), 8 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/s-imaged.adb b/gcc/ada/libgnat/s-imaged.adb
index 800a8e421cd..3a3b34960ca 100644
--- a/gcc/ada/libgnat/s-imaged.adb
+++ b/gcc/ada/libgnat/s-imaged.adb
@@ -29,10 +29,42 @@ 
 --                                                                          --
 ------------------------------------------------------------------------------
 
+with System.Image_I;
 with System.Img_Util; use System.Img_Util;
+with System.Value_I_Spec;
+with System.Value_U_Spec;
 
 package body System.Image_D is
 
+   --  Contracts, 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 (Assert             => Ignore,
+                            Assert_And_Cut     => Ignore,
+                            Contract_Cases     => Ignore,
+                            Ghost              => Ignore,
+                            Loop_Invariant     => Ignore,
+                            Pre                => Ignore,
+                            Post               => Ignore,
+                            Subprogram_Variant => Ignore);
+
+   package Uns_Spec is new System.Value_U_Spec (Uns);
+   package Int_Spec is new System.Value_I_Spec (Int, Uns, Uns_Spec);
+
+   package Image_I is new System.Image_I
+     (Int    => Int,
+      Uns    => Uns,
+      U_Spec => Uns_Spec,
+      I_Spec => Int_Spec);
+
+   procedure Set_Image_Integer
+     (V : Int;
+      S : in out String;
+      P : in out Natural)
+     renames Image_I.Set_Image_Integer;
+
    -------------------
    -- Image_Decimal --
    -------------------
@@ -71,11 +103,28 @@  package body System.Image_D is
       Aft   : Natural;
       Exp   : Natural)
    is
-      Digs : String := Int'Image (V);
-      --  Sign and digits of decimal value
+      Maxdigs : constant Natural := Int'Width;
+      --  Maximum length needed for Image of an Int
+
+      Digs  : String (1 .. Maxdigs);
+      Ndigs : Natural;
+      --  Buffer for the image of the integer value
 
    begin
-      Set_Decimal_Digits (Digs, Digs'Length, S, P, Scale, Fore, Aft, Exp);
+      --  Set the first character like Image
+
+      if V >= 0 then
+         Digs (1) := ' ';
+         Ndigs := 1;
+      else
+         Ndigs := 0;
+      end if;
+
+      Set_Image_Integer (V, Digs, Ndigs);
+
+      pragma Assert (1 <= Ndigs and then Ndigs <= Maxdigs);
+
+      Set_Decimal_Digits (Digs, Ndigs, S, P, Scale, Fore, Aft, Exp);
    end Set_Image_Decimal;
 
 end System.Image_D;
diff --git a/gcc/ada/libgnat/s-imaged.ads b/gcc/ada/libgnat/s-imaged.ads
index 5fe8f82fa17..927ea50e769 100644
--- a/gcc/ada/libgnat/s-imaged.ads
+++ b/gcc/ada/libgnat/s-imaged.ads
@@ -36,6 +36,7 @@ 
 generic
 
    type Int is range <>;
+   type Uns is mod <>;
 
 package System.Image_D is
 
@@ -46,8 +47,8 @@  package System.Image_D is
       Scale : Integer);
    --  Computes fixed_type'Image (V), where V is the integer value (in units of
    --  delta) of a decimal type whose Scale is as given and stores the result
-   --  S (1 .. P), updating P to the value of L. The image is given by the
-   --  rules in RM 3.5(34) for fixed-point type image functions. The caller
+   --  S (1 .. P), updating P on return. The result is computed according to
+   --  the rules for image for fixed-point types (RM 3.5(34)). The caller
    --  guarantees that S is long enough to hold the result and has a lower
    --  bound of 1.
 
diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb
index 46e7ab09e09..56992064fb1 100644
--- a/gcc/ada/libgnat/s-imagef.adb
+++ b/gcc/ada/libgnat/s-imagef.adb
@@ -274,8 +274,15 @@  package body System.Image_F is
       --  Aft0 digits (unless V is zero). In both cases, we compute one more
       --  digit than requested so that Set_Decimal_Digits can round at Aft.
 
+      --  Aft0 is bounded by the 'Aft of a type with delta 1/2**(Int'Size - 1)
+      --  which is N = ceil ((Int'Siz - 1) * log2 / log10). Aft lies in the
+      --  range of type Field declared in Ada.Text_IO so is bounded by 255.
+      --  Thus A is bounded by 256 + ceil ((Int'Siz - 1) * log2 / log10).
+
       D : constant Integer :=
             Integer'Max (-Maxdigs, Integer'Min (A, Maxdigs - (For0 - 1)));
+      --  D lies in the range -Maxdigs .. A
+
       Y : constant Int     := Num * 10**Integer'Max (0, D);
       Z : constant Int     := Den * 10**Integer'Max (0, -D);
       --  See the description of the algorithm above
@@ -285,6 +292,8 @@  package body System.Image_F is
       --  is larger than A if the first round does not compute all the digits
       --  before the decimal point, i.e. (For0 - 1) larger than Maxdigs.
 
+      --  AF is bounded by 256 + Maxdigs + ceil ((Int'Siz - 1) * log2 / log10)
+
       N : constant Natural := 1 + (AF + Maxdigs - 1) / Maxdigs;
       --  Number of rounds of scaled divide to be performed
 
diff --git a/gcc/ada/libgnat/s-imde128.ads b/gcc/ada/libgnat/s-imde128.ads
index ce165b4f29c..5c6e2396fd6 100644
--- a/gcc/ada/libgnat/s-imde128.ads
+++ b/gcc/ada/libgnat/s-imde128.ads
@@ -39,8 +39,9 @@  with System.Image_D;
 package System.Img_Decimal_128 is
 
    subtype Int128 is Interfaces.Integer_128;
+   subtype Uns128 is Interfaces.Unsigned_128;
 
-   package Impl is new Image_D (Int128);
+   package Impl is new Image_D (Int128, Uns128);
 
    procedure Image_Decimal128
      (V     : Int128;
diff --git a/gcc/ada/libgnat/s-imde32.ads b/gcc/ada/libgnat/s-imde32.ads
index 5951d91638c..9a5b582ebc3 100644
--- a/gcc/ada/libgnat/s-imde32.ads
+++ b/gcc/ada/libgnat/s-imde32.ads
@@ -39,8 +39,9 @@  with System.Image_D;
 package System.Img_Decimal_32 is
 
    subtype Int32 is Interfaces.Integer_32;
+   subtype Uns32 is Interfaces.Unsigned_32;
 
-   package Impl is new Image_D (Int32);
+   package Impl is new Image_D (Int32, Uns32);
 
    procedure Image_Decimal32
      (V     : Int32;
diff --git a/gcc/ada/libgnat/s-imde64.ads b/gcc/ada/libgnat/s-imde64.ads
index 5f39dcae6a2..f5aec4e2c87 100644
--- a/gcc/ada/libgnat/s-imde64.ads
+++ b/gcc/ada/libgnat/s-imde64.ads
@@ -39,8 +39,9 @@  with System.Image_D;
 package System.Img_Decimal_64 is
 
    subtype Int64 is Interfaces.Integer_64;
+   subtype Uns64 is Interfaces.Unsigned_64;
 
-   package Impl is new Image_D (Int64);
+   package Impl is new Image_D (Int64, Uns64);
 
    procedure Image_Decimal64
      (V     : Int64;