From 7f727df1193363944ccc1c94aa93c49097112c6c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 10 Jan 2020 15:46:21 -0800 Subject: [PATCH] [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 | 22 ++++++++-------------- sledge/src/llair/exp.mli | 4 ++-- sledge/src/llair/frontend.ml | 6 +----- sledge/src/llair/term.ml | 15 +++++---------- sledge/src/llair/term.mli | 4 ++-- sledge/src/symbheap/exec.ml | 8 ++++---- 6 files changed, 22 insertions(+), 37 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 40df044f0..cc387831e 100644 --- a/sledge/src/llair/exp.ml +++ b/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) ; - match siz.desc with - | Integer {data} -> assert (Z.equal (Z.of_int (Typ.size_of typ)) data) - | _ -> () ) + assert (Typ.is_sized typ) | 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 = - { desc= Ap2 (Splat, typ, byt, siz) - ; term= Term.splat ~byt:byt.term ~siz:siz.term } +let splat typ byt = + {desc= Ap1 (Splat, typ, byt); term= Term.splat byt.term} |> check invariant (* records (struct / array values) *) diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 8048fbddd..30e5ff13e 100644 --- a/sledge/src/llair/exp.mli +++ b/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 diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 0845b1184..5338f18f1 100644 --- a/sledge/src/llair/frontend.ml +++ b/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 - 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)) + Exp.splat typ (Exp.integer Typ.byt Z.zero) | _ -> fail "ConstantAggregateZero of type %a" Typ.pp typ () ) | ConstantVector | ConstantArray -> let typ = xlate_type x (Llvm.type_of llv) in diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 03ccf4185..ab14fe7c9 100644 --- a/sledge/src/llair/term.ml +++ b/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 = - match siz with - | Integer {data} when Z.equal Z.zero data -> simp_concat Vector.empty - | _ -> Ap2 (Splat, byt, siz) - +let simp_splat byt = Ap1 (Splat, byt) 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 diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli index 711b5df06..b2148f646 100644 --- a/sledge/src/llair/term.mli +++ b/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 diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 316cf6588..d8166ba0b 100644 --- a/sledge/src/symbheap/exec.ml +++ b/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}