[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
5 years ago · e17f8adfe9
parent 4fdc2f6c76
commit e17f8adfe9
1 changed files with 237 additions and 174 deletions
--- 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,8 +495,9 @@ 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
+    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
@ -488,13 +505,15 @@ and xlate_opcode stk : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
      | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc | FPExt | PtrToInt
       |IntToPtr | BitCast | AddrSpaceCast ->
          Exp.convert src ~to_:dst arg
-    | _ -> fail "convert: %a" pp_llvalue llv ()
+      | _ -> 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