From 0903355a0e957be2e0de24688ed76aa3556ee9a7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 8 Oct 2019 06:25:00 -0700 Subject: [PATCH] [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 | 68 +++---------------------------------- sledge/src/llair/exp.mli | 6 ---- sledge/src/symbheap/term.ml | 3 -- 3 files changed, 4 insertions(+), 73 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index d5b805156..3f9f0d9d3 100644 --- a/sledge/src/llair/exp.ml +++ b/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 diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index ae4bf3a5b..18cfd7bf9 100644 --- a/sledge/src/llair/exp.mli +++ b/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 diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml index c99b97505..fe958d20c 100644 --- a/sledge/src/symbheap/term.ml +++ b/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}