Fix fatal errors caused by missing locations after proof timeouts

Ref. eng/recordflux/RecordFlux#1782
AdaCore · Sep 11, 2024 · 64a0df8 · 64a0df8
1 parent 6c0c94d
commit 64a0df8
Show file tree

Hide file tree

Showing 5 changed files with 23 additions and 8 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -31,6 +31,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Missing checks in state machine to improve provability (eng/recordflux/RecordFlux#1704)
 - Copying of sequence fields for external IO buffers (eng/recordflux/RecordFlux#1704)
 - Syntax highlighting for identifiers with numbers or keywords (AdaCore/RecordFlux#1301, eng/recordflux/RecordFlux#1776)
+- Fatal errors caused by missing locations after proof timeouts (eng/recordflux/RecordFlux#1782)
 
 ## [0.23.0] - 2024-08-23
 

diff --git a/rflx/expr_proof.py b/rflx/expr_proof.py
@@ -62,7 +62,8 @@ def error(self) -> list[tuple[str, Location | None]]:
 
         if self._result == ProofResult.UNKNOWN:
             assert self._unknown_reason is not None
-            return [(self._unknown_reason, None)]
+            assert self._expr.location is not None
+            return [(self._unknown_reason, self._expr.location)]
 
         solver = z3.SolverFor(self._logic)
         solver.set(unsat_core=True)

diff --git a/rflx/model/message.py b/rflx/model/message.py
@@ -1965,7 +1965,14 @@ def is_proper_prefix(path: tuple[Link, ...], paths: set[tuple[Link, ...]]) -> bo
 
                 facts = self._path_constraints(path)
                 outgoing = self.outgoing(path[-1].target)
-                condition = expr.Or(*[o.condition for o in outgoing]) if outgoing else expr.TRUE
+                condition = (
+                    expr.Or(
+                        *[o.condition for o in outgoing],
+                        location=Location.merge([o.condition.location for o in outgoing]),
+                    )
+                    if outgoing
+                    else expr.TRUE
+                )
                 proof = expr_proof.Proof(
                     condition,
                     [
@@ -1974,7 +1981,7 @@ def is_proper_prefix(path: tuple[Link, ...], paths: set[tuple[Link, ...]]) -> bo
                         *self.message_constraints,
                     ],
                 )
-                assert proof.result != expr_proof.ProofResult.SAT
+                assert proof.result != expr_proof.ProofResult.SAT, proof.result
 
                 paths.append((path, proof.error))
                 unreachable_paths.add(path)
@@ -2255,7 +2262,11 @@ def _prove_message_size(self, proofs: expr_proof.ParallelProofs) -> None:
                 ],
             )
             proofs.add(
-                expr.NotEqual(expr.Mod(message_size, expr.Number(8)), expr.Number(0)),
+                expr.NotEqual(
+                    expr.Mod(message_size, expr.Number(8)),
+                    expr.Number(0),
+                    location=self.location,
+                ),
                 facts,
                 sat_error=error.entries,
                 unknown_error=error.entries,

diff --git a/rflx/model/type_decl.py b/rflx/model/type_decl.py
@@ -477,7 +477,7 @@ def constraints(
                 *[
                     expr.Equal(
                         expr.Variable(name, type_=self.type_),
-                        expr.Literal(l),
+                        expr.Literal(l, location=l.location),
                         self.location,
                     )
                     for l in literals
@@ -487,7 +487,7 @@ def constraints(
         ]
         result.extend(
             [
-                expr.Equal(expr.Literal(l, type_=self.type_), v, self.location)
+                expr.Equal(expr.Literal(l, type_=self.type_, location=l.location), v, self.location)
                 for l, v in literals.items()
             ],
         )

diff --git a/tests/unit/expr_proof_test.py b/tests/unit/expr_proof_test.py
@@ -39,17 +39,19 @@
     Variable,
 )
 from rflx.expr_proof import Proof, ProofResult, Z3TypeError, _to_z3
+from rflx.rapidflux import Location
 from tests.utils import assert_equal
 
 
 def test_proof_invalid_logic() -> None:
-    expr = Less(Mod(Variable("X"), Variable("Y")), Number(100))
+    location = Location((1, 2))
+    expr = Less(Mod(Variable("X"), Variable("Y")), Number(100), location=location)
     p = Proof(expr, logic="QF_IDL")
     assert p.result == ProofResult.UNKNOWN
     assert p.error == [
         (
             "Benchmark is not in QF_IDL (integer difference logic).",
-            None,
+            location,
         ),
     ]