[sledge] Strengthen solver with implied sizes of concatenated byte arrays

Summary:
- Change representation of Concat expressions from curried binary
  operator to an nary one. This enables normalizing Concat expressions
  with respect to associativity.

- Generalize Exp.solve to return a map rather than a pair of exps, to
  enable expressing cases where solving an equation yields multiple
  equations.

- Strengthen solver with implied equalities between sums of sizes of
  concatenations of byte arrays.

Reviewed By: ngorogiannis

Differential Revision: D14297865

fbshipit-source-id: b40871559

sledge/src/import/vector.ml

@@ -70,6 +70,11 @@ let map_preserving_phys_equal xs ~f =
 
 let mapi x ~f = v (Array.mapi (a x) ~f)
 let map2_exn x y ~f = v (Array.map2_exn (a x) (a y) ~f)
+
+let fold_map x ~init ~f =
+  let s, x = Array.fold_map (a x) ~init ~f in
+  (s, v x)
+
 let concat xs = v (Array.concat (al xs))
 let of_array = v
 let of_list x = v (Array.of_list x)

sledge/src/import/vector.mli

@@ -109,7 +109,7 @@ val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
 (* val folding_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'c t *)
 (* val folding_mapi : 'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b * 'c) ->
    'c t *)
-(* val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t *)
+val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t
 
 (* val fold_mapi :
  *   'a t -> init:'b -> f:(int -> 'b -> 'a -> 'b * 'c) -> 'b * 'c t *)

sledge/src/llair/exp.ml

@@ -61,13 +61,14 @@ module rec T : sig
     (* nary: arithmetic, numeric and pointer *)
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
+    (* pointer and memory constants and operations *)
+    | Splat of {byt: t; siz: t}
+    | Memory of {siz: t; arr: t}
+    | Concat of {args: t vector}
+    (* nullary *)
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
-    (* pointer and memory constants and operations *)
-    | Splat
-    | Memory
-    | Concat
     (* numeric constants *)
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
@@ -123,12 +124,12 @@ and T0 : sig
     | App of {op: t; arg: t}
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
+    | Splat of {byt: t; siz: t}
+    | Memory of {siz: t; arr: t}
+    | Concat of {args: t vector}
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
-    | Splat
-    | Memory
-    | Concat
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
     | Eq
@@ -167,12 +168,12 @@ end = struct
     | App of {op: t; arg: t}
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
+    | Splat of {byt: t; siz: t}
+    | Memory of {siz: t; arr: t}
+    | Concat of {args: t vector}
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
-    | Splat
-    | Memory
-    | Concat
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
     | Eq
@@ -211,6 +212,7 @@ type _t = T0.t
 
 include T
 
+let empty_map = Map.empty (module T)
 let empty_qset = Qset.empty (module T)
 let sorted e f = compare e f <= 0
 let sort e f = if sorted e f then (e, f) else (f, e)
@@ -250,12 +252,9 @@ let rec pp fs exp =
     | Nondet {msg} -> pf "nondet \"%s\"" msg
     | Label {name} -> pf "%s" name
     | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
-    | Splat -> pf "^"
-    | Memory -> pf "⟨_,_⟩"
-    | App {op= Memory; arg= siz} -> pf "@<1>⟨%a,_@<1>⟩" pp siz
-    | App {op= App {op= Memory; arg= siz}; arg= bytes} ->
-        pf "@<1>⟨%a,%a@<1>⟩" pp siz pp bytes
-    | Concat -> pf "^"
+    | Splat {byt; siz} -> pf "%a^%a" pp byt pp siz
+    | Memory {siz; arr} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
+    | Concat {args} -> pf "%a" (Vector.pp "@,^" pp) args
     | Integer {data} -> pf "%a" Z.pp data
     | Float {data} -> pf "%s" data
     | Eq -> pf "="
@@ -363,10 +362,10 @@ let typ_of = function
 
 let typ = typ_of
 
-let type_check typ e =
+let type_check e typ =
   assert (Option.for_all ~f:(Typ.castable typ) (typ_of e))
 
-let type_check2 typ e f = type_check typ e ; type_check typ f
+let type_check2 e f typ = type_check e typ ; type_check f typ
 
 (* an indeterminate (factor of a monomial) is any non-Add/Mul/Integer exp *)
 let rec assert_indeterminate = function
@@ -453,7 +452,16 @@ let invariant ?(partial = false) e =
       | Some typ, Some typ' -> assert (Typ.castable typ typ')
       | _ -> assert true )
     | _ -> assert_arity 2 )
-  | Splat | Memory | Concat | Ord | Uno | Select -> assert_arity 2
+  | Concat {args} -> assert (Vector.length args <> 1)
+  | Splat {byt; siz} -> (
+      assert (Option.exists ~f:(Typ.convertible Typ.byt) (typ_of byt)) ;
+      assert (Option.exists ~f:(Typ.convertible Typ.siz) (typ_of siz)) ;
+      match siz with
+      | Integer {data} -> assert (not (Z.equal Z.zero data))
+      | _ -> () )
+  | Memory {siz} ->
+      assert (Option.for_all ~f:(Typ.convertible Typ.siz) (typ_of siz))
+  | Ord | Uno | Select -> assert_arity 2
   | Conditional | Update -> assert_arity 3
   | Record -> assert (partial || not (List.is_empty args))
   | Struct_rec {elts} ->
@@ -552,7 +560,7 @@ module Var = struct
              Format.fprintf fs "@[[%a ↦ %a]@]" pp_t k pp_t v ))
         (Map.to_alist s)
 
-    let empty = Map.empty (module T)
+    let empty = empty_map
     let is_empty = Map.is_empty
 
     let freshen vs ~wrt =
@@ -607,11 +615,14 @@ let fold_exps e ~init ~f =
   let fold_exps_ fold_exps_ e z =
     let z =
       match e with
-      | App {op; arg} -> fold_exps_ op (fold_exps_ arg z)
+      | App {op= x; arg= y}
+       |Splat {byt= x; siz= y}
+       |Memory {siz= x; arr= y} ->
+          fold_exps_ y (fold_exps_ x z)
       | Add {args} | Mul {args} ->
           Qset.fold args ~init:z ~f:(fun arg _ z -> fold_exps_ arg z)
-      | Struct_rec {elts} ->
-          Vector.fold elts ~init:z ~f:(fun z elt -> fold_exps_ elt z)
+      | Concat {args} | Struct_rec {elts= args} ->
+          Vector.fold args ~init:z ~f:(fun z elt -> fold_exps_ elt z)
       | _ -> z
     in
     f z e
@@ -1041,15 +1052,22 @@ let simp_ashr x y =
 
 let iter e ~f =
   match e with
-  | App {op; arg} -> f op ; f arg
+  | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
+    ->
+      f x ; f y
   | Add {args} | Mul {args} -> Qset.iter ~f:(fun arg _ -> f arg) args
+  | Concat {args} | Struct_rec {elts= args} -> Vector.iter ~f args
   | _ -> ()
 
 let fold e ~init:s ~f =
   match e with
-  | App {op; arg} -> f op (f arg s)
+  | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
+    ->
+      f y (f x s)
   | Add {args} | Mul {args} ->
       Qset.fold ~f:(fun e _ s -> f e s) args ~init:s
+  | Concat {args} | Struct_rec {elts= args} ->
+      Vector.fold ~f:(fun s e -> f e s) args ~init:s
   | _ -> s
 
 let for_all e ~f = fold ~f:(fun a so_far -> so_far && f a) ~init:true e
@@ -1110,16 +1128,46 @@ let addN typ args = simp_add typ args |> check invariant
 let mulN typ args = simp_mul typ args |> check invariant
 
 let check1 op typ x =
-  type_check typ x ;
+  type_check x typ ;
   op typ x |> check invariant
 
 let check2 op typ x y =
-  type_check2 typ x y ;
+  type_check2 x y typ ;
   op typ x y |> check invariant
 
-let splat ~byt ~siz = app2 Splat byt siz
-let memory ~siz ~arr = app2 Memory siz arr
-let concat = app2 Concat
+let simp_memory siz arr = Memory {siz; arr}
+
+let memory ~siz ~arr =
+  type_check siz Typ.siz ;
+  simp_memory siz arr |> check invariant
+
+let simp_concat xs =
+  if Vector.length xs = 1 then Vector.get xs 0
+  else
+    let args =
+      if Vector.for_all xs ~f:(function Concat _ -> false | _ -> true)
+      then xs
+      else
+        Vector.concat
+          (Vector.fold_right xs ~init:[] ~f:(fun x s ->
+               match x with
+               | Concat {args} -> args :: s
+               | x -> Vector.of_array [|x|] :: s ))
+    in
+    Concat {args}
+
+let concat xs = simp_concat (Vector.of_array xs) |> check invariant
+
+let simp_splat byt siz =
+  match siz with
+  | Integer {data} when Z.equal Z.zero data -> concat [||]
+  | _ -> Splat {byt; siz}
+
+let splat ~byt ~siz =
+  type_check byt Typ.byt ;
+  type_check siz Typ.siz ;
+  simp_splat byt siz |> check invariant
+
 let eq = app2 Eq
 let dq = app2 Dq
 let gt = app2 Gt
@@ -1180,20 +1228,38 @@ let convert ?(signed = false) ~dst ~src exp =
 (** Transform *)
 
 let map e ~f =
+  let map_bin mk ~f x y =
+    let x' = f x in
+    let y' = f y in
+    if x' == x && y' == y then e else mk x' y'
+  in
+  let map_vector mk ~f args =
+    let args' = Vector.map_preserving_phys_equal ~f args in
+    if args' == args then e else mk args'
+  in
   let map_qset mk typ ~f args =
     let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
     if args' == args then e else mk typ args'
   in
   match e with
-  | App {op; arg} ->
-      let op' = f op in
-      let arg' = f arg in
-      if op' == op && arg' == arg then e else app1 ~partial:true op' arg'
+  | App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg
   | Add {args; typ} -> map_qset addN typ ~f args
   | Mul {args; typ} -> map_qset mulN typ ~f args
+  | Splat {byt; siz} -> map_bin simp_splat ~f byt siz
+  | Memory {siz; arr} -> map_bin simp_memory ~f siz arr
+  | Concat {args} -> map_vector simp_concat ~f args
   | _ -> e
 
 let fold_map e ~init:s ~f =
+  let fold_map_bin mk ~f x y ~init:s =
+    let s, x' = f s x in
+    let s, y' = f s y in
+    if x' == x && y' == y then (s, e) else (s, mk x' y')
+  in
+  let fold_map_vector mk ~f ~init args =
+    let s, args' = Vector.fold_map args ~init ~f in
+    if args' == args then (s, e) else (s, mk args')
+  in
   let fold_map_qset mk typ ~f ~init args =
     let args', s =
       Qset.fold_map args ~init ~f:(fun x q s ->
@@ -1203,13 +1269,12 @@ let fold_map e ~init:s ~f =
     if args' == args then (s, e) else (s, mk typ args')
   in
   match e with
-  | App {op; arg} ->
-      let s, op' = f s op in
-      let s, arg' = f s arg in
-      if op' == op && arg' == arg then (s, e)
-      else (s, app1 ~partial:true op' arg')
+  | App {op; arg} -> fold_map_bin (app1 ~partial:true) ~f op arg ~init:s
   | Add {args; typ} -> fold_map_qset addN typ ~f args ~init:s
   | Mul {args; typ} -> fold_map_qset mulN typ ~f args ~init:s
+  | Splat {byt; siz} -> fold_map_bin simp_splat ~f byt siz ~init:s
+  | Memory {siz; arr} -> fold_map_bin simp_memory ~f siz arr ~init:s
+  | Concat {args} -> fold_map_vector simp_concat ~f args ~init:s
   | _ -> (s, e)
 
 let rename e sub =
@@ -1279,13 +1344,17 @@ let is_false = function
   | Integer {data; typ= Integer {bits= 1}} -> Z.is_false data
   | _ -> false
 
-let is_simple = function App _ | Add _ | Mul _ -> false | _ -> true
-
-let rec is_constant = function
+let rec is_constant e =
+  let is_constant_bin x y = is_constant x && is_constant y in
+  match e with
   | Var _ | Nondet _ -> false
-  | App {op; arg} -> is_constant arg && is_constant op
+  | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
+    ->
+      is_constant_bin x y
   | Add {args} | Mul {args} ->
       Qset.for_all ~f:(fun arg _ -> is_constant arg) args
+  | Concat {args} | Struct_rec {elts= args} ->
+      Vector.for_all ~f:is_constant args
   | _ -> true
 
 let classify = function
@@ -1296,25 +1365,43 @@ let classify = function
 let solve e f =
   [%Trace.call fun {pf} -> pf "%a@ %a" pp e pp f]
   ;
-  ( match (typ e, typ f) with
-  | Some typ, _ | _, Some typ -> (
-    match sub typ e f with
-    | Add {args} ->
-        let c, q = Qset.min_elt_exn args in
-        let n = Sum.to_exp typ (Qset.remove args c) in
-        let d = rational (Q.neg q) typ in
-        let r = div n d in
-        Some (c, r)
-    | e_f ->
-        let z = integer Z.zero typ in
-        if is_constant e_f && not (equal e_f z) then None else Some (e_f, z)
-    )
-  | _ ->
+  let rec solve_ e f s =
+    let solve_uninterp e f =
       let ord = compare e f in
       if is_constant e && is_constant f && ord <> 0 then None
-      else if ord < 0 then Some (f, e)
-      else Some (e, f) )
+      else
+        (* orient equation to choose preferred class representative *)
+        let key, data = if ord > 0 then (e, f) else (f, e) in
+        Some (Map.add_exn s ~key ~data)
+    in
+    match (e, f) with
+    | (Add {typ} | Mul {typ} | Integer {typ}), _
+     |_, (Add {typ} | Mul {typ} | Integer {typ}) -> (
+      match sub typ e f with
+      | Add {args} ->
+          let c, q = Qset.min_elt_exn args in
+          let n = Sum.to_exp typ (Qset.remove args c) in
+          let d = rational (Q.neg q) typ in
+          let r = div n d in
+          Some (Map.add_exn s ~key:c ~data:r)
+      | e_f ->
+          let z = integer Z.zero typ in
+          if is_constant e_f && not (equal e_f z) then None
+          else solve_uninterp e_f z )
+    | Concat {args= ms}, Concat {args= ns} -> (
+        let siz args =
+          Vector.fold_until args ~init:(integer Z.zero Typ.siz)
+            ~f:(fun sum -> function
+              | Memory {siz} -> Continue (add Typ.siz siz sum)
+              | _ -> Stop None )
+            ~finish:(fun _ -> None)
+        in
+        match (siz ms, siz ns) with
+        | Some p, Some q -> solve_uninterp e f >>= solve_ p q
+        | _ -> solve_uninterp e f )
+    | _ -> solve_uninterp e f
+  in
+  solve_ e f empty_map
   |>
   [%Trace.retn fun {pf} ->
-    function
-    | Some (e, f) -> pf "%a @<2>↦ %a" pp e pp f | None -> pf "false"]
+    function Some s -> pf "%a" Var.Subst.pp s | None -> pf "false"]

sledge/src/llair/exp.mli

@@ -30,15 +30,16 @@ and t = private
       (** Application of function symbol to argument, curried *)
   | Add of {args: qset; typ: Typ.t}  (** Addition *)
   | Mul of {args: qset; typ: Typ.t}  (** Multiplication *)
+  | Splat of {byt: t; siz: t}
+      (** Iterated concatenation of a single byte *)
+  | Memory of {siz: t; arr: t}  (** Size-tagged byte-array *)
+  | Concat of {args: t vector}  (** Byte-array concatenation *)
   | Var of {id: int; name: string}  (** Local variable / virtual register *)
   | Nondet of {msg: string}
       (** Anonymous local variable with arbitrary value, representing
           non-deterministic approximation of value described by [msg] *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
-  | Splat  (** Iterated concatenation of a single byte *)
-  | Memory  (** Size-tagged byte-array *)
-  | Concat  (** Byte-array concatenation *)
   | Integer of {data: Z.t; typ: Typ.t}
       (** Integer constant, or if [typ] is a [Pointer], null pointer value
           that never refers to an object *)
@@ -137,7 +138,7 @@ val label : parent:string -> name:string -> t
 val null : t
 val splat : byt:t -> siz:t -> t
 val memory : siz:t -> arr:t -> t
-val concat : t -> t -> t
+val concat : t array -> t
 val bool : bool -> t
 val integer : Z.t -> Typ.t -> t
 val rational : Q.t -> Typ.t -> t
@@ -218,8 +219,7 @@ val rename : t -> Var.Subst.t -> t
 val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
-val is_simple : t -> bool
 val is_constant : t -> bool
 val typ : t -> Typ.t option
 val classify : t -> [> `Atomic | `Interpreted | `Uninterpreted]
-val solve : t -> t -> (t * t) option
+val solve : t -> t -> (t, t, comparator_witness) Map.t option

sledge/src/llair/typ.ml

@@ -101,11 +101,12 @@ let struct_ =
 (** Constants *)
 
 let bool = integer ~bits:1
+let byt = integer ~bits:8
 let siz = integer ~bits:64
 
 (** [ptr] is semantically equivalent to [siz], but has a distinct
     representation because the element type is important for [Global]s *)
-let ptr = pointer ~elt:(integer ~bits:8)
+let ptr = pointer ~elt:byt
 
 (** Queries *)
 

sledge/src/llair/typ.mli

@@ -34,6 +34,7 @@ include Invariant.S with type t := t
 (** Constructors *)
 
 val bool : t
+val byt : t
 val siz : t
 val ptr : t
 val function_ : return:t option -> args:t vector -> t

sledge/src/symbheap/congruence.ml

@@ -251,12 +251,14 @@ let map_base ai ~f =
       if a' == a then ai else Exp.add typ a' (Exp.rational i typ)
   | None -> f ai
 
+let is_simple = function Exp.App _ | Add _ | Mul _ -> false | _ -> true
+
 (** [norm_base r a] is [a'+k] where [r] implies [a = a'+k] and [a'] is a
     rep, requires [a] to not have any offset and be in the carrier *)
 let norm_base r e =
   assert (Option.is_none (Exp.offset e)) ;
   try Map.find_exn r.rep e with Caml.Not_found ->
-    assert (Exp.is_simple e) ;
+    assert (is_simple e) ;
     e
 
 (** [norm r a+i] is [a'+k] where [r] implies [a+i = a'+k] and [a'] is a rep,
@@ -265,7 +267,7 @@ let norm r e = map_base ~f:(norm_base r) e
 
 (** test membership in carrier, strictly in the sense that an exp with an
     offset is not in the carrier even when its base is *)
-let in_car r e = Exp.is_simple e || Map.mem r.rep e
+let in_car r e = is_simple e || Map.mem r.rep e
 
 (** test if an exp is a representative, requires exp to have no offset *)
 let is_rep r e = Exp.equal e (norm_base r e)
@@ -285,7 +287,7 @@ let pre_invariant r =
       let a', a_k = solve_for_base a'k a in
       (* carrier is closed under rep *)
       assert (in_car r a') ;
-      if Exp.is_simple a' then
+      if is_simple a' then
         (* rep is sparse for symbols *)
         assert (
           (not (Map.mem r.rep a'))
@@ -331,7 +333,7 @@ let pre_invariant r =
         || Trace.fail "empty use list should not have been added" ) ;
       Use.iter a_use ~f:(fun u ->
           (* uses are applications *)
-          assert (not (Exp.is_simple u)) ;
+          assert (not (is_simple u)) ;
           (* uses have no offsets *)
           assert (Option.is_none (Exp.offset u)) ;
           (* subexps of uses in carrier *)
@@ -440,7 +442,7 @@ let add_directed_equation r0 ~exp:bj ~rep:ai =
         let c, aijk = solve_for_base ck aij in
         let r =
           if Exp.equal a c || Exp.is_false (Exp.eq c aijk) then false_
-          else if Exp.is_simple c && Exp.equal c aijk then r
+          else if is_simple c && Exp.equal c aijk then r
           else {r with rep= Map.set r.rep ~key:c ~data:aijk}
         in
         (* a+i-j-k = c so a = c-i+j+k *)
@@ -527,7 +529,7 @@ let rec norm_extend r ek =
   [%Trace.call fun {pf} -> pf "%a@ %a" Exp.pp ek pp r]
   ;
   let e = Exp.base ek in
-  ( if Exp.is_simple e then (r, norm r ek)
+  ( if is_simple e then (r, norm r ek)
   else
     Map.find_or_add r.rep e
       ~if_found:(fun e' ->

sledge/src/symbheap/equality.ml

@@ -142,14 +142,12 @@ let rec extend a r =
 
 let extend a r = extend a r |> check invariant
 
-let compose r a a' =
-  let s = Map.singleton (module Exp) a a' in
+let compose r s =
   let rep = Map.map ~f:(norm s) r.rep in
   let rep =
-    Map.update rep a ~f:(function
-      | None -> a'
-      | Some b when Exp.equal a' b -> b
-      | _ -> fail "domains intersect: %a" Exp.pp a () )
+    Map.merge_skewed rep s ~combine:(fun ~key v1 v2 ->
+        if Exp.equal v1 v2 then v1
+        else fail "domains intersect: %a" Exp.pp key () )
   in
   {r with rep} |> check invariant
 
@@ -157,7 +155,7 @@ let merge a b r =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
   ;
   ( match Exp.solve a b with
-  | Some (c, c') -> compose r c c'
+  | Some s -> compose r s
   | None -> {r with sat= false} )
   |>
   [%Trace.retn fun {pf} r' ->

sledge/src/symbheap/equality_test.ml

@@ -108,13 +108,13 @@ let%test_module _ =
       pp r2 ;
       [%expect
         {|
-          %x_5 = ((i64)(i8) %x_5) = %y_6 = %z_7
+          ((i64)(i8) %x_5) = %x_5 = %y_6 = %z_7
 
           {sat= true;
-           rep= [[((i64)(i8) %x_5) ↦ %x_5];
-                 [%x_5 ↦ ];
-                 [%y_6 ↦ %x_5];
-                 [%z_7 ↦ %x_5];
+           rep= [[((i64)(i8) %x_5) ↦ ];
+                 [%x_5 ↦ ((i64)(i8) %x_5)];
+                 [%y_6 ↦ ((i64)(i8) %x_5)];
+                 [%z_7 ↦ ((i64)(i8) %x_5)];
                  [(i64)(i8) ↦ ]]} |}]
 
     let%test _ = entails_eq r2 x z

sledge/src/symbheap/exec.ml

@@ -165,8 +165,8 @@ let memmov_foot us dst src len =
   let siz_mid = Exp.sub Typ.siz len src_dst in
   let mem_mid = Exp.memory ~siz:siz_mid ~arr:arr_mid in
   let mem_src = Exp.memory ~siz:src_dst ~arr:arr_src in
-  let mem_mid_src = Exp.concat mem_mid mem_src in
-  let mem_dst_mid_src = Exp.concat mem_dst mem_mid_src in
+  let mem_mid_src = Exp.concat [|mem_mid; mem_src|] in
+  let mem_dst_mid_src = Exp.concat [|mem_dst; mem_mid_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 =
@@ -192,7 +192,7 @@ 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 = Exp.concat (Exp.concat mem_mid mem_src) mem_src in
+  let mem_mid_src_src = Exp.concat [|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 =
@@ -218,7 +218,7 @@ 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 = Exp.concat mem_src (Exp.concat mem_src mem_mid) in
+  let mem_src_src_mid = Exp.concat [|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 =

sledge/src/symbheap/solver.ml

@@ -138,8 +138,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
       (Exp.eq
          (Exp.memory ~siz:o ~arr:a)
          (Exp.concat
-            (Exp.memory ~siz:n ~arr:a0)
-            (Exp.memory ~siz:o_n ~arr:a1)))
+            [|Exp.memory ~siz:n ~arr:a0; Exp.memory ~siz:o_n ~arr:a1|]))
       (Sh.star
          (Sh.seg
             {loc= Exp.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1})
@@ -182,8 +181,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
          (Sh.and_
             (Exp.eq
                (Exp.concat
-                  (Exp.memory ~siz:o ~arr:a)
-                  (Exp.memory ~siz:n_o ~arr:a1'))
+                  [|Exp.memory ~siz:o ~arr:a; Exp.memory ~siz:n_o ~arr:a1'|])
                (Exp.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg
@@ -227,8 +225,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       (Exp.eq
          (Exp.memory ~siz:o ~arr:a)
          (Exp.concat
-            (Exp.memory ~siz:l_k ~arr:a0)
-            (Exp.memory ~siz:n ~arr:a1)))
+            [|Exp.memory ~siz:l_k ~arr:a0; Exp.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))
@@ -273,10 +270,9 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       (Exp.eq
          (Exp.memory ~siz:o ~arr:a)
          (Exp.concat
-            (Exp.memory ~siz:l_k ~arr:a0)
-            (Exp.concat
-               (Exp.memory ~siz:n ~arr:a1)
-               (Exp.memory ~siz:ko_ln ~arr:a2))))
+            [| Exp.memory ~siz:l_k ~arr:a0
+             ; Exp.memory ~siz:n ~arr:a1
+             ; Exp.memory ~siz:ko_ln ~arr:a2 |]))
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.star
@@ -325,8 +321,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
       (Exp.eq
          (Exp.memory ~siz:o ~arr:a)
          (Exp.concat
-            (Exp.memory ~siz:l_k ~arr:a0)
-            (Exp.memory ~siz:ko_l ~arr:a1)))
+            [|Exp.memory ~siz:l_k ~arr:a0; Exp.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))
@@ -337,8 +332,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
          (Sh.and_
             (Exp.eq
                (Exp.concat
-                  (Exp.memory ~siz:ko_l ~arr:a1)
-                  (Exp.memory ~siz:ln_ko ~arr:a2'))
+                  [| Exp.memory ~siz:ko_l ~arr:a1
+                   ; Exp.memory ~siz:ln_ko ~arr:a2' |])
                (Exp.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'})
@@ -377,8 +372,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (Exp.eq
                (Exp.concat
-                  (Exp.memory ~siz:k_l ~arr:a0')
-                  (Exp.memory ~siz:o ~arr:a))
+                  [|Exp.memory ~siz:k_l ~arr:a0'; Exp.memory ~siz:o ~arr:a|])
                (Exp.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
@@ -421,10 +415,9 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (Exp.eq
                (Exp.concat
-                  (Exp.memory ~siz:k_l ~arr:a0')
-                  (Exp.concat
-                     (Exp.memory ~siz:o ~arr:a)
-                     (Exp.memory ~siz:ln_ko ~arr:a2')))
+                  [| Exp.memory ~siz:k_l ~arr:a0'
+                   ; Exp.memory ~siz:o ~arr:a
+                   ; Exp.memory ~siz:ln_ko ~arr:a2' |])
                (Exp.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
@@ -470,8 +463,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
       (Exp.eq
          (Exp.memory ~siz:o ~arr:a)
          (Exp.concat
-            (Exp.memory ~siz:ln_k ~arr:a1)
-            (Exp.memory ~siz:ko_ln ~arr:a2)))
+            [|Exp.memory ~siz:ln_k ~arr:a1; Exp.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))
@@ -482,8 +474,8 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (Exp.eq
                (Exp.concat
-                  (Exp.memory ~siz:k_l ~arr:a0')
-                  (Exp.memory ~siz:ln_k ~arr:a1))
+                  [| Exp.memory ~siz:k_l ~arr:a0'
+                   ; Exp.memory ~siz:ln_k ~arr:a1 |])
                (Exp.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})