[sledge] Remove size of Splat exps and terms

Summary:
The size of Splats is redundant, as they always appear as subterms of
a Memory chunk or a heap segment, both of which are sized.

Reviewed By: ngorogiannis

Differential Revision: D19221870

fbshipit-source-id: 74044d1ad

sledge/src/llair/exp.ml

@@ -17,6 +17,7 @@ module T = struct
       | Unsigned of {bits: int}
       | Convert of {src: Typ.t}
       (* array/struct operations *)
+      | Splat
       | Select of int
     [@@deriving compare, equal, hash, sexp]
 
@@ -50,7 +51,6 @@ module T = struct
       | Lshr
       | Ashr
       (* array/struct operations *)
-      | Splat
       | Update of int
     [@@deriving compare, equal, hash, sexp]
 
@@ -133,7 +133,6 @@ let pp_op2 fs op =
   | Shl -> pf "shl"
   | Lshr -> pf "lshr"
   | Ashr -> pf "ashr"
-  | Splat -> pf "^"
   | Update idx -> pf "[_|%i→_]" idx
 
 let rec pp fs exp =
@@ -158,8 +157,8 @@ let rec pp fs exp =
         pf "((%a)(u%i)@ %a)" Typ.pp dst bits pp arg
     | Ap1 (Convert {src}, dst, arg) ->
         pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg
+    | Ap1 (Splat, _, byt) -> pf "%a^" pp byt
     | Ap1 (Select idx, _, rcd) -> pf "%a[%i]" pp rcd idx
-    | Ap2 (Splat, _, byt, siz) -> pf "%a^%a" pp byt pp siz
     | Ap2 (Update idx, _, rcd, elt) ->
         pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
     | Ap2 (Xor, Integer {bits= 1}, {desc= Integer {data}}, x)
@@ -232,13 +231,9 @@ let rec invariant exp =
       | Array _ -> assert true
       | Tuple {elts} | Struct {elts} -> assert (valid_idx idx elts)
       | _ -> assert false )
-  | Ap2 (Splat, typ, byt, siz) -> (
+  | Ap1 (Splat, typ, byt) ->
       assert (Typ.convertible Typ.byt (typ_of byt)) ;
-      assert (Typ.convertible Typ.siz (typ_of siz)) ;
+      assert (Typ.is_sized typ)
-      assert (Typ.is_sized typ) ;
-      match siz.desc with
-      | Integer {data} -> assert (Z.equal (Z.of_int (Typ.size_of typ)) data)
-      | _ -> () )
   | Ap2 (Update idx, typ, rcd, elt) -> (
       assert (Typ.castable typ (typ_of rcd)) ;
       match typ with
@@ -284,7 +279,7 @@ and typ_of exp =
   match exp.desc with
   | Reg {typ} | Nondet {typ} | Integer {typ} | Float {typ} -> typ
   | Label _ -> Typ.ptr
-  | Ap1 ((Signed _ | Unsigned _ | Convert _), dst, _) -> dst
+  | Ap1 ((Signed _ | Unsigned _ | Convert _ | Splat), dst, _) -> dst
   | Ap1 (Select idx, typ, _) -> (
     match typ with
     | Array {elt} -> elt
@@ -298,7 +293,7 @@ and typ_of exp =
       Typ.bool
   | Ap2
       ( ( Add | Sub | Mul | Div | Rem | Udiv | Urem | And | Or | Xor | Shl
-        | Lshr | Ashr | Splat | Update _ )
+        | Lshr | Ashr | Update _ )
       , typ
       , _
       , _ )
@@ -489,9 +484,8 @@ let conditional ?typ ~cnd ~thn ~els =
 
 (* memory *)
 
-let splat typ ~byt ~siz =
+let splat typ byt =
-  { desc= Ap2 (Splat, typ, byt, siz)
+  {desc= Ap1 (Splat, typ, byt); term= Term.splat byt.term}
-  ; term= Term.splat ~byt:byt.term ~siz:siz.term }
   |> check invariant
 
 (* records (struct / array values) *)

sledge/src/llair/exp.mli

@@ -30,6 +30,7 @@ type op1 =
           to type [dst], possibly with loss of information. The [src] and
           [dst] types must be [Typ.convertible] and must not both be
           [Integer] types. *)
+  | Splat  (** Iterated concatenation of a single byte *)
   | Select of int  (** Select an index from a record *)
 [@@deriving compare, equal, hash, sexp]
 
@@ -59,7 +60,6 @@ type op2 =
   | Shl  (** Shift left, bitwise *)
   | Lshr  (** Logical shift right, bitwise *)
   | Ashr  (** Arithmetic shift right, bitwise *)
-  | Splat  (** Iterated concatenation of a single byte *)
   | Update of int  (** Constant record with updated index *)
 [@@deriving compare, equal, hash, sexp]
 
@@ -194,7 +194,7 @@ val ashr : ?typ:Typ.t -> t -> t -> t
 val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t
 
 (* memory *)
-val splat : Typ.t -> byt:t -> siz:t -> t
+val splat : Typ.t -> t -> t
 
 (* records (struct / array values) *)
 val record : Typ.t -> t vector -> t

sledge/src/llair/frontend.ml

@@ -399,11 +399,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
         | Integer _ -> Exp.integer typ Z.zero
         | Pointer _ -> Exp.null
         | Array _ | Tuple _ | Struct _ ->
-            let siz = Typ.size_of typ in
+            Exp.splat typ (Exp.integer Typ.byt Z.zero)
-            if siz = 0 then todo "ConstantAggregateZero of size 0" () ;
-            Exp.splat typ
-              ~byt:(Exp.integer Typ.byt Z.zero)
-              ~siz:(Exp.integer Typ.siz (Z.of_int siz))
         | _ -> fail "ConstantAggregateZero of type %a" Typ.pp typ () )
     | ConstantVector | ConstantArray ->
         let typ = xlate_type x (Llvm.type_of llv) in

sledge/src/llair/term.ml

@@ -13,6 +13,7 @@ type op1 =
   | Signed of {bits: int}
   | Unsigned of {bits: int}
   | Convert of {src: Typ.t; dst: Typ.t}
+  | Splat
   | Select of int
 [@@deriving compare, equal, hash, sexp]
 
@@ -31,7 +32,6 @@ type op2 =
   | Shl
   | Lshr
   | Ashr
-  | Splat
   | Memory
   | Update of int
 [@@deriving compare, equal, hash, sexp]
@@ -196,7 +196,7 @@ let rec ppx strength fs term =
     | Ap2 (Ashr, x, y) -> pf "(%a@ ashr %a)" pp x pp y
     | Ap3 (Conditional, cnd, thn, els) ->
         pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els
-    | Ap2 (Splat, byt, siz) -> pf "%a^%a" pp byt pp siz
+    | Ap1 (Splat, byt) -> pf "%a^" pp byt
     | Ap2 (Memory, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
     | ApN (Concat, args) -> pf "%a" (Vector.pp "@,^" pp) args
     | ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts
@@ -283,7 +283,6 @@ let invariant e =
   match e with
   | Add _ -> assert_polynomial e |> Fn.id
   | Mul _ -> assert_monomial e |> Fn.id
-  | Ap2 (Splat, _, Integer {data}) -> assert (not (Z.equal Z.zero data))
   | ApN (Concat, mems) -> assert (Vector.length mems <> 1)
   | ApN (Record, elts) | RecN (Record, elts) ->
       assert (not (Vector.is_empty elts))
@@ -792,11 +791,7 @@ let simp_concat xs =
     in
     ApN (Concat, args)
 
-let simp_splat byt siz =
+let simp_splat byt = Ap1 (Splat, byt)
-  match siz with
-  | Integer {data} when Z.equal Z.zero data -> simp_concat Vector.empty
-  | _ -> Ap2 (Splat, byt, siz)
-
 let simp_memory siz arr = Ap2 (Memory, siz, arr)
 
 (* records *)
@@ -834,12 +829,12 @@ let norm1 op x =
   | Signed {bits} -> simp_signed bits x
   | Unsigned {bits} -> simp_unsigned bits x
   | Convert {src; dst} -> simp_convert src dst x
+  | Splat -> simp_splat x
   | Select idx -> simp_select idx x )
   |> check invariant
 
 let norm2 op x y =
   ( match op with
-  | Splat -> simp_splat x y
   | Memory -> simp_memory x y
   | Eq -> simp_eq x y
   | Dq -> simp_dq x y
@@ -892,7 +887,7 @@ let shl = norm2 Shl
 let lshr = norm2 Lshr
 let ashr = norm2 Ashr
 let conditional ~cnd ~thn ~els = norm3 Conditional cnd thn els
-let splat ~byt ~siz = norm2 Splat byt siz
+let splat byt = norm1 Splat byt
 let memory ~siz ~arr = norm2 Memory siz arr
 let concat xs = normN Concat (Vector.of_array xs)
 let record elts = normN Record elts

sledge/src/llair/term.mli

@@ -26,6 +26,7 @@ type op1 =
           to type [dst], possibly with loss of information. The [src] and
           [dst] types must be [Typ.convertible] and must not both be
           [Integer] types. *)
+  | Splat  (** Iterated concatenation of a single byte *)
   | Select of int  (** Select an index from a record *)
 [@@deriving compare, equal, hash, sexp]
 
@@ -44,7 +45,6 @@ type op2 =
   | Shl  (** Shift left, bitwise *)
   | Lshr  (** Logical shift right, bitwise *)
   | Ashr  (** Arithmetic shift right, bitwise *)
-  | Splat  (** Iterated concatenation of a single byte *)
   | Memory  (** Size-tagged byte-array *)
   | Update of int  (** Constant record with updated index *)
 [@@deriving compare, equal, hash, sexp]
@@ -212,7 +212,7 @@ val ashr : t -> t -> t
 val conditional : cnd:t -> thn:t -> els:t -> t
 
 (* memory contents *)
-val splat : byt:t -> siz:t -> t
+val splat : t -> t
 val memory : siz:t -> arr:t -> t
 val concat : t array -> t
 

sledge/src/symbheap/exec.ml

@@ -94,12 +94,12 @@ let store_spec us ptr exp len =
 
 (* { d-[b;m)->⟨l,α⟩ }
  *   memset l d b
- * { d-[b;m)->⟨l,b^l⟩ }
+ * { d-[b;m)->⟨l,b^⟩ }
  *)
 let memset_spec us dst byt len =
   let {us= _; xs; seg} = fresh_seg ~loc:dst ~siz:len us in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with arr= Term.splat ~byt ~siz:len} in
+  let post = Sh.seg {seg with arr= Term.splat byt} in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d=s * l=0 * d-[b;m)->⟨l,α⟩ }
@@ -305,7 +305,7 @@ let mallocx_spec us reg siz =
 
 (* { emp }
  *   calloc r [n × l]
- * { r=0 ∨ r-[r;(n×l)Θ)->⟨(n×l)Θ,0^(n×l)Θ⟩ }
+ * { r=0 ∨ r-[r;(n×l)Θ)->⟨(n×l)Θ,0^⟩ }
  *)
 let calloc_spec us reg num len =
   let foot = Sh.emp in
@@ -313,7 +313,7 @@ let calloc_spec us reg num len =
   let sub, ms, us = assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) ~us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
-  let arr = Term.splat ~byt:Term.zero ~siz in
+  let arr = Term.splat Term.zero in
   let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~arr us in
   let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}