diff --git a/plugins/optimization/optimization_main.ml b/plugins/optimization/optimization_main.ml index 314534750..4b3f89c1d 100644 --- a/plugins/optimization/optimization_main.ml +++ b/plugins/optimization/optimization_main.ml @@ -1,20 +1,16 @@ -open Core_kernel[@@warning "-D"] +open Core_kernel [@@warning "-D"] open Bap.Std open Regular.Std open Format -include Self() - +include Self () module Digest = Data.Cache.Digest module O = Optimization_data type level = int - type cls = Phys | Virt | Flag let classify is_flag var = - if is_flag var then Flag - else if Var.is_physical var then Phys - else Virt + if is_flag var then Flag else if Var.is_physical var then Phys else Virt let is_optimization_allowed is_flag level var = match classify is_flag var with @@ -22,56 +18,58 @@ let is_optimization_allowed is_flag level var = | Flag -> level > 1 | Phys -> level > 2 -let def_use_collector = object - inherit [Var.Set.t * Var.Set.t] Term.visitor +let def_use_collector = + object + inherit [Var.Set.t * Var.Set.t] Term.visitor - method! enter_def t (defs,uses) = - Set.add defs (Def.lhs t), Set.union uses (Def.free_vars t) + method! enter_def t (defs, uses) = + (Set.add defs (Def.lhs t), Set.union uses (Def.free_vars t)) - method! enter_phi t (defs,uses) = - Set.add defs (Phi.lhs t), Set.union uses (Phi.free_vars t) + method! enter_phi t (defs, uses) = + (Set.add defs (Phi.lhs t), Set.union uses (Phi.free_vars t)) - method! enter_jmp t (defs,uses) = - defs, Set.union uses (Jmp.free_vars t) -end + method! enter_jmp t (defs, uses) = (defs, Set.union uses (Jmp.free_vars t)) + end let computed_def_use sub = - def_use_collector#visit_sub sub (Var.Set.empty,Var.Set.empty) + def_use_collector#visit_sub sub (Var.Set.empty, Var.Set.empty) let compute_dead can_touch protected sub = - let defs,uses = computed_def_use sub in + let defs, uses = computed_def_use sub in let dead = Set.diff defs uses in let live v = not (Set.mem dead v) in - Term.enum blk_t sub |> - Seq.fold ~init:Tid.Set.empty ~f:(fun dead blk -> - Term.enum ~rev:true def_t blk |> - Seq.fold ~init:(protected,dead) ~f:(fun (protected,dead) def -> + Term.enum blk_t sub + |> Seq.fold ~init:Tid.Set.empty ~f:(fun dead blk -> + Term.enum ~rev:true def_t blk + |> Seq.fold ~init:(protected, dead) ~f:(fun (protected, dead) def -> let v = Def.lhs def in - if not (can_touch v) || live v - then (protected,dead) - else if Set.mem protected (Var.base v) - then Set.remove protected (Var.base v), dead - else protected, Set.add dead (Term.tid def)) |> - snd) + if (not (can_touch v)) || live v then (protected, dead) + else if Set.mem protected (Var.base v) then + (Set.remove protected (Var.base v), dead) + else (protected, Set.add dead (Term.tid def))) + |> snd) let is_alive dead t = not (Set.mem dead (Term.tid t)) let live_phi dead blk = Term.filter phi_t ~f:(is_alive dead) blk let live_def can_touch dead blk = Term.filter def_t blk ~f:(fun d -> - not (can_touch (Def.lhs d)) || is_alive dead d) + (not (can_touch (Def.lhs d))) || is_alive dead d) let rec substitute vars exp = - let substituter = object - inherit Exp.mapper as super - method! map_let var ~exp ~body = - let exp = super#map_exp exp in - let body = substitute (Map.remove vars var) body in - Bil.let_ var exp body - method! map_var v = match Map.find vars v with - | None -> Bil.var v - | Some e -> e - end in + let substituter = + object + inherit Exp.mapper as super + + method! map_let var ~exp ~body = + let exp = super#map_exp exp in + let body = substitute (Map.remove vars var) body in + Bil.let_ var exp body + + method! map_var v = + match Map.find vars v with None -> Bil.var v | Some e -> e + end + in substituter#map_exp exp |> Exp.fold_consts let equal_kinds j j' = compare_jmp_kind (Jmp.kind j) (Jmp.kind j') = 0 @@ -79,48 +77,47 @@ let equal_kinds j j' = compare_jmp_kind (Jmp.kind j) (Jmp.kind j') = 0 let substitute sub vars = let def d = let rhs = substitute vars (Def.rhs d) in - if Exp.(Def.rhs d <> rhs) then - O.mark_updated (Def.with_rhs d rhs) - else d in + if Exp.(Def.rhs d <> rhs) then O.mark_updated (Def.with_rhs d rhs) else d + in let jmp j = let j' = Jmp.map_exp j ~f:(substitute vars) in - if Exp.(Jmp.cond j <> Jmp.cond j') || not (equal_kinds j j') - then O.mark_updated j' - else j in + if Exp.(Jmp.cond j <> Jmp.cond j') || not (equal_kinds j j') then + O.mark_updated j' + else j + in Term.map blk_t sub ~f:(Blk.map_elts ~def ~jmp) (* A simple constant propagation. Note, the input is required to be in SSA. *) let propagate_consts can_touch sub = - Seq.fold (Term.enum blk_t sub) ~init:Var.Map.empty - ~f:(fun vars b -> - Seq.fold (Term.enum def_t b) ~init:vars - ~f:(fun vars d -> - let v = Def.lhs d in - if can_touch v then - match Def.rhs d with - | Bil.Unknown _ | Bil.Int _ as exp -> - Map.set vars ~key:v ~data:exp - | _ -> vars - else vars)) |> - substitute sub + Seq.fold (Term.enum blk_t sub) ~init:Var.Map.empty ~f:(fun vars b -> + Seq.fold (Term.enum def_t b) ~init:vars ~f:(fun vars d -> + let v = Def.lhs d in + if can_touch v then + match Def.rhs d with + | (Bil.Unknown _ | Bil.Int _) as exp -> + Map.set vars ~key:v ~data:exp + | _ -> vars + else vars)) + |> substitute sub let clean can_touch dead sub = Term.map blk_t sub ~f:(fun b -> live_def can_touch dead b |> live_phi dead) let is_flag arch = - let module T = (val (target_of_arch arch)) in + let module T = (val target_of_arch arch) in T.CPU.is_flag let free_vars prog = report_progress ~note:"free-vars" (); - let (++) = Set.union in + let ( ++ ) = Set.union in let collect cls t ~f = - Seq.fold (Term.enum cls t) ~init:Var.Set.empty - ~f:(fun acc x -> acc ++ f x) in + Seq.fold (Term.enum cls t) ~init:Var.Set.empty ~f:(fun acc x -> acc ++ f x) + in let sub_free sub = Sub.free_vars sub |> Set.filter ~f:Var.is_physical in let sub_args sub = collect arg_t sub ~f:(fun arg -> - Set.add (Exp.free_vars (Arg.rhs arg)) (Arg.lhs arg)) in + Set.add (Exp.free_vars (Arg.rhs arg)) (Arg.lhs arg)) + in collect sub_t prog ~f:(fun sub -> sub_args sub ++ sub_free sub) let process_sub free can_touch sub = @@ -128,27 +125,32 @@ let process_sub free can_touch sub = let s = propagate_consts can_touch s in let dead' = compute_dead can_touch free s in let dead = Set.union dead dead' in - if Set.is_empty dead' then s, dead - else loop dead (clean can_touch dead' s) in + if Set.is_empty dead' then (s, dead) + else loop dead (clean can_touch dead' s) + in let sub', dead = loop Tid.Set.empty (Sub.ssa sub) in O.create dead sub' let digest_of_sub sub level = - let add addrs t = match Term.get_attr t address with + let add addrs t = + match Term.get_attr t address with | None -> addrs - | Some a -> Set.add addrs a in + | Some a -> Set.add addrs a + in let addrs = - Term.to_sequence blk_t sub |> - Seq.fold ~init:(Set.empty (module Addr)) - ~f:(fun addrs b -> - Seq.fold (Blk.elts b) ~init:(add addrs b) - ~f:(fun addrs -> function - | `Def d -> add addrs d - | `Jmp j -> add addrs j - | `Phi p -> add addrs p)) in + Term.to_sequence blk_t sub + |> Seq.fold + ~init:(Set.empty (module Addr)) + ~f:(fun addrs b -> + Seq.fold (Blk.elts b) ~init:(add addrs b) ~f:(fun addrs -> function + | `Def d -> add addrs d + | `Jmp j -> add addrs j + | `Phi p -> add addrs p)) + in let digest = Digest.create ~namespace:"optimization" in - let digest = Set.fold addrs ~init:digest ~f:(fun d a -> - Digest.add d "%a" Addr.pp a) in + let digest = + Set.fold addrs ~init:digest ~f:(fun d a -> Digest.add d "%a" Addr.pp a) + in let digest = Digest.add digest "%s" (Sub.name sub) in Digest.add digest "%d" level @@ -158,73 +160,64 @@ let run level proj = Project.map_program proj ~f:(fun prog -> let free = free_vars prog in Term.map sub_t prog ~f:(fun sub -> - let digest = digest_of_sub sub level in - match O.Cache.load digest with - | Some data -> O.apply sub data - | None -> - let data = process_sub free can_touch sub in - let sub = O.update sub data in - let data = O.find_unreachable sub data in - O.Cache.save digest data; - O.remove_dead_code sub data)) + let data = process_sub free can_touch sub in + let sub = O.update sub data in + let data = O.find_unreachable sub data in + O.remove_dead_code sub data)) let () = - Config.manpage [ - `S "SYNOPSIS"; - `Pre " - $(b,--)$(mname) -"; - `S "DESCRIPTION"; - - `P "An autorun pass that conservatively removes dead code. The - removed dead code is usually produced by a lifter, though it might - be possible that a binary indeed contains a dead code. The algorithm - doesn't remove variables that are stored in memory, only registers - are considered"; - - `S "ALGORITHM"; - - `P "Applies constant folding, dead code elimination, and constant - propagation in a loop until the fixed point is reached. The - algorithm is interprocedural, however it is not call graph - sensitive, as instead of considering the call graph we use an over - approximation that any function can call any other, thus any - variables that occurs free in any function is considered to be - non-constant. The algorithm is, however, flow sensitive on the - control flow graph level and uses the SSA form to encode data - facts. Since, it is not always safe to rely on the control flow - integrity and CFG precision, by default we optimize only flags and - virtual variables under a presumption that those two kind of data - points rarely used non-locally. - - See the $(b,--optimization-level) parameter for the list of - available optimization levels and their consequences."; - - `S "DEPENDENCIES"; - `P "$(b,bap-plugin-api)(1)"; - - `S "SEE ALSO"; - `P "$(b,bap-plugin-api)(1), $(b,bap-plugin-ssa)(1)"; - ]; + Config.manpage + [ + `S "SYNOPSIS"; + `Pre "\n $(b,--)$(mname)\n"; + `S "DESCRIPTION"; + `P + "An autorun pass that conservatively removes dead code. The\n\ + \ removed dead code is usually produced by a lifter, though it might\n\ + \ be possible that a binary indeed contains a dead code. The algorithm\n\ + \ doesn't remove variables that are stored in memory, only registers\n\ + \ are considered"; + `S "ALGORITHM"; + `P + "Applies constant folding, dead code elimination, and constant\n\ + \ propagation in a loop until the fixed point is reached. The\n\ + \ algorithm is interprocedural, however it is not call graph\n\ + \ sensitive, as instead of considering the call graph we use an over\n\ + \ approximation that any function can call any other, thus any\n\ + \ variables that occurs free in any function is considered to be\n\ + \ non-constant. The algorithm is, however, flow sensitive on the\n\ + \ control flow graph level and uses the SSA form to encode data\n\ + \ facts. Since, it is not always safe to rely on the control flow\n\ + \ integrity and CFG precision, by default we optimize only flags and\n\ + \ virtual variables under a presumption that those two kind of data\n\ + \ points rarely used non-locally.\n\n\ + \ See the $(b,--optimization-level) parameter for the list of\n\ + \ available optimization levels and their consequences."; + `S "DEPENDENCIES"; + `P "$(b,bap-plugin-api)(1)"; + `S "SEE ALSO"; + `P "$(b,bap-plugin-api)(1), $(b,bap-plugin-ssa)(1)"; + ]; let level = let doc = - "Specifies the optimization level. The higher the value the more - aggressive (and less safe) optimizations are applied. On level - 0 we touch nothing, only some constant folding may occur. On - level 1 we optimize only the synthetic code that was generated - by the lifter. Since such code can't leave a scope of instruction - it is not affected by the imprecision of a control flow graph. - On level 2, we also move and optimize processor flags. This - removes a significant amount of code and simplifies the program - and is a fair compromise between safety and performance. - (Since flags are rarely used non-locally). - Finally, on level 3 we extend our analysis to all variables." in - - Config.(param int ~default:0 ~doc "level") in - - Config.declare_extension - ~doc:"removes dead code and propagates constants" - ~provides:["pass"; "optimization"; "analysis"; "simplification"] - (fun {Config.get=(!)} -> - if !level > 0 - then Project.register_pass ~deps:["api"] ~autorun:true (run !level)) + "Specifies the optimization level. The higher the value the more\n\ + \ aggressive (and less safe) optimizations are applied. On level\n\ + \ 0 we touch nothing, only some constant folding may occur. On\n\ + \ level 1 we optimize only the synthetic code that was generated\n\ + \ by the lifter. Since such code can't leave a scope of instruction\n\ + \ it is not affected by the imprecision of a control flow graph.\n\ + \ On level 2, we also move and optimize processor flags. This\n\ + \ removes a significant amount of code and simplifies the program\n\ + \ and is a fair compromise between safety and performance.\n\ + \ (Since flags are rarely used non-locally).\n\ + \ Finally, on level 3 we extend our analysis to all variables." + in + + Config.(param int ~default:0 ~doc "level") + in + + Config.declare_extension ~doc:"removes dead code and propagates constants" + ~provides:[ "pass"; "optimization"; "analysis"; "simplification" ] + (fun { Config.get = ( ! ) } -> + if !level > 0 then + Project.register_pass ~deps:[ "api" ] ~autorun:true (run !level)) diff --git a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml index ee4b2e9bc..4fddc684d 100644 --- a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml +++ b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml @@ -256,6 +256,10 @@ let export = Primus.Lisp.Type.Spec.[ "get-current-program-counter", unit @-> int, "(get-current-program-counter) is an alias to (get-program-counter)"; + "get-instruction-length", unit @-> int, + "(get-instruction-length) returns the length of the current instruction \ + in bytes."; + "set-symbol-value", tuple [any; a] @-> a, "(set-symbol-value S X) sets the value of the symbol S to X. Returns X"; @@ -839,6 +843,12 @@ module Primitives(CT : Theory.Core)(T : Target) = struct | None -> !!(empty s) | Some addr -> forget@@const_int s addr + let get_instruction_length s lbl = + let open Bap.Std in + KB.collect Memory.slot lbl >>= function + | None -> !!(empty s) + | Some mem -> forget@@int s (Memory.length mem) + let require_symbol v k = match symbol v with | Some name -> k name @@ -1479,6 +1489,7 @@ module Primitives(CT : Theory.Core)(T : Target) = struct | "store-word",_-> data@@store_word t args | "get-program-counter",[] | "get-current-program-counter",[] -> pure@@get_pc s lbl + | "get-instruction-length",[] -> pure@@get_instruction_length s lbl | "set-symbol-value",[sym;x] -> data@@set_symbol t sym x | "symbol-concat",syms -> pure@@symbol_concat s syms | "symbol",[x] -> pure@@mksymbol s x diff --git a/plugins/primus_lisp/site-lisp/llvm-x86-64-floats.lisp b/plugins/primus_lisp/site-lisp/llvm-x86-64-floats.lisp index e8980b26d..a75b833c5 100644 --- a/plugins/primus_lisp/site-lisp/llvm-x86-64-floats.lisp +++ b/plugins/primus_lisp/site-lisp/llvm-x86-64-floats.lisp @@ -24,7 +24,7 @@ (defun reg-val (reg) (case (reg-name reg) - 'RIP (+ (get-current-program-counter) 8) + 'RIP (+ (get-current-program-counter) (get-instruction-length)) 'RSP RSP 'RBP RBP (error "unknown register"))) diff --git a/plugins/x86/semantics/x86-64.lisp b/plugins/x86/semantics/x86-64.lisp index d2551ccda..045c5fc5b 100644 --- a/plugins/x86/semantics/x86-64.lisp +++ b/plugins/x86/semantics/x86-64.lisp @@ -24,7 +24,7 @@ (defun reg# (reg) (if (is-rip reg) - (+ (get-program-counter) 8) + (+ (get-program-counter) (get-instruction-length)) reg)) (defun load-mem (reg off) @@ -478,4 +478,4 @@ (set rd (opo (opi rn rm)))) (defmacro bitwise-rrm (set opo opi rd rn ptr off) - (set rd (opo (opi rn (load-bits (word-width (unquote rn)) (+ ptr off)))))) + (set rd (opo (opi rn (load-bits (word-width (unquote rn)) (+ (reg# ptr) off)))))) diff --git a/plugins/x86/x86_lifter.ml b/plugins/x86/x86_lifter.ml index 5db51f02d..b4b6459ac 100644 --- a/plugins/x86/x86_lifter.ml +++ b/plugins/x86/x86_lifter.ml @@ -1,16 +1,15 @@ (** Native lifter of x86 instructions to the BAP IL *) -open Core_kernel[@@warning "-D"] +open Core_kernel [@@warning "-D"] open Bap.Std open Format open Bil.Types open X86_types open X86_utils open X86_env -include Self() +include Self () module ToIR = struct - let cf_e = Bil.var cf let pf_e = Bil.var pf let af_e = Bil.var af @@ -19,44 +18,40 @@ module ToIR = struct let of_e = Bil.var oF let df_e = Bil.var df - let size_of_typ s = Size.of_int_exn !!s (** doubts here *) - + (** doubts here *) + let size_of_typ s = Size.of_int_exn !!s let undefine = List.map ~f:(fun r -> Bil.(r := unknown "#undefined" (Var.typ r))) - (* stmt helpers *) let store_s mode s t a e = - let mem = match mode with - | X86 -> R32.mem - | X8664 -> R64.mem in + let mem = match mode with X86 -> R32.mem | X8664 -> R64.mem in let sz = size_of_typ t in match s with | None -> Bil.Move (mem, Bil.(Store (Var mem, a, e, LittleEndian, sz))) - | Some v -> Bil.Move (mem, Bil.(Store (Var mem, Var v + a, e, - LittleEndian, sz))) + | Some v -> + Bil.Move (mem, Bil.(Store (Var mem, Var v + a, e, LittleEndian, sz))) (* copypasted from op2e_s below, but keeps the opcode width *) let op2e_s_keep_width mode ss has_rex t operand = - let (=) = Type.equal in + let ( = ) = Type.equal in match operand with | Ovec r when t = reg256_t -> (bits2ymme mode r, t) | Ovec r when t = reg128_t -> (bits2ymm128e mode r, t) | Ovec r when t = reg64_t -> (bits2ymm64e mode r, t) | Ovec r when t = reg32_t -> (bits2ymm32e mode r, t) | Ovec _ -> - let i = match t with - | Type.Imm n -> ": "^(string_of_int n) - | _ -> "" in - disfailwith mode ("invalid SIMD register size for op2e"^i) + let i = match t with Type.Imm n -> ": " ^ string_of_int n | _ -> "" in + disfailwith mode ("invalid SIMD register size for op2e" ^ i) | Oreg r when t = reg64_t -> (bits2reg64e mode r, t) | Oreg r when t = reg32_t -> (bits2reg32e mode r, t) | Oreg r when t = reg16_t -> (bits2reg16e mode r, t) | Oreg r when t = reg8_t -> (bits2reg8e mode ~has_rex r, t) | Oreg _ -> unimplemented mode "unknown register" - | Oseg r when t = reg64_t -> Bil.(Cast (UNSIGNED, !!reg64_t, bits2segrege r), t) + | Oseg r when t = reg64_t -> + Bil.(Cast (UNSIGNED, !!reg64_t, bits2segrege r), t) (* There is no 32-bit extension of segment selectors; this is not a bug *) | Oseg r when t = reg16_t -> (bits2segrege r, t) | Oseg _ -> (disfailwith mode "Segment register when t is not r16", t) @@ -64,23 +59,22 @@ module ToIR = struct | Oimm i -> Bil.(Int (resize_word i !!t), t) let op2e_s mode ss has_rex t operand = - let (=) = Type.equal in + let ( = ) = Type.equal in match operand with | Ovec r when t = reg256_t -> bits2ymme mode r | Ovec r when t = reg128_t -> bits2ymm128e mode r | Ovec r when t = reg64_t -> bits2ymm64e mode r | Ovec r when t = reg32_t -> bits2ymm32e mode r | Ovec _ -> - let i = match t with - | Type.Imm n -> ": "^(string_of_int n) - | _ -> "" in - disfailwith mode ("invalid SIMD register size for op2e"^i) + let i = match t with Type.Imm n -> ": " ^ string_of_int n | _ -> "" in + disfailwith mode ("invalid SIMD register size for op2e" ^ i) | Oreg r when t = reg64_t -> bits2reg64e mode r | Oreg r when t = reg32_t -> bits2reg32e mode r | Oreg r when t = reg16_t -> bits2reg16e mode r | Oreg r when t = reg8_t -> bits2reg8e mode ~has_rex r | Oreg _ -> unimplemented mode "unknown register" - | Oseg r when t = reg64_t -> Bil.(Cast (UNSIGNED, !!reg64_t, bits2segrege r)) + | Oseg r when t = reg64_t -> + Bil.(Cast (UNSIGNED, !!reg64_t, bits2segrege r)) (* There is no 32-bit extension of segment selectors; this is not a bug *) | Oseg r when t = reg16_t -> bits2segrege r | Oseg _ -> disfailwith mode "Segment register when t is not r16" @@ -89,66 +83,71 @@ module ToIR = struct let assn_s mode s has_rex has_vex t v e = (* Assign to some bits of v, starting at bit off, while preserving the other bits *) - let sub_assn ?(off=0) t v e = + let sub_assn ?(off = 0) t v e = let concat_exps = ref [] in let bits = !!(Var.typ v) in let assnbits = !!t in (* Add the upper preserved bits, if any *) - let ubh = (bits-1) and ubl = (assnbits+off) in - if ubh > ubl then concat_exps := (Bil.(Extract (ubh, ubl, Var v)))::!concat_exps; + let ubh = bits - 1 and ubl = assnbits + off in + if ubh > ubl then + concat_exps := Bil.(Extract (ubh, ubl, Var v)) :: !concat_exps; (* Add e *) - concat_exps := e::!concat_exps; + concat_exps := e :: !concat_exps; (* Add the lower preserved bits, if any *) - let lbh = (off-1) and lbl = 0 in + let lbh = off - 1 and lbl = 0 in if lbh > lbl then - concat_exps := (Bil.(Extract (lbh, lbl, Var v)))::!concat_exps; + concat_exps := Bil.(Extract (lbh, lbl, Var v)) :: !concat_exps; - let final_e = List.reduce_exn ~f:(fun big_e e -> Bil.Concat (e, big_e)) !concat_exps in + let final_e = + List.reduce_exn ~f:(fun big_e e -> Bil.Concat (e, big_e)) !concat_exps + in Bil.Move (v, final_e) in let is8664 = [%compare.equal: mode] mode X8664 in - match v, t with + match (v, t) with (* Zero-extend 128-bit assignments to 256-bit ymms. *) - | Ovec r, Type.Imm (128|64|32) when has_vex -> - let v = bits2ymm mode r in - sub_assn reg256_t v Bil.(Cast (UNSIGNED, !!reg256_t, e)) - | Ovec r, Type.Imm (256|128|64|32) -> - let v = bits2ymm mode r in - sub_assn t v e + | Ovec r, Type.Imm (128 | 64 | 32) when has_vex -> + let v = bits2ymm mode r in + sub_assn reg256_t v Bil.(Cast (UNSIGNED, !!reg256_t, e)) + | Ovec r, Type.Imm (256 | 128 | 64 | 32) -> + let v = bits2ymm mode r in + sub_assn t v e | Ovec _, _ -> disfailwith mode "invalid SIMD register size for assignment" (* Zero-extend 32-bit assignments to 64-bit registers. *) | Oreg r, Type.Imm 32 when is8664 -> - let v = bits2genreg mode r in - sub_assn reg64_t v Bil.(Cast (UNSIGNED, !!reg64_t, e)) - | Oreg r, Type.Imm (64|32|16) -> - let v = bits2genreg mode r in - sub_assn t v e - | Oreg r, Type.Imm 8 when r < 4 || ([%compare.equal: mode] mode X8664 && has_rex) -> - let v = bits2genreg mode r in - sub_assn t v e + let v = bits2genreg mode r in + sub_assn reg64_t v Bil.(Cast (UNSIGNED, !!reg64_t, e)) + | Oreg r, Type.Imm (64 | 32 | 16) -> + let v = bits2genreg mode r in + sub_assn t v e + | Oreg r, Type.Imm 8 + when r < 4 || ([%compare.equal: mode] mode X8664 && has_rex) -> + let v = bits2genreg mode r in + sub_assn t v e | Oreg r, Type.Imm 8 -> - let v = bits2genreg mode (r land 3) in - sub_assn ~off:8 t v e + let v = bits2genreg mode (r land 3) in + sub_assn ~off:8 t v e | Oreg _, _ -> unimplemented mode "assignment to sub registers" | Oseg r, _ when Type.equal t reg16_t -> - let v = bits2segreg r in - Bil.Move (v, e) - | Oseg _, _ -> disfailwith mode "Can't assign to non 16 bit segment register" + let v = bits2segreg r in + Bil.Move (v, e) + | Oseg _, _ -> + disfailwith mode "Can't assign to non 16 bit segment register" | Oaddr a, _ -> store_s mode s t a e - | Oimm _, _ -> disfailwith mode "disasm x86: Can't assign to an immediate value" - + | Oimm _, _ -> + disfailwith mode "disasm x86: Can't assign to an immediate value" (* Double width operands, as used by multiplication and division *) let op_dbl t = let open Type in match t with - | Imm 8 -> [reg16_t, o_rax] - | Imm 16 -> [reg16_t, o_rdx; reg16_t, o_rax] - | Imm 32 -> [reg32_t, o_rdx; reg32_t, o_rax] - | Imm 64 -> [reg64_t, o_rdx; reg64_t, o_rax] + | Imm 8 -> [ (reg16_t, o_rax) ] + | Imm 16 -> [ (reg16_t, o_rdx); (reg16_t, o_rax) ] + | Imm 32 -> [ (reg32_t, o_rdx); (reg32_t, o_rax) ] + | Imm 64 -> [ (reg64_t, o_rdx); (reg64_t, o_rax) ] | _ -> disfailwith X86 "op_dbl only defined for Reg 8, 16, 32, and 64" (* Return an expression for a double-width operand, as used by the div @@ -156,30 +155,36 @@ module ToIR = struct let op2e_dbl_s mode ss has_rex t = let cf (ct, o) = op2e_s mode ss has_rex ct o in let ol = List.map ~f:cf (op_dbl t) in - List.reduce_exn - ~f:(fun bige little -> Bil.(bige ^ little)) - ol + List.reduce_exn ~f:(fun bige little -> Bil.(bige ^ little)) ol (* Double width assignments, as used by multiplication *) let assn_dbl_s mode s has_rex has_vex t e = match op_dbl t with - | (t,o) :: [] -> [assn_s mode s has_rex has_vex t o e], op2e_s mode s has_rex t o + | (t, o) :: [] -> + ([ assn_s mode s has_rex has_vex t o e ], op2e_s mode s has_rex t o) | l -> - let tmp = tmp (Type.Imm (!!t * 2)) in - let f (stmts, off) (ct, o) = - let newoff = off + !!ct in - assn_s mode s has_rex has_vex ct o (Bil.Extract (newoff-1, off, Bil.Var tmp))::stmts, newoff - in - List.rev (fst (List.fold_left ~f:f ~init:([Bil.Move (tmp, e)], 0) (List.rev l))), Bil.Var tmp + let tmp = tmp (Type.Imm (!!t * 2)) in + let f (stmts, off) (ct, o) = + let newoff = off + !!ct in + ( assn_s mode s has_rex has_vex ct o + (Bil.Extract (newoff - 1, off, Bil.Var tmp)) + :: stmts, + newoff ) + in + ( List.rev + (fst + (List.fold_left ~f ~init:([ Bil.Move (tmp, e) ], 0) (List.rev l))), + Bil.Var tmp ) (* A function for computing the target of jumps. *) let compute_jump_target mode s has_rex = let t = type_of_mode mode in function | Jabs o -> op2e_s mode s has_rex t o - | Jrel (na,offset) -> - (*let i,t = Arithmetic.binop PLUS (na,t) (offset,t) in*) - Bil.((Int na) + (Int offset)) + | Jrel (na, offset) -> + (*let i,t = Arithmetic.binop PLUS (na,t) (offset,t) in*) + Bil.(Int na + Int offset) + let jump_target = compute_jump_target let string_incr mode t v = @@ -192,25 +197,26 @@ module ToIR = struct let rep_wrap ?check_zf ~mode ~addr:_ ~next:_ stmts = let extend = big_int_of_mode mode in let zero = extend Word.b0 and one = extend Word.b1 in - let rcx = match mode with - | X86 -> R32.rcx - | X8664 -> R64.rcx in + let rcx = match mode with X86 -> R32.rcx | X8664 -> R64.rcx in let flag = tmp bool_t in let cond = Bil.((var rcx <> int zero) land var flag) in let head = Bil.(flag := int Word.b1) in let tail = - Bil.(rcx := var rcx - int one) :: match check_zf with + Bil.(rcx := var rcx - int one) + :: + (match check_zf with | None -> [] - | Some x when x = repz -> Bil.[flag := zf_e] - | Some x when x = repnz -> Bil.[flag := lnot zf_e] - | _ -> failwith "invalid value for ?check_zf" in - Bil.[head; while_ cond (stmts @ tail)] + | Some x when x = repz -> Bil.[ flag := zf_e ] + | Some x when x = repnz -> Bil.[ flag := lnot zf_e ] + | _ -> failwith "invalid value for ?check_zf") + in + Bil.[ head; while_ cond (stmts @ tail) ] let compute_sf result = Bil.(Cast (HIGH, !!bool_t, result)) let compute_zf t result = let bi0 = BV.of_int ~width:t 0 in - Bil.((Int bi0) = result) + Bil.(Int bi0 = result) let compute_pf t r = let acc = tmp t in @@ -219,8 +225,17 @@ module ToIR = struct (* extra parens do not change semantics but do make it pretty print nicer *) let open Bil in - exp_not (Cast (LOW, !!bool_t, - ((Let(acc, (r lsr (int_exp 4 t')) lxor r, Let(acc, (var_acc lsr (int_exp 2 t')) lxor var_acc, (var_acc lsr (int_exp 1 t')) lxor var_acc)))))) + exp_not + (Cast + ( LOW, + !!bool_t, + Let + ( acc, + (r lsr int_exp 4 t') lxor r, + Let + ( acc, + (var_acc lsr int_exp 2 t') lxor var_acc, + (var_acc lsr int_exp 1 t') lxor var_acc ) ) )) let set_sf r = Bil.Move (sf, compute_sf r) let set_zf t r = Bil.Move (zf, compute_zf t r) @@ -228,9 +243,7 @@ module ToIR = struct let set_pszf t r = let t' = !!t in - [set_pf t r; - set_sf r; - set_zf t' r] + [ set_pf t r; set_sf r; set_zf t' r ] (* Adjust flag @@ -246,39 +259,38 @@ module ToIR = struct let set_apszf t s1 s2 r = let bit4 = int_exp (1 lsl 4) t in let t = Type.Imm t in - Bil.Move (af, Bil.(bit4 = (bit4 land ((r lxor s1) lxor s2)))) - ::set_pszf t r + Bil.Move (af, Bil.(bit4 = bit4 land (r lxor s1 lxor s2))) :: set_pszf t r (* Helper functions to set flags for adding *) let set_aopszf_add t s1 s2 r = (* Move (oF, Bop.(Cast (CAST_HIGH, r1, (s1 = s2) land (s1 lxor r)))) *) let s1_high = Bil.(Cast (HIGH, !!bool_t, s1)) in let s2_high = Bil.(Cast (HIGH, !!bool_t, s2)) in - let r_high = Bil.(Cast (HIGH, !!bool_t, r)) in + let r_high = Bil.(Cast (HIGH, !!bool_t, r)) in Bil.Move (oF, Bil.((s1_high = s2_high) land (s1_high lxor r_high))) - ::set_apszf t s1 s2 r + :: set_apszf t s1 s2 r let set_flags_add t s1 s2 r = - Bil.Move (cf, Bil.(r < s1)) - ::set_aopszf_add t s1 s2 r + Bil.Move (cf, Bil.(r < s1)) :: set_aopszf_add t s1 s2 r (* Helper functions to set flags for subtracting *) let set_apszf_sub t s1 s2 r = set_apszf t s1 s2 r let set_aopszf_sub t s1 s2 r = - Bil.Move (oF, Bil.(Cast (HIGH, !!bool_t, (s1 lxor s2) land (s1 lxor r)))) - ::set_apszf_sub t s1 s2 r + Bil.Move (oF, Bil.(Cast (HIGH, !!bool_t, s1 lxor s2 land (s1 lxor r)))) + :: set_apszf_sub t s1 s2 r let set_flags_sub t s1 s2 r = - Bil.Move (cf, Bil.(s2 > s1)) - ::set_aopszf_sub t s1 s2 r + Bil.Move (cf, Bil.(s2 > s1)) :: set_aopszf_sub t s1 s2 r - let popcount x ~one ~two ~four ~sh ~m1 ~m2 ~m4 ~h01 = Bil.[ - x := var x - ((var x lsr int one) land int m1); - x := (var x land int m2) + ((var x lsr int two) land int m2); - x := (var x + (var x lsr int four)) land int m4; - x := (var x * int h01) lsr int sh; - ] + let popcount x ~one ~two ~four ~sh ~m1 ~m2 ~m4 ~h01 = + Bil. + [ + x := var x - ((var x lsr int one) land int m1); + x := (var x land int m2) + ((var x lsr int two) land int m2); + x := (var x + (var x lsr int four)) land int m4; + x := (var x * int h01) lsr int sh; + ] let popcnt16 x = let one = Word.one 16 in @@ -313,59 +325,68 @@ module ToIR = struct let h01 = Word.of_int64 ~width:64 0x0101010101010101L in popcount x ~one ~two ~four ~sh ~m1 ~m2 ~m4 ~h01 - let clz16 x = Bil.[ - x := var x lor (var x lsr int Word.(one 16)); - x := var x lor (var x lsr int Word.(of_int 2 ~width:16)); - x := var x lor (var x lsr int Word.(of_int 4 ~width:16)); - x := var x lor (var x lsr int Word.(of_int 8 ~width:16)); - x := lnot (var x); - ] @ popcnt16 x - - let clz32 x = Bil.[ - x := var x lor (var x lsr int Word.(one 32)); - x := var x lor (var x lsr int Word.(of_int 2 ~width:32)); - x := var x lor (var x lsr int Word.(of_int 4 ~width:32)); - x := var x lor (var x lsr int Word.(of_int 8 ~width:32)); - x := var x lor (var x lsr int Word.(of_int 16 ~width:32)); - x := lnot (var x); - ] @ popcnt32 x - - let clz64 x = Bil.[ - x := var x lor (var x lsr int Word.(one 64)); - x := var x lor (var x lsr int Word.(of_int 2 ~width:64)); - x := var x lor (var x lsr int Word.(of_int 4 ~width:64)); - x := var x lor (var x lsr int Word.(of_int 8 ~width:64)); - x := var x lor (var x lsr int Word.(of_int 16 ~width:64)); - x := var x lor (var x lsr int Word.(of_int 32 ~width:64)); - x := lnot (var x); - ] @ popcnt64 x - - let ctz16 x = Bil.( - x := (var x land unop NEG (var x)) - int Word.(one 16) - ) :: popcnt16 x - - let ctz32 x = Bil.( - x := (var x land unop NEG (var x)) - int Word.(one 32) - ) :: popcnt32 x - - let ctz64 x = Bil.( - x := (var x land unop NEG (var x)) - int Word.(one 64) - ) :: popcnt64 x + let clz16 x = + Bil. + [ + x := var x lor (var x lsr int Word.(one 16)); + x := var x lor (var x lsr int Word.(of_int 2 ~width:16)); + x := var x lor (var x lsr int Word.(of_int 4 ~width:16)); + x := var x lor (var x lsr int Word.(of_int 8 ~width:16)); + x := lnot (var x); + ] + @ popcnt16 x + + let clz32 x = + Bil. + [ + x := var x lor (var x lsr int Word.(one 32)); + x := var x lor (var x lsr int Word.(of_int 2 ~width:32)); + x := var x lor (var x lsr int Word.(of_int 4 ~width:32)); + x := var x lor (var x lsr int Word.(of_int 8 ~width:32)); + x := var x lor (var x lsr int Word.(of_int 16 ~width:32)); + x := lnot (var x); + ] + @ popcnt32 x + + let clz64 x = + Bil. + [ + x := var x lor (var x lsr int Word.(one 64)); + x := var x lor (var x lsr int Word.(of_int 2 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 4 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 8 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 16 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 32 ~width:64)); + x := lnot (var x); + ] + @ popcnt64 x + + let ctz16 x = + Bil.(x := (var x land unop NEG (var x)) - int Word.(one 16)) :: popcnt16 x + + let ctz32 x = + Bil.(x := (var x land unop NEG (var x)) - int Word.(one 32)) :: popcnt32 x + + let ctz64 x = + Bil.(x := (var x land unop NEG (var x)) - int Word.(one 64)) :: popcnt64 x let bitscan_flags is_zero_count = - let l = Bil.[ - oF := unknown "bits" bool_t; - sf := unknown "bits" bool_t; - af := unknown "bits" bool_t; - pf := unknown "bits" bool_t; - ] in - if is_zero_count then l - else Bil.(cf := unknown "bits" bool_t) :: l + let l = + Bil. + [ + oF := unknown "bits" bool_t; + sf := unknown "bits" bool_t; + af := unknown "bits" bool_t; + pf := unknown "bits" bool_t; + ] + in + if is_zero_count then l else Bil.(cf := unknown "bits" bool_t) :: l let rec to_ir mode addr next ss pref has_rex has_vex = - let module R = (val (vars_of_mode mode)) in + let module R = (val vars_of_mode mode) in let open R in - let load = load_s mode ss in (* Need to change this if we want seg_ds <> None *) + let load = load_s mode ss in + (* Need to change this if we want seg_ds <> None *) let op2e = op2e_s mode ss has_rex in let op2e_keep_width = op2e_s_keep_width mode ss has_rex in let op2e_dbl = op2e_dbl_s mode ss has_rex in @@ -383,911 +404,1097 @@ module ToIR = struct let ah_e = ah_e mode in let disfailwith = disfailwith mode in let unimplemented = unimplemented mode in - let is_small_imm op t = match op with + let is_small_imm op t = + match op with | Oimm imm -> Word.bitwidth imm < bitwidth_of_type t - | _ -> false in + | _ -> false + in let sign_extend_imm op t = - let op_typ = match op with + let op_typ = + match op with | Oimm imm -> Type.imm (Word.bitwidth imm) - | _ -> disfailwith "imm operand expected" in - Bil.(cast signed (bitwidth_of_type t) (op2e op_typ op)) in - let is_repz = function - | [x] -> x = repz - | _ -> false in - let is_repnz = function - | [x] -> x = repnz - | _ -> false in + | _ -> disfailwith "imm operand expected" + in + Bil.(cast signed (bitwidth_of_type t) (op2e op_typ op)) + in + let is_repz = function [ x ] -> x = repz | _ -> false in + let is_repnz = function [ x ] -> x = repnz | _ -> false in function | Nop -> [] - | Bswap(t, op) -> - let e = match t with - | Type.Imm 32 | Type.Imm 64 -> let (op', t') = op2e_keep_width t op in - reverse_bytes op' t' - | _ -> disfailwith "bswap: Expected 32 or 64 bit type" - in - [assn t op e] - | Retn (op, far_ret) when List.is_empty pref || is_repz pref || is_repnz pref -> - let temp = tmp mt in - let load_stmt = if far_ret - then (* TODO Mess with segment selectors here *) - unimplemented "long retn not supported" - else Bil.Move (temp, load_s mode seg_ss (size_of_typ mt) rsp_e) - in - let rsp_stmts = - Bil.Move (rsp, Bil.(rsp_e + (Int (mi (bytes_of_width mt))))):: - (match op with - | None -> [] - | Some(t, src) -> - [Bil.Move (rsp, Bil.(rsp_e + (op2e t src)))] - ) in - load_stmt:: - rsp_stmts@ - [Bil.Jmp (Bil.Var temp)] - | Mov(t, dst, src, condition) -> - let c_src = (match condition with + | Bswap (t, op) -> + let e = + match t with + | Type.Imm 32 | Type.Imm 64 -> + let op', t' = op2e_keep_width t op in + reverse_bytes op' t' + | _ -> disfailwith "bswap: Expected 32 or 64 bit type" + in + [ assn t op e ] + | Retn (op, far_ret) + when List.is_empty pref || is_repz pref || is_repnz pref -> + let temp = tmp mt in + let load_stmt = + if far_ret then (* TODO Mess with segment selectors here *) + unimplemented "long retn not supported" + else Bil.Move (temp, load_s mode seg_ss (size_of_typ mt) rsp_e) + in + let rsp_stmts = + Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width mt)))) + :: + (match op with + | None -> [] + | Some (t, src) -> [ Bil.Move (rsp, Bil.(rsp_e + op2e t src)) ]) + in + (load_stmt :: rsp_stmts) @ [ Bil.Jmp (Bil.Var temp) ] + | Mov (t, dst, src, condition) -> + let c_src = + match condition with | None -> op2e t src - | Some c -> Bil.Ite (c, op2e t src, op2e t dst)) - in - (* Find base by looking at LDT or GDT *) - let base_e e = - (* 0 = GDT, 1 = LDT *) - let ti = Bil.Extract (3, 3, e) in - let base = Bil.Ite (ti, Bil.var ldt, Bil.var gdt) in - (* Extract index into table *) - let entry_size, entry_shift = match mode with - | X86 -> reg64_t, 6 (* "1<<6 = 64" *) - | X8664 -> reg128_t, 7 (* "1<<7 = 128" *) - in - let index = Bil.(Cast (UNSIGNED, !!mt, (Extract (15, 4, e)) lsl (Int (mi entry_shift)))) in - (* Load the table entry *) - let table_entry = load_s mode None (size_of_typ entry_size) (Bil.(base + index)) in - (* Extract the base *) - concat_explist - ((match mode with - | X86 -> [] - | X8664 -> (Bil.Extract (95, 64, table_entry)) :: []) - @ (Bil.Extract (63, 56, table_entry)) - :: (Bil.Extract (39, 32, table_entry)) - :: (Bil.Extract (31, 16, table_entry)) - :: []) - in - let bs = - let dst_e = op2e t dst in - if [%compare.equal: operand] dst o_fs && !compute_segment_bases - then [Bil.Move (fs_base, base_e dst_e)] - else if [%compare.equal: operand] dst o_gs && !compute_segment_bases - then [Bil.Move (gs_base, base_e dst_e)] - else [] - in - assn t dst c_src :: bs - | Movs(Type.Imm _bits as t) -> - let stmts = - store_s mode seg_es t rdi_e (load_s mode seg_es (size_of_typ t) rsi_e) - :: string_incr mode t rsi - :: string_incr mode t rdi - :: [] - in - if List.is_empty pref then - stmts - else if ints_mem pref repz || ints_mem pref repnz then - (* movs has only rep instruction others just considered to be rep *) - rep_wrap ~mode ~addr ~next stmts - else - unimplemented "unsupported prefix for movs" - | Movzx(t, dst, ts, src) -> - [assn t dst Bil.(Cast (UNSIGNED, !!t, op2e ts src))] - | Movsx(t, dst, ts, src) -> - [assn t dst Bil.(Cast (SIGNED, !!t, op2e ts src))] - | Movdq(ts, s, td, d, align) -> - let (s, al) = match s with - | Ovec _ | Oreg _-> op2e ts s, [] - | Oaddr a -> op2e ts s, [a] - | Oimm _ | Oseg _ -> disfailwith "invalid source operand for movdq" - in - let (d, al) = match d with - (* Behavior is to clear the xmm bits *) - | Ovec _ -> assn td d Bil.(Cast (UNSIGNED, !!td, s)), al - | Oreg _ -> assn td d s, al - | Oaddr a -> assn td d s, a::al - | Oimm _ | Oseg _ -> disfailwith "invalid dest operand for movdq" - in - (* sources tell me that movdqa raises a general protection exception - * if its operands aren't aligned on a 16-byte boundary *) - let im i = Bil.Int (int_of_mode mode i) in - let al = - if align then - List.map ~f:(fun a -> Bil.If (Bil.((a land im 15) = im 0), [], [Cpu_exceptions.general_protection])) al - else [] - in - d::al - | Movoffset((tdst, dst), offsets) -> - (* If a vex prefix is present, then extra space is filled with 0. + | Some c -> Bil.Ite (c, op2e t src, op2e t dst) + in + (* Find base by looking at LDT or GDT *) + let base_e e = + (* 0 = GDT, 1 = LDT *) + let ti = Bil.Extract (3, 3, e) in + let base = Bil.Ite (ti, Bil.var ldt, Bil.var gdt) in + (* Extract index into table *) + let entry_size, entry_shift = + match mode with + | X86 -> (reg64_t, 6 (* "1<<6 = 64" *)) + | X8664 -> (reg128_t, 7 (* "1<<7 = 128" *)) + in + let index = + Bil.( + Cast (UNSIGNED, !!mt, Extract (15, 4, e) lsl Int (mi entry_shift))) + in + (* Load the table entry *) + let table_entry = + load_s mode None (size_of_typ entry_size) Bil.(base + index) + in + (* Extract the base *) + concat_explist + ((match mode with + | X86 -> [] + | X8664 -> Bil.Extract (95, 64, table_entry) :: []) + @ [ + Bil.Extract (63, 56, table_entry); + Bil.Extract (39, 32, table_entry); + Bil.Extract (31, 16, table_entry); + ]) + in + let bs = + let dst_e = op2e t dst in + if [%compare.equal: operand] dst o_fs && !compute_segment_bases then + [ Bil.Move (fs_base, base_e dst_e) ] + else if [%compare.equal: operand] dst o_gs && !compute_segment_bases + then [ Bil.Move (gs_base, base_e dst_e) ] + else [] + in + assn t dst c_src :: bs + | Movs (Type.Imm _bits as t) -> + let stmts = + [ + store_s mode seg_es t rdi_e + (load_s mode seg_es (size_of_typ t) rsi_e); + string_incr mode t rsi; + string_incr mode t rdi; + ] + in + if List.is_empty pref then stmts + else if ints_mem pref repz || ints_mem pref repnz then + (* movs has only rep instruction others just considered to be rep *) + rep_wrap ~mode ~addr ~next stmts + else unimplemented "unsupported prefix for movs" + | Movzx (t, dst, ts, src) -> + [ assn t dst Bil.(Cast (UNSIGNED, !!t, op2e ts src)) ] + | Movsx (t, dst, ts, src) -> + [ assn t dst Bil.(Cast (SIGNED, !!t, op2e ts src)) ] + | Movdq (ts, s, td, d, align) -> + let s, al = + match s with + | Ovec _ | Oreg _ -> (op2e ts s, []) + | Oaddr a -> (op2e ts s, [ a ]) + | Oimm _ | Oseg _ -> disfailwith "invalid source operand for movdq" + in + let d, al = + match d with + (* Behavior is to clear the xmm bits *) + | Ovec _ -> (assn td d Bil.(Cast (UNSIGNED, !!td, s)), al) + | Oreg _ -> (assn td d s, al) + | Oaddr a -> (assn td d s, a :: al) + | Oimm _ | Oseg _ -> disfailwith "invalid dest operand for movdq" + in + (* sources tell me that movdqa raises a general protection exception + * if its operands aren't aligned on a 16-byte boundary *) + let im i = Bil.Int (int_of_mode mode i) in + let al = + if align then + List.map + ~f:(fun a -> + Bil.If + ( Bil.(a land im 15 = im 0), + [], + [ Cpu_exceptions.general_protection ] )) + al + else [] + in + d :: al + | Movoffset ((tdst, dst), offsets) -> + (* If a vex prefix is present, then extra space is filled with 0. Otherwise, the bits are preserved. *) - let padding hi lo = - if hi < lo then [] - else if has_vex then [int_exp 0 (hi - lo + 1)] - else [Bil.Extract (hi, lo, op2e tdst dst)] - in - let offsets = List.sort ~compare:(fun {offdstoffset=o1; _} {offdstoffset=o2; _} -> Int.compare o1 o2) offsets in - let add_exp (elist,nextbit) {offlen; offtyp; offop; offsrcoffset; offdstoffset} = - Bil.Extract ((!!offlen + offsrcoffset - 1), offsrcoffset, (op2e offtyp offop)) - :: padding (offdstoffset - 1) nextbit - @ elist, offdstoffset + !!offlen - in - let elist, nextbit = List.fold_left ~f:add_exp ~init:([],0) offsets in - let elist = padding (!!tdst - 1) nextbit @ elist in - [assn tdst dst (concat_explist elist)] - | Punpck(t, et, o, d, s, vs) -> - let nelem = match t, et with - | Type.Imm n, Type.Imm n' -> n / n' - | _ -> disfailwith "invalid" - in - assert (nelem mod 2 = 0); - let nelem_per_src = nelem / 2 in - let halft = Type.Imm (!!t / 2) in - let castf = match o with - | High -> fun e -> Bil.(Cast (HIGH, !!halft, e)) - | Low -> fun e -> Bil.(Cast (LOW, !!halft, e)) - in - let se, de = castf (op2e t s), castf (op2e t d) in - let st, dt = tmp halft, tmp halft in - let et' = !!et in - let mape i = - [extract_element et' (Bil.Var st) i; extract_element et' (Bil.Var dt) i] - in - let e = concat_explist (List.concat (List.map ~f:mape (List.range ~stride:(-1) ~stop:`inclusive (nelem_per_src-1) 0))) in - let dest = match vs with - | None -> d - | Some vdst -> vdst - in - [Bil.Move (st, se); - Bil.Move (dt, de); - assn t dest e] - | Ppackedbinop(t, et, fbop, _, d, s, vs) -> - let t_width = bitwidth_of_type t in - let e_width = bitwidth_of_type et in - let nops = t_width / e_width in - let byte = 8 in - let tmp_dst = tmp t in - let vdst = Option.value ~default:d vs in - let iv = tmp (Type.imm byte) in - let elt = tmp et in - let zero = Word.zero t_width in - let bits = Word.of_int ~width:byte e_width in - - let foreach_size f = List.concat @@ List.init nops ~f in - let getelement o i = - (* assumption: immediate operands are repeated for all vector + let padding hi lo = + if hi < lo then [] + else if has_vex then [ int_exp 0 (hi - lo + 1) ] + else [ Bil.Extract (hi, lo, op2e tdst dst) ] + in + let offsets = + List.sort + ~compare:(fun { offdstoffset = o1; _ } { offdstoffset = o2; _ } -> + Int.compare o1 o2) + offsets + in + let add_exp (elist, nextbit) + { offlen; offtyp; offop; offsrcoffset; offdstoffset } = + ( Bil.Extract + (!!offlen + offsrcoffset - 1, offsrcoffset, op2e offtyp offop) + :: padding (offdstoffset - 1) nextbit + @ elist, + offdstoffset + !!offlen ) + in + let elist, nextbit = List.fold_left ~f:add_exp ~init:([], 0) offsets in + let elist = padding (!!tdst - 1) nextbit @ elist in + [ assn tdst dst (concat_explist elist) ] + | Punpck (t, et, o, d, s, vs) -> + let nelem = + match (t, et) with + | Type.Imm n, Type.Imm n' -> n / n' + | _ -> disfailwith "invalid" + in + assert (nelem mod 2 = 0); + let nelem_per_src = nelem / 2 in + let halft = Type.Imm (!!t / 2) in + let castf = + match o with + | High -> fun e -> Bil.(Cast (HIGH, !!halft, e)) + | Low -> fun e -> Bil.(Cast (LOW, !!halft, e)) + in + let se, de = (castf (op2e t s), castf (op2e t d)) in + let st, dt = (tmp halft, tmp halft) in + let et' = !!et in + let mape i = + [ + extract_element et' (Bil.Var st) i; + extract_element et' (Bil.Var dt) i; + ] + in + let e = + concat_explist + (List.concat + (List.map ~f:mape + (List.range ~stride:(-1) ~stop:`inclusive (nelem_per_src - 1) + 0))) + in + let dest = match vs with None -> d | Some vdst -> vdst in + [ Bil.Move (st, se); Bil.Move (dt, de); assn t dest e ] + | Ppackedbinop (t, et, fbop, _, d, s, vs) -> + let t_width = bitwidth_of_type t in + let e_width = bitwidth_of_type et in + let nops = t_width / e_width in + let byte = 8 in + let tmp_dst = tmp t in + let vdst = Option.value ~default:d vs in + let iv = tmp (Type.imm byte) in + let elt = tmp et in + let zero = Word.zero t_width in + let bits = Word.of_int ~width:byte e_width in + + let foreach_size f = List.concat @@ List.init nops ~f in + let getelement o i = + (* assumption: immediate operands are repeated for all vector elements *) - match o with - | Oimm _ -> op2e et o - | _ -> extract_element !!et (op2e t o) i in - - List.concat Bil.[ - [tmp_dst := int zero]; - foreach_size (fun i -> [ - elt := fbop (getelement d i) (getelement s i); - iv := int @@ Word.of_int ~width:byte i; - tmp_dst := - var tmp_dst lor - ((cast unsigned t_width (var elt)) lsl (var iv * int bits)) - ] - ); - [assn t vdst (var tmp_dst)] - ] - | Pbinop(t, fbop, _s, o1, o2, vop) -> - (match vop with - | None -> [assn t o1 (fbop (op2e t o1) (op2e t o2))] - | Some vop -> [assn t o1 (fbop (op2e t vop) (op2e t o2))]) - | Pcmp (t,elet,bop,_,dst,src,vsrc) -> - let elebits = bitwidth_of_type elet in - let t_width = bitwidth_of_type t in - let ncmps = t_width / elebits in - let src = match src with - | Ovec _ -> op2e t src - | Oaddr a -> load (size_of_typ t) a - | Oreg _ | Oimm _ | Oseg _ -> disfailwith "invalid" in - let vsrc = Option.value ~default:dst vsrc in - let byte = 8 in - let tmp_dst = tmp t in - let iv = tmp (Type.imm byte) in - let elt = tmp elet in - let elt_1 = tmp elet in - let elt_2 = tmp elet in - let _one = Word.of_int ~width:elebits (-1) in - let zero = Word.zero elebits in - let bits = Word.of_int ~width:byte elebits in - let zero_long = Word.zero t_width in - let foreach_size f = - let sizes = List.init ncmps ~f:(fun i -> - let left_bit = i * elebits in - let right_bit = (i + 1) * elebits - 1 in - let i = Word.of_int ~width:byte i in - i, left_bit, right_bit) in - List.concat @@ List.map sizes ~f in - - List.concat Bil.[ - [tmp_dst := int zero_long]; - foreach_size (fun (i, left_bit, right_bit) -> [ - elt_1 := extract right_bit left_bit src; - elt_2 := extract right_bit left_bit (op2e t vsrc); - iv := int i; - if_ (binop bop (var elt_1) (var elt_2)) [ - elt := int _one; - ] [ - elt := int zero; - ]; - tmp_dst := - var tmp_dst lor - ((cast unsigned t_width (var elt)) lsl (var iv * int bits)) - ]); - [assn t dst (var tmp_dst)] ] + match o with + | Oimm _ -> op2e et o + | _ -> extract_element !!et (op2e t o) i + in + + List.concat + Bil. + [ + [ tmp_dst := int zero ]; + foreach_size (fun i -> + [ + elt := fbop (getelement d i) (getelement s i); + iv := int @@ Word.of_int ~width:byte i; + tmp_dst := + var tmp_dst + lor cast unsigned t_width (var elt) + lsl (var iv * int bits); + ]); + [ assn t vdst (var tmp_dst) ]; + ] + | Pbinop (t, fbop, _s, o1, o2, vop) -> ( + match vop with + | None -> [ assn t o1 (fbop (op2e t o1) (op2e t o2)) ] + | Some vop -> [ assn t o1 (fbop (op2e t vop) (op2e t o2)) ]) + | Pcmp (t, elet, bop, _, dst, src, vsrc) -> + let elebits = bitwidth_of_type elet in + let t_width = bitwidth_of_type t in + let ncmps = t_width / elebits in + let src = + match src with + | Ovec _ -> op2e t src + | Oaddr a -> load (size_of_typ t) a + | Oreg _ | Oimm _ | Oseg _ -> disfailwith "invalid" + in + let vsrc = Option.value ~default:dst vsrc in + let byte = 8 in + let tmp_dst = tmp t in + let iv = tmp (Type.imm byte) in + let elt = tmp elet in + let elt_1 = tmp elet in + let elt_2 = tmp elet in + let _one = Word.of_int ~width:elebits (-1) in + let zero = Word.zero elebits in + let bits = Word.of_int ~width:byte elebits in + let zero_long = Word.zero t_width in + let foreach_size f = + let sizes = + List.init ncmps ~f:(fun i -> + let left_bit = i * elebits in + let right_bit = ((i + 1) * elebits) - 1 in + let i = Word.of_int ~width:byte i in + (i, left_bit, right_bit)) + in + List.concat @@ List.map sizes ~f + in + + List.concat + Bil. + [ + [ tmp_dst := int zero_long ]; + foreach_size (fun (i, left_bit, right_bit) -> + [ + elt_1 := extract right_bit left_bit src; + elt_2 := extract right_bit left_bit (op2e t vsrc); + iv := int i; + if_ + (binop bop (var elt_1) (var elt_2)) + [ elt := int _one ] + [ elt := int zero ]; + tmp_dst := + var tmp_dst + lor cast unsigned t_width (var elt) + lsl (var iv * int bits); + ]); + [ assn t dst (var tmp_dst) ]; + ] | Pmov (t, dstet, srcet, dst, src, ext, _) -> - let nelem = match t, dstet with - | Type.Imm n, Type.Imm n' -> n / n' - | _ -> disfailwith "invalid" - in - let getelt op i = extract_element !!srcet (op2e t op) i in - let extcast = - let open Exp in - match ext with - | UNSIGNED | SIGNED -> fun e -> Bil.Cast (ext, !!dstet, e) - | _ -> disfailwith "invalid" - in - let extend i = extcast (getelt src i) in - let e = concat_explist (List.map ~f:extend (List.range ~stride:(-1) ~stop:`inclusive (nelem-1) 0)) in - [assn t dst e] - | Pmovmskb (t,dst,src) -> - let nbytes = bytes_of_width t in - let src = match src with - | Ovec _ -> op2e t src - | _ -> disfailwith "invalid operand" - in - let get_bit i = Bil.Extract(i*8-1, i*8-1, src) in - let byte_indices = List.init ~f:(fun i -> i + 1) nbytes in (* list 1-nbytes *) - let all_bits = List.rev (List.map ~f:get_bit byte_indices) in - (* could also be done with shifts *) - let padt = Type.Imm(32 - nbytes) in - let or_together_bits = List.fold_left ~f:(fun acc i -> Bil.Concat(acc,i)) ~init:(int_exp 0 (!!padt)) all_bits in - [assn reg32_t dst or_together_bits] - | Palignr (t,dst,src,vsrc,imm) -> - let (dst_e, t_concat) = op2e_keep_width t dst in - let (src_e, t_concat') = op2e_keep_width t src in - (* previously, this code called Typecheck.infer_ast. - * We're now just preserving the widths, so here we assert - * that our 2 "preserved widths" are the same. *) - assert (!!t_concat = !!t_concat'); - let imm = op2e t imm in - let conct = Bil.(dst_e ^ src_e) in - let shift = Bil.(conct lsr (Cast (UNSIGNED, !!t_concat, imm lsl (int_exp 3 !!t)))) in - let high, low = match t with - | Type.Imm 256 -> 255, 0 - | Type.Imm 128 -> 127, 0 - | Type.Imm 64 -> 63, 0 - | _ -> disfailwith "impossible: used non 64/128/256-bit operand in palignr" - in - let result = Bil.Extract (high, low, shift) in - let im i = Bil.Int (int_of_mode mode i) in - let addresses = List.fold - ~f:(fun acc -> function Oaddr a -> a::acc | _ -> acc) ~init:[] [src;dst] in - (* Palignr seems to cause a CPU general protection exception if this fails. - * previously this code used the ast.ml Assert statement, which is gone, - * so it's been replaced with Bil's CpuExn *) - List.map ~f:(fun addr -> Bil.If (Bil.((addr land im 15) = im 0), - [], [Cpu_exceptions.general_protection])) addresses - @ (match vsrc with - | None -> [assn t dst result] - | Some vdst -> [assn t vdst result]) - | Pcmpstr(t,xmm1,xmm2m128,_imm,imm8cb,pcmpinfo) -> - let open Pcmpstr in - let concat elt_width exps = match exps with - | [] -> disfailwith "trying concat on empty list" - | first :: exps' -> - let len = List.length exps * elt_width in - let exp = List.fold exps' ~init:first ~f:(fun e e' -> Bil.(e ^ e')) in - let tmp = tmp (Type.imm len) in - tmp, Bil.[tmp := exp] in - - (* All bytes and bits are numbered with zero being the least + let nelem = + match (t, dstet) with + | Type.Imm n, Type.Imm n' -> n / n' + | _ -> disfailwith "invalid" + in + let getelt op i = extract_element !!srcet (op2e t op) i in + let extcast = + let open Exp in + match ext with + | UNSIGNED | SIGNED -> fun e -> Bil.Cast (ext, !!dstet, e) + | _ -> disfailwith "invalid" + in + let extend i = extcast (getelt src i) in + let e = + concat_explist + (List.map ~f:extend + (List.range ~stride:(-1) ~stop:`inclusive (nelem - 1) 0)) + in + [ assn t dst e ] + | Pmovmskb (t, dst, src) -> + let nbytes = bytes_of_width t in + let src = + match src with + | Ovec _ -> op2e t src + | _ -> disfailwith "invalid operand" + in + let get_bit i = Bil.Extract ((i * 8) - 1, (i * 8) - 1, src) in + let byte_indices = List.init ~f:(fun i -> i + 1) nbytes in + (* list 1-nbytes *) + let all_bits = List.rev (List.map ~f:get_bit byte_indices) in + (* could also be done with shifts *) + let padt = Type.Imm (32 - nbytes) in + let or_together_bits = + List.fold_left + ~f:(fun acc i -> Bil.Concat (acc, i)) + ~init:(int_exp 0 !!padt) all_bits + in + [ assn reg32_t dst or_together_bits ] + | Palignr (t, dst, src, vsrc, imm) -> ( + let dst_e, t_concat = op2e_keep_width t dst in + let src_e, t_concat' = op2e_keep_width t src in + (* previously, this code called Typecheck.infer_ast. + * We're now just preserving the widths, so here we assert + * that our 2 "preserved widths" are the same. *) + assert (!!t_concat = !!t_concat'); + let imm = op2e t imm in + let conct = Bil.(dst_e ^ src_e) in + let shift = + Bil.(conct lsr Cast (UNSIGNED, !!t_concat, imm lsl int_exp 3 !!t)) + in + let high, low = + match t with + | Type.Imm 256 -> (255, 0) + | Type.Imm 128 -> (127, 0) + | Type.Imm 64 -> (63, 0) + | _ -> + disfailwith + "impossible: used non 64/128/256-bit operand in palignr" + in + let result = Bil.Extract (high, low, shift) in + let im i = Bil.Int (int_of_mode mode i) in + let addresses = + List.fold + ~f:(fun acc -> function Oaddr a -> a :: acc | _ -> acc) + ~init:[] [ src; dst ] + in + (* Palignr seems to cause a CPU general protection exception if this fails. + * previously this code used the ast.ml Assert statement, which is gone, + * so it's been replaced with Bil's CpuExn *) + List.map + ~f:(fun addr -> + Bil.If + ( Bil.(addr land im 15 = im 0), + [], + [ Cpu_exceptions.general_protection ] )) + addresses + @ + match vsrc with + | None -> [ assn t dst result ] + | Some vdst -> [ assn t vdst result ]) + | Pcmpstr (t, xmm1, xmm2m128, _imm, imm8cb, pcmpinfo) -> + let open Pcmpstr in + let concat elt_width exps = + match exps with + | [] -> disfailwith "trying concat on empty list" + | first :: exps' -> + let len = List.length exps * elt_width in + let exp = + List.fold exps' ~init:first ~f:(fun e e' -> Bil.(e ^ e')) + in + let tmp = tmp (Type.imm len) in + (tmp, Bil.[ tmp := exp ]) + in + + (* All bytes and bits are numbered with zero being the least significant. This includes strings! *) - (* NOTE: Strings are backwards, at least when they are in + (* NOTE: Strings are backwards, at least when they are in registers. This doesn't seem to be documented in the Intel manual. This means that the NULL byte comes before the string. *) - let xmm1_e = op2e t xmm1 in - let xmm2m128_e = op2e t xmm2m128 in - let regm = type_of_mode mode in - - let nelem, _nbits, elemt = match imm8cb.ssize with - | Bytes -> 16, 8, Type.imm 8 - | Words -> 8, 16, Type.imm 16 in + let xmm1_e = op2e t xmm1 in + let xmm2m128_e = op2e t xmm2m128 in + let regm = type_of_mode mode in + + let nelem, _nbits, elemt = + match imm8cb.ssize with + | Bytes -> (16, 8, Type.imm 8) + | Words -> (8, 16, Type.imm 16) + in - (* Get element index in e *) - let get_elem = extract_element !!elemt in - let get_xmm1 = get_elem xmm1_e in - let get_xmm2 = get_elem xmm2m128_e in + (* Get element index in e *) + let get_elem = extract_element !!elemt in + let get_xmm1 = get_elem xmm1_e in + let get_xmm2 = get_elem xmm2m128_e in - let nelem_range = - List.range ~stride:(-1) ~stop:`inclusive (nelem-1) 0 in + let nelem_range = + List.range ~stride:(-1) ~stop:`inclusive (nelem - 1) 0 + in - (* Build expressions that assigns the correct values to the + (* Build expressions that assigns the correct values to the is_valid variables using implicit (NULL-based) string length. *) - let implicit_check is_valid_xmm_i get_xmm_i = - let f acc i = - let previous_valid = - if i = 0 then exp_true - else Bil.var (is_valid_xmm_i (i - 1)) in - let current_valid = - Bil.(get_xmm_i i <> (int_exp 0 !!elemt)) in - let x = is_valid_xmm_i i in - Bil.(x := previous_valid land current_valid) :: acc in - List.fold ~f:f ~init:[] nelem_range in - - (* Build expressions that assigns the correct values to the + let implicit_check is_valid_xmm_i get_xmm_i = + let f acc i = + let previous_valid = + if i = 0 then exp_true else Bil.var (is_valid_xmm_i (i - 1)) + in + let current_valid = Bil.(get_xmm_i i <> int_exp 0 !!elemt) in + let x = is_valid_xmm_i i in + Bil.(x := previous_valid land current_valid) :: acc + in + List.fold ~f ~init:[] nelem_range + in + + (* Build expressions that assigns the correct values to the is_valid variables using explicit string length. *) - let explicit_check is_valid_xmm_i sizee = - (* Max size is nelem *) - let nelem_e = Word.of_int ~width:(bitwidth_of_type regm) nelem in - let sizev = tmp ~name:"sz" regm in - let init = Bil.[ - if_ (int nelem_e < sizee) [ - sizev := int nelem_e; - ] [ - sizev := sizee; - ] - ] in - let f acc i = - (* Current element is valid *) - let current_valid = Bil.(int_exp i !!regm < var sizev) in - let x = is_valid_xmm_i i in - Bil.(x := current_valid) :: acc in - List.fold_left ~f ~init nelem_range in - - (* Get var name indicating whether index in xmm num is a valid - byte (before NULL byte). *) - (* XXX more hashtable code *) - let is_valid = - let vh = Hashtbl.Poly.create () ~size:(2*nelem) in - (fun xmmnum index -> match Hashtbl.find vh (xmmnum,index) with - | Some v -> v - | None -> - let name = sprintf "is_valid_xmm%d_ele%d" xmmnum index in - let v = tmp ~name bool_t in - Hashtbl.add_exn vh ~key:(xmmnum,index) ~data:v; - v) in - - let is_valid_xmm1 index = is_valid 1 index in - let is_valid_xmm2 index = is_valid 2 index in - let is_valid_xmm1_e index = Bil.Var(is_valid_xmm1 index) in - let is_valid_xmm2_e index = Bil.Var(is_valid_xmm2 index) in - - let xmm1_checks, xmm2_checks = - match pcmpinfo.len with - | Implicit -> - implicit_check is_valid_xmm1 get_xmm1, - implicit_check is_valid_xmm2 get_xmm2 - | Explicit -> - explicit_check is_valid_xmm1 rax_e, - explicit_check is_valid_xmm2 rdx_e in - - let get_bit index = - match imm8cb.agg with - | EqualAny -> - (* Is xmm2[index] at xmm1[j]? *) - let check_char acc j = - let is_eql = Bil.(get_xmm2 index = get_xmm1 j) in - let is_valid = is_valid_xmm1_e j in - Bil.((is_eql land is_valid) lor acc) + let explicit_check is_valid_xmm_i sizee = + (* Max size is nelem *) + let nelem_e = Word.of_int ~width:(bitwidth_of_type regm) nelem in + let sizev = tmp ~name:"sz" regm in + let init = + Bil. + [ + if_ + (int nelem_e < sizee) + [ sizev := int nelem_e ] + [ sizev := sizee ]; + ] in - (* Is xmm2[index] included in xmm1[j] for any j? *) - Bil.(is_valid_xmm2_e index land - (List.fold ~f:check_char ~init:exp_false nelem_range)) - | Ranges -> - (* Is there an even j such that xmm1[j] <= xmm2[index] <= + let f acc i = + (* Current element is valid *) + let current_valid = Bil.(int_exp i !!regm < var sizev) in + let x = is_valid_xmm_i i in + Bil.(x := current_valid) :: acc + in + List.fold_left ~f ~init nelem_range + in + + (* Get var name indicating whether index in xmm num is a valid + byte (before NULL byte). *) + (* XXX more hashtable code *) + let is_valid = + let vh = Hashtbl.Poly.create () ~size:(2 * nelem) in + fun xmmnum index -> + match Hashtbl.find vh (xmmnum, index) with + | Some v -> v + | None -> + let name = sprintf "is_valid_xmm%d_ele%d" xmmnum index in + let v = tmp ~name bool_t in + Hashtbl.add_exn vh ~key:(xmmnum, index) ~data:v; + v + in + + let is_valid_xmm1 index = is_valid 1 index in + let is_valid_xmm2 index = is_valid 2 index in + let is_valid_xmm1_e index = Bil.Var (is_valid_xmm1 index) in + let is_valid_xmm2_e index = Bil.Var (is_valid_xmm2 index) in + + let xmm1_checks, xmm2_checks = + match pcmpinfo.len with + | Implicit -> + ( implicit_check is_valid_xmm1 get_xmm1, + implicit_check is_valid_xmm2 get_xmm2 ) + | Explicit -> + ( explicit_check is_valid_xmm1 rax_e, + explicit_check is_valid_xmm2 rdx_e ) + in + + let get_bit index = + match imm8cb.agg with + | EqualAny -> + (* Is xmm2[index] at xmm1[j]? *) + let check_char acc j = + let is_eql = Bil.(get_xmm2 index = get_xmm1 j) in + let is_valid = is_valid_xmm1_e j in + Bil.(is_eql land is_valid lor acc) + in + (* Is xmm2[index] included in xmm1[j] for any j? *) + Bil.( + is_valid_xmm2_e index + land List.fold ~f:check_char ~init:exp_false nelem_range) + | Ranges -> + (* Is there an even j such that xmm1[j] <= xmm2[index] <= xmm1[j+1]? *) - let check_char acc j = - (* XXX: Should this be AND? *) - let ind0 = 2 * j in - let ind1 = ind0 + 1 in - let rangevalid = Bil.(is_valid_xmm1_e ind0 land is_valid_xmm1_e ind1) in - let (<=) = match imm8cb.ssign with - | Unsigned -> Bil.(<=) - | Signed -> Bil.(<=$) in - let (land) = Bil.(land) in - let inrange = - (get_xmm1 ind0 <= get_xmm2 index) land (get_xmm2 index <= get_xmm1 ind1) in - Bil.(rangevalid land (inrange lor acc)) in - Bil.(is_valid_xmm2_e index land - List.fold_left ~f:check_char ~init:exp_false (List.range ~stride:(-1) ~stop:`inclusive Stdlib.(nelem/2-1) 0)) - | EqualEach -> - (* Does xmm1[index] = xmm2[index]? *) - let xmm1_invalid = Bil.(UnOp (NOT, (is_valid_xmm1_e index))) in - let xmm2_invalid = Bil.(UnOp (NOT, (is_valid_xmm2_e index))) in - let bothinvalid = Bil.(xmm1_invalid land xmm2_invalid) in - let eitherinvalid = Bil.(xmm1_invalid lor xmm2_invalid) in - let equal = Bil.(get_xmm1 index = get_xmm2 index) in - (* both invalid -> true + let check_char acc j = + (* XXX: Should this be AND? *) + let ind0 = 2 * j in + let ind1 = ind0 + 1 in + let rangevalid = + Bil.(is_valid_xmm1_e ind0 land is_valid_xmm1_e ind1) + in + let ( <= ) = + match imm8cb.ssign with + | Unsigned -> Bil.( <= ) + | Signed -> Bil.( <=$ ) + in + let ( land ) = Bil.( land ) in + let inrange = + (get_xmm1 ind0 <= get_xmm2 index) + land (get_xmm2 index <= get_xmm1 ind1) + in + Bil.(rangevalid land (inrange lor acc)) + in + Bil.( + is_valid_xmm2_e index + land List.fold_left ~f:check_char ~init:exp_false + (List.range ~stride:(-1) ~stop:`inclusive + Stdlib.((nelem / 2) - 1) + 0)) + | EqualEach -> + (* Does xmm1[index] = xmm2[index]? *) + let xmm1_invalid = Bil.(UnOp (NOT, is_valid_xmm1_e index)) in + let xmm2_invalid = Bil.(UnOp (NOT, is_valid_xmm2_e index)) in + let bothinvalid = Bil.(xmm1_invalid land xmm2_invalid) in + let eitherinvalid = Bil.(xmm1_invalid lor xmm2_invalid) in + let equal = Bil.(get_xmm1 index = get_xmm2 index) in + (* both invalid -> true one invalid -> false both valid -> check same byte *) - Bil.(bothinvalid lor (UnOp (NOT, eitherinvalid) land equal)) - | EqualOrdered -> - (* Does the substring xmm1 occur at xmm2[index]? *) - let check_char acc j = - let equal = Bil.(get_xmm1 j = get_xmm2 Stdlib.(index+j)) in - let substrended = Bil.(UnOp (NOT, (is_valid_xmm1_e j))) in - let bigstrended = Bil.UnOp (NOT, (is_valid_xmm2_e (index+j))) in - (* substrended => true + Bil.(bothinvalid lor (UnOp (NOT, eitherinvalid) land equal)) + | EqualOrdered -> + (* Does the substring xmm1 occur at xmm2[index]? *) + let check_char acc j = + let equal = Bil.(get_xmm1 j = get_xmm2 Stdlib.(index + j)) in + let substrended = Bil.(UnOp (NOT, is_valid_xmm1_e j)) in + let bigstrended = Bil.UnOp (NOT, is_valid_xmm2_e (index + j)) in + (* substrended => true bigstrended => false byte diff => false byte same => keep going *) - Bil.(substrended lor - (UnOp (NOT,bigstrended) land (equal land acc))) in - (* Is xmm1[j] equal to xmm2[index+j]? *) - List.fold_left ~f:check_char ~init:exp_true (List.range - ~stride:(-1) ~stop:`inclusive (nelem-index-1) 0) - in - let bits = List.map ~f:get_bit nelem_range in - let res, res_bil = concat 1 bits in - let int_res_1 = tmp ~name:"IntRes1" reg16_t in - let int_res_2 = tmp ~name:"IntRes2" reg16_t in - - let contains_null e = - let elts = List.init nelem ~f:(fun i -> Bil.(get_elem e i = int_exp 0 !!elemt)) in - List.fold elts ~init:exp_false ~f:(fun acc elt -> Bil.(acc lor elt)) in - - (* For pcmpistri/pcmpestri *) - let sb exp = - List.fold_left ~f:(fun acc i -> - Bil.Ite (Bil.(exp_true = Extract (i, i, exp)), - (int_exp i !!regm), acc)) - ~init:(int_exp nelem !!regm) - (match imm8cb.outselectsig with - | LSB -> List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem 0 - | MSB -> List.init ~f:(fun x -> x) nelem) - in + Bil.( + substrended lor (UnOp (NOT, bigstrended) land (equal land acc))) + in + (* Is xmm1[j] equal to xmm2[index+j]? *) + List.fold_left ~f:check_char ~init:exp_true + (List.range ~stride:(-1) ~stop:`inclusive (nelem - index - 1) 0) + in + let bits = List.map ~f:get_bit nelem_range in + let res, res_bil = concat 1 bits in + let int_res_1 = tmp ~name:"IntRes1" reg16_t in + let int_res_2 = tmp ~name:"IntRes2" reg16_t in + + let contains_null e = + let elts = + List.init nelem ~f:(fun i -> Bil.(get_elem e i = int_exp 0 !!elemt)) + in + List.fold elts ~init:exp_false ~f:(fun acc elt -> Bil.(acc lor elt)) + in + + (* For pcmpistri/pcmpestri *) + let sb exp = + List.fold_left + ~f:(fun acc i -> + Bil.Ite + (Bil.(exp_true = Extract (i, i, exp)), int_exp i !!regm, acc)) + ~init:(int_exp nelem !!regm) + (match imm8cb.outselectsig with + | LSB -> + List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem + 0 + | MSB -> List.init ~f:(fun x -> x) nelem) + in - (* For pcmpistrm/pcmpestrm *) - let mask e = - match imm8cb.outselectmask with - | Bitmask -> Bil.(cast unsigned 128 e) - | Bytemask -> - let get_element i = - Bil.(cast unsigned !!elemt (extract i i e)) in - let range = List.range ~stride:(-1) - ~start:`exclusive ~stop:`inclusive nelem 0 in - concat_explist (List.map ~f:get_element range) in - - let res_of_cb = match imm8cb with - | {negintres1=false; _} -> Bil.(int_res_2 := var int_res_1) - | {negintres1=true; maskintres1=false; _} -> (* int_res_1 is bitwise-notted *) - Bil.(int_res_2 := unop not (var int_res_1)) - | {negintres1=true; maskintres1=true; _} -> - (* only the valid elements in xmm2 are bitwise-notted *) - (* XXX: Right now we duplicate the valid element computations + (* For pcmpistrm/pcmpestrm *) + let mask e = + match imm8cb.outselectmask with + | Bitmask -> Bil.(cast unsigned 128 e) + | Bytemask -> + let get_element i = Bil.(cast unsigned !!elemt (extract i i e)) in + let range = + List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem + 0 + in + concat_explist (List.map ~f:get_element range) + in + + let res_of_cb = + match imm8cb with + | { negintres1 = false; _ } -> Bil.(int_res_2 := var int_res_1) + | { negintres1 = true; maskintres1 = false; _ } -> + (* int_res_1 is bitwise-notted *) + Bil.(int_res_2 := unop not (var int_res_1)) + | { negintres1 = true; maskintres1 = true; _ } -> + (* only the valid elements in xmm2 are bitwise-notted *) + (* XXX: Right now we duplicate the valid element computations when negating the valid elements. They are also used by the aggregation functions. A better way to implement this might be to write the valid element information out as a temporary bitvector. The aggregation functions and this code would then extract the relevant bit to see if an element is valid. *) - let validvector = - let range = List.range ~stride:(-1) - ~start:`exclusive ~stop:`inclusive nelem 0 in - let bits = List.map ~f:is_valid_xmm2_e range in - Bil.(cast unsigned 16 (concat_explist bits)) in - Bil.(int_res_2 := validvector lxor var int_res_1) in - - let res_of_pcmpinfo = match pcmpinfo.out with - | Index -> Bil.(rcx := sb (var int_res_2)) - (* FIXME: ymms should be used instead of xmms here *) - | Mask -> Bil.(ymms.(0) := mask (var int_res_2)) in - - List.concat [ - xmm1_checks; - xmm2_checks; - res_bil; - Bil.[ - int_res_1 := cast unsigned 16 (var res); - res_of_cb; - res_of_pcmpinfo; - cf := var int_res_2 <> int_exp 0 16; - zf := contains_null xmm2m128_e; - sf := contains_null xmm1_e; - oF := extract 0 0 (var int_res_2); - af := int_exp 0 1; - pf := int_exp 0 1; - ] - ] + let validvector = + let range = + List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive + nelem 0 + in + let bits = List.map ~f:is_valid_xmm2_e range in + Bil.(cast unsigned 16 (concat_explist bits)) + in + Bil.(int_res_2 := validvector lxor var int_res_1) + in + + let res_of_pcmpinfo = + match pcmpinfo.out with + | Index -> Bil.(rcx := sb (var int_res_2)) + (* FIXME: ymms should be used instead of xmms here *) + | Mask -> Bil.(ymms.(0) := mask (var int_res_2)) + in - | Pshufd (t, dst, src, vsrc, imm) -> - let src_e = op2e t src in - let imm_e = op2e t imm in - (* XXX: This would be more straight-forward if implemented using + List.concat + [ + xmm1_checks; + xmm2_checks; + res_bil; + Bil. + [ + int_res_1 := cast unsigned 16 (var res); + res_of_cb; + res_of_pcmpinfo; + cf := var int_res_2 <> int_exp 0 16; + zf := contains_null xmm2m128_e; + sf := contains_null xmm1_e; + oF := extract 0 0 (var int_res_2); + af := int_exp 0 1; + pf := int_exp 0 1; + ]; + ] + | Pshufd (t, dst, src, vsrc, imm) -> ( + let src_e = op2e t src in + let imm_e = op2e t imm in + (* XXX: This would be more straight-forward if implemented using map, instead of fold *) - let get_dword ndword = - let high_b = 2 * (ndword mod 4) + 1 in - let low_b = 2 * (ndword mod 4) in - let index = Bil.(Cast (UNSIGNED, !!t, Extract (high_b, low_b, imm_e))) in - let t' = !!t in - (* Use the same pattern for the top half of a ymm register *) - (* had to stop using extract_element_symbolic, since that calls + let get_dword ndword = + let high_b = (2 * (ndword mod 4)) + 1 in + let low_b = 2 * (ndword mod 4) in + let index = + Bil.(Cast (UNSIGNED, !!t, Extract (high_b, low_b, imm_e))) + in + let t' = !!t in + (* Use the same pattern for the top half of a ymm register *) + (* had to stop using extract_element_symbolic, since that calls * Typecheck.infer_ast. I believe this captures the same * "width logic", but this is a good place to check if things start * going wrong later. *) - let (index, index_width) = if t' = 256 && ndword > 3 then - (Bil.(index + (Int (BV.of_int ~width:(!!t) 4))), 256) - else (index, t') in - extract_element_symbolic_with_width (Type.imm 32) src_e index index_width - in - let topdword = match t with Type.Imm 128 -> 3 | _ -> 7 in - let dwords = concat_explist (List.map ~f:get_dword (List.range ~stride:(-1) ~stop:`inclusive topdword 0)) in - (match vsrc with - | None -> [assn t dst dwords] - | Some vdst -> [assn t vdst dwords]) + let index, index_width = + if t' = 256 && ndword > 3 then + (Bil.(index + Int (BV.of_int ~width:!!t 4)), 256) + else (index, t') + in + extract_element_symbolic_with_width (Type.imm 32) src_e index + index_width + in + let topdword = match t with Type.Imm 128 -> 3 | _ -> 7 in + let dwords = + concat_explist + (List.map ~f:get_dword + (List.range ~stride:(-1) ~stop:`inclusive topdword 0)) + in + match vsrc with + | None -> [ assn t dst dwords ] + | Some vdst -> [ assn t vdst dwords ]) | Pshufb (exp_type, dst_op, src_op, vsrc) -> - let op_size = bitwidth_of_type exp_type in - let index_bits = match op_size with - | 64 -> 3 - | 128 | 256 -> 4 - | _ -> disfailwith "invalid size for pshufb" in - let foreach_byte f = List.concat @@ List.init (op_size / 8) ~f in - - let src = op2e exp_type src_op in - let dst = op2e exp_type dst_op in - let dst_op = Option.value ~default:dst_op vsrc in - let zero = Bil.int (Word.zero op_size) in - let msb_one = Bil.int (Word.of_int ~width:8 0x80) in - - let byte_t = Type.imm 8 in - let byte = int_exp 8 8 in - let iv = tmp ~name:"i" byte_t in - let mask_byte_i = tmp byte_t in - let tmp_byte = tmp exp_type in - let tmp_dst = tmp exp_type in - let ind = tmp byte_t in - - let check_mem_alignment = match src_op with - | Oaddr addr when (op_size = 128) -> - let word_size = width_of_mode mode in - let zero = Bil.int (Word.zero word_size) in - let oxf = Bil.int (Word.of_int ~width:word_size 0xf) in - [ Bil.(if_ (oxf land addr <> zero) [cpuexn 13] []) ] - | _ -> [] in - - List.concat [ - check_mem_alignment; - [Bil.move tmp_dst zero]; - foreach_byte (fun i -> - Bil.[ - iv := int (Word.of_int ~width:8 i); - mask_byte_i := extract 7 0 (src lsr (var iv * byte)); - if_ (msb_one land var mask_byte_i = msb_one) [ - tmp_byte := zero; - ] (* else *) [ - ind := cast unsigned 8 (extract index_bits 0 (var mask_byte_i)); - tmp_byte := - cast unsigned op_size (extract 7 0 (dst lsr (var ind * byte))) - ]; - tmp_dst := Bil.(var tmp_dst lor (var tmp_byte lsl (var iv * byte))); - ]); - [assn exp_type dst_op (Bil.var tmp_dst)] - ] + let op_size = bitwidth_of_type exp_type in + let index_bits = + match op_size with + | 64 -> 3 + | 128 | 256 -> 4 + | _ -> disfailwith "invalid size for pshufb" + in + let foreach_byte f = List.concat @@ List.init (op_size / 8) ~f in + + let src = op2e exp_type src_op in + let dst = op2e exp_type dst_op in + let dst_op = Option.value ~default:dst_op vsrc in + let zero = Bil.int (Word.zero op_size) in + let msb_one = Bil.int (Word.of_int ~width:8 0x80) in + + let byte_t = Type.imm 8 in + let byte = int_exp 8 8 in + let iv = tmp ~name:"i" byte_t in + let mask_byte_i = tmp byte_t in + let tmp_byte = tmp exp_type in + let tmp_dst = tmp exp_type in + let ind = tmp byte_t in + + let check_mem_alignment = + match src_op with + | Oaddr addr when op_size = 128 -> + let word_size = width_of_mode mode in + let zero = Bil.int (Word.zero word_size) in + let oxf = Bil.int (Word.of_int ~width:word_size 0xf) in + [ Bil.(if_ (oxf land addr <> zero) [ cpuexn 13 ] []) ] + | _ -> [] + in - | Lea(t, r, a) when List.is_empty pref -> - (* See Table 3-64 *) - (* previously, it checked whether addrbits > opbits before the cast_low. + List.concat + [ + check_mem_alignment; + [ Bil.move tmp_dst zero ]; + foreach_byte (fun i -> + Bil. + [ + iv := int (Word.of_int ~width:8 i); + mask_byte_i := extract 7 0 (src lsr (var iv * byte)); + if_ + (msb_one land var mask_byte_i = msb_one) + [ tmp_byte := zero ] + (* else *) + [ + ind := + cast unsigned 8 + (extract index_bits 0 (var mask_byte_i)); + tmp_byte := + cast unsigned op_size + (extract 7 0 (dst lsr (var ind * byte))); + ]; + (tmp_dst := + Bil.(var tmp_dst lor (var tmp_byte lsl (var iv * byte)))); + ]); + [ assn exp_type dst_op (Bil.var tmp_dst) ]; + ] + | Lea (t, r, a) when List.is_empty pref -> + (* See Table 3-64 *) + (* previously, it checked whether addrbits > opbits before the cast_low. * The conclusion we came to was that - if they were equal, the cast is basically a nop - if it was the other way round, you want to extend it anyway. * (I may be remembering things wrongly) *) - [assn t r Bil.(Cast (LOW, !!t, a))] - | Call(o1, ra) -> - (* If o1 is an immediate, we should syntactically have Jump(imm) + [ assn t r Bil.(Cast (LOW, !!t, a)) ] + | Call (o1, ra) -> ( + (* If o1 is an immediate, we should syntactically have Jump(imm) so that the CFG algorithm knows where the jump goes. Otherwise it will point to BB_Indirect. Otherwise, we should evaluate the operand before decrementing esp. (This really only matters when esp is the base register of a memory lookup. *) - let target = op2e mt o1 in - (match o1 with - | Oimm _ -> - [Bil.Move (rsp, Bil.(rsp_e - (Int (mi (bytes_of_width mt))))); - store_s mode None mt rsp_e (Bil.Int ra); - Bil.Jmp target] - | _ -> - let t = tmp mt in - [Bil.Move (t, target); - Bil.Move (rsp, Bil.(rsp_e - (Int (mi (bytes_of_width mt))))); - store_s mode None mt rsp_e (Bil.Int ra); - Bil.Jmp (Bil.Var t)]) - | Jump(o) -> - [Bil.Jmp (jump_target mode ss has_rex o)] - | Jcc(o, c) -> - [Bil.If (c, [Bil.Jmp (jump_target mode ss has_rex o)], [])] - | Setcc(t, o1, c) -> - [assn t o1 Bil.(Cast (UNSIGNED, !!t, c))] - | Shift(st, s, dst, shift) -> - let old = tmp ~name:"tmp" s in - let s' = !!s in - let size = int_exp s' s' in - let s_f = Bil.(match st with - | LSHIFT -> (lsl) - | RSHIFT -> (lsr) - | ARSHIFT -> (asr) - | _ -> disfailwith "invalid shift type") in - let dste = op2e s dst in - let count_mask = Bil.(size - int_exp 1 s') in - let count = Bil.(op2e s shift land count_mask) in - let new_of = match st with - | LSHIFT -> Bil.((Cast (HIGH, !!bool_t, dste)) lxor cf_e) - | RSHIFT -> Bil.(Cast (HIGH, !!bool_t, var old)) - | ARSHIFT -> exp_false - | _ -> disfailwith "impossible" - in - let new_cf = - (* undefined for SHL and SHR instructions where the count is greater than + let target = op2e mt o1 in + match o1 with + | Oimm _ -> + [ + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width mt)))); + store_s mode None mt rsp_e (Bil.Int ra); + Bil.Jmp target; + ] + | _ -> + let t = tmp mt in + [ + Bil.Move (t, target); + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width mt)))); + store_s mode None mt rsp_e (Bil.Int ra); + Bil.Jmp (Bil.Var t); + ]) + | Jump o -> [ Bil.Jmp (jump_target mode ss has_rex o) ] + | Jcc (o, c) -> + [ Bil.If (c, [ Bil.Jmp (jump_target mode ss has_rex o) ], []) ] + | Setcc (t, o1, c) -> [ assn t o1 Bil.(Cast (UNSIGNED, !!t, c)) ] + | Shift (st, s, dst, shift) -> + let old = tmp ~name:"tmp" s in + let s' = !!s in + let size = int_exp s' s' in + let s_f = + Bil.( + match st with + | LSHIFT -> ( lsl ) + | RSHIFT -> ( lsr ) + | ARSHIFT -> ( asr ) + | _ -> disfailwith "invalid shift type") + in + let dste = op2e s dst in + let count_mask = Bil.(size - int_exp 1 s') in + let count = Bil.(op2e s shift land count_mask) in + let new_of = + match st with + | LSHIFT -> Bil.(Cast (HIGH, !!bool_t, dste) lxor cf_e) + | RSHIFT -> Bil.(Cast (HIGH, !!bool_t, var old)) + | ARSHIFT -> exp_false + | _ -> disfailwith "impossible" + in + let new_cf = + (* undefined for SHL and SHR instructions where the count is greater than or equal to the size (in bits) of the destination operand *) - match st with - | LSHIFT -> Bil.(Cast (LOW, !!bool_t, var old lsr (size - count))) - | RSHIFT | ARSHIFT -> - Bil.(Cast (HIGH, !!bool_t, var old lsl (size - count))) - | _ -> failwith "impossible" - in - Bil.[ - old := dste; - assn s dst (s_f dste count); - if_ (count <> int_exp 0 s') [ - cf := new_cf; - sf := compute_sf dste; - zf := compute_zf s' dste; - pf := compute_pf s dste; - af := unknown "after-shift" bool_t; - if_ (count = int_exp 1 s') [ - oF := new_of; - ] [ - oF := unknown "after-shift" bool_t; + match st with + | LSHIFT -> Bil.(Cast (LOW, !!bool_t, var old lsr (size - count))) + | RSHIFT | ARSHIFT -> + Bil.(Cast (HIGH, !!bool_t, var old lsl (size - count))) + | _ -> failwith "impossible" + in + Bil. + [ + old := dste; + assn s dst (s_f dste count); + if_ + (count <> int_exp 0 s') + [ + cf := new_cf; + sf := compute_sf dste; + zf := compute_zf s' dste; + pf := compute_pf s dste; + af := unknown "after-shift" bool_t; + if_ + (count = int_exp 1 s') + [ oF := new_of ] + [ oF := unknown "after-shift" bool_t ]; + ] + []; ] - ] []; - ] - | Shiftd(st, s, dst, fill, count) -> - let was = tmp ~name:"tmp" s in - let e_dst = op2e s dst in - let e_fill = op2e s fill in - let s' = !!s in - (* Check for 64-bit operand *) - let size = int_exp s' s' in - let count_mask = Bil.(size - int_exp 1 s') in - let e_count = Bil.(op2e s count land count_mask) in - let new_cf = match st with - | LSHIFT -> Bil.(Cast (LOW, !!bool_t, var was lsr (size - e_count))) - | RSHIFT -> Bil.(Cast (HIGH, !!bool_t, var was lsl (size - e_count))) - | _ -> disfailwith "impossible" in - let new_of = Bil.(Cast (HIGH, !!bool_t, (var was lxor e_dst))) in - let unk_of = - Bil.Unknown ("OF undefined after shiftd of more then 1 bit", bool_t) in - let ret1 = match st with - | LSHIFT -> Bil.(e_fill lsr (size - e_count)) - | RSHIFT -> Bil.(e_fill lsl (size - e_count)) - | _ -> disfailwith "impossible" in - let ret2 = match st with - | LSHIFT -> Bil.(e_dst lsl e_count) - | RSHIFT -> Bil.(e_dst lsr e_count) - | _ -> disfailwith "impossible" in - let result = Bil.(ret1 lor ret2) in - (* SWXXX If shift is greater than the operand size, dst and + | Shiftd (st, s, dst, fill, count) -> + let was = tmp ~name:"tmp" s in + let e_dst = op2e s dst in + let e_fill = op2e s fill in + let s' = !!s in + (* Check for 64-bit operand *) + let size = int_exp s' s' in + let count_mask = Bil.(size - int_exp 1 s') in + let e_count = Bil.(op2e s count land count_mask) in + let new_cf = + match st with + | LSHIFT -> Bil.(Cast (LOW, !!bool_t, var was lsr (size - e_count))) + | RSHIFT -> Bil.(Cast (HIGH, !!bool_t, var was lsl (size - e_count))) + | _ -> disfailwith "impossible" + in + let new_of = Bil.(Cast (HIGH, !!bool_t, var was lxor e_dst)) in + let unk_of = + Bil.Unknown ("OF undefined after shiftd of more then 1 bit", bool_t) + in + let ret1 = + match st with + | LSHIFT -> Bil.(e_fill lsr (size - e_count)) + | RSHIFT -> Bil.(e_fill lsl (size - e_count)) + | _ -> disfailwith "impossible" + in + let ret2 = + match st with + | LSHIFT -> Bil.(e_dst lsl e_count) + | RSHIFT -> Bil.(e_dst lsr e_count) + | _ -> disfailwith "impossible" + in + let result = Bil.(ret1 lor ret2) in + (* SWXXX If shift is greater than the operand size, dst and flags are undefined *) - Bil.[ - was := e_dst; - assn s dst result; - if_ (e_count <> int_exp 0 s') [ - cf := new_cf; - sf := compute_sf e_dst; - zf := compute_zf s' e_dst; - pf := compute_pf s e_dst; - (* For a 1-bit shift, the OF flag is set if a sign change occurred; + Bil. + [ + was := e_dst; + assn s dst result; + if_ + (e_count <> int_exp 0 s') + [ + cf := new_cf; + sf := compute_sf e_dst; + zf := compute_zf s' e_dst; + pf := compute_pf s e_dst; + (* For a 1-bit shift, the OF flag is set if a sign change occurred; otherwise, it is cleared. For shifts greater than 1 bit, the OF flag is undefined. *) - if_ (e_count = int_exp 1 s') [ - oF := new_of; - ] [ - oF := unk_of; + if_ (e_count = int_exp 1 s') [ oF := new_of ] [ oF := unk_of ]; + ] + []; ] - ] [] - ] - | Rotate(shift_type, exp_type, dst_op, shift_op, use_cf) -> - if use_cf then unimplemented "rotate use_vf"; - let word_size = bitwidth_of_type exp_type in - let mask_size = word_size - 1 in - let count_var = tmp exp_type in - let count = Bil.var count_var in - let zero = int_exp 0 word_size in - let one = int_exp 1 word_size in - let dst = op2e exp_type dst_op in - let shift_mask = int_exp mask_size word_size in - let size = int_exp word_size word_size in - let shift = op2e exp_type shift_op in - - if [%compare.equal: binop] shift_type LSHIFT then - Bil.[ - count_var := (shift land shift_mask) mod size; - assn exp_type dst_op ((dst lsl count) lor (dst lsr (size - count))); - if_ (count = zero) [ - cf := cast low 1 dst; - ] (* else *) [ - if_ (count = one) [ - oF := cf_e lxor (cast high 1 dst); - ] (* else *) [ - oF := unknown "OF undefined after rotate of more then 1 bit" bool_t; + | Rotate (shift_type, exp_type, dst_op, shift_op, use_cf) -> + if use_cf then unimplemented "rotate use_vf"; + let word_size = bitwidth_of_type exp_type in + let mask_size = word_size - 1 in + let count_var = tmp exp_type in + let count = Bil.var count_var in + let zero = int_exp 0 word_size in + let one = int_exp 1 word_size in + let dst = op2e exp_type dst_op in + let shift_mask = int_exp mask_size word_size in + let size = int_exp word_size word_size in + let shift = op2e exp_type shift_op in + + if [%compare.equal: binop] shift_type LSHIFT then + Bil. + [ + count_var := shift land shift_mask mod size; + assn exp_type dst_op ((dst lsl count) lor (dst lsr (size - count))); + if_ (count = zero) + [ cf := cast low 1 dst ] + (* else *) + [ + if_ (count = one) + [ oF := cf_e lxor cast high 1 dst ] + (* else *) + [ + oF := + unknown "OF undefined after rotate of more then 1 bit" + bool_t; + ]; + ]; ] - ] - ] - else - Bil.[ - count_var := (shift land shift_mask) mod size; - assn exp_type dst_op ((dst lsr count) lor (dst lsl (size - count))); - if_ (count = zero) [ - cf := cast high 1 dst; - ] (* else *) [ - if_ (count = one) [ - oF := cast high 1 dst lxor (cast high 1 (dst lsl int_exp 1 word_size)); - ] (* else *) [ - oF := unknown "OF undefined after rotate of more then 1 bit" bool_t; + else + Bil. + [ + count_var := shift land shift_mask mod size; + assn exp_type dst_op ((dst lsr count) lor (dst lsl (size - count))); + if_ (count = zero) + [ cf := cast high 1 dst ] + (* else *) + [ + if_ (count = one) + [ + oF := + cast high 1 dst + lxor cast high 1 (dst lsl int_exp 1 word_size); + ] + (* else *) + [ + oF := + unknown "OF undefined after rotate of more then 1 bit" + bool_t; + ]; + ]; ] - ] + | Bt (t, bitoffset, bitbase) -> + let t' = !!t in + let offset = op2e t bitoffset in + let value, shift = + match bitbase with + | Oreg _ -> + let reg = op2e t bitbase in + let shift = Bil.(offset land int_exp Stdlib.(t' - 1) t') in + (reg, shift) + | Oaddr a -> + let offset = Bil.(cast unsigned (width_of_mode mode) offset) in + let byte = + load (size_of_typ reg8_t) Bil.(a + (offset lsr int_exp 3 t')) + in + let shift = Bil.(Cast (LOW, !!reg8_t, offset) land int_exp 7 8) in + (byte, shift) + | Ovec _ | Oseg _ | Oimm _ -> disfailwith "Invalid bt operand" + in + [ + Bil.Move (cf, Bil.(Cast (LOW, !!bool_t, value lsr shift))); + Bil.Move (oF, Bil.Unknown ("OF undefined after bt", bool_t)); + Bil.Move (sf, Bil.Unknown ("SF undefined after bt", bool_t)); + Bil.Move (af, Bil.Unknown ("AF undefined after bt", bool_t)); + Bil.Move (pf, Bil.Unknown ("PF undefined after bt", bool_t)); ] - | Bt(t, bitoffset, bitbase) -> - let t' = !!t in - let offset = op2e t bitoffset in - let value, shift = match bitbase with - | Oreg _ -> - let reg = op2e t bitbase in - let shift = Bil.(offset land int_exp Stdlib.(t' - 1) t') in - reg, shift - | Oaddr a -> - let offset = Bil.(cast unsigned (width_of_mode mode) offset) in - let byte = load (size_of_typ reg8_t) Bil.(a + offset lsr int_exp 3 t') in - let shift = Bil.(Cast (LOW, !!reg8_t, offset) land int_exp 7 8) in - byte, shift - | Ovec _ | Oseg _ | Oimm _ -> disfailwith "Invalid bt operand" - in - [ - Bil.Move (cf, Bil.(Cast (LOW, !!bool_t, value lsr shift))); - Bil.Move (oF, Bil.Unknown ("OF undefined after bt", bool_t)); - Bil.Move (sf, Bil.Unknown ("SF undefined after bt", bool_t)); - Bil.Move (af, Bil.Unknown ("AF undefined after bt", bool_t)); - Bil.Move (pf, Bil.Unknown ("PF undefined after bt", bool_t)) - ] - | Bs(t, dst, src, dir) -> - let is_zero_count = List.rev pref |> List.exists ~f:Int.((=) 0xf3) in - let width = !!t in - let src_e = op2e t src in - let is_fwd = match dir with - | Backward -> false - | Forward -> true in - let res = tmp t in - let assn_res = Bil.(res := src_e) in - let scan_bil = - if is_fwd then match width with - | 16 -> ctz16 res - | 32 -> ctz32 res - | 64 -> ctz64 res - | _ -> disfailwith "Invalid bitscan width" - else match width with - | 16 -> clz16 res - | 32 -> clz32 res - | 64 -> clz64 res - | _ -> disfailwith "Invalid bitscan width" in - let assn_result = - let n1 = width - 1 in - assn t dst @@ if is_zero_count || is_fwd then Bil.var res - else Bil.(var res lxor int Word.(of_int n1 ~width)) in - let bil = assn_res :: scan_bil in - let bil = - if is_zero_count then bil @ Bil.[ - assn_result; - cf := var res = int Word.(of_int ~width width); - zf := var res = int Word.(zero width); - ] - else Bil.[ - if_ (src_e = int (Word.zero width)) [ - zf := int Word.b1; - assn t dst @@ unknown "bits" t; - ] (bil @ Bil.[assn_result; zf := int Word.b0]); - ] in - bil @ bitscan_flags is_zero_count + | Bs (t, dst, src, dir) -> + let is_zero_count = List.rev pref |> List.exists ~f:Int.(( = ) 0xf3) in + let width = !!t in + let src_e = op2e t src in + let is_fwd = match dir with Backward -> false | Forward -> true in + let res = tmp t in + let assn_res = Bil.(res := src_e) in + let scan_bil = + if is_fwd then + match width with + | 16 -> ctz16 res + | 32 -> ctz32 res + | 64 -> ctz64 res + | _ -> disfailwith "Invalid bitscan width" + else + match width with + | 16 -> clz16 res + | 32 -> clz32 res + | 64 -> clz64 res + | _ -> disfailwith "Invalid bitscan width" + in + let assn_result = + let n1 = width - 1 in + assn t dst + @@ + if is_zero_count || is_fwd then Bil.var res + else Bil.(var res lxor int Word.(of_int n1 ~width)) + in + let bil = assn_res :: scan_bil in + let bil = + if is_zero_count then + bil + @ Bil. + [ + assn_result; + cf := var res = int Word.(of_int ~width width); + zf := var res = int Word.(zero width); + ] + else + Bil. + [ + if_ + (src_e = int (Word.zero width)) + [ zf := int Word.b1; assn t dst @@ unknown "bits" t ] + (bil @ Bil.[ assn_result; zf := int Word.b0 ]); + ] + in + bil @ bitscan_flags is_zero_count | Hlt -> [] (* x86 Hlt is essentially a NOP *) | Rdtsc -> - let undef reg = assn reg32_t reg (Bil.Unknown ("rdtsc", reg32_t)) in - List.map ~f:undef [o_rax; o_rdx] + let undef reg = assn reg32_t reg (Bil.Unknown ("rdtsc", reg32_t)) in + List.map ~f:undef [ o_rax; o_rdx ] | Cpuid -> - let undef reg = assn reg32_t reg (Bil.Unknown ("cpuid", reg32_t)) in - List.map ~f:undef [o_rax; o_rbx; o_rcx; o_rdx] + let undef reg = assn reg32_t reg (Bil.Unknown ("cpuid", reg32_t)) in + List.map ~f:undef [ o_rax; o_rbx; o_rcx; o_rdx ] | Xgetbv -> - let undef reg = assn reg32_t reg (Bil.Unknown ("xgetbv", reg32_t)) in - List.map ~f:undef [o_rax; o_rdx] - | Stmxcsr (dst) -> - let dst = match dst with - | Oaddr addr -> addr - | _ -> disfailwith "stmxcsr argument cannot be non-memory" - in - [store reg32_t dst (Bil.Var mxcsr);(*(Unknown ("stmxcsr", reg32_t));*) ] - | Ldmxcsr (src) -> - let src = match src with - | Oaddr addr -> addr - | _ -> disfailwith "ldmxcsr argument cannot be non-memory" - in - [ Bil.Move (mxcsr, load (size_of_typ reg32_t) src); ] - | Fnstcw (dst) -> - let dst = match dst with - | Oaddr addr -> addr - | _ -> disfailwith "fnstcw argument cannot be non-memory" - in - [store reg16_t dst (Bil.Var fpu_ctrl); ] - | Fldcw (src) -> - let src = match src with - | Oaddr addr -> addr - | _ -> disfailwith "fldcw argument cannot be non-memory" - in - [ Bil.Move (fpu_ctrl, load (size_of_typ reg16_t) src); ] - | Fld _src -> - unimplemented "unsupported FPU register stack" - | Fst (_dst,_pop) -> - unimplemented "unsupported FPU flags" - | Cmps(Type.Imm _bits as t) -> - let t' = !!t in - let src1 = tmp t in - let src2 = tmp t in - let tmpres = tmp t in - let stmts = - Bil.Move (src1, op2e t (Oaddr rsi_e)) - :: Bil.Move (src2, op2e_s mode seg_es has_rex t (Oaddr rdi_e)) - :: Bil.Move (tmpres, Bil.(Var src1 - Var src2)) - :: string_incr mode t rsi - :: string_incr mode t rdi - :: set_flags_sub t' (Bil.Var src1) (Bil.Var src2) (Bil.Var tmpres) - in - begin match pref with + let undef reg = assn reg32_t reg (Bil.Unknown ("xgetbv", reg32_t)) in + List.map ~f:undef [ o_rax; o_rdx ] + | Stmxcsr dst -> + let dst = + match dst with + | Oaddr addr -> addr + | _ -> disfailwith "stmxcsr argument cannot be non-memory" + in + [ + store reg32_t dst (Bil.Var mxcsr); (*(Unknown ("stmxcsr", reg32_t));*) + ] + | Ldmxcsr src -> + let src = + match src with + | Oaddr addr -> addr + | _ -> disfailwith "ldmxcsr argument cannot be non-memory" + in + [ Bil.Move (mxcsr, load (size_of_typ reg32_t) src) ] + | Fnstcw dst -> + let dst = + match dst with + | Oaddr addr -> addr + | _ -> disfailwith "fnstcw argument cannot be non-memory" + in + [ store reg16_t dst (Bil.Var fpu_ctrl) ] + | Fldcw src -> + let src = + match src with + | Oaddr addr -> addr + | _ -> disfailwith "fldcw argument cannot be non-memory" + in + [ Bil.Move (fpu_ctrl, load (size_of_typ reg16_t) src) ] + | Fld _src -> unimplemented "unsupported FPU register stack" + | Fst (_dst, _pop) -> unimplemented "unsupported FPU flags" + | Cmps (Type.Imm _bits as t) -> + let t' = !!t in + let src1 = tmp t in + let src2 = tmp t in + let tmpres = tmp t in + let stmts = + Bil.Move (src1, op2e t (Oaddr rsi_e)) + :: Bil.Move (src2, op2e_s mode seg_es has_rex t (Oaddr rdi_e)) + :: Bil.Move (tmpres, Bil.(Var src1 - Var src2)) + :: string_incr mode t rsi :: string_incr mode t rdi + :: set_flags_sub t' (Bil.Var src1) (Bil.Var src2) (Bil.Var tmpres) + in + begin match pref with | [] -> stmts - | [single] when single = repz || single = repnz -> - rep_wrap ~mode ~check_zf:single ~addr ~next stmts - | _ -> unimplemented "unsupported flags in cmps" end - | Scas(Type.Imm _bits as t) -> - let t' = !!t in - let src1 = tmp t in - let src2 = tmp t in - let tmpres = tmp t in - let stmts = - let open Stmt in - Move (src1, Bil.(Cast (LOW, !!t, Var rax))) - :: Move (src2, op2e_s mode seg_es has_rex t (Oaddr rdi_e)) - :: Move (tmpres, Bil.(Var src1 - Var src2)) - :: string_incr mode t rdi - :: set_flags_sub t' (Bil.Var src1) (Bil.Var src2) (Bil.Var tmpres) - in - begin match pref with + | [ single ] when single = repz || single = repnz -> + rep_wrap ~mode ~check_zf:single ~addr ~next stmts + | _ -> unimplemented "unsupported flags in cmps" + end + | Scas (Type.Imm _bits as t) -> + let t' = !!t in + let src1 = tmp t in + let src2 = tmp t in + let tmpres = tmp t in + let stmts = + let open Stmt in + Move (src1, Bil.(Cast (LOW, !!t, Var rax))) + :: Move (src2, op2e_s mode seg_es has_rex t (Oaddr rdi_e)) + :: Move (tmpres, Bil.(Var src1 - Var src2)) + :: string_incr mode t rdi + :: set_flags_sub t' (Bil.Var src1) (Bil.Var src2) (Bil.Var tmpres) + in + begin match pref with | [] -> stmts - | [single] when single = repz || single = repnz -> - rep_wrap ~mode ~check_zf:single ~addr ~next stmts - | _ -> unimplemented "unsupported flags in scas" end - | Stos(Type.Imm _bits as t) -> - let stmts = [store_s mode seg_es t rdi_e (op2e t o_rax); - string_incr mode t rdi] - in - begin match pref with + | [ single ] when single = repz || single = repnz -> + rep_wrap ~mode ~check_zf:single ~addr ~next stmts + | _ -> unimplemented "unsupported flags in scas" + end + | Stos (Type.Imm _bits as t) -> + let stmts = + [ store_s mode seg_es t rdi_e (op2e t o_rax); string_incr mode t rdi ] + in + begin match pref with | [] -> stmts - | [single] when single = repz -> rep_wrap ~mode ~addr ~next stmts - | _ -> unimplemented "unsupported prefix for stos" end - | Push(t, o) -> - let o = if is_small_imm o t then sign_extend_imm o t - else op2e t o in - let tmp = tmp t in (* only really needed when o involves esp *) - Bil.Move (tmp, o) - :: Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width t)))) - :: store_s mode seg_ss t rsp_e (Bil.var tmp) (* FIXME: can ss be overridden? *) - :: [] - | Pop(t, o) -> - (* From the manual: + | [ single ] when single = repz -> rep_wrap ~mode ~addr ~next stmts + | _ -> unimplemented "unsupported prefix for stos" + end + | Push (t, o) -> + let o = if is_small_imm o t then sign_extend_imm o t else op2e t o in + let tmp = tmp t in + (* only really needed when o involves esp *) + [ + Bil.Move (tmp, o); + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width t)))); + store_s mode seg_ss t rsp_e (Bil.var tmp) + (* FIXME: can ss be overridden? *); + ] + | Pop (t, o) -> + (* From the manual: "The POP ESP instruction increments the stack pointer (ESP) before data at the old top of stack is written into the @@ -1295,131 +1502,145 @@ module ToIR = struct So, effectively there is no incrementation. *) - assn t o (load_s mode seg_ss (size_of_typ t) rsp_e) - :: if [%compare.equal: operand] o o_rsp then [] - else [Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width t))))] - | Pushf(t) -> - (* Note that we currently treat these fields as unknowns, but the + assn t o (load_s mode seg_ss (size_of_typ t) rsp_e) + :: + (if [%compare.equal: operand] o o_rsp then [] + else [ Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width t)))) ]) + | Pushf t -> + (* Note that we currently treat these fields as unknowns, but the manual says: When copying the entire EFLAGS register to the stack, the VM and RF flags (bits 16 and 17) are not copied; instead, the values for these flags are cleared in the EFLAGS image stored on the stack. *) - let flags_e = match t with - | Type.Imm 16 -> flags_e - | Type.Imm 32 -> eflags_e - | Type.Imm 64 -> rflags_e - | _ -> failwith "impossible" - in - Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width t)))) - :: store_s mode seg_ss t rsp_e flags_e - :: [] + let flags_e = + match t with + | Type.Imm 16 -> flags_e + | Type.Imm 32 -> eflags_e + | Type.Imm 64 -> rflags_e + | _ -> failwith "impossible" + in + [ + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width t)))); + store_s mode seg_ss t rsp_e flags_e; + ] | Popf t -> - let assnsf = match t with - | Type.Imm 16 -> assns_flags_to_bap - | Type.Imm 32 -> assns_eflags_to_bap - | Type.Imm 64 -> assns_rflags_to_bap - | _ -> failwith "impossible" - in - let tmp = tmp t in - let extractlist = - List.map - ~f:(fun i -> - Bil.(Extract (i, i, Var tmp))) - (List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive !!t 0) - in - Bil.Move (tmp, load_s mode seg_ss (size_of_typ t) rsp_e) - :: Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width t)))) - :: List.concat (List.map2_exn ~f:(fun f e -> f e) assnsf - extractlist) - | Popcnt(t, s, d) -> - let width = !!t in - let bits = op2e t s in - let res = tmp t in - let assn_src = Bil.(res := bits) in - let cnt = match width with - | 16 -> popcnt16 res - | 32 -> popcnt32 res - | 64 -> popcnt64 res - | _ -> disfailwith "Invalid popcnt width" in - let bil = (assn_src :: cnt) @ Bil.[assn t d (var res)] in - let flags = List.map ~f:(fun r -> - Bil.Move (r, int_exp 0 1)) [cf; oF; sf; af; pf] in - set_zf width bits :: (bil @ flags) + let assnsf = + match t with + | Type.Imm 16 -> assns_flags_to_bap + | Type.Imm 32 -> assns_eflags_to_bap + | Type.Imm 64 -> assns_rflags_to_bap + | _ -> failwith "impossible" + in + let tmp = tmp t in + let extractlist = + List.map + ~f:(fun i -> Bil.(Extract (i, i, Var tmp))) + (List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive !!t 0) + in + Bil.Move (tmp, load_s mode seg_ss (size_of_typ t) rsp_e) + :: Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width t)))) + :: List.concat (List.map2_exn ~f:(fun f e -> f e) assnsf extractlist) + | Popcnt (t, s, d) -> + let width = !!t in + let bits = op2e t s in + let res = tmp t in + let assn_src = Bil.(res := bits) in + let cnt = + match width with + | 16 -> popcnt16 res + | 32 -> popcnt32 res + | 64 -> popcnt64 res + | _ -> disfailwith "Invalid popcnt width" + in + let bil = (assn_src :: cnt) @ Bil.[ assn t d (var res) ] in + let flags = + List.map + ~f:(fun r -> Bil.Move (r, int_exp 0 1)) + [ cf; oF; sf; af; pf ] + in + set_zf width bits :: (bil @ flags) | Sahf -> - let assnsf = assns_lflags_to_bap in - let tah = tmp ~name:"AH" reg8_t in - let extractlist = - List.map - ~f:(fun i -> - Bil.(Extract (i, i, Var tah))) - (List.range ~stride:(-1) ~stop:`inclusive 7 0) - in - Bil.Move (tah, ah_e) - :: List.concat (List.map2_exn ~f:(fun f e -> f e) assnsf extractlist) + let assnsf = assns_lflags_to_bap in + let tah = tmp ~name:"AH" reg8_t in + let extractlist = + List.map + ~f:(fun i -> Bil.(Extract (i, i, Var tah))) + (List.range ~stride:(-1) ~stop:`inclusive 7 0) + in + Bil.Move (tah, ah_e) + :: List.concat (List.map2_exn ~f:(fun f e -> f e) assnsf extractlist) | Lahf -> - let o_ah = Oreg 4 in - [assn reg8_t o_ah lflags_e] - | Add(t, o1, o2) -> - let tmp = tmp t and tmp2 = tmp t in - Bil.Move (tmp, op2e t o1) - :: Bil.Move (tmp2, op2e t o2) - :: assn t o1 Bil.(op2e t o1 + Var tmp2) - :: let s1 = Bil.Var tmp in let s2 = Bil.Var tmp2 in let r = op2e t o1 in - set_flags_add !!t s1 s2 r - | Adc(t, o1, o2) -> - let orig1 = tmp t in - let orig2 = tmp t in - let bits = !!t in - let t' = Type.Imm (bits + 1) in - let c e = Bil.(Cast (UNSIGNED, !!t', e)) in - (* Literally compute the addition with an extra bit and see + let o_ah = Oreg 4 in + [ assn reg8_t o_ah lflags_e ] + | Add (t, o1, o2) -> + let tmp = tmp t and tmp2 = tmp t in + Bil.Move (tmp, op2e t o1) + :: Bil.Move (tmp2, op2e t o2) + :: assn t o1 Bil.(op2e t o1 + Var tmp2) + :: + (let s1 = Bil.Var tmp in + let s2 = Bil.Var tmp2 in + let r = op2e t o1 in + set_flags_add !!t s1 s2 r) + | Adc (t, o1, o2) -> + let orig1 = tmp t in + let orig2 = tmp t in + let bits = !!t in + let t' = Type.Imm (bits + 1) in + let c e = Bil.(Cast (UNSIGNED, !!t', e)) in + (* Literally compute the addition with an extra bit and see what the value is for CF *) - let s1 = Bil.Var orig1 in let s2 = Bil.Var orig2 in let r = op2e t o1 in - let bige = Bil.(c s1 + c s2 + c (Cast (UNSIGNED, !!t, cf_e))) in - Bil.Move (orig1, op2e t o1) - :: Bil.Move (orig2, op2e t o2) - :: assn t o1 Bil.(s1 + s2 + Cast (UNSIGNED, !!t, cf_e)) - :: Bil.Move (cf, Bil.Extract (bits, bits, bige)) - :: set_aopszf_add !!t s1 s2 r - | Inc(t, o) (* o = o + 1 *) -> - let t' = !!t in - let tmp = tmp t in - Bil.Move (tmp, op2e t o) - :: assn t o Bil.(op2e t o + int_exp 1 t') - :: set_aopszf_add t' (Bil.Var tmp) (int_exp 1 t') (op2e t o) - | Dec(t, o) (* o = o - 1 *) -> - let t' = !!t in - let tmp = tmp t in - Bil.Move (tmp, op2e t o) - :: assn t o Bil.(op2e t o - int_exp 1 t') - :: set_aopszf_sub t' (Bil.Var tmp) (int_exp 1 t') (op2e t o) (* CF is maintained *) - | Sub(t, o1, o2) (* o1 = o1 - o2 *) -> - let oldo1 = tmp t in - let oldo2 = tmp t in - let op1 = op2e t o1 in - let op2 = - if is_small_imm o2 t then sign_extend_imm o2 t - else op2e t o2 in - Bil.([ - oldo1 := op1; - oldo2 := op2; - assn t o1 (op1 - op2); - ] @ set_flags_sub (bitwidth_of_type t) (var oldo1) (var oldo2) op1) - | Sbb(t, o1, o2) -> - let tmp_s = tmp t in - let tmp_d = tmp t in - let orig_s = Bil.Var tmp_s in - let orig_d = Bil.Var tmp_d in - let sube = Bil.(orig_s + Cast (UNSIGNED, !!t, cf_e)) in - let d = op2e t o1 in - let s1 = - if is_small_imm o2 t then sign_extend_imm o2 t - else op2e t o2 in - Bil.Move (tmp_s, s1) - :: Bil.Move (tmp_d, d) - :: assn t o1 Bil.(orig_d - sube) - :: Bil.Move (oF, Bil.(Cast (HIGH, !!bool_t, (orig_s lxor orig_d) land (orig_d lxor d)))) - (* When src = 0xffffffff and cf=1, the processor sets CF=1. + let s1 = Bil.Var orig1 in + let s2 = Bil.Var orig2 in + let r = op2e t o1 in + let bige = Bil.(c s1 + c s2 + c (Cast (UNSIGNED, !!t, cf_e))) in + Bil.Move (orig1, op2e t o1) + :: Bil.Move (orig2, op2e t o2) + :: assn t o1 Bil.(s1 + s2 + Cast (UNSIGNED, !!t, cf_e)) + :: Bil.Move (cf, Bil.Extract (bits, bits, bige)) + :: set_aopszf_add !!t s1 s2 r + | Inc (t, o) (* o = o + 1 *) -> + let t' = !!t in + let tmp = tmp t in + Bil.Move (tmp, op2e t o) + :: assn t o Bil.(op2e t o + int_exp 1 t') + :: set_aopszf_add t' (Bil.Var tmp) (int_exp 1 t') (op2e t o) + | Dec (t, o) (* o = o - 1 *) -> + let t' = !!t in + let tmp = tmp t in + Bil.Move (tmp, op2e t o) + :: assn t o Bil.(op2e t o - int_exp 1 t') + :: set_aopszf_sub t' (Bil.Var tmp) (int_exp 1 t') (op2e t o) + (* CF is maintained *) + | Sub (t, o1, o2) (* o1 = o1 - o2 *) -> + let oldo1 = tmp t in + let oldo2 = tmp t in + let op1 = op2e t o1 in + let op2 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + Bil.( + [ oldo1 := op1; oldo2 := op2; assn t o1 (op1 - op2) ] + @ set_flags_sub (bitwidth_of_type t) (var oldo1) (var oldo2) op1) + | Sbb (t, o1, o2) -> + let tmp_s = tmp t in + let tmp_d = tmp t in + let orig_s = Bil.Var tmp_s in + let orig_d = Bil.Var tmp_d in + let sube = Bil.(orig_s + Cast (UNSIGNED, !!t, cf_e)) in + let d = op2e t o1 in + let s1 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + Bil.Move (tmp_s, s1) + :: Bil.Move (tmp_d, d) + :: assn t o1 Bil.(orig_d - sube) + :: Bil.Move + ( oF, + Bil.( + Cast (HIGH, !!bool_t, orig_s lxor orig_d land (orig_d lxor d))) + ) + (* When src = 0xffffffff and cf=1, the processor sets CF=1. Note that we compute dest = dest - (0xffffffff + 1) = 0, so the subtraction does not overflow. @@ -1430,262 +1651,288 @@ module ToIR = struct Maybe we should implement this by doing the actual computation, like we do for adc. *) - (* sub overflow | add overflow *) - :: Bil.Move (cf, Bil.((sube > orig_d) lor (sube < orig_s))) - :: set_apszf !!t orig_s orig_d d - | Cmp(t, o1, o2) -> - let tmp = tmp t in - Bil.Move (tmp, Bil.(op2e t o1 - op2e t o2)) - :: set_flags_sub !!t (op2e t o1) (op2e t o2) (Bil.Var tmp) - | Cmpxchg(t, src, dst) -> - let t' = !!t in - let eax_e = op2e t o_rax in - let dst_e = op2e t dst in - let src_e = op2e t src in - let tmp = tmp t in - Bil.Move (tmp, Bil.(eax_e - dst_e)) - :: set_flags_sub t' eax_e dst_e (Bil.Var tmp) - @ assn t dst (Bil.Ite (zf_e, src_e, dst_e)) - :: assn t o_rax (Bil.Ite (zf_e, eax_e, dst_e)) - :: [] - | Cmpxchg8b o -> (* only 32bit case *) - let accumulator = Bil.Concat((op2e reg32_t o_rdx),(op2e reg32_t o_rax)) in - let dst_e = op2e reg64_t o in - let src_e = Bil.Concat((op2e reg32_t o_rcx),(op2e reg32_t o_rbx)) in - let dst_low_e = Bil.Extract(63, 32, dst_e) in - let dst_hi_e = Bil.Extract(31, 0, dst_e) in - let eax_e = op2e reg32_t o_rax in - let edx_e = op2e reg32_t o_rdx in - let equal = tmp bool_t in - let equal_v = Bil.Var equal in - [ - Bil.Move (equal, Bil.(accumulator = dst_e)); - Bil.Move (zf, equal_v); - assn reg64_t o (Bil.Ite (equal_v, src_e, dst_e)); - assn reg32_t o_rax (Bil.Ite (equal_v, eax_e, dst_low_e)); - assn reg32_t o_rdx (Bil.Ite (equal_v, edx_e, dst_hi_e)) - ] - | Xadd(t, dst_op, src_op) -> - let tmp_res = tmp t in - let tmp_dst = tmp t in - let tmp_src = tmp t in - let dst = op2e t dst_op in - let src = op2e t src_op in - Bil.[ - tmp_src := src; - tmp_dst := dst; - tmp_res := src + dst; - assn t src_op dst; - assn t dst_op (var tmp_res); - ] @ set_flags_add !!t (Bil.var tmp_dst) (Bil.var tmp_src) dst; - | Xchg(t, src, dst) -> - let tmp = tmp t in - [ Bil.Move (tmp, op2e t src); - assn t src (op2e t dst); - assn t dst (Bil.Var tmp); ] - | And(t, o1, o2) -> - assn t o1 Bil.(op2e t o1 land op2e t o2) - :: Bil.Move (oF, exp_false) - :: Bil.Move (cf, exp_false) - :: Bil.Move (af, Bil.Unknown ("AF is undefined after and", bool_t)) - :: set_pszf t (op2e t o1) - | Or(t, o1, o2) -> - let o2 = - if is_small_imm o2 t then sign_extend_imm o2 t - else op2e t o2 in - assn t o1 Bil.(op2e t o1 lor o2) - :: Bil.Move (oF, exp_false) - :: Bil.Move (cf, exp_false) - :: Bil.Move (af, Bil.Unknown ("AF is undefined after or", bool_t)) - :: set_pszf t (op2e t o1) - | Xor(t, o1, o2) when [%compare.equal: operand] o1 o2 -> - assn t o1 Bil.(Int (BV.of_int ~width:(!!t) 0)) - :: Bil.Move (af, Bil.Unknown ("AF is undefined after xor", bool_t)) - :: List.map ~f:(fun v -> Bil.Move (v, exp_true)) [zf; pf] - @ List.map ~f:(fun v -> Bil.Move (v, exp_false)) [oF; cf; sf] - | Xor(t, o1, o2) -> - assn t o1 Bil.(op2e t o1 lxor op2e t o2) - :: Bil.Move (oF, exp_false) - :: Bil.Move (cf, exp_false) - :: Bil.Move (af, Bil.Unknown ("AF is undefined after xor", bool_t)) - :: set_pszf t (op2e t o1) - | Test(t, o1, o2) -> - let o2 = - if is_small_imm o2 t then sign_extend_imm o2 t - else op2e t o2 in - let tmp = tmp t in - Bil.Move (tmp, Bil.(op2e t o1 land o2)) - :: Bil.Move (oF, exp_false) - :: Bil.Move (cf, exp_false) - :: Bil.Move (af, Bil.Unknown ("AF is undefined after and", bool_t)) - :: set_pszf t (Bil.Var tmp) - | Ptest(t, o1, o2) -> - let open Stmt in - let t' = !!t in - let tmp1 = tmp t and tmp2 = tmp t in - Move (tmp1, Bil.(op2e t o2 land op2e t o1)) - :: Move (tmp2, Bil.(op2e t o2 land (exp_not (op2e t o1)))) - :: Move (af, exp_false) - :: Move (oF, exp_false) - :: Move (pf, exp_false) - :: Move (sf, exp_false) - :: Move (zf, Bil.(Var tmp1 = Int (BV.of_int ~width:t' 0))) - :: [Move (cf, Bil.(Var tmp2 = Int (BV.of_int ~width:t' 0)))] - | Not(t, o) -> - [assn t o (exp_not (op2e t o))] - | Neg(t, o) -> - let t' = !!t in - let tmp = tmp t in - let min_int = - Bil.BinOp (LSHIFT, int_exp 1 t', int_exp (t'-1) t') - in - Bil.Move (tmp, op2e t o) - ::assn t o Bil.(int_exp 0 t' - op2e t o) - ::Bil.Move (cf, Bil.(Ite (Var tmp = int_exp 0 t', int_exp 0 1, int_exp 1 1))) - ::Bil.Move (oF, Bil.(Ite (Var tmp = min_int, int_exp 1 1, int_exp 0 1))) - ::set_apszf_sub t' (Bil.Var tmp) (int_exp 0 t') (op2e t o) + (* sub overflow | add overflow *) + :: Bil.Move (cf, Bil.((sube > orig_d) lor (sube < orig_s))) + :: set_apszf !!t orig_s orig_d d + | Cmp (t, o1, o2) -> + let tmp = tmp t in + Bil.Move (tmp, Bil.(op2e t o1 - op2e t o2)) + :: set_flags_sub !!t (op2e t o1) (op2e t o2) (Bil.Var tmp) + | Cmpxchg (t, src, dst) -> + let t' = !!t in + let eax_e = op2e t o_rax in + let dst_e = op2e t dst in + let src_e = op2e t src in + let tmp = tmp t in + Bil.Move (tmp, Bil.(eax_e - dst_e)) + :: set_flags_sub t' eax_e dst_e (Bil.Var tmp) + @ [ + assn t dst (Bil.Ite (zf_e, src_e, dst_e)); + assn t o_rax (Bil.Ite (zf_e, eax_e, dst_e)); + ] + | Cmpxchg8b o -> + (* only 32bit case *) + let accumulator = Bil.Concat (op2e reg32_t o_rdx, op2e reg32_t o_rax) in + let dst_e = op2e reg64_t o in + let src_e = Bil.Concat (op2e reg32_t o_rcx, op2e reg32_t o_rbx) in + let dst_low_e = Bil.Extract (63, 32, dst_e) in + let dst_hi_e = Bil.Extract (31, 0, dst_e) in + let eax_e = op2e reg32_t o_rax in + let edx_e = op2e reg32_t o_rdx in + let equal = tmp bool_t in + let equal_v = Bil.Var equal in + [ + Bil.Move (equal, Bil.(accumulator = dst_e)); + Bil.Move (zf, equal_v); + assn reg64_t o (Bil.Ite (equal_v, src_e, dst_e)); + assn reg32_t o_rax (Bil.Ite (equal_v, eax_e, dst_low_e)); + assn reg32_t o_rdx (Bil.Ite (equal_v, edx_e, dst_hi_e)); + ] + | Xadd (t, dst_op, src_op) -> + let tmp_res = tmp t in + let tmp_dst = tmp t in + let tmp_src = tmp t in + let dst = op2e t dst_op in + let src = op2e t src_op in + Bil. + [ + tmp_src := src; + tmp_dst := dst; + tmp_res := src + dst; + assn t src_op dst; + assn t dst_op (var tmp_res); + ] + @ set_flags_add !!t (Bil.var tmp_dst) (Bil.var tmp_src) dst + | Xchg (t, src, dst) -> + let tmp = tmp t in + [ + Bil.Move (tmp, op2e t src); + assn t src (op2e t dst); + assn t dst (Bil.Var tmp); + ] + | And (t, o1, o2) -> + assn t o1 Bil.(op2e t o1 land op2e t o2) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after and", bool_t)) + :: set_pszf t (op2e t o1) + | Or (t, o1, o2) -> + let o2 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + assn t o1 Bil.(op2e t o1 lor o2) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after or", bool_t)) + :: set_pszf t (op2e t o1) + | Xor (t, o1, o2) when [%compare.equal: operand] o1 o2 -> + assn t o1 Bil.(Int (BV.of_int ~width:!!t 0)) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after xor", bool_t)) + :: List.map ~f:(fun v -> Bil.Move (v, exp_true)) [ zf; pf ] + @ List.map ~f:(fun v -> Bil.Move (v, exp_false)) [ oF; cf; sf ] + | Xor (t, o1, o2) -> + assn t o1 Bil.(op2e t o1 lxor op2e t o2) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after xor", bool_t)) + :: set_pszf t (op2e t o1) + | Test (t, o1, o2) -> + let o2 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + let tmp = tmp t in + Bil.Move (tmp, Bil.(op2e t o1 land o2)) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after and", bool_t)) + :: set_pszf t (Bil.Var tmp) + | Ptest (t, o1, o2) -> + let open Stmt in + let t' = !!t in + let tmp1 = tmp t and tmp2 = tmp t in + Move (tmp1, Bil.(op2e t o2 land op2e t o1)) + :: Move (tmp2, Bil.(op2e t o2 land exp_not (op2e t o1))) + :: Move (af, exp_false) + :: Move (oF, exp_false) + :: Move (pf, exp_false) + :: Move (sf, exp_false) + :: Move (zf, Bil.(Var tmp1 = Int (BV.of_int ~width:t' 0))) + :: [ Move (cf, Bil.(Var tmp2 = Int (BV.of_int ~width:t' 0))) ] + | Not (t, o) -> [ assn t o (exp_not (op2e t o)) ] + | Neg (t, o) -> + let t' = !!t in + let tmp = tmp t in + let min_int = Bil.BinOp (LSHIFT, int_exp 1 t', int_exp (t' - 1) t') in + Bil.Move (tmp, op2e t o) + :: assn t o Bil.(int_exp 0 t' - op2e t o) + :: Bil.Move + (cf, Bil.(Ite (Var tmp = int_exp 0 t', int_exp 0 1, int_exp 1 1))) + :: Bil.Move (oF, Bil.(Ite (Var tmp = min_int, int_exp 1 1, int_exp 0 1))) + :: set_apszf_sub t' (Bil.Var tmp) (int_exp 0 t') (op2e t o) | Mul (t, src) -> - (* Mul always multiplies EAX by src and stores the result in EDX:EAX + (* Mul always multiplies EAX by src and stores the result in EDX:EAX starting from the "right hand side" based on the type t of src *) - (* The OF and CF flags are set to 0 if the upper half of the result is 0; + (* The OF and CF flags are set to 0 if the upper half of the result is 0; otherwise, they are set to 1 *) - let new_t = Type.Imm (!!t * 2) in - let assnstmts, assne = Bil.(assn_dbl t ((Cast (UNSIGNED, !!new_t, op2e t o_rax)) * (Cast (UNSIGNED, !!new_t, op2e t src)))) - in - let flag = - let highbit = !!new_t - 1 in - let lowbit = !!new_t / 2 in - Bil.((Extract (highbit, lowbit, assne)) <> int_exp 0 !!t) - in - assnstmts - @ - [ - Bil.Move (oF, flag); - Bil.Move (cf, flag); - Bil.Move (sf, Bil.Unknown ("SF is undefined after Mul", bool_t)); - Bil.Move (zf, Bil.Unknown ("ZF is undefined after Mul", bool_t)); - Bil.Move (af, Bil.Unknown ("AF is undefined after Mul", bool_t)); - Bil.Move (pf, Bil.Unknown ("PF is undefined after Mul", bool_t)) - ] + let new_t = Type.Imm (!!t * 2) in + let assnstmts, assne = + Bil.( + assn_dbl t + (Cast (UNSIGNED, !!new_t, op2e t o_rax) + * Cast (UNSIGNED, !!new_t, op2e t src))) + in + let flag = + let highbit = !!new_t - 1 in + let lowbit = !!new_t / 2 in + Bil.(Extract (highbit, lowbit, assne) <> int_exp 0 !!t) + in + assnstmts + @ [ + Bil.Move (oF, flag); + Bil.Move (cf, flag); + Bil.Move (sf, Bil.Unknown ("SF is undefined after Mul", bool_t)); + Bil.Move (zf, Bil.Unknown ("ZF is undefined after Mul", bool_t)); + Bil.Move (af, Bil.Unknown ("AF is undefined after Mul", bool_t)); + Bil.Move (pf, Bil.Unknown ("PF is undefined after Mul", bool_t)); + ] | Imul (t, (oneopform, dst), src1, src2) -> - let new_t = Type.Imm (!!t * 2) in - let mul_stmts = - (match oneopform with - | true -> - (* For one operand form, use assn_double *) - let assnstmts, assne = - assn_dbl t Bil.((Cast (SIGNED, !!new_t, op2e t src1)) * (Cast (SIGNED, !!new_t, op2e t src2))) in - let flag = - (* Intel checks if EAX == EDX:EAX. Instead of doing this, we are just + let new_t = Type.Imm (!!t * 2) in + let mul_stmts = + match oneopform with + | true -> + (* For one operand form, use assn_double *) + let assnstmts, assne = + assn_dbl t + Bil.( + Cast (SIGNED, !!new_t, op2e t src1) + * Cast (SIGNED, !!new_t, op2e t src2)) + in + let flag = + (* Intel checks if EAX == EDX:EAX. Instead of doing this, we are just going to check if the upper bits are != 0 *) - let highbit = !!new_t - 1 in - let lowbit = !!new_t / 2 in - Bil.((Extract (highbit, lowbit, assne)) <> int_exp 0 !!t) - in - assnstmts @ - [Bil.Move (oF, flag); - Bil.Move (cf, flag)] - | false -> - (* Two and three operand forms *) - let tmp = tmp new_t in - (* Flag is set when the result is truncated *) - let flag = Bil.(Var tmp <> Cast (SIGNED, !!new_t, op2e t dst)) in - [(Bil.Move (tmp, Bil.((Cast (SIGNED, !!new_t, op2e t src1)) * (Cast (SIGNED, !!new_t, op2e t src2))))); - (assn t dst Bil.(Cast (LOW, !!t, Var tmp))); - Bil.Move (oF, flag); - Bil.Move (cf, flag)] ) - in - mul_stmts@[ - Bil.Move (pf, Bil.Unknown ("PF is undefined after imul", bool_t)); - Bil.Move (sf, Bil.Unknown ("SF is undefined after imul", bool_t)); - Bil.Move (zf, Bil.Unknown ("ZF is undefined after imul", bool_t)); - Bil.Move (af, Bil.Unknown ("AF is undefined after imul", bool_t));] - | Div(t, src) -> - let dt' = !!t * 2 in - let dt = Type.Imm dt' in - let zero = int_exp 0 dt' in - let dividend = tmp ~name:"dividend" dt in - let divisor = tmp ~name:"divisor" dt in - let tdiv = tmp ~name:"div" dt in - let trem = tmp ~name:"rem" dt in - let result = Bil.(cast low!!t (var trem) ^ cast low !!t (var tdiv)) in - let apply_result = fst (assn_dbl t result) in - Bil.[ - divisor := cast unsigned !!dt (op2e t src); - dividend := op2e_dbl t; - if_ (var divisor = zero) [ - Cpu_exceptions.divide_by_zero - ](* else *) [ - tdiv := var dividend / var divisor; - trem := var dividend mod var divisor; - if_ (cast high !!t (var tdiv) = int_exp 0 !!t) - apply_result (* else *) - [Cpu_exceptions.divide_by_zero] + let highbit = !!new_t - 1 in + let lowbit = !!new_t / 2 in + Bil.(Extract (highbit, lowbit, assne) <> int_exp 0 !!t) + in + assnstmts @ [ Bil.Move (oF, flag); Bil.Move (cf, flag) ] + | false -> + (* Two and three operand forms *) + let tmp = tmp new_t in + (* Flag is set when the result is truncated *) + let flag = Bil.(Var tmp <> Cast (SIGNED, !!new_t, op2e t dst)) in + [ + Bil.Move + ( tmp, + Bil.( + Cast (SIGNED, !!new_t, op2e t src1) + * Cast (SIGNED, !!new_t, op2e t src2)) ); + assn t dst Bil.(Cast (LOW, !!t, Var tmp)); + Bil.Move (oF, flag); + Bil.Move (cf, flag); + ] + in + mul_stmts + @ [ + Bil.Move (pf, Bil.Unknown ("PF is undefined after imul", bool_t)); + Bil.Move (sf, Bil.Unknown ("SF is undefined after imul", bool_t)); + Bil.Move (zf, Bil.Unknown ("ZF is undefined after imul", bool_t)); + Bil.Move (af, Bil.Unknown ("AF is undefined after imul", bool_t)); + ] + | Div (t, src) -> + let dt' = !!t * 2 in + let dt = Type.Imm dt' in + let zero = int_exp 0 dt' in + let dividend = tmp ~name:"dividend" dt in + let divisor = tmp ~name:"divisor" dt in + let tdiv = tmp ~name:"div" dt in + let trem = tmp ~name:"rem" dt in + let result = Bil.(cast low !!t (var trem) ^ cast low !!t (var tdiv)) in + let apply_result = fst (assn_dbl t result) in + Bil. + [ + divisor := cast unsigned !!dt (op2e t src); + dividend := op2e_dbl t; + if_ + (var divisor = zero) + [ Cpu_exceptions.divide_by_zero ] + (* else *) + [ + tdiv := var dividend / var divisor; + trem := var dividend mod var divisor; + if_ + (cast high !!t (var tdiv) = int_exp 0 !!t) + apply_result (* else *) + [ Cpu_exceptions.divide_by_zero ]; + ]; + ] + @ undefine [ cf; oF; sf; zf; af; pf ] + | Idiv (t, src) -> + let dt' = !!t * 2 in + let dt = Type.Imm dt' in + let zero = int_exp 0 dt' in + let dividend = tmp ~name:"dividend" dt in + let divisor = tmp ~name:"divisor" dt in + let tdiv = tmp ~name:"div" dt in + let trem = tmp ~name:"rem" dt in + let result = Bil.(cast low !!t (var trem) ^ cast low !!t (var tdiv)) in + let apply_result = fst @@ assn_dbl t result in + let lbound = + let dtm1 = dt' - 1 in + Word.(one dt' lsl of_int ~width:dt' dtm1) + in + let ubound = Word.(lbound - one dt') in + Bil. + [ + divisor := cast signed !!dt (op2e t src); + dividend := op2e_dbl t; + if_ + (var divisor = zero) + [ Cpu_exceptions.divide_by_zero ] + (* else *) + [ + tdiv := var dividend /$ var divisor; + trem := var dividend %$ var divisor; + if_ + ((var tdiv >$ int ubound) lor (var tdiv <$ int lbound)) + [ Cpu_exceptions.divide_by_zero ] (* else *) + apply_result; + ]; + ] + @ undefine [ cf; oF; sf; zf; af; pf ] + | Cld -> [ Bil.Move (df, exp_false) ] + | Leave t when List.is_empty pref -> + (* #UD if Lock prefix is used *) + Bil.Move (rsp, rbp_e) + :: to_ir mode addr next ss pref has_rex has_vex (Pop (t, o_rbp)) + | Interrupt3 -> [ Bil.CpuExn 3 ] + | Interrupt (Oimm i) -> + [ + (match Addr.to_int i with + | Ok i -> Bil.cpuexn i + | Error _ -> + let dst = asprintf "interrupt@%s" (Addr.string_of_value i) in + Bil.(encode call dst)); ] - ] @ undefine [cf; oF; sf; zf; af; pf] - | Idiv(t, src) -> - let dt' = !!t * 2 in - let dt = Type.Imm dt' in - let zero = int_exp 0 dt' in - let dividend = tmp ~name:"dividend" dt in - let divisor = tmp ~name:"divisor" dt in - let tdiv = tmp ~name:"div" dt in - let trem = tmp ~name:"rem" dt in - let result = Bil.(cast low !!t (var trem) ^ cast low !!t (var tdiv)) in - let apply_result = fst @@ assn_dbl t result in - let lbound = - let dtm1 = dt' - 1 in - Word.(one dt' lsl of_int ~width:dt' dtm1) in - let ubound = Word.(lbound - one dt') in - Bil.[ - divisor := cast signed !!dt (op2e t src); - dividend := op2e_dbl t; - if_ (var divisor = zero) [ - Cpu_exceptions.divide_by_zero - ] (* else *) [ - tdiv := var dividend /$ var divisor; - trem := var dividend %$ var divisor; - if_ ((var tdiv >$ int ubound) lor (var tdiv <$ int lbound)) [ - Cpu_exceptions.divide_by_zero; - ] (* else *) - apply_result; - ]; - ] @ undefine [cf; oF; sf; zf; af; pf] - | Cld -> - [Bil.Move (df, exp_false)] - | Leave t when List.is_empty pref -> (* #UD if Lock prefix is used *) - Bil.Move (rsp, rbp_e) - ::to_ir mode addr next ss pref has_rex has_vex (Pop(t, o_rbp)) - | Interrupt3 -> [Bil.CpuExn 3] - | Interrupt(Oimm i) -> [ - match Addr.to_int i with - | Ok i -> Bil.cpuexn i - | Error _ -> - let dst = asprintf "interrupt@%s" (Addr.string_of_value i) in - Bil.(encode call dst) - ] - | Sysenter | Syscall -> [ - Bil.(encode call "syscall") - ] + | Sysenter | Syscall -> [ Bil.(encode call "syscall") ] (* Match everything exhaustively *) - | Leave _ -> unimplemented "to_ir: Leave" - | Lea _ -> unimplemented "to_ir: Lea" - | Movs _ -> unimplemented "to_ir: Movs" - | Cmps _ -> unimplemented "to_ir: Cmps" - | Scas _ -> unimplemented "to_ir: Scas" - | Stos _ -> unimplemented "to_ir: Stos" - | Retn _ -> unimplemented "to_ir: Retn" - | Interrupt _ -> unimplemented "to_ir: Interrupt" - -end (* ToIR *) + | Leave _ -> unimplemented "to_ir: Leave" + | Lea _ -> unimplemented "to_ir: Lea" + | Movs _ -> unimplemented "to_ir: Movs" + | Cmps _ -> unimplemented "to_ir: Cmps" + | Scas _ -> unimplemented "to_ir: Scas" + | Stos _ -> unimplemented "to_ir: Stos" + | Retn _ -> unimplemented "to_ir: Retn" + | Interrupt _ -> unimplemented "to_ir: Interrupt" +end +(* ToIR *) let disasm_instr mode mem addr = let module D = X86_disasm in - let (pref, prefix, op, na) = D.parse_instr mode mem addr in + let pref, prefix, op, na = D.parse_instr mode mem addr in let has_rex = Option.is_some prefix.rex in let has_vex = Option.is_some prefix.vex in - let (ss, pref) = D.parse_prefixes mode pref op in + let ss, pref = D.parse_prefixes mode pref op in ToIR.to_ir mode addr na ss pref has_rex has_vex op let insn arch mem insn = @@ -1693,25 +1940,28 @@ let insn arch mem insn = let addr = Memory.min_addr mem in match disasm_instr mode mem addr with | exception No_semantics -> Ok [] - | exception Arch_exception (_,msg) -> - Or_error.errorf "invalid instruction: %s" msg + | exception Arch_exception (_, msg) -> + Or_error.errorf "invalid instruction: %s" msg | exception exn -> - Or_error.errorf "internal error in the legacy lifter: %s@\n%s@\n" - (Exn.to_string exn) - (Printexc.get_backtrace ()) - | bil -> match Type.check bil with - | Ok () -> Ok bil - | Error err -> - warning "BIL is not well-typed in the legacy lifter at %a - %a" - pp_insn (mem,insn) Type.Error.pp err; - Error (Error.of_string "type error") + Or_error.errorf "internal error in the legacy lifter: %s@\n%s@\n" + (Exn.to_string exn) + (Printexc.get_backtrace ()) + | bil -> ( + match Type.check bil with + | Ok () -> Ok bil + | Error err -> + warning "BIL is not well-typed in the legacy lifter at %a - %a" + pp_insn (mem, insn) Type.Error.pp err; + Error (Error.of_string "type error")) module AMD64 = struct module CPU = X86_cpu.AMD64 + let lift mem i = insn `x86_64 mem i end module IA32 = struct module CPU = X86_cpu.IA32 + let lift mem i = insn `x86 mem i end diff --git a/plugins/x86/x86_main.ml b/plugins/x86/x86_main.ml index 28cbc76ff..08c190398 100644 --- a/plugins/x86/x86_main.ml +++ b/plugins/x86/x86_main.ml @@ -1,95 +1,115 @@ -open Core_kernel[@@warning "-D"] +open Core_kernel [@@warning "-D"] open Bap_core_theory open Poly open Bap.Std open X86_targets -include Self() +open X86_sym_imm_targets +include Self () -type kind = Legacy | Modern | Merge [@@deriving equal] +type kind = Legacy | Modern | Merge | SymImm [@@deriving equal] let main backend kind abi = let abi = Option.map ~f:(Theory.Abi.read ~package:"bap") abi in X86_target.load ?abi ?backend (); let kind = if backend = Some "ghidra" then Modern else kind in - let ia32, amd64 = match kind with - | Legacy -> (module IA32L : Target), (module AMD64L : Target) - | Modern -> (module IA32 : Target), (module AMD64 : Target) - | Merge -> (module IA32M : Target), (module AMD64M : Target) in + let ia32, amd64 = + match kind with + | Legacy -> ((module IA32L : Target), (module AMD64L : Target)) + | Modern -> ((module IA32 : Target), (module AMD64 : Target)) + | Merge -> ((module IA32M : Target), (module AMD64M : Target)) + | SymImm -> ((module IA32SI_M : Target), (module AMD64SI_M : Target)) + in register_target `x86 ia32; register_target `x86_64 amd64 let () = - let () = Config.manpage [ - `S "SYNOPSIS"; - `P "$(b,bap) FILE [--x86-abi=ABI]"; - `P "$(b,bap) FILE [--x86-64-abi=ABI]"; - `S "DESCRIPTION"; - `P "Provides lifter and implements a set of ABI for x86 and - x86-64 architectures. No parameters are usually required. Once the - plugin is installed it will automatically provide it - services. However it is possible to override default abi, e.g., - when working with an executable compiled for MS Windows - platform. For a full set of supported ABI use corresponding list - option."; - `S "EXAMPLE"; - `P "To choose a correct ABI for a binary compiled for MS Windows - x64 target, use the following:"; - `P "$(b,bap) FILE --x86-64=ms"; - `S "SEE ALSO"; - `P "$(b,bap-x86-cpu)(3), $(b,bap-plugin-abi)(1), $(b,bap-plugin-arm)(1)" - ] in + let () = + Config.manpage + [ + `S "SYNOPSIS"; + `P "$(b,bap) FILE [--x86-abi=ABI]"; + `P "$(b,bap) FILE [--x86-64-abi=ABI]"; + `S "DESCRIPTION"; + `P + "Provides lifter and implements a set of ABI for x86 and\n\ + \ x86-64 architectures. No parameters are usually required. Once \ + the\n\ + \ plugin is installed it will automatically provide it\n\ + \ services. However it is possible to override default abi, e.g.,\n\ + \ when working with an executable compiled for MS Windows\n\ + \ platform. For a full set of supported ABI use corresponding list\n\ + \ option."; + `S "EXAMPLE"; + `P + "To choose a correct ABI for a binary compiled for MS Windows\n\ + \ x64 target, use the following:"; + `P "$(b,bap) FILE --x86-64=ms"; + `S "SEE ALSO"; + `P "$(b,bap-x86-cpu)(3), $(b,bap-plugin-abi)(1), $(b,bap-plugin-arm)(1)"; + ] + in let abi = let doc = "Override the ABI detection and use the selected ABI." in - Config.(param (some string) "abi" ~synonyms:["64-abi"] ~doc) in - let fp_lifter = Config.flag "with-floating-points" - ~doc:"DEPRECATED" in - let legacy_lifter = Config.flag "with-legacy-floating-points" - ~doc:"Enables the legacy floating-point lifter and \ - disables the intrinsic semantics of floating-point \ - operations" in + Config.(param (some string) "abi" ~synonyms:[ "64-abi" ] ~doc) + in + let fp_lifter = Config.flag "with-floating-points" ~doc:"DEPRECATED" in + let legacy_lifter = + Config.flag "with-legacy-floating-points" + ~doc: + "Enables the legacy floating-point lifter and disables the intrinsic \ + semantics of floating-point operations" + in let disable_intrinsics = Config.flag "disable-floating-point-intrinsics" - ~doc:"Disables translation of floating-point instructions \ - into calls to intrinsic functions." in - let backend = Config.param Config.(some string) "backend" - ~synonyms:["64-backend"] in + ~doc: + "Disables translation of floating-point instructions into calls to \ + intrinsic functions." + in + let backend = + Config.param Config.(some string) "backend" ~synonyms:[ "64-backend" ] + in let kind = - let kinds = ["legacy", Legacy; - "modern", Modern; - "merge", Merge] in + let kinds = + [ + ("legacy", Legacy); + ("modern", Modern); + ("merge", Merge); + ("sym-imm", SymImm); + ] + in let default = Merge in let doc = - sprintf "Debug purpose only. The $(docv) must be %s. Default: $(docv) = %s." + sprintf + "Debug purpose only. The $(docv) must be %s. Default: $(docv) = %s." (Config.doc_enum kinds) - (List.find_map_exn kinds - ~f:(fun (name, kind) -> - Option.some_if (equal_kind kind default) name)) in - Config.(param (enum kinds) "lifter" ~doc ~default) in - Config.declare_extension - ~doc:"provides x86/x86-64 semantics" - ~provides:["disassembler"; "lifter"; "semantics"; "x86"; "abi"] - @@ fun {Config.get=(!!)} -> + (List.find_map_exn kinds ~f:(fun (name, kind) -> + Option.some_if (equal_kind kind default) name)) + in + Config.(param (enum kinds) "lifter" ~doc ~default) + in + Config.declare_extension ~doc:"provides x86/x86-64 semantics" + ~provides:[ "disassembler"; "lifter"; "semantics"; "x86"; "abi" ] + @@ fun { Config.get = ( !! ) } -> let open Bap_core_theory in let open Bap_primus.Std in - main !!backend !!kind !!abi; if !!fp_lifter || !!legacy_lifter then begin let open Bap_core_theory in let open Bap_primus.Std in - if !!fp_lifter then Format.eprintf - "The --with-floating-points flag is deprecated \ - and will be removed in the following versions of bap. \ - This flag enables the legacy lifter that is incomplete \ - and disables the new version that translates \ - floating-point operations into the intrinsic calls. \ - If you still need the legacy lifter use the \ - --x86-with-legacy-floating-points option instead.@\n%!"; + if !!fp_lifter then + Format.eprintf + "The --with-floating-points flag is deprecated and will be removed in \ + the following versions of bap. This flag enables the legacy lifter \ + that is incomplete and disables the new version that translates \ + floating-point operations into the intrinsic calls. If you still need \ + the legacy lifter use the --x86-with-legacy-floating-points option \ + instead.@\n\ + %!"; X86_legacy_bil_lifter.init (); - X86_legacy_bil_semantics.init (); - end else if not !!disable_intrinsics - then + X86_legacy_bil_semantics.init () + end + else if not !!disable_intrinsics then KB.promise Primus.Lisp.Semantics.context @@ fun _ -> - KB.return @@ - Primus.Lisp.Context.create [ - "x86-floating-points", ["intrinsic-semantics"] - ] + KB.return + @@ Primus.Lisp.Context.create + [ ("x86-floating-points", [ "intrinsic-semantics" ]) ] diff --git a/plugins/x86/x86_sym_imm_lifter.ml b/plugins/x86/x86_sym_imm_lifter.ml new file mode 100644 index 000000000..695a480c3 --- /dev/null +++ b/plugins/x86/x86_sym_imm_lifter.ml @@ -0,0 +1,1967 @@ +(** Native lifter of x86 instructions to the BAP IL *) + +open Core_kernel [@@warning "-D"] +open Bap.Std +open Format +open Bil.Types +open X86_types +open X86_utils +open X86_env +include Self () + +module ToIR = struct + let cf_e = Bil.var cf + let pf_e = Bil.var pf + let af_e = Bil.var af + let zf_e = Bil.var zf + let sf_e = Bil.var sf + let of_e = Bil.var oF + let df_e = Bil.var df + + (** doubts here *) + let size_of_typ s = Size.of_int_exn !!s + + let undefine = + List.map ~f:(fun r -> Bil.(r := unknown "#undefined" (Var.typ r))) + + (* stmt helpers *) + + let store_s mode s t a e = + let mem = match mode with X86 -> R32.mem | X8664 -> R64.mem in + let sz = size_of_typ t in + match s with + | None -> Bil.Move (mem, Bil.(Store (Var mem, a, e, LittleEndian, sz))) + | Some v -> + Bil.Move (mem, Bil.(Store (Var mem, Var v + a, e, LittleEndian, sz))) + + (* copypasted from op2e_s below, but keeps the opcode width *) + let op2e_s_keep_width mode ss has_rex t operand = + let ( = ) = Type.equal in + match operand with + | Ovec r when t = reg256_t -> (bits2ymme mode r, t) + | Ovec r when t = reg128_t -> (bits2ymm128e mode r, t) + | Ovec r when t = reg64_t -> (bits2ymm64e mode r, t) + | Ovec r when t = reg32_t -> (bits2ymm32e mode r, t) + | Ovec _ -> + let i = match t with Type.Imm n -> ": " ^ string_of_int n | _ -> "" in + disfailwith mode ("invalid SIMD register size for op2e" ^ i) + | Oreg r when t = reg64_t -> (bits2reg64e mode r, t) + | Oreg r when t = reg32_t -> (bits2reg32e mode r, t) + | Oreg r when t = reg16_t -> (bits2reg16e mode r, t) + | Oreg r when t = reg8_t -> (bits2reg8e mode ~has_rex r, t) + | Oreg _ -> unimplemented mode "unknown register" + | Oseg r when t = reg64_t -> + Bil.(Cast (UNSIGNED, !!reg64_t, bits2segrege r), t) + (* There is no 32-bit extension of segment selectors; this is not a bug *) + | Oseg r when t = reg16_t -> (bits2segrege r, t) + | Oseg _ -> (disfailwith mode "Segment register when t is not r16", t) + | Oaddr e -> (load_s mode ss (size_of_typ t) e, t) + | Oimm i -> Bil.(Var (Var.create ~is_virtual:true "IMM" t), t) + + let op2e_s mode ss has_rex t operand = + let ( = ) = Type.equal in + match operand with + | Ovec r when t = reg256_t -> bits2ymme mode r + | Ovec r when t = reg128_t -> bits2ymm128e mode r + | Ovec r when t = reg64_t -> bits2ymm64e mode r + | Ovec r when t = reg32_t -> bits2ymm32e mode r + | Ovec _ -> + let i = match t with Type.Imm n -> ": " ^ string_of_int n | _ -> "" in + disfailwith mode ("invalid SIMD register size for op2e" ^ i) + | Oreg r when t = reg64_t -> bits2reg64e mode r + | Oreg r when t = reg32_t -> bits2reg32e mode r + | Oreg r when t = reg16_t -> bits2reg16e mode r + | Oreg r when t = reg8_t -> bits2reg8e mode ~has_rex r + | Oreg _ -> unimplemented mode "unknown register" + | Oseg r when t = reg64_t -> + Bil.(Cast (UNSIGNED, !!reg64_t, bits2segrege r)) + (* There is no 32-bit extension of segment selectors; this is not a bug *) + | Oseg r when t = reg16_t -> bits2segrege r + | Oseg _ -> disfailwith mode "Segment register when t is not r16" + | Oaddr e -> load_s mode ss (size_of_typ t) e + | Oimm i -> Bil.(Var (Var.create ~is_virtual:true "IMM" t)) + + let assn_s mode s has_rex has_vex t v e = + (* Assign to some bits of v, starting at bit off, while preserving the other bits *) + let sub_assn ?(off = 0) t v e = + let concat_exps = ref [] in + let bits = !!(Var.typ v) in + let assnbits = !!t in + + (* Add the upper preserved bits, if any *) + let ubh = bits - 1 and ubl = assnbits + off in + if ubh > ubl then + concat_exps := Bil.(Extract (ubh, ubl, Var v)) :: !concat_exps; + + (* Add e *) + concat_exps := e :: !concat_exps; + + (* Add the lower preserved bits, if any *) + let lbh = off - 1 and lbl = 0 in + if lbh > lbl then + concat_exps := Bil.(Extract (lbh, lbl, Var v)) :: !concat_exps; + + let final_e = + List.reduce_exn ~f:(fun big_e e -> Bil.Concat (e, big_e)) !concat_exps + in + Bil.Move (v, final_e) + in + let is8664 = [%compare.equal: mode] mode X8664 in + match (v, t) with + (* Zero-extend 128-bit assignments to 256-bit ymms. *) + | Ovec r, Type.Imm (128 | 64 | 32) when has_vex -> + let v = bits2ymm mode r in + sub_assn reg256_t v Bil.(Cast (UNSIGNED, !!reg256_t, e)) + | Ovec r, Type.Imm (256 | 128 | 64 | 32) -> + let v = bits2ymm mode r in + sub_assn t v e + | Ovec _, _ -> disfailwith mode "invalid SIMD register size for assignment" + (* Zero-extend 32-bit assignments to 64-bit registers. *) + | Oreg r, Type.Imm 32 when is8664 -> + let v = bits2genreg mode r in + sub_assn reg64_t v Bil.(Cast (UNSIGNED, !!reg64_t, e)) + | Oreg r, Type.Imm (64 | 32 | 16) -> + let v = bits2genreg mode r in + sub_assn t v e + | Oreg r, Type.Imm 8 + when r < 4 || ([%compare.equal: mode] mode X8664 && has_rex) -> + let v = bits2genreg mode r in + sub_assn t v e + | Oreg r, Type.Imm 8 -> + let v = bits2genreg mode (r land 3) in + sub_assn ~off:8 t v e + | Oreg _, _ -> unimplemented mode "assignment to sub registers" + | Oseg r, _ when Type.equal t reg16_t -> + let v = bits2segreg r in + Bil.Move (v, e) + | Oseg _, _ -> + disfailwith mode "Can't assign to non 16 bit segment register" + | Oaddr a, _ -> store_s mode s t a e + | Oimm _, _ -> + disfailwith mode "disasm x86: Can't assign to an immediate value" + + (* Double width operands, as used by multiplication and division *) + let op_dbl t = + let open Type in + match t with + | Imm 8 -> [ (reg16_t, o_rax) ] + | Imm 16 -> [ (reg16_t, o_rdx); (reg16_t, o_rax) ] + | Imm 32 -> [ (reg32_t, o_rdx); (reg32_t, o_rax) ] + | Imm 64 -> [ (reg64_t, o_rdx); (reg64_t, o_rax) ] + | _ -> disfailwith X86 "op_dbl only defined for Reg 8, 16, 32, and 64" + + (* Return an expression for a double-width operand, as used by the div + instruction. *) + let op2e_dbl_s mode ss has_rex t = + let cf (ct, o) = op2e_s mode ss has_rex ct o in + let ol = List.map ~f:cf (op_dbl t) in + List.reduce_exn ~f:(fun bige little -> Bil.(bige ^ little)) ol + + (* Double width assignments, as used by multiplication *) + let assn_dbl_s mode s has_rex has_vex t e = + match op_dbl t with + | (t, o) :: [] -> + ([ assn_s mode s has_rex has_vex t o e ], op2e_s mode s has_rex t o) + | l -> + let tmp = tmp (Type.Imm (!!t * 2)) in + let f (stmts, off) (ct, o) = + let newoff = off + !!ct in + ( assn_s mode s has_rex has_vex ct o + (Bil.Extract (newoff - 1, off, Bil.Var tmp)) + :: stmts, + newoff ) + in + ( List.rev + (fst + (List.fold_left ~f ~init:([ Bil.Move (tmp, e) ], 0) (List.rev l))), + Bil.Var tmp ) + + (* A function for computing the target of jumps. *) + let compute_jump_target mode s has_rex = + let t = type_of_mode mode in + function + | Jabs o -> op2e_s mode s has_rex t o + | Jrel (na, offset) -> + (*let i,t = Arithmetic.binop PLUS (na,t) (offset,t) in*) + Bil.(Int na + Int offset) + + let jump_target = compute_jump_target + + let string_incr mode t v = + let i n = Bil.Int (int_of_mode mode n) in + if Type.equal t reg8_t then + Bil.Move (v, Bil.(Var v + df_to_offset mode df_e)) + else + Bil.Move (v, Bil.(Var v + (df_to_offset mode df_e * i (bytes_of_width t)))) + + let rep_wrap ?check_zf ~mode ~addr:_ ~next:_ stmts = + let extend = big_int_of_mode mode in + let zero = extend Word.b0 and one = extend Word.b1 in + let rcx = match mode with X86 -> R32.rcx | X8664 -> R64.rcx in + let flag = tmp bool_t in + let cond = Bil.((var rcx <> int zero) land var flag) in + let head = Bil.(flag := int Word.b1) in + let tail = + Bil.(rcx := var rcx - int one) + :: + (match check_zf with + | None -> [] + | Some x when x = repz -> Bil.[ flag := zf_e ] + | Some x when x = repnz -> Bil.[ flag := lnot zf_e ] + | _ -> failwith "invalid value for ?check_zf") + in + Bil.[ head; while_ cond (stmts @ tail) ] + + let compute_sf result = Bil.(Cast (HIGH, !!bool_t, result)) + + let compute_zf t result = + let bi0 = BV.of_int ~width:t 0 in + Bil.(Int bi0 = result) + + let compute_pf t r = + let acc = tmp t in + let var_acc = Bil.Var acc in + let t' = !!t in + (* extra parens do not change semantics but do make it pretty + print nicer *) + let open Bil in + exp_not + (Cast + ( LOW, + !!bool_t, + Let + ( acc, + (r lsr int_exp 4 t') lxor r, + Let + ( acc, + (var_acc lsr int_exp 2 t') lxor var_acc, + (var_acc lsr int_exp 1 t') lxor var_acc ) ) )) + + let set_sf r = Bil.Move (sf, compute_sf r) + let set_zf t r = Bil.Move (zf, compute_zf t r) + let set_pf t r = Bil.Move (pf, compute_pf t r) + + let set_pszf t r = + let t' = !!t in + [ set_pf t r; set_sf r; set_zf t' r ] + + (* Adjust flag + + AF is set when there is a carry to or borrow from bit 4 (starting + at 0), when considering unsigned operands. Let X_i denote bit i of + value X. Note that in addition, r_4 = c + [(op1_4 + op2_4) mod 2], + where c is the carry bit from the lower four bits. Since AF = c, + and we want to know the value of AF, we can rewrite as AF = c = r_4 + - [(op1_4 + op2_4) mod 2]. Noting that addition and subtraction mod + 2 is just xor, we can simplify to AF = r_4 xor op1_4 xor op2_4. + *) + + let set_apszf t s1 s2 r = + let bit4 = int_exp (1 lsl 4) t in + let t = Type.Imm t in + Bil.Move (af, Bil.(bit4 = bit4 land (r lxor s1 lxor s2))) :: set_pszf t r + + (* Helper functions to set flags for adding *) + let set_aopszf_add t s1 s2 r = + (* Move (oF, Bop.(Cast (CAST_HIGH, r1, (s1 = s2) land (s1 lxor r)))) *) + let s1_high = Bil.(Cast (HIGH, !!bool_t, s1)) in + let s2_high = Bil.(Cast (HIGH, !!bool_t, s2)) in + let r_high = Bil.(Cast (HIGH, !!bool_t, r)) in + Bil.Move (oF, Bil.((s1_high = s2_high) land (s1_high lxor r_high))) + :: set_apszf t s1 s2 r + + let set_flags_add t s1 s2 r = + Bil.Move (cf, Bil.(r < s1)) :: set_aopszf_add t s1 s2 r + + (* Helper functions to set flags for subtracting *) + let set_apszf_sub t s1 s2 r = set_apszf t s1 s2 r + + let set_aopszf_sub t s1 s2 r = + Bil.Move (oF, Bil.(Cast (HIGH, !!bool_t, s1 lxor s2 land (s1 lxor r)))) + :: set_apszf_sub t s1 s2 r + + let set_flags_sub t s1 s2 r = + Bil.Move (cf, Bil.(s2 > s1)) :: set_aopszf_sub t s1 s2 r + + let popcount x ~one ~two ~four ~sh ~m1 ~m2 ~m4 ~h01 = + Bil. + [ + x := var x - ((var x lsr int one) land int m1); + x := (var x land int m2) + ((var x lsr int two) land int m2); + x := (var x + (var x lsr int four)) land int m4; + x := (var x * int h01) lsr int sh; + ] + + let popcnt16 x = + let one = Word.one 16 in + let two = Word.succ one in + let four = Word.of_int ~width:16 4 in + let sh = Word.of_int ~width:16 8 in + let m1 = Word.of_int ~width:16 0x5555 in + let m2 = Word.of_int ~width:16 0x3333 in + let m4 = Word.of_int ~width:16 0x0f0f in + let h01 = Word.of_int ~width:16 0x0101 in + popcount x ~one ~two ~four ~sh ~m1 ~m2 ~m4 ~h01 + + let popcnt32 x = + let one = Word.one 32 in + let two = Word.succ one in + let four = Word.of_int ~width:32 4 in + let sh = Word.of_int ~width:32 24 in + let m1 = Word.of_int ~width:32 0x55555555 in + let m2 = Word.of_int ~width:32 0x33333333 in + let m4 = Word.of_int ~width:32 0x0f0f0f0f in + let h01 = Word.of_int ~width:32 0x01010101 in + popcount x ~one ~two ~four ~sh ~m1 ~m2 ~m4 ~h01 + + let popcnt64 x = + let one = Word.one 64 in + let two = Word.succ one in + let four = Word.of_int ~width:64 4 in + let sh = Word.of_int ~width:64 56 in + let m1 = Word.of_int64 ~width:64 0x5555555555555555L in + let m2 = Word.of_int64 ~width:64 0x3333333333333333L in + let m4 = Word.of_int64 ~width:64 0x0f0f0f0f0f0f0f0fL in + let h01 = Word.of_int64 ~width:64 0x0101010101010101L in + popcount x ~one ~two ~four ~sh ~m1 ~m2 ~m4 ~h01 + + let clz16 x = + Bil. + [ + x := var x lor (var x lsr int Word.(one 16)); + x := var x lor (var x lsr int Word.(of_int 2 ~width:16)); + x := var x lor (var x lsr int Word.(of_int 4 ~width:16)); + x := var x lor (var x lsr int Word.(of_int 8 ~width:16)); + x := lnot (var x); + ] + @ popcnt16 x + + let clz32 x = + Bil. + [ + x := var x lor (var x lsr int Word.(one 32)); + x := var x lor (var x lsr int Word.(of_int 2 ~width:32)); + x := var x lor (var x lsr int Word.(of_int 4 ~width:32)); + x := var x lor (var x lsr int Word.(of_int 8 ~width:32)); + x := var x lor (var x lsr int Word.(of_int 16 ~width:32)); + x := lnot (var x); + ] + @ popcnt32 x + + let clz64 x = + Bil. + [ + x := var x lor (var x lsr int Word.(one 64)); + x := var x lor (var x lsr int Word.(of_int 2 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 4 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 8 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 16 ~width:64)); + x := var x lor (var x lsr int Word.(of_int 32 ~width:64)); + x := lnot (var x); + ] + @ popcnt64 x + + let ctz16 x = + Bil.(x := (var x land unop NEG (var x)) - int Word.(one 16)) :: popcnt16 x + + let ctz32 x = + Bil.(x := (var x land unop NEG (var x)) - int Word.(one 32)) :: popcnt32 x + + let ctz64 x = + Bil.(x := (var x land unop NEG (var x)) - int Word.(one 64)) :: popcnt64 x + + let bitscan_flags is_zero_count = + let l = + Bil. + [ + oF := unknown "bits" bool_t; + sf := unknown "bits" bool_t; + af := unknown "bits" bool_t; + pf := unknown "bits" bool_t; + ] + in + if is_zero_count then l else Bil.(cf := unknown "bits" bool_t) :: l + + let rec to_ir mode addr next ss pref has_rex has_vex = + let module R = (val vars_of_mode mode) in + let open R in + let load = load_s mode ss in + (* Need to change this if we want seg_ds <> None *) + let op2e = op2e_s mode ss has_rex in + let op2e_keep_width = op2e_s_keep_width mode ss has_rex in + let op2e_dbl = op2e_dbl_s mode ss has_rex in + let store = store_s mode ss in + let assn = assn_s mode ss has_rex has_vex in + let assn_dbl = assn_dbl_s mode ss has_rex has_vex in + let mi = int_of_mode mode in + let mt = type_of_mode mode in + let rbp_e = Bil.var rbp in + let rsp_e = Bil.var rsp in + let rsi_e = Bil.var rsi in + let rdi_e = Bil.var rdi in + let rax_e = Bil.var rax in + let rdx_e = Bil.var rdx in + let ah_e = ah_e mode in + let disfailwith = disfailwith mode in + let unimplemented = unimplemented mode in + let is_small_imm op t = + match op with + | Oimm imm -> Word.bitwidth imm < bitwidth_of_type t + | _ -> false + in + let sign_extend_imm op t = + let op_typ = + match op with + | Oimm imm -> Type.imm (Word.bitwidth imm) + | _ -> disfailwith "imm operand expected" + in + Bil.(cast signed (bitwidth_of_type t) (op2e op_typ op)) + in + let is_repz = function [ x ] -> x = repz | _ -> false in + let is_repnz = function [ x ] -> x = repnz | _ -> false in + function + | Nop -> [] + | Bswap (t, op) -> + let e = + match t with + | Type.Imm 32 | Type.Imm 64 -> + let op', t' = op2e_keep_width t op in + reverse_bytes op' t' + | _ -> disfailwith "bswap: Expected 32 or 64 bit type" + in + [ assn t op e ] + | Retn (op, far_ret) + when List.is_empty pref || is_repz pref || is_repnz pref -> + let temp = tmp mt in + let load_stmt = + if far_ret then (* TODO Mess with segment selectors here *) + unimplemented "long retn not supported" + else Bil.Move (temp, load_s mode seg_ss (size_of_typ mt) rsp_e) + in + let rsp_stmts = + Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width mt)))) + :: + (match op with + | None -> [] + | Some (t, src) -> [ Bil.Move (rsp, Bil.(rsp_e + op2e t src)) ]) + in + (load_stmt :: rsp_stmts) @ [ Bil.Jmp (Bil.Var temp) ] + | Mov (t, dst, src, condition) -> + let c_src = + match condition with + | None -> op2e t src + | Some c -> Bil.Ite (c, op2e t src, op2e t dst) + in + (* Find base by looking at LDT or GDT *) + let base_e e = + (* 0 = GDT, 1 = LDT *) + let ti = Bil.Extract (3, 3, e) in + let base = Bil.Ite (ti, Bil.var ldt, Bil.var gdt) in + (* Extract index into table *) + let entry_size, entry_shift = + match mode with + | X86 -> (reg64_t, 6 (* "1<<6 = 64" *)) + | X8664 -> (reg128_t, 7 (* "1<<7 = 128" *)) + in + let index = + Bil.( + Cast (UNSIGNED, !!mt, Extract (15, 4, e) lsl Int (mi entry_shift))) + in + (* Load the table entry *) + let table_entry = + load_s mode None (size_of_typ entry_size) Bil.(base + index) + in + (* Extract the base *) + concat_explist + ((match mode with + | X86 -> [] + | X8664 -> Bil.Extract (95, 64, table_entry) :: []) + @ [ + Bil.Extract (63, 56, table_entry); + Bil.Extract (39, 32, table_entry); + Bil.Extract (31, 16, table_entry); + ]) + in + let bs = + let dst_e = op2e t dst in + if [%compare.equal: operand] dst o_fs && !compute_segment_bases then + [ Bil.Move (fs_base, base_e dst_e) ] + else if [%compare.equal: operand] dst o_gs && !compute_segment_bases + then [ Bil.Move (gs_base, base_e dst_e) ] + else [] + in + assn t dst c_src :: bs + | Movs (Type.Imm _bits as t) -> + let stmts = + [ + store_s mode seg_es t rdi_e + (load_s mode seg_es (size_of_typ t) rsi_e); + string_incr mode t rsi; + string_incr mode t rdi; + ] + in + if List.is_empty pref then stmts + else if ints_mem pref repz || ints_mem pref repnz then + (* movs has only rep instruction others just considered to be rep *) + rep_wrap ~mode ~addr ~next stmts + else unimplemented "unsupported prefix for movs" + | Movzx (t, dst, ts, src) -> + [ assn t dst Bil.(Cast (UNSIGNED, !!t, op2e ts src)) ] + | Movsx (t, dst, ts, src) -> + [ assn t dst Bil.(Cast (SIGNED, !!t, op2e ts src)) ] + | Movdq (ts, s, td, d, align) -> + let s, al = + match s with + | Ovec _ | Oreg _ -> (op2e ts s, []) + | Oaddr a -> (op2e ts s, [ a ]) + | Oimm _ | Oseg _ -> disfailwith "invalid source operand for movdq" + in + let d, al = + match d with + (* Behavior is to clear the xmm bits *) + | Ovec _ -> (assn td d Bil.(Cast (UNSIGNED, !!td, s)), al) + | Oreg _ -> (assn td d s, al) + | Oaddr a -> (assn td d s, a :: al) + | Oimm _ | Oseg _ -> disfailwith "invalid dest operand for movdq" + in + (* sources tell me that movdqa raises a general protection exception + * if its operands aren't aligned on a 16-byte boundary *) + let im i = Bil.Int (int_of_mode mode i) in + let al = + if align then + List.map + ~f:(fun a -> + Bil.If + ( Bil.(a land im 15 = im 0), + [], + [ Cpu_exceptions.general_protection ] )) + al + else [] + in + d :: al + | Movoffset ((tdst, dst), offsets) -> + (* If a vex prefix is present, then extra space is filled with 0. + Otherwise, the bits are preserved. *) + let padding hi lo = + if hi < lo then [] + else if has_vex then [ int_exp 0 (hi - lo + 1) ] + else [ Bil.Extract (hi, lo, op2e tdst dst) ] + in + let offsets = + List.sort + ~compare:(fun { offdstoffset = o1; _ } { offdstoffset = o2; _ } -> + Int.compare o1 o2) + offsets + in + let add_exp (elist, nextbit) + { offlen; offtyp; offop; offsrcoffset; offdstoffset } = + ( Bil.Extract + (!!offlen + offsrcoffset - 1, offsrcoffset, op2e offtyp offop) + :: padding (offdstoffset - 1) nextbit + @ elist, + offdstoffset + !!offlen ) + in + let elist, nextbit = List.fold_left ~f:add_exp ~init:([], 0) offsets in + let elist = padding (!!tdst - 1) nextbit @ elist in + [ assn tdst dst (concat_explist elist) ] + | Punpck (t, et, o, d, s, vs) -> + let nelem = + match (t, et) with + | Type.Imm n, Type.Imm n' -> n / n' + | _ -> disfailwith "invalid" + in + assert (nelem mod 2 = 0); + let nelem_per_src = nelem / 2 in + let halft = Type.Imm (!!t / 2) in + let castf = + match o with + | High -> fun e -> Bil.(Cast (HIGH, !!halft, e)) + | Low -> fun e -> Bil.(Cast (LOW, !!halft, e)) + in + let se, de = (castf (op2e t s), castf (op2e t d)) in + let st, dt = (tmp halft, tmp halft) in + let et' = !!et in + let mape i = + [ + extract_element et' (Bil.Var st) i; + extract_element et' (Bil.Var dt) i; + ] + in + let e = + concat_explist + (List.concat + (List.map ~f:mape + (List.range ~stride:(-1) ~stop:`inclusive (nelem_per_src - 1) + 0))) + in + let dest = match vs with None -> d | Some vdst -> vdst in + [ Bil.Move (st, se); Bil.Move (dt, de); assn t dest e ] + | Ppackedbinop (t, et, fbop, _, d, s, vs) -> + let t_width = bitwidth_of_type t in + let e_width = bitwidth_of_type et in + let nops = t_width / e_width in + let byte = 8 in + let tmp_dst = tmp t in + let vdst = Option.value ~default:d vs in + let iv = tmp (Type.imm byte) in + let elt = tmp et in + let zero = Word.zero t_width in + let bits = Word.of_int ~width:byte e_width in + + let foreach_size f = List.concat @@ List.init nops ~f in + let getelement o i = + (* assumption: immediate operands are repeated for all vector + elements *) + match o with + | Oimm _ -> op2e et o + | _ -> extract_element !!et (op2e t o) i + in + + List.concat + Bil. + [ + [ tmp_dst := int zero ]; + foreach_size (fun i -> + [ + elt := fbop (getelement d i) (getelement s i); + iv := int @@ Word.of_int ~width:byte i; + tmp_dst := + var tmp_dst + lor cast unsigned t_width (var elt) + lsl (var iv * int bits); + ]); + [ assn t vdst (var tmp_dst) ]; + ] + | Pbinop (t, fbop, _s, o1, o2, vop) -> ( + match vop with + | None -> [ assn t o1 (fbop (op2e t o1) (op2e t o2)) ] + | Some vop -> [ assn t o1 (fbop (op2e t vop) (op2e t o2)) ]) + | Pcmp (t, elet, bop, _, dst, src, vsrc) -> + let elebits = bitwidth_of_type elet in + let t_width = bitwidth_of_type t in + let ncmps = t_width / elebits in + let src = + match src with + | Ovec _ -> op2e t src + | Oaddr a -> load (size_of_typ t) a + | Oreg _ | Oimm _ | Oseg _ -> disfailwith "invalid" + in + let vsrc = Option.value ~default:dst vsrc in + let byte = 8 in + let tmp_dst = tmp t in + let iv = tmp (Type.imm byte) in + let elt = tmp elet in + let elt_1 = tmp elet in + let elt_2 = tmp elet in + let _one = Word.of_int ~width:elebits (-1) in + let zero = Word.zero elebits in + let bits = Word.of_int ~width:byte elebits in + let zero_long = Word.zero t_width in + let foreach_size f = + let sizes = + List.init ncmps ~f:(fun i -> + let left_bit = i * elebits in + let right_bit = ((i + 1) * elebits) - 1 in + let i = Word.of_int ~width:byte i in + (i, left_bit, right_bit)) + in + List.concat @@ List.map sizes ~f + in + + List.concat + Bil. + [ + [ tmp_dst := int zero_long ]; + foreach_size (fun (i, left_bit, right_bit) -> + [ + elt_1 := extract right_bit left_bit src; + elt_2 := extract right_bit left_bit (op2e t vsrc); + iv := int i; + if_ + (binop bop (var elt_1) (var elt_2)) + [ elt := int _one ] + [ elt := int zero ]; + tmp_dst := + var tmp_dst + lor cast unsigned t_width (var elt) + lsl (var iv * int bits); + ]); + [ assn t dst (var tmp_dst) ]; + ] + | Pmov (t, dstet, srcet, dst, src, ext, _) -> + let nelem = + match (t, dstet) with + | Type.Imm n, Type.Imm n' -> n / n' + | _ -> disfailwith "invalid" + in + let getelt op i = extract_element !!srcet (op2e t op) i in + let extcast = + let open Exp in + match ext with + | UNSIGNED | SIGNED -> fun e -> Bil.Cast (ext, !!dstet, e) + | _ -> disfailwith "invalid" + in + let extend i = extcast (getelt src i) in + let e = + concat_explist + (List.map ~f:extend + (List.range ~stride:(-1) ~stop:`inclusive (nelem - 1) 0)) + in + [ assn t dst e ] + | Pmovmskb (t, dst, src) -> + let nbytes = bytes_of_width t in + let src = + match src with + | Ovec _ -> op2e t src + | _ -> disfailwith "invalid operand" + in + let get_bit i = Bil.Extract ((i * 8) - 1, (i * 8) - 1, src) in + let byte_indices = List.init ~f:(fun i -> i + 1) nbytes in + (* list 1-nbytes *) + let all_bits = List.rev (List.map ~f:get_bit byte_indices) in + (* could also be done with shifts *) + let padt = Type.Imm (32 - nbytes) in + let or_together_bits = + List.fold_left + ~f:(fun acc i -> Bil.Concat (acc, i)) + ~init:(int_exp 0 !!padt) all_bits + in + [ assn reg32_t dst or_together_bits ] + | Palignr (t, dst, src, vsrc, imm) -> ( + let dst_e, t_concat = op2e_keep_width t dst in + let src_e, t_concat' = op2e_keep_width t src in + (* previously, this code called Typecheck.infer_ast. + * We're now just preserving the widths, so here we assert + * that our 2 "preserved widths" are the same. *) + assert (!!t_concat = !!t_concat'); + let imm = op2e t imm in + let conct = Bil.(dst_e ^ src_e) in + let shift = + Bil.(conct lsr Cast (UNSIGNED, !!t_concat, imm lsl int_exp 3 !!t)) + in + let high, low = + match t with + | Type.Imm 256 -> (255, 0) + | Type.Imm 128 -> (127, 0) + | Type.Imm 64 -> (63, 0) + | _ -> + disfailwith + "impossible: used non 64/128/256-bit operand in palignr" + in + let result = Bil.Extract (high, low, shift) in + let im i = Bil.Int (int_of_mode mode i) in + let addresses = + List.fold + ~f:(fun acc -> function Oaddr a -> a :: acc | _ -> acc) + ~init:[] [ src; dst ] + in + (* Palignr seems to cause a CPU general protection exception if this fails. + * previously this code used the ast.ml Assert statement, which is gone, + * so it's been replaced with Bil's CpuExn *) + List.map + ~f:(fun addr -> + Bil.If + ( Bil.(addr land im 15 = im 0), + [], + [ Cpu_exceptions.general_protection ] )) + addresses + @ + match vsrc with + | None -> [ assn t dst result ] + | Some vdst -> [ assn t vdst result ]) + | Pcmpstr (t, xmm1, xmm2m128, _imm, imm8cb, pcmpinfo) -> + let open Pcmpstr in + let concat elt_width exps = + match exps with + | [] -> disfailwith "trying concat on empty list" + | first :: exps' -> + let len = List.length exps * elt_width in + let exp = + List.fold exps' ~init:first ~f:(fun e e' -> Bil.(e ^ e')) + in + let tmp = tmp (Type.imm len) in + (tmp, Bil.[ tmp := exp ]) + in + + (* All bytes and bits are numbered with zero being the least + significant. This includes strings! *) + (* NOTE: Strings are backwards, at least when they are in + registers. This doesn't seem to be documented in the Intel + manual. This means that the NULL byte comes before the + string. *) + let xmm1_e = op2e t xmm1 in + let xmm2m128_e = op2e t xmm2m128 in + let regm = type_of_mode mode in + + let nelem, _nbits, elemt = + match imm8cb.ssize with + | Bytes -> (16, 8, Type.imm 8) + | Words -> (8, 16, Type.imm 16) + in + + (* Get element index in e *) + let get_elem = extract_element !!elemt in + let get_xmm1 = get_elem xmm1_e in + let get_xmm2 = get_elem xmm2m128_e in + + let nelem_range = + List.range ~stride:(-1) ~stop:`inclusive (nelem - 1) 0 + in + + (* Build expressions that assigns the correct values to the + is_valid variables using implicit (NULL-based) string length. *) + let implicit_check is_valid_xmm_i get_xmm_i = + let f acc i = + let previous_valid = + if i = 0 then exp_true else Bil.var (is_valid_xmm_i (i - 1)) + in + let current_valid = Bil.(get_xmm_i i <> int_exp 0 !!elemt) in + let x = is_valid_xmm_i i in + Bil.(x := previous_valid land current_valid) :: acc + in + List.fold ~f ~init:[] nelem_range + in + + (* Build expressions that assigns the correct values to the + is_valid variables using explicit string length. *) + let explicit_check is_valid_xmm_i sizee = + (* Max size is nelem *) + let nelem_e = Word.of_int ~width:(bitwidth_of_type regm) nelem in + let sizev = tmp ~name:"sz" regm in + let init = + Bil. + [ + if_ + (int nelem_e < sizee) + [ sizev := int nelem_e ] + [ sizev := sizee ]; + ] + in + let f acc i = + (* Current element is valid *) + let current_valid = Bil.(int_exp i !!regm < var sizev) in + let x = is_valid_xmm_i i in + Bil.(x := current_valid) :: acc + in + List.fold_left ~f ~init nelem_range + in + + (* Get var name indicating whether index in xmm num is a valid + byte (before NULL byte). *) + (* XXX more hashtable code *) + let is_valid = + let vh = Hashtbl.Poly.create () ~size:(2 * nelem) in + fun xmmnum index -> + match Hashtbl.find vh (xmmnum, index) with + | Some v -> v + | None -> + let name = sprintf "is_valid_xmm%d_ele%d" xmmnum index in + let v = tmp ~name bool_t in + Hashtbl.add_exn vh ~key:(xmmnum, index) ~data:v; + v + in + + let is_valid_xmm1 index = is_valid 1 index in + let is_valid_xmm2 index = is_valid 2 index in + let is_valid_xmm1_e index = Bil.Var (is_valid_xmm1 index) in + let is_valid_xmm2_e index = Bil.Var (is_valid_xmm2 index) in + + let xmm1_checks, xmm2_checks = + match pcmpinfo.len with + | Implicit -> + ( implicit_check is_valid_xmm1 get_xmm1, + implicit_check is_valid_xmm2 get_xmm2 ) + | Explicit -> + ( explicit_check is_valid_xmm1 rax_e, + explicit_check is_valid_xmm2 rdx_e ) + in + + let get_bit index = + match imm8cb.agg with + | EqualAny -> + (* Is xmm2[index] at xmm1[j]? *) + let check_char acc j = + let is_eql = Bil.(get_xmm2 index = get_xmm1 j) in + let is_valid = is_valid_xmm1_e j in + Bil.(is_eql land is_valid lor acc) + in + (* Is xmm2[index] included in xmm1[j] for any j? *) + Bil.( + is_valid_xmm2_e index + land List.fold ~f:check_char ~init:exp_false nelem_range) + | Ranges -> + (* Is there an even j such that xmm1[j] <= xmm2[index] <= + xmm1[j+1]? *) + let check_char acc j = + (* XXX: Should this be AND? *) + let ind0 = 2 * j in + let ind1 = ind0 + 1 in + let rangevalid = + Bil.(is_valid_xmm1_e ind0 land is_valid_xmm1_e ind1) + in + let ( <= ) = + match imm8cb.ssign with + | Unsigned -> Bil.( <= ) + | Signed -> Bil.( <=$ ) + in + let ( land ) = Bil.( land ) in + let inrange = + (get_xmm1 ind0 <= get_xmm2 index) + land (get_xmm2 index <= get_xmm1 ind1) + in + Bil.(rangevalid land (inrange lor acc)) + in + Bil.( + is_valid_xmm2_e index + land List.fold_left ~f:check_char ~init:exp_false + (List.range ~stride:(-1) ~stop:`inclusive + Stdlib.((nelem / 2) - 1) + 0)) + | EqualEach -> + (* Does xmm1[index] = xmm2[index]? *) + let xmm1_invalid = Bil.(UnOp (NOT, is_valid_xmm1_e index)) in + let xmm2_invalid = Bil.(UnOp (NOT, is_valid_xmm2_e index)) in + let bothinvalid = Bil.(xmm1_invalid land xmm2_invalid) in + let eitherinvalid = Bil.(xmm1_invalid lor xmm2_invalid) in + let equal = Bil.(get_xmm1 index = get_xmm2 index) in + (* both invalid -> true + one invalid -> false + both valid -> check same byte *) + Bil.(bothinvalid lor (UnOp (NOT, eitherinvalid) land equal)) + | EqualOrdered -> + (* Does the substring xmm1 occur at xmm2[index]? *) + let check_char acc j = + let equal = Bil.(get_xmm1 j = get_xmm2 Stdlib.(index + j)) in + let substrended = Bil.(UnOp (NOT, is_valid_xmm1_e j)) in + let bigstrended = Bil.UnOp (NOT, is_valid_xmm2_e (index + j)) in + (* substrended => true + bigstrended => false + byte diff => false + byte same => keep going *) + Bil.( + substrended lor (UnOp (NOT, bigstrended) land (equal land acc))) + in + (* Is xmm1[j] equal to xmm2[index+j]? *) + List.fold_left ~f:check_char ~init:exp_true + (List.range ~stride:(-1) ~stop:`inclusive (nelem - index - 1) 0) + in + let bits = List.map ~f:get_bit nelem_range in + let res, res_bil = concat 1 bits in + let int_res_1 = tmp ~name:"IntRes1" reg16_t in + let int_res_2 = tmp ~name:"IntRes2" reg16_t in + + let contains_null e = + let elts = + List.init nelem ~f:(fun i -> Bil.(get_elem e i = int_exp 0 !!elemt)) + in + List.fold elts ~init:exp_false ~f:(fun acc elt -> Bil.(acc lor elt)) + in + + (* For pcmpistri/pcmpestri *) + let sb exp = + List.fold_left + ~f:(fun acc i -> + Bil.Ite + (Bil.(exp_true = Extract (i, i, exp)), int_exp i !!regm, acc)) + ~init:(int_exp nelem !!regm) + (match imm8cb.outselectsig with + | LSB -> + List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem + 0 + | MSB -> List.init ~f:(fun x -> x) nelem) + in + + (* For pcmpistrm/pcmpestrm *) + let mask e = + match imm8cb.outselectmask with + | Bitmask -> Bil.(cast unsigned 128 e) + | Bytemask -> + let get_element i = Bil.(cast unsigned !!elemt (extract i i e)) in + let range = + List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive nelem + 0 + in + concat_explist (List.map ~f:get_element range) + in + + let res_of_cb = + match imm8cb with + | { negintres1 = false; _ } -> Bil.(int_res_2 := var int_res_1) + | { negintres1 = true; maskintres1 = false; _ } -> + (* int_res_1 is bitwise-notted *) + Bil.(int_res_2 := unop not (var int_res_1)) + | { negintres1 = true; maskintres1 = true; _ } -> + (* only the valid elements in xmm2 are bitwise-notted *) + (* XXX: Right now we duplicate the valid element computations + when negating the valid elements. They are also used by the + aggregation functions. A better way to implement this might + be to write the valid element information out as a temporary + bitvector. The aggregation functions and this code would + then extract the relevant bit to see if an element is + valid. *) + let validvector = + let range = + List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive + nelem 0 + in + let bits = List.map ~f:is_valid_xmm2_e range in + Bil.(cast unsigned 16 (concat_explist bits)) + in + Bil.(int_res_2 := validvector lxor var int_res_1) + in + + let res_of_pcmpinfo = + match pcmpinfo.out with + | Index -> Bil.(rcx := sb (var int_res_2)) + (* FIXME: ymms should be used instead of xmms here *) + | Mask -> Bil.(ymms.(0) := mask (var int_res_2)) + in + + List.concat + [ + xmm1_checks; + xmm2_checks; + res_bil; + Bil. + [ + int_res_1 := cast unsigned 16 (var res); + res_of_cb; + res_of_pcmpinfo; + cf := var int_res_2 <> int_exp 0 16; + zf := contains_null xmm2m128_e; + sf := contains_null xmm1_e; + oF := extract 0 0 (var int_res_2); + af := int_exp 0 1; + pf := int_exp 0 1; + ]; + ] + | Pshufd (t, dst, src, vsrc, imm) -> ( + let src_e = op2e t src in + let imm_e = op2e t imm in + (* XXX: This would be more straight-forward if implemented using + map, instead of fold *) + let get_dword ndword = + let high_b = (2 * (ndword mod 4)) + 1 in + let low_b = 2 * (ndword mod 4) in + let index = + Bil.(Cast (UNSIGNED, !!t, Extract (high_b, low_b, imm_e))) + in + let t' = !!t in + (* Use the same pattern for the top half of a ymm register *) + (* had to stop using extract_element_symbolic, since that calls + * Typecheck.infer_ast. I believe this captures the same + * "width logic", but this is a good place to check if things start + * going wrong later. *) + let index, index_width = + if t' = 256 && ndword > 3 then + (Bil.(index + Int (BV.of_int ~width:!!t 4)), 256) + else (index, t') + in + extract_element_symbolic_with_width (Type.imm 32) src_e index + index_width + in + let topdword = match t with Type.Imm 128 -> 3 | _ -> 7 in + let dwords = + concat_explist + (List.map ~f:get_dword + (List.range ~stride:(-1) ~stop:`inclusive topdword 0)) + in + match vsrc with + | None -> [ assn t dst dwords ] + | Some vdst -> [ assn t vdst dwords ]) + | Pshufb (exp_type, dst_op, src_op, vsrc) -> + let op_size = bitwidth_of_type exp_type in + let index_bits = + match op_size with + | 64 -> 3 + | 128 | 256 -> 4 + | _ -> disfailwith "invalid size for pshufb" + in + let foreach_byte f = List.concat @@ List.init (op_size / 8) ~f in + + let src = op2e exp_type src_op in + let dst = op2e exp_type dst_op in + let dst_op = Option.value ~default:dst_op vsrc in + let zero = Bil.int (Word.zero op_size) in + let msb_one = Bil.int (Word.of_int ~width:8 0x80) in + + let byte_t = Type.imm 8 in + let byte = int_exp 8 8 in + let iv = tmp ~name:"i" byte_t in + let mask_byte_i = tmp byte_t in + let tmp_byte = tmp exp_type in + let tmp_dst = tmp exp_type in + let ind = tmp byte_t in + + let check_mem_alignment = + match src_op with + | Oaddr addr when op_size = 128 -> + let word_size = width_of_mode mode in + let zero = Bil.int (Word.zero word_size) in + let oxf = Bil.int (Word.of_int ~width:word_size 0xf) in + [ Bil.(if_ (oxf land addr <> zero) [ cpuexn 13 ] []) ] + | _ -> [] + in + + List.concat + [ + check_mem_alignment; + [ Bil.move tmp_dst zero ]; + foreach_byte (fun i -> + Bil. + [ + iv := int (Word.of_int ~width:8 i); + mask_byte_i := extract 7 0 (src lsr (var iv * byte)); + if_ + (msb_one land var mask_byte_i = msb_one) + [ tmp_byte := zero ] + (* else *) + [ + ind := + cast unsigned 8 + (extract index_bits 0 (var mask_byte_i)); + tmp_byte := + cast unsigned op_size + (extract 7 0 (dst lsr (var ind * byte))); + ]; + (tmp_dst := + Bil.(var tmp_dst lor (var tmp_byte lsl (var iv * byte)))); + ]); + [ assn exp_type dst_op (Bil.var tmp_dst) ]; + ] + | Lea (t, r, a) when List.is_empty pref -> + (* See Table 3-64 *) + (* previously, it checked whether addrbits > opbits before the cast_low. + * The conclusion we came to was that + - if they were equal, the cast is basically a nop + - if it was the other way round, you want to extend it anyway. + * (I may be remembering things wrongly) *) + [ assn t r Bil.(Cast (LOW, !!t, a)) ] + | Call (o1, ra) -> ( + (* If o1 is an immediate, we should syntactically have Jump(imm) + so that the CFG algorithm knows where the jump goes. Otherwise + it will point to BB_Indirect. + + Otherwise, we should evaluate the operand before decrementing esp. + (This really only matters when esp is the base register of a memory + lookup. *) + let target = op2e mt o1 in + match o1 with + | Oimm _ -> + [ + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width mt)))); + store_s mode None mt rsp_e (Bil.Int ra); + Bil.Jmp target; + ] + | _ -> + let t = tmp mt in + [ + Bil.Move (t, target); + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width mt)))); + store_s mode None mt rsp_e (Bil.Int ra); + Bil.Jmp (Bil.Var t); + ]) + | Jump o -> [ Bil.Jmp (jump_target mode ss has_rex o) ] + | Jcc (o, c) -> + [ Bil.If (c, [ Bil.Jmp (jump_target mode ss has_rex o) ], []) ] + | Setcc (t, o1, c) -> [ assn t o1 Bil.(Cast (UNSIGNED, !!t, c)) ] + | Shift (st, s, dst, shift) -> + let old = tmp ~name:"tmp" s in + let s' = !!s in + let size = int_exp s' s' in + let s_f = + Bil.( + match st with + | LSHIFT -> ( lsl ) + | RSHIFT -> ( lsr ) + | ARSHIFT -> ( asr ) + | _ -> disfailwith "invalid shift type") + in + let dste = op2e s dst in + let count_mask = Bil.(size - int_exp 1 s') in + let count = Bil.(op2e s shift land count_mask) in + let new_of = + match st with + | LSHIFT -> Bil.(Cast (HIGH, !!bool_t, dste) lxor cf_e) + | RSHIFT -> Bil.(Cast (HIGH, !!bool_t, var old)) + | ARSHIFT -> exp_false + | _ -> disfailwith "impossible" + in + let new_cf = + (* undefined for SHL and SHR instructions where the count is greater than + or equal to the size (in bits) of the destination operand *) + match st with + | LSHIFT -> Bil.(Cast (LOW, !!bool_t, var old lsr (size - count))) + | RSHIFT | ARSHIFT -> + Bil.(Cast (HIGH, !!bool_t, var old lsl (size - count))) + | _ -> failwith "impossible" + in + Bil. + [ + old := dste; + assn s dst (s_f dste count); + if_ + (count <> int_exp 0 s') + [ + cf := new_cf; + sf := compute_sf dste; + zf := compute_zf s' dste; + pf := compute_pf s dste; + af := unknown "after-shift" bool_t; + if_ + (count = int_exp 1 s') + [ oF := new_of ] + [ oF := unknown "after-shift" bool_t ]; + ] + []; + ] + | Shiftd (st, s, dst, fill, count) -> + let was = tmp ~name:"tmp" s in + let e_dst = op2e s dst in + let e_fill = op2e s fill in + let s' = !!s in + (* Check for 64-bit operand *) + let size = int_exp s' s' in + let count_mask = Bil.(size - int_exp 1 s') in + let e_count = Bil.(op2e s count land count_mask) in + let new_cf = + match st with + | LSHIFT -> Bil.(Cast (LOW, !!bool_t, var was lsr (size - e_count))) + | RSHIFT -> Bil.(Cast (HIGH, !!bool_t, var was lsl (size - e_count))) + | _ -> disfailwith "impossible" + in + let new_of = Bil.(Cast (HIGH, !!bool_t, var was lxor e_dst)) in + let unk_of = + Bil.Unknown ("OF undefined after shiftd of more then 1 bit", bool_t) + in + let ret1 = + match st with + | LSHIFT -> Bil.(e_fill lsr (size - e_count)) + | RSHIFT -> Bil.(e_fill lsl (size - e_count)) + | _ -> disfailwith "impossible" + in + let ret2 = + match st with + | LSHIFT -> Bil.(e_dst lsl e_count) + | RSHIFT -> Bil.(e_dst lsr e_count) + | _ -> disfailwith "impossible" + in + let result = Bil.(ret1 lor ret2) in + (* SWXXX If shift is greater than the operand size, dst and + flags are undefined *) + Bil. + [ + was := e_dst; + assn s dst result; + if_ + (e_count <> int_exp 0 s') + [ + cf := new_cf; + sf := compute_sf e_dst; + zf := compute_zf s' e_dst; + pf := compute_pf s e_dst; + (* For a 1-bit shift, the OF flag is set if a sign change occurred; + otherwise, it is cleared. For shifts greater than 1 bit, the OF flag + is undefined. *) + if_ (e_count = int_exp 1 s') [ oF := new_of ] [ oF := unk_of ]; + ] + []; + ] + | Rotate (shift_type, exp_type, dst_op, shift_op, use_cf) -> + if use_cf then unimplemented "rotate use_vf"; + let word_size = bitwidth_of_type exp_type in + let mask_size = word_size - 1 in + let count_var = tmp exp_type in + let count = Bil.var count_var in + let zero = int_exp 0 word_size in + let one = int_exp 1 word_size in + let dst = op2e exp_type dst_op in + let shift_mask = int_exp mask_size word_size in + let size = int_exp word_size word_size in + let shift = op2e exp_type shift_op in + + if [%compare.equal: binop] shift_type LSHIFT then + Bil. + [ + count_var := shift land shift_mask mod size; + assn exp_type dst_op ((dst lsl count) lor (dst lsr (size - count))); + if_ (count = zero) + [ cf := cast low 1 dst ] + (* else *) + [ + if_ (count = one) + [ oF := cf_e lxor cast high 1 dst ] + (* else *) + [ + oF := + unknown "OF undefined after rotate of more then 1 bit" + bool_t; + ]; + ]; + ] + else + Bil. + [ + count_var := shift land shift_mask mod size; + assn exp_type dst_op ((dst lsr count) lor (dst lsl (size - count))); + if_ (count = zero) + [ cf := cast high 1 dst ] + (* else *) + [ + if_ (count = one) + [ + oF := + cast high 1 dst + lxor cast high 1 (dst lsl int_exp 1 word_size); + ] + (* else *) + [ + oF := + unknown "OF undefined after rotate of more then 1 bit" + bool_t; + ]; + ]; + ] + | Bt (t, bitoffset, bitbase) -> + let t' = !!t in + let offset = op2e t bitoffset in + let value, shift = + match bitbase with + | Oreg _ -> + let reg = op2e t bitbase in + let shift = Bil.(offset land int_exp Stdlib.(t' - 1) t') in + (reg, shift) + | Oaddr a -> + let offset = Bil.(cast unsigned (width_of_mode mode) offset) in + let byte = + load (size_of_typ reg8_t) Bil.(a + (offset lsr int_exp 3 t')) + in + let shift = Bil.(Cast (LOW, !!reg8_t, offset) land int_exp 7 8) in + (byte, shift) + | Ovec _ | Oseg _ | Oimm _ -> disfailwith "Invalid bt operand" + in + [ + Bil.Move (cf, Bil.(Cast (LOW, !!bool_t, value lsr shift))); + Bil.Move (oF, Bil.Unknown ("OF undefined after bt", bool_t)); + Bil.Move (sf, Bil.Unknown ("SF undefined after bt", bool_t)); + Bil.Move (af, Bil.Unknown ("AF undefined after bt", bool_t)); + Bil.Move (pf, Bil.Unknown ("PF undefined after bt", bool_t)); + ] + | Bs (t, dst, src, dir) -> + let is_zero_count = List.rev pref |> List.exists ~f:Int.(( = ) 0xf3) in + let width = !!t in + let src_e = op2e t src in + let is_fwd = match dir with Backward -> false | Forward -> true in + let res = tmp t in + let assn_res = Bil.(res := src_e) in + let scan_bil = + if is_fwd then + match width with + | 16 -> ctz16 res + | 32 -> ctz32 res + | 64 -> ctz64 res + | _ -> disfailwith "Invalid bitscan width" + else + match width with + | 16 -> clz16 res + | 32 -> clz32 res + | 64 -> clz64 res + | _ -> disfailwith "Invalid bitscan width" + in + let assn_result = + let n1 = width - 1 in + assn t dst + @@ + if is_zero_count || is_fwd then Bil.var res + else Bil.(var res lxor int Word.(of_int n1 ~width)) + in + let bil = assn_res :: scan_bil in + let bil = + if is_zero_count then + bil + @ Bil. + [ + assn_result; + cf := var res = int Word.(of_int ~width width); + zf := var res = int Word.(zero width); + ] + else + Bil. + [ + if_ + (src_e = int (Word.zero width)) + [ zf := int Word.b1; assn t dst @@ unknown "bits" t ] + (bil @ Bil.[ assn_result; zf := int Word.b0 ]); + ] + in + bil @ bitscan_flags is_zero_count + | Hlt -> [] (* x86 Hlt is essentially a NOP *) + | Rdtsc -> + let undef reg = assn reg32_t reg (Bil.Unknown ("rdtsc", reg32_t)) in + List.map ~f:undef [ o_rax; o_rdx ] + | Cpuid -> + let undef reg = assn reg32_t reg (Bil.Unknown ("cpuid", reg32_t)) in + List.map ~f:undef [ o_rax; o_rbx; o_rcx; o_rdx ] + | Xgetbv -> + let undef reg = assn reg32_t reg (Bil.Unknown ("xgetbv", reg32_t)) in + List.map ~f:undef [ o_rax; o_rdx ] + | Stmxcsr dst -> + let dst = + match dst with + | Oaddr addr -> addr + | _ -> disfailwith "stmxcsr argument cannot be non-memory" + in + [ + store reg32_t dst (Bil.Var mxcsr); (*(Unknown ("stmxcsr", reg32_t));*) + ] + | Ldmxcsr src -> + let src = + match src with + | Oaddr addr -> addr + | _ -> disfailwith "ldmxcsr argument cannot be non-memory" + in + [ Bil.Move (mxcsr, load (size_of_typ reg32_t) src) ] + | Fnstcw dst -> + let dst = + match dst with + | Oaddr addr -> addr + | _ -> disfailwith "fnstcw argument cannot be non-memory" + in + [ store reg16_t dst (Bil.Var fpu_ctrl) ] + | Fldcw src -> + let src = + match src with + | Oaddr addr -> addr + | _ -> disfailwith "fldcw argument cannot be non-memory" + in + [ Bil.Move (fpu_ctrl, load (size_of_typ reg16_t) src) ] + | Fld _src -> unimplemented "unsupported FPU register stack" + | Fst (_dst, _pop) -> unimplemented "unsupported FPU flags" + | Cmps (Type.Imm _bits as t) -> + let t' = !!t in + let src1 = tmp t in + let src2 = tmp t in + let tmpres = tmp t in + let stmts = + Bil.Move (src1, op2e t (Oaddr rsi_e)) + :: Bil.Move (src2, op2e_s mode seg_es has_rex t (Oaddr rdi_e)) + :: Bil.Move (tmpres, Bil.(Var src1 - Var src2)) + :: string_incr mode t rsi :: string_incr mode t rdi + :: set_flags_sub t' (Bil.Var src1) (Bil.Var src2) (Bil.Var tmpres) + in + begin match pref with + | [] -> stmts + | [ single ] when single = repz || single = repnz -> + rep_wrap ~mode ~check_zf:single ~addr ~next stmts + | _ -> unimplemented "unsupported flags in cmps" + end + | Scas (Type.Imm _bits as t) -> + let t' = !!t in + let src1 = tmp t in + let src2 = tmp t in + let tmpres = tmp t in + let stmts = + let open Stmt in + Move (src1, Bil.(Cast (LOW, !!t, Var rax))) + :: Move (src2, op2e_s mode seg_es has_rex t (Oaddr rdi_e)) + :: Move (tmpres, Bil.(Var src1 - Var src2)) + :: string_incr mode t rdi + :: set_flags_sub t' (Bil.Var src1) (Bil.Var src2) (Bil.Var tmpres) + in + begin match pref with + | [] -> stmts + | [ single ] when single = repz || single = repnz -> + rep_wrap ~mode ~check_zf:single ~addr ~next stmts + | _ -> unimplemented "unsupported flags in scas" + end + | Stos (Type.Imm _bits as t) -> + let stmts = + [ store_s mode seg_es t rdi_e (op2e t o_rax); string_incr mode t rdi ] + in + begin match pref with + | [] -> stmts + | [ single ] when single = repz -> rep_wrap ~mode ~addr ~next stmts + | _ -> unimplemented "unsupported prefix for stos" + end + | Push (t, o) -> + let o = if is_small_imm o t then sign_extend_imm o t else op2e t o in + let tmp = tmp t in + (* only really needed when o involves esp *) + [ + Bil.Move (tmp, o); + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width t)))); + store_s mode seg_ss t rsp_e (Bil.var tmp) + (* FIXME: can ss be overridden? *); + ] + | Pop (t, o) -> + (* From the manual: + + "The POP ESP instruction increments the stack pointer (ESP) + before data at the old top of stack is written into the + destination" + + So, effectively there is no incrementation. + *) + assn t o (load_s mode seg_ss (size_of_typ t) rsp_e) + :: + (if [%compare.equal: operand] o o_rsp then [] + else [ Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width t)))) ]) + | Pushf t -> + (* Note that we currently treat these fields as unknowns, but the + manual says: When copying the entire EFLAGS register to the + stack, the VM and RF flags (bits 16 and 17) are not copied; + instead, the values for these flags are cleared in the EFLAGS + image stored on the stack. *) + let flags_e = + match t with + | Type.Imm 16 -> flags_e + | Type.Imm 32 -> eflags_e + | Type.Imm 64 -> rflags_e + | _ -> failwith "impossible" + in + [ + Bil.Move (rsp, Bil.(rsp_e - Int (mi (bytes_of_width t)))); + store_s mode seg_ss t rsp_e flags_e; + ] + | Popf t -> + let assnsf = + match t with + | Type.Imm 16 -> assns_flags_to_bap + | Type.Imm 32 -> assns_eflags_to_bap + | Type.Imm 64 -> assns_rflags_to_bap + | _ -> failwith "impossible" + in + let tmp = tmp t in + let extractlist = + List.map + ~f:(fun i -> Bil.(Extract (i, i, Var tmp))) + (List.range ~stride:(-1) ~start:`exclusive ~stop:`inclusive !!t 0) + in + Bil.Move (tmp, load_s mode seg_ss (size_of_typ t) rsp_e) + :: Bil.Move (rsp, Bil.(rsp_e + Int (mi (bytes_of_width t)))) + :: List.concat (List.map2_exn ~f:(fun f e -> f e) assnsf extractlist) + | Popcnt (t, s, d) -> + let width = !!t in + let bits = op2e t s in + let res = tmp t in + let assn_src = Bil.(res := bits) in + let cnt = + match width with + | 16 -> popcnt16 res + | 32 -> popcnt32 res + | 64 -> popcnt64 res + | _ -> disfailwith "Invalid popcnt width" + in + let bil = (assn_src :: cnt) @ Bil.[ assn t d (var res) ] in + let flags = + List.map + ~f:(fun r -> Bil.Move (r, int_exp 0 1)) + [ cf; oF; sf; af; pf ] + in + set_zf width bits :: (bil @ flags) + | Sahf -> + let assnsf = assns_lflags_to_bap in + let tah = tmp ~name:"AH" reg8_t in + let extractlist = + List.map + ~f:(fun i -> Bil.(Extract (i, i, Var tah))) + (List.range ~stride:(-1) ~stop:`inclusive 7 0) + in + Bil.Move (tah, ah_e) + :: List.concat (List.map2_exn ~f:(fun f e -> f e) assnsf extractlist) + | Lahf -> + let o_ah = Oreg 4 in + [ assn reg8_t o_ah lflags_e ] + | Add (t, o1, o2) -> + let tmp = tmp t and tmp2 = tmp t in + Bil.Move (tmp, op2e t o1) + :: Bil.Move (tmp2, op2e t o2) + :: assn t o1 Bil.(op2e t o1 + Var tmp2) + :: + (let s1 = Bil.Var tmp in + let s2 = Bil.Var tmp2 in + let r = op2e t o1 in + set_flags_add !!t s1 s2 r) + | Adc (t, o1, o2) -> + let orig1 = tmp t in + let orig2 = tmp t in + let bits = !!t in + let t' = Type.Imm (bits + 1) in + let c e = Bil.(Cast (UNSIGNED, !!t', e)) in + (* Literally compute the addition with an extra bit and see + what the value is for CF *) + let s1 = Bil.Var orig1 in + let s2 = Bil.Var orig2 in + let r = op2e t o1 in + let bige = Bil.(c s1 + c s2 + c (Cast (UNSIGNED, !!t, cf_e))) in + Bil.Move (orig1, op2e t o1) + :: Bil.Move (orig2, op2e t o2) + :: assn t o1 Bil.(s1 + s2 + Cast (UNSIGNED, !!t, cf_e)) + :: Bil.Move (cf, Bil.Extract (bits, bits, bige)) + :: set_aopszf_add !!t s1 s2 r + | Inc (t, o) (* o = o + 1 *) -> + let t' = !!t in + let tmp = tmp t in + Bil.Move (tmp, op2e t o) + :: assn t o Bil.(op2e t o + int_exp 1 t') + :: set_aopszf_add t' (Bil.Var tmp) (int_exp 1 t') (op2e t o) + | Dec (t, o) (* o = o - 1 *) -> + let t' = !!t in + let tmp = tmp t in + Bil.Move (tmp, op2e t o) + :: assn t o Bil.(op2e t o - int_exp 1 t') + :: set_aopszf_sub t' (Bil.Var tmp) (int_exp 1 t') (op2e t o) + (* CF is maintained *) + | Sub (t, o1, o2) (* o1 = o1 - o2 *) -> + let oldo1 = tmp t in + let oldo2 = tmp t in + let op1 = op2e t o1 in + let op2 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + Bil.( + [ oldo1 := op1; oldo2 := op2; assn t o1 (op1 - op2) ] + @ set_flags_sub (bitwidth_of_type t) (var oldo1) (var oldo2) op1) + | Sbb (t, o1, o2) -> + let tmp_s = tmp t in + let tmp_d = tmp t in + let orig_s = Bil.Var tmp_s in + let orig_d = Bil.Var tmp_d in + let sube = Bil.(orig_s + Cast (UNSIGNED, !!t, cf_e)) in + let d = op2e t o1 in + let s1 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + Bil.Move (tmp_s, s1) + :: Bil.Move (tmp_d, d) + :: assn t o1 Bil.(orig_d - sube) + :: Bil.Move + ( oF, + Bil.( + Cast (HIGH, !!bool_t, orig_s lxor orig_d land (orig_d lxor d))) + ) + (* When src = 0xffffffff and cf=1, the processor sets CF=1. + + Note that we compute dest = dest - (0xffffffff + 1) = 0, so the + subtraction does not overflow. + + So, I am guessing that CF is set if the subtraction overflows + or the addition overflows. + + Maybe we should implement this by doing the actual computation, + like we do for adc. + *) + (* sub overflow | add overflow *) + :: Bil.Move (cf, Bil.((sube > orig_d) lor (sube < orig_s))) + :: set_apszf !!t orig_s orig_d d + | Cmp (t, o1, o2) -> + let tmp = tmp t in + Bil.Move (tmp, Bil.(op2e t o1 - op2e t o2)) + :: set_flags_sub !!t (op2e t o1) (op2e t o2) (Bil.Var tmp) + | Cmpxchg (t, src, dst) -> + let t' = !!t in + let eax_e = op2e t o_rax in + let dst_e = op2e t dst in + let src_e = op2e t src in + let tmp = tmp t in + Bil.Move (tmp, Bil.(eax_e - dst_e)) + :: set_flags_sub t' eax_e dst_e (Bil.Var tmp) + @ [ + assn t dst (Bil.Ite (zf_e, src_e, dst_e)); + assn t o_rax (Bil.Ite (zf_e, eax_e, dst_e)); + ] + | Cmpxchg8b o -> + (* only 32bit case *) + let accumulator = Bil.Concat (op2e reg32_t o_rdx, op2e reg32_t o_rax) in + let dst_e = op2e reg64_t o in + let src_e = Bil.Concat (op2e reg32_t o_rcx, op2e reg32_t o_rbx) in + let dst_low_e = Bil.Extract (63, 32, dst_e) in + let dst_hi_e = Bil.Extract (31, 0, dst_e) in + let eax_e = op2e reg32_t o_rax in + let edx_e = op2e reg32_t o_rdx in + let equal = tmp bool_t in + let equal_v = Bil.Var equal in + [ + Bil.Move (equal, Bil.(accumulator = dst_e)); + Bil.Move (zf, equal_v); + assn reg64_t o (Bil.Ite (equal_v, src_e, dst_e)); + assn reg32_t o_rax (Bil.Ite (equal_v, eax_e, dst_low_e)); + assn reg32_t o_rdx (Bil.Ite (equal_v, edx_e, dst_hi_e)); + ] + | Xadd (t, dst_op, src_op) -> + let tmp_res = tmp t in + let tmp_dst = tmp t in + let tmp_src = tmp t in + let dst = op2e t dst_op in + let src = op2e t src_op in + Bil. + [ + tmp_src := src; + tmp_dst := dst; + tmp_res := src + dst; + assn t src_op dst; + assn t dst_op (var tmp_res); + ] + @ set_flags_add !!t (Bil.var tmp_dst) (Bil.var tmp_src) dst + | Xchg (t, src, dst) -> + let tmp = tmp t in + [ + Bil.Move (tmp, op2e t src); + assn t src (op2e t dst); + assn t dst (Bil.Var tmp); + ] + | And (t, o1, o2) -> + assn t o1 Bil.(op2e t o1 land op2e t o2) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after and", bool_t)) + :: set_pszf t (op2e t o1) + | Or (t, o1, o2) -> + let o2 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + assn t o1 Bil.(op2e t o1 lor o2) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after or", bool_t)) + :: set_pszf t (op2e t o1) + | Xor (t, o1, o2) when [%compare.equal: operand] o1 o2 -> + assn t o1 Bil.(Int (BV.of_int ~width:!!t 0)) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after xor", bool_t)) + :: List.map ~f:(fun v -> Bil.Move (v, exp_true)) [ zf; pf ] + @ List.map ~f:(fun v -> Bil.Move (v, exp_false)) [ oF; cf; sf ] + | Xor (t, o1, o2) -> + assn t o1 Bil.(op2e t o1 lxor op2e t o2) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after xor", bool_t)) + :: set_pszf t (op2e t o1) + | Test (t, o1, o2) -> + let o2 = + if is_small_imm o2 t then sign_extend_imm o2 t else op2e t o2 + in + let tmp = tmp t in + Bil.Move (tmp, Bil.(op2e t o1 land o2)) + :: Bil.Move (oF, exp_false) + :: Bil.Move (cf, exp_false) + :: Bil.Move (af, Bil.Unknown ("AF is undefined after and", bool_t)) + :: set_pszf t (Bil.Var tmp) + | Ptest (t, o1, o2) -> + let open Stmt in + let t' = !!t in + let tmp1 = tmp t and tmp2 = tmp t in + Move (tmp1, Bil.(op2e t o2 land op2e t o1)) + :: Move (tmp2, Bil.(op2e t o2 land exp_not (op2e t o1))) + :: Move (af, exp_false) + :: Move (oF, exp_false) + :: Move (pf, exp_false) + :: Move (sf, exp_false) + :: Move (zf, Bil.(Var tmp1 = Int (BV.of_int ~width:t' 0))) + :: [ Move (cf, Bil.(Var tmp2 = Int (BV.of_int ~width:t' 0))) ] + | Not (t, o) -> [ assn t o (exp_not (op2e t o)) ] + | Neg (t, o) -> + let t' = !!t in + let tmp = tmp t in + let min_int = Bil.BinOp (LSHIFT, int_exp 1 t', int_exp (t' - 1) t') in + Bil.Move (tmp, op2e t o) + :: assn t o Bil.(int_exp 0 t' - op2e t o) + :: Bil.Move + (cf, Bil.(Ite (Var tmp = int_exp 0 t', int_exp 0 1, int_exp 1 1))) + :: Bil.Move (oF, Bil.(Ite (Var tmp = min_int, int_exp 1 1, int_exp 0 1))) + :: set_apszf_sub t' (Bil.Var tmp) (int_exp 0 t') (op2e t o) + | Mul (t, src) -> + (* Mul always multiplies EAX by src and stores the result in EDX:EAX + starting from the "right hand side" based on the type t of src *) + + (* The OF and CF flags are set to 0 if the upper half of the result is 0; + otherwise, they are set to 1 *) + let new_t = Type.Imm (!!t * 2) in + let assnstmts, assne = + Bil.( + assn_dbl t + (Cast (UNSIGNED, !!new_t, op2e t o_rax) + * Cast (UNSIGNED, !!new_t, op2e t src))) + in + let flag = + let highbit = !!new_t - 1 in + let lowbit = !!new_t / 2 in + Bil.(Extract (highbit, lowbit, assne) <> int_exp 0 !!t) + in + assnstmts + @ [ + Bil.Move (oF, flag); + Bil.Move (cf, flag); + Bil.Move (sf, Bil.Unknown ("SF is undefined after Mul", bool_t)); + Bil.Move (zf, Bil.Unknown ("ZF is undefined after Mul", bool_t)); + Bil.Move (af, Bil.Unknown ("AF is undefined after Mul", bool_t)); + Bil.Move (pf, Bil.Unknown ("PF is undefined after Mul", bool_t)); + ] + | Imul (t, (oneopform, dst), src1, src2) -> + let new_t = Type.Imm (!!t * 2) in + let mul_stmts = + match oneopform with + | true -> + (* For one operand form, use assn_double *) + let assnstmts, assne = + assn_dbl t + Bil.( + Cast (SIGNED, !!new_t, op2e t src1) + * Cast (SIGNED, !!new_t, op2e t src2)) + in + let flag = + (* Intel checks if EAX == EDX:EAX. Instead of doing this, we are just + going to check if the upper bits are != 0 *) + let highbit = !!new_t - 1 in + let lowbit = !!new_t / 2 in + Bil.(Extract (highbit, lowbit, assne) <> int_exp 0 !!t) + in + assnstmts @ [ Bil.Move (oF, flag); Bil.Move (cf, flag) ] + | false -> + (* Two and three operand forms *) + let tmp = tmp new_t in + (* Flag is set when the result is truncated *) + let flag = Bil.(Var tmp <> Cast (SIGNED, !!new_t, op2e t dst)) in + [ + Bil.Move + ( tmp, + Bil.( + Cast (SIGNED, !!new_t, op2e t src1) + * Cast (SIGNED, !!new_t, op2e t src2)) ); + assn t dst Bil.(Cast (LOW, !!t, Var tmp)); + Bil.Move (oF, flag); + Bil.Move (cf, flag); + ] + in + mul_stmts + @ [ + Bil.Move (pf, Bil.Unknown ("PF is undefined after imul", bool_t)); + Bil.Move (sf, Bil.Unknown ("SF is undefined after imul", bool_t)); + Bil.Move (zf, Bil.Unknown ("ZF is undefined after imul", bool_t)); + Bil.Move (af, Bil.Unknown ("AF is undefined after imul", bool_t)); + ] + | Div (t, src) -> + let dt' = !!t * 2 in + let dt = Type.Imm dt' in + let zero = int_exp 0 dt' in + let dividend = tmp ~name:"dividend" dt in + let divisor = tmp ~name:"divisor" dt in + let tdiv = tmp ~name:"div" dt in + let trem = tmp ~name:"rem" dt in + let result = Bil.(cast low !!t (var trem) ^ cast low !!t (var tdiv)) in + let apply_result = fst (assn_dbl t result) in + Bil. + [ + divisor := cast unsigned !!dt (op2e t src); + dividend := op2e_dbl t; + if_ + (var divisor = zero) + [ Cpu_exceptions.divide_by_zero ] + (* else *) + [ + tdiv := var dividend / var divisor; + trem := var dividend mod var divisor; + if_ + (cast high !!t (var tdiv) = int_exp 0 !!t) + apply_result (* else *) + [ Cpu_exceptions.divide_by_zero ]; + ]; + ] + @ undefine [ cf; oF; sf; zf; af; pf ] + | Idiv (t, src) -> + let dt' = !!t * 2 in + let dt = Type.Imm dt' in + let zero = int_exp 0 dt' in + let dividend = tmp ~name:"dividend" dt in + let divisor = tmp ~name:"divisor" dt in + let tdiv = tmp ~name:"div" dt in + let trem = tmp ~name:"rem" dt in + let result = Bil.(cast low !!t (var trem) ^ cast low !!t (var tdiv)) in + let apply_result = fst @@ assn_dbl t result in + let lbound = + let dtm1 = dt' - 1 in + Word.(one dt' lsl of_int ~width:dt' dtm1) + in + let ubound = Word.(lbound - one dt') in + Bil. + [ + divisor := cast signed !!dt (op2e t src); + dividend := op2e_dbl t; + if_ + (var divisor = zero) + [ Cpu_exceptions.divide_by_zero ] + (* else *) + [ + tdiv := var dividend /$ var divisor; + trem := var dividend %$ var divisor; + if_ + ((var tdiv >$ int ubound) lor (var tdiv <$ int lbound)) + [ Cpu_exceptions.divide_by_zero ] (* else *) + apply_result; + ]; + ] + @ undefine [ cf; oF; sf; zf; af; pf ] + | Cld -> [ Bil.Move (df, exp_false) ] + | Leave t when List.is_empty pref -> + (* #UD if Lock prefix is used *) + Bil.Move (rsp, rbp_e) + :: to_ir mode addr next ss pref has_rex has_vex (Pop (t, o_rbp)) + | Interrupt3 -> [ Bil.CpuExn 3 ] + | Interrupt (Oimm i) -> + [ + (match Addr.to_int i with + | Ok i -> Bil.cpuexn i + | Error _ -> + let dst = asprintf "interrupt@%s" (Addr.string_of_value i) in + Bil.(encode call dst)); + ] + | Sysenter | Syscall -> [ Bil.(encode call "syscall") ] + (* Match everything exhaustively *) + | Leave _ -> unimplemented "to_ir: Leave" + | Lea _ -> unimplemented "to_ir: Lea" + | Movs _ -> unimplemented "to_ir: Movs" + | Cmps _ -> unimplemented "to_ir: Cmps" + | Scas _ -> unimplemented "to_ir: Scas" + | Stos _ -> unimplemented "to_ir: Stos" + | Retn _ -> unimplemented "to_ir: Retn" + | Interrupt _ -> unimplemented "to_ir: Interrupt" +end +(* ToIR *) + +let disasm_instr mode mem addr = + let module D = X86_disasm in + let pref, prefix, op, na = D.parse_instr mode mem addr in + let has_rex = Option.is_some prefix.rex in + let has_vex = Option.is_some prefix.vex in + let ss, pref = D.parse_prefixes mode pref op in + ToIR.to_ir mode addr na ss pref has_rex has_vex op + +let insn arch mem insn = + let mode = match arch with `x86 -> X86 | `x86_64 -> X8664 in + let addr = Memory.min_addr mem in + match disasm_instr mode mem addr with + | exception No_semantics -> Ok [] + | exception Arch_exception (_, msg) -> + Or_error.errorf "invalid instruction: %s" msg + | exception exn -> + Or_error.errorf "internal error in the legacy lifter: %s@\n%s@\n" + (Exn.to_string exn) + (Printexc.get_backtrace ()) + | bil -> ( + match Type.check bil with + | Ok () -> Ok bil + | Error err -> + warning "BIL is not well-typed in the legacy lifter at %a - %a" + pp_insn (mem, insn) Type.Error.pp err; + Error (Error.of_string "type error")) + +module AMD64 = struct + module CPU = X86_cpu.AMD64 + + let lift mem i = insn `x86_64 mem i +end + +module IA32 = struct + module CPU = X86_cpu.IA32 + + let lift mem i = insn `x86 mem i +end diff --git a/plugins/x86/x86_sym_imm_lifter.mli b/plugins/x86/x86_sym_imm_lifter.mli new file mode 100644 index 000000000..741877bd6 --- /dev/null +++ b/plugins/x86/x86_sym_imm_lifter.mli @@ -0,0 +1,12 @@ +open Core_kernel[@@warning "-D"] +open Bap.Std + +module IA32 : sig + module CPU : CPU + val lift : lifter +end + +module AMD64 : sig + module CPU : CPU + val lift : lifter +end diff --git a/plugins/x86/x86_sym_imm_targets.ml b/plugins/x86/x86_sym_imm_targets.ml new file mode 100644 index 000000000..4203ede12 --- /dev/null +++ b/plugins/x86/x86_sym_imm_targets.ml @@ -0,0 +1,22 @@ +open Core_kernel [@@warning "-D"] +open Bap.Std +module Insn = Disasm_expert.Basic.Insn +module IA32SI_L = X86_sym_imm_lifter.IA32 +module AMD64SI_L = X86_sym_imm_lifter.AMD64 + +module IA32SI_D = struct + module CPU = IA32SI_L.CPU + + let lift _mem _insn = Ok [] +end + +module AMD64SI_D = struct + module CPU = AMD64SI_L.CPU + + let lift _mem _insn = Ok [] +end + +module IA32SI = X86_backend.IA32.Make (IA32SI_D) +module AMD64SI = X86_backend.AMD64.Make (AMD64SI_D) +module IA32SI_M = X86_backend.IA32.Make (IA32SI_L) +module AMD64SI_M = X86_backend.AMD64.Make (AMD64SI_L) diff --git a/plugins/x86/x86_sym_imm_targets.mli b/plugins/x86/x86_sym_imm_targets.mli new file mode 100644 index 000000000..71aeb55de --- /dev/null +++ b/plugins/x86/x86_sym_imm_targets.mli @@ -0,0 +1,14 @@ +open Core_kernel[@@warning "-D"] +open Bap.Std + +module IA32SI : Target + +module AMD64SI : Target + +module IA32SI_L : Target + +module AMD64SI_L : Target + +module IA32SI_M : Target + +module AMD64SI_M : Target