From 8173eedf1fe568f579e9bd3520e1cb8c018196ea Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Thu, 11 Jul 2019 06:55:39 -0700 Subject: [PATCH] [sledge] Fix solver crash Summary: Fix a crash that occurs when subtrahend has an existential variable that was renamed as in the test. The crash is due to an assertion in `Sh.exists` that says only variables in the vocabulary can be existentialy quantifed out. The problem was `Sh.exists` call in Solver.ml:611. Where `ws` (existentials of the subthrehend) are not present in the vocabulary of the remainder. This is because remainder "inheirts" the vocabulary of the minued. This fix simply extends the vocabulary of minued with `ws`, which means the remaainder has the correct vocabulary. This should have no externally visible effect as `ws` are then existentialed out. Another option would be to try to change all the `excise_seg` functions, to keep the vocabulary, but that looked annoying to implement. Reviewed By: jvillard Differential Revision: D16201423 fbshipit-source-id: b88c3abc4 --- sledge/src/symbheap/solver.ml | 1 + sledge/src/symbheap/solver_test.ml | 19 +++++++++++++++++++ 2 files changed, 20 insertions(+) diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index 7f9a35f80..7384a1a63 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -606,6 +606,7 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = let ws, sub = Sh.bind_exists sub ~wrt:xs in let sub = Sh.and_cong min.cong sub in let zs = Var.Set.empty in + let min = Sh.extend_us ws min in excise {us; com; min; xs; sub; zs; pgs= true} >>| fun remainder -> Sh.exists (Set.union ys ws) remainder ) >>| fun remainder -> Sh.or_ remainders remainder ) diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index 21a0a3f79..e68c71260 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/sledge/src/symbheap/solver_test.ml @@ -88,6 +88,25 @@ let%test_module _ = \- %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ ) infer_frame: emp |}] + let%expect_test _ = + let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; arr= a2} in + let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; arr= a} in + let minued = Sh.star common seg1 in + let subtrahend = + Sh.and_ (Exp.eq m n) + (Sh.exists + (Var.Set.of_list [m_]) + (Sh.extend_us (Var.Set.of_list [m_]) common)) + in + infer_frame minued [n_; m_] subtrahend ; + [%expect + {| + ( infer_frame: + %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ * %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩ + \- ∃ %m_8, %n_9 . + ∃ %m_10 . %m_8 = %n_9 ∧ %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩ + ) infer_frame: ∃ %m_10 . %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ |}] + let%expect_test _ = check_frame (Sh.star