From: Eric Botcazou <ebotca...@adacore.com>
This happens for very large Smalls with regard to the size of the mantissa,
because the prerequisites of the implementation used in this case are not
met, although they are documented in the head comment of Integer_To_Fixed.
This change documents them at the beginning of the body of System.Value_F
and adjusts the compiler interface accordingly.
gcc/ada/ChangeLog:
* libgnat/s-valuef.adb: Document the prerequisites more precisely.
* libgnat/a-tifiio.adb (OK_Get_32): Adjust to the prerequisites.
(OK_Get_64): Likewise.
* libgnat/a-tifiio__128.adb (OK_Get_32): Likewise.
(OK_Get_64): Likewise.
(OK_Get_128): Likewise.
* libgnat/a-wtfiio.adb (OK_Get_32): Likewise.
(OK_Get_64): Likewise.
* libgnat/a-wtfiio__128.adb (OK_Get_32): Likewise.
(OK_Get_64): Likewise.
(OK_Get_128): Likewise.
* libgnat/a-ztfiio.adb (OK_Get_32): Likewise.
(OK_Get_64): Likewise.
* libgnat/a-ztfiio__128.adb (OK_Get_32): Likewise.
(OK_Get_64): Likewise.
(OK_Get_128): Likewise.
* exp_imgv.adb (Expand_Value_Attribute): Adjust the conditions under
which the RE_Value_Fixed{32,64,128} routines are called for ordinary
fixed-point types.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/exp_imgv.adb | 7 +++----
gcc/ada/libgnat/a-tifiio.adb | 6 ------
gcc/ada/libgnat/a-tifiio__128.adb | 9 ---------
gcc/ada/libgnat/a-wtfiio.adb | 6 ------
gcc/ada/libgnat/a-wtfiio__128.adb | 9 ---------
gcc/ada/libgnat/a-ztfiio.adb | 6 ------
gcc/ada/libgnat/a-ztfiio__128.adb | 9 ---------
gcc/ada/libgnat/s-valuef.adb | 16 ++++++++++------
8 files changed, 13 insertions(+), 55 deletions(-)
diff --git a/gcc/ada/exp_imgv.adb b/gcc/ada/exp_imgv.adb
index c7cf06ba444..6c2b940736b 100644
--- a/gcc/ada/exp_imgv.adb
+++ b/gcc/ada/exp_imgv.adb
@@ -1640,23 +1640,22 @@ package body Exp_Imgv is
Num : constant Uint := Norm_Num (Small_Value (Rtyp));
Den : constant Uint := Norm_Den (Small_Value (Rtyp));
Max : constant Uint := UI_Max (Num, Den);
- Min : constant Uint := UI_Min (Num, Den);
Siz : constant Uint := Esize (Rtyp);
begin
if Siz <= 32
and then Max <= Uint_2 ** 31
- and then (Min = Uint_1 or else Max <= Uint_2 ** 27)
+ and then (Num = Uint_1 or else Max <= Uint_2 ** 27)
then
Vid := RE_Value_Fixed32;
elsif Siz <= 64
and then Max <= Uint_2 ** 63
- and then (Min = Uint_1 or else Max <= Uint_2 ** 59)
+ and then (Num = Uint_1 or else Max <= Uint_2 ** 59)
then
Vid := RE_Value_Fixed64;
elsif System_Max_Integer_Size = 128
and then Max <= Uint_2 ** 127
- and then (Min = Uint_1 or else Max <= Uint_2 ** 123)
+ and then (Num = Uint_1 or else Max <= Uint_2 ** 123)
then
Vid := RE_Value_Fixed128;
else
diff --git a/gcc/ada/libgnat/a-tifiio.adb b/gcc/ada/libgnat/a-tifiio.adb
index 735859c3f15..26f04ed726e 100644
--- a/gcc/ada/libgnat/a-tifiio.adb
+++ b/gcc/ada/libgnat/a-tifiio.adb
@@ -194,9 +194,6 @@ package body Ada.Text_IO.Fixed_IO with SPARK_Mode => Off is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**31)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**31)
- or else
(Num'Base'Small_Numerator <= 2**27
and then Num'Base'Small_Denominator <= 2**27));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -223,9 +220,6 @@ package body Ada.Text_IO.Fixed_IO with SPARK_Mode => Off is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**63)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**63)
- or else
(Num'Base'Small_Numerator <= 2**59
and then Num'Base'Small_Denominator <= 2**59));
-- These conditions are derived from the prerequisites of System.Value_F
diff --git a/gcc/ada/libgnat/a-tifiio__128.adb
b/gcc/ada/libgnat/a-tifiio__128.adb
index 7424346fe3d..78c25f29bc8 100644
--- a/gcc/ada/libgnat/a-tifiio__128.adb
+++ b/gcc/ada/libgnat/a-tifiio__128.adb
@@ -201,9 +201,6 @@ package body Ada.Text_IO.Fixed_IO with SPARK_Mode => Off is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**31)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**31)
- or else
(Num'Base'Small_Numerator <= 2**27
and then Num'Base'Small_Denominator <= 2**27));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -230,9 +227,6 @@ package body Ada.Text_IO.Fixed_IO with SPARK_Mode => Off is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**63)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**63)
- or else
(Num'Base'Small_Numerator <= 2**59
and then Num'Base'Small_Denominator <= 2**59));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -259,9 +253,6 @@ package body Ada.Text_IO.Fixed_IO with SPARK_Mode => Off is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**127)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**127)
- or else
(Num'Base'Small_Numerator <= 2**123
and then Num'Base'Small_Denominator <= 2**123));
-- These conditions are derived from the prerequisites of System.Value_F
diff --git a/gcc/ada/libgnat/a-wtfiio.adb b/gcc/ada/libgnat/a-wtfiio.adb
index ed69d65df09..3ceda12b9ec 100644
--- a/gcc/ada/libgnat/a-wtfiio.adb
+++ b/gcc/ada/libgnat/a-wtfiio.adb
@@ -73,9 +73,6 @@ package body Ada.Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**31)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**31)
- or else
(Num'Base'Small_Numerator <= 2**27
and then Num'Base'Small_Denominator <= 2**27));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -102,9 +99,6 @@ package body Ada.Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**63)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**63)
- or else
(Num'Base'Small_Numerator <= 2**59
and then Num'Base'Small_Denominator <= 2**59));
-- These conditions are derived from the prerequisites of System.Value_F
diff --git a/gcc/ada/libgnat/a-wtfiio__128.adb
b/gcc/ada/libgnat/a-wtfiio__128.adb
index ec8deca6ca4..8757ffb2514 100644
--- a/gcc/ada/libgnat/a-wtfiio__128.adb
+++ b/gcc/ada/libgnat/a-wtfiio__128.adb
@@ -80,9 +80,6 @@ package body Ada.Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**31)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**31)
- or else
(Num'Base'Small_Numerator <= 2**27
and then Num'Base'Small_Denominator <= 2**27));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -109,9 +106,6 @@ package body Ada.Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**63)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**63)
- or else
(Num'Base'Small_Numerator <= 2**59
and then Num'Base'Small_Denominator <= 2**59));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -138,9 +132,6 @@ package body Ada.Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**127)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**127)
- or else
(Num'Base'Small_Numerator <= 2**123
and then Num'Base'Small_Denominator <= 2**123));
-- These conditions are derived from the prerequisites of System.Value_F
diff --git a/gcc/ada/libgnat/a-ztfiio.adb b/gcc/ada/libgnat/a-ztfiio.adb
index edf58ad85ea..b9f4f43226f 100644
--- a/gcc/ada/libgnat/a-ztfiio.adb
+++ b/gcc/ada/libgnat/a-ztfiio.adb
@@ -73,9 +73,6 @@ package body Ada.Wide_Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**31)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**31)
- or else
(Num'Base'Small_Numerator <= 2**27
and then Num'Base'Small_Denominator <= 2**27));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -102,9 +99,6 @@ package body Ada.Wide_Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**63)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**63)
- or else
(Num'Base'Small_Numerator <= 2**59
and then Num'Base'Small_Denominator <= 2**59));
-- These conditions are derived from the prerequisites of System.Value_F
diff --git a/gcc/ada/libgnat/a-ztfiio__128.adb
b/gcc/ada/libgnat/a-ztfiio__128.adb
index bc0062f9d9f..eb02a4a2cec 100644
--- a/gcc/ada/libgnat/a-ztfiio__128.adb
+++ b/gcc/ada/libgnat/a-ztfiio__128.adb
@@ -81,9 +81,6 @@ package body Ada.Wide_Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**31)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**31)
- or else
(Num'Base'Small_Numerator <= 2**27
and then Num'Base'Small_Denominator <= 2**27));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -110,9 +107,6 @@ package body Ada.Wide_Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**63)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**63)
- or else
(Num'Base'Small_Numerator <= 2**59
and then Num'Base'Small_Denominator <= 2**59));
-- These conditions are derived from the prerequisites of System.Value_F
@@ -139,9 +133,6 @@ package body Ada.Wide_Wide_Text_IO.Fixed_IO is
((Num'Base'Small_Numerator = 1
and then Num'Base'Small_Denominator <= 2**127)
or else
- (Num'Base'Small_Denominator = 1
- and then Num'Base'Small_Numerator <= 2**127)
- or else
(Num'Base'Small_Numerator <= 2**123
and then Num'Base'Small_Denominator <= 2**123));
-- These conditions are derived from the prerequisites of System.Value_F
diff --git a/gcc/ada/libgnat/s-valuef.adb b/gcc/ada/libgnat/s-valuef.adb
index 1743749f542..f38f2cc66ac 100644
--- a/gcc/ada/libgnat/s-valuef.adb
+++ b/gcc/ada/libgnat/s-valuef.adb
@@ -36,12 +36,13 @@ with System.Value_R;
package body System.Value_F is
-- The prerequisite of the implementation is that the computation of the
- -- operands of the scaled divide does not unduly overflow when the small
- -- is neither an integer nor the reciprocal of an integer, which means
- -- that its numerator and denominator must be both not larger than the
- -- smallest divide 2**(Int'Size - 1) / Base where Base ranges over the
- -- supported values for the base of the literal. Given that the largest
- -- supported base is 16, this gives a limit of 2**(Int'Size - 5).
+ -- operands of the scaled divide does not unduly overflow, which means
+ -- that the numerator and the denominator of the small must be both not
+ -- larger than the smallest divide 2**(Int'Size - 1) / Base where Base
+ -- ranges over the supported values for the base of the literal, except
+ -- when the numerator is 1, in which case up to 2**(Int'Size - 1) is
+ -- permitted for the denominator. Given that the largest supported base
+ -- is 16, this gives a limit of 2**(Int'Size - 5) in the general case.
pragma Assert (Int'Size <= Uns'Size);
-- We need an unsigned type large enough to represent the mantissa
@@ -135,6 +136,9 @@ package body System.Value_F is
-- Num * (Base ** -ScaleB) <= Num * (B ** N) < Den * B
-- which means that the product does not overflow if Den <= 2**(M-1) / B.
+ -- Moreover, if 2**(M-1) / B < Den <= 2**(M-1), we can add 1 to ScaleB and
+ -- divide Val by B while preserving the rightmost B-digit of Val in Extra2
+ -- without changing the computation when Num = 1.
----------------------
-- Integer_To_Fixed --
--
2.43.0
