Code generation for functions in sessions

[treiher]

Context and Problem Statement

Functions enable the execution of externally defined code in the session state machine. For each function declaration in the session specification a formal procedure declaration is added to the corresponding generic session package. The return type and parameters of a function are represented by the first and subsequent parameters of the generated procedure declaration. The set of allowed parameter and return types has a high impact on the code generation. Scalar types as parameters and return type are essential and simple to support. Further potential parameter and return types will be described in the following.

Considered Options

O1 Opaque type as parameter

+ Required to allow externally defined operations on byte arrays (e.g., encryption/decryption)
− Copying potentially necessary when represented by Ada array

O2 Opaque type as return value

− Not representable by single out parameter if length of array is not fixed

O3 Message or sequence represented by context

− External function depends on generated code
− Incompatible to potential C binding
− Generic message/sequence packages need to be instantiated externally and passed into generic session package to allow use of type in formal subprogram declarations
− Sequence contexts and message contexts representing function parameters would need to be copied before passing them as argument, as sequence context must be writeable to allow iterating over sequence

O4 Message represented by Ada record

Each message context used as parameter or return type needs a corresponding record type and both must be transformable into the other.

+ Required for complex return values
− Restricted to messages with fixed size

Decision Outcome

O1 and O4.

For now support will be added for:

• Scalars as parameter and return types
• Opaque as parameter type
• Specific message types as return types (messages with fixed size consisting of opaque and scalar types)

For message types the following functionality needs to be added:

• Detection and size determination of messages with fixed size
• Generation of record type for messages with fixed size consisting of opaque and scalar types
• Generation of transformations of message contexts and records into the other
• Support for messages with bounded size and no optional fields

Future work:

• Support for messages as parameter types
• Support for messages containing sequences

[treiher]

O4 also requires an instantiation of (some) message types used in a function. Opaque as a parameter type will require to use a buffer type in the generated subprogram. This buffer type is provided by a generic package, which leads to the issue described in #659.

[treiher]

The current restriction to fixed-size messages is too limited for the intended use case. For the TLS record layer we need to support messages with variable-sized opaque fields. It should be possible to loosen the restrictions and also support messages with bounded message size (no opaque field size depends on Message'Size) and no optional fields.