Skip to content

Commit

Permalink
Parallelize remaining (suitable) verification functions
Browse files Browse the repository at this point in the history 
Ref. #625
  • Loading branch information
@senier
Alexander Senier authored and senier committed Aug 25, 2021
1 parent 9d7ff74 commit 4929554
Show file tree
Hide file tree
Showing 2 changed files with 112 additions and 93 deletions.
203 changes: 110 additions & 93 deletions rflx/model/message.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -691,25 +691,28 @@ def add(
facts: List[expr.Expr],
expected: expr.ProofResult,
message: RecordFluxError,
unexpected: bool = False,
negate: bool = False,
add_unsat: bool = False,
) -> None:
self.current.append((goal, facts, expected, message, unexpected, add_unsat))
# pylint: disable=too-many-arguments
self.current.append((goal, facts, expected, message, negate, add_unsat))

def pop(self) -> None:
def push(self) -> None:
if self.current:
self.proofs.append(copy(self.current))
self.current.clear()

@classmethod
def check_proof(
cls,
argument: List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]],
argument: List[
Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool, bool]
],
) -> RecordFluxError:
result = RecordFluxError()
for goal, facts, expected, message, unexpected, add_unsat in argument:
for goal, facts, expected, message, negate, add_unsat in argument:
proof = goal.check(facts)
if unexpected == (proof.result != expected):
if negate == (proof.result != expected):
continue
result.extend(message)
if add_unsat:
Expand All @@ -722,7 +725,7 @@ def check_proof(
return result

def check(self, error: RecordFluxError) -> None:
self.pop()
self.push()
with ProcessPoolExecutor() as executor:
for e in executor.map(ParallelProofs.check_proof, self.proofs):
error.extend(e)
Expand Down Expand Up @@ -1287,39 +1290,48 @@ def valid_upper(expression: expr.Expr) -> bool:
)

def __prove_conflicting_conditions(self) -> None:
proofs = ParallelProofs()
for f in (INITIAL, *self.fields):
for i1, c1 in enumerate(self.outgoing(f)):
for i2, c2 in enumerate(self.outgoing(f)):
if i1 < i2:
conflict = expr.And(c1.condition, c2.condition)
proof = conflict.check(self.type_constraints(conflict))
if proof.result == expr.ProofResult.SAT:
c1_message = str(c1.condition).replace("\n", " ")
c2_message = str(c2.condition).replace("\n", " ")
self.error.extend(
[
(
f'conflicting conditions for field "{f.name}"',
Subsystem.MODEL,
Severity.ERROR,
f.identifier.location,
),
(
f"condition {i1} ({f.identifier} ->"
f" {c1.target.identifier}): {c1_message}",
Subsystem.MODEL,
Severity.INFO,
c1.condition.location,
),
(
f"condition {i2} ({f.identifier} ->"
f" {c2.target.identifier}): {c2_message}",
Subsystem.MODEL,
Severity.INFO,
c2.condition.location,
),
],
)
error = RecordFluxError()
c1_message = str(c1.condition).replace("\n", " ")
c2_message = str(c2.condition).replace("\n", " ")
error.extend(
[
(
f'conflicting conditions for field "{f.name}"',
Subsystem.MODEL,
Severity.ERROR,
f.identifier.location,
),
(
f"condition {i1} ({f.identifier} ->"
f" {c1.target.identifier}): {c1_message}",
Subsystem.MODEL,
Severity.INFO,
c1.condition.location,
),
(
f"condition {i2} ({f.identifier} ->"
f" {c2.target.identifier}): {c2_message}",
Subsystem.MODEL,
Severity.INFO,
c2.condition.location,
),
],
)
proofs.add(
conflict,
self.type_constraints(conflict),
expr.ProofResult.SAT,
error,
negate=True,
)
proofs.push()
proofs.check(self.error)

def __prove_reachability(self) -> None:
def has_final(field: Field) -> bool:
Expand Down Expand Up @@ -1446,6 +1458,7 @@ def __prove_coverage(self) -> None:
effectively pruning the range that this field covers from the bit range of the message. For
the overall expression, prove that it is false for all f, i.e. no bits are left.
"""
proofs = ParallelProofs()
for path in [p[:-1] for p in self.paths(FINAL) if p]:

facts: Sequence[expr.Expr]
Expand Down Expand Up @@ -1478,54 +1491,53 @@ def __prove_coverage(self) -> None:
facts.extend([f for l in path for f in self.__link_expression(l)])

# Coverage expression must be False, i.e. no bits left
proof = expr.TRUE.check(facts)
if proof.result == expr.ProofResult.SAT:
self.error.extend(
[
error = RecordFluxError()
error.extend(
[
(
"path does not cover whole message",
Subsystem.MODEL,
Severity.ERROR,
self.identifier.location,
),
*[
(
"path does not cover whole message",
f'on path: "{l.target.identifier}"',
Subsystem.MODEL,
Severity.ERROR,
self.identifier.location,
),
*[
(
f'on path: "{l.target.identifier}"',
Subsystem.MODEL,
Severity.INFO,
l.target.identifier.location,
)
for l in path
],
]
)
return
Severity.INFO,
l.target.identifier.location,
)
for l in path
],
]
)
proofs.add(expr.TRUE, facts, expr.ProofResult.SAT, error, negate=True)
proofs.check(self.error)

def __prove_overlays(self) -> None:
proofs = ParallelProofs()
for f in (INITIAL, *self.fields):
for p, l in [(p, p[-1]) for p in self.paths(f) if p]:
if l.first != expr.UNDEFINED and isinstance(l.first, expr.First):
facts = [f for l in p for f in self.__link_expression(l)]
overlaid = expr.Equal(
self.__target_last(l), expr.Last(l.first.prefix), l.location
)
proof = overlaid.check(facts)
if proof.result != expr.ProofResult.SAT:
self.error.extend(
[
(
f'field "{f.name}" not congruent with'
f' overlaid field "{l.first.prefix}"',
Subsystem.MODEL,
Severity.ERROR,
self.identifier.location,
),
*[
(f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, l)
for m, l in proof.error
],
]
)
error = RecordFluxError()
error.extend(
[
(
f'field "{f.name}" not congruent with'
f' overlaid field "{l.first.prefix}"',
Subsystem.MODEL,
Severity.ERROR,
self.identifier.location,
)
],
)
proofs.add(overlaid, facts, expr.ProofResult.SAT, error, add_unsat=True)
proofs.push()
proofs.check(self.error)

def __prove_field_positions(self) -> None:
# pylint: disable=too-many-locals
Expand Down Expand Up @@ -1652,13 +1664,14 @@ def __prove_field_positions(self) -> None:
expr.ProofResult.UNSAT,
error,
)
proofs.pop()
proofs.push()
proofs.check(self.error)

def __prove_message_size(self) -> None:
"""
Prove that all message paths lead to a message with a size that is a multiple of 8 bit.
"""
proofs = ParallelProofs()
type_constraints = self.type_constraints(expr.TRUE)
field_size_constraints = [
expr.Equal(expr.Mod(expr.Size(f.name), expr.Number(8)), expr.Number(0))
Expand All @@ -1679,27 +1692,31 @@ def __prove_message_size(self) -> None:
*type_constraints,
*field_size_constraints,
]
proof = expr.NotEqual(expr.Mod(message_size, expr.Number(8)), expr.Number(0)).check(
facts
error = RecordFluxError()
error.extend(
[
(
"message size must be multiple of 8 bit",
Subsystem.MODEL,
Severity.ERROR,
self.identifier.location,
),
(
"on path " + " -> ".join(l.target.name for l in path),
Subsystem.MODEL,
Severity.INFO,
self.identifier.location,
),
],
)
if proof.result == expr.ProofResult.SAT:
self.error.extend(
[
(
"message size must be multiple of 8 bit",
Subsystem.MODEL,
Severity.ERROR,
self.identifier.location,
),
(
"on path " + " -> ".join(l.target.name for l in path),
Subsystem.MODEL,
Severity.INFO,
self.identifier.location,
),
],
)
return
proofs.add(
expr.NotEqual(expr.Mod(message_size, expr.Number(8)), expr.Number(0)),
facts,
expr.ProofResult.SAT,
error,
negate=True,
)
proofs.check(self.error)

def __prove_path_property(self, prop: expr.Expr, path: Sequence[Link]) -> expr.Proof:
conditions = [l.condition for l in path if l.condition != expr.TRUE]
Expand Down
2 changes: 2 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,8 @@ 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}:257:18: model: error: size of opaque field "
f'"F2" not multiple of 8 bit (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\"",
Expand Down

0 comments on commit 4929554

Please sign in to comment.