From 0578064a7fc0fb18882204de921d4fcd16d5b9f6 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 5 Mar 2019 09:02:17 -0800
Subject: [PATCH] [sledge] Revise solver existential instantiation

Summary:
In case the starting locations of two heap segments are
related (provably equal up to some offset), add equations between
their enclosing block to the goal. In these cases, the enclosing
blocks must be the same, so no completeness is lost. This has the
effect of instantiating existentials in the enclosing block prior to
others, which can avoid incomplete instantiation guesses.

Reviewed By: mbouaziz

Differential Revision: D14323550

fbshipit-source-id: 89a34a2c8
---
 sledge/src/symbheap/solver.ml      | 140 +++++++++++++++--------------
 sledge/src/symbheap/solver_test.ml |  22 +++++
 2 files changed, 96 insertions(+), 66 deletions(-)

diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index d20cb9169..e6fed561e 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -486,74 +486,82 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
 (* C ❮ k-[b;m)->⟨o,α⟩ * M ⊢ ∃xs. l-[b';m')->⟨n,α'⟩ * S ❯ R *)
 let excise_seg ({sub} as goal) msg ssg =
   [%Trace.info "@[<2>excise_seg@ %a@  |-  %a@]" Sh.pp_seg msg Sh.pp_seg ssg] ;
-  let {Sh.loc= k; siz= o} = msg in
-  let {Sh.loc= l; siz= n} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in
   Equality.difference sub.cong k l
   >>= fun k_l ->
-  match[@warning "-p"] Z.sign k_l with
-  (* k-l < 0 so k < l *)
-  | -1 -> (
-      let ko = Exp.add Typ.ptr k o in
-      let ln = Exp.add Typ.ptr l n in
-      Equality.difference sub.cong ko ln
-      >>= fun ko_ln ->
-      match[@warning "-p"] Z.sign ko_ln with
-      (* k+o-(l+n) < 0 so k+o < l+n *)
-      | -1 -> (
-          Equality.difference sub.cong l ko
-          >>= fun l_ko ->
-          match[@warning "-p"] Z.sign l_ko with
-          (* l-(k+o) < 0     [k;   o)
-           * so l < k+o    ⊢    [l;  n) *)
-          | -1 ->
-              Some
-                (excise_seg_min_skew goal msg ssg (Z.neg k_l) (Z.neg l_ko)
-                   (Z.neg ko_ln))
-          | _ -> None )
-      (* k+o-(l+n) = 0     [k;    o)
-       * so k+o = l+n    ⊢    [l; n) *)
-      | 0 -> Some (excise_seg_sub_suffix goal msg ssg (Z.neg k_l))
-      (* k+o-(l+n) > 0     [k;      o)
-       * so k+o > l+n    ⊢    [l; n) *)
-      | 1 -> Some (excise_seg_sub_infix goal msg ssg (Z.neg k_l) ko_ln) )
-  (* k-l = 0 so k = l *)
-  | 0 -> (
-    match Equality.difference sub.cong o n with
-    | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub}
-    | Some o_n -> (
-      match[@warning "-p"] Z.sign o_n with
-      (* o-n < 0      [k; o)
-       * so o < n   ⊢ [l;   n) *)
-      | -1 -> Some (excise_seg_min_prefix goal msg ssg (Z.neg o_n))
-      (* o-n = 0      [k; o)
-       * so o = n   ⊢ [l; n) *)
-      | 0 -> Some (excise_seg_same goal msg ssg)
-      (* o-n > 0      [k;   o)
-       * so o > n   ⊢ [l; n) *)
-      | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
-  (* k-l > 0 so k > l *)
-  | 1 -> (
-      let ko = Exp.add Typ.ptr k o in
-      let ln = Exp.add Typ.ptr l n in
-      Equality.difference sub.cong ko ln
-      >>= fun ko_ln ->
-      match[@warning "-p"] Z.sign ko_ln with
-      (* k+o-(l+n) < 0        [k; o)
-       * so k+o < l+n    ⊢ [l;      n) *)
-      | -1 -> Some (excise_seg_min_infix goal msg ssg k_l (Z.neg ko_ln))
-      (* k+o-(l+n) = 0        [k; o)
-       * so k+o = l+n    ⊢ [l;    n) *)
-      | 0 -> Some (excise_seg_min_suffix goal msg ssg k_l)
-      (* k+o-(l+n) > 0 so k+o > l+n *)
-      | 1 -> (
-          Equality.difference sub.cong k ln
-          >>= fun k_ln ->
-          match[@warning "-p"] Z.sign k_ln with
-          (* k-(l+n) < 0        [k;  o)
-           * so k < l+n    ⊢ [l;   n) *)
-          | -1 ->
-              Some (excise_seg_sub_skew goal msg ssg k_l (Z.neg k_ln) ko_ln)
-          | _ -> None ) )
+  if
+    (not (Equality.entails_eq sub.cong b b'))
+    || not (Equality.entails_eq sub.cong m m')
+  then
+    Some
+      {goal with sub= Sh.and_ (Exp.eq b b') (Sh.and_ (Exp.eq m m') goal.sub)}
+  else
+    match[@warning "-p"] Z.sign k_l with
+    (* k-l < 0 so k < l *)
+    | -1 -> (
+        let ko = Exp.add Typ.ptr k o in
+        let ln = Exp.add Typ.ptr l n in
+        Equality.difference sub.cong ko ln
+        >>= fun ko_ln ->
+        match[@warning "-p"] Z.sign ko_ln with
+        (* k+o-(l+n) < 0 so k+o < l+n *)
+        | -1 -> (
+            Equality.difference sub.cong l ko
+            >>= fun l_ko ->
+            match[@warning "-p"] Z.sign l_ko with
+            (* l-(k+o) < 0     [k;   o)
+             * so l < k+o    ⊢    [l;  n) *)
+            | -1 ->
+                Some
+                  (excise_seg_min_skew goal msg ssg (Z.neg k_l) (Z.neg l_ko)
+                     (Z.neg ko_ln))
+            | _ -> None )
+        (* k+o-(l+n) = 0     [k;    o)
+         * so k+o = l+n    ⊢    [l; n) *)
+        | 0 -> Some (excise_seg_sub_suffix goal msg ssg (Z.neg k_l))
+        (* k+o-(l+n) > 0     [k;      o)
+         * so k+o > l+n    ⊢    [l; n) *)
+        | 1 -> Some (excise_seg_sub_infix goal msg ssg (Z.neg k_l) ko_ln) )
+    (* k-l = 0 so k = l *)
+    | 0 -> (
+      match Equality.difference sub.cong o n with
+      | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub}
+      | Some o_n -> (
+        match[@warning "-p"] Z.sign o_n with
+        (* o-n < 0      [k; o)
+         * so o < n   ⊢ [l;   n) *)
+        | -1 -> Some (excise_seg_min_prefix goal msg ssg (Z.neg o_n))
+        (* o-n = 0      [k; o)
+         * so o = n   ⊢ [l; n) *)
+        | 0 -> Some (excise_seg_same goal msg ssg)
+        (* o-n > 0      [k;   o)
+         * so o > n   ⊢ [l; n) *)
+        | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
+    (* k-l > 0 so k > l *)
+    | 1 -> (
+        let ko = Exp.add Typ.ptr k o in
+        let ln = Exp.add Typ.ptr l n in
+        Equality.difference sub.cong ko ln
+        >>= fun ko_ln ->
+        match[@warning "-p"] Z.sign ko_ln with
+        (* k+o-(l+n) < 0        [k; o)
+         * so k+o < l+n    ⊢ [l;      n) *)
+        | -1 -> Some (excise_seg_min_infix goal msg ssg k_l (Z.neg ko_ln))
+        (* k+o-(l+n) = 0        [k; o)
+         * so k+o = l+n    ⊢ [l;    n) *)
+        | 0 -> Some (excise_seg_min_suffix goal msg ssg k_l)
+        (* k+o-(l+n) > 0 so k+o > l+n *)
+        | 1 -> (
+            Equality.difference sub.cong k ln
+            >>= fun k_ln ->
+            match[@warning "-p"] Z.sign k_ln with
+            (* k-(l+n) < 0        [k;  o)
+             * so k < l+n    ⊢ [l;   n) *)
+            | -1 ->
+                Some
+                  (excise_seg_sub_skew goal msg ssg k_l (Z.neg k_ln) ko_ln)
+            | _ -> None ) )
 
 let excise_heap ({min; sub} as goal) =
   [%Trace.info "@[<2>excise_heap@ %a@]" pp goal] ;
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index 110037612..56ed6ff76 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -130,4 +130,26 @@ let%test_module _ =
           ∧ %a_2 = %a1_8
           ∧ 16 = %m_7
           ∧ emp |}]
+
+    let%expect_test _ =
+      check_frame
+        (Sh.star
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; arr= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; arr= a2}))
+        [a3_; m_]
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a3}) ;
+      [%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⟩
+        ) infer_frame:
+          ∃  .
+          ∃ %a1_8 .
+            ⟨%m_7,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_8⟩
+          ∧ %a_2 = %a1_8
+          ∧ 16 = %m_7
+          ∧ emp |}]
   end )