Skip to content

Commit

Permalink
Simplify code after removal of Predecessor Field
Browse files Browse the repository at this point in the history 
* Remove some now useless assignments
* simplify Reset_Dependent_Fields code
  • Loading branch information
@kanigsson
kanigsson committed Sep 25, 2023
1 parent e7a0a30 commit f6bb751
Show file tree
Hide file tree
Showing 30 changed files with 232 additions and 714 deletions.
5 changes: 4 additions & 1 deletion rflx/generator/common.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -924,14 +924,17 @@ def unchanged_cursor_before_or_invalid(
limit: Expr,
loop_entry: bool,
or_invalid: bool = True,
including_limit: bool = False,
) -> Expr:
return ForAllIn(
"F",
Variable("Field"),
IfExpr(
[
(
Less(Variable("F"), limit),
LessEqual(Variable("F"), limit)
if including_limit
else Less(Variable("F"), limit),
Equal(
Indexed(
Variable("Ctx.Cursors"),
Expand Down
7 changes: 6 additions & 1 deletion rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -581,8 +581,13 @@ def _create_message(self, message: Message) -> dict[ID, Unit]: # noqa: PLR0912
message_generator.create_successor_function,
self._prefix,
message,
sequence_fields,
),
self._executor.submit(
message_generator.create_invalid_successor_function,
message,
SerializerGenerator.requires_set_procedure(message),
),
self._executor.submit(message_generator.create_invalid_successor_function, message),
self._executor.submit(message_generator.create_valid_next_function, message),
self._executor.submit(
message_generator.create_available_space_function,
Expand Down
203 changes: 84 additions & 119 deletions rflx/generator/message.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@
Length,
Less,
LessEqual,
LoopEntry,
Max,
Mod,
NamedAggregate,
Expand Down Expand Up @@ -78,7 +79,6 @@
SubprogramBody,
SubprogramDeclaration,
SubprogramVariant,
Succ,
UnitPart,
UseTypeClause,
ValueRange,
Expand Down Expand Up @@ -2220,7 +2220,16 @@ def condition(field: Field, message: Message) -> Expr:
)


def create_successor_function(prefix: str, message: Message) -> UnitPart:
def create_successor_function(
prefix: str,
message: Message,
sequence_fields: abc.Mapping[Field, Type],
) -> UnitPart:
if (
len(sequence_fields) == 0
and len([t for t in message.field_types.values() if isinstance(t, (Opaque, Sequence))]) == 0
):
return UnitPart()
specification = FunctionSpecification(
"Successor",
"Virtual_Field",
Expand All @@ -2229,57 +2238,60 @@ def create_successor_function(prefix: str, message: Message) -> UnitPart:

return UnitPart(
[],
[
# Eng/RecordFlux/Workarounds#31
Pragma("Warnings", [Variable("Off"), String("precondition is always False")]),
ExpressionFunctionDeclaration(
specification,
Case(
Variable("Fld"),
[
(
Variable(f.affixed_name),
If(
[
(
l.condition.substituted(
common.substitution(message, prefix),
common.wrap_warning(
[
ExpressionFunctionDeclaration(
specification,
Case(
Variable("Fld"),
[
(
Variable(f.affixed_name),
If(
[
(
l.condition.substituted(
common.substitution(message, prefix),
)
.simplified()
.ada_expr(),
Variable(l.target.affixed_name),
)
.simplified()
.ada_expr(),
Variable(l.target.affixed_name),
)
for l in message.outgoing(f)
],
Variable(INITIAL.affixed_name),
for l in message.outgoing(f)
],
Variable(INITIAL.affixed_name),
),
)
for f in message.fields
],
),
[
Precondition(
And(
Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
Call(
prefix * message.identifier * "Well_Formed",
[Variable("Ctx"), Variable("Fld")],
),
Call(
prefix * message.identifier * "Valid_Next",
[Variable("Ctx"), Variable("Fld")],
),
),
)
for f in message.fields
),
],
),
[
Precondition(
And(
Call(prefix * message.identifier * "Has_Buffer", [Variable("Ctx")]),
Call(
prefix * message.identifier * "Well_Formed",
[Variable("Ctx"), Variable("Fld")],
),
Call(
prefix * message.identifier * "Valid_Next",
[Variable("Ctx"), Variable("Fld")],
),
),
),
],
),
Pragma("Warnings", [Variable("On"), String("precondition is always False")]),
],
],
[
# Eng/RecordFlux/Workarounds#31
"precondition is always False",
],
),
)


def create_invalid_successor_function(message: Message) -> UnitPart:
if len(message.fields) == 1:
def create_invalid_successor_function(message: Message, requires_set_procedure: bool) -> UnitPart:
if len(message.fields) == 1 or not requires_set_procedure:
return UnitPart()

specification = FunctionSpecification(
Expand Down Expand Up @@ -2759,11 +2771,11 @@ def create_reset_dependent_fields_procedure(prefix: str, message: Message) -> Un
field_location_invariant = And(
Equal(
Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
Variable("First"),
LoopEntry(Call("Field_First", [Variable("Ctx"), Variable("Fld")])),
),
Equal(
Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
Variable("Size"),
LoopEntry(Call("Field_Size", [Variable("Ctx"), Variable("Fld")])),
),
)

Expand All @@ -2772,69 +2784,36 @@ def create_reset_dependent_fields_procedure(prefix: str, message: Message) -> Un
[
SubprogramBody(
specification,
[],
[
ObjectDeclaration(
["First"],
const.TYPES_BIT_LENGTH,
Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
constant=True,
aspects=[Ghost()],
),
ObjectDeclaration(
["Size"],
const.TYPES_BIT_LENGTH,
Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
constant=True,
aspects=[Ghost()],
),
],
[
PragmaStatement("Assert", [field_location_invariant]),
*(
[]
if len(message.fields) == 1
else [
ForIn(
"Fld_Loop",
ValueRange(Succ("Field", Variable("Fld")), Last("Field")),
ForIn(
"Fld_Loop",
ValueRange(Variable("Fld"), Last("Field")),
[
PragmaStatement("Loop_Invariant", [field_location_invariant]),
PragmaStatement(
"Loop_Invariant",
[
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Variable("Fld_Loop"),
),
NamedAggregate(
("State", Variable("S_Invalid")),
("others", Variable("<>")),
),
),
PragmaStatement("Loop_Invariant", [field_location_invariant]),
PragmaStatement(
"Loop_Invariant",
[
common.unchanged_cursor_before_or_invalid(
Variable("Fld_Loop"),
loop_entry=True,
),
],
common.unchanged_cursor_before_or_invalid(
Variable("Fld_Loop"),
loop_entry=True,
including_limit=True,
),
],
reverse=True,
),
]
),
PragmaStatement("Assert", [field_location_invariant]),
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Variable("Fld"),
),
NamedAggregate(
("State", Variable("S_Invalid")),
("others", Variable("<>")),
),
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Variable("Fld_Loop"),
),
NamedAggregate(
("State", Variable("S_Invalid")),
("others", Variable("<>")),
),
),
],
reverse=True,
),
PragmaStatement("Assert", [field_location_invariant]),
],
[
Precondition(
Expand All @@ -2848,20 +2827,6 @@ def create_reset_dependent_fields_procedure(prefix: str, message: Message) -> Un
Postcondition(
And(
Call("Valid_Next", [Variable("Ctx"), Variable("Fld")]),
Call(
"Invalid",
[Indexed(Variable("Ctx.Cursors"), Variable("Fld"))],
),
*(
[
Call(
"Invalid_Successor",
[Variable("Ctx"), Variable("Fld")],
),
]
if len(message.fields) > 1
else []
),
*common.context_invariant(message),
*[
Equal(e, Old(e))
Expand Down
21 changes: 0 additions & 21 deletions rflx/generator/parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -347,27 +347,6 @@ def create_verify_procedure(
else set_context_cursor_scalar()
if scalar_fields and not composite_fields
else set_context_cursor_composite_field("Fld"),
*(
[
# Eng/RecordFlux/RecordFlux#664
# The provability of the context predicate is increased by splitting the
# assignment into multiple statements.
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Call(
"Successor",
[Variable("Ctx"), Variable("Fld")],
),
),
NamedAggregate(
("others", Variable("<>")),
),
),
]
if len(message.fields) > 1
else []
),
]

return UnitPart(
Expand Down
14 changes: 1 addition & 13 deletions rflx/generator/serializer.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -321,19 +321,6 @@ def set_context_cursor(field_type: CursorState) -> Assignment:
],
[set_context_cursor(CursorState.WELL_FORMED)],
),
Assignment(
Indexed(
Variable("Ctx.Cursors"),
Call(
"Successor",
[Variable("Ctx"), Variable("Fld")],
),
),
NamedAggregate(
("State", Variable("S_Invalid")),
("others", Variable("<>")),
),
),
PragmaStatement(
"Assert",
[
Expand Down Expand Up @@ -510,6 +497,7 @@ def set_context_cursor(field_type: CursorState) -> Assignment:
Variable("Fld"),
loop_entry=False,
or_invalid=False,
including_limit=False,
),
]
if len(message.fields) > 1
Expand Down
20 changes: 7 additions & 13 deletions tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,6 @@ is
RFLX.Test.Message.Valid_Next (Ctx, Fld),
Post =>
Valid_Next (Ctx, Fld)
and Invalid (Ctx.Cursors (Fld))
and Ctx.Buffer_First = Ctx.Buffer_First'Old
and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
and Ctx.First = Ctx.First'Old
Expand All @@ -114,18 +113,14 @@ is
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
and Invalid (Ctx, F_Data)
is
First : constant RFLX_Types.Bit_Length := Field_First (Ctx, Fld) with
Ghost;
Size : constant RFLX_Types.Bit_Length := Field_Size (Ctx, Fld) with
Ghost;
begin
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
Ctx.Cursors (Fld) := (State => S_Invalid, others => <>);
pragma Assert (Field_First (Ctx, Fld) = First
and Field_Size (Ctx, Fld) = Size);
for Fld_Loop in reverse Fld .. Field'Last loop
pragma Loop_Invariant (Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Loop_Entry
and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Loop_Entry);
pragma Loop_Invariant ((for all F in Field =>
(if F <= Fld_Loop then Ctx.Cursors (F) = Ctx.Cursors'Loop_Entry (F) else Invalid (Ctx, F))));
Ctx.Cursors (Fld_Loop) := (State => S_Invalid, others => <>);
end loop;
end Reset_Dependent_Fields;

function Composite_Field (Unused_Fld : Field) return Boolean is
Expand Down Expand Up @@ -238,7 +233,6 @@ is
else
Ctx.Cursors (Fld) := (State => S_Well_Formed, First => First, Last => Last, Value => Val);
end if;
Ctx.Cursors (Successor (Ctx, Fld)) := (State => S_Invalid, others => <>);
pragma Assert (Last = (Field_First (Ctx, Fld) + Size) - 1);
end Set;

Expand Down
Loading

0 comments on commit f6bb751

Please sign in to comment.