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=pytest,z3,pydotplus

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

@@ -1520,3 +1520,20 @@ def test_opaque_length_valid_multiple_of_8_dynamic_cond() -> None:
         ],
         {Field("L"): MODULAR_INTEGER, Field("O"): Opaque()},
     )
+
+
+def test_length_range_underflow() -> None:
+    with pytest.raises(
+        RecordFluxError,
+        match=r'^<stdin>:44:3: model: error: negative length for field "O" [(]L -> O[)]$',
+    ):
+        o = Field(ID("O", location=Location((44, 3))))
+        Message(
+            "P.M",
+            [
+                Link(INITIAL, Field("L")),
+                Link(Field("L"), o, length=Mul(Number(8), Sub(Variable("L"), Number(50))),),
+                Link(o, FINAL),
+            ],
+            {Field("L"): RangeInteger("P.Len", Number(40), Number(1500), Number(16)), o: Opaque()},
+        )

tests/test_verification.py

@@ -502,13 +502,7 @@ def test_invalid_negative_field_length() -> None:
         Field("F2"): 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"$",
+        structure, types, r"^" r'model: error: negative length for field "F2" [(]F1 -> F2[)]' r"$",
     )
 
 
@@ -638,7 +632,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"$",
     )