Change semantics of abbreviated form of field conditions

[treiher]

Context and Problem Statement

The current semantics of conditions at message fields (without using a then-clause) seems to be confusing. A field definition of the form F : T if C adds the condition C to all incoming edges of F. Because of that semantic it is not possible to reference F in condition C, although F is syntactically mentioned before C. Here is a more complex example inspired by IPv4 packets:

package Test is

   type Length is range 5 .. 2**16 - 1 with Size => 16;
   type Address is mod 2**32;

   type M1 is
      message
         IHL : Length;
         Total_Length : Length
            then Source
               if Total_Length >= IHL * 4;
         Source : Address;
         Destination : Address
            then Options
               with Size => IHL * 32 - (Destination'Last - Message'First + 1);
         Options : Opaque
            then Payload
               with Size => Total_Length * 8 - (IHL * 32);
         Payload : Opaque;
      end message;

   type M2 is
      message
         IHL : Length;
         Total_Length : Length;
         Source : Address
            if Total_Length >= IHL * 4;
         Destination : Address;
         Options : Opaque
            with Size => IHL * 32 - (Destination'Last - Message'First + 1);
         Payload : Opaque
            with Size => Total_Length * 8 - (IHL * 32);
      end message;

   type M3 is
      message
         IHL : Length;
         Total_Length : Length
            if Total_Length >= IHL * 4;  -- error: undefined variable "Total_Length"
         Source : Address;
         Destination : Address;
         Options : Opaque
            with Size => IHL * 32 - (Destination'Last - Message'First + 1);
         Payload : Opaque
            with Size => Total_Length * 8 - (IHL * 32);
      end message;

end Test;

M1 shows the message specification in the regular form using then-clauses. In the current implementation, M2 is a semantically equivalent variant of M1 using the abbreviated forms for conditions and size aspects. M3 is invalid, as Total_Length is referenced in the incoming edge to Total_Length, although it seems to be the more intuitive way of adding the condition.

Considered Options

O1 Add field conditions to incoming edges of field (keep current implementation)

+ Consistent behavior of aspects and conditions in abbreviated form (i.e. for transforming the regular into the abbreviated form the with ... as well as if ... has to be moved to the subsequent field): A : T then B if C with Size => 8; B : Opaque; is equivalent to A : T; B : Opaque if C with Size => 8;.
− Being unable to reference field containing condition feels intuitive (cf. M2)

O2 Add field conditions to outgoing edges of field

+ More intuitive (cf. M3)
+ Allows adding conditions to last message field without then null (cf. TLS Alert)

Decision Outcome

O2

[treiher]

I think changing the semantics (O2) would be worth the effort. The behavior is more intuitive and makes specifications clearer and easier understandable.

[senier]

I think changing the semantics (O2) would be worth the effort. The behavior is more intuitive and makes specifications clearer and easier understandable.

That's what we should do (as discussed separately)