Skip to content

Commit

Permalink
Test separation of proof generation from proofs
Browse files Browse the repository at this point in the history 
Ref. #625
  • Loading branch information
Alexander Senier committed Aug 25, 2021
1 parent cc41042 commit 7f38fb5
Show file tree
Hide file tree
Showing 3 changed files with 142 additions and 96 deletions.
227 changes: 132 additions & 95 deletions rflx/model/message.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1474,51 +1474,145 @@ def __prove_overlays(self) -> None:
)

def __prove_field_positions(self) -> None:
for f in (*self.fields, FINAL):
for path in self.paths(f):
def proofs() -> List[
List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]]
]:
# pylint: disable=too-many-locals
results = []
for f in (*self.fields, FINAL):
for path in self.paths(f):
last = path[-1]
negative = expr.Less(
self.__target_size(last), expr.Number(0), last.size.location
)
start = expr.GreaterEqual(
self.__target_first(last),
expr.First("Message"),
last.source.identifier.location,
)

last = path[-1]
negative = expr.Less(self.__target_size(last), expr.Number(0), last.size.location)
start = expr.GreaterEqual(
self.__target_first(last), expr.First("Message"), last.location
)
facts = [fact for link in path for fact in self.__link_expression(link)]

facts = [fact for link in path for fact in self.__link_expression(link)]
outgoing = self.outgoing(f)
if f != FINAL and outgoing:
facts.append(
expr.Or(
*[o.condition for o in outgoing], location=f.identifier.location
)
)

outgoing = self.outgoing(f)
if f != FINAL and outgoing:
facts.append(
expr.Or(*[o.condition for o in outgoing], location=f.identifier.location)
)
facts.extend(self.type_constraints(negative))
facts.extend(self.type_constraints(start))

facts.extend(self.type_constraints(negative))
facts.extend(self.type_constraints(start))
proof = expr.TRUE.check(facts)

proof = expr.TRUE.check(facts)
# Only check positions of reachable paths
if proof.result != expr.ProofResult.SAT:
continue

# Only check positions of reachable paths
if proof.result != expr.ProofResult.SAT:
continue
result: List[
Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]
] = []

proof = negative.check(facts)
if proof.result != expr.ProofResult.UNSAT:
error = RecordFluxError()
path_message = " -> ".join([l.target.name for l in path])
self.error.extend(
[
(
f'negative size for field "{f.name}" ({path_message})',
error.append(
f'negative size for field "{f.name}" ({path_message})',
Subsystem.MODEL,
Severity.ERROR,
f.identifier.location,
)
result.append((negative, facts, expr.ProofResult.UNSAT, error, False))

error = RecordFluxError()
path_message = " -> ".join([last.target.name for last in path])
error.append(
f'negative start for field "{f.name}" ({path_message})',
Subsystem.MODEL,
Severity.ERROR,
self.identifier.location,
)
result.append((start, facts, expr.ProofResult.SAT, error, True))

if f in self.types:
t = self.types[f]
if isinstance(t, mty.Opaque):
element_size = t.element_size
start_aligned = expr.Not(
expr.Equal(
expr.Mod(self.__target_first(last), element_size),
expr.Number(1),
last.location,
)
)

error = RecordFluxError()
path_message = " -> ".join([p.target.name for p in path])
error.append(
f'opaque field "{f.name}" not aligned to {element_size} '
f"bit boundary ({path_message})",
Subsystem.MODEL,
Severity.ERROR,
f.identifier.location,
)
],
)
return
result.append(
(
start_aligned,
[
*facts,
*self.message_constraints(),
*self.type_constraints(start_aligned),
],
expr.ProofResult.UNSAT,
error,
False,
)
)

proof = start.check(facts)
if proof.result != expr.ProofResult.SAT:
path_message = " -> ".join([last.target.name for last in path])
self.error.extend(
is_multiple_of_element_size = expr.Not(
expr.Equal(
expr.Mod(self.__target_size(last), element_size),
expr.Number(0),
last.location,
)
)

error = RecordFluxError()
path_message = " -> ".join([p.target.name for p in path])
error.append(
f'size of opaque field "{f.name}" not multiple of {element_size}'
f" bit ({path_message})",
Subsystem.MODEL,
Severity.ERROR,
f.identifier.location,
)
result.append(
(
is_multiple_of_element_size,
[
*facts,
*self.message_constraints(),
*self.type_constraints(is_multiple_of_element_size),
],
expr.ProofResult.UNSAT,
error,
False,
),
)
results.append(result)
return results

def check(
proofs: List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]]
) -> RecordFluxError:
result = RecordFluxError()
for goal, facts, expected, error, unsat in proofs:
proof = goal.check(facts)
if proof.result == expected:
continue
result.extend(error)
if unsat:
result.extend(
[
(
f'negative start for field "{f.name}" ({path_message})',
Expand All @@ -1532,70 +1626,13 @@ def __prove_field_positions(self) -> None:
],
]
)
return

if f in self.types:
t = self.types[f]
if not isinstance(t, mty.Opaque):
continue
element_size = t.element_size
start_aligned = expr.Not(
expr.Equal(
expr.Mod(self.__target_first(last), element_size),
expr.Number(1),
last.location,
)
)
proof = start_aligned.check(
[
*facts,
*self.message_constraints(),
*self.type_constraints(start_aligned),
]
)
if proof.result != expr.ProofResult.UNSAT:
path_message = " -> ".join([p.target.name for p in path])
self.error.extend(
[
(
f'opaque field "{f.name}" not aligned to {element_size} bit'
f" boundary ({path_message})",
Subsystem.MODEL,
Severity.ERROR,
f.identifier.location,
)
],
)
return
break
return result

is_multiple_of_element_size = expr.Not(
expr.Equal(
expr.Mod(self.__target_size(last), element_size),
expr.Number(0),
last.location,
)
)
proof = is_multiple_of_element_size.check(
[
*facts,
*self.message_constraints(),
*self.type_constraints(is_multiple_of_element_size),
]
)
if proof.result != expr.ProofResult.UNSAT:
path_message = " -> ".join([p.target.name for p in path])
self.error.extend(
[
(
f'size of opaque field "{f.name}" not multiple of'
f" {element_size} bit ({path_message})",
Subsystem.MODEL,
Severity.ERROR,
f.identifier.location,
)
],
)
return
errors = map(check, proofs())
for e in errors:
self.error.extend(e)
self.error.propagate()

def __prove_message_size(self) -> None:
"""
Expand Down
6 changes: 6 additions & 0 deletions tests/ide/ide_test.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,12 @@ def test_multiple_errors() -> None:
f'{path}:250:19: model: error: undefined variable "F1"',
f"{path}:250:19: model: info: on path F1",
f'{path}:257:18: model: error: negative size for field "F2" (F1 -> F2)',
f'{path}:254:9: model: error: negative start for field "Final" (F1 -> F2 -> Final)',
f"{path}:257:18: model: info: unsatisfied \"F2'Last ="
" (F1'Last + 1 + (F1 - 2**33)) - 1\"",
f"{path}:256:10: model: info: unsatisfied \"F1'Last = (Message'First + 32) - 1\"",
f'{path}:199:9: model: info: unsatisfied "F1 < 2**32"',
f"{path}:260:10: model: info: unsatisfied \"F2'Last + 1 >= Message'First\"",
f'{path}:266:10: model: error: unconstrained field "F1" without size aspect',
f'{path}:271:9: model: error: field "F3" not congruent with overlaid field "F1"',
f"{path}:271:9: model: info: unsatisfied \"F1'First = Message'First\"",
Expand Down
5 changes: 4 additions & 1 deletion tests/unit/model/message_test.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1744,7 +1744,10 @@ def test_field_after_message_start(monkeypatch: ty.Any) -> None:
types,
r"^"
r'model: error: negative start for field "F2" [(]F1 -> F2[)]\n'
r'model: info: unsatisfied "Message\'First - 1000 >= Message\'First"'
r'model: info: unsatisfied "Message\'First - 1000 >= Message\'First"\n'
r'model: error: negative start for field "Final" [(]F1 -> F2 -> Final[)]\n'
r'model: info: unsatisfied "F2\'Last = [(]Message\'First - 1000 [+] 8[)] - 1"\n'
r'model: info: unsatisfied "F2\'Last [+] 1 >= Message\'First"'
r"$",
)

Expand Down

0 comments on commit 7f38fb5

Please sign in to comment.