From e17f8adfe94983a85e0d9fa0a273bd411314e54c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 10 Jun 2020 07:05:21 -0700 Subject: [PATCH] [sledge] Refactor: Support instruction prefix in value translation Summary: Refactor frontend translation of LLVM values, opcodes, etc. to support emitting not only a LLAIR expression, but also a sequence of instructions to be prefixed onto the uses of the resulting expression. This is currently unused, as all prefixes are empty. Later, it will be used to translate e.g. `undef` to `r := nondet(); r`. Reviewed By: jvillard Differential Revision: D21720972 fbshipit-source-id: b89bb57de --- sledge/bin/frontend.ml | 411 ++++++++++++++++++++++++----------------- 1 file changed, 237 insertions(+), 174 deletions(-) diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml index 1f65f6c53..b9cc1262a 100644 --- a/sledge/bin/frontend.ml +++ b/sledge/bin/frontend.ml @@ -326,7 +326,12 @@ let xlate_name_opt : x -> Llvm.llvalue -> Reg.t option = | Void -> None | _ -> Some (xlate_name x instr) -let memo_value : (bool * Llvm.llvalue, Exp.t) Hashtbl.t = +let pp_prefix_exp fs (insts, exp) = + Format.fprintf fs "@[%a%t%a@]" (List.pp "@ " Inst.pp) insts + (fun fs -> if List.is_empty insts then () else Format.fprintf fs "@ ") + Exp.pp exp + +let memo_value : (bool * Llvm.llvalue, Inst.t list * Exp.t) Hashtbl.t = Hashtbl.Poly.create () let memo_global : (Llvm.llvalue, Global.t) Hashtbl.t = @@ -373,19 +378,29 @@ let xlate_llvm_eh_typeid_for : x -> Typ.t -> Exp.t -> Exp.t = fun x typ arg -> Exp.convert typ ~to_:(i32 x) arg let rec xlate_intrinsic_exp stk : - string -> (x -> Llvm.llvalue -> Exp.t) option = + string -> (x -> Llvm.llvalue -> Inst.t list * Exp.t) option = fun name -> match name with | "llvm.eh.typeid.for" -> Some (fun x llv -> let rand = Llvm.operand llv 0 in - let arg = xlate_value stk x rand in + let pre, arg = xlate_value stk x rand in let src = xlate_type x (Llvm.type_of rand) in - xlate_llvm_eh_typeid_for x src arg ) + (pre, xlate_llvm_eh_typeid_for x src arg) ) | _ -> None -and xlate_value ?(inline = false) stk : x -> Llvm.llvalue -> Exp.t = +and xlate_values stk x len val_i = + let rec loop i (pre, args) = + if i < 0 then (pre, args) + else + let pre_i, arg_i = xlate_value stk x (val_i i) in + loop (i - 1) (pre_i @ pre, arg_i :: args) + in + loop (len - 1) ([], []) + +and xlate_value ?(inline = false) stk : + x -> Llvm.llvalue -> Inst.t list * Exp.t = fun x llv -> let xlate_value_ llv = match Llvm.classify_value llv with @@ -394,54 +409,54 @@ and xlate_value ?(inline = false) stk : x -> Llvm.llvalue -> Exp.t = let fname = Llvm.value_name func in match xlate_intrinsic_exp stk fname with | Some intrinsic when inline || should_inline llv -> intrinsic x llv - | _ -> Exp.reg (xlate_name x llv) ) + | _ -> ([], Exp.reg (xlate_name x llv)) ) | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg) |Argument -> - Exp.reg (xlate_name x llv) - | Function | GlobalVariable -> Exp.reg (xlate_global stk x llv).reg + ([], Exp.reg (xlate_name x llv)) + | Function | GlobalVariable -> ([], Exp.reg (xlate_global stk x llv).reg) | GlobalAlias -> xlate_value stk x (Llvm.operand llv 0) - | ConstantInt -> xlate_int x llv - | ConstantFP -> xlate_float x llv - | ConstantPointerNull -> Exp.null + | ConstantInt -> ([], xlate_int x llv) + | ConstantFP -> ([], xlate_float x llv) + | ConstantPointerNull -> ([], Exp.null) | ConstantAggregateZero -> ( let typ = xlate_type x (Llvm.type_of llv) in match typ with - | Integer _ -> Exp.integer typ Z.zero - | Pointer _ -> Exp.null + | Integer _ -> ([], Exp.integer typ Z.zero) + | Pointer _ -> ([], Exp.null) | Array _ | Tuple _ | Struct _ -> - Exp.splat typ (Exp.integer Typ.byt Z.zero) + ([], 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 let len = Llvm.num_operands llv in - let f i = xlate_value stk x (Llvm.operand llv i) in - Exp.record typ (IArray.init len ~f) + let pre, args = xlate_values stk x len (Llvm.operand llv) in + (pre, Exp.record typ (IArray.of_list args)) | ConstantDataVector -> let typ = xlate_type x (Llvm.type_of llv) in let len = Llvm.vector_size (Llvm.type_of llv) in - let f i = xlate_value stk x (Llvm.const_element llv i) in - Exp.record typ (IArray.init len ~f) + let pre, args = xlate_values stk x len (Llvm.const_element llv) in + (pre, Exp.record typ (IArray.of_list args)) | ConstantDataArray -> let typ = xlate_type x (Llvm.type_of llv) in let len = Llvm.array_length (Llvm.type_of llv) in - let f i = xlate_value stk x (Llvm.const_element llv i) in - Exp.record typ (IArray.init len ~f) + let pre, args = xlate_values stk x len (Llvm.const_element llv) in + (pre, Exp.record typ (IArray.of_list args)) | ConstantStruct -> ( let typ = xlate_type x (Llvm.type_of llv) in match List.findi llv stk with - | Some i -> Exp.rec_record i typ + | Some i -> ([], Exp.rec_record i typ) | None -> let stk = llv :: stk in - Exp.record typ - (IArray.init (Llvm.num_operands llv) ~f:(fun i -> - xlate_value stk x (Llvm.operand llv i) )) ) + let len = Llvm.num_operands llv in + let pre, args = xlate_values stk x len (Llvm.operand llv) in + (pre, Exp.record typ (IArray.of_list args)) ) | BlockAddress -> let parent = find_name (Llvm.operand llv 0) in let name = find_name (Llvm.operand llv 1) in - Exp.label ~parent ~name + ([], Exp.label ~parent ~name) | UndefValue -> let typ = xlate_type x (Llvm.type_of llv) in - Exp.nondet typ (Llvm.string_of_llvalue llv) + ([], Exp.nondet typ (Llvm.string_of_llvalue llv)) | Instruction ( ( Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc | FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast @@ -450,7 +465,7 @@ and xlate_value ?(inline = false) stk : x -> Llvm.llvalue -> Exp.t = | Select | GetElementPtr | ExtractElement | InsertElement | ShuffleVector | ExtractValue | InsertValue ) as opcode ) -> if inline || should_inline llv then xlate_opcode stk x llv opcode - else Exp.reg (xlate_name x llv) + else ([], Exp.reg (xlate_name x llv)) | ConstantExpr -> xlate_opcode stk x llv (Llvm.constexpr_opcode llv) | GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv () | Instruction (CatchPad | CleanupPad | CatchSwitch) -> @@ -467,9 +482,10 @@ and xlate_value ?(inline = false) stk : x -> Llvm.llvalue -> Exp.t = ; xlate_value_ llv |> - [%Trace.retn fun {pf} exp -> pf "%a" Exp.pp exp] ) + [%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp] ) -and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = +and xlate_opcode stk : + x -> Llvm.llvalue -> Llvm.Opcode.t -> Inst.t list * Exp.t = fun x llv opcode -> [%Trace.call fun {pf} -> pf "%a" pp_llvalue llv] ; @@ -479,22 +495,25 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = let dst = Lazy.force typ in let rand = Llvm.operand llv 0 in let src = xlate_type x (Llvm.type_of rand) in - let arg = xlate_value stk x rand in - match (opcode : Llvm.Opcode.t) with - | Trunc -> Exp.signed (Typ.bit_size_of dst) arg ~to_:dst - | SExt -> Exp.signed (Typ.bit_size_of src) arg ~to_:dst - | ZExt -> Exp.unsigned (Typ.bit_size_of src) arg ~to_:dst - | (BitCast | AddrSpaceCast) when Typ.equal dst src -> arg - | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc | FPExt | PtrToInt - |IntToPtr | BitCast | AddrSpaceCast -> - Exp.convert src ~to_:dst arg - | _ -> fail "convert: %a" pp_llvalue llv () + let pre, arg = xlate_value stk x rand in + ( pre + , match (opcode : Llvm.Opcode.t) with + | Trunc -> Exp.signed (Typ.bit_size_of dst) arg ~to_:dst + | SExt -> Exp.signed (Typ.bit_size_of src) arg ~to_:dst + | ZExt -> Exp.unsigned (Typ.bit_size_of src) arg ~to_:dst + | (BitCast | AddrSpaceCast) when Typ.equal dst src -> arg + | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc | FPExt | PtrToInt + |IntToPtr | BitCast | AddrSpaceCast -> + Exp.convert src ~to_:dst arg + | _ -> fail "convert: %a" pp_llvalue llv () ) in let binary (mk : ?typ:_ -> _) = if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then todo "vector operations: %a" pp_llvalue llv () ; let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in - mk ~typ (xlate_rand 0) (xlate_rand 1) + let pre_0, arg_0 = xlate_rand 0 in + let pre_1, arg_1 = xlate_rand 1 in + (pre_0 @ pre_1, mk ~typ arg_0 arg_1) in let unordered_or mk = binary (fun ?typ e f -> @@ -549,8 +568,10 @@ and xlate_opcode stk : 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) - ~els:(xlate_rand 2) + let pre_0, cnd = xlate_rand 0 in + let pre_1, thn = xlate_rand 1 in + let pre_2, els = xlate_rand 2 in + (pre_0 @ pre_1 @ pre_2, Exp.conditional ~typ ~cnd ~thn ~els) | ExtractElement | InsertElement -> ( let typ = let lltyp = Llvm.type_of (Llvm.operand llv 0) in @@ -563,20 +584,25 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = in let idx i = match xlate_rand i with - | Integer {data} -> Z.to_int data + | pre, Integer {data} -> (pre, Z.to_int data) | _ -> todo "vector operations: %a" pp_llvalue llv () in - let rcd = xlate_rand 0 in + let pre_0, rcd = xlate_rand 0 in match opcode with - | ExtractElement -> Exp.select typ rcd (idx 1) - | InsertElement -> Exp.update typ ~rcd (idx 2) ~elt:(xlate_rand 1) + | ExtractElement -> + let pre_1, idx_1 = idx 1 in + (pre_0 @ pre_1, Exp.select typ rcd idx_1) + | InsertElement -> + let pre_1, elt = xlate_rand 1 in + let pre_2, idx_2 = idx 2 in + (pre_0 @ pre_1 @ pre_2, Exp.update typ ~rcd idx_2 ~elt) | _ -> assert false ) | ExtractValue | InsertValue -> - let agg = xlate_rand 0 in + let pre_0, agg = xlate_rand 0 in let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in let indices = Llvm.indices llv in let num = Array.length indices in - let rec xlate_indices i rcd typ = + let rec xlate_indices pre0 i rcd typ = let rcd_i, typ_i, upd = match (typ : Typ.t) with | Tuple {elts} | Struct {elts} -> @@ -591,17 +617,19 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = in let update_or_return elt ret = match[@warning "p"] opcode with - | InsertValue -> upd ~elt:(Lazy.force elt) - | ExtractValue -> ret + | InsertValue -> + let pre, elt = Lazy.force elt in + (pre0 @ pre, upd ~elt) + | ExtractValue -> (pre0, ret) in if i < num - 1 then - let elt = xlate_indices (i + 1) rcd_i typ_i in - update_or_return (lazy elt) elt + let pre, elt = xlate_indices pre0 (i + 1) rcd_i typ_i in + update_or_return (lazy (pre, elt)) elt else - let elt = lazy (xlate_rand 1) in - update_or_return elt rcd_i + let pre_elt = lazy (xlate_rand 1) in + update_or_return pre_elt rcd_i in - xlate_indices 0 agg typ + xlate_indices pre_0 0 agg typ | GetElementPtr -> if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then todo "vector operations: %a" pp_llvalue llv () ; @@ -613,13 +641,14 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = [%Trace.call fun {pf} -> pf "%i %a" i pp_llvalue (Llvm.operand llv i)] ; + let pre_i, arg_i = xlate_rand i in let idx = convert_to_siz (xlate_type x (Llvm.type_of (Llvm.operand llv i))) - (xlate_rand i) + arg_i in ( if i = 1 then - let base = xlate_rand 0 in + let pre_0, base = xlate_rand 0 in let lltyp = Llvm.type_of (Llvm.operand llv 0) in let llelt = match Llvm.classify_type lltyp with @@ -627,13 +656,13 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = | _ -> fail "xlate_opcode: %i %a" i pp_llvalue llv () in (* translate [gep t*, iN M] as [gep [1 x t]*, iN M] *) - (ptr_idx x ~ptr:base ~idx ~llelt, llelt) + ((pre_0 @ pre_i, ptr_idx x ~ptr:base ~idx ~llelt), llelt) else - let ptr, lltyp = xlate_indices (i - 1) in + let (pre_i1, ptr), lltyp = xlate_indices (i - 1) in match Llvm.classify_type lltyp with | Array | Vector -> let llelt = Llvm.element_type lltyp in - (ptr_idx x ~ptr ~idx ~llelt, llelt) + ((pre_i1 @ pre_i, ptr_idx x ~ptr ~idx ~llelt), llelt) | Struct -> let fld = match @@ -644,11 +673,11 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = | None -> fail "xlate_opcode: %i %a" i pp_llvalue llv () in let llelt = (Llvm.struct_element_types lltyp).(fld) in - (ptr_fld x ~ptr ~fld ~lltyp, llelt) + ((pre_i1 @ pre_i, ptr_fld x ~ptr ~fld ~lltyp), llelt) | _ -> fail "xlate_opcode: %i %a" i pp_llvalue llv () ) |> - [%Trace.retn fun {pf} (exp, llt) -> - pf "%a %a" Exp.pp exp pp_lltype llt] + [%Trace.retn fun {pf} (pre_exp, llt) -> + pf "%a %a" pp_prefix_exp pre_exp pp_lltype llt] in fst (xlate_indices (len - 1)) | ShuffleVector -> ( @@ -668,7 +697,7 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = |CatchRet | CatchPad | CleanupPad | CatchSwitch | VAArg -> fail "xlate_opcode: %a" pp_llvalue llv () ) |> - [%Trace.retn fun {pf} exp -> pf "%a" Exp.pp exp] + [%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp] and xlate_global stk : x -> Llvm.llvalue -> Global.t = fun x llg -> @@ -684,7 +713,10 @@ and xlate_global stk : x -> Llvm.llvalue -> Global.t = match Llvm.classify_value llg with | GlobalVariable -> Option.map (Llvm.global_initializer llg) ~f:(fun llv -> - (xlate_value stk x llv, size_of x (Llvm.type_of llv)) ) + let pre, init = xlate_value stk x llv in + if not (List.is_empty pre) then + todo "global initializer instructions" () ; + (init, size_of x (Llvm.type_of llv)) ) | _ -> None in Global.mk ?init g loc @@ -693,6 +725,7 @@ and xlate_global stk : x -> Llvm.llvalue -> Global.t = let xlate_intrinsic_exp = xlate_intrinsic_exp [] let xlate_value ?inline = xlate_value ?inline [] +let xlate_values = xlate_values [] let xlate_opcode = xlate_opcode [] let xlate_global = xlate_global [] @@ -769,12 +802,12 @@ let exception_typs = the PHIs of [dst] translated to a move. *) let xlate_jump : x - -> ?reg_exps:(Reg.t * Exp.t) list + -> ?reg_exps:(Reg.t * (Inst.t list * Exp.t)) list -> Llvm.llvalue -> Llvm.llbasicblock -> Loc.t -> Llair.block list - -> Llair.jump * Llair.block list = + -> Inst.t list * Llair.jump * Llair.block list = fun x ?(reg_exps = []) instr dst loc blocks -> let src = Llvm.instr_parent instr in let rec xlate_jump_ reg_exps (pos : _ Llvm.llpos) = @@ -796,9 +829,16 @@ let xlate_jump : let dst_lbl = label_of_block dst in let jmp = Jump.mk dst_lbl in match xlate_jump_ reg_exps (Llvm.instr_begin dst) with - | [] -> (jmp, blocks) - | reg_exps -> - let mov = Inst.move ~reg_exps:(IArray.of_list_rev reg_exps) ~loc in + | [] -> ([], jmp, blocks) + | rev_reg_pre_exps -> + let rev_pre, rev_reg_exps = + List.fold_map rev_reg_pre_exps ~init:[] + ~f:(fun rev_pre (reg, (pre, exp)) -> + (List.rev_append pre rev_pre, (reg, exp)) ) + in + let mov = + Inst.move ~reg_exps:(IArray.of_list_rev rev_reg_exps) ~loc + in let lbl = find_name instr ^ ".jmp." ^ dst_lbl in let blk = Block.mk ~lbl @@ -812,7 +852,7 @@ let xlate_jump : assert (Block.equal blk0 blk) ; blocks in - (Jump.mk lbl, blocks) + (List.rev rev_pre, Jump.mk lbl, blocks) (** An LLVM instruction is translated to a sequence of LLAIR instructions and a terminator, plus some additional blocks to which it may refer @@ -836,7 +876,7 @@ let pp_code fs (insts, term, blocks) = let rec xlate_func_name x llv = match Llvm.classify_value llv with - | Function | GlobalVariable -> Exp.reg (xlate_name x ~global:() llv) + | Function | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv)) | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv) | Argument | Instruction _ -> xlate_value x llv | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0) @@ -867,8 +907,8 @@ let xlate_instr : continue insts_term_to_code in let nop () = continue (fun (insts, term) -> (insts, term, [])) in - let emit_inst inst = - continue (fun (insts, term) -> (inst :: insts, term, [])) + let emit_inst ?(prefix = []) inst = + continue (fun (insts, term) -> (prefix @ (inst :: insts), term, [])) in let emit_term ?(prefix = []) ?(blocks = []) term = [%Trace.retn fun {pf} () -> pf "%a" pp_code (prefix, term, blocks)] () ; @@ -880,34 +920,31 @@ let xlate_instr : if should_inline instr then nop () else let reg = xlate_name x instr in - let exp = xlate instr in + let prefix, exp = xlate instr in let reg_exps = IArray.of_array [|(reg, exp)|] in - emit_inst (Inst.move ~reg_exps ~loc) + emit_inst ~prefix (Inst.move ~reg_exps ~loc) in let opcode = Llvm.instr_opcode instr in match opcode with | Load -> let reg = xlate_name x instr in let len = xlate_size_of x instr in - let ptr = xlate_value x (Llvm.operand instr 0) in - emit_inst (Inst.load ~reg ~ptr ~len ~loc) + let prefix, ptr = xlate_value x (Llvm.operand instr 0) in + emit_inst ~prefix (Inst.load ~reg ~ptr ~len ~loc) | Store -> let rand0 = Llvm.operand instr 0 in - let exp = xlate_value x rand0 in + let pre0, exp = xlate_value x rand0 in let len = xlate_size_of x rand0 in - let ptr = xlate_value x (Llvm.operand instr 1) in - emit_inst (Inst.store ~ptr ~exp ~len ~loc) + let pre1, ptr = xlate_value x (Llvm.operand instr 1) in + emit_inst ~prefix:(pre0 @ pre1) (Inst.store ~ptr ~exp ~len ~loc) | Alloca -> let reg = xlate_name x instr in let rand = Llvm.operand instr 0 in - let num = - convert_to_siz - (xlate_type x (Llvm.type_of rand)) - (xlate_value x rand) - in + let prefix, arg = xlate_value x rand in + let num = convert_to_siz (xlate_type x (Llvm.type_of rand)) arg in assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ; let len = xlate_size_of x instr in - emit_inst (Inst.alloc ~reg ~num ~len ~loc) + emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc) | Call -> ( let maybe_llfunc = Llvm.operand instr (Llvm.num_operands instr - 1) in let lltyp = Llvm.type_of maybe_llfunc in @@ -940,25 +977,24 @@ let xlate_instr : | None -> ( match String.split fname ~on:'.' with | ["__llair_throw"] -> - let exc = xlate_value x (Llvm.operand instr 0) in - emit_term ~prefix:(pop loc) (Term.throw ~exc ~loc) + let pre, exc = xlate_value x (Llvm.operand instr 0) in + emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc) | ["__llair_alloc" (* void* __llair_alloc(unsigned size) *)] -> let reg = xlate_name x instr in let num_operand = Llvm.operand instr 0 in + let prefix, arg = xlate_value x num_operand in let num = - convert_to_siz - (xlate_type x (Llvm.type_of num_operand)) - (xlate_value x num_operand) + convert_to_siz (xlate_type x (Llvm.type_of num_operand)) arg in let len = Exp.integer Typ.siz (Z.of_int 1) in - emit_inst (Inst.alloc ~reg ~num ~len ~loc) + emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc) | ["_Znwm" (* operator new(size_t num) *)] |[ "_ZnwmSt11align_val_t" (* operator new(unsigned long, std::align_val_t) *) ] -> let reg = xlate_name x instr in - let num = xlate_value x (Llvm.operand instr 0) in + let prefix, num = xlate_value x (Llvm.operand instr 0) in let len = xlate_size_of x instr in - emit_inst (Inst.alloc ~reg ~num ~len ~loc) + emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc) | ["_ZdlPv" (* operator delete(void* ptr) *)] |[ "_ZdlPvSt11align_val_t" (* operator delete(void* ptr, std::align_val_t) *) ] @@ -966,23 +1002,29 @@ let xlate_instr : (* operator delete(void* ptr, unsigned long, std::align_val_t) *) ] |["free" (* void free(void* ptr) *)] -> - let ptr = xlate_value x (Llvm.operand instr 0) in - emit_inst (Inst.free ~ptr ~loc) + let prefix, ptr = xlate_value x (Llvm.operand instr 0) in + emit_inst ~prefix (Inst.free ~ptr ~loc) | "llvm" :: "memset" :: _ -> - let dst = xlate_value x (Llvm.operand instr 0) in - let byt = xlate_value x (Llvm.operand instr 1) in - let len = xlate_value x (Llvm.operand instr 2) in - emit_inst (Inst.memset ~dst ~byt ~len ~loc) + let pre_0, dst = xlate_value x (Llvm.operand instr 0) in + let pre_1, byt = xlate_value x (Llvm.operand instr 1) in + let pre_2, len = xlate_value x (Llvm.operand instr 2) in + emit_inst + ~prefix:(pre_0 @ pre_1 @ pre_2) + (Inst.memset ~dst ~byt ~len ~loc) | "llvm" :: "memcpy" :: _ -> - let dst = xlate_value x (Llvm.operand instr 0) in - let src = xlate_value x (Llvm.operand instr 1) in - let len = xlate_value x (Llvm.operand instr 2) in - emit_inst (Inst.memcpy ~dst ~src ~len ~loc) + let pre_0, dst = xlate_value x (Llvm.operand instr 0) in + let pre_1, src = xlate_value x (Llvm.operand instr 1) in + let pre_2, len = xlate_value x (Llvm.operand instr 2) in + emit_inst + ~prefix:(pre_0 @ pre_1 @ pre_2) + (Inst.memcpy ~dst ~src ~len ~loc) | "llvm" :: "memmove" :: _ -> - let dst = xlate_value x (Llvm.operand instr 0) in - let src = xlate_value x (Llvm.operand instr 1) in - let len = xlate_value x (Llvm.operand instr 2) in - emit_inst (Inst.memmov ~dst ~src ~len ~loc) + let pre_0, dst = xlate_value x (Llvm.operand instr 0) in + let pre_1, src = xlate_value x (Llvm.operand instr 1) in + let pre_2, len = xlate_value x (Llvm.operand instr 2) in + emit_inst + ~prefix:(pre_0 @ pre_1 @ pre_2) + (Inst.memmov ~dst ~src ~len ~loc) | ["abort"] | ["llvm"; "trap"] -> emit_inst (Inst.abort ~loc) (* dropped / handled elsewhere *) | ["llvm"; "dbg"; ("declare" | "value")] @@ -1002,11 +1044,11 @@ let xlate_instr : skip "inline asm" (* general function call that may not throw *) | _ -> - let callee = xlate_func_name x llfunc in + let pre0, callee = xlate_func_name x llfunc in let typ = xlate_type x lltyp in let lbl = name ^ ".ret" in - let call = - let actuals = + let pre, call = + let pre, actuals = let num_actuals = if not (Llvm.is_var_arg (Llvm.element_type lltyp)) then Llvm.num_arg_operands instr @@ -1027,17 +1069,17 @@ let xlate_instr : pp_llvalue instr () ) ; Array.length (Llvm.param_types llfty) in - List.rev_init num_actuals ~f:(fun i -> - xlate_value x (Llvm.operand instr i) ) + xlate_values x num_actuals (Llvm.operand instr) in let areturn = xlate_name_opt x instr in let return = Jump.mk lbl in - Term.call ~callee ~typ ~actuals ~areturn ~return ~throw:None - ~loc + ( pre + , Term.call ~callee ~typ ~actuals ~areturn ~return ~throw:None + ~loc ) in continue (fun (insts, term) -> let cmnd = IArray.of_list insts in - ([], call, [Block.mk ~lbl ~cmnd ~term]) ) ) ) + (pre0 @ pre, call, [Block.mk ~lbl ~cmnd ~term]) ) ) ) | Invoke -> ( let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in let lltyp = Llvm.type_of llfunc in @@ -1060,60 +1102,69 @@ let xlate_instr : (* intrinsics *) match String.split fname ~on:'.' with | _ when Option.is_some (xlate_intrinsic_exp fname) -> - let dst, blocks = xlate_jump x instr return_blk loc [] in - emit_term (Term.goto ~dst ~loc) ~blocks + let prefix, dst, blocks = xlate_jump x instr return_blk loc [] in + emit_term ~prefix (Term.goto ~dst ~loc) ~blocks | ["__llair_throw"] -> - let dst, blocks = xlate_jump x instr unwind_blk loc [] in - emit_term (Term.goto ~dst ~loc) ~blocks + let prefix, dst, blocks = xlate_jump x instr unwind_blk loc [] in + emit_term ~prefix (Term.goto ~dst ~loc) ~blocks | ["abort"] -> emit_term ~prefix:[Inst.abort ~loc] Term.unreachable | ["_Znwm" (* operator new(size_t num) *)] |[ "_ZnwmSt11align_val_t" (* operator new(unsigned long num, std::align_val_t) *) ] when num_actuals > 0 -> let reg = xlate_name x instr in - let num = xlate_value x (Llvm.operand instr 0) in + let pre_0, num = xlate_value x (Llvm.operand instr 0) in let len = xlate_size_of x instr in - let dst, blocks = xlate_jump x instr return_blk loc [] in + let prefix, dst, blocks = xlate_jump x instr return_blk loc [] in emit_term - ~prefix:[Inst.alloc ~reg ~num ~len ~loc] + ~prefix:(pre_0 @ (Inst.alloc ~reg ~num ~len ~loc :: prefix)) (Term.goto ~dst ~loc) ~blocks (* unimplemented *) | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ -> todo "statepoints:@ %a" pp_llvalue instr () (* general function call that may throw *) | _ -> - let callee = xlate_func_name x llfunc in + let pre_0, callee = xlate_func_name x llfunc in let typ = xlate_type x (Llvm.type_of llfunc) in - let actuals = - List.rev_init num_actuals ~f:(fun i -> - xlate_value x (Llvm.operand instr i) ) + let pre_1, actuals = + xlate_values x num_actuals (Llvm.operand instr) in let areturn = xlate_name_opt x instr in - let return, blocks = xlate_jump x instr return_blk loc [] in - let throw, blocks = xlate_jump x instr unwind_blk loc blocks in + let pre_2, return, blocks = + xlate_jump x instr return_blk loc [] + in + let pre_3, throw, blocks = + xlate_jump x instr unwind_blk loc blocks + in let throw = Some throw in emit_term + ~prefix:(List.concat [pre_0; pre_1; pre_2; pre_3]) (Term.call ~callee ~typ ~actuals ~areturn ~return ~throw ~loc) ~blocks ) | Ret -> - let exp = - if Llvm.num_operands instr = 0 then None - else Some (xlate_value x (Llvm.operand instr 0)) + let pre, exp = + if Llvm.num_operands instr = 0 then ([], None) + else + let pre, arg = xlate_value x (Llvm.operand instr 0) in + (pre, Some arg) in - emit_term ~prefix:(pop loc) (Term.return ~exp ~loc) + emit_term ~prefix:(pop loc @ pre) (Term.return ~exp ~loc) | Br -> ( match Option.value_exn (Llvm.get_branch instr) with | `Unconditional blk -> - let dst, blocks = xlate_jump x instr blk loc [] in - emit_term (Term.goto ~dst ~loc) ~blocks + let prefix, dst, blocks = xlate_jump x instr blk loc [] in + emit_term ~prefix (Term.goto ~dst ~loc) ~blocks | `Conditional (cnd, thn, els) -> - let key = xlate_value x cnd in - let thn, blocks = xlate_jump x instr thn loc [] in - let els, blocks = xlate_jump x instr els loc blocks in - emit_term (Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks ) + let pre_c, key = xlate_value x cnd in + let pre_t, thn, blocks = xlate_jump x instr thn loc [] in + let pre_e, els, blocks = xlate_jump x instr els loc blocks in + emit_term + ~prefix:(List.concat [pre_c; pre_t; pre_e]) + (Term.branch ~key ~nzero:thn ~zero:els ~loc) + ~blocks ) | Switch -> - let key = xlate_value x (Llvm.operand instr 0) in - let cases, blocks = + let pre_k, key = xlate_value x (Llvm.operand instr 0) in + let pre_t, cases, blocks = let num_cases = (Llvm.num_operands instr / 2) - 1 in let rec xlate_cases i blocks = if i <= num_cases then @@ -1121,35 +1172,38 @@ let xlate_instr : let blk = Llvm.block_of_value (Llvm.operand instr ((2 * i) + 1)) in - let num = xlate_value x idx in - let jmp, blocks = xlate_jump x instr blk loc blocks in - let rest, blocks = xlate_cases (i + 1) blocks in - ((num, jmp) :: rest, blocks) - else ([], blocks) + let pre_i, num = xlate_value x idx in + let pre_j, jmp, blocks = xlate_jump x instr blk loc blocks in + let pre, rest, blocks = xlate_cases (i + 1) blocks in + (List.concat [pre_i; pre_j; pre], (num, jmp) :: rest, blocks) + else ([], [], blocks) in xlate_cases 1 [] in let tbl = IArray.of_list cases in let blk = Llvm.block_of_value (Llvm.operand instr 1) in - let els, blocks = xlate_jump x instr blk loc blocks in - emit_term (Term.switch ~key ~tbl ~els ~loc) ~blocks + let pre_e, els, blocks = xlate_jump x instr blk loc blocks in + emit_term + ~prefix:(List.concat [pre_k; pre_t; pre_e]) + (Term.switch ~key ~tbl ~els ~loc) + ~blocks | IndirectBr -> - let ptr = xlate_value x (Llvm.operand instr 0) in + let pre_0, ptr = xlate_value x (Llvm.operand instr 0) in let num_dests = Llvm.num_operands instr - 1 in - let lldests, blocks = + let pre, lldests, blocks = let rec dests i blocks = if i <= num_dests then let v = Llvm.operand instr i in let blk = Llvm.block_of_value v in - let jmp, blocks = xlate_jump x instr blk loc blocks in - let rest, blocks = dests (i + 1) blocks in - (jmp :: rest, blocks) - else ([], blocks) + let pre_j, jmp, blocks = xlate_jump x instr blk loc blocks in + let pre, rest, blocks = dests (i + 1) blocks in + (pre_j @ pre, jmp :: rest, blocks) + else ([], [], blocks) in dests 1 [] in let tbl = IArray.of_list lldests in - emit_term (Term.iswitch ~ptr ~tbl ~loc) ~blocks + emit_term ~prefix:(pre_0 @ pre) (Term.iswitch ~ptr ~tbl ~loc) ~blocks | LandingPad -> (* Translate the landingpad clauses to code to load the type_info from the thrown exception, and test the type_info against the clauses, @@ -1194,9 +1248,9 @@ let xlate_instr : in let goto_unwind i sel blocks = let dst, blocks = jump_unwind i sel blocks in - (Term.goto ~dst ~loc, blocks) + ([], Term.goto ~dst ~loc, blocks) in - let term_unwind, rev_blocks = + let pre, term_unwind, rev_blocks = if Llvm.is_cleanup instr then goto_unwind 0 (Exp.integer i32 Z.zero) [] else @@ -1216,55 +1270,64 @@ let xlate_instr : let num_tis = Llvm.num_operands clause in if num_tis = 0 then let dst, rev_blocks = match_filter i rev_blocks in - (Term.goto ~dst ~loc, rev_blocks) + ([], Term.goto ~dst ~loc, rev_blocks) else match Llvm.classify_type (Llvm.type_of clause) with | Array (* filter *) -> ( match Llvm.classify_value clause with | ConstantArray -> let rec xlate_filter i = - let tiI = xlate_value x (Llvm.operand clause i) in + let preI, tiI = + xlate_value x (Llvm.operand clause i) + in if i < num_tis - 1 then - Exp.and_ ~typ:Typ.bool (Exp.dq ~typ:tip tiI ti) - (xlate_filter (i + 1)) - else Exp.dq ~typ:tip tiI ti + let pre, dqs = xlate_filter (i + 1) in + ( preI @ pre + , Exp.and_ ~typ:Typ.bool (Exp.dq ~typ:tip tiI ti) + dqs ) + else (preI, Exp.dq ~typ:tip tiI ti) in - let key = xlate_filter 0 in + let pre, key = xlate_filter 0 in let nzero, rev_blocks = match_filter i rev_blocks in - ( Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) + ( pre + , Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) , rev_blocks ) | _ -> fail "xlate_instr: %a" pp_llvalue instr () ) | _ (* catch *) -> let typ = xlate_type x (Llvm.type_of clause) in - let clause = xlate_value x clause in + let pre, clause = xlate_value x clause in let key = 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 - ( Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) + ( pre + , Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) , rev_blocks ) in let rec rev_blocks i z = if i < num_clauses then - let term, z = xlate_clause i z in - rev_blocks (i + 1) (block i term :: z) - else block i Term.unreachable :: z + let pre_i, term, z = xlate_clause i z in + let pre, blks = rev_blocks (i + 1) (block i term :: z) in + (pre_i @ pre, blks) + else ([], block i Term.unreachable :: z) in - xlate_clause 0 (rev_blocks 1 []) + let pre1, rev_blks = rev_blocks 1 [] in + let pre0, term, blks = xlate_clause 0 rev_blks in + (pre0 @ pre1, term, blks) in continue (fun (insts, term) -> - ( [load_ti] + ( load_ti :: pre , term_unwind , List.rev_append rev_blocks [Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term] ) ) | Resume -> let llrcd = Llvm.operand instr 0 in let typ = xlate_type x (Llvm.type_of llrcd) in - let rcd = xlate_value x llrcd in + let pre, rcd = xlate_value x llrcd in let exc = Exp.select typ rcd 0 in - emit_term ~prefix:(pop loc) (Term.throw ~exc ~loc) + emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc) | Unreachable -> emit_term Term.unreachable | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast | Add | FAdd