Skip to content

Commit

Permalink
Improve provability of generated code
Browse files Browse the repository at this point in the history 
Ref. #659
  • Loading branch information
@treiher
treiher authored and Isabell Zorr committed Jun 29, 2021
1 parent f2e0aeb commit 85b3929
Show file tree
Hide file tree
Showing 13 changed files with 196 additions and 28 deletions.
14 changes: 10 additions & 4 deletions rflx/ada.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1382,15 +1382,21 @@ def __init__(
self,
control_expression: Expr,
case_statements: Sequence[Tuple[Expr, Sequence[Statement]]],
case_grouping: bool = True,
) -> None:
self.control_expression = control_expression
self.case_statements = case_statements
self.case_grouping = case_grouping

def __str__(self) -> str:
grouped_cases = [
(" | ".join(str(c) for c, _ in choices), statements)
for statements, choices in itertools.groupby(self.case_statements, lambda x: x[1])
]
grouped_cases = (
[
(" | ".join(str(c) for c, _ in choices), statements)
for statements, choices in itertools.groupby(self.case_statements, lambda x: x[1])
]
if self.case_grouping
else [(str(case), statements) for case, statements in self.case_statements]
)
cases = "".join(
[
"\nwhen {} =>\n{}".format(choice, indent("\n".join(str(s) for s in statements), 3))
Expand Down
43 changes: 30 additions & 13 deletions rflx/generator/parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,20 @@ def create_verify_procedure(
),
)

set_message_last = Assignment(
Variable("Ctx.Message_Last"),
Mul(
Div(
Add(
Call("Field_Last", [Variable("Ctx"), Variable("Fld")]),
Number(7),
),
Number(8),
),
Number(8),
),
)

set_cursors_statements = [
*(
[
Expand Down Expand Up @@ -236,19 +250,22 @@ def create_verify_procedure(
if len(message.fields) > 1
else []
),
Assignment(
Variable("Ctx.Message_Last"),
Mul(
Div(
Add(
Call("Field_Last", [Variable("Ctx"), Variable("Fld")]),
Number(7),
),
Number(8),
),
Number(8),
),
),
# Componolit/RecordFlux#664:
# The provability of the context predicate is increased by duplicating the statement
# inside a case statement.
CaseStatement(
Variable("Fld"),
[
(
Variable(f.affixed_name),
[set_message_last],
)
for f in message.fields
],
case_grouping=False,
)
if len(message.fields) > 1
else set_message_last,
IfStatement(
[
(
Expand Down
9 changes: 8 additions & 1 deletion tests/spark/generated/rflx-derivation-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,14 @@ is
or Fld = F_Value
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Tag =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Value =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
17 changes: 16 additions & 1 deletion tests/spark/generated/rflx-ethernet-frame.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -341,7 +341,22 @@ is
Fld = F_Payload
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Destination =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Source =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Type_Length_TPID =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_TPID =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_TCI =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Type_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Payload =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
35 changes: 34 additions & 1 deletion tests/spark/generated/rflx-icmp-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -793,7 +793,40 @@ is
or Fld = F_Transmit_Timestamp
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Tag =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Code_Destination_Unreachable =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Code_Redirect =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Code_Time_Exceeded =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Code_Zero =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Checksum =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Gateway_Internet_Address =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Identifier =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Pointer =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Unused_32 =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Sequence_Number =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Unused_24 =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Originate_Timestamp =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Data =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Receive_Timestamp =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Transmit_Timestamp =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
13 changes: 12 additions & 1 deletion tests/spark/generated/rflx-ipv4-option.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,18 @@ is
or Fld = F_Option_Number
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Copied =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Option_Class =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Option_Number =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Option_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Option_Data =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
37 changes: 36 additions & 1 deletion tests/spark/generated/rflx-ipv4-packet.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -799,7 +799,42 @@ is
Fld = F_Payload
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Version =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_IHL =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_DSCP =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_ECN =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Total_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Identification =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Flag_R =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Flag_DF =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Flag_MF =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Fragment_Offset =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_TTL =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Protocol =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Header_Checksum =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Source =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Destination =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Options =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Payload =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
7 changes: 6 additions & 1 deletion tests/spark/generated/rflx-sequence-inner_message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,12 @@ is
Fld = F_Payload
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Payload =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
13 changes: 12 additions & 1 deletion tests/spark/generated/rflx-sequence-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,18 @@ is
Fld = F_AV_Enumeration_Vector
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Modular_Vector =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Range_Vector =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Enumeration_Vector =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_AV_Enumeration_Vector =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
7 changes: 6 additions & 1 deletion tests/spark/generated/rflx-sequence-messages_message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,12 @@ is
Fld = F_Messages
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Messages =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
7 changes: 6 additions & 1 deletion tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,12 @@ is
Fld = F_Vector
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Header =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Vector =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
9 changes: 8 additions & 1 deletion tests/spark/generated/rflx-tlv-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,14 @@ is
or Fld = F_Value
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Tag =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Value =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down
13 changes: 12 additions & 1 deletion tests/spark/generated/rflx-udp-datagram.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -258,7 +258,18 @@ is
Fld = F_Payload
then
Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
case Fld is
when F_Source_Port =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Destination_Port =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Length =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Checksum =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
when F_Payload =>
Ctx.Message_Last := ((Field_Last (Ctx, Fld) + 7) / 8) * 8;
end case;
if Composite_Field (Fld) then
Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
else
Expand Down

0 comments on commit 85b3929

Please sign in to comment.