ada

Range check failed when using reduction expression in Ada

I tried to convert the array concatenation in function A to the new Ada 2022 reduction expression (see function B), but I get a range check failed error. What am I doing wrong?

    with Ada.Text_IO;
    with Ada.Unchecked_Conversion;
    with Interfaces;
    
    procedure Learn is
      type u8 is new Interfaces.Unsigned_8;
      type u32 is new Interfaces.Unsigned_32;
      
      type Bytes is array (Positive range <>) of aliased u8;
      type Words is array (Positive range <>) of aliased u32;
      
      Some_Words : Words (1 .. 3) := [1111, 22222, 333333];
      
      subtype Bytes_4 is Bytes (1 .. 4);
      function Convert is new Ada.Unchecked_Conversion (u32, Bytes_4);
      
      function A (W : Words) return Bytes is
        (Convert (W (1)) & Convert (W (2)) & Convert (W (3)));
      A1 : Bytes := A (Some_Words);
      
      function B (W : Words) return Bytes is
        ([for X of W => Convert (X)]'Reduce ("&", []));
      B1 : Bytes := B (Some_Words);
    begin
        Ada.Text_IO.Put_Line (A1'Image);
        Ada.Text_IO.Put_Line (B1'Image);
    end Learn;

Console output:

$ gprbuild -q -P main.gpr
learn.adb:22:30: warning: too many elements for subtype of "Bytes" defined at line 22 [enabled by default]
learn.adb:22:30: warning: expected 0 elements; found 4 elements [enabled by default]
learn.adb:22:30: warning: Constraint_Error will be raised at run time [enabled by default]
Build completed successfully.
$ ./learn
raised CONSTRAINT_ERROR : learn.adb:22 range check failed
exit status: 1
Solution

  • I’m not sure this is a bug. It could be an (overly?) simple interpretation of the ARM.

    The learn.adacore section on reduction expressions says, a little way down, that

    A := [2, 3, 4];
I := A'Reduce ("+", 0);

    is equivalent to

    I := 0;
for E of A loop
   I := I + E;
end loop;

    and you can see that in your case you initialize the accumulator (a local variable equivalent to I above) to [], with fixed length 0.

    Indeed, using the -gnatG switch, we get this indication of the compiler's internal representation of your function B:

       function b (w : words) return bytes is
   begin
      null;
      return
         do
            [subtype T14b is bytes (1 .. 0)]
            B37b : T14b := [];
            L39b : for C40b in w'first(1) .. w'last(1) loop
               [constraint_error when
                 not (integer(C40b) in w'first .. w'last)
                 "index check failed"]
               x : u32 renames w (C40b);
               B37b := [constraint_error "range check failed"];
            end loop L39b;
         in B37b end
      ....
   end learn__b;

    (B37b is the accumulator, and the assignment raises an unconditional CE).

    The ARM says in ARM 4.5.10(24) that "The evaluation of a use of this attribute ... initializes the accumulator of the reduction expression to the ... initial value". So far, so good (or bad, depending on your point of view).

    The next paragraph says that "each value of the value_sequence is passed, in order, as the second (Value) parameter to a call on Reducer, with the first (Accumulator) parameter being the prior value of the accumulator, saving the result as the new value of the accumulator". I think you’d need to use recursion when the required result type is unconstrained, and I very much doubt that the ARG would require an implementer to do that.