[sledge] Replace Memory and Concat Term constructors with eq_concat

Summary:
The exposed constructors for Memory and Concat Terms are only used in
a very special idiom: to construct an equality between a single Memory
chunk and the Concat of multiple Memory chunks. This diff specializes
and simplifies by exposing a Term.eq_concat constructor for this
idiom, and removes the underlying Term.memory and Term.concat
constructors.

Reviewed By: ngorogiannis

Differential Revision: D19221866

fbshipit-source-id: 4842737d2

sledge/src/llair/term.ml

@@ -895,6 +895,10 @@ let select ~rcd ~idx = norm1 (Select idx) rcd
 let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
 let size_of t = integer (Z.of_int (Typ.size_of t))
 
+let eq_concat (siz, arr) ms =
+  eq (memory ~siz ~arr)
+    (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))
+
 (** Transform *)
 
 let map e ~f =

sledge/src/llair/term.mli

@@ -213,8 +213,7 @@ val conditional : cnd:t -> thn:t -> els:t -> t
 
 (* memory contents *)
 val splat : t -> t
-val memory : siz:t -> arr:t -> t
+val eq_concat : t * t -> (t * t) array -> t
-val concat : t array -> t
 
 (* records (struct / array values) *)
 val record : t vector -> t

sledge/src/symbheap/exec.ml

@@ -159,16 +159,15 @@ let memmov_foot us dst src len =
   let arr_mid, us, xs = fresh_var "a" us xs in
   let arr_src, us, xs = fresh_var "a" us xs in
   let src_dst = Term.sub src dst in
-  let mem_dst = Term.memory ~siz:src_dst ~arr:arr_dst in
+  let mem_dst = (src_dst, arr_dst) in
   let siz_mid = Term.sub len src_dst in
-  let mem_mid = Term.memory ~siz:siz_mid ~arr:arr_mid in
+  let mem_mid = (siz_mid, arr_mid) in
-  let mem_src = Term.memory ~siz:src_dst ~arr:arr_src in
+  let mem_src = (src_dst, arr_src) in
-  let mem_dst_mid_src = Term.concat [|mem_dst; mem_mid; mem_src|] in
+  let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in
   let siz_dst_mid_src, us, xs = fresh_var "m" us xs in
   let arr_dst_mid_src, _, xs = fresh_var "a" us xs in
   let eq_mem_dst_mid_src =
-    Term.eq mem_dst_mid_src
+    Term.eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src
-      (Term.memory ~siz:siz_dst_mid_src ~arr:arr_dst_mid_src)
   in
   let seg =
     Sh.seg
@@ -189,12 +188,11 @@ let memmov_dn_spec us dst src len =
   let xs, bas, siz, _, mem_mid, mem_src, foot =
     memmov_foot us dst src len
   in
-  let mem_mid_src_src = Term.concat [|mem_mid; mem_src; mem_src|] in
+  let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in
   let siz_mid_src_src, us, xs = fresh_var "m" us xs in
   let arr_mid_src_src, _, xs = fresh_var "a" us xs in
   let eq_mem_mid_src_src =
-    Term.eq mem_mid_src_src
+    Term.eq_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src
-      (Term.memory ~siz:siz_mid_src_src ~arr:arr_mid_src_src)
   in
   let post =
     Sh.and_ eq_mem_mid_src_src
@@ -215,12 +213,11 @@ let memmov_up_spec us dst src len =
   let xs, bas, siz, mem_src, mem_mid, _, foot =
     memmov_foot us src dst len
   in
-  let mem_src_src_mid = Term.concat [|mem_src; mem_src; mem_mid|] in
+  let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in
   let siz_src_src_mid, us, xs = fresh_var "m" us xs in
   let arr_src_src_mid, _, xs = fresh_var "a" us xs in
   let eq_mem_src_src_mid =
-    Term.eq mem_src_src_mid
+    Term.eq_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid
-      (Term.memory ~siz:siz_src_src_mid ~arr:arr_src_src_mid)
   in
   let post =
     Sh.and_ eq_mem_src_src_mid
@@ -375,16 +372,8 @@ let realloc_spec us reg ptr siz =
       (Sh.and_
          Term.(
            conditional ~cnd:(le len siz)
-             ~thn:
+             ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|])
-               (eq (memory ~siz ~arr:a1)
+             ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
-                  (concat
-                     [| memory ~siz:len ~arr:a0
-                      ; memory ~siz:(sub siz len) ~arr:a2 |]))
-             ~els:
-               (eq (memory ~siz:len ~arr:a0)
-                  (concat
-                     [| memory ~siz ~arr:a1
-                      ; memory ~siz:(sub len siz) ~arr:a2 |])))
          (Sh.seg rseg))
   in
   {xs; foot; sub; ms; post}
@@ -415,16 +404,8 @@ let rallocx_spec us reg ptr siz =
       (Sh.and_
          Term.(
            conditional ~cnd:(le len siz)
-             ~thn:
+             ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|])
-               (eq (memory ~siz ~arr:a1)
+             ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
-                  (concat
-                     [| memory ~siz:len ~arr:a0
-                      ; memory ~siz:(sub siz len) ~arr:a2 |]))
-             ~els:
-               (eq (memory ~siz:len ~arr:a0)
-                  (concat
-                     [| memory ~siz ~arr:a1
-                      ; memory ~siz:(sub len siz) ~arr:a2 |])))
          (Sh.seg rseg))
   in
   {xs; foot; sub; ms; post}
@@ -458,16 +439,8 @@ let xallocx_spec us reg ptr siz ext =
       Term.(
         and_
           (conditional ~cnd:(le len siz)
-             ~thn:
+             ~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|])
-               (eq (memory ~siz ~arr:a1)
+             ~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
-                  (concat
-                     [| memory ~siz:len ~arr:a0
-                      ; memory ~siz:(sub siz len) ~arr:a2 |]))
-             ~els:
-               (eq (memory ~siz:len ~arr:a0)
-                  (concat
-                     [| memory ~siz ~arr:a1
-                      ; memory ~siz:(sub len siz) ~arr:a2 |])))
           (and_ (le siz reg) (le reg (add siz ext))))
       (Sh.seg seg')
   in

sledge/src/symbheap/sh.ml

@@ -58,13 +58,17 @@ let var_strength q =
   in
   var_strength_ Var.Set.empty Var.Map.empty q
 
+let pp_memory x fs (siz, arr) =
+  let term_pp = Term.ppx x in
+  Format.fprintf fs "@<1>⟨%a,%a@<1>⟩" term_pp siz term_pp arr
+
 let pp_seg x fs {loc; bas; len; siz; arr} =
   let term_pp = Term.ppx x in
   Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
     (fun fs (bas, len) ->
       if (not (Term.equal loc bas)) || not (Term.equal len siz) then
         Format.fprintf fs " %a, %a " term_pp bas term_pp len )
-    (bas, len) term_pp (Term.memory ~siz ~arr)
+    (bas, len) (pp_memory x) (siz, arr)
 
 let pp_seg_norm cong fs seg =
   let x _ = None in
@@ -91,8 +95,7 @@ let pp_block x fs segs =
   in
   let term_pp = Term.ppx x in
   let pp_mems =
-    List.pp "@,^" (fun fs seg ->
+    List.pp "@,^" (fun fs seg -> pp_memory x fs (seg.siz, seg.arr))
-        term_pp fs (Term.memory ~siz:seg.siz ~arr:seg.arr) )
   in
   match segs with
   | {loc; bas; len; _} :: _ ->

sledge/src/symbheap/solver.ml

@@ -140,10 +140,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
   let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
   let min =
     Sh.and_
-      (Term.eq
+      (Term.eq_concat (o, a) [|(n, a0); (o_n, a1)|])
-         (Term.memory ~siz:o ~arr:a)
-         (Term.concat
-            [|Term.memory ~siz:n ~arr:a0; Term.memory ~siz:o_n ~arr:a1|]))
       (Sh.star
          (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; arr= a1})
          (Sh.rem_seg msg min))
@@ -184,11 +181,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq
+            (Term.eq_concat (n, a') [|(o, a); (n_o, a1')|])
-               (Term.concat
-                  [| Term.memory ~siz:o ~arr:a
-                   ; Term.memory ~siz:n_o ~arr:a1' |])
-               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg
                   {loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'})
@@ -224,10 +217,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Term.eq
+      (Term.eq_concat (o, a) [|(l_k, a0); (n, a1)|])
-         (Term.memory ~siz:o ~arr:a)
-         (Term.concat
-            [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:n ~arr:a1|]))
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.rem_seg msg min))
@@ -271,11 +261,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Term.eq
+      (Term.eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|])
-         (Term.memory ~siz:o ~arr:a)
-         (Term.concat
-            [| Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:n ~arr:a1
-             ; Term.memory ~siz:ko_ln ~arr:a2 |]))
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.star
@@ -322,10 +308,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Term.eq
+      (Term.eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|])
-         (Term.memory ~siz:o ~arr:a)
-         (Term.concat
-            [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:ko_l ~arr:a1|]))
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.rem_seg msg min))
@@ -334,11 +317,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq
+            (Term.eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
-               (Term.concat
-                  [| Term.memory ~siz:ko_l ~arr:a1
-                   ; Term.memory ~siz:ln_ko ~arr:a2' |])
-               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'})
                (Sh.rem_seg ssg sub))))
@@ -374,11 +353,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq
+            (Term.eq_concat (n, a') [|(k_l, a0'); (o, a)|])
-               (Term.concat
-                  [| Term.memory ~siz:k_l ~arr:a0'
-                   ; Term.memory ~siz:o ~arr:a |])
-               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.rem_seg ssg sub))))
@@ -418,11 +393,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq
+            (Term.eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
-               (Term.concat
-                  [| Term.memory ~siz:k_l ~arr:a0'; Term.memory ~siz:o ~arr:a
-                   ; Term.memory ~siz:ln_ko ~arr:a2' |])
-               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.star
@@ -464,10 +435,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   in
   let min =
     Sh.and_
-      (Term.eq
+      (Term.eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|])
-         (Term.memory ~siz:o ~arr:a)
-         (Term.concat
-            [|Term.memory ~siz:ln_k ~arr:a1; Term.memory ~siz:ko_ln ~arr:a2|]))
       (Sh.star
          (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2})
          (Sh.rem_seg msg min))
@@ -476,11 +444,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq
+            (Term.eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
-               (Term.concat
-                  [| Term.memory ~siz:k_l ~arr:a0'
-                   ; Term.memory ~siz:ln_k ~arr:a1 |])
-               (Term.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.rem_seg ssg sub))))