Skip to content

Commit

Permalink
Fix contradiction and field position verification
Browse files Browse the repository at this point in the history 
The fix for #277 was actually not proper, as any contradiction would
be flagged as an error. However, as long as there is at least one
non-contradictory path, we cannot treat a field condition as
contradictory.

This problem occurred in the test, but was not discovered as the test
was missing a error.propagate() call after message construction. This
was noticed when making Message constructors raise exceptions again in
the discussion of #285.

Ref. #248
  • Loading branch information
@treiher
Alexander Senier authored and treiher committed Jul 23, 2020
1 parent 579729f commit d09a8e5
Show file tree
Hide file tree
Showing 2 changed files with 87 additions and 61 deletions.
103 changes: 65 additions & 38 deletions rflx/model.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -928,37 +928,45 @@ def has_final(field: Field) -> bool:

def __prove_contradictions(self) -> None:
for f in (INITIAL, *self.fields):
contradictions = []
paths = 0
for path in self._state.paths[f]:
facts = [fact for link in path for fact in self.__link_expression(link)]
for c in self.outgoing(f):
paths += 1
contradiction = c.condition
constraints = self.__type_constraints(contradiction)
proof = contradiction.check([*constraints, *facts])
if proof.result == ProofResult.unsat:
self.error.append(
f'contradicting condition in "{self.identifier}"',
Subsystem.MODEL,
Severity.ERROR,
c.condition.location,
)
self.error.extend(
[
(
f'on path "{l.target.identifier}"',
Subsystem.MODEL,
Severity.INFO,
l.target.identifier.location,
)
for l in path
]
)
self.error.extend(
[
(f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, l)
for m, l in proof.error
]
)
return
if proof.result == ProofResult.sat:
continue

contradictions.append((path, c.condition, proof.error))

if paths == len(contradictions):
for path, cond, errors in sorted(contradictions):
self.error.append(
f'contradicting condition in "{self.identifier}"',
Subsystem.MODEL,
Severity.ERROR,
cond.location,
)
self.error.extend(
[
(
f'on path: "{l.target.identifier}"',
Subsystem.MODEL,
Severity.INFO,
l.target.identifier.location,
)
for l in path
]
)
self.error.extend(
[
(f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, l)
for m, l in errors
]
)

@staticmethod
def __target_first(link: Link) -> Expr:
Expand Down Expand Up @@ -1001,14 +1009,33 @@ def __link_expression(self, link: Link) -> Sequence[Expr]:
]

def __prove_field_positions(self) -> None:
for f in self.fields:
for p, l in [(p, p[-1]) for p in self._state.paths[f] if p]:
positive = GreaterEqual(self.__target_length(l), Number(0), l.length.location)
facts = [f for l in p for f in self.__link_expression(l)]
for f in (*self.fields, FINAL):
for path in self._state.paths[f]:

last = path[-1]
positive = GreaterEqual(self.__target_length(last), Number(0), last.length.location)
start = GreaterEqual(self.__target_first(last), First("Message"), last.location)

facts = [fact for link in path for fact in self.__link_expression(link)]

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

facts.extend(self.__type_constraints(positive))
facts.extend(self.__type_constraints(start))

proof = TRUE.check(facts)

# Only check positions of reachable paths
if proof.result != ProofResult.sat:
continue

proof = positive.check(facts)
if proof.result != ProofResult.sat:
path_message = " -> ".join([l.target.name for l in p])
path_message = " -> ".join([l.target.name for l in path])
self.error.append(
f'negative length for field "{f.name}" ({path_message})',
Subsystem.MODEL,
Expand All @@ -1017,16 +1044,15 @@ def __prove_field_positions(self) -> None:
)
self.error.extend(
[
(f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, l)
for m, l in proof.error
(f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, locn)
for m, locn in proof.error
]
)
return

start = GreaterEqual(self.__target_first(l), First("Message"), l.location)
facts.extend(self.__type_constraints(start))
proof = start.check(facts)
if proof.result != ProofResult.sat:
path_message = " -> ".join([l.target.name for l in p])
path_message = " -> ".join([last.target.name for last in path])
self.error.append(
f'negative length for field "{f.name}" ({path_message})',
Subsystem.MODEL,
Expand All @@ -1035,10 +1061,11 @@ def __prove_field_positions(self) -> None:
)
self.error.extend(
[
(f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, l)
for m, l in proof.error
(f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, locn)
for m, locn in proof.error
]
)
return

def __prove_coverage(self) -> None:
"""
Expand Down Expand Up @@ -1093,7 +1120,7 @@ def __prove_coverage(self) -> None:
self.error.extend(
[
(
f'on path "{l.target.identifier}"',
f'on path: "{l.target.identifier}"',
Subsystem.MODEL,
Severity.INFO,
l.target.identifier.location,
Expand Down
45 changes: 22 additions & 23 deletions tests/test_verification.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,7 @@ def test_invalid_path_1(monkeypatch: Any) -> None:
types,
r"^"
r'<stdin>:5:10: model: error: contradicting condition in "P.M"\n'
r'<stdin>:20:10: model: info: on path "F1"\n'
r'<stdin>:20:10: model: info: on path: "F1"\n'
r'<stdin>:5:10: model: info: unsatisfied "1 = 2"',
)

Expand All @@ -219,17 +219,15 @@ def test_invalid_path_2(monkeypatch: Any) -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "F1"\n'
r'model: info: on path: "F1"\n'
r'model: info: unsatisfied "1 = 2"',
)


def test_contradiction() -> None:
structure = [
Link(INITIAL, Field("F1")),
Link(Field("F1"), Field("F2"), condition=Equal(Number(1), Number(2))),
Link(Field("F1"), Field("F2"), condition=Less(Variable("F1"), Number(50))),
Link(Field("F1"), FINAL, condition=Greater(Variable("F1"), Number(60))),
Link(Field("F1"), Field("F2"), condition=Greater(Variable("F1"), Number(1000))),
Link(Field("F2"), FINAL),
]
types = {
Expand All @@ -241,8 +239,9 @@ def test_contradiction() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "F1"\n'
r'model: info: unsatisfied "1 = 2"',
r'model: info: on path: "F1"\n'
r'model: info: unsatisfied "F1 <= 100"\n'
r'model: info: unsatisfied "F1 > 1000"',
)


Expand All @@ -261,7 +260,7 @@ def test_invalid_type_condition_range_low() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "F1"\n'
r'model: info: on path: "F1"\n'
r'model: info: unsatisfied "F1 >= 1"\n'
r'model: info: unsatisfied "F1 < 1"',
)
Expand All @@ -282,7 +281,7 @@ def test_invalid_type_condition_range_high() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "F1"\n'
r'model: info: on path: "F1"\n'
r'model: info: unsatisfied "F1 <= 100"\n'
r'model: info: unsatisfied "F1 > 200"',
)
Expand All @@ -303,7 +302,7 @@ def test_invalid_type_condition_modular_upper() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "F1"\n'
r'model: info: on path: "F1"\n'
r'model: info: unsatisfied "F1 < 256"\n'
r'model: info: unsatisfied "F1 > 65537"',
)
Expand All @@ -324,7 +323,7 @@ def test_invalid_type_condition_modular_lower() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "F1"\n'
r'model: info: on path: "F1"\n'
r'model: info: unsatisfied "F1 >= 0"\n'
r'model: info: unsatisfied "F1 < 0"',
)
Expand Down Expand Up @@ -564,8 +563,8 @@ def test_field_coverage_1(monkeypatch: Any) -> None:
types,
r"^"
r"model: error: path does not cover whole message\n"
r'model: info: on path "F1"\n'
r'model: info: on path "F2"'
r'model: info: on path: "F1"\n'
r'model: info: on path: "F2"'
r"$",
)

Expand Down Expand Up @@ -597,10 +596,10 @@ def test_field_coverage_2(monkeypatch: Any) -> None:
types,
r"^"
r"model: error: path does not cover whole message\n"
r'model: info: on path "F1"\n'
r'model: info: on path "F2"\n'
r'model: info: on path "F3"\n'
r'model: info: on path "F4"'
r'model: info: on path: "F1"\n'
r'model: info: on path: "F2"\n'
r'model: info: on path: "F3"\n'
r'model: info: on path: "F4"'
r"$",
)

Expand Down Expand Up @@ -969,7 +968,7 @@ def test_aggregate_equal_invalid_length1() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "Magic"\n'
r'model: info: on path: "Magic"\n'
r'model: info: unsatisfied "2 [*] 8 = Magic\'Length"\n'
r'model: info: unsatisfied "Magic\'Length = 40"',
)
Expand All @@ -992,7 +991,7 @@ def test_aggregate_equal_invalid_length2() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "Magic"\n'
r'model: info: on path: "Magic"\n'
r'model: info: unsatisfied "2 [*] 8 = Magic\'Length"\n'
r'model: info: unsatisfied "Magic\'Length = 40"',
)
Expand Down Expand Up @@ -1032,7 +1031,7 @@ def test_aggregate_inequal_invalid_length() -> None:
types,
r"^"
r'model: error: contradicting condition in "P.M"\n'
r'model: info: on path "Magic"\n'
r'model: info: on path: "Magic"\n'
r'model: info: unsatisfied "2 [*] 8 = Magic\'Length"\n'
r'model: info: unsatisfied "Magic\'Length = 40"',
)
Expand Down Expand Up @@ -1076,7 +1075,7 @@ def test_aggregate_equal_array_invalid_length() -> None:
types,
r"^"
r'<stdin>:17:3: model: error: contradicting condition in "P.M"\n'
r'<stdin>:3:5: model: info: on path "Magic"\n'
r'<stdin>:3:5: model: info: on path: "Magic"\n'
r'<stdin>:17:3: model: info: unsatisfied "2 [*] Modular\'Length = Magic\'Length"\n'
r'<stdin>:66:3: model: info: unsatisfied "Modular\'Length = 7"\n'
r'<stdin>:19:17: model: info: unsatisfied "Magic\'Length = 40"',
Expand Down Expand Up @@ -1110,8 +1109,8 @@ def test_aggregate_equal_invalid_length_field() -> None:
types,
r"^"
r'<stdin>:10:5: model: error: contradicting condition in "P.M"\n'
r'<stdin>:2:5: model: info: on path "Length"\n'
r'<stdin>:3:5: model: info: on path "Magic"\n'
r'<stdin>:2:5: model: info: on path: "Length"\n'
r'<stdin>:3:5: model: info: on path: "Magic"\n'
r'<stdin>:10:5: model: info: unsatisfied "2 [*] 8 = Magic\'Length"\n'
r'<stdin>:5:10: model: info: unsatisfied "Length >= 10"\n'
r'<stdin>:6:5: model: info: unsatisfied "Magic\'Length = 8 [*] Length"',
Expand Down

0 comments on commit d09a8e5

Please sign in to comment.