Skip to content

Commit

Permalink
Improve code generation for Reset_Dependent_Fields
Browse files Browse the repository at this point in the history 
Use a loop rather than case statement + explicit assignments to
reset the fields.

Closes #840
  • Loading branch information
@kanigsson
kanigsson committed Nov 10, 2021
1 parent dd4eb1b commit d5d10fe
Show file tree
Hide file tree
Showing 43 changed files with 516 additions and 1,560 deletions.
34 changes: 34 additions & 0 deletions rflx/ada.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -771,6 +771,20 @@ def precedence(self) -> Precedence:
return Precedence.LITERAL


class Succ(Expr):
def __init__(self, type_identifier: StrID, expression: Expr) -> None:
super().__init__()
self.type_identifier = ID(type_identifier)
self.expression = expression

def _update_str(self) -> None:
self._str = intern(f"{self.type_identifier}'Succ ({self.expression})")

@property
def precedence(self) -> Precedence:
raise NotImplementedError


class QualifiedExpr(Expr):
def __init__(self, type_identifier: StrID, expression: Expr) -> None:
super().__init__()
Expand Down Expand Up @@ -1596,6 +1610,26 @@ def __str__(self) -> str:
return f"for {self.identifier} of {reverse}{self.iterator} loop\n{statements}\nend loop;"


class ForIn(Statement):
def __init__(
self,
identifier: StrID,
iterator: Expr,
statements: Sequence[Statement],
reverse: bool = False,
) -> None:
assert len(statements) > 0
self.identifier = identifier
self.iterator = iterator
self.statements = statements
self.reverse = reverse

def __str__(self) -> str:
statements = indent("\n".join(str(s) for s in self.statements), 3)
reverse = "reverse " if self.reverse else ""
return f"for {self.identifier} in {reverse}{self.iterator} loop\n{statements}\nend loop;"


class Declare(Statement):
def __init__(
self, declarations: Sequence[Declaration], statements: Sequence[Statement]
Expand Down
162 changes: 86 additions & 76 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@
Call,
CallStatement,
Case,
CaseStatement,
Component,
Constrained,
ContextItem,
Expand All @@ -40,6 +39,7 @@
ExpressionFunctionDeclaration,
First,
ForAllIn,
ForIn,
FormalDeclaration,
FormalSubprogramDeclaration,
FunctionSpecification,
Expand All @@ -59,6 +59,7 @@
Length,
Less,
LessEqual,
LoopEntry,
Mod,
ModularType,
NamedAggregate,
Expand Down Expand Up @@ -99,6 +100,7 @@
SubprogramBody,
SubprogramDeclaration,
SubprogramUnitPart,
Succ,
Unit,
UnitPart,
UsePackageClause,
Expand Down Expand Up @@ -1900,22 +1902,48 @@ def __create_reset_dependent_fields_procedure(message: Message) -> UnitPart:
"Reset_Dependent_Fields",
[InOutParameter(["Ctx"], "Context"), Parameter(["Fld"], "Field")],
)
field_location_invariant = And(
Equal(
Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
Variable("First"),
),
Equal(
Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
Variable("Size"),
),
)

field_location_invariant = PragmaStatement(
"Assert",
[
And(
Equal(
Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
Variable("First"),
),
Equal(
Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
Variable("Size"),
def unchanged_before_or_invalid(limit: Expr, loop_entry: bool) -> Expr:
return ForAllIn(
"F",
Variable("Field"),
IfExpr(
[
(
Less(Variable("F"), limit),
Equal(
Indexed(
Variable("Ctx.Cursors"),
Variable("F"),
),
Indexed(
LoopEntry(Variable("Ctx.Cursors"))
if loop_entry
else Old(Variable("Ctx.Cursors")),
Variable("F"),
),
),
)
],
Call(
"Invalid",
[
Variable("Ctx"),
Variable("F"),
],
),
)
],
)
),
)

return UnitPart(
[],
Expand All @@ -1939,49 +1967,58 @@ def __create_reset_dependent_fields_procedure(message: Message) -> UnitPart:
),
],
[
field_location_invariant,
CaseStatement(
Variable("Fld"),
[
(
Variable(f.affixed_name),
ty.cast(ty.List[Statement], [])
+ [
PragmaStatement("Assert", [field_location_invariant]),
*(
[]
if len(message.fields) == 1
else [
ForIn(
"F_Loop",
ValueRange(Succ("Field", Variable("Fld")), Last("Field")),
[
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Variable(s.affixed_name),
Variable("F_Loop"),
),
Aggregate(
Variable("S_Invalid"),
Variable(FINAL.affixed_name),
),
)
for s in reversed(message.successors(f))
]
+ [
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Variable(f.affixed_name),
),
Aggregate(
Variable("S_Invalid"),
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable(f.affixed_name),
),
"Predecessor",
),
),
)
]
+ [field_location_invariant],
),
PragmaStatement(
"Loop_Invariant", [field_location_invariant]
),
PragmaStatement(
"Loop_Invariant",
[
unchanged_before_or_invalid(
Variable("F_Loop"), loop_entry=True
)
],
),
],
reverse=True,
)
for f in message.fields
],
]
),
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Variable("Fld"),
),
Aggregate(
Variable("S_Invalid"),
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable("Fld"),
),
"Predecessor",
),
),
),
PragmaStatement("Assert", [field_location_invariant]),
],
[
Precondition(
Expand Down Expand Up @@ -2033,34 +2070,7 @@ def __create_reset_dependent_fields_procedure(message: Message) -> UnitPart:
],
)
if len(message.fields) == 1
else ForAllIn(
"F",
Variable("Field"),
IfExpr(
[
(
Less(Variable("F"), Variable("Fld")),
Equal(
Indexed(
Variable("Ctx.Cursors"),
Variable("F"),
),
Indexed(
Old(Variable("Ctx.Cursors")),
Variable("F"),
),
),
)
],
Call(
"Invalid",
[
Variable("Ctx"),
Variable("F"),
],
),
),
),
else unchanged_before_or_invalid(Variable("Fld"), loop_entry=False),
)
),
],
Expand Down
61 changes: 10 additions & 51 deletions tests/integration/messages/generated/rflx-universal-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -184,57 +184,16 @@ is
begin
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
case Fld is
when F_Message_Type =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, F_Final);
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, F_Final);
Ctx.Cursors (F_Message_Type) := (S_Invalid, Ctx.Cursors (F_Message_Type).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Length =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, F_Final);
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, Ctx.Cursors (F_Length).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Data =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, F_Final);
Ctx.Cursors (F_Data) := (S_Invalid, Ctx.Cursors (F_Data).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Option_Types =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Types) := (S_Invalid, Ctx.Cursors (F_Option_Types).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Options =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, F_Final);
Ctx.Cursors (F_Options) := (S_Invalid, Ctx.Cursors (F_Options).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Value =>
Ctx.Cursors (F_Values) := (S_Invalid, F_Final);
Ctx.Cursors (F_Value) := (S_Invalid, Ctx.Cursors (F_Value).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Values =>
Ctx.Cursors (F_Values) := (S_Invalid, Ctx.Cursors (F_Values).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
end case;
for F_Loop in reverse Field'Succ (Fld) .. Field'Last loop
Ctx.Cursors (F_Loop) := (S_Invalid, F_Final);
pragma Loop_Invariant (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
pragma Loop_Invariant ((for all F in Field =>
(if F < F_Loop then Ctx.Cursors (F) = Ctx.Cursors'Loop_Entry (F) else Invalid (Ctx, F))));
end loop;
Ctx.Cursors (Fld) := (S_Invalid, Ctx.Cursors (Fld).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
end Reset_Dependent_Fields;

function Composite_Field (Fld : Field) return Boolean is
Expand Down
27 changes: 10 additions & 17 deletions tests/integration/messages/generated/rflx-universal-option.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,23 +146,16 @@ is
begin
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
case Fld is
when F_Option_Type =>
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, F_Final);
Ctx.Cursors (F_Option_Type) := (S_Invalid, Ctx.Cursors (F_Option_Type).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Length =>
Ctx.Cursors (F_Data) := (S_Invalid, F_Final);
Ctx.Cursors (F_Length) := (S_Invalid, Ctx.Cursors (F_Length).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
when F_Data =>
Ctx.Cursors (F_Data) := (S_Invalid, Ctx.Cursors (F_Data).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
end case;
for F_Loop in reverse Field'Succ (Fld) .. Field'Last loop
Ctx.Cursors (F_Loop) := (S_Invalid, F_Final);
pragma Loop_Invariant (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
pragma Loop_Invariant ((for all F in Field =>
(if F < F_Loop then Ctx.Cursors (F) = Ctx.Cursors'Loop_Entry (F) else Invalid (Ctx, F))));
end loop;
Ctx.Cursors (Fld) := (S_Invalid, Ctx.Cursors (Fld).Predecessor);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
end Reset_Dependent_Fields;

function Composite_Field (Fld : Field) return Boolean is
Expand Down
Loading

0 comments on commit d5d10fe

Please sign in to comment.