From 162f027249f2c97bef4c28f80d71d97db310d669 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 10 Oct 2019 06:16:35 -0700 Subject: [PATCH] [sledge] Make type argument of Exp constructors optional where computable Reviewed By: bennostein Differential Revision: D17665251 fbshipit-source-id: 4d8bccfe8 --- sledge/src/control.ml | 7 +- sledge/src/llair/exp.ml | 146 ++++++++++------------------------ sledge/src/llair/exp.mli | 53 ++++++------ sledge/src/llair/frontend.ml | 31 ++++---- sledge/src/llair/term_test.ml | 4 +- 5 files changed, 88 insertions(+), 153 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index a24eb7a36..49dda8bb3 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -406,15 +406,14 @@ module Make (Dom : Domain_sig.Dom) = struct | Switch {key; tbl; els} -> Vector.fold tbl ~f:(fun x (case, jump) -> - match Dom.exec_assume state (Exp.eq (Exp.typ key) key case) with + match Dom.exec_assume state (Exp.eq key case) with | Some state -> exec_jump stk state block jump |> Work.seq x | None -> x ) ~init: ( match Dom.exec_assume state (Vector.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) -> - Exp.and_ Typ.bool (Exp.dq (Exp.typ key) key case) b - )) + Exp.and_ (Exp.dq key case) b )) with | Some state -> exec_jump stk state block els | None -> Work.skip ) @@ -422,7 +421,7 @@ module Make (Dom : Domain_sig.Dom) = struct Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) -> match Dom.exec_assume state - (Exp.eq Typ.ptr ptr + (Exp.eq ptr (Exp.label ~parent:(Reg.name jump.dst.parent.name.reg) ~name:jump.dst.lbl)) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 45c593f3c..9634516a7 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -284,8 +284,6 @@ and typ_of exp = typ [@@warning "-9"] -let typ = typ_of - type exp = t let pp_exp = pp @@ -406,121 +404,59 @@ let convert ?(unsigned = false) ~dst ~src exp = (* comparisons *) -let unsigned typ op x y = - let bits = Option.value_exn (Typ.prim_bit_size_of typ) in - op - (Term.extract ~unsigned:true ~bits x) - (Term.extract ~unsigned:true ~bits y) - -let eq typ x y = - {desc= Ap2 (Eq, typ, x, y); term= Term.eq x.term y.term} - |> check invariant - -let dq typ x y = - {desc= Ap2 (Dq, typ, x, y); term= Term.dq x.term y.term} - |> check invariant - -let gt typ x y = - {desc= Ap2 (Gt, typ, x, y); term= Term.lt y.term x.term} - |> check invariant - -let ge typ x y = - {desc= Ap2 (Ge, typ, x, y); term= Term.le y.term x.term} - |> check invariant - -let lt typ x y = - {desc= Ap2 (Lt, typ, x, y); term= Term.lt x.term y.term} - |> check invariant - -let le typ x y = - {desc= Ap2 (Le, typ, x, y); term= Term.le x.term y.term} - |> check invariant - -let ugt typ x y = - {desc= Ap2 (Ugt, typ, x, y); term= unsigned typ Term.lt y.term x.term} - |> check invariant - -let uge typ x y = - {desc= Ap2 (Uge, typ, x, y); term= unsigned typ Term.le y.term x.term} - |> check invariant - -let ult typ x y = - {desc= Ap2 (Ult, typ, x, y); term= unsigned typ Term.lt x.term y.term} - |> check invariant - -let ule typ x y = - {desc= Ap2 (Ule, typ, x, y); term= unsigned typ Term.le x.term y.term} - |> check invariant - -let ord typ x y = - {desc= Ap2 (Ord, typ, x, y); term= Term.ord x.term y.term} - |> check invariant - -let uno typ x y = - {desc= Ap2 (Uno, typ, x, y); term= Term.uno x.term y.term} - |> check invariant +let binary op mk ?typ x y = + let typ = match typ with Some typ -> typ | None -> typ_of x in + {desc= Ap2 (op, typ, x, y); term= mk x.term y.term} |> check invariant + +let ubinary op mk ?typ x y = + let typ = match typ with Some typ -> typ | None -> typ_of x in + let umk x y = + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + mk + (Term.extract ~unsigned:true ~bits x) + (Term.extract ~unsigned:true ~bits y) + in + binary op umk ~typ x y + +let eq = binary Eq Term.eq +let dq = binary Dq Term.dq +let gt = binary Gt (fun x y -> Term.lt y x) +let ge = binary Ge (fun x y -> Term.le y x) +let lt = binary Lt Term.lt +let le = binary Le Term.le +let ugt = ubinary Ugt (fun x y -> Term.lt y x) +let uge = ubinary Uge (fun x y -> Term.le y x) +let ult = ubinary Ult Term.lt +let ule = ubinary Ule Term.le +let ord = binary Ord Term.ord +let uno = binary Uno Term.uno (* arithmetic *) -let add typ x y = - {desc= Ap2 (Add, typ, x, y); term= Term.add x.term y.term} - |> check invariant - -let sub typ x y = - {desc= Ap2 (Sub, typ, x, y); term= Term.sub x.term y.term} - |> check invariant - -let mul typ x y = - {desc= Ap2 (Mul, typ, x, y); term= Term.mul x.term y.term} - |> check invariant - -let div typ x y = - {desc= Ap2 (Div, typ, x, y); term= Term.div x.term y.term} - |> check invariant - -let rem typ x y = - {desc= Ap2 (Rem, typ, x, y); term= Term.rem x.term y.term} - |> check invariant - -let udiv typ x y = - {desc= Ap2 (Udiv, typ, x, y); term= unsigned typ Term.div x.term y.term} - |> check invariant - -let urem typ x y = - {desc= Ap2 (Urem, typ, x, y); term= unsigned typ Term.rem x.term y.term} - |> check invariant +let add = binary Add Term.add +let sub = binary Sub Term.sub +let mul = binary Mul Term.mul +let div = binary Div Term.div +let rem = binary Rem Term.rem +let udiv = ubinary Udiv Term.div +let urem = ubinary Urem Term.rem (* boolean / bitwise *) -let and_ typ x y = - {desc= Ap2 (And, typ, x, y); term= Term.and_ x.term y.term} - |> check invariant - -let or_ typ x y = - {desc= Ap2 (Or, typ, x, y); term= Term.or_ x.term y.term} - |> check invariant +let and_ = binary And Term.and_ +let or_ = binary Or Term.or_ (* bitwise *) -let xor typ x y = - {desc= Ap2 (Xor, typ, x, y); term= Term.xor x.term y.term} - |> check invariant - -let shl typ x y = - {desc= Ap2 (Shl, typ, x, y); term= Term.shl x.term y.term} - |> check invariant - -let lshr typ x y = - {desc= Ap2 (Lshr, typ, x, y); term= Term.lshr x.term y.term} - |> check invariant - -let ashr typ x y = - {desc= Ap2 (Ashr, typ, x, y); term= Term.ashr x.term y.term} - |> check invariant +let xor = binary Xor Term.xor +let shl = binary Shl Term.shl +let lshr = binary Lshr Term.lshr +let ashr = binary Ashr Term.ashr (* if-then-else *) -let conditional typ ~cnd ~thn ~els = +let conditional ?typ ~cnd ~thn ~els = + let typ = match typ with Some typ -> typ | None -> typ_of thn in { desc= Ap3 (Conditional, typ, cnd, thn, els) ; term= Term.conditional ~cnd:cnd.term ~thn:thn.term ~els:els.term } |> check invariant diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index b0d2aa252..0352673c1 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -141,40 +141,40 @@ val float : Typ.t -> string -> t val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t (* comparisons *) -val eq : Typ.t -> t -> t -> t -val dq : Typ.t -> t -> t -> t -val gt : Typ.t -> t -> t -> t -val ge : Typ.t -> t -> t -> t -val lt : Typ.t -> t -> t -> t -val le : Typ.t -> t -> t -> t -val ugt : Typ.t -> t -> t -> t -val uge : Typ.t -> t -> t -> t -val ult : Typ.t -> t -> t -> t -val ule : Typ.t -> t -> t -> t -val ord : Typ.t -> t -> t -> t -val uno : Typ.t -> t -> t -> t +val eq : ?typ:Typ.t -> t -> t -> t +val dq : ?typ:Typ.t -> t -> t -> t +val gt : ?typ:Typ.t -> t -> t -> t +val ge : ?typ:Typ.t -> t -> t -> t +val lt : ?typ:Typ.t -> t -> t -> t +val le : ?typ:Typ.t -> t -> t -> t +val ugt : ?typ:Typ.t -> t -> t -> t +val uge : ?typ:Typ.t -> t -> t -> t +val ult : ?typ:Typ.t -> t -> t -> t +val ule : ?typ:Typ.t -> t -> t -> t +val ord : ?typ:Typ.t -> t -> t -> t +val uno : ?typ:Typ.t -> t -> t -> t (* arithmetic *) -val add : Typ.t -> t -> t -> t -val sub : Typ.t -> t -> t -> t -val mul : Typ.t -> t -> t -> t -val div : Typ.t -> t -> t -> t -val rem : Typ.t -> t -> t -> t -val udiv : Typ.t -> t -> t -> t -val urem : Typ.t -> t -> t -> t +val add : ?typ:Typ.t -> t -> t -> t +val sub : ?typ:Typ.t -> t -> t -> t +val mul : ?typ:Typ.t -> t -> t -> t +val div : ?typ:Typ.t -> t -> t -> t +val rem : ?typ:Typ.t -> t -> t -> t +val udiv : ?typ:Typ.t -> t -> t -> t +val urem : ?typ:Typ.t -> t -> t -> t (* boolean / bitwise *) -val and_ : Typ.t -> t -> t -> t -val or_ : Typ.t -> t -> t -> t +val and_ : ?typ:Typ.t -> t -> t -> t +val or_ : ?typ:Typ.t -> t -> t -> t (* bitwise *) -val xor : Typ.t -> t -> t -> t -val shl : Typ.t -> t -> t -> t -val lshr : Typ.t -> t -> t -> t -val ashr : Typ.t -> t -> t -> t +val xor : ?typ:Typ.t -> t -> t -> t +val shl : ?typ:Typ.t -> t -> t -> t +val lshr : ?typ:Typ.t -> t -> t -> t +val ashr : ?typ:Typ.t -> t -> t -> t (* if-then-else *) -val conditional : Typ.t -> cnd:t -> thn:t -> els:t -> t +val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t (* records (struct / array values) *) val record : Typ.t -> t vector -> t @@ -199,6 +199,5 @@ val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a (** Query *) val term : t -> Term.t -val typ : t -> Typ.t val is_true : t -> bool val is_false : t -> bool diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index abfe97b29..106b002e3 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -331,12 +331,12 @@ let ptr_fld x ~ptr ~fld ~lltyp = let offset = Llvm_target.DataLayout.offset_of_element lltyp fld x.lldatalayout in - Exp.add Typ.ptr ptr (Exp.integer Typ.siz (Z.of_int64 offset)) + Exp.add ~typ:Typ.ptr ptr (Exp.integer Typ.siz (Z.of_int64 offset)) let ptr_idx x ~ptr ~idx ~llelt = let stride = Llvm_target.DataLayout.abi_size llelt x.lldatalayout in - Exp.add Typ.ptr ptr - (Exp.mul Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx) + Exp.add ~typ:Typ.ptr ptr + (Exp.mul ~typ:Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx) let xlate_llvm_eh_typeid_for : x -> Typ.t -> Exp.t -> Exp.t = fun x typ arg -> Exp.convert ~dst:(i32 x) ~src:typ arg @@ -457,13 +457,14 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = let arg = xlate_value x rand in Exp.convert ?unsigned ~dst ~src arg in - let binary mk = + let binary (mk : ?typ:_ -> _) = Lazy.force check_vector ; let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in - mk typ (xlate_rand 0) (xlate_rand 1) + mk ~typ (xlate_rand 0) (xlate_rand 1) in let unordered_or mk = - binary (fun typ e f -> Exp.or_ Typ.bool (Exp.uno typ e f) (mk typ e f)) + binary (fun ?typ e f -> + Exp.or_ ~typ:Typ.bool (Exp.uno ?typ e f) (mk ?typ e f) ) in ( match opcode with | AddrSpaceCast | BitCast -> cast () @@ -484,7 +485,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = | Ule -> binary Exp.ule ) | FCmp -> ( match Llvm.fcmp_predicate llv with - | None | Some False -> binary (fun _ _ _ -> Exp.false_) + | None | Some False -> binary (fun ?typ:_ _ _ -> Exp.false_) | Some Oeq -> binary Exp.eq | Some Ogt -> binary Exp.gt | Some Oge -> binary Exp.ge @@ -499,7 +500,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = | Some Ult -> unordered_or Exp.lt | Some Ule -> unordered_or Exp.le | Some Une -> unordered_or Exp.dq - | Some True -> binary (fun _ _ _ -> Exp.true_) ) + | Some True -> binary (fun ?typ:_ _ _ -> Exp.true_) ) | Add | FAdd -> binary Exp.add | Sub | FSub -> binary Exp.sub | Mul | FMul -> binary Exp.mul @@ -515,7 +516,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = | Xor -> binary Exp.xor | Select -> let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 1)) in - Exp.conditional typ ~cnd:(xlate_rand 0) ~thn:(xlate_rand 1) + Exp.conditional ~typ ~cnd:(xlate_rand 0) ~thn:(xlate_rand 1) ~els:(xlate_rand 2) | ExtractElement | InsertElement -> todo "vector operations: %a" pp_llvalue llv () @@ -1150,7 +1151,7 @@ let xlate_instr : in let match_filter i rev_blocks = jump_unwind i - (Exp.sub i32 (Exp.integer i32 Z.zero) typeid) + (Exp.sub ~typ:i32 (Exp.integer i32 Z.zero) typeid) rev_blocks in let xlate_clause i rev_blocks = @@ -1167,9 +1168,9 @@ let xlate_instr : let rec xlate_filter i = let tiI = xlate_value x (Llvm.operand clause i) in if i < num_tis - 1 then - Exp.and_ Typ.bool (Exp.dq tip tiI ti) + Exp.and_ ~typ:Typ.bool (Exp.dq ~typ:tip tiI ti) (xlate_filter (i + 1)) - else Exp.dq tip tiI ti + else Exp.dq ~typ:tip tiI ti in let key = xlate_filter 0 in let nzero, rev_blocks = match_filter i rev_blocks in @@ -1180,9 +1181,9 @@ let xlate_instr : let typ = xlate_type x (Llvm.type_of clause) in let clause = xlate_value x clause in let key = - Exp.or_ Typ.bool - (Exp.eq typ clause Exp.null) - (Exp.eq typ clause ti) + Exp.or_ ~typ:Typ.bool + (Exp.eq ~typ clause Exp.null) + (Exp.eq ~typ clause ti) in let nzero, rev_blocks = jump_unwind i typeid rev_blocks in ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) diff --git a/sledge/src/llair/term_test.ml b/sledge/src/llair/term_test.ml index 3413657b0..d79356dad 100644 --- a/sledge/src/llair/term_test.ml +++ b/sledge/src/llair/term_test.ml @@ -35,7 +35,7 @@ let%test_module _ = let%test "boolean overflow" = Term.is_true - (Exp.eq Typ.bool + (Exp.eq (Exp.integer Typ.bool Z.minus_one) (Exp.convert ~dst:Typ.bool ~src:Typ.siz (Exp.integer Typ.siz Z.one))) @@ -43,7 +43,7 @@ let%test_module _ = let%test "unsigned boolean overflow" = Term.is_true - (Exp.uge Typ.bool + (Exp.uge (Exp.integer Typ.bool Z.minus_one) (Exp.convert ~dst:Typ.bool ~src:Typ.siz (Exp.integer Typ.siz Z.one)))