https://gcc.gnu.org/g:b2dcb85380b606e4064089bb79dde2c9ff271ad0
commit r16-1932-gb2dcb85380b606e4064089bb79dde2c9ff271ad0
Author: Eric Botcazou <ebotca...@adacore.com>
Date: Tue Jun 3 18:54:03 2025 +0200
ada: Fix spurious Constraint_Error raised by 'Value of fixed-point types
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.
Diff:
---
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 c7cf06ba444f..6c2b940736ba 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 735859c3f150..26f04ed726ee 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 7424346fe3d6..78c25f29bc8b 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 ed69d65df09d..3ceda12b9ec3 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 ec8deca6ca4e..8757ffb25149 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 edf58ad85ead..b9f4f43226f0 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 bc0062f9d9f8..eb02a4a2cece 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 1743749f5421..f38f2cc66ac3 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 --
