[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

@@ -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= k; bas= b; len= m; siz= o} = msg in
-  let {Sh.loc= l; siz= n} = ssg 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
+  if
-  (* k-l < 0 so k < l *)
+    (not (Equality.entails_eq sub.cong b b'))
-  | -1 -> (
+    || not (Equality.entails_eq sub.cong m m')
-      let ko = Exp.add Typ.ptr k o in
+  then
-      let ln = Exp.add Typ.ptr l n in
+    Some
-      Equality.difference sub.cong ko ln
+      {goal with sub= Sh.and_ (Exp.eq b b') (Sh.and_ (Exp.eq m m') goal.sub)}
-      >>= fun ko_ln ->
+  else
-      match[@warning "-p"] Z.sign ko_ln with
+    match[@warning "-p"] Z.sign k_l with
-      (* k+o-(l+n) < 0 so k+o < l+n *)
+    (* k-l < 0 so k < l *)
-      | -1 -> (
+    | -1 -> (
-          Equality.difference sub.cong l ko
+        let ko = Exp.add Typ.ptr k o in
-          >>= fun l_ko ->
+        let ln = Exp.add Typ.ptr l n in
-          match[@warning "-p"] Z.sign l_ko with
+        Equality.difference sub.cong ko ln
-          (* l-(k+o) < 0     [k;   o)
+        >>= fun ko_ln ->
-           * so l < k+o    ⊢    [l;  n) *)
+        match[@warning "-p"] Z.sign ko_ln with
-          | -1 ->
+        (* k+o-(l+n) < 0 so k+o < l+n *)
-              Some
+        | -1 -> (
-                (excise_seg_min_skew goal msg ssg (Z.neg k_l) (Z.neg l_ko)
+            Equality.difference sub.cong l ko
-                   (Z.neg ko_ln))
+            >>= fun l_ko ->
-          | _ -> None )
+            match[@warning "-p"] Z.sign l_ko with
-      (* k+o-(l+n) = 0     [k;    o)
+            (* l-(k+o) < 0     [k;   o)
-       * so k+o = l+n    ⊢    [l; n) *)
+             * so l < k+o    ⊢    [l;  n) *)
-      | 0 -> Some (excise_seg_sub_suffix goal msg ssg (Z.neg k_l))
+            | -1 ->
-      (* k+o-(l+n) > 0     [k;      o)
+                Some
-       * so k+o > l+n    ⊢    [l; n) *)
+                  (excise_seg_min_skew goal msg ssg (Z.neg k_l) (Z.neg l_ko)
-      | 1 -> Some (excise_seg_sub_infix goal msg ssg (Z.neg k_l) ko_ln) )
+                     (Z.neg ko_ln))
-  (* k-l = 0 so k = l *)
+            | _ -> None )
-  | 0 -> (
+        (* k+o-(l+n) = 0     [k;    o)
-    match Equality.difference sub.cong o n with
+         * so k+o = l+n    ⊢    [l; n) *)
-    | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub}
+        | 0 -> Some (excise_seg_sub_suffix goal msg ssg (Z.neg k_l))
-    | Some o_n -> (
+        (* k+o-(l+n) > 0     [k;      o)
-      match[@warning "-p"] Z.sign o_n with
+         * so k+o > l+n    ⊢    [l; n) *)
-      (* o-n < 0      [k; o)
+        | 1 -> Some (excise_seg_sub_infix goal msg ssg (Z.neg k_l) ko_ln) )
-       * so o < n   ⊢ [l;   n) *)
+    (* k-l = 0 so k = l *)
-      | -1 -> Some (excise_seg_min_prefix goal msg ssg (Z.neg o_n))
+    | 0 -> (
-      (* o-n = 0      [k; o)
+      match Equality.difference sub.cong o n with
-       * so o = n   ⊢ [l; n) *)
+      | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub}
-      | 0 -> Some (excise_seg_same goal msg ssg)
+      | Some o_n -> (
-      (* o-n > 0      [k;   o)
+        match[@warning "-p"] Z.sign o_n with
-       * so o > n   ⊢ [l; n) *)
+        (* o-n < 0      [k; o)
-      | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
+         * so o < n   ⊢ [l;   n) *)
-  (* k-l > 0 so k > l *)
+        | -1 -> Some (excise_seg_min_prefix goal msg ssg (Z.neg o_n))
-  | 1 -> (
+        (* o-n = 0      [k; o)
-      let ko = Exp.add Typ.ptr k o in
+         * so o = n   ⊢ [l; n) *)
-      let ln = Exp.add Typ.ptr l n in
+        | 0 -> Some (excise_seg_same goal msg ssg)
-      Equality.difference sub.cong ko ln
+        (* o-n > 0      [k;   o)
-      >>= fun ko_ln ->
+         * so o > n   ⊢ [l; n) *)
-      match[@warning "-p"] Z.sign ko_ln with
+        | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
-      (* k+o-(l+n) < 0        [k; o)
+    (* k-l > 0 so k > l *)
-       * so k+o < l+n    ⊢ [l;      n) *)
+    | 1 -> (
-      | -1 -> Some (excise_seg_min_infix goal msg ssg k_l (Z.neg ko_ln))
+        let ko = Exp.add Typ.ptr k o in
-      (* k+o-(l+n) = 0        [k; o)
+        let ln = Exp.add Typ.ptr l n in
-       * so k+o = l+n    ⊢ [l;    n) *)
+        Equality.difference sub.cong ko ln
-      | 0 -> Some (excise_seg_min_suffix goal msg ssg k_l)
+        >>= fun ko_ln ->
-      (* k+o-(l+n) > 0 so k+o > l+n *)
+        match[@warning "-p"] Z.sign ko_ln with
-      | 1 -> (
+        (* k+o-(l+n) < 0        [k; o)
-          Equality.difference sub.cong k ln
+         * so k+o < l+n    ⊢ [l;      n) *)
-          >>= fun k_ln ->
+        | -1 -> Some (excise_seg_min_infix goal msg ssg k_l (Z.neg ko_ln))
-          match[@warning "-p"] Z.sign k_ln with
+        (* k+o-(l+n) = 0        [k; o)
-          (* k-(l+n) < 0        [k;  o)
+         * so k+o = l+n    ⊢ [l;    n) *)
-           * so k < l+n    ⊢ [l;   n) *)
+        | 0 -> Some (excise_seg_min_suffix goal msg ssg k_l)
-          | -1 ->
+        (* k+o-(l+n) > 0 so k+o > l+n *)
-              Some (excise_seg_sub_skew goal msg ssg k_l (Z.neg k_ln) ko_ln)
+        | 1 -> (
-          | _ -> None ) )
+            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] ;

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 )