Skip to content

Commit

Permalink
Prevent name conflicts between literals and field names
Browse files Browse the repository at this point in the history 
Ref. #329
  • Loading branch information
@treiher
treiher committed Jul 9, 2020
1 parent 1bdb0c1 commit 5163a97
Show file tree
Hide file tree
Showing 4 changed files with 67 additions and 55 deletions.
2 changes: 1 addition & 1 deletion generated/rflx-ipv4-generic_packet.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -279,7 +279,7 @@ is
when F_Destination =>
(case Fld is
when F_Payload =>
(Types.Bit_Length (Ctx.Cursors (F_Total_Length).Value.Total_Length_Value) * 8 + (((-Ctx.Cursors (F_Destination).Last) + Ctx.Cursors (F_Version).First - 1))),
(Types.Bit_Length (Ctx.Cursors (F_Total_Length).Value.Total_Length_Value) * 8 - Ctx.Cursors (F_Destination).Last + Ctx.Cursors (F_Version).First - 1),
when F_Options =>
(Types.Bit_Length (Ctx.Cursors (F_IHL).Value.IHL_Value) * 32 - 160),
when others =>
Expand Down
14 changes: 6 additions & 8 deletions rflx/generator/common.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -369,10 +369,10 @@ def valid_predecessors_invariant() -> Expr:
),
Variable(l.source.affixed_name),
),
l.condition,
)
.substituted(substitution(message, embedded=True))
.simplified()
l.condition.substituted(
substitution(message, embedded=True)
),
).simplified()
for l in message.incoming(f)
]
),
Expand Down Expand Up @@ -478,7 +478,7 @@ def valid_path_to_next_field_condition(message: Message, field: Field) -> Sequen
If(
[
(
l.condition,
l.condition.substituted(substitution(message, public=True)),
And(
Equal(
Call(
Expand All @@ -492,9 +492,7 @@ def valid_path_to_next_field_condition(message: Message, field: Field) -> Sequen
),
)
]
)
.substituted(substitution(message, public=True))
.simplified()
).simplified()
for l in message.outgoing(field)
if l.target != FINAL
]
Expand Down
84 changes: 38 additions & 46 deletions rflx/generator/core.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -822,7 +822,7 @@ def __create_take_buffer_procedure(context_invariant: Sequence[Expr]) -> UnitPar
def __create_path_condition_function(message: Message) -> UnitPart:
def condition(field: Field, message: Message) -> Expr:
cases: List[Tuple[Expr, Expr]] = [
(target, Or(*[c for _, c in conditions]))
(target, Or(*[c for _, c in conditions]).substituted(common.substitution(message)))
for target, conditions in itertools.groupby(
[
(Variable(l.target.affixed_name), l.condition)
Expand All @@ -834,9 +834,7 @@ def condition(field: Field, message: Message) -> Expr:
]
if set(message.fields) - {l.target for l in message.outgoing(field)}:
cases.append((Variable("others"), FALSE))
return (
Case(Variable("Fld"), cases).substituted(common.substitution(message)).simplified()
)
return Case(Variable("Fld"), cases).simplified()

specification = FunctionSpecification(
"Path_Condition",
Expand Down Expand Up @@ -886,28 +884,25 @@ def length(field: Field, message: Message) -> Expr:
if len(links) == 1:
length = links[0].length
elif len(links) > 1:
length = (
If(
[(l.condition, l.length) for l in links],
Variable(const.TYPES_UNREACHABLE_BIT_LENGTH),
)
.substituted(
common.substitution(message, target_type=const.TYPES_BIT_LENGTH)
)
.simplified()
length = If(
[(l.condition, l.length) for l in links],
Variable(const.TYPES_UNREACHABLE_BIT_LENGTH),
)
cases.append((Variable(target.affixed_name), length))
cases.append(
(
Variable(target.affixed_name),
length.substituted(
common.substitution(message, target_type=const.TYPES_BIT_LENGTH)
).simplified(),
)
)

if not cases:
return Number(0)

if set(message.fields) - {l.target for l in message.outgoing(field)}:
cases.append((Variable("others"), Variable(const.TYPES_UNREACHABLE_BIT_LENGTH)))
return (
Case(Variable("Fld"), cases)
.substituted(common.substitution(message, target_type=const.TYPES_BIT_LENGTH))
.simplified()
)
return Case(Variable("Fld"), cases).simplified()

specification = FunctionSpecification(
"Field_Length",
Expand Down Expand Up @@ -953,31 +948,27 @@ def first(field: Field, message: Message) -> Expr:
Number(1),
)

return (
If(
[
(
AndThen(
Equal(
Selected(
Indexed(Variable("Ctx.Cursors"), Variable("Fld")),
"Predecessor",
),
Variable(l.source.affixed_name),
return If(
[
(
AndThen(
Equal(
Selected(
Indexed(Variable("Ctx.Cursors"), Variable("Fld")),
"Predecessor",
),
l.condition,
Variable(l.source.affixed_name),
),
l.first.substituted(
lambda x: contiguous_first if x == UNDEFINED else x
),
)
for l in message.incoming(field)
],
Variable(const.TYPES_UNREACHABLE_BIT_LENGTH),
)
.substituted(common.substitution(message))
.simplified()
)
l.condition.substituted(common.substitution(message)),
),
l.first.substituted(
lambda x: contiguous_first if x == UNDEFINED else x
).substituted(common.substitution(message)),
)
for l in message.incoming(field)
],
Variable(const.TYPES_UNREACHABLE_BIT_LENGTH),
).simplified()

specification = FunctionSpecification(
"Field_First",
Expand Down Expand Up @@ -1135,13 +1126,14 @@ def __create_successor_function(message: Message) -> UnitPart:
Variable(f.affixed_name),
If(
[
(l.condition, Variable(l.target.affixed_name))
(
l.condition.substituted(common.substitution(message)),
Variable(l.target.affixed_name),
)
for l in message.outgoing(f)
],
Variable(INITIAL.affixed_name),
)
.substituted(common.substitution(message))
.simplified(),
).simplified(),
)
for f in message.fields
],
Expand Down
22 changes: 22 additions & 0 deletions tests/test_integration.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,3 +160,25 @@ def test_comparison_big_integers(condition: str) -> None:
end Test;
"""
)


def test_potential_name_conflicts_fields_literals() -> None:
assert_compilable_code_string(
"""
package Test is
type E is (F_A => 0, F_B => 1) with Size => 8;
type M is
message
A : E
then null
if A = F_A,
then B
if A = F_B;
B : E;
end message;
end Test;
"""
)

0 comments on commit 5163a97

Please sign in to comment.