Use of incomplete or partially invalid messages in sessions

[treiher]

Context and Problem Statement

Currently, it is possible to access fields of an incomplete or even partially invalid message, as only the validity of a single field is checked before the access. This might be an unexpected behavior.

Example

   type M is
      message
         A : T;
         B : T;
         C : T;
      end message;

      In_Msg : Messages::M;
   begin
      state Start is
      begin
         I'Read (In_Msg);
      transition
         goto Copy
            if In_Msg'Has_Data
         goto Terminated
      end Start;

      state Copy is
      begin
         Out_Msg := Messages::O'(A => In_Msg.A, B => In_Msg.B);
      transition
         goto Reply
      exception
         goto Terminated
      end Copy;

Copy will be reached and Out_Msg will be created without exception, even if In_Msg.C was missing or invalid during parsing.

Considered Options

O1 No implicit check for completeness of validity of message (current behavior)

+ Full flexibility − Potential unintentional use of an incomplete or partially invalid message

O2 Check completeness and validity of message implicitly after Read and transition to exception state in case of error

+ Prevents unintentional use of an incomplete or partially invalid message − Adds requirement for exception transition in all IO states containing Read

Decision Outcome

TBD

[treiher]

I think the implicit checking of completeness and validity of a message should be preferred (O2). I'm not aware of a use case where the current behavior would be required (O1).

[jklmnn]

I think this can be closed as the problem was addressed in https://github.com/Componolit/RecordFlux/issues/1067.

[treiher]

I think this can be closed as the problem was addressed in #1067.

I don't see how #1067 addresses the problem of this design ticket. With the implementation of #1067 we enabled the creation of incomplete messages. But while #1067 is about creating messages, this issue is about the validity of received messages. We have to decide if we want to allow using potentially incomplete or invalid messages after 'Read (O1) or if we want to add implicit validity checks after 'Read (O2).

[jklmnn]

I see. I initially thought this ticket was a result of the discussion if we wanted to allow the creation and usage of incomplete messages (e.g. to be used for signing).