<commit_before>(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

(** Translate LLVM to LLAIR *)

open Llair

let pp_lltype fs t = Format.pp_print_string fs (Llvm.string_of_lltype t)

(* WARNING: SLOW on instructions and functions *)
let pp_llvalue fs t = Format.pp_print_string fs (Llvm.string_of_llvalue t)

let pp_llblock fs t =
  Format.pp_print_string fs (Llvm.string_of_llvalue (Llvm.value_of_block t))

;;
Exp.demangle :=
  let open Ctypes in
  let cxa_demangle =
    (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
    Foreign.foreign "__cxa_demangle"
      ( string
      @-> ptr char
      @-> ptr size_t
      @-> ptr int
      @-> returning string_opt )
  in
  let null_ptr_char = from_voidp char null in
  let null_ptr_size_t = from_voidp size_t null in
  let status = allocate int 0 in
  fun mangled ->
    if String.prefix ~pre:"_Z" mangled then
      let demangled =
        cxa_demangle mangled null_ptr_char null_ptr_size_t status
      in
      if !@status = 0 then demangled else None
    else None

exception Invalid_llvm of string

let invalid_llvm : string -> 'a =
 fun msg ->
  let first_line =
    Option.map_or ~default:msg
      ~f:(fun i -> String.take i msg)
      (String.index msg '\n')
  in
  Format.printf "@\n%s@\n" msg ;
  raise (Invalid_llvm first_line)

(* gather names and debug locations *)

(* number of register ids used so far *)
let sym_count = ref 0

(* map frontend-synthesized register names to ids, registers that come from
   LLVM are stored in sym_tbl *)
let id_memo = String.Tbl.create ()

(* lookup or generate the id for a frontend-synthesized register name *)
let get_id name =
  String.Tbl.find_or_add id_memo name ~default:(fun () ->
      incr sym_count ;
      !sym_count )

module LlvalueTbl = HashTable.Make (struct
  type t = Llvm.llvalue

  include Poly
end)

module SymTbl = LlvalueTbl

let sym_tbl : (string * int * Loc.t) SymTbl.t =
  SymTbl.create ~size:4_194_304 ()

module ScopeTbl = HashTable.Make (struct
  type t = [`Fun of Llvm.llvalue | `Mod of Llvm.llmodule]

  include Poly
end)

let scope_tbl : (int ref * int String.Tbl.t) ScopeTbl.t =
  ScopeTbl.create ~size:32_768 ()

let realpath_tbl = String.Tbl.create ()

let get_debug_loc_directory llv =
  let+ dir = Llvm.get_debug_loc_directory llv in
  if String.is_empty dir then dir
  else
    String.Tbl.find_or_add realpath_tbl dir ~default:(fun () ->
        try Core.Filename.realpath dir with Unix.Unix_error _ -> dir )

open struct
  open struct
    let loc_of_global g =
      Loc.mk
        ~dir:(get_debug_loc_directory g)
        ~file:(Llvm.get_debug_loc_filename g)
        ~line:(Some (Llvm.get_debug_loc_line g))
        ~col:None

    let loc_of_function f =
      Loc.mk
        ~dir:(get_debug_loc_directory f)
        ~file:(Llvm.get_debug_loc_filename f)
        ~line:(Some (Llvm.get_debug_loc_line f))
        ~col:None

    let loc_of_instr i =
      Loc.mk
        ~dir:(get_debug_loc_directory i)
        ~file:(Llvm.get_debug_loc_filename i)
        ~line:(Some (Llvm.get_debug_loc_line i))
        ~col:(Some (Llvm.get_debug_loc_column i))

    let find_scope scope =
      ScopeTbl.find_or_add scope_tbl scope ~default:(fun () ->
          (ref 0, String.Tbl.create ()) )

    let add_sym llv loc =
      let maybe_scope =
        match Llvm.classify_value llv with
        | Argument -> Some (`Fun (Llvm.param_parent llv))
        | BasicBlock ->
            Some (`Fun (Llvm.block_parent (Llvm.block_of_value llv)))
        | Instruction _ ->
            Some (`Fun (Llvm.block_parent (Llvm.instr_parent llv)))
        | GlobalVariable | Function -> Some (`Mod (Llvm.global_parent llv))
        | UndefValue -> None
        | ConstantExpr -> None
        | ConstantPointerNull -> None
        | _ ->
            warn "Unexpected type of llv, might crash: %a" pp_llvalue llv () ;
            Some (`Mod (Llvm.global_parent llv))
      in
      match maybe_scope with
      | None -> ()
      | Some scope -> (
        match SymTbl.find sym_tbl llv with
        | Some (name, id, loc0) ->
            if Loc.equal loc0 Loc.none then
              SymTbl.set sym_tbl ~key:llv ~data:(name, id, loc)
        | None ->
            let name =
              if Poly.(Llvm.classify_type (Llvm.type_of llv) = Void) then
                if Poly.(Llvm.classify_value llv = Instruction Call) then (
                  (* LLVM does not give unique names to the result of
                     void-returning function calls. We need unique names for
                     these as they determine the labels of newly-created
                     return blocks. *)
                  let next, void_tbl = find_scope scope in
                  let fname =
                    match
                      Llvm.(value_name (operand llv (num_operands llv - 1)))
                    with
                    | "" -> Int.to_string (!next - 1)
                    | s -> s
                  in
                  match String.Tbl.find void_tbl fname with
                  | None ->
                      String.Tbl.set void_tbl ~key:fname ~data:1 ;
                      fname ^ ".void"
                  | Some count ->
                      String.Tbl.set void_tbl ~key:fname ~data:(count + 1) ;
                      String.concat ~sep:""
                        [fname; ".void."; Int.to_string count] )
                else ""
              else
                match Llvm.value_name llv with
                | "" ->
                    (* anonymous values take the next SSA name *)
                    let next, _ = find_scope scope in
                    let name = !next in
                    next := name + 1 ;
                    Int.to_string name
                | name -> (
                  match Int.of_string name with
                  | Some _ ->
                      (* escape to avoid clash with names of anonymous
                         values *)
                      "\"" ^ name ^ "\""
                  | None -> name )
            in
            let id = 1 + SymTbl.length sym_tbl in
            SymTbl.set sym_tbl ~key:llv ~data:(name, id, loc) )
  end

  let scan_names_and_locs : Llvm.llmodule -> unit =
   fun m ->
    assert (!sym_count = 0) ;
    let scan_global g = add_sym g (loc_of_global g) in
    let scan_instr i =
      let loc = loc_of_instr i in
      add_sym i loc ;
      match Llvm.instr_opcode i with
      | Call -> (
        match Llvm.(value_name (operand i (num_arg_operands i))) with
        | "llvm.dbg.declare" ->
            let md = Llvm.(get_mdnode_operands (operand i 0)) in
            if not (Array.is_empty md) then add_sym md.(0) loc
            else
              warn
                "could not find variable for debug info at %a with \
                 metadata %a"
                Loc.pp loc (List.pp ", " pp_llvalue) (Array.to_list md) ()
        | _ -> () )
      | _ -> ()
    in
    let scan_block b =
      add_sym (Llvm.value_of_block b) Loc.none ;
      Llvm.iter_instrs scan_instr b
    in
    let scan_function f =
      Llvm.iter_params (fun prm -> add_sym prm Loc.none) f ;
      add_sym f (loc_of_function f) ;
      Llvm.iter_blocks scan_block f
    in
    Llvm.iter_globals scan_global m ;
    Llvm.iter_functions scan_function m ;
    sym_count := SymTbl.length sym_tbl

  let find_name : Llvm.llvalue -> string * int =
   fun v ->
    let name, id, _ = SymTbl.find_exn sym_tbl v in
    assert (not (String.is_empty name)) ;
    (name, id)

  let find_loc : Llvm.llvalue -> Loc.t =
   fun v -> trd3 (SymTbl.find_exn sym_tbl v)
end

let label_of_block : Llvm.llbasicblock -> string =
 fun blk -> fst (find_name (Llvm.value_of_block blk))

module LltypeTbl = HashTable.Make (struct
  type t = Llvm.lltype

  include Poly
end)

let anon_struct_name : string LltypeTbl.t = LltypeTbl.create ()

let struct_name : Llvm.lltype -> string =
 fun llt ->
  match Llvm.struct_name llt with
  | Some name -> name
  | None ->
      LltypeTbl.find_or_add anon_struct_name llt ~default:(fun () ->
          Int.to_string (LltypeTbl.length anon_struct_name) )

type x = {llcontext: Llvm.llcontext; lldatalayout: Llvm_target.DataLayout.t}

let ptr_siz : x -> int =
 fun x -> Llvm_target.DataLayout.pointer_size x.lldatalayout

let size_of, bit_size_of =
  let size_to_int size_of x llt =
    if Llvm.type_is_sized llt then
      match Int64.unsigned_to_int (size_of llt x.lldatalayout) with
      | Some n -> n
      | None -> todo "type size too large: %a" pp_lltype llt ()
    else todo "types with undetermined size: %a" pp_lltype llt ()
  in
  ( size_to_int Llvm_target.DataLayout.abi_size
  , size_to_int Llvm_target.DataLayout.size_in_bits )

let memo_type : Typ.t LltypeTbl.t = LltypeTbl.create ()

let rec xlate_type : x -> Llvm.lltype -> Typ.t =
 fun x llt ->
  let xlate_type_ llt =
    if Llvm.type_is_sized llt then
      let byts = size_of x llt in
      let bits = bit_size_of x llt in
      match Llvm.classify_type llt with
      | Half | Float | Double | Fp128 -> Typ.float ~bits ~byts ~enc:`IEEE
      | X86fp80 -> Typ.float ~bits ~byts ~enc:`Extended
      | Ppc_fp128 -> Typ.float ~bits ~byts ~enc:`Pair
      | Integer -> Typ.integer ~bits ~byts
      | X86_mmx -> Typ.integer ~bits ~byts
      | Pointer ->
          if byts <> ptr_siz x then
            todo "non-integral pointer types: %a" pp_lltype llt () ;
          let elt = xlate_type x (Llvm.element_type llt) in
          Typ.pointer ~elt
      | Array ->
          let elt = xlate_type x (Llvm.element_type llt) in
          let len = Llvm.array_length llt in
          Typ.array ~elt ~len ~bits ~byts
      | Struct ->
          let llelts = Llvm.struct_element_types llt in
          let len = Array.length llelts in
          let fld_off i =
            match
              Int64.unsigned_to_int
                (Llvm_target.DataLayout.offset_of_element llt i
                   x.lldatalayout)
            with
            | Some i -> i
            | None -> todo "offset too large: %a" pp_lltype llt ()
          in
          if Llvm.is_literal llt then
            let elts =
              IArray.mapi
                ~f:(fun i elt -> (fld_off i, xlate_type x elt))
                (IArray.of_array llelts)
            in
            Typ.tuple elts ~bits ~byts
          else
            let name = struct_name llt in
            let elts =
              IArray.init len ~f:(fun i ->
                  lazy (fld_off i, xlate_type x llelts.(i)) )
            in
            Typ.struct_ ~name elts ~bits ~byts
      | Function -> fail "expected to be unsized: %a" pp_lltype llt ()
      | Vector -> todo "vector types: %a" pp_lltype llt ()
      | Void | Label | Metadata | Token -> assert false
    else
      match Llvm.classify_type llt with
      | Function ->
          let return = xlate_type_opt x (Llvm.return_type llt) in
          let llargs = Llvm.param_types llt in
          let len = Array.length llargs in
          let args =
            IArray.init len ~f:(fun i -> xlate_type x llargs.(i))
          in
          Typ.function_ ~return ~args
      | Struct when Llvm.is_opaque llt -> Typ.opaque ~name:(struct_name llt)
      | Token -> Typ.opaque ~name:"token"
      | Vector | Array | Struct ->
          todo "unsized non-opaque aggregate types: %a" pp_lltype llt ()
      | Half | Float | Double | X86fp80 | Fp128 | Ppc_fp128 | Integer
       |X86_mmx | Pointer ->
          fail "expected to be sized: %a" pp_lltype llt ()
      | Void | Label | Metadata -> assert false
  in
  LltypeTbl.find_or_add memo_type llt ~default:(fun () ->
      [%Trace.call fun {pf} -> pf "@ %a" pp_lltype llt]
      ;
      xlate_type_ llt
      |>
      [%Trace.retn fun {pf} ty ->
        pf "%a" Typ.pp_defn ty ;
        assert (
          (not (Llvm.type_is_sized llt))
          || (not (Typ.is_sized ty))
          || Typ.size_of ty = size_of x llt )] )

and xlate_type_opt : x -> Llvm.lltype -> Typ.t option =
 fun x llt ->
  match Llvm.classify_type llt with
  | Void -> None
  | _ -> Some (xlate_type x llt)

let i32 x = xlate_type x (Llvm.i32_type x.llcontext)

let suffix_after_last_space : string -> string =
 fun str -> String.drop (String.rindex_exn str ' ' + 1) str

let xlate_int : x -> Llvm.llvalue -> Exp.t =
 fun x llv ->
  let llt = Llvm.type_of llv in
  let typ = xlate_type x llt in
  let data =
    match Llvm.int64_of_const llv with
    | Some n -> Z.of_int64 n
    | None ->
        Z.of_string (suffix_after_last_space (Llvm.string_of_llvalue llv))
  in
  Exp.integer typ data

let xlate_float : x -> Llvm.llvalue -> Exp.t =
 fun x llv ->
  let llt = Llvm.type_of llv in
  let typ = xlate_type x llt in
  let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in
  Exp.float typ data

let xlate_name x : Llvm.llvalue -> Reg.t =
 fun llv ->
  let typ = xlate_type x (Llvm.type_of llv) in
  let name, id = find_name llv in
  Reg.mk typ id name

let xlate_name_opt : x -> Llvm.llvalue -> Reg.t option =
 fun x instr ->
  let llt = Llvm.type_of instr in
  match Llvm.classify_type llt with
  | Void -> None
  | _ -> Some (xlate_name x instr)

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

(* per-function count of 'undef' values, used to translate each occurrence
   of 'undef' to a distinct register *)
let undef_count = ref 0

module GlobTbl = LlvalueTbl

let memo_global : GlobalDefn.t GlobTbl.t = GlobTbl.create ()

module ValTbl = HashTable.Make (struct
  type t = bool * Llvm.llvalue

  include Poly
end)

let memo_value : (Inst.t list * Exp.t) ValTbl.t = ValTbl.create ()

let should_inline : Llvm.llvalue -> bool =
 fun llv ->
  match Llvm.use_begin llv with
  | Some use -> (
    match Llvm.use_succ use with
    | Some _ -> (
      match Llvm.classify_value llv with
      | Instruction
          ( Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP
          | FPTrunc | FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast
            ) ->
          true (* inline casts *)
      | _ -> false (* do not inline if >= 2 uses *) )
    | None -> true )
  | None -> true

let ptr_fld x ~ptr ~fld ~lltyp =
  let offset =
    Llvm_target.DataLayout.offset_of_element lltyp fld x.lldatalayout
  in
  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:Typ.ptr ptr
    (Exp.mul ~typ:Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx)

let convert_to_siz =
  let siz_bits = Typ.bit_size_of Typ.siz in
  fun typ arg ->
    match (typ : Typ.t) with
    | Integer {bits} ->
        if siz_bits < bits then Exp.signed siz_bits arg ~to_:Typ.siz
        else if siz_bits > bits then Exp.signed bits arg ~to_:Typ.siz
        else arg
    | _ -> fail "convert_to_siz: %a" Typ.pp typ ()

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 :
    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 pre, arg = xlate_value x rand in
          let src = xlate_type x (Llvm.type_of rand) in
          (pre, xlate_llvm_eh_typeid_for x src arg) )
  | _ -> None

and xlate_values x len val_i =
  let xlate_i j pre_0_i =
    let pre_j, arg_j = xlate_value x (val_i j) in
    (arg_j, Iter.append pre_0_i (Iter.of_list pre_j))
  in
  let pre, vals = Iter.(fold_map (0 -- (len - 1)) empty ~f:xlate_i) in
  (Iter.to_list pre, IArray.of_iter vals)

and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
    =
 fun x llv ->
  let xlate_value_ llv =
    match Llvm.classify_value llv with
    | Instruction Call -> (
        let func = Llvm.operand llv (Llvm.num_arg_operands llv) in
        let fname = Llvm.value_name func in
        match xlate_intrinsic_exp fname with
        | Some intrinsic when inline || should_inline llv -> intrinsic x llv
        | _ -> ([], Exp.reg (xlate_name x llv)) )
    | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
     |Argument ->
        ([], Exp.reg (xlate_name x llv))
    | Function ->
        ( []
        , Exp.function_
            (Function.mk
               (xlate_type x (Llvm.type_of llv))
               (fst (find_name llv))) )
    | GlobalVariable -> ([], Exp.global (xlate_global x llv).name)
    | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
    | 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)
        | Array _ | Tuple _ | Struct _ ->
            ([], 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 pre, args = xlate_values x len (Llvm.operand llv) in
        (pre, Exp.record typ args)
    | ConstantDataVector ->
        let typ = xlate_type x (Llvm.type_of llv) in
        let len = Llvm.vector_size (Llvm.type_of llv) in
        let pre, args = xlate_values x len (Llvm.const_element llv) in
        (pre, Exp.record typ args)
    | ConstantDataArray ->
        let typ = xlate_type x (Llvm.type_of llv) in
        let len = Llvm.array_length (Llvm.type_of llv) in
        let pre, args = xlate_values x len (Llvm.const_element llv) in
        (pre, Exp.record typ args)
    | ConstantStruct ->
        let typ = xlate_type x (Llvm.type_of llv) in
        let len = Llvm.num_operands llv in
        let pre, args = xlate_values x len (Llvm.operand llv) in
        (pre, Exp.record typ args)
    | BlockAddress ->
        let parent, _ = find_name (Llvm.operand llv 0) in
        let name, _ = find_name (Llvm.operand llv 1) in
        ([], Exp.label ~parent ~name)
    | UndefValue ->
        let llt = Llvm.type_of llv in
        let typ = xlate_type x llt in
        if not (Typ.is_sized typ) then
          todo "types with undetermined size: %a" pp_lltype llt () ;
        let name = Printf.sprintf "undef_%i" !undef_count in
        let loc = Loc.none in
        let id = get_id name in
        let reg = Reg.mk typ id name in
        let msg = Llvm.string_of_llvalue llv in
        ([Inst.nondet ~reg:(Some reg) ~msg ~loc], Exp.reg reg)
    | Instruction
        ( ( Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP
          | FPTrunc | FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast
          | Add | FAdd | Sub | FSub | Mul | FMul | UDiv | SDiv | FDiv | URem
          | SRem | FRem | Shl | LShr | AShr | And | Or | Xor | ICmp | FCmp
          | Select | GetElementPtr | ExtractElement | InsertElement
          | ShuffleVector | ExtractValue | InsertValue ) as opcode ) ->
        if inline || should_inline llv then xlate_opcode x llv opcode
        else ([], Exp.reg (xlate_name x llv))
    | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
    | GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv ()
    | Instruction (CatchPad | CleanupPad | CatchSwitch) ->
        todo "windows exception handling: %a" pp_llvalue llv ()
    | Instruction
        ( Invalid | Ret | Br | Switch | IndirectBr | Invalid2 | Unreachable
        | Store | UserOp1 | UserOp2 | Fence | AtomicCmpXchg | AtomicRMW
        | Resume | CleanupRet | CatchRet )
     |NullValue | BasicBlock | InlineAsm | MDNode | MDString ->
        fail "xlate_value: %a" pp_llvalue llv ()
  in
  ValTbl.find_or_add memo_value (inline, llv) ~default:(fun () ->
      [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue llv]
      ;
      xlate_value_ llv
      |>
      [%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp] )

and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Inst.t list * Exp.t
    =
 fun x llv opcode ->
  [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue llv]
  ;
  let xlate_rand i = xlate_value x (Llvm.operand llv i) in
  let typ = lazy (xlate_type x (Llvm.type_of llv)) in
  let convert opcode =
    let dst = Lazy.force typ in
    let rand = Llvm.operand llv 0 in
    let src = xlate_type x (Llvm.type_of rand) in
    let pre, arg = xlate_value 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
    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 ->
        Exp.or_ ~typ:Typ.bool (Exp.uno ?typ e f) (mk ?typ e f) )
  in
  ( match opcode with
  | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc
   |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast ->
      convert opcode
  | ICmp -> (
    match Option.get_exn (Llvm.icmp_predicate llv) with
    | Eq -> binary Exp.eq
    | Ne -> binary Exp.dq
    | Sgt -> binary Exp.gt
    | Sge -> binary Exp.ge
    | Slt -> binary Exp.lt
    | Sle -> binary Exp.le
    | Ugt -> binary Exp.ugt
    | Uge -> binary Exp.uge
    | Ult -> binary Exp.ult
    | Ule -> binary Exp.ule )
  | FCmp -> (
    match Llvm.fcmp_predicate llv with
    | None | Some False -> binary (fun ?typ:_ _ _ -> Exp.false_)
    | Some Oeq -> binary Exp.eq
    | Some Ogt -> binary Exp.gt
    | Some Oge -> binary Exp.ge
    | Some Olt -> binary Exp.lt
    | Some Ole -> binary Exp.le
    | Some One -> binary Exp.dq
    | Some Ord -> binary Exp.ord
    | Some Uno -> binary Exp.uno
    | Some Ueq -> unordered_or Exp.eq
    | Some Ugt -> unordered_or Exp.gt
    | Some Uge -> unordered_or Exp.ge
    | Some Ult -> unordered_or Exp.lt
    | Some Ule -> unordered_or Exp.le
    | Some Une -> unordered_or Exp.dq
    | Some True -> binary (fun ?typ:_ _ _ -> Exp.true_) )
  | Add | FAdd -> binary Exp.add
  | Sub | FSub -> binary Exp.sub
  | Mul | FMul -> binary Exp.mul
  | SDiv | FDiv -> binary Exp.div
  | UDiv -> binary Exp.udiv
  | SRem | FRem -> binary Exp.rem
  | URem -> binary Exp.urem
  | Shl -> binary Exp.shl
  | LShr -> binary Exp.lshr
  | AShr -> binary Exp.ashr
  | And -> binary Exp.and_
  | Or -> binary Exp.or_
  | Xor -> binary Exp.xor
  | Select ->
      let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 1)) in
      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
        let llelt = Llvm.element_type lltyp in
        let elt = xlate_type x llelt in
        let len = Llvm.vector_size lltyp in
        let bits = bit_size_of x lltyp in
        let byts = size_of x lltyp in
        Typ.array ~elt ~len ~bits ~byts
      in
      let idx i =
        match xlate_rand i with
        | pre, Integer {data} -> (pre, Z.to_int data)
        | _ -> todo "vector operations: %a" pp_llvalue llv ()
      in
      let pre_0, rcd = xlate_rand 0 in
      match opcode with
      | 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 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 pre0 i rcd typ =
        let rcd_i, typ_i, upd =
          match (typ : Typ.t) with
          | Tuple {elts} | Struct {elts} ->
              ( Exp.select typ rcd indices.(i)
              , snd (IArray.get elts indices.(i))
              , Exp.update typ ~rcd indices.(i) )
          | Array {elt} ->
              ( Exp.select typ rcd indices.(i)
              , elt
              , Exp.update typ ~rcd indices.(i) )
          | _ -> fail "xlate_value: %a" pp_llvalue llv ()
        in
        let update_or_return elt ret =
          match[@warning "p"] opcode with
          | InsertValue ->
              let pre, elt = Lazy.force elt in
              (pre0 @ pre, upd ~elt)
          | ExtractValue -> (pre0, ret)
        in
        if i < num - 1 then
          let pre, elt = xlate_indices pre0 (i + 1) rcd_i typ_i in
          update_or_return (lazy (pre, elt)) elt
        else
          let pre_elt = lazy (xlate_rand 1) in
          update_or_return pre_elt rcd_i
      in
      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 () ;
      let len = Llvm.num_operands llv in
      assert (len > 0 || invalid_llvm (Llvm.string_of_llvalue llv)) ;
      if len = 1 then convert BitCast
      else
        let rec xlate_indices i =
          [%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)))
              arg_i
          in
          ( if i = 1 then
            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
              | Pointer -> Llvm.element_type lltyp
              | _ -> fail "xlate_opcode: %i %a" i pp_llvalue llv ()
            in
            (* translate [gep t*, iN M] as [gep [1 x t]*, iN M] *)
            ((pre_0 @ pre_i, ptr_idx x ~ptr:base ~idx ~llelt), llelt)
          else
            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
                ((pre_i1 @ pre_i, ptr_idx x ~ptr ~idx ~llelt), llelt)
            | Struct ->
                let fld =
                  match
                    Option.bind ~f:Int64.unsigned_to_int
                      (Llvm.int64_of_const (Llvm.operand llv i))
                  with
                  | Some n -> n
                  | None -> fail "xlate_opcode: %i %a" i pp_llvalue llv ()
                in
                let llelt = (Llvm.struct_element_types lltyp).(fld) in
                ((pre_i1 @ pre_i, ptr_fld x ~ptr ~fld ~lltyp), llelt)
            | _ -> fail "xlate_opcode: %i %a" i pp_llvalue llv () )
          |>
          [%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 -> (
      (* translate shufflevector <N x t> %x, _, <N x i32> zeroinitializer to
         %x *)
      let exp = xlate_value x (Llvm.operand llv 0) in
      let exp_typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in
      let llmask = Llvm.operand llv 2 in
      let mask_typ = xlate_type x (Llvm.type_of llmask) in
      match (exp_typ, mask_typ) with
      | Array {len= m}, Array {len= n} when m = n && Llvm.is_null llmask ->
          exp
      | _ -> todo "vector operations: %a" pp_llvalue llv () )
  | Invalid | Ret | Br | Switch | IndirectBr | Invoke | Invalid2
   |Unreachable | Alloca | Load | Store | PHI | Call | UserOp1 | UserOp2
   |Fence | AtomicCmpXchg | AtomicRMW | Resume | LandingPad | CleanupRet
   |CatchRet | CatchPad | CleanupPad | CatchSwitch | VAArg ->
      fail "xlate_opcode: %a" pp_llvalue llv () )
  |>
  [%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp]

and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t =
 fun x llg ->
  GlobTbl.find_or_add memo_global llg ~default:(fun () ->
      [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue llg]
      ;
      let g =
        Global.mk (xlate_type x (Llvm.type_of llg)) (fst (find_name llg))
      in
      let loc = find_loc llg in
      (* add to tbl without initializer in case of recursive occurrences in
         its own initializer *)
      GlobTbl.set memo_global ~key:llg ~data:(GlobalDefn.mk g loc) ;
      let init =
        match Llvm.classify_value llg with
        | GlobalVariable ->
            Option.map (Llvm.global_initializer llg) ~f:(fun llv ->
                let pre, init = xlate_value x llv in
                (* Nondet insts to set up globals can be dropped to simply
                   leave the undef regs unconstrained. Other insts to set up
                   globals are currently not supported *)
                let is_nondet = function Nondet _ -> true | _ -> false in
                if not (List.for_all ~f:is_nondet pre) then
                  todo "global initializer instructions" () ;
                init )
        | _ -> None
      in
      GlobalDefn.mk ?init g loc
      |>
      [%Trace.retn fun {pf} -> pf "%a" GlobalDefn.pp] )

type pop_thunk = Loc.t -> Llair.inst list

let pop_stack_frame_of_function :
    x -> Llvm.llvalue -> Llvm.llbasicblock -> pop_thunk =
 fun x func entry_blk ->
  let append_stack_regs blk regs =
    Llvm.fold_right_instrs
      (fun instr regs ->
        match Llvm.instr_opcode instr with
        | Alloca -> xlate_name x instr :: regs
        | _ -> regs )
      blk regs
  in
  let entry_regs = append_stack_regs entry_blk [] in
  Llvm.iter_blocks
    (fun blk ->
      if not (Poly.equal entry_blk blk) then
        Llvm.iter_instrs
          (fun instr ->
            match Llvm.instr_opcode instr with
            | Alloca ->
                warn "stack allocation after function entry:@ %a" Loc.pp
                  (find_loc instr) ()
            | _ -> () )
          blk )
    func ;
  let pop retn_loc =
    List.map entry_regs ~f:(fun reg ->
        Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc )
  in
  pop

let check_exception_typ x instr llt =
  if
    not
      ( Poly.(Llvm.classify_type llt = Struct)
      &&
      let llelts = Llvm.struct_element_types llt in
      Array.length llelts = 2
      && Poly.(llelts.(0) = Llvm.pointer_type (Llvm.i8_type x.llcontext))
      && Poly.(llelts.(1) = Llvm.i32_type x.llcontext) )
  then
    todo "exception of type other than {i8*, i32}: %a" pp_llvalue instr ()

(** construct the types involved in landingpads: i32, std::type_info*, and
    __cxa_exception *)
let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
 fun x instr ->
  check_exception_typ x instr (Llvm.type_of instr) ;
  let i32 = i32 x in
  let llcontext =
    Llvm.(
      module_context (global_parent (block_parent (instr_parent instr))))
  in
  let llpi8 = Llvm.(pointer_type (integer_type llcontext 8)) in
  let ti = Llvm.(named_struct_type llcontext "class.std::type_info") in
  let tip = Llvm.pointer_type ti in
  let void = Llvm.void_type llcontext in
  let dtor = Llvm.(pointer_type (function_type void [|llpi8|])) in
  let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in
  (i32, xlate_type x tip, cxa_exception)

let exception_typs =
  let pi8 = Typ.pointer ~elt:Typ.byt in
  let i32 = Typ.integer ~bits:32 ~byts:4 in
  let exc =
    Typ.tuple (IArray.of_array [|(0, pi8); (8, i32)|]) ~bits:96 ~byts:12
  in
  (pi8, i32, exc)

(** Translate a control transfer from instruction [instr] to block [dst] to
    a jump, if necessary by extending [blocks] with a trampoline containing
    the PHIs of [dst] translated to a move. *)
let xlate_jump :
       x
    -> ?reg_exps:(Reg.t * (Inst.t list * Exp.t)) list
    -> Llvm.llvalue
    -> Llvm.llbasicblock
    -> Loc.t
    -> 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) =
    match pos with
    | Before dst_instr -> (
      match Llvm.instr_opcode dst_instr with
      | PHI ->
          let reg_exp =
            List.find_map_exn (Llvm.incoming dst_instr)
              ~f:(fun (arg, pred) ->
                if Poly.equal pred src then
                  Some (xlate_name x dst_instr, xlate_value x arg)
                else None )
          in
          xlate_jump_ (reg_exp :: reg_exps) (Llvm.instr_succ dst_instr)
      | _ -> reg_exps )
    | At_end blk -> fail "xlate_jump: %a" pp_llblock blk ()
  in
  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)
  | rev_reg_pre_exps ->
      let rev_reg_exps, rev_pre =
        List.fold_map rev_reg_pre_exps []
          ~f:(fun (reg, (pre, exp)) rev_pre ->
            ((reg, exp), List.rev_append pre rev_pre) )
      in
      let mov =
        Inst.move ~reg_exps:(IArray.of_list_rev rev_reg_exps) ~loc
      in
      let src_lbl = label_of_block (Llvm.instr_parent instr) in
      let lbl = src_lbl ^ ".jmp." ^ dst_lbl in
      let blk =
        Block.mk ~lbl
          ~cmnd:(IArray.of_array [|mov|])
          ~term:(Term.goto ~dst:jmp ~loc)
      in
      let blocks =
        match List.find blocks ~f:(fun b -> String.equal lbl b.lbl) with
        | None -> blk :: blocks
        | Some blk0 ->
            assert (Block.equal blk0 blk) ;
            blocks
      in
      (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
    (that is, essentially a function body). These are needed since LLVM and
    LLAIR blocks are not in 1:1 correspondence. *)
type code = Llair.inst list * Llair.term * Llair.block list

let pp_code fs (insts, term, blocks) =
  Format.fprintf fs "@[<hv>@,@[%a%t@]%t@[<hv>%a@]@]" (List.pp "@ " Inst.pp)
    insts
    (fun fs ->
      match term with
      | Unreachable -> ()
      | _ ->
          Format.fprintf fs "%t%a"
            (fun fs ->
              if List.is_empty insts then () else Format.fprintf fs "@ " )
            Term.pp term )
    (fun fs -> if List.is_empty blocks then () else Format.fprintf fs "@\n")
    (List.pp "@ " Block.pp) blocks

module StringS = HashSet.Make (String)

let ignored_callees = StringS.create 0

let xlate_size_of x llv =
  Exp.integer Typ.siz (Z.of_int (size_of x (Llvm.type_of llv)))

let norm_callee llfunc =
  match Llvm.classify_value llfunc with
  | Function | Instruction _ | InlineAsm | Argument -> llfunc
  | ConstantExpr -> (
    match Llvm.constexpr_opcode llfunc with
    | BitCast -> Llvm.operand llfunc 0
    | _ -> todo "callee kind %a" pp_llvalue llfunc () )
  | _ -> todo "callee kind %a" pp_llvalue llfunc ()

let num_actuals instr lltyp llfunc =
  assert (Poly.(Llvm.classify_type lltyp = Pointer)) ;
  let llelt = Llvm.element_type lltyp in
  if not (Llvm.is_var_arg llelt) then Llvm.num_arg_operands instr
  else
    let fname = Llvm.value_name llfunc in
    let is_decl llfunc =
      Poly.(Llvm.classify_value llfunc = Function)
      (* llfunc might be a formal, which Llvm.is_declaration doesn't like *)
      && Llvm.is_declaration llfunc
    in
    if StringS.add ignored_callees fname && not (is_decl llfunc) then
      warn "ignoring variable arguments to variadic function: %s" fname () ;
    Array.length (Llvm.param_types llelt)

let xlate_intrinsic_inst emit_inst x name_segs instr num_actuals loc =
  let emit_inst ?prefix inst = Some (emit_inst ?prefix inst) in
  match name_segs with
  | ["__llair_choice"] ->
      let reg = xlate_name x instr in
      let msg = "__llair_choice" in
      emit_inst (Inst.nondet ~reg:(Some reg) ~msg ~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)) arg
      in
      let len = 1 in
      emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc)
  | ["_Znam" (* operator new[](unsigned long) *)]
   |["_Znwm" (* operator new(size_t num) *)]
   |[ "_ZnwmSt11align_val_t"
      (* operator new(unsigned long, std::align_val_t) *) ]
    when num_actuals > 0 ->
      let reg = xlate_name x instr in
      let prefix, num = xlate_value x (Llvm.operand instr 0) in
      let len = size_of x (Llvm.type_of instr) in
      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) *) ]
   |[ "_ZdlPvmSt11align_val_t"
      (* operator delete(void* ptr, unsigned long, std::align_val_t) *) ]
   |["free" (* void free(void* ptr) *)] ->
      let prefix, ptr = xlate_value x (Llvm.operand instr 0) in
      emit_inst ~prefix (Inst.free ~ptr ~loc)
  | ["abort"] | ["llvm"; "trap"] -> emit_inst (Inst.abort ~loc)
  | [iname] | "llvm" :: iname :: _ -> (
    match Intrinsic.of_name iname with
    | Some name ->
        let reg = xlate_name_opt x instr in
        let xlate_arg i pre =
          let pre_i, arg_i = xlate_value x (Llvm.operand instr i) in
          (arg_i, pre_i @ pre)
        in
        let prefix, args =
          Iter.fold_map ~f:xlate_arg Iter.(0 -- (num_actuals - 1)) []
        in
        let args = IArray.of_iter args in
        emit_inst ~prefix (Inst.intrinsic ~reg ~name ~args ~loc)
    | None -> None )
  | _ -> None

let calls_to_backpatch = ref []

let term_call x llcallee ~typ ~actuals ~areturn ~return ~throw ~loc =
  match Llvm.classify_value llcallee with
  | Function ->
      let name = Llvm.value_name llcallee in
      let call, backpatch =
        Term.call ~name ~typ ~actuals ~areturn ~return ~throw ~loc
      in
      calls_to_backpatch :=
        (llcallee, typ, backpatch) :: !calls_to_backpatch ;
      ([], call)
  | _ ->
      let prefix, callee = xlate_value x llcallee in
      (prefix, Term.icall ~callee ~typ ~actuals ~areturn ~return ~throw ~loc)

let xlate_instr :
       pop_thunk
    -> x
    -> Llvm.llvalue
    -> ((Llair.inst list * Llair.term -> code) -> code)
    -> code =
 fun pop x instr continue ->
  [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue instr]
  ;
  let continue insts_term_to_code =
    [%Trace.retn
      fun {pf} () ->
        pf "%a" pp_code (insts_term_to_code ([], Term.unreachable))]
      () ;
    continue insts_term_to_code
  in
  let nop () = continue (fun (insts, term) -> (insts, term, [])) in
  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)] () ;
    (prefix, term, blocks)
  in
  let loc = find_loc instr in
  let inline_or_move xlate =
    if should_inline instr then nop ()
    else
      let reg = xlate_name x instr in
      let prefix, exp = xlate instr in
      let reg_exps = IArray.of_array [|(reg, exp)|] in
      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 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 pre0, exp = xlate_value x rand0 in
      let len = xlate_size_of x rand0 in
      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 num_elts = Llvm.operand instr 0 in
      let prefix, num = xlate_value x num_elts in
      let num = convert_to_siz (xlate_type x (Llvm.type_of num_elts)) num in
      assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
      let len = size_of x (Llvm.element_type (Llvm.type_of instr)) in
      emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc)
  | Call -> (
      let llcallee = Llvm.operand instr (Llvm.num_operands instr - 1) in
      let lltyp = Llvm.type_of llcallee in
      let llcallee = norm_callee llcallee in
      let num_actuals = num_actuals instr lltyp llcallee in
      let fname = Llvm.value_name llcallee in
      let name_segs = String.split_on_char fname ~by:'.' in
      let skip msg =
        if StringS.add ignored_callees fname then
          warn "ignoring uninterpreted %s %s" msg fname () ;
        let reg = xlate_name_opt x instr in
        emit_inst (Inst.nondet ~reg ~msg:fname ~loc)
      in
      (* intrinsics *)
      match xlate_intrinsic_exp fname with
      | Some intrinsic -> inline_or_move (intrinsic x)
      | None -> (
        match
          xlate_intrinsic_inst emit_inst x name_segs instr num_actuals loc
        with
        | Some code -> code
        | None -> (
          match name_segs with
          | ["__llair_throw"] ->
              let pre, exc = xlate_value x (Llvm.operand instr 0) in
              emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc)
          | ["__llair_unreachable"] -> emit_term Term.unreachable
          (* dropped / handled elsewhere *)
          | ["llvm"; "dbg"; ("declare" | "label" | "value")]
           |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _
            ->
              nop ()
          (* unimplemented *)
          | ["llvm"; ("stacksave" | "stackrestore")] ->
              skip "dynamic stack deallocation"
          | "llvm" :: "coro" :: _ ->
              todo "coroutines:@ %a" pp_llvalue instr ()
          | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ ->
              todo "statepoints:@ %a" pp_llvalue instr ()
          | ["llvm"; ("va_start" | "va_copy" | "va_end")] ->
              skip "variadic function intrinsic"
          | "llvm" :: _ -> skip "intrinsic"
          | _ when Poly.equal (Llvm.classify_value llcallee) InlineAsm ->
              skip "inline asm"
          (* general function call that may not throw *)
          | _ ->
              let typ = xlate_type x lltyp in
              let name, _ = find_name instr in
              let lbl = name ^ ".ret" in
              let pre_1, actuals =
                xlate_values x num_actuals (Llvm.operand instr)
              in
              let areturn = xlate_name_opt x instr in
              let return = Jump.mk lbl in
              let pre_0, call =
                term_call x llcallee ~typ ~actuals ~areturn ~return
                  ~throw:None ~loc
              in
              continue (fun (insts, term) ->
                  let cmnd = IArray.of_list insts in
                  (pre_0 @ pre_1, call, [Block.mk ~lbl ~cmnd ~term]) ) ) ) )
  | Invoke -> (
      let llcallee = Llvm.operand instr (Llvm.num_operands instr - 3) in
      let lltyp = Llvm.type_of llcallee in
      let llcallee = norm_callee llcallee in
      let num_actuals = num_actuals instr lltyp llcallee in
      let fname = Llvm.value_name llcallee in
      let name_segs = String.split_on_char fname ~by:'.' in
      let return_blk = Llvm.get_normal_dest instr in
      let unwind_blk = Llvm.get_unwind_dest instr in<commit_msg>[sledge] Update operand index of Invoke callee<commit_after>(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

(** Translate LLVM to LLAIR *)

open Llair

let pp_lltype fs t = Format.pp_print_string fs (Llvm.string_of_lltype t)

(* WARNING: SLOW on instructions and functions *)
let pp_llvalue fs t = Format.pp_print_string fs (Llvm.string_of_llvalue t)

let pp_llblock fs t =
  Format.pp_print_string fs (Llvm.string_of_llvalue (Llvm.value_of_block t))

;;
Exp.demangle :=
  let open Ctypes in
  let cxa_demangle =
    (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
    Foreign.foreign "__cxa_demangle"
      ( string
      @-> ptr char
      @-> ptr size_t
      @-> ptr int
      @-> returning string_opt )
  in
  let null_ptr_char = from_voidp char null in
  let null_ptr_size_t = from_voidp size_t null in
  let status = allocate int 0 in
  fun mangled ->
    if String.prefix ~pre:"_Z" mangled then
      let demangled =
        cxa_demangle mangled null_ptr_char null_ptr_size_t status
      in
      if !@status = 0 then demangled else None
    else None

exception Invalid_llvm of string

let invalid_llvm : string -> 'a =
 fun msg ->
  let first_line =
    Option.map_or ~default:msg
      ~f:(fun i -> String.take i msg)
      (String.index msg '\n')
  in
  Format.printf "@\n%s@\n" msg ;
  raise (Invalid_llvm first_line)

(* gather names and debug locations *)

(* number of register ids used so far *)
let sym_count = ref 0

(* map frontend-synthesized register names to ids, registers that come from
   LLVM are stored in sym_tbl *)
let id_memo = String.Tbl.create ()

(* lookup or generate the id for a frontend-synthesized register name *)
let get_id name =
  String.Tbl.find_or_add id_memo name ~default:(fun () ->
      incr sym_count ;
      !sym_count )

module LlvalueTbl = HashTable.Make (struct
  type t = Llvm.llvalue

  include Poly
end)

module SymTbl = LlvalueTbl

let sym_tbl : (string * int * Loc.t) SymTbl.t =
  SymTbl.create ~size:4_194_304 ()

module ScopeTbl = HashTable.Make (struct
  type t = [`Fun of Llvm.llvalue | `Mod of Llvm.llmodule]

  include Poly
end)

let scope_tbl : (int ref * int String.Tbl.t) ScopeTbl.t =
  ScopeTbl.create ~size:32_768 ()

let realpath_tbl = String.Tbl.create ()

let get_debug_loc_directory llv =
  let+ dir = Llvm.get_debug_loc_directory llv in
  if String.is_empty dir then dir
  else
    String.Tbl.find_or_add realpath_tbl dir ~default:(fun () ->
        try Core.Filename.realpath dir with Unix.Unix_error _ -> dir )

open struct
  open struct
    let loc_of_global g =
      Loc.mk
        ~dir:(get_debug_loc_directory g)
        ~file:(Llvm.get_debug_loc_filename g)
        ~line:(Some (Llvm.get_debug_loc_line g))
        ~col:None

    let loc_of_function f =
      Loc.mk
        ~dir:(get_debug_loc_directory f)
        ~file:(Llvm.get_debug_loc_filename f)
        ~line:(Some (Llvm.get_debug_loc_line f))
        ~col:None

    let loc_of_instr i =
      Loc.mk
        ~dir:(get_debug_loc_directory i)
        ~file:(Llvm.get_debug_loc_filename i)
        ~line:(Some (Llvm.get_debug_loc_line i))
        ~col:(Some (Llvm.get_debug_loc_column i))

    let find_scope scope =
      ScopeTbl.find_or_add scope_tbl scope ~default:(fun () ->
          (ref 0, String.Tbl.create ()) )

    let add_sym llv loc =
      let maybe_scope =
        match Llvm.classify_value llv with
        | Argument -> Some (`Fun (Llvm.param_parent llv))
        | BasicBlock ->
            Some (`Fun (Llvm.block_parent (Llvm.block_of_value llv)))
        | Instruction _ ->
            Some (`Fun (Llvm.block_parent (Llvm.instr_parent llv)))
        | GlobalVariable | Function -> Some (`Mod (Llvm.global_parent llv))
        | UndefValue -> None
        | ConstantExpr -> None
        | ConstantPointerNull -> None
        | _ ->
            warn "Unexpected type of llv, might crash: %a" pp_llvalue llv () ;
            Some (`Mod (Llvm.global_parent llv))
      in
      match maybe_scope with
      | None -> ()
      | Some scope -> (
        match SymTbl.find sym_tbl llv with
        | Some (name, id, loc0) ->
            if Loc.equal loc0 Loc.none then
              SymTbl.set sym_tbl ~key:llv ~data:(name, id, loc)
        | None ->
            let name =
              if Poly.(Llvm.classify_type (Llvm.type_of llv) = Void) then
                if Poly.(Llvm.classify_value llv = Instruction Call) then (
                  (* LLVM does not give unique names to the result of
                     void-returning function calls. We need unique names for
                     these as they determine the labels of newly-created
                     return blocks. *)
                  let next, void_tbl = find_scope scope in
                  let fname =
                    match
                      Llvm.(value_name (operand llv (num_operands llv - 1)))
                    with
                    | "" -> Int.to_string (!next - 1)
                    | s -> s
                  in
                  match String.Tbl.find void_tbl fname with
                  | None ->
                      String.Tbl.set void_tbl ~key:fname ~data:1 ;
                      fname ^ ".void"
                  | Some count ->
                      String.Tbl.set void_tbl ~key:fname ~data:(count + 1) ;
                      String.concat ~sep:""
                        [fname; ".void."; Int.to_string count] )
                else ""
              else
                match Llvm.value_name llv with
                | "" ->
                    (* anonymous values take the next SSA name *)
                    let next, _ = find_scope scope in
                    let name = !next in
                    next := name + 1 ;
                    Int.to_string name
                | name -> (
                  match Int.of_string name with
                  | Some _ ->
                      (* escape to avoid clash with names of anonymous
                         values *)
                      "\"" ^ name ^ "\""
                  | None -> name )
            in
            let id = 1 + SymTbl.length sym_tbl in
            SymTbl.set sym_tbl ~key:llv ~data:(name, id, loc) )
  end

  let scan_names_and_locs : Llvm.llmodule -> unit =
   fun m ->
    assert (!sym_count = 0) ;
    let scan_global g = add_sym g (loc_of_global g) in
    let scan_instr i =
      let loc = loc_of_instr i in
      add_sym i loc ;
      match Llvm.instr_opcode i with
      | Call -> (
        match Llvm.(value_name (operand i (num_arg_operands i))) with
        | "llvm.dbg.declare" ->
            let md = Llvm.(get_mdnode_operands (operand i 0)) in
            if not (Array.is_empty md) then add_sym md.(0) loc
            else
              warn
                "could not find variable for debug info at %a with \
                 metadata %a"
                Loc.pp loc (List.pp ", " pp_llvalue) (Array.to_list md) ()
        | _ -> () )
      | _ -> ()
    in
    let scan_block b =
      add_sym (Llvm.value_of_block b) Loc.none ;
      Llvm.iter_instrs scan_instr b
    in
    let scan_function f =
      Llvm.iter_params (fun prm -> add_sym prm Loc.none) f ;
      add_sym f (loc_of_function f) ;
      Llvm.iter_blocks scan_block f
    in
    Llvm.iter_globals scan_global m ;
    Llvm.iter_functions scan_function m ;
    sym_count := SymTbl.length sym_tbl

  let find_name : Llvm.llvalue -> string * int =
   fun v ->
    let name, id, _ = SymTbl.find_exn sym_tbl v in
    assert (not (String.is_empty name)) ;
    (name, id)

  let find_loc : Llvm.llvalue -> Loc.t =
   fun v -> trd3 (SymTbl.find_exn sym_tbl v)
end

let label_of_block : Llvm.llbasicblock -> string =
 fun blk -> fst (find_name (Llvm.value_of_block blk))

module LltypeTbl = HashTable.Make (struct
  type t = Llvm.lltype

  include Poly
end)

let anon_struct_name : string LltypeTbl.t = LltypeTbl.create ()

let struct_name : Llvm.lltype -> string =
 fun llt ->
  match Llvm.struct_name llt with
  | Some name -> name
  | None ->
      LltypeTbl.find_or_add anon_struct_name llt ~default:(fun () ->
          Int.to_string (LltypeTbl.length anon_struct_name) )

type x = {llcontext: Llvm.llcontext; lldatalayout: Llvm_target.DataLayout.t}

let ptr_siz : x -> int =
 fun x -> Llvm_target.DataLayout.pointer_size x.lldatalayout

let size_of, bit_size_of =
  let size_to_int size_of x llt =
    if Llvm.type_is_sized llt then
      match Int64.unsigned_to_int (size_of llt x.lldatalayout) with
      | Some n -> n
      | None -> todo "type size too large: %a" pp_lltype llt ()
    else todo "types with undetermined size: %a" pp_lltype llt ()
  in
  ( size_to_int Llvm_target.DataLayout.abi_size
  , size_to_int Llvm_target.DataLayout.size_in_bits )

let memo_type : Typ.t LltypeTbl.t = LltypeTbl.create ()

let rec xlate_type : x -> Llvm.lltype -> Typ.t =
 fun x llt ->
  let xlate_type_ llt =
    if Llvm.type_is_sized llt then
      let byts = size_of x llt in
      let bits = bit_size_of x llt in
      match Llvm.classify_type llt with
      | Half | Float | Double | Fp128 -> Typ.float ~bits ~byts ~enc:`IEEE
      | X86fp80 -> Typ.float ~bits ~byts ~enc:`Extended
      | Ppc_fp128 -> Typ.float ~bits ~byts ~enc:`Pair
      | Integer -> Typ.integer ~bits ~byts
      | X86_mmx -> Typ.integer ~bits ~byts
      | Pointer ->
          if byts <> ptr_siz x then
            todo "non-integral pointer types: %a" pp_lltype llt () ;
          let elt = xlate_type x (Llvm.element_type llt) in
          Typ.pointer ~elt
      | Array ->
          let elt = xlate_type x (Llvm.element_type llt) in
          let len = Llvm.array_length llt in
          Typ.array ~elt ~len ~bits ~byts
      | Struct ->
          let llelts = Llvm.struct_element_types llt in
          let len = Array.length llelts in
          let fld_off i =
            match
              Int64.unsigned_to_int
                (Llvm_target.DataLayout.offset_of_element llt i
                   x.lldatalayout)
            with
            | Some i -> i
            | None -> todo "offset too large: %a" pp_lltype llt ()
          in
          if Llvm.is_literal llt then
            let elts =
              IArray.mapi
                ~f:(fun i elt -> (fld_off i, xlate_type x elt))
                (IArray.of_array llelts)
            in
            Typ.tuple elts ~bits ~byts
          else
            let name = struct_name llt in
            let elts =
              IArray.init len ~f:(fun i ->
                  lazy (fld_off i, xlate_type x llelts.(i)) )
            in
            Typ.struct_ ~name elts ~bits ~byts
      | Function -> fail "expected to be unsized: %a" pp_lltype llt ()
      | Vector -> todo "vector types: %a" pp_lltype llt ()
      | Void | Label | Metadata | Token -> assert false
    else
      match Llvm.classify_type llt with
      | Function ->
          let return = xlate_type_opt x (Llvm.return_type llt) in
          let llargs = Llvm.param_types llt in
          let len = Array.length llargs in
          let args =
            IArray.init len ~f:(fun i -> xlate_type x llargs.(i))
          in
          Typ.function_ ~return ~args
      | Struct when Llvm.is_opaque llt -> Typ.opaque ~name:(struct_name llt)
      | Token -> Typ.opaque ~name:"token"
      | Vector | Array | Struct ->
          todo "unsized non-opaque aggregate types: %a" pp_lltype llt ()
      | Half | Float | Double | X86fp80 | Fp128 | Ppc_fp128 | Integer
       |X86_mmx | Pointer ->
          fail "expected to be sized: %a" pp_lltype llt ()
      | Void | Label | Metadata -> assert false
  in
  LltypeTbl.find_or_add memo_type llt ~default:(fun () ->
      [%Trace.call fun {pf} -> pf "@ %a" pp_lltype llt]
      ;
      xlate_type_ llt
      |>
      [%Trace.retn fun {pf} ty ->
        pf "%a" Typ.pp_defn ty ;
        assert (
          (not (Llvm.type_is_sized llt))
          || (not (Typ.is_sized ty))
          || Typ.size_of ty = size_of x llt )] )

and xlate_type_opt : x -> Llvm.lltype -> Typ.t option =
 fun x llt ->
  match Llvm.classify_type llt with
  | Void -> None
  | _ -> Some (xlate_type x llt)

let i32 x = xlate_type x (Llvm.i32_type x.llcontext)

let suffix_after_last_space : string -> string =
 fun str -> String.drop (String.rindex_exn str ' ' + 1) str

let xlate_int : x -> Llvm.llvalue -> Exp.t =
 fun x llv ->
  let llt = Llvm.type_of llv in
  let typ = xlate_type x llt in
  let data =
    match Llvm.int64_of_const llv with
    | Some n -> Z.of_int64 n
    | None ->
        Z.of_string (suffix_after_last_space (Llvm.string_of_llvalue llv))
  in
  Exp.integer typ data

let xlate_float : x -> Llvm.llvalue -> Exp.t =
 fun x llv ->
  let llt = Llvm.type_of llv in
  let typ = xlate_type x llt in
  let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in
  Exp.float typ data

let xlate_name x : Llvm.llvalue -> Reg.t =
 fun llv ->
  let typ = xlate_type x (Llvm.type_of llv) in
  let name, id = find_name llv in
  Reg.mk typ id name

let xlate_name_opt : x -> Llvm.llvalue -> Reg.t option =
 fun x instr ->
  let llt = Llvm.type_of instr in
  match Llvm.classify_type llt with
  | Void -> None
  | _ -> Some (xlate_name x instr)

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

(* per-function count of 'undef' values, used to translate each occurrence
   of 'undef' to a distinct register *)
let undef_count = ref 0

module GlobTbl = LlvalueTbl

let memo_global : GlobalDefn.t GlobTbl.t = GlobTbl.create ()

module ValTbl = HashTable.Make (struct
  type t = bool * Llvm.llvalue

  include Poly
end)

let memo_value : (Inst.t list * Exp.t) ValTbl.t = ValTbl.create ()

let should_inline : Llvm.llvalue -> bool =
 fun llv ->
  match Llvm.use_begin llv with
  | Some use -> (
    match Llvm.use_succ use with
    | Some _ -> (
      match Llvm.classify_value llv with
      | Instruction
          ( Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP
          | FPTrunc | FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast
            ) ->
          true (* inline casts *)
      | _ -> false (* do not inline if >= 2 uses *) )
    | None -> true )
  | None -> true

let ptr_fld x ~ptr ~fld ~lltyp =
  let offset =
    Llvm_target.DataLayout.offset_of_element lltyp fld x.lldatalayout
  in
  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:Typ.ptr ptr
    (Exp.mul ~typ:Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx)

let convert_to_siz =
  let siz_bits = Typ.bit_size_of Typ.siz in
  fun typ arg ->
    match (typ : Typ.t) with
    | Integer {bits} ->
        if siz_bits < bits then Exp.signed siz_bits arg ~to_:Typ.siz
        else if siz_bits > bits then Exp.signed bits arg ~to_:Typ.siz
        else arg
    | _ -> fail "convert_to_siz: %a" Typ.pp typ ()

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 :
    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 pre, arg = xlate_value x rand in
          let src = xlate_type x (Llvm.type_of rand) in
          (pre, xlate_llvm_eh_typeid_for x src arg) )
  | _ -> None

and xlate_values x len val_i =
  let xlate_i j pre_0_i =
    let pre_j, arg_j = xlate_value x (val_i j) in
    (arg_j, Iter.append pre_0_i (Iter.of_list pre_j))
  in
  let pre, vals = Iter.(fold_map (0 -- (len - 1)) empty ~f:xlate_i) in
  (Iter.to_list pre, IArray.of_iter vals)

and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
    =
 fun x llv ->
  let xlate_value_ llv =
    match Llvm.classify_value llv with
    | Instruction Call -> (
        let func = Llvm.operand llv (Llvm.num_arg_operands llv) in
        let fname = Llvm.value_name func in
        match xlate_intrinsic_exp fname with
        | Some intrinsic when inline || should_inline llv -> intrinsic x llv
        | _ -> ([], Exp.reg (xlate_name x llv)) )
    | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
     |Argument ->
        ([], Exp.reg (xlate_name x llv))
    | Function ->
        ( []
        , Exp.function_
            (Function.mk
               (xlate_type x (Llvm.type_of llv))
               (fst (find_name llv))) )
    | GlobalVariable -> ([], Exp.global (xlate_global x llv).name)
    | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
    | 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)
        | Array _ | Tuple _ | Struct _ ->
            ([], 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 pre, args = xlate_values x len (Llvm.operand llv) in
        (pre, Exp.record typ args)
    | ConstantDataVector ->
        let typ = xlate_type x (Llvm.type_of llv) in
        let len = Llvm.vector_size (Llvm.type_of llv) in
        let pre, args = xlate_values x len (Llvm.const_element llv) in
        (pre, Exp.record typ args)
    | ConstantDataArray ->
        let typ = xlate_type x (Llvm.type_of llv) in
        let len = Llvm.array_length (Llvm.type_of llv) in
        let pre, args = xlate_values x len (Llvm.const_element llv) in
        (pre, Exp.record typ args)
    | ConstantStruct ->
        let typ = xlate_type x (Llvm.type_of llv) in
        let len = Llvm.num_operands llv in
        let pre, args = xlate_values x len (Llvm.operand llv) in
        (pre, Exp.record typ args)
    | BlockAddress ->
        let parent, _ = find_name (Llvm.operand llv 0) in
        let name, _ = find_name (Llvm.operand llv 1) in
        ([], Exp.label ~parent ~name)
    | UndefValue ->
        let llt = Llvm.type_of llv in
        let typ = xlate_type x llt in
        if not (Typ.is_sized typ) then
          todo "types with undetermined size: %a" pp_lltype llt () ;
        let name = Printf.sprintf "undef_%i" !undef_count in
        let loc = Loc.none in
        let id = get_id name in
        let reg = Reg.mk typ id name in
        let msg = Llvm.string_of_llvalue llv in
        ([Inst.nondet ~reg:(Some reg) ~msg ~loc], Exp.reg reg)
    | Instruction
        ( ( Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP
          | FPTrunc | FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast
          | Add | FAdd | Sub | FSub | Mul | FMul | UDiv | SDiv | FDiv | URem
          | SRem | FRem | Shl | LShr | AShr | And | Or | Xor | ICmp | FCmp
          | Select | GetElementPtr | ExtractElement | InsertElement
          | ShuffleVector | ExtractValue | InsertValue ) as opcode ) ->
        if inline || should_inline llv then xlate_opcode x llv opcode
        else ([], Exp.reg (xlate_name x llv))
    | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
    | GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv ()
    | Instruction (CatchPad | CleanupPad | CatchSwitch) ->
        todo "windows exception handling: %a" pp_llvalue llv ()
    | Instruction
        ( Invalid | Ret | Br | Switch | IndirectBr | Invalid2 | Unreachable
        | Store | UserOp1 | UserOp2 | Fence | AtomicCmpXchg | AtomicRMW
        | Resume | CleanupRet | CatchRet )
     |NullValue | BasicBlock | InlineAsm | MDNode | MDString ->
        fail "xlate_value: %a" pp_llvalue llv ()
  in
  ValTbl.find_or_add memo_value (inline, llv) ~default:(fun () ->
      [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue llv]
      ;
      xlate_value_ llv
      |>
      [%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp] )

and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Inst.t list * Exp.t
    =
 fun x llv opcode ->
  [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue llv]
  ;
  let xlate_rand i = xlate_value x (Llvm.operand llv i) in
  let typ = lazy (xlate_type x (Llvm.type_of llv)) in
  let convert opcode =
    let dst = Lazy.force typ in
    let rand = Llvm.operand llv 0 in
    let src = xlate_type x (Llvm.type_of rand) in
    let pre, arg = xlate_value 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
    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 ->
        Exp.or_ ~typ:Typ.bool (Exp.uno ?typ e f) (mk ?typ e f) )
  in
  ( match opcode with
  | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc
   |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast ->
      convert opcode
  | ICmp -> (
    match Option.get_exn (Llvm.icmp_predicate llv) with
    | Eq -> binary Exp.eq
    | Ne -> binary Exp.dq
    | Sgt -> binary Exp.gt
    | Sge -> binary Exp.ge
    | Slt -> binary Exp.lt
    | Sle -> binary Exp.le
    | Ugt -> binary Exp.ugt
    | Uge -> binary Exp.uge
    | Ult -> binary Exp.ult
    | Ule -> binary Exp.ule )
  | FCmp -> (
    match Llvm.fcmp_predicate llv with
    | None | Some False -> binary (fun ?typ:_ _ _ -> Exp.false_)
    | Some Oeq -> binary Exp.eq
    | Some Ogt -> binary Exp.gt
    | Some Oge -> binary Exp.ge
    | Some Olt -> binary Exp.lt
    | Some Ole -> binary Exp.le
    | Some One -> binary Exp.dq
    | Some Ord -> binary Exp.ord
    | Some Uno -> binary Exp.uno
    | Some Ueq -> unordered_or Exp.eq
    | Some Ugt -> unordered_or Exp.gt
    | Some Uge -> unordered_or Exp.ge
    | Some Ult -> unordered_or Exp.lt
    | Some Ule -> unordered_or Exp.le
    | Some Une -> unordered_or Exp.dq
    | Some True -> binary (fun ?typ:_ _ _ -> Exp.true_) )
  | Add | FAdd -> binary Exp.add
  | Sub | FSub -> binary Exp.sub
  | Mul | FMul -> binary Exp.mul
  | SDiv | FDiv -> binary Exp.div
  | UDiv -> binary Exp.udiv
  | SRem | FRem -> binary Exp.rem
  | URem -> binary Exp.urem
  | Shl -> binary Exp.shl
  | LShr -> binary Exp.lshr
  | AShr -> binary Exp.ashr
  | And -> binary Exp.and_
  | Or -> binary Exp.or_
  | Xor -> binary Exp.xor
  | Select ->
      let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 1)) in
      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
        let llelt = Llvm.element_type lltyp in
        let elt = xlate_type x llelt in
        let len = Llvm.vector_size lltyp in
        let bits = bit_size_of x lltyp in
        let byts = size_of x lltyp in
        Typ.array ~elt ~len ~bits ~byts
      in
      let idx i =
        match xlate_rand i with
        | pre, Integer {data} -> (pre, Z.to_int data)
        | _ -> todo "vector operations: %a" pp_llvalue llv ()
      in
      let pre_0, rcd = xlate_rand 0 in
      match opcode with
      | 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 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 pre0 i rcd typ =
        let rcd_i, typ_i, upd =
          match (typ : Typ.t) with
          | Tuple {elts} | Struct {elts} ->
              ( Exp.select typ rcd indices.(i)
              , snd (IArray.get elts indices.(i))
              , Exp.update typ ~rcd indices.(i) )
          | Array {elt} ->
              ( Exp.select typ rcd indices.(i)
              , elt
              , Exp.update typ ~rcd indices.(i) )
          | _ -> fail "xlate_value: %a" pp_llvalue llv ()
        in
        let update_or_return elt ret =
          match[@warning "p"] opcode with
          | InsertValue ->
              let pre, elt = Lazy.force elt in
              (pre0 @ pre, upd ~elt)
          | ExtractValue -> (pre0, ret)
        in
        if i < num - 1 then
          let pre, elt = xlate_indices pre0 (i + 1) rcd_i typ_i in
          update_or_return (lazy (pre, elt)) elt
        else
          let pre_elt = lazy (xlate_rand 1) in
          update_or_return pre_elt rcd_i
      in
      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 () ;
      let len = Llvm.num_operands llv in
      assert (len > 0 || invalid_llvm (Llvm.string_of_llvalue llv)) ;
      if len = 1 then convert BitCast
      else
        let rec xlate_indices i =
          [%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)))
              arg_i
          in
          ( if i = 1 then
            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
              | Pointer -> Llvm.element_type lltyp
              | _ -> fail "xlate_opcode: %i %a" i pp_llvalue llv ()
            in
            (* translate [gep t*, iN M] as [gep [1 x t]*, iN M] *)
            ((pre_0 @ pre_i, ptr_idx x ~ptr:base ~idx ~llelt), llelt)
          else
            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
                ((pre_i1 @ pre_i, ptr_idx x ~ptr ~idx ~llelt), llelt)
            | Struct ->
                let fld =
                  match
                    Option.bind ~f:Int64.unsigned_to_int
                      (Llvm.int64_of_const (Llvm.operand llv i))
                  with
                  | Some n -> n
                  | None -> fail "xlate_opcode: %i %a" i pp_llvalue llv ()
                in
                let llelt = (Llvm.struct_element_types lltyp).(fld) in
                ((pre_i1 @ pre_i, ptr_fld x ~ptr ~fld ~lltyp), llelt)
            | _ -> fail "xlate_opcode: %i %a" i pp_llvalue llv () )
          |>
          [%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 -> (
      (* translate shufflevector <N x t> %x, _, <N x i32> zeroinitializer to
         %x *)
      let exp = xlate_value x (Llvm.operand llv 0) in
      let exp_typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in
      let llmask = Llvm.operand llv 2 in
      let mask_typ = xlate_type x (Llvm.type_of llmask) in
      match (exp_typ, mask_typ) with
      | Array {len= m}, Array {len= n} when m = n && Llvm.is_null llmask ->
          exp
      | _ -> todo "vector operations: %a" pp_llvalue llv () )
  | Invalid | Ret | Br | Switch | IndirectBr | Invoke | Invalid2
   |Unreachable | Alloca | Load | Store | PHI | Call | UserOp1 | UserOp2
   |Fence | AtomicCmpXchg | AtomicRMW | Resume | LandingPad | CleanupRet
   |CatchRet | CatchPad | CleanupPad | CatchSwitch | VAArg ->
      fail "xlate_opcode: %a" pp_llvalue llv () )
  |>
  [%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp]

and xlate_global : x -> Llvm.llvalue -> GlobalDefn.t =
 fun x llg ->
  GlobTbl.find_or_add memo_global llg ~default:(fun () ->
      [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue llg]
      ;
      let g =
        Global.mk (xlate_type x (Llvm.type_of llg)) (fst (find_name llg))
      in
      let loc = find_loc llg in
      (* add to tbl without initializer in case of recursive occurrences in
         its own initializer *)
      GlobTbl.set memo_global ~key:llg ~data:(GlobalDefn.mk g loc) ;
      let init =
        match Llvm.classify_value llg with
        | GlobalVariable ->
            Option.map (Llvm.global_initializer llg) ~f:(fun llv ->
                let pre, init = xlate_value x llv in
                (* Nondet insts to set up globals can be dropped to simply
                   leave the undef regs unconstrained. Other insts to set up
                   globals are currently not supported *)
                let is_nondet = function Nondet _ -> true | _ -> false in
                if not (List.for_all ~f:is_nondet pre) then
                  todo "global initializer instructions" () ;
                init )
        | _ -> None
      in
      GlobalDefn.mk ?init g loc
      |>
      [%Trace.retn fun {pf} -> pf "%a" GlobalDefn.pp] )

type pop_thunk = Loc.t -> Llair.inst list

let pop_stack_frame_of_function :
    x -> Llvm.llvalue -> Llvm.llbasicblock -> pop_thunk =
 fun x func entry_blk ->
  let append_stack_regs blk regs =
    Llvm.fold_right_instrs
      (fun instr regs ->
        match Llvm.instr_opcode instr with
        | Alloca -> xlate_name x instr :: regs
        | _ -> regs )
      blk regs
  in
  let entry_regs = append_stack_regs entry_blk [] in
  Llvm.iter_blocks
    (fun blk ->
      if not (Poly.equal entry_blk blk) then
        Llvm.iter_instrs
          (fun instr ->
            match Llvm.instr_opcode instr with
            | Alloca ->
                warn "stack allocation after function entry:@ %a" Loc.pp
                  (find_loc instr) ()
            | _ -> () )
          blk )
    func ;
  let pop retn_loc =
    List.map entry_regs ~f:(fun reg ->
        Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc )
  in
  pop

let check_exception_typ x instr llt =
  if
    not
      ( Poly.(Llvm.classify_type llt = Struct)
      &&
      let llelts = Llvm.struct_element_types llt in
      Array.length llelts = 2
      && Poly.(llelts.(0) = Llvm.pointer_type (Llvm.i8_type x.llcontext))
      && Poly.(llelts.(1) = Llvm.i32_type x.llcontext) )
  then
    todo "exception of type other than {i8*, i32}: %a" pp_llvalue instr ()

(** construct the types involved in landingpads: i32, std::type_info*, and
    __cxa_exception *)
let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
 fun x instr ->
  check_exception_typ x instr (Llvm.type_of instr) ;
  let i32 = i32 x in
  let llcontext =
    Llvm.(
      module_context (global_parent (block_parent (instr_parent instr))))
  in
  let llpi8 = Llvm.(pointer_type (integer_type llcontext 8)) in
  let ti = Llvm.(named_struct_type llcontext "class.std::type_info") in
  let tip = Llvm.pointer_type ti in
  let void = Llvm.void_type llcontext in
  let dtor = Llvm.(pointer_type (function_type void [|llpi8|])) in
  let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in
  (i32, xlate_type x tip, cxa_exception)

let exception_typs =
  let pi8 = Typ.pointer ~elt:Typ.byt in
  let i32 = Typ.integer ~bits:32 ~byts:4 in
  let exc =
    Typ.tuple (IArray.of_array [|(0, pi8); (8, i32)|]) ~bits:96 ~byts:12
  in
  (pi8, i32, exc)

(** Translate a control transfer from instruction [instr] to block [dst] to
    a jump, if necessary by extending [blocks] with a trampoline containing
    the PHIs of [dst] translated to a move. *)
let xlate_jump :
       x
    -> ?reg_exps:(Reg.t * (Inst.t list * Exp.t)) list
    -> Llvm.llvalue
    -> Llvm.llbasicblock
    -> Loc.t
    -> 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) =
    match pos with
    | Before dst_instr -> (
      match Llvm.instr_opcode dst_instr with
      | PHI ->
          let reg_exp =
            List.find_map_exn (Llvm.incoming dst_instr)
              ~f:(fun (arg, pred) ->
                if Poly.equal pred src then
                  Some (xlate_name x dst_instr, xlate_value x arg)
                else None )
          in
          xlate_jump_ (reg_exp :: reg_exps) (Llvm.instr_succ dst_instr)
      | _ -> reg_exps )
    | At_end blk -> fail "xlate_jump: %a" pp_llblock blk ()
  in
  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)
  | rev_reg_pre_exps ->
      let rev_reg_exps, rev_pre =
        List.fold_map rev_reg_pre_exps []
          ~f:(fun (reg, (pre, exp)) rev_pre ->
            ((reg, exp), List.rev_append pre rev_pre) )
      in
      let mov =
        Inst.move ~reg_exps:(IArray.of_list_rev rev_reg_exps) ~loc
      in
      let src_lbl = label_of_block (Llvm.instr_parent instr) in
      let lbl = src_lbl ^ ".jmp." ^ dst_lbl in
      let blk =
        Block.mk ~lbl
          ~cmnd:(IArray.of_array [|mov|])
          ~term:(Term.goto ~dst:jmp ~loc)
      in
      let blocks =
        match List.find blocks ~f:(fun b -> String.equal lbl b.lbl) with
        | None -> blk :: blocks
        | Some blk0 ->
            assert (Block.equal blk0 blk) ;
            blocks
      in
      (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
    (that is, essentially a function body). These are needed since LLVM and
    LLAIR blocks are not in 1:1 correspondence. *)
type code = Llair.inst list * Llair.term * Llair.block list

let pp_code fs (insts, term, blocks) =
  Format.fprintf fs "@[<hv>@,@[%a%t@]%t@[<hv>%a@]@]" (List.pp "@ " Inst.pp)
    insts
    (fun fs ->
      match term with
      | Unreachable -> ()
      | _ ->
          Format.fprintf fs "%t%a"
            (fun fs ->
              if List.is_empty insts then () else Format.fprintf fs "@ " )
            Term.pp term )
    (fun fs -> if List.is_empty blocks then () else Format.fprintf fs "@\n")
    (List.pp "@ " Block.pp) blocks

module StringS = HashSet.Make (String)

let ignored_callees = StringS.create 0

let xlate_size_of x llv =
  Exp.integer Typ.siz (Z.of_int (size_of x (Llvm.type_of llv)))

let norm_callee llfunc =
  match Llvm.classify_value llfunc with
  | Function | Instruction _ | InlineAsm | Argument -> llfunc
  | ConstantExpr -> (
    match Llvm.constexpr_opcode llfunc with
    | BitCast -> Llvm.operand llfunc 0
    | _ -> todo "callee kind %a" pp_llvalue llfunc () )
  | _ -> todo "callee kind %a" pp_llvalue llfunc ()

let num_actuals instr lltyp llfunc =
  assert (Poly.(Llvm.classify_type lltyp = Pointer)) ;
  let llelt = Llvm.element_type lltyp in
  if not (Llvm.is_var_arg llelt) then Llvm.num_arg_operands instr
  else
    let fname = Llvm.value_name llfunc in
    let is_decl llfunc =
      Poly.(Llvm.classify_value llfunc = Function)
      (* llfunc might be a formal, which Llvm.is_declaration doesn't like *)
      && Llvm.is_declaration llfunc
    in
    if StringS.add ignored_callees fname && not (is_decl llfunc) then
      warn "ignoring variable arguments to variadic function: %s" fname () ;
    Array.length (Llvm.param_types llelt)

let xlate_intrinsic_inst emit_inst x name_segs instr num_actuals loc =
  let emit_inst ?prefix inst = Some (emit_inst ?prefix inst) in
  match name_segs with
  | ["__llair_choice"] ->
      let reg = xlate_name x instr in
      let msg = "__llair_choice" in
      emit_inst (Inst.nondet ~reg:(Some reg) ~msg ~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)) arg
      in
      let len = 1 in
      emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc)
  | ["_Znam" (* operator new[](unsigned long) *)]
   |["_Znwm" (* operator new(size_t num) *)]
   |[ "_ZnwmSt11align_val_t"
      (* operator new(unsigned long, std::align_val_t) *) ]
    when num_actuals > 0 ->
      let reg = xlate_name x instr in
      let prefix, num = xlate_value x (Llvm.operand instr 0) in
      let len = size_of x (Llvm.type_of instr) in
      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) *) ]
   |[ "_ZdlPvmSt11align_val_t"
      (* operator delete(void* ptr, unsigned long, std::align_val_t) *) ]
   |["free" (* void free(void* ptr) *)] ->
      let prefix, ptr = xlate_value x (Llvm.operand instr 0) in
      emit_inst ~prefix (Inst.free ~ptr ~loc)
  | ["abort"] | ["llvm"; "trap"] -> emit_inst (Inst.abort ~loc)
  | [iname] | "llvm" :: iname :: _ -> (
    match Intrinsic.of_name iname with
    | Some name ->
        let reg = xlate_name_opt x instr in
        let xlate_arg i pre =
          let pre_i, arg_i = xlate_value x (Llvm.operand instr i) in
          (arg_i, pre_i @ pre)
        in
        let prefix, args =
          Iter.fold_map ~f:xlate_arg Iter.(0 -- (num_actuals - 1)) []
        in
        let args = IArray.of_iter args in
        emit_inst ~prefix (Inst.intrinsic ~reg ~name ~args ~loc)
    | None -> None )
  | _ -> None

let calls_to_backpatch = ref []

let term_call x llcallee ~typ ~actuals ~areturn ~return ~throw ~loc =
  match Llvm.classify_value llcallee with
  | Function ->
      let name = Llvm.value_name llcallee in
      let call, backpatch =
        Term.call ~name ~typ ~actuals ~areturn ~return ~throw ~loc
      in
      calls_to_backpatch :=
        (llcallee, typ, backpatch) :: !calls_to_backpatch ;
      ([], call)
  | _ ->
      let prefix, callee = xlate_value x llcallee in
      (prefix, Term.icall ~callee ~typ ~actuals ~areturn ~return ~throw ~loc)

let xlate_instr :
       pop_thunk
    -> x
    -> Llvm.llvalue
    -> ((Llair.inst list * Llair.term -> code) -> code)
    -> code =
 fun pop x instr continue ->
  [%Trace.call fun {pf} -> pf "@ %a" pp_llvalue instr]
  ;
  let continue insts_term_to_code =
    [%Trace.retn
      fun {pf} () ->
        pf "%a" pp_code (insts_term_to_code ([], Term.unreachable))]
      () ;
    continue insts_term_to_code
  in
  let nop () = continue (fun (insts, term) -> (insts, term, [])) in
  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)] () ;
    (prefix, term, blocks)
  in
  let loc = find_loc instr in
  let inline_or_move xlate =
    if should_inline instr then nop ()
    else
      let reg = xlate_name x instr in
      let prefix, exp = xlate instr in
      let reg_exps = IArray.of_array [|(reg, exp)|] in
      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 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 pre0, exp = xlate_value x rand0 in
      let len = xlate_size_of x rand0 in
      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 num_elts = Llvm.operand instr 0 in
      let prefix, num = xlate_value x num_elts in
      let num = convert_to_siz (xlate_type x (Llvm.type_of num_elts)) num in
      assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
      let len = size_of x (Llvm.element_type (Llvm.type_of instr)) in
      emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc)
  | Call -> (
      let llcallee = Llvm.operand instr (Llvm.num_operands instr - 1) in
      let lltyp = Llvm.type_of llcallee in
      let llcallee = norm_callee llcallee in
      let num_actuals = num_actuals instr lltyp llcallee in
      let fname = Llvm.value_name llcallee in
      let name_segs = String.split_on_char fname ~by:'.' in
      let skip msg =
        if StringS.add ignored_callees fname then
          warn "ignoring uninterpreted %s %s" msg fname () ;
        let reg = xlate_name_opt x instr in
        emit_inst (Inst.nondet ~reg ~msg:fname ~loc)
      in
      (* intrinsics *)
      match xlate_intrinsic_exp fname with
      | Some intrinsic -> inline_or_move (intrinsic x)
      | None -> (
        match
          xlate_intrinsic_inst emit_inst x name_segs instr num_actuals loc
        with
        | Some code -> code
        | None -> (
          match name_segs with
          | ["__llair_throw"] ->
              let pre, exc = xlate_value x (Llvm.operand instr 0) in
              emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc)
          | ["__llair_unreachable"] -> emit_term Term.unreachable
          (* dropped / handled elsewhere *)
          | ["llvm"; "dbg"; ("declare" | "label" | "value")]
           |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _
            ->
              nop ()
          (* unimplemented *)
          | ["llvm"; ("stacksave" | "stackrestore")] ->
              skip "dynamic stack deallocation"
          | "llvm" :: "coro" :: _ ->
              todo "coroutines:@ %a" pp_llvalue instr ()
          | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ ->
              todo "statepoints:@ %a" pp_llvalue instr ()
          | ["llvm"; ("va_start" | "va_copy" | "va_end")] ->
              skip "variadic function intrinsic"
          | "llvm" :: _ -> skip "intrinsic"
          | _ when Poly.equal (Llvm.classify_value llcallee) InlineAsm ->
              skip "inline asm"
          (* general function call that may not throw *)
          | _ ->
              let typ = xlate_type x lltyp in
              let name, _ = find_name instr in
              let lbl = name ^ ".ret" in
              let pre_1, actuals =
                xlate_values x num_actuals (Llvm.operand instr)
              in
              let areturn = xlate_name_opt x instr in
              let return = Jump.mk lbl in
              let pre_0, call =
                term_call x llcallee ~typ ~actuals ~areturn ~return
                  ~throw:None ~loc
              in
              continue (fun (insts, term) ->
                  let cmnd = IArray.of_list insts in
                  (pre_0 @ pre_1, call, [Block.mk ~lbl ~cmnd ~term]) ) ) ) )
  | Invoke -> (
      let llcallee = Llvm.operand instr (Llvm.num_operands instr - 1) in
      let lltyp = Llvm.type_of llcallee in
      let llcallee = norm_callee llcallee in
      let num_actuals = num_actuals instr lltyp llcallee in
      let fname = Llvm.value_name llcallee in
      let name_segs = String.split_on_char fname ~by:'.' in
      let return_blk = Llvm.get_normal_dest instr in
      let unwind_blk = Llvm.get_unwind_dest instr in
{'fraction_non_alphanumeric': 0.10456805645225231, 'fraction_numerical': 0.005346200459863853, 'mean_word_length': 2.074201747971726, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 715, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4516663', 'n_tokens_mistral': 31500, 'n_tokens_neox': 30337, 'n_words': 9077}