diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index afe6d8708..66ef8e43d 100644 --- a/sledge/src/llair/exp.ml +++ b/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 = diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 0352673c1..b89d90425 100644 --- a/sledge/src/llair/exp.mli +++ b/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 diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index ee810f979..fc35350ed 100644 --- a/sledge/src/llair/frontend.ml +++ b/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