Check compile-time values for Size/Object_Size/Alignment in generic instances only

[yannickmoy]

Summary

Currently, Ada only allows specifying the Size/Object_Size/Alignment of types with static values. This makes it impossible to specify them in generics when they refer to values from formal parameters. So the following code is rejected:

--  bytes.ads
package Bytes is

   type U32 is mod 2**32;

   generic
      type Payload is private;
   function Extract (Data : Payload) return U32;

end Bytes;

--  bytes.adb
package body Bytes is

   function Extract (Data : Payload) return U32 is
      type Arr is array (1 .. Payload'Size / U32'Size) of U32
        with Size => (Payload'Size / U32'Size) * U32'Size;
      Data_Arr : Arr with Address => Data'Address;
      Res : U32 := 0;
   begin
      for Value of Data_Arr loop
         Res := Res + Value;
      end loop;
      return Res;
   end Extract;

end Bytes;

--  use_bytes.adb
with Bytes; use Bytes;

procedure Use_Bytes is

   type Rec is record
      A, B, C : Integer;
   end record;

   R : Rec := (0, 1, 41);

   function Extract_Rec is new Extract (Rec);
begin
   pragma Assert (Extract_Rec (R) = 42);
end Use_Bytes;

Even without generics, Ada only allows specifying static values for Size/Object_Size/Alignment. This makes it impossible to compute such a value based on the Size/Object_Size/Alignment of other types. So the following code is also rejected:

procedure Use_Bytes is

   type Rec is record
      A, B, C : Integer;
   end record;

   R : Rec := (0, 1, 41);

   type U32 is mod 2**32;
   subtype Payload is Rec;

   function Extract (Data : Payload) return U32 is
      type Arr is array (1 .. Payload'Size / U32'Size) of U32
        with Size => (Payload'Size / U32'Size) * U32'Size;
      Data_Arr : Arr with Address => Data'Address;
      Res : U32 := 0;
   begin
      for Value of Data_Arr loop
         Res := Res + Value;
      end loop;
      return Res;
   end Extract;

begin
   pragma Assert (Extract (R) = 42);
end Use_Bytes;

Motivation

Infrastructure software needs sometimes to interpret data through different types, without copying it. This can be done by overlaying a variable on top of another one, specifying the address of one for the other, like in the examples above. Given that the type system of Ada does not guard against reading too little or too much data here, it would be safer to specify the intended Size/Object_Size/Alignment of the overlay. This is also needed for the SPARK tool to be able to verify statically that the overlay does not allow reading past the overlaid object.

Caveats and alternatives

The alternative if to not specify the representation attributes of such types, and let the compiler decide, but check them with the GNAT-specific pragma Compile_Time_Assert, as in:

pragma Compile_Time_Error (Arr'Size /= (Payload'Size / U32'Size) * U32'Size, "unexpected size for Arr");

Note that the semantics of this pragma are subtle, as it's not guaranteed to fail at compilation if the compiler frontend cannot determine statically the value of the expression. The SPARK tool takes a stricter approach and issues a message if it cannot determine that the expression is always False. This would be the outcome currently (a message from SPARK tool), but possibly the tool could be modified to link that kind of assertions with the corresponding type, as a kind of heuristic replacement for the corresponding representation aspect or clause.

[QuentinOchem]

Thanks for submitting this one @yannickmoy ! I have had this issue as well a few times in the past. Here are some thoughts:

Specifically for the generic issue, could we have a way in Ada to specify that a generic parameter needs to be static? e.g.

generic
   Gen_Size : Integer with Static;
package Z is
   type T is range 0 .. 5 with Size => Gen_Size;
end Z;

with regards to (Payload'Size / U32'Size) * U32'Size, isn't that a static expression? (so maybe we should also allow static expressions)?

[yannickmoy]

@QuentinOchem the ability to specify that a generic parameter is static seems different from this issue. And T'Size is a static expression only when T is a static scalar subtype, see http://www.ada-auth.org/standards/2xrm/html/RM-4-9.html

[yannickmoy]

A colleague pointed out that one can use Pack and Component_Size on type Arr, which is sufficient for the compiler to compute the Size of the type (at least if the implementation advice of Ada RM 13.3(73) is followed, which is the case in GNAT).

But this is not possible if array Arr (or a record) contains elements whose type is defined by a formal parameter of the generic. In that case, we'd like to express Component_Size again in terms of non-static expressions according to the Ada RM, which is rejected.

Thus, it seems worthwhile to make it possible to express all such representative clauses/aspects for Size/Object_Size/Component_Size/Alignment more liberally in a generic, provided the expression is statically known in the instance. This might be easier to do in a generic spec than in a generic body, according to Ada RM 12.3(11):

In a generic unit, Legality Rules are enforced at compile time of the generic_declaration and generic body, given the properties of the formals. In the visible part and formal part of an instance, Legality Rules are enforced at compile time of the generic_instantiation, given the properties of the actuals. In other parts of an instance, Legality Rules are not enforced; this rule does not apply when a given rule explicitly specifies otherwise.

This allows rules where we assume the best in a generic spec (because instance rechecking acts as a safety net if an optimistic guess turns out to be wrong) and conservatively assume the worst in a generic body (because there is no instance rechecking).