[sledge] Re-add Splat expression for zero-initialized aggregates

Summary:
This is needed since expressions distinguish between the integer or
pointer zero value and zero-initialized array/tuple/struct aggregates
based on type, and the backend distinguishes them semantically.

Reviewed By: bennostein

Differential Revision: D17801938

fbshipit-source-id: ac8665e65

sledge/src/llair/exp.ml

@@ -48,6 +48,7 @@ module T = struct
       | Lshr
       | Ashr
       (* array/struct operations *)
+      | Splat
       | Update of int
     [@@deriving compare, equal, hash, sexp]
 
@@ -130,6 +131,7 @@ 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 =
@@ -155,6 +157,7 @@ let rec pp fs exp =
     | Ap1 (Convert {dst}, src, arg) ->
         pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg
     | 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)
@@ -217,6 +220,13 @@ let rec invariant exp =
       | Array _ -> assert true
       | Tuple {elts} | Struct {elts} -> assert (valid_idx idx elts)
       | _ -> assert false )
+  | Ap2 (Splat, typ, byt, siz) -> (
+      assert (Typ.convertible Typ.byt (typ_of byt)) ;
+      assert (Typ.convertible Typ.siz (typ_of siz)) ;
+      match (Typ.prim_bit_size_of typ, siz.desc) with
+      | Some n, Integer {data} -> assert (Z.equal (Z.of_int n) data)
+      | None, Integer {data} -> assert (not (Z.equal Z.zero data))
+      | _ -> () )
   | Ap2 (Update idx, typ, rcd, elt) -> (
       assert (Typ.castable typ (typ_of rcd)) ;
       match typ with
@@ -276,7 +286,7 @@ and typ_of exp =
       Typ.bool
   | Ap2
       ( ( Add | Sub | Mul | Div | Rem | Udiv | Urem | And | Or | Xor | Shl
-        | Lshr | Ashr | Update _ )
+        | Lshr | Ashr | Splat | Update _ )
       , typ
       , _
       , _ )
@@ -462,6 +472,13 @@ let conditional ?typ ~cnd ~thn ~els =
   ; term= Term.conditional ~cnd:cnd.term ~thn:thn.term ~els:els.term }
   |> check invariant
 
+(* memory *)
+
+let splat typ ~byt ~siz =
+  { desc= Ap2 (Splat, typ, byt, siz)
+  ; term= Term.splat ~byt:byt.term ~siz:siz.term }
+  |> check invariant
+
 (* records (struct / array values) *)
 
 let record typ elts =

sledge/src/llair/exp.mli

@@ -48,6 +48,7 @@ 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]
 
@@ -176,6 +177,9 @@ val ashr : ?typ:Typ.t -> t -> t -> t
 (* if-then-else *)
 val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t
 
+(* memory *)
+val splat : Typ.t -> byt:t -> siz:t -> t
+
 (* records (struct / array values) *)
 val record : Typ.t -> t vector -> t
 val select : Typ.t -> t -> int -> t

sledge/src/llair/frontend.ml

@@ -371,7 +371,18 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
     | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
     | ConstantInt -> xlate_int x llv
     | ConstantFP -> xlate_float x llv
-    | ConstantPointerNull | ConstantAggregateZero -> Exp.null
+    | ConstantPointerNull -> Exp.null
+    | ConstantAggregateZero -> (
+        let llt = Llvm.type_of llv in
+        let typ = xlate_type x llt in
+        match typ with
+        | Integer _ -> Exp.integer typ Z.zero
+        | Pointer _ -> Exp.null
+        | Array _ | Tuple _ | Struct _ ->
+            Exp.splat typ
+              ~byt:(Exp.integer Typ.byt Z.zero)
+              ~siz:(Exp.integer Typ.siz (Z.of_int (size_of x llt)))
+        | _ -> fail "ConstantAggregateZero of type %a" Typ.pp typ () )
     | ConstantVector | ConstantArray ->
         let typ = xlate_type x (Llvm.type_of llv) in
         let len = Llvm.num_operands llv in