Skip to content

Commit

Permalink
Replace large postcondition of Reset_Dependent_Fields
Browse files Browse the repository at this point in the history 
For #806
  • Loading branch information
@kanigsson
kanigsson committed Oct 19, 2021
1 parent 225ebd0 commit 3b7a6e0
Show file tree
Hide file tree
Showing 16 changed files with 63 additions and 830 deletions.
68 changes: 35 additions & 33 deletions rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@
Expr,
ExpressionFunctionDeclaration,
First,
ForAllIn,
FormalDeclaration,
FormalSubprogramDeclaration,
FunctionSpecification,
Expand All @@ -47,6 +48,7 @@
Greater,
GreaterEqual,
If,
IfExpr,
IfStatement,
In,
Indexed,
Expand Down Expand Up @@ -2013,41 +2015,41 @@ def __create_reset_dependent_fields_procedure(message: Message) -> UnitPart:
),
]
],
Case(
Variable("Fld"),
Call(
"Invalid",
[
(
Variable(f.affixed_name),
And(
*[
Equal(
Indexed(
Variable("Ctx.Cursors"),
Variable(p.affixed_name),
),
Old(
Indexed(
Variable("Ctx.Cursors"),
Variable(p.affixed_name),
)
),
)
for p in message.predecessors(f)
],
*[
Call(
"Invalid",
[
Variable("Ctx"),
Variable(s.affixed_name),
],
)
for s in [f, *message.successors(f)]
],
),
)
for f in message.fields
Variable("Ctx"),
Variable(message.fields[0].affixed_name),
],
)
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"),
],
),
),
),
)
),
Expand Down
9 changes: 2 additions & 7 deletions tests/integration/parameterized_messages/generated/rflx-test-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,13 +132,8 @@ is
and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
and (case Fld is
when F_Data =>
Invalid (Ctx, F_Data)
and Invalid (Ctx, F_Extension),
when F_Extension =>
Ctx.Cursors (F_Data) = Ctx.Cursors (F_Data)'Old
and Invalid (Ctx, F_Extension))
and (for all F in Field =>
(if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F) else Invalid (Ctx, F)))
is
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Expand Down
15 changes: 2 additions & 13 deletions tests/spark/generated/rflx-derivation-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,19 +136,8 @@ is
and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
and (case Fld is
when F_Tag =>
Invalid (Ctx, F_Tag)
and Invalid (Ctx, F_Length)
and Invalid (Ctx, F_Value),
when F_Length =>
Ctx.Cursors (F_Tag) = Ctx.Cursors (F_Tag)'Old
and Invalid (Ctx, F_Length)
and Invalid (Ctx, F_Value),
when F_Value =>
Ctx.Cursors (F_Tag) = Ctx.Cursors (F_Tag)'Old
and Ctx.Cursors (F_Length) = Ctx.Cursors (F_Length)'Old
and Invalid (Ctx, F_Value))
and (for all F in Field =>
(if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F) else Invalid (Ctx, F)))
is
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Expand Down
4 changes: 1 addition & 3 deletions tests/spark/generated/rflx-enumeration-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,9 +105,7 @@ is
and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
and (case Fld is
when F_Priority =>
Invalid (Ctx, F_Priority))
and Invalid (Ctx, F_Priority)
is
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Expand Down
59 changes: 2 additions & 57 deletions tests/spark/generated/rflx-ethernet-frame.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,63 +168,8 @@ is
and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
and (case Fld is
when F_Destination =>
Invalid (Ctx, F_Destination)
and Invalid (Ctx, F_Source)
and Invalid (Ctx, F_Type_Length_TPID)
and Invalid (Ctx, F_TPID)
and Invalid (Ctx, F_TCI)
and Invalid (Ctx, F_Type_Length)
and Invalid (Ctx, F_Payload),
when F_Source =>
Ctx.Cursors (F_Destination) = Ctx.Cursors (F_Destination)'Old
and Invalid (Ctx, F_Source)
and Invalid (Ctx, F_Type_Length_TPID)
and Invalid (Ctx, F_TPID)
and Invalid (Ctx, F_TCI)
and Invalid (Ctx, F_Type_Length)
and Invalid (Ctx, F_Payload),
when F_Type_Length_TPID =>
Ctx.Cursors (F_Destination) = Ctx.Cursors (F_Destination)'Old
and Ctx.Cursors (F_Source) = Ctx.Cursors (F_Source)'Old
and Invalid (Ctx, F_Type_Length_TPID)
and Invalid (Ctx, F_TPID)
and Invalid (Ctx, F_TCI)
and Invalid (Ctx, F_Type_Length)
and Invalid (Ctx, F_Payload),
when F_TPID =>
Ctx.Cursors (F_Destination) = Ctx.Cursors (F_Destination)'Old
and Ctx.Cursors (F_Source) = Ctx.Cursors (F_Source)'Old
and Ctx.Cursors (F_Type_Length_TPID) = Ctx.Cursors (F_Type_Length_TPID)'Old
and Invalid (Ctx, F_TPID)
and Invalid (Ctx, F_TCI)
and Invalid (Ctx, F_Type_Length)
and Invalid (Ctx, F_Payload),
when F_TCI =>
Ctx.Cursors (F_Destination) = Ctx.Cursors (F_Destination)'Old
and Ctx.Cursors (F_Source) = Ctx.Cursors (F_Source)'Old
and Ctx.Cursors (F_Type_Length_TPID) = Ctx.Cursors (F_Type_Length_TPID)'Old
and Ctx.Cursors (F_TPID) = Ctx.Cursors (F_TPID)'Old
and Invalid (Ctx, F_TCI)
and Invalid (Ctx, F_Type_Length)
and Invalid (Ctx, F_Payload),
when F_Type_Length =>
Ctx.Cursors (F_Destination) = Ctx.Cursors (F_Destination)'Old
and Ctx.Cursors (F_Source) = Ctx.Cursors (F_Source)'Old
and Ctx.Cursors (F_Type_Length_TPID) = Ctx.Cursors (F_Type_Length_TPID)'Old
and Ctx.Cursors (F_TPID) = Ctx.Cursors (F_TPID)'Old
and Ctx.Cursors (F_TCI) = Ctx.Cursors (F_TCI)'Old
and Invalid (Ctx, F_Type_Length)
and Invalid (Ctx, F_Payload),
when F_Payload =>
Ctx.Cursors (F_Destination) = Ctx.Cursors (F_Destination)'Old
and Ctx.Cursors (F_Source) = Ctx.Cursors (F_Source)'Old
and Ctx.Cursors (F_Type_Length_TPID) = Ctx.Cursors (F_Type_Length_TPID)'Old
and Ctx.Cursors (F_TPID) = Ctx.Cursors (F_TPID)'Old
and Ctx.Cursors (F_TCI) = Ctx.Cursors (F_TCI)'Old
and Ctx.Cursors (F_Type_Length) = Ctx.Cursors (F_Type_Length)'Old
and Invalid (Ctx, F_Payload))
and (for all F in Field =>
(if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F) else Invalid (Ctx, F)))
is
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Expand Down
4 changes: 1 addition & 3 deletions tests/spark/generated/rflx-expression-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,9 +116,7 @@ is
and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
and (case Fld is
when F_Payload =>
Invalid (Ctx, F_Payload))
and Invalid (Ctx, F_Payload)
is
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Expand Down
9 changes: 2 additions & 7 deletions tests/spark/generated/rflx-fixed_size-simple_message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,13 +123,8 @@ is
and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
and (case Fld is
when F_Message_Type =>
Invalid (Ctx, F_Message_Type)
and Invalid (Ctx, F_Data),
when F_Data =>
Ctx.Cursors (F_Message_Type) = Ctx.Cursors (F_Message_Type)'Old
and Invalid (Ctx, F_Data))
and (for all F in Field =>
(if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F) else Invalid (Ctx, F)))
is
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Expand Down
Loading

0 comments on commit 3b7a6e0

Please sign in to comment.