If it matters, this discussion really starts here. Consider the following vector declaration:
package IntVecs is new Ada.Containers.Vectors
(Index_Type => Positive, Element_Type => Positive);
…later used as follows (Value has type Positive):
if Proper_Divisors (Value)'Reduce ("+", 0) > Value then
return True;
end if;
In gnat 13.2.2, this was fine. In gnat 14.x, it crashes.
Should it?
The type of the result of the 'Reduce expression is not specified. Since it is told to start with 0, I would assume it would be no smaller than Natural, and ordinarily I’d have expected universal integer. Apparently 13.2.2 agreed with me in some fashion, while 14.x assumes it’s Positive, eventually throwing an error.
I took a look at ARM 4.5.10 but didn’t come out any more enlightened for it. In particular, the definition of “the expected type for a reduction_attribute_reference” seems vague. It says that Accum_Type is “a subtype of the expected type” of that, and Value_Type seems to be defined by the Reducer function and procedure below that. Then, " The expected type of an initial_value_expression of a reduction_specification is that of subtype Accum_Type."
Now, I’ve provided 0 as the initial value, which IMHO should tell the compiler that the expected type can be no smaller than Natural. But it picks Positive?
pragma Ada_2022;
with Ada.Text_IO; use Ada.Text_IO;
procedure Reduction is
Arr : array (Positive range <>) of Positive
:= (1, 3, 5, 7, 9);
begin
Put_Line (Arr'Reduce ("+", 0)'Image);
end Reduction;
gives
$ gnatmake reduction -f
gcc -c reduction.adb
reduction.adb:7:31: warning: value not in range of type "Standard.Positive" [enabled by default]
reduction.adb:7:31: warning: Constraint_Error will be raised at run time [enabled by default]
gnatbind -x reduction.ali
gnatlink reduction.ali
ramoth:gcc simon$ ./reduction
raised CONSTRAINT_ERROR : reduction.adb:7 range check failed
It’d be good if the container version produced the same warnings!
I think the justification is in ARM 14.5.10(19), " A reduction_attribute_reference denotes a value, with its nominal subtype being the subtype of the first parameter of the subprogram denoted by the reducer_ name", i.e. "+"; 0 is universal, so the only other type around is Positive.
This does seem a straightforward example, you’d think it would work!
You can work around this by specifying the Natural version of "+". For example with a renames, as in:
function Is_Abundant (Value : Positive) return Boolean is
function Add(Left, Right : Natural) return Natural renames "+";
begin
if Not_Abundant_Cache.Contains (Value)
or else Semiperfect_Cache.Contains (Value)
then
return False;
end if;
if Proper_Divisors (Value)'Reduce (Add, 0) > Value then
return True;
end if;
Not_Abundant_Cache.Insert (Value);
return False;
end Is_Abundant;
Edit:
another workaround would be an operator with the profile expected/required by 'Reduce:
function "+"(Left : Natural; Right : Positive) return Natural renames Standard."+";
What the operator is capable of doesn’t matter here, 'Reduce requires specific subtypes, and since there’s no (overloaded) operator with the required profile available, the compiler seems to use Positive for both Left and Right.
Another workaround would be to provide the exact profile:
function "+"(Left : Natural; Right : Positive) return Natural renames Standard."+";
'Parallel_Reduce har even stricter rules (Left and Right must statically match)
Whether the compiler should be able to resolve this without workarounds is of course a very good question. A qualifier for 0 should suffice (which has no effect at this time), in my opinion. Maybe the compiler just defaults to the rules for 'Parallel_Reduce in this case?
This is pretty clearly a GNAT bug in my view. Subtypes should come from the reducer subprogram (RM 4.5.10(12/5-13/5)):
12/5
function Reducer(Accumulator : Accum_Type;
Value : Value_Type) return Accum_Type;
13/5
procedure Reducer(Accumulator : in out Accum_Type;
Value : in Value_Type);
The “+” operator takes the base subtypes, so there should be no constraint applied here, except that needed to avoid overflow, which at a minimum should be the base range of Integer, which is Integer’First … Integer’Last, typically -2**31 .. +2**31-1.
I don’t disagree with your general assertion, but I do think the RM is not as clear on it.
11/5 says that A reducer subprogram is subtype conformant with one of the following specifications which sounds more like the reducer specification is based on the accum_type rather than the other way around.
10/5 says Accum_Type is a subtype of the expected type of the reduction_attribute_reference, which makes me lean towards the value_sequence being worked on sets the subtype for Accum_Type
I think it could go either way based on the wording and how you view the context. Maybe this is a good place for some wording updates to clarify exactly how Accum_Type is supposed to be determined?
I agree the RM is not crystal clear here, but I do know the original intent, and it is that the Accum_Type comes from the reducer subprogram, and in this case, it is the predefined “+” operator of Integer, which does not impose any constraint on the parameter or result subtypes.
The Annotated Ada RM (aka “AARM”) includes the following annotation at AARM 4.5.10(9.a/5):
9.a/5 Discussion:Accum_Type represents the result of the reduction (the accumulator type), and Value_Type represents the type of the input values to the reduction.
The actual RM “Name Resolution” wording also already indicates that the Accum_Type and the Value_Type are determined by a set of bullets, one of which requires that the Reducer subprogram be subtype conformant with a spec that uses Accum_Type and Value_Type as parameter and/or result subtypes. So although it doesn’t directly say that that is where these two subtypes come from, the requirement for subtype conformance requires subtype matching, so it would be an error if they didn’t match the parameter/results subtypes of the reducer subprogram. So if GNAT accepts it, it should mean that Accum_Type and Value_Type match the subtypes of the specified reducer, and in this case, that reducer imposes no constraints.
Admittedly it is somewhat backward reasoning, but Name Resolution rules tend to be a bit “declarative” in nature, where the compiler is required to find a set of types, subtypes, and subprograms that all “work” given the various Name Resolution specifications, and it is not specified exactly how the compiler has to do this, provided it complains if there are zero interpretations (unresolved), or more than one (ambiguity).
This is my recollection, but I couldn’t find it in the ARM. The definition of the predefined operators for integer types in 4.5 use the first-named subtype name. Where is this use of the base subtype defined?
For a signed integer type, the exception Constraint_Error is raised by the execution of an operation that cannot deliver the correct result because it is outside the base range of the type.
In RM 3.5.4(24/5) there is an additional Implementation Permission:
For the execution of a predefined operation of a signed integer type, it is optional to raise Constraint_Error if the result is outside the base range of the type, so long as the correct result is produced.
RM 4.5(11) has the following Implementation Requirement:
The implementation of a predefined operator that delivers a result of an integer or fixed point type may raise Constraint_Error only if the result is outside the base range of the result type.
There is an important annotation in AARM 4.5.1(3.b/2-3.i/2):
Ramification: {AI95-00145-01} For these operators, we are talking about the type without any (interesting) subtype, and not some subtype with a constraint or exclusion. Since it’s possible that there is no name for the “uninteresting” subtype, we denote the type with an italicized T. This applies to the italicized T in many other predefined operators and attributes as well.
{AI95-00145-01} In many cases, there is a subtype with the correct properties available. The italicized T means:
T’Base, for scalars;
the first subtype of T, for tagged types;
a subtype of the type T without any constraint or null exclusion, in other cases.
Note that “without a constraint” is not the same as unconstrained. For instance, a record type with no discriminant part is considered constrained; no subtype of it has a constraint, but the subtype is still constrained.
Thus, the last case often is the same as the first subtype of T, but that isn’t the case for constrained array types (where the correct subtype is unconstrained) and for access types with a null_exclusion (where the correct subtype does not exclude null).
This italicized T is used for defining operators and attributes of the language. The meaning is intended to be as described here.
Thanks for the explanation. I was aware of the paragraphs with the wording “outside the base range”, but was looking for something like
function "+" (Left : in S'Base; Right : in S'Base) return S'Base;
I missed the annotation in AARM 4.5.1 because I was looking for integer operators that returned a value of the type, and 4.5.1 is about boolean operators that return a boolean type, so I didn’t look at it (had it been in 4.5, I would have seen it). Now that you’ve brought it to my attention, it’s obvious that the operators for “every specific numeric type T” are defined for the base type.
I think that defining them explicitly in terms of S’Base would be clearer, though.
This bug was already reported as [TA10-005 public] on Sat, 10 Oct 2020 16:05:30 +0200 for the Roman_Number example 4.2.1(19/5ff).
Seems like AdaCore doesn’t care much for public bug reports.
$ gnatmake reduction.adb
gcc -c reduction.adb
reduction.adb:7:31: warning: value not in range of type "Standard.Positive" [enabled by default]
reduction.adb:7:31: warning: Constraint_Error will be raised at run time [enabled by default]
gnatbind -x reduction.ali
gnatlink reduction.ali
on gcc version 14.2.1 20241116 (Gentoo 14.2.1_p20241116 p3).
and
$ ./reduction
raised CONSTRAINT_ERROR : reduction.adb:7 range check failed
procedure IntVec is
package IntVecs is new Ada.Containers.Vectors
(Index_Type => Positive, Element_Type => Positive);
V: IntVecs.Vector;
U: Positive;
begin
V.Append (1);
U := V'Reduce ("+", 0);
end IntVec;
What if we’d left out the V.Append? V’Reduce would have tried to return the initial value, 0, which would clearly have resulted in CE.
Write U : Natural;. GCC 14: error as before; GCC 15: no error! I’ll update the PR to that effect.