[sledge] Remove unused Exp constructors for memory exps

Summary:
Splat, Memory, and Concat expressions are never used. Only the term
forms are needed.

Reviewed By: bennostein

Differential Revision: D17665259

fbshipit-source-id: cbfd7650d

sledge/src/llair/exp.ml

@@ -53,10 +53,6 @@ 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 *)
     | Reg of {name: string; global: bool}
     | Nondet of {msg: string}
@@ -119,9 +115,6 @@ and T0 : sig
   type 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}
     | Reg of {name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
@@ -163,9 +156,6 @@ end = struct
   type 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}
     | Reg of {name: string; global: bool}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
@@ -245,9 +235,6 @@ 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 {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} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
     | Float {data} -> pf "%s" data
     | Eq -> pf "="
@@ -459,15 +446,6 @@ let invariant ?(partial = false) e =
       | Some typ, Some typ' -> assert (Typ.castable typ typ')
       | _ -> assert true )
     | _ -> 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))
@@ -560,13 +538,10 @@ let fold_exps e ~init ~f =
   let fold_exps_ fold_exps_ e z =
     let z =
       match e with
-      | App {op= x; arg= y}
-       |Splat {byt= x; siz= y}
-       |Memory {siz= x; arr= y} ->
-          fold_exps_ y (fold_exps_ x z)
+      | App {op= x; arg= 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)
-      | Concat {args} | Struct_rec {elts= args} ->
+      | Struct_rec {elts= args} ->
           Vector.fold args ~init:z ~f:(fun z elt -> fold_exps_ elt z)
       | _ -> z
     in
@@ -1004,11 +979,9 @@ let simp_ashr x y =
 
 let iter e ~f =
   match e with
-  | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y}
-    ->
-      f x ; f y
+  | App {op= x; arg= 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
+  | Struct_rec {elts= args} -> Vector.iter ~f args
   | _ -> ()
 
 let is_subexp ~sub ~sup =
@@ -1075,39 +1048,6 @@ let check2 op typ x y =
   type_check2 x y typ ;
   op typ x y |> check invariant
 
-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

sledge/src/llair/exp.mli

@@ -23,10 +23,6 @@ type qset = (t, comparator_witness) Qset.t
 and t = private
   | 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 *)
   | Reg of {name: string; global: bool}
       (** Local variable / virtual register *)
   | Nondet of {msg: string}
@@ -121,8 +117,6 @@ val reg : Reg.t -> t
 val nondet : string -> t
 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 bool : bool -> t
 val integer : Z.t -> Typ.t -> t
 val float : string -> t

sledge/src/symbheap/term.ml

@@ -1257,9 +1257,6 @@ let rec of_exp (e : Exp.t) =
   match e with
   | Add {args; typ} -> Add {args= of_exps args; typ}
   | Mul {args; typ} -> Mul {args= of_exps args; typ}
-  | Splat {byt; siz} -> Splat {byt= of_exp byt; siz= of_exp siz}
-  | Memory {siz; arr} -> Memory {siz= of_exp siz; arr= of_exp arr}
-  | Concat {args} -> Concat {args= Vector.map ~f:of_exp args}
   | Reg {name} -> Var {id= 0; name}
   | Nondet {msg} -> Nondet {msg}
   | Label {parent; name} -> Label {parent; name}