Issue 336: Underflow not detected for range length field

.isort.cfg

@@ -4,3 +4,4 @@ include_trailing_comma=True
 force_grid_wrap=0
 use_parentheses=True
 line_length=100
+known_third_party=icontract,pydotplus,pyparsing,pytest,z3

rflx/model.py

@@ -1012,11 +1012,9 @@ def get_constraints(aggregate: Aggregate, field: Variable) -> Sequence[Expr]:
             Equal(Mod(Length("Message"), Number(8)), Number(0)),
         ]
 
-        return (
-            message_constraints
-            + aggregate_constraints
-            + [c for n, t in scalar_types for c in t.constraints(name=n, proof=True)]
-        )
+        scalar_constraints = [c for n, t in scalar_types for c in t.constraints(name=n, proof=True)]
+
+        return [*message_constraints, *aggregate_constraints, *scalar_constraints]
 
     def __prove_conflicting_conditions(self) -> None:
         for f in (INITIAL, *self.fields):
@@ -1187,7 +1185,7 @@ def __prove_field_positions(self) -> None:
             for path in self._state.paths[f]:
 
                 last = path[-1]
-                positive = GreaterEqual(self.__target_length(last), Number(0), last.length.location)
+                negative = Less(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)]
@@ -1198,7 +1196,7 @@ def __prove_field_positions(self) -> None:
                         Or(*[o.condition for o in outgoing], location=f.identifier.location)
                     )
 
-                facts.extend(self.__type_constraints(positive))
+                facts.extend(self.__type_constraints(negative))
                 facts.extend(self.__type_constraints(start))
 
                 proof = TRUE.check(facts)
@@ -1207,28 +1205,22 @@ def __prove_field_positions(self) -> None:
                 if proof.result != ProofResult.sat:
                     continue
 
-                proof = positive.check(facts)
-                if proof.result != ProofResult.sat:
+                proof = negative.check(facts)
+                if proof.result != ProofResult.unsat:
                     path_message = " -> ".join([l.target.name for l in path])
                     self.error.append(
                         f'negative length for field "{f.name}" ({path_message})',
                         Subsystem.MODEL,
                         Severity.ERROR,
-                        self.identifier.location,
-                    )
-                    self.error.extend(
-                        [
-                            (f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, locn)
-                            for m, locn in proof.error
-                        ]
+                        f.identifier.location,
                     )
                     return
 
                 proof = start.check(facts)
                 if proof.result != ProofResult.sat:
                     path_message = " -> ".join([last.target.name for last in path])
                     self.error.append(
-                        f'negative length for field "{f.name}" ({path_message})',
+                        f'negative start for field "{f.name}" ({path_message})',
                         Subsystem.MODEL,
                         Severity.ERROR,
                         self.identifier.location,

tests/test_model.py

@@ -1,6 +1,6 @@
 # pylint: disable=too-many-lines
 from copy import deepcopy
-from typing import Mapping, Sequence
+from typing import Sequence
 
 import pytest
 
@@ -48,7 +48,7 @@
     UnprovenMessage,
 )
 from tests.models import ENUMERATION, ETHERNET_FRAME, MODULAR_INTEGER, RANGE_INTEGER
-from tests.utils import assert_equal
+from tests.utils import assert_equal, assert_message_model_error
 
 M_NO_REF = UnprovenMessage(
     "P.No_Ref",
@@ -148,13 +148,6 @@ def assert_model_error(types: Sequence[Type], regex: str) -> None:
         Model([*BUILTIN_TYPES.values(), *types])
 
 
-def assert_message_model_error(
-    structure: Sequence[Link], types: Mapping[Field, Type], regex: str
-) -> None:
-    with pytest.raises(RecordFluxError, match=regex):
-        Message("P.M", structure, types, Location((10, 8)))
-
-
 def assert_message(actual: Message, expected: Message, msg: str = None) -> None:
     msg = f"{expected.full_name} - {msg}" if msg else expected.full_name
     assert actual.full_name == expected.full_name, msg
@@ -414,6 +407,7 @@ def test_message_ambiguous_first_field() -> None:
         '^<stdin>:10:8: model: error: ambiguous first field in "P.M"\n'
         "<stdin>:2:6: model: info: duplicate\n"
         "<stdin>:3:6: model: info: duplicate",
+        Location((10, 8)),
     )
 
 
@@ -549,12 +543,13 @@ def test_message_cycle() -> None:
     assert_message_model_error(
         structure,
         types,
-        '^<stdin>:10:8: model: error: structure of "P.M" contains cycle'
+        '^<stdin>:10:8: model: error: structure of "P.M" contains cycle',
         # ISSUE: Componolit/RecordFlux#256
         # '\n'
         # '<stdin>:3:5: model: info: field "X" links to "Y"\n'
         # '<stdin>:4:5: model: info: field "Y" links to "Z"\n'
         # '<stdin>:5:5: model: info: field "Z" links to "X"\n',
+        Location((10, 8)),
     )
 
 

tests/test_verification.py

@@ -1,9 +1,7 @@
 # pylint: disable=too-many-lines
-from typing import Any, Mapping, Sequence
+from typing import Any
 
-import pytest
-
-from rflx.error import Location, RecordFluxError
+from rflx.error import Location
 from rflx.expression import (
     Add,
     Aggregate,
@@ -33,17 +31,9 @@
     ModularInteger,
     Opaque,
     RangeInteger,
-    Type,
 )
 from tests.models import ARRAYS_MODULAR_VECTOR, ENUMERATION, MODULAR_INTEGER, RANGE_INTEGER
-
-
-def assert_message_model_error(
-    structure: Sequence[Link], types: Mapping[Field, Type], regex: str
-) -> None:
-    with pytest.raises(RecordFluxError, match=regex):
-        message = Message("P.M", structure, types)
-        message.error.propagate()
+from tests.utils import assert_message_model_error
 
 
 def test_exclusive_valid() -> None:
@@ -491,24 +481,33 @@ def test_invalid_length_forward_reference() -> None:
     assert_message_model_error(structure, types, '^model: error: subsequent field "F2" referenced$')
 
 
-def test_invalid_negative_field_length() -> None:
+def test_invalid_negative_field_length_modular() -> None:
     structure = [
         Link(INITIAL, Field("F1")),
-        Link(Field("F1"), Field("F2"), length=Sub(Variable("F1"), Number(300))),
+        Link(Field("F1"), Field("F2"), length=Sub(Variable("F1"), Number(2))),
         Link(Field("F2"), FINAL),
     ]
     types = {
         Field("F1"): MODULAR_INTEGER,
         Field("F2"): Opaque(),
     }
+    assert_message_model_error(
+        structure, types, r'^model: error: negative length for field "F2" [(]F1 -> F2[)]$',
+    )
+
+
+def test_invalid_negative_field_length_range_integer() -> None:
+    o = Field(ID("O", location=Location((44, 3))))
+    structure = [
+        Link(INITIAL, Field("L")),
+        Link(Field("L"), o, length=Mul(Number(8), Sub(Variable("L"), Number(50))),),
+        Link(o, FINAL),
+    ]
+    types = {Field("L"): RANGE_INTEGER, o: Opaque()}
     assert_message_model_error(
         structure,
         types,
-        r"^"
-        r'model: error: negative length for field "F2" [(]F1 -> F2[)]\n'
-        r'model: info: unsatisfied "F1 < 256"\n'
-        r'model: info: unsatisfied "F1 - 300 >= 0"'
-        r"$",
+        r'^<stdin>:44:3: model: error: negative length for field "O" [(]L -> O[)]$',
     )
 
 
@@ -638,7 +637,7 @@ def test_field_after_message_start(monkeypatch: Any) -> None:
         structure,
         types,
         r"^"
-        r'model: error: negative length for field "F2" [(]F1 -> F2[)]\n'
+        r'model: error: negative start for field "F2" [(]F1 -> F2[)]\n'
         r'model: info: unsatisfied "Message\'First - 1000 >= Message\'First"'
         r"$",
     )

tests/utils.py

@@ -1,5 +1,17 @@
-from typing import Any
+from typing import Any, Mapping, Sequence
+
+import pytest
+
+from rflx.error import Location, RecordFluxError
+from rflx.model import Field, Link, Message, Type
 
 
 def assert_equal(left: Any, right: Any) -> None:
     assert left == right
+
+
+def assert_message_model_error(
+    structure: Sequence[Link], types: Mapping[Field, Type], regex: str, location: Location = None
+) -> None:
+    with pytest.raises(RecordFluxError, match=regex):
+        Message("P.M", structure, types, location)