Odd behaviour with indefinite types

[sidisyom]

Consider the following declarations:

type My_Type is range 1 .. 3;
type My_Array is array (My_Type) of Float;
type Your_Array is array (My_Type range <>) of Float;

MA : My_Array; --   Definite type, no bounds required
YAB : Your_Array (1 .. 2); --  Indefinite type, explicit bounds
YAU : Your_Array := (1.1, 2.2, 3.3); --   No explicit bounds but will be 1 .. 3

Now, suppose we want to iterate over all different ranges of the above types and objects like so:

for I in My_Type'Range loop
   case I is
      when 1 => null;
      when 2 => null;
      when 3 => null;
   end case;
end loop;

for I in MA'Range loop
   case I is
      when 1 => null;
      when 2 => null;
      when 3 => null;
   end case;
end loop;

for I in YAB'Range loop
   case I is
      when 1 => null;
      when 2 => null;
   end case;
end loop;

The compiler can very nicely determine all possible ranges and statically confirm that all possible alternatives in the case statements have been covered.

However, trying to do the same with the last object where the bounds are determined from the assignment i.e. :

for I in YAU'Range loop
   case I is
      when 1 => null;
      when 2 => null;
      when 3 => null;
   end case;
end loop;

results in the error:

So, in this case I is clearly taken to be a signed byte which is the base type that the compiler has chosen for My_Type and hence it complains that the rest of the alternatives aren’t covered in the case.

The solution is to add a when others => .. like so:

for I in YAU'Range loop
   case I is
      when 1 => null;
      when 2 => null;
      when 3 => null;
      when others => raise Constraint_Error with "Impossible!";
   end case;
end loop;

But this others case can never be, right? Isn’t it a bit odd that the compiler can pick the bounds up in all other cases but in this last case it fails to do that and it falls-back to the base type range?

What’s even more interesting is that doing something like:

YAU : Your_Array := (1.1, 2.2, 3.3, 4.4);

results in the warning:

so clearly, the compiler is able to determine the bounds statically in the bounds-from-assignment case..

(The same behaviour occurs in the case where YAU would be passed as an argument to a subprogram i.e. maybe declared to take YA : Your_Array)

The somewhat inconvenient issue here might be the fact that a fabricated when others => .. alternative needs to be added which slightly breaks the nice static case alternatives coverage and perhaps lowers the confidence to someone reading this code.

Any thoughts? (using gnat_native=14.2.1)

[JC001]

I haven’t come across this with unconstrained array types, but have encountered a case involving a constrained array inside a record. It turns out this is required by the ARM:

procedure Bnd is
   subtype ID is Integer range 1 .. 2;
   type Sequence is array (ID) of Integer;
   
   type Rec is record
      V1 : Float;
      V2 : Sequence;
      V3 : Boolean;
   end record;
   
   V : Rec;
begin -- Bnd
   for I in V.V2'Range loop
      case I is
      when 1 => null;
      when 2 => null;
      end case;
   end loop;
end Bnd;

Gnat 14.2.0 gives

bnd.adb:14:07: error: missing case values: -16#8000_0000# .. 0
bnd.adb:14:07: error: missing case values: 3 .. 16#7FFF_FFFF#
bnd.adb:14:12: error: bounds of "I" are not static, alternatives must cover base type

[Irvise]

AFAIK, I remember reading that doing case for Integer types always requires a default so as to ensure that any value that is not when, is also matched. This is required by the exhaustiveness requirement of case.

Now, as you have shown, this is correctly done with your examples, then, why is the compiler still complaining?

@sidisyom I believe in your third example, the compiler may be delaying the analysis of ranges to a later point during compilation and my be defaulting to the general rage of the base, bit representation of My_Type. Because of that, it complains that the bounds are not static and that ranges from -128 .. 0 and 4 .. 127 need to be covered by the default.

Something similar may be happening with Jeff’s example. Since it is a subtype, the compiler may not go deep enough into the analysis and may do a similar thing to the one explained above.

Maybe GNAT could be made smarter and/or the ARM could be made more loose with the requirement that the compiler proves that all cases are fulfilled…

Best,
Fer

[jere]

@JC001

It turns out this is required by the ARM

Out of curiosity, what is the RM section to look for this?

[Irvise]

@jere

Out of curiosity, what is the RM section to look for this?

5.4 Case Statements, 8/3 “If the type of the selecting_ expression is root_integer, universal_integer, or a descendant of a formal scalar type, then the case_statement shall have an others discrete_choice.” in the Ada 2022 RM.

Best regards,
Fer

[sidisyom]

Agreed, since it is able to determine the bounds in all other cases and generate a warning in the declaration with initial value, it should, in theory, have all the information it needs to decide on the exhaustiveness of the case.

But maybe, that’s more easily said that done..

Thanks.

[jere]

My guess is it has to do with the range <> part of the declaration of the array. Perhaps that allows it utilize My_Type'Base in some contexts, so it thinks it needs the others “in general”? Not sure, just thinking out loud.

[sidisyom]

Yeah, could be the implicit range context that causes this, the explicit one i.e. the YAB : Your_Array (1 .. 2); doesn’t seem to require this extended-coverage behaviour.

[jere]

I’m thinking null array objects like YAU : Your_Array(1..0) := (others => <>); would potentially require it maybe? I don’t know if it is related directly to this or not though. Though again, I’m not smart enough to know why it applies in some areas and not others.

[sidisyom]

Indeed! Though in some slightly different way.

So, given:

YAU : Your_Array (1..0) := [others => <>];

and

for I in YAU'Range loop
  case I is         
  when 1 => null;
  when 2 => null;
  end case;
end loop;

there’s one warning and two errors:

Changing the loop to:

for I in YAU'Range loop
  case I is         
  when 0 => null;      
  end case;
end loop;

results in:

(and setting the when to 1 it complains the maximum allowed value is 0)

[JC001]

@jere

what is the RM section to look for this?

I don’t remember, and a quick search in the ada-lang.io c.l.a. archive didn’t find the discussion. I think it was the intersection of several different things in the ARM, since it involves multiple concepts. If the object is not a record component, for example, you don’t get this error. ARM editor Brukhardt said the ARM requires the compiler to treat the loop index as non-static in this case.

[JC001]

@Irvise

5.4 Case Statements, 8/3 “If the type of the selecting_ expression is root_integer, universal_integer, or a descendant of a formal scalar type, then the case_statement shall have an others discrete_choice.” in the Ada 2022 RM.

Clearly not that (or at least not just that), since

procedure Bnd is
   subtype ID is Integer range 1 .. 2;
   type Sequence is array (ID) of Integer;

   V : Sequence;
begin -- Bnd
   for I in V'Range loop
      case I is
      when 1 => null;
      when 2 => null;
      end case;
   end loop;
end Bnd;

doesn’t result in the error.

[jere]

@sidisyom

Indeed! Though in some slightly different way.

So, given:

YAU : Your_Array (1..0) := [others => <>];

and

for I in YAU'Range loop
  case I is         
  when 1 => null;
  when 2 => null;
  end case;
end loop;

Sorry what I meant was because you can do null arrays like that, maybe there are rules requiring the evaluation of Your_Array’s index type as My_Type'Base instead of just My_Type in some contexts and it bleeds over into utilizing the case statement in what is an otherwise seemingly obvious boundary. My_Type'Base would require the others selection.

My thought process is “why would it require an others for that? Maybe the case statement is evaluating it as My_Type'Base instead, but why is that? Maybe because the range <> paired with no explicit indexes forces some rule making the evaluation consider that?”. It could be a wrong through process though.