RecordFlux
RecordFlux copied to clipboard
AdaCore
Mapping values of two scalar types
Context and Problem Statement
In protocols the values of two scalar types sometimes have to be mapped onto / converted into each other in a way that cannot be done by a calculation. The most prominent example are algorithms selected in a protocol session which result in response messages of different lengths:
package Test is
type Alg is (Alg1, -- 1 byte response
Alg2, -- 2 byte response
Alg3) -- 4 byte response
with Size => 8;
type Len is mod 2 ** 16;
type Request is
message
Alg : Alg;
end message;
type Response (Len : Len) is
message
Data : Opaque
with Size => 8 * Len;
end message;
generic
Transport : Channel with Readable, Writable;
session S with
Initial => Receive,
Final => Done
is
Request : Request;
Response : Response;
begin
state Receive is
begin
Transport'Read (Request);
transition
goto Done
if Request'Valid /= True
goto Prepare_Response
end Receive;
state Prepare_Response
is
begin
Response := Response'(Len => 1, -- FIXME: Depends on Request.Alg
Data => [1]);
transition
goto Send_Response
exception
goto Done
end Prepare_Response;
state Send_Response is
begin
Transport'Write (Response);
transition
goto Done
end Send_Response;
state Done is null state;
end S;
end Test;
Use Cases
- Determine size of
DIGESTSresponse based on selected hash algorithm in SPDM protocol (7.4)
Considered Options
O1
Use states to select the corresponding value:
generic
Transport : Channel with Readable, Writable;
session S with
Initial => Receive,
Final => Done
is
Request : Request;
Response : Response;
Len : Len;
begin
state Receive is
begin
Transport'Read (Request);
transition
goto Done
if Request'Valid /= True
goto Set_Alg1_Length
if Request.Alg = Alg1
goto Set_Alg2_Length
if Request.Alg = Alg2
goto Set_Alg3_Length
if Request.Alg = Alg3
goto Prepare_Response
end Receive;
state Set_Alg1_Length is
begin
Len := 1;
transition
goto Prepare_Response
end Set_Alg1_Length;
state Set_Alg2_Length is
begin
Len := 2;
transition
goto Prepare_Response
end Set_Alg2_Length;
state Set_Alg3_Length is
begin
Len := 4;
transition
goto Prepare_Response
end Set_Alg3_Length;
state Prepare_Response
is
begin
Response := Response'(Len => Len,
Data => [1]);
transition
goto Send_Response
exception
goto Done
end Prepare_Response;
state Send_Response is
begin
Transport'Write (Response);
transition
goto Done
end Send_Response;
state Done is null state;
end S;
+ No changes required − Very verbose − Potentially many additional states − Totality not enforced
O2
Use sequences and list comprehension:
generic
Transport : Channel with Readable, Writable;
session S with
Initial => Receive,
Final => Done
is
Request : Request;
Response : Response;
begin
state Receive is
begin
Transport'Read (Request);
transition
goto Done
if Request'Valid /= True
goto Prepare_Response
end Receive;
state Prepare_Response
is
Maps : Maps;
Lens : Maps;
Sel : Map;
begin
Maps'Append (Map'(Alg => Alg1, Len => 1));
Maps'Append (Map'(Alg => Alg2, Len => 2));
Maps'Append (Map'(Alg => Alg3, Len => 4));
Lens := [for M in Maps if M.Alg = Request.Alg => M];
Sel := Lens'Head;
Response := Response'(Len => Sel.Len,
Data => [1]);
transition
goto Send_Response
exception
goto Done
end Prepare_Response;
state Send_Response is
begin
Transport'Write (Response);
transition
goto Done
end Send_Response;
state Done is null state;
end S;
+ No changes required − Convoluted syntax − Inefficient code (space and time) − Intent is not conveyed clearly in specification − Totality not enforced
O3
Introduce case expression:
generic
Transport : Channel with Readable, Writable;
session S with
Initial => Receive,
Final => Done
is
Request : Request;
Response : Response;
begin
state Receive is
begin
Transport'Read (Request);
transition
goto Done
if Request'Valid /= True
goto Prepare_Response
end Receive;
state Prepare_Response
is
begin
Response := Response'(Len => (case Request.Alg is
when Alg1 => 1,
when Alg2 => 2,
when Alg3 => 4),
Data => [1]);
transition
goto Send_Response
exception
goto Done
end Prepare_Response;
state Send_Response is
begin
Transport'Write (Response);
transition
goto Done
end Send_Response;
state Done is null state;
end S;
+ Concise + Conveys the intent clearly + Totality can be enforced + Probably easy to transform to SPARK − Somewhat redundant to existing state transitions − Inefficient when same mapping is required in multiple places − Reusability questionable
O4
Use external function:
generic
Transport : Channel with Readable, Writable;
with function Alg_Len (Alg : Alg) return Len;
session S with
Initial => Receive,
Final => Done
is
Request : Request;
Response : Response;
begin
state Receive is
begin
Transport'Read (Request);
transition
goto Done
if Request'Valid /= True
goto Prepare_Response
end Receive;
state Prepare_Response
is
Len : Len;
Alg : Alg;
begin
Alg := Request.Alg;
Len := Alg_Len (Alg);
Response := Response'(Len => Len,
Data => [1]);
transition
goto Send_Response
exception
goto Done
end Prepare_Response;
state Send_Response is
begin
Transport'Write (Response);
transition
goto Done
end Send_Response;
state Done is null state;
end S;
+ Concise + No changes required − Intent is not conveyed in specification at all − Totality not enforced − Code changes may break specification − Proof may become hard or impossible
O5
Introduce a dedicated mapping type (concrete syntax to be defined):
package Test is
type Alg is (Alg1, -- 1 byte response
Alg2, -- 2 byte response
Alg3) -- 4 byte response
with Size => 8;
type Len is mod 2 ** 16;
type Alg_Len is map (Alg) of Len;
type Request is
message
Alg : Alg;
end message;
type Response (Len : Len) is
message
Data : Opaque
with Size => 8 * Len;
end message;
generic
Transport : Channel with Readable, Writable;
session S with
Initial => Receive,
Final => Done
is
Request : Request;
Response : Response;
Alg_Len : Alg_Len := (Alg1 => 1, Alg2 => 2, Alg3 => 4);
begin
state Receive is
begin
Transport'Read (Request);
transition
goto Done
if Request'Valid /= True
goto Prepare_Response
end Receive;
state Prepare_Response
is
begin
Response := Response'(Len => Alg_Len (Request.Alg),
Data => [1]);
transition
goto Send_Response
exception
goto Done
end Prepare_Response;
state Send_Response is
begin
Transport'Write (Response);
transition
goto Done
end Send_Response;
state Done is null state;
end S;
end Test;
+ Concise + Intent conveyed clearly + Potentially easy to translate into SPARK (using arrays) + Totality can be enforced + Efficient − Reusability questionable
O6
Introduce expression functions and case expressions:
package Test is
type Alg is (Alg1, -- 1 byte response
Alg2, -- 2 byte response
Alg3) -- 4 byte response
with Size => 8;
type Len is mod 2 ** 16;
function Alg_Len (Alg : Alg) return Len is (case Alg is
when Alg1 => 1,
when Alg2 => 2,
when Alg3 => 4);
type Request is
message
Alg : Alg;
end message;
type Response (Len : Len) is
message
Data : Opaque
with Size => 8 * Len;
end message;
generic
Transport : Channel with Readable, Writable;
session S with
Initial => Receive,
Final => Done
is
Request : Request;
Response : Response;
begin
state Receive is
begin
Transport'Read (Request);
transition
goto Done
if Request'Valid /= True
goto Prepare_Response
end Receive;
state Prepare_Response
is
begin
Response := Response'(Len => Alg_Len (Request.Alg),
Data => [1]);
transition
goto Send_Response
exception
goto Done
end Prepare_Response;
state Send_Response is
begin
Transport'Write (Response);
transition
goto Done
end Send_Response;
state Done is null state;
end S;
end Test;
+ Concise + Intent conveyed clearly + Totality can be enforced + Efficient + Reusable + Expressive − May be overkill for problem to solve
O7a
Introduce a dedicated mapping type:
package Test is
type Alg is (Alg1, -- 1 byte response
Alg2, -- 2 byte response
Alg3) -- 4 byte response
with Size => 8;
type Len is mod 2 ** 16;
for Alg use mapping Alg_Len to Len is (Alg1 => 1,
Alg2 => 2,
Alg3 => 4);
end Test;
O7b
Introduce a dedicated mapping type:
package Test is
type Alg is (Alg1, -- 1 byte response
Alg2, -- 2 byte response
Alg3) -- 4 byte response
with Size => 8;
type Len is mod 2 ** 16;
mapping Alg_Len (Alg) to Len is
(Alg1 => 1,
Alg2 => 2,
Alg3 => 4);
end Test;
+ Concise + Intent conveyed clearly + Potentially easy to translate into SPARK (using arrays) + Totality can be enforced + Efficient − Not reusable − Unusual syntax − Two new keywords for one new feature
Decision Outcome
O6
FWIW, the list comprehension syntax does not match that provided by Ada 2022 "filters" -- filters use "when M.Alg = Request_Alg" rather than "if ...", hence "[for M in Maps when M.Alg = Request.Alg => M];" This also might not produce exactly one result.
The "dedicated mapping type" could use Ada 2022 syntax for container aggregates (these use "[...]" rather than "(...)") and Ada 2012 syntax for indexing and be supported by SPARK directly. Not sure what you mean by "reusability" concerns.
A simple array aggregate would seem to be the simplest, however, in that that provides totality and efficiency.
@sttaft Thanks for your input!
FWIW, the list comprehension syntax does not match that provided by Ada 2022 "filters" -- filters use "when M.Alg = Request_Alg" rather than "if ...", hence "[for M in Maps when M.Alg = Request.Alg => M];" This also might not produce exactly one result.
We actually changed syntax for list comprehensions in the meantime to be more consistent to Ada 2022 (cf. #702), although we decided to still deviate by using the if keyword instead of when. when would have been a new keyword for the RecordFlux language, and we did not see a good reason for introducing when just for comprehensions.
The "dedicated mapping type" could use Ada 2022 syntax for container aggregates (these use "[...]" rather than "(...)") and Ada 2012 syntax for indexing and be supported by SPARK directly. Not sure what you mean by "reusability" concerns.
The concern is that we are adding this new language construct just for this very specific issue. I think newly added feature should ideally cover multiple use cases.
A simple array aggregate would seem to be the simplest, however, in that that provides totality and efficiency.
Do you propose adding an array type similar to Ada? That is not yet part of the language, but we could certainly consider it as an option.
