[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

@@ -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 )