From 077b4d3da770f4e09b7b6a15c5bed738e2d9417f Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 19 Mar 2019 09:26:27 -0700 Subject: [PATCH] [sledge] Add Solver tests demonstrating incompleteness Summary: The SL solver is currently not always able to append segments which have been split symbolically, that is, at an internal point expressed using a variable, rather than merely a constant. Also, existential instantiation, that is, the choice of witnesses during proof search, is currently sensitive to the order of subformulas. This can lead to fragile incompleteness. Reviewed By: mbouaziz Differential Revision: D14481991 fbshipit-source-id: 80fe2f0a8 --- sledge/src/symbheap/solver_test.ml | 169 ++++++++++++++++++++++++----- 1 file changed, 141 insertions(+), 28 deletions(-) diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index c0da338a0..539fe0bbe 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/sledge/src/symbheap/solver_test.ml @@ -14,17 +14,24 @@ let%test_module _ = ~config:(Result.ok_exn (Trace.parse "+Solver.infer_frame")) () + let infer_frame p xs q = + Solver.infer_frame p (Var.Set.of_list xs) q + |> (ignore : Sh.t option -> _) + let check_frame p xs q = Solver.infer_frame p (Var.Set.of_list xs) q |> fun r -> assert (Option.is_some r) let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz let ( + ) = Exp.add Typ.ptr + let ( - ) = Exp.sub Typ.siz + let ( * ) = Exp.mul Typ.siz let wrt = Var.Set.empty let a_, wrt = Var.fresh "a" ~wrt let a2_, wrt = Var.fresh "a" ~wrt let a3_, wrt = Var.fresh "a" ~wrt let b_, wrt = Var.fresh "b" ~wrt + let k_, wrt = Var.fresh "k" ~wrt let l_, wrt = Var.fresh "l" ~wrt let l2_, wrt = Var.fresh "l" ~wrt let m_, wrt = Var.fresh "m" ~wrt @@ -33,6 +40,7 @@ let%test_module _ = let a2 = Exp.var a2_ let a3 = Exp.var a3_ let b = Exp.var b_ + let k = Exp.var k_ let l = Exp.var l_ let l2 = Exp.var l2_ let m = Exp.var m_ @@ -58,8 +66,8 @@ let%test_module _ = [] Sh.emp ; [%expect {| - ( infer_frame: %l_5 -[ %b_4, %m_7 )-> ⟨%n_8,%a_1⟩ \- emp - ) infer_frame: %l_5 -[ %b_4, %m_7 )-> ⟨%n_8,%a_1⟩ |}] + ( infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \- emp + ) infer_frame: %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ |}] let%expect_test _ = check_frame @@ -69,8 +77,8 @@ let%test_module _ = [%expect {| ( infer_frame: - %l_5 -[ %b_4, %m_7 )-> ⟨%n_8,%a_1⟩ - \- %l_5 -[ %b_4, %m_7 )-> ⟨%n_8,%a_1⟩ + %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ + \- %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ ) infer_frame: emp |}] let%expect_test _ = @@ -83,10 +91,10 @@ let%test_module _ = [%expect {| ( infer_frame: - %l_5 -[ %b_4, %m_7 )-> ⟨%n_8,%a_1⟩ - * %l_6 -[ %b_4, %m_7 )-> ⟨%n_8,%a_2⟩ - \- %l_5 -[ %b_4, %m_7 )-> ⟨%n_8,%a_1⟩ - ) infer_frame: %l_6 -[ %b_4, %m_7 )-> ⟨%n_8,%a_2⟩ |}] + %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ + * %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩ + \- %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ + ) infer_frame: %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩ |}] let%expect_test _ = check_frame @@ -98,12 +106,12 @@ let%test_module _ = [%expect {| ( infer_frame: - (%l_5 + 8) -[ %l_5, 16 )-> ⟨8,%a_2⟩ - * %l_5 -[ %l_5, 16 )-> ⟨8,%a_1⟩ + (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩ + * %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩ \- ∃ %a_3 . - %l_5 -[)-> ⟨16,%a_3⟩ + %l_6 -[)-> ⟨16,%a_3⟩ ) infer_frame: - ∃ %a1_6 . ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_6⟩ ∧ %a_2 = %a1_6 ∧ emp |}] + ∃ %a1_7 . ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_7⟩ ∧ %a_2 = %a1_7 ∧ emp |}] let%expect_test _ = check_frame @@ -115,15 +123,15 @@ let%test_module _ = [%expect {| ( infer_frame: - (%l_5 + 8) -[ %l_5, 16 )-> ⟨8,%a_2⟩ - * %l_5 -[ %l_5, 16 )-> ⟨8,%a_1⟩ - \- ∃ %a_3, %m_7 . - %l_5 -[ %l_5, %m_7 )-> ⟨16,%a_3⟩ + (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩ + * %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩ + \- ∃ %a_3, %m_8 . + %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩ ) infer_frame: - ∃ %a1_8 . - ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_8⟩ - ∧ %a_2 = %a1_8 - ∧ 16 = %m_7 + ∃ %a1_9 . + ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_9⟩ + ∧ %a_2 = %a1_9 + ∧ 16 = %m_8 ∧ emp |}] let%expect_test _ = @@ -136,14 +144,119 @@ let%test_module _ = [%expect {| ( infer_frame: - (%l_5 + 8) -[ %l_5, 16 )-> ⟨8,%a_2⟩ - * %l_5 -[ %l_5, 16 )-> ⟨8,%a_1⟩ - \- ∃ %a_3, %m_7 . - %l_5 -[)-> ⟨%m_7,%a_3⟩ + (%l_6 + 8) -[ %l_6, 16 )-> ⟨8,%a_2⟩ + * %l_6 -[ %l_6, 16 )-> ⟨8,%a_1⟩ + \- ∃ %a_3, %m_8 . + %l_6 -[)-> ⟨%m_8,%a_3⟩ ) infer_frame: - ∃ %a1_8 . - ⟨%m_7,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_8⟩ - ∧ %a_2 = %a1_8 - ∧ 16 = %m_7 + ∃ %a1_9 . + ⟨%m_8,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_9⟩ + ∧ %a_2 = %a1_9 + ∧ 16 = %m_8 ∧ emp |}] + + let%expect_test _ = + check_frame + (Sh.star + (Sh.seg {loc= k; bas= k; len= !16; siz= !32; arr= a}) + (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= !16})) + [a2_; m_; n_] + (Sh.star + (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= n}) + (Sh.seg {loc= k; bas= k; len= m; siz= n; arr= a2})) ; + [%expect + {| + ( infer_frame: + %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩ + \- ∃ %a_2, %m_8, %n_9 . + %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩ + ) infer_frame: + ∃ %a0_10, %a1_11 . + ⟨32,%a_1⟩ = ⟨%n_9,%a0_10⟩^⟨16,%a1_11⟩ + ∧ %a_2 = %a0_10 + ∧ 16 = %m_8 = %n_9 + ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}] + + (* Incompleteness: changing the order of the subtrahend leads to + different existential instantiation, which fails *) + let%expect_test _ = + infer_frame + (Sh.star + (Sh.seg {loc= k; bas= k; len= !16; siz= !32; arr= a}) + (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= !16})) + [a2_; m_; n_] + (Sh.star + (Sh.seg {loc= k; bas= k; len= m; siz= n; arr= a2}) + (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= n})) ; + [%expect + {| + ( infer_frame: + %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩ + \- ∃ %a_2, %m_8, %n_9 . + %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩ + ) infer_frame: |}] + + let seg_split_symbolically = + Sh.star + (Sh.seg {loc= l; bas= l; len= !16; siz= !8 * n; arr= a2}) + (Sh.seg + { loc= l + (!8 * n) + ; bas= l + ; len= !16 + ; siz= !16 - (!8 * n) + ; arr= a3 }) + + let%expect_test _ = + check_frame + (Sh.and_ + Exp.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2)) + seg_split_symbolically) + [m_; a_] + (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ; + [%expect + {| + ( infer_frame: + (%l_6 + 8 × %n_9) -[ %l_6, 16 )-> ⟨(-8 × %n_9 + 16),%a_3⟩ + * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩ + * ( ( 2 = %n_9 ∧ emp) + ∨ ( 0 = %n_9 ∧ emp) + ∨ ( 1 = %n_9 ∧ emp) + ) + \- ∃ %a_1, %m_8 . + %l_6 -[)-> ⟨%m_8,%a_1⟩ + ) infer_frame: + emp + * ( ( %a_1 = %a_2 + ∧ 2 = %n_9 + ∧ 16 = %m_8 + ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩) + ∨ (∃ %a1_10 . + ⟨%m_8,%a_1⟩ = ⟨(8 × %n_9),%a_2⟩^⟨8,%a1_10⟩ + ∧ %a_3 = %a1_10 + ∧ 1 = %n_9 + ∧ 16 = %m_8 + ∧ emp) + ∨ (∃ %a1_10 . + ⟨%m_8,%a_1⟩ = ⟨(8 × %n_9),%a_2⟩^⟨16,%a1_10⟩ + ∧ %a_3 = %a1_10 + ∧ 0 = %n_9 + ∧ 16 = %m_8 + ∧ emp) + ) |}] + + (* Incompleteness: equivalent to above but using ≤ instead of ∨ *) + let%expect_test _ = + infer_frame + (Sh.and_ (Exp.le n !2) seg_split_symbolically) + [m_; a_] + (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ; + [%expect + {| + ( infer_frame: + (%n_9 ≤ 2) + ∧ (%l_6 + 8 × %n_9) -[ %l_6, 16 )-> ⟨(-8 × %n_9 + 16),%a_3⟩ + * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩ + \- ∃ %a_1, %m_8 . + %l_6 -[)-> ⟨%m_8,%a_1⟩ + ) infer_frame: |}] end )