From a115deb2c68bd43b246ade4b4cf83febf2b05a77 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Fri, 5 Jun 2020 08:55:15 -0700 Subject: [PATCH 01/25] adds radare2 symbolizer --- oasis/radare2 | 8 ++-- plugins/radare2/radare2_main.ml | 83 +++++++++------------------------ 2 files changed, 27 insertions(+), 64 deletions(-) diff --git a/oasis/radare2 b/oasis/radare2 index 4610686ba..cf74eea97 100644 --- a/oasis/radare2 +++ b/oasis/radare2 @@ -2,14 +2,14 @@ Flag radare2 Description: Build radare2 plugin Default: false -Library radare2_plugin - Build$: flag(everything) || flag(radare2) +Library objdump_plugin + Build$: flag(everything) || flag(objdump) Path: plugins/radare2 FindlibName: bap-plugin-radare2 CompiledObject: best BuildDepends: bap, re.pcre, regular, bap-core-theory, bap-future, core_kernel, bap-knowledge, - zarith, bitvec, radare2, yojson + zarith, bitvec, radaer2, yojson InternalModules: Radare2_main XMETADescription: use radare2 to provide a symbolizer - XMETAExtraLines: tags="symbolizer, radare2" + XMETAExtraLines: tags="objdump, radare2" diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index 29a6be11e..5a0ab0a57 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -21,68 +21,31 @@ let provide_roots funcs = promise_property Theory.Label.is_valid; promise_property Theory.Label.is_subroutine -module Field = struct - (* unfortunately, we can't use Yojson.*.Utils because they are - undefined for the Yojson type *) - - let member name = function - | `Assoc xs -> List.Assoc.find xs ~equal:String.equal name - | _ -> invalid_arg "expects and assoc list" - - let string = function - | `String x -> x - | x -> invalid_argf "expects a string got %s" - (Yojson.to_string x) () - - let number = function - | `Int i -> Z.of_int i - | `Intlit s -> Z.of_string s - | s -> invalid_argf "expected an address got %s" - (Yojson.to_string s) () - - let field name parse obj = match member name obj with - | None -> invalid_argf "expected member %S in the object %s" - name (Yojson.to_string obj) () - | Some field -> parse field - - let addr = field "vaddr" number - let name = field "name" string - let kind = field "type" string -end - -let strip str = - if String.is_prefix ~prefix:"func." str then None - else Option.some @@ match String.chop_prefix str ~prefix:"imp." with - | Some str -> str - | None -> str - -let provide_radare2 file = +let provide_radare2 file = let funcs = Hashtbl.create (module struct type t = Z.t let compare = Z.compare and hash = Z.hash let sexp_of_t x = Sexp.Atom (Z.to_string x) end) in - let accept name addr = Hashtbl.set funcs addr name in - let symbols = match R2.with_command_j "isj" file with - | `List list -> Some list - | s -> warning "unexpected radare2 output: %a" Yojson.pp s; None - | exception Invalid_argument msg -> - warning "failed to get symbols: %s" msg; None in - Option.iter symbols ~f:(List.iter ~f:(fun s -> - match Field.name s, Field.addr s, Field.kind s with - | name,addr, "FUNC" -> accept (strip name) addr - | _ -> debug "skipping json item %a" Yojson.pp s)); - if Hashtbl.length funcs = 0 - then warning "failed to obtain symbols"; - let symbolizer = Symbolizer.create @@ fun addr -> - let addr = Bitvec.to_bigint (Word.to_bitvec addr) in - match Hashtbl.find funcs addr with - | Some name -> name - | None -> None in - Symbolizer.provide agent symbolizer; - provide_roots funcs - -let main () = Stream.observe Project.Info.file @@ provide_radare2 + let accept name addr = Hashtbl.set funcs addr name in + let extract name json = Yojson.Basic.Util.member name json in + try + let symbol_list = Yojson.Basic.Util.to_list (R2.with_command_j "aaa;aflj" file) in + List.fold symbol_list ~init:() ~f:(fun () symbol -> + accept (Yojson.Basic.Util.to_string (extract "name" symbol)) (Yojson.Basic.Util.to_int (extract "offset" symbol) |> Z.of_int) + ); + if Hashtbl.length funcs = 0 + then warning "failed to obtain symbols"; + let symbolizer = Symbolizer.create @@ fun addr -> + Hashtbl.find funcs @@ + Bitvec.to_bigint (Word.to_bitvec addr) in + Symbolizer.provide agent symbolizer; + provide_roots funcs + with _ -> warning "failed to use radare2";() + + + +let main = Stream.observe Project.Info.file @@ provide_radare2 let () = Config.manpage [ @@ -90,10 +53,10 @@ let () = `P "This plugin provides a symbolizer based on radare2."; `S "EXAMPLES"; `P "To view the symbols after running the plugin:"; - `P "$(b, bap) $(i,executable) --dump-symbols "; + `P "$(b, bap) $(i,executable) --no-objdump --dump-symbols "; `P "To view symbols without this plugin:"; - `P "$(b, bap) $(i,executable) --no-radare2 --dump-symbols"; + `P "$(b, bap) $(i,executable) --no-objdump -no-radare2-main --dump-symbols"; `S "SEE ALSO"; `P "$(b,bap-plugin-objdump)(1)" ]; - Config.when_ready (fun {get=_} -> main ()) + Config.when_ready (fun {get=_} -> main) \ No newline at end of file From fcdf8ee78c8cc9201e9d100c1207e28eaaa9402b Mon Sep 17 00:00:00 2001 From: phosphorus Date: Sat, 6 Jun 2020 00:02:58 +0800 Subject: [PATCH 02/25] Fixes errors within oasis file --- oasis/radare2 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/oasis/radare2 b/oasis/radare2 index cf74eea97..47cc826c0 100644 --- a/oasis/radare2 +++ b/oasis/radare2 @@ -3,7 +3,7 @@ Flag radare2 Default: false Library objdump_plugin - Build$: flag(everything) || flag(objdump) + Build$: flag(everything) Path: plugins/radare2 FindlibName: bap-plugin-radare2 CompiledObject: best @@ -12,4 +12,4 @@ Library objdump_plugin zarith, bitvec, radaer2, yojson InternalModules: Radare2_main XMETADescription: use radare2 to provide a symbolizer - XMETAExtraLines: tags="objdump, radare2" + XMETAExtraLines: tags="symbol, radare2" From 0a3f07ce50d73cdff07b6a3356d3634aa31ce464 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Fri, 5 Jun 2020 23:01:25 -0700 Subject: [PATCH 03/25] fixes silly mistakes --- oasis/radare2 | 8 ++++---- plugins/radare2/radare2_main.ml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/oasis/radare2 b/oasis/radare2 index 47cc826c0..4610686ba 100644 --- a/oasis/radare2 +++ b/oasis/radare2 @@ -2,14 +2,14 @@ Flag radare2 Description: Build radare2 plugin Default: false -Library objdump_plugin - Build$: flag(everything) +Library radare2_plugin + Build$: flag(everything) || flag(radare2) Path: plugins/radare2 FindlibName: bap-plugin-radare2 CompiledObject: best BuildDepends: bap, re.pcre, regular, bap-core-theory, bap-future, core_kernel, bap-knowledge, - zarith, bitvec, radaer2, yojson + zarith, bitvec, radare2, yojson InternalModules: Radare2_main XMETADescription: use radare2 to provide a symbolizer - XMETAExtraLines: tags="symbol, radare2" + XMETAExtraLines: tags="symbolizer, radare2" diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index 5a0ab0a57..6710e7f07 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -55,7 +55,7 @@ let () = `P "To view the symbols after running the plugin:"; `P "$(b, bap) $(i,executable) --no-objdump --dump-symbols "; `P "To view symbols without this plugin:"; - `P "$(b, bap) $(i,executable) --no-objdump -no-radare2-main --dump-symbols"; + `P "$(b, bap) $(i,executable) --no-objdump --no-radare2 --dump-symbols"; `S "SEE ALSO"; `P "$(b,bap-plugin-objdump)(1)" ]; From b8e8ce114847c130fa18934ebdb567469bb65cd5 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Wed, 10 Jun 2020 13:07:36 +0800 Subject: [PATCH 04/25] use 'isj' to dump symbols --- plugins/radare2/radare2_main.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index 6710e7f07..f63bdebdd 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -30,9 +30,9 @@ let provide_radare2 file = let accept name addr = Hashtbl.set funcs addr name in let extract name json = Yojson.Basic.Util.member name json in try - let symbol_list = Yojson.Basic.Util.to_list (R2.with_command_j "aaa;aflj" file) in + let symbol_list = Yojson.Basic.Util.to_list (R2.with_command_j "isj" file) in List.fold symbol_list ~init:() ~f:(fun () symbol -> - accept (Yojson.Basic.Util.to_string (extract "name" symbol)) (Yojson.Basic.Util.to_int (extract "offset" symbol) |> Z.of_int) + accept (Yojson.Basic.Util.to_string (extract "name" symbol)) (Yojson.Basic.Util.to_int (extract "vaddr" symbol) |> Z.of_int) ); if Hashtbl.length funcs = 0 then warning "failed to obtain symbols"; @@ -53,9 +53,9 @@ let () = `P "This plugin provides a symbolizer based on radare2."; `S "EXAMPLES"; `P "To view the symbols after running the plugin:"; - `P "$(b, bap) $(i,executable) --no-objdump --dump-symbols "; + `P "$(b, bap) $(i,executable) --dump-symbols "; `P "To view symbols without this plugin:"; - `P "$(b, bap) $(i,executable) --no-objdump --no-radare2 --dump-symbols"; + `P "$(b, bap) $(i,executable) --no-radare2 --dump-symbols"; `S "SEE ALSO"; `P "$(b,bap-plugin-objdump)(1)" ]; From 2c6dfd37c5c29311247df77fa49fe8e2aba90e64 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Fri, 12 Jun 2020 21:36:46 +0800 Subject: [PATCH 05/25] thumb lifter draft --- plugins/arm_thumb/.merlin | 1 + plugins/arm_thumb/thumb.ml | 72 +++++++++++++++++++ plugins/arm_thumb/thumb_defs.ml | 119 +++++++++++++++++++++++++++++++ plugins/arm_thumb/thumb_env.ml | 72 +++++++++++++++++++ plugins/arm_thumb/thumb_flags.ml | 51 +++++++++++++ 5 files changed, 315 insertions(+) create mode 100644 plugins/arm_thumb/.merlin create mode 100644 plugins/arm_thumb/thumb.ml create mode 100644 plugins/arm_thumb/thumb_defs.ml create mode 100644 plugins/arm_thumb/thumb_env.ml create mode 100644 plugins/arm_thumb/thumb_flags.ml diff --git a/plugins/arm_thumb/.merlin b/plugins/arm_thumb/.merlin new file mode 100644 index 000000000..2fb3f0bc1 --- /dev/null +++ b/plugins/arm_thumb/.merlin @@ -0,0 +1 @@ +REC \ No newline at end of file diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml new file mode 100644 index 000000000..a10abadf0 --- /dev/null +++ b/plugins/arm_thumb/thumb.ml @@ -0,0 +1,72 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Defs = Thumb_defs +module Flags = Thumb_flags.Flags + +let package = "arm-thumb" + +type insns = Defs.insn * (Defs.op list) + +exception Lift_Error of string + +module Thumb(Core : Theory.Core) = struct + open Core + open Defs + module Env = Thumb_env.Env + + module Flags = Flags(Core) + + let skip = perform Theory.Effect.Sort.bot + let pass = perform Theory.Effect.Sort.bot + + let nop = + KB.return @@ + Theory.Effect.empty Theory.Effect.Sort.top + + let reg = Env.load_reg + + let move eff = + KB.Object.create Theory.Program.cls >>= fun lbl -> + blk lbl eff skip + + let ctrl eff pc = + Theory.Label.for_addr pc >>= fun lbl -> + blk lbl pass eff + + let move_reg dest src = set (reg dest) (var (reg src)) + + let set_reg dest imm = + set (reg dest) (int Env.value (Bap.Std.Word.to_bitvec imm)) + + let mover dest src = match dest, src with + | `Reg d, `Reg s -> (move_reg d s) |> move + | _ -> raise (Lift_Error "dest or src is not a register") + + let movei8 dest imm = match dest, imm with + | `Reg d, `Imm v -> seq (set_reg d v) (Flags.set_nzf (reg d)) |> move + | _ -> raise (Lift_Error "incorrect oprands") + + let addrr d s1 s2 = match d, s1, s2 with + | `Reg d, `Reg s1, `Reg s2 -> + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (add (var s1) (var s2))) + (Flags.set_add (var s1) (var s2) d) + |> move + | _ -> raise (Lift_Error "oprends must be registers") + + let lift_move insn ops = + match insn, ops with + | `tMOVr, [dest; src] -> mover dest src + | `tMOVi8, [dest; imm] -> movei8 dest imm + | `tADDrr, [dest; src1; src2] -> addrr dest src1 src2 + | _ -> nop + + let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = + match ins with + | #move_insn -> lift_move ins ops + | _ -> nop + +end diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml new file mode 100644 index 000000000..eef3b861c --- /dev/null +++ b/plugins/arm_thumb/thumb_defs.ml @@ -0,0 +1,119 @@ +open Core_kernel +open Regular.Std +open Bap.Std + +type cond = [ + | `EQ + | `NE + | `CS + | `CC + | `MI + | `PL + | `VS + | `VC + | `HI + | `LS + | `GE + | `LT + | `GT + | `LE + | `AL +] [@@deriving bin_io, compare, sexp, enumerate] + +type nil_reg = [ `Nil ] +[@@deriving bin_io, compare, sexp, enumerate] + +(** General purpose registers *) +type gpr_reg = [ + | `R0 + | `R1 + | `R2 + | `R3 + | `R4 + | `R5 + | `R6 + | `R7 + | `LR + | `PC + | `SP +] [@@deriving bin_io, compare, sexp, enumerate] + +type gpr_or_nil = [nil_reg | gpr_reg] +[@@deriving bin_io, compare, sexp, enumerate] + +(** conditition code registers *) +type ccr_reg = [ + | `CPSR + | `SPSR + | `ITSTATE +] [@@deriving bin_io, compare, sexp, enumerate] + +type ccr_or_nil = [nil_reg | ccr_reg ] +[@@deriving bin_io, compare, sexp, enumerate] + +type non_nil_reg = [gpr_reg | ccr_reg] +[@@deriving bin_io, compare, sexp, enumerate] + +type reg = [nil_reg | non_nil_reg] +[@@deriving bin_io, compare, sexp, enumerate] + +type op = [ + | `Reg of reg + | `Imm of word +] [@@deriving bin_io, compare, sexp] + +type move_insn = [ + | `tMOVi8 (* Rd imm8 *) + | `tMOVr (* Rd Rs *) + | `tMOVSr (* Rd Rm affect CSPR *) + | `tADDrr (* Rd Rn Rm *) + | `tADDi3 (* Rd Rs imm *) + | `tMUL (* Rd Rn *) +] [@@deriving bin_io, compare, sexp, enumerate] + +(** Rd [reglist] *) +type mem_multi_insn = [ + | `tSTMIA + | `tLDMIA +] [@@deriving bin_io, compare, sexp, enumerate] + + +type mem_insn = [ + | mem_multi_insn +] [@@deriving bin_io, compare, sexp, enumerate] + +type branch_insn = [ + | `tBL +] [@@deriving bin_io, compare, sexp, enumerate] + +type insn = [ + | move_insn + | mem_insn + | branch_insn +] [@@deriving bin_io, compare, sexp, enumerate] + +(** Memory access operations *) + +(** Types for single-register memory access *) +type mode_r = Offset | PreIndex | PostIndex +type sign = Signed | Unsigned +type operation = Ld | St +type size = B | H | W | D +[@@deriving compare] + +(** Types for multiple-register memory access *) +type mode_m = IA | IB | DA | DB +type update_m = Update | NoUpdate + +(** Types for data movement operations *) +type arth = [`ADD | `ADC | `SBC | `RSC | `SUB | `RSB ] +type move = [`AND | `BIC | `EOR | `MOV | `MVN | `ORR ] +type data_oper = [ arth | move] + +type repair = [`POS | `NEG] [@@deriving compare] + +(** shift types *) +type shift = [`ASR | `LSL | `LSR | `ROR | `RRX] + + +type smul_size = BB | BT | TB | TT | D | DX | WB | WT \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_env.ml b/plugins/arm_thumb/thumb_env.ml new file mode 100644 index 000000000..ecff54e63 --- /dev/null +++ b/plugins/arm_thumb/thumb_env.ml @@ -0,0 +1,72 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = struct +type value +type byte +type reg_single +type half_byte + + let bit : Theory.Bool.t Theory.Value.sort = + Theory.Bool.t + + (** grps are defined by 3-bit indices *) + let reg_single : reg_single Theory.Bitv.t Theory.Value.sort = + Theory.Bitv.define 3 + + let value : value Theory.Bitv.t Theory.Value.sort = + Theory.Bitv.define 32 + + let half_byte : half_byte Theory.Bitv.t Theory.Value.sort = + Theory.Bitv.define 4 + + let byte : byte Theory.Bitv.t Theory.Value.sort = + Theory.Bitv.define 8 + + let heap_type = Theory.Mem.define value byte + + let heap = Theory.Var.define heap_type "mem" + + (** define grps *) + let r0 = Theory.Var.define value "r0" + let r1 = Theory.Var.define value "r1" + let r2 = Theory.Var.define value "r2" + let r3 = Theory.Var.define value "r3" + let r4 = Theory.Var.define value "r4" + let r5 = Theory.Var.define value "r5" + let r6 = Theory.Var.define value "r6" + let r7 = Theory.Var.define value "r7" + + let lr = Theory.Var.define value "lr" + let pc = Theory.Var.define value "pc" + let sp = Theory.Var.define value "sp" +(* The following are temporarily not used *) + let spsr = Theory.Var.define value "spsr" + let cpsr = Theory.Var.define value "cpsr" +(* The following are individual flag *) + let nf = Theory.Var.define bit "nf" + let zf = Theory.Var.define bit "zf" + let cf = Theory.Var.define bit "cf" + let vf = Theory.Var.define bit "vf" + let qf = Theory.Var.define bit "qf" + let ge = Theory.Var.define half_byte "ge" + +exception Unbound_Reg +module Defs = Thumb_defs + let load_reg (op : Defs.reg) = let open Thumb_defs in + match op with + | `R0 -> r0 + | `R1 -> r1 + | `R2 -> r2 + | `R3 -> r3 + | `R4 -> r4 + | `R5 -> r5 + | `R6 -> r6 + | `R7 -> r7 + | `LR -> lr + | `SP -> sp + | `PC -> pc + | _ -> raise Unbound_Reg + +end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_flags.ml b/plugins/arm_thumb/thumb_flags.ml new file mode 100644 index 000000000..4e7efcf84 --- /dev/null +++ b/plugins/arm_thumb/thumb_flags.ml @@ -0,0 +1,51 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = Thumb_env.Env + +module Flags(Core : Theory.Core) = struct +open Core + +let set_nzf r = + seq + (set (Env.nf) (msb (var r))) + (set (Env.zf) (eq (var r) (int Env.value (Bitvec.zero)))) + +let set_vnzf_add s1 s2 r = + seq + (set (Env.vf) (msb (logand (not (logxor s1 s2)) (logxor s1 (var r))))) + (set_nzf r) + +let set_add s1 s2 r = + seq + (set Env.cf (slt (var r) s1)) + (set_vnzf_add s1 s2 r) +end + +(* +let set_vnzf_sub s1 s2 r t = + Bil.move Env.vf (msb Bil.((s1 lxor s2) land (s1 lxor r))) :: + set_nzf r t + +let set_sub s1 s2 r t = + Bil.move Env.cf Bil.(s2 <= s1) :: set_vnzf_sub s1 s2 r t + +let set_adc s1 s2 r t = + let sum_with_carry = + let extend = Bil.(cast unsigned) (bitlen t + 1) in + Bil.(extend s1 + extend s2 + extend (var Env.cf)) in + Bil.move Env.cf (msb sum_with_carry) :: set_vnzf_add s1 s2 r t + +let set_sbc s1 s2 r t = set_adc s1 Bil.(lnot s2) r t + +let set_cf_data ~imm ~data = + let value = + let width = Word.bitwidth imm in + if Word.(of_int ~width 255 >= imm && imm >= zero width) then + let width = Word.bitwidth data in + if Word.(Int_exn.(data land of_int ~width 0xf00) = zero width) + then Bil.unknown "undefined" bool_t + else Bil.int Word.b0 + else msb Bil.(int imm) in + Bil.move Env.cf value*) \ No newline at end of file From 13ae335dd12b2c9a0b1056ad3b7c70c2ff03de64 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Fri, 12 Jun 2020 21:59:48 +0800 Subject: [PATCH 06/25] fix typo --- plugins/arm_thumb/thumb.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index a10abadf0..a60352d0f 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -46,7 +46,7 @@ module Thumb(Core : Theory.Core) = struct let movei8 dest imm = match dest, imm with | `Reg d, `Imm v -> seq (set_reg d v) (Flags.set_nzf (reg d)) |> move - | _ -> raise (Lift_Error "incorrect oprands") + | _ -> raise (Lift_Error "incorrect operands") let addrr d s1 s2 = match d, s1, s2 with | `Reg d, `Reg s1, `Reg s2 -> @@ -55,7 +55,7 @@ module Thumb(Core : Theory.Core) = struct (set d (add (var s1) (var s2))) (Flags.set_add (var s1) (var s2) d) |> move - | _ -> raise (Lift_Error "oprends must be registers") + | _ -> raise (Lift_Error "operands must be registers") let lift_move insn ops = match insn, ops with From 80f8dc850b38fc92f633bce4b3879476e7ac5dce Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Sun, 14 Jun 2020 13:44:34 +0800 Subject: [PATCH 07/25] chop 'sym.imp' prefix --- plugins/radare2/radare2_main.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index f63bdebdd..01dd69d52 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -31,8 +31,13 @@ let provide_radare2 file = let extract name json = Yojson.Basic.Util.member name json in try let symbol_list = Yojson.Basic.Util.to_list (R2.with_command_j "isj" file) in + let strip str = let open String in + match chop_prefix str ~prefix:"sym.imp." with + | Some str -> str + | None -> str + in List.fold symbol_list ~init:() ~f:(fun () symbol -> - accept (Yojson.Basic.Util.to_string (extract "name" symbol)) (Yojson.Basic.Util.to_int (extract "vaddr" symbol) |> Z.of_int) + accept (Yojson.Basic.Util.to_string (extract "name" symbol) |> strip) (Yojson.Basic.Util.to_int (extract "vaddr" symbol) |> Z.of_int) ); if Hashtbl.length funcs = 0 then warning "failed to obtain symbols"; From c03508af6623be9b509b3aed376ac2bc73751aac Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Sun, 14 Jun 2020 20:19:02 +0800 Subject: [PATCH 08/25] extends register set --- plugins/arm_thumb/thumb.ml | 59 +++++++++++++++++++++++++++++--- plugins/arm_thumb/thumb_defs.ml | 18 ++++++++-- plugins/arm_thumb/thumb_env.ml | 31 ++++++++++++++++- plugins/arm_thumb/thumb_flags.ml | 39 ++++++++++++++------- 4 files changed, 125 insertions(+), 22 deletions(-) diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index a60352d0f..2b4448bd3 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -18,6 +18,10 @@ module Thumb(Core : Theory.Core) = struct module Flags = Flags(Core) + let bool_as_bitv b = ite b (int Env.value Bitvec.one) (int Env.value Bitvec.zero) + + let word_as_bitv w = (int Env.value (Bap.Std.Word.to_bitvec w)) + let skip = perform Theory.Effect.Sort.bot let pass = perform Theory.Effect.Sort.bot @@ -27,6 +31,8 @@ module Thumb(Core : Theory.Core) = struct let reg = Env.load_reg + let reg_wide = Env.load_reg_wide + let move eff = KB.Object.create Theory.Program.cls >>= fun lbl -> blk lbl eff skip @@ -35,19 +41,50 @@ module Thumb(Core : Theory.Core) = struct Theory.Label.for_addr pc >>= fun lbl -> blk lbl pass eff - let move_reg dest src = set (reg dest) (var (reg src)) + let move_reg ?lreg:(lreg = reg) dest src = set (lreg dest) (var (lreg src)) - let set_reg dest imm = - set (reg dest) (int Env.value (Bap.Std.Word.to_bitvec imm)) + let set_reg ?lreg:(lreg = reg) dest imm = + set (lreg dest) (word_as_bitv imm) let mover dest src = match dest, src with - | `Reg d, `Reg s -> (move_reg d s) |> move + | `Reg d, `Reg s -> (move_reg ~lreg:reg_wide d s) |> move + | _ -> raise (Lift_Error "dest or src is not a register") + + let movesr dest src = match dest, src with + | `Reg d, `Reg s -> seq (move_reg d s) (Flags.set_nzf (reg d)) |> move | _ -> raise (Lift_Error "dest or src is not a register") let movei8 dest imm = match dest, imm with | `Reg d, `Imm v -> seq (set_reg d v) (Flags.set_nzf (reg d)) |> move | _ -> raise (Lift_Error "incorrect operands") + let mul dest src = match dest, src with + | `Reg d, `Reg s -> + let (dest, src) = (reg d, reg s) in + seq + (set dest (mul (var dest) (var src))) + (Flags.set_nzf dest) + |> move + | _ -> raise (Lift_Error "dest or src is not a register") + + let addi3 dest src imm = match dest, src, imm with + | `Reg d, `Reg s, `Imm v -> + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + seq + (set d (add (var s1) s2)) + (Flags.set_add (var s1) s2 d) + |> move + | _ -> raise (Lift_Error "incorrect operands") + + let addi8 dest imm = match dest, imm with + | `Reg d, `Imm v -> + let (d, s) = (reg d, word_as_bitv v) in + seq + (set d (add (var d) s)) + (Flags.set_add (var d) s d) + |> move + | _ -> raise (Lift_Error "incorrect operands") + let addrr d s1 s2 = match d, s1, s2 with | `Reg d, `Reg s1, `Reg s2 -> let (d, s1, s2) = (reg d, reg s1, reg s2) in @@ -57,11 +94,23 @@ module Thumb(Core : Theory.Core) = struct |> move | _ -> raise (Lift_Error "operands must be registers") + let adc d s1 s2 = match d, s1, s2 with + | `Reg d, `Reg s1, `Reg s2 -> + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (add (add (var s1) (var s2)) (bool_as_bitv (var Env.cf)))) + (Flags.set_adc (var s1) (var s2) d) + |> move + | _ -> raise (Lift_Error "operands must be registers") + let lift_move insn ops = match insn, ops with + | `tADC, [dest; src1; src2] -> adc dest src1 src2 + | `tADDrr, [dest; src1; src2] -> addrr dest src1 src2 | `tMOVr, [dest; src] -> mover dest src + | `tMOVSr, [dest; src] -> movesr dest src | `tMOVi8, [dest; imm] -> movei8 dest imm - | `tADDrr, [dest; src1; src2] -> addrr dest src1 src2 + | `tMUL, [dest; src] -> mul dest src | _ -> nop let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index eef3b861c..9e23fe09f 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -33,6 +33,12 @@ type gpr_reg = [ | `R5 | `R6 | `R7 +(* all the ARM GRPs are still needed *) + | `R8 + | `R9 + | `R10 + | `R11 + | `R12 | `LR | `PC | `SP @@ -61,13 +67,19 @@ type op = [ | `Reg of reg | `Imm of word ] [@@deriving bin_io, compare, sexp] - +(** all the `mov` series, registers marked with `e` means extended *) type move_insn = [ | `tMOVi8 (* Rd imm8 *) - | `tMOVr (* Rd Rs *) + | `tMOVr (* Rde Rse *) | `tMOVSr (* Rd Rm affect CSPR *) - | `tADDrr (* Rd Rn Rm *) + | `tADC (* Rd Rn Rm *) | `tADDi3 (* Rd Rs imm *) + | `tADDi8 (* Rd imm *) + | `tADDrr (* Rd Rn Rm *) + | `tADDhirr (* Rde Rse *) + | `tADR (* Rd imm *) + | `tADDrSPi (* Rd imm *) + | `tADDspi (* imm *) | `tMUL (* Rd Rn *) ] [@@deriving bin_io, compare, sexp, enumerate] diff --git a/plugins/arm_thumb/thumb_env.ml b/plugins/arm_thumb/thumb_env.ml index ecff54e63..07368df8c 100644 --- a/plugins/arm_thumb/thumb_env.ml +++ b/plugins/arm_thumb/thumb_env.ml @@ -26,7 +26,7 @@ type half_byte let heap_type = Theory.Mem.define value byte - let heap = Theory.Var.define heap_type "mem" + let memory = Theory.Var.define heap_type "mem" (** define grps *) let r0 = Theory.Var.define value "r0" @@ -38,6 +38,13 @@ type half_byte let r6 = Theory.Var.define value "r6" let r7 = Theory.Var.define value "r7" + (** grps which are not commonly accessible *) + let r8 = Theory.Var.define value "r8" + let r9 = Theory.Var.define value "r9" + let r10 = Theory.Var.define value "r10" + let r11 = Theory.Var.define value "r11" + let r12 = Theory.Var.define value "r12" + let lr = Theory.Var.define value "lr" let pc = Theory.Var.define value "pc" let sp = Theory.Var.define value "sp" @@ -54,6 +61,28 @@ type half_byte exception Unbound_Reg module Defs = Thumb_defs + + (* to elimiate ambiguity *) + let load_reg_wide (op : Defs.reg) = let open Thumb_defs in + match op with + | `R0 -> r0 + | `R1 -> r1 + | `R2 -> r2 + | `R3 -> r3 + | `R4 -> r4 + | `R5 -> r5 + | `R6 -> r6 + | `R7 -> r7 + | `R8 -> r8 + | `R9 -> r9 + | `R10 -> r10 + | `R11 -> r11 + | `R12 -> r12 + | `LR -> lr + | `SP -> sp + | `PC -> pc + | _ -> raise Unbound_Reg + let load_reg (op : Defs.reg) = let open Thumb_defs in match op with | `R0 -> r0 diff --git a/plugins/arm_thumb/thumb_flags.ml b/plugins/arm_thumb/thumb_flags.ml index 4e7efcf84..56c7be491 100644 --- a/plugins/arm_thumb/thumb_flags.ml +++ b/plugins/arm_thumb/thumb_flags.ml @@ -6,6 +6,10 @@ module Env = Thumb_env.Env module Flags(Core : Theory.Core) = struct open Core +type value_extend + +let value : value_extend Theory.Bitv.t Theory.Value.sort = + Theory.Bitv.define 33 (* 33 bits for carry flag inspection *) let set_nzf r = seq @@ -21,23 +25,32 @@ let set_add s1 s2 r = seq (set Env.cf (slt (var r) s1)) (set_vnzf_add s1 s2 r) -end -(* -let set_vnzf_sub s1 s2 r t = - Bil.move Env.vf (msb Bil.((s1 lxor s2) land (s1 lxor r))) :: - set_nzf r t +let set_vnzf_sub s1 s2 r = + seq + (set (Env.vf) (msb (logand (logxor s1 s2) (logxor s1 (var r))))) + (set_nzf r) -let set_sub s1 s2 r t = - Bil.move Env.cf Bil.(s2 <= s1) :: set_vnzf_sub s1 s2 r t +let set_sub s1 s2 r = + seq + (set Env.cf (sle s2 s1)) + (set_vnzf_add s1 s2 r) -let set_adc s1 s2 r t = - let sum_with_carry = - let extend = Bil.(cast unsigned) (bitlen t + 1) in - Bil.(extend s1 + extend s2 + extend (var Env.cf)) in - Bil.move Env.cf (msb sum_with_carry) :: set_vnzf_add s1 s2 r t +let as_bitv b = ite b (int value Bitvec.one) (int value Bitvec.zero) -let set_sbc s1 s2 r t = set_adc s1 Bil.(lnot s2) r t +let set_adc s1 s2 r = + let sum_with_carry = + let extend = cast value b0 in + add (add (extend s1) (extend s2)) (as_bitv (var Env.cf)) + in seq + (set Env.cf (msb sum_with_carry)) + (set_vnzf_add s1 s2 r) + +let set_sbc s1 s2 r = set_adc s1 (not s2) r + +end + +(* let set_cf_data ~imm ~data = let value = From 3bb5fabc95f1e78e20eda5e4c1a2d201e56a79f9 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Sun, 14 Jun 2020 21:39:44 +0800 Subject: [PATCH 09/25] complete & extract move-like instructions --- plugins/arm_thumb/thumb.ml | 87 +++------------- plugins/arm_thumb/thumb_defs.ml | 8 ++ plugins/arm_thumb/thumb_env.ml | 2 + plugins/arm_thumb/thumb_flags.ml | 2 +- plugins/arm_thumb/thumb_mov.ml | 167 +++++++++++++++++++++++++++++++ 5 files changed, 194 insertions(+), 72 deletions(-) create mode 100644 plugins/arm_thumb/thumb_mov.ml diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 2b4448bd3..19417bf83 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -9,18 +9,12 @@ let package = "arm-thumb" type insns = Defs.insn * (Defs.op list) -exception Lift_Error of string - module Thumb(Core : Theory.Core) = struct open Core open Defs module Env = Thumb_env.Env - module Flags = Flags(Core) - - let bool_as_bitv b = ite b (int Env.value Bitvec.one) (int Env.value Bitvec.zero) - - let word_as_bitv w = (int Env.value (Bap.Std.Word.to_bitvec w)) + module Mov = Thumb_mov.Mov(Core) let skip = perform Theory.Effect.Sort.bot let pass = perform Theory.Effect.Sort.bot @@ -41,81 +35,32 @@ module Thumb(Core : Theory.Core) = struct Theory.Label.for_addr pc >>= fun lbl -> blk lbl pass eff - let move_reg ?lreg:(lreg = reg) dest src = set (lreg dest) (var (lreg src)) - - let set_reg ?lreg:(lreg = reg) dest imm = - set (lreg dest) (word_as_bitv imm) - - let mover dest src = match dest, src with - | `Reg d, `Reg s -> (move_reg ~lreg:reg_wide d s) |> move - | _ -> raise (Lift_Error "dest or src is not a register") - - let movesr dest src = match dest, src with - | `Reg d, `Reg s -> seq (move_reg d s) (Flags.set_nzf (reg d)) |> move - | _ -> raise (Lift_Error "dest or src is not a register") - - let movei8 dest imm = match dest, imm with - | `Reg d, `Imm v -> seq (set_reg d v) (Flags.set_nzf (reg d)) |> move - | _ -> raise (Lift_Error "incorrect operands") - - let mul dest src = match dest, src with - | `Reg d, `Reg s -> - let (dest, src) = (reg d, reg s) in - seq - (set dest (mul (var dest) (var src))) - (Flags.set_nzf dest) - |> move - | _ -> raise (Lift_Error "dest or src is not a register") - - let addi3 dest src imm = match dest, src, imm with - | `Reg d, `Reg s, `Imm v -> - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - seq - (set d (add (var s1) s2)) - (Flags.set_add (var s1) s2 d) - |> move - | _ -> raise (Lift_Error "incorrect operands") - - let addi8 dest imm = match dest, imm with - | `Reg d, `Imm v -> - let (d, s) = (reg d, word_as_bitv v) in - seq - (set d (add (var d) s)) - (Flags.set_add (var d) s d) - |> move - | _ -> raise (Lift_Error "incorrect operands") - - let addrr d s1 s2 = match d, s1, s2 with - | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (add (var s1) (var s2))) - (Flags.set_add (var s1) (var s2) d) - |> move - | _ -> raise (Lift_Error "operands must be registers") - - let adc d s1 s2 = match d, s1, s2 with - | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (add (add (var s1) (var s2)) (bool_as_bitv (var Env.cf)))) - (Flags.set_adc (var s1) (var s2) d) - |> move - | _ -> raise (Lift_Error "operands must be registers") - let lift_move insn ops = + let open Mov in match insn, ops with | `tADC, [dest; src1; src2] -> adc dest src1 src2 + | `tADDi3, [dest; src; imm] -> addi3 dest src imm + | `tADDi8, [dest; imm] -> addi8 dest imm | `tADDrr, [dest; src1; src2] -> addrr dest src1 src2 + | `tADDhirr, [dest; src] -> addhirr dest src + | `tADR, [dest; imm] -> adr dest imm + | `tADDrSPi, [dest; imm] -> addrspi dest imm + | `tADDspi, [imm] -> addspi imm | `tMOVr, [dest; src] -> mover dest src | `tMOVSr, [dest; src] -> movesr dest src | `tMOVi8, [dest; imm] -> movei8 dest imm | `tMUL, [dest; src] -> mul dest src - | _ -> nop + | `tMVN, [dest; src] -> movenot dest src + | `tSBC, [dest; src] -> sbc dest src + | `tSUBi3, [dest; src; imm] -> subi3 dest src imm + | `tSUBi8, [dest; imm] -> subi8 dest imm + | `tSUBrr, [dest; src1; src2] -> subrr dest src1 src2 + | `tSUBspi, [imm] -> subspi imm + | _ -> pass let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = match ins with - | #move_insn -> lift_move ins ops + | #move_insn -> lift_move ins ops |> move | _ -> nop end diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index 9e23fe09f..4a58ece93 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -2,6 +2,8 @@ open Core_kernel open Regular.Std open Bap.Std +exception Lift_Error of string + type cond = [ | `EQ | `NE @@ -72,6 +74,7 @@ type move_insn = [ | `tMOVi8 (* Rd imm8 *) | `tMOVr (* Rde Rse *) | `tMOVSr (* Rd Rm affect CSPR *) + | `tMVN (* Rd Rm *) | `tADC (* Rd Rn Rm *) | `tADDi3 (* Rd Rs imm *) | `tADDi8 (* Rd imm *) @@ -80,6 +83,11 @@ type move_insn = [ | `tADR (* Rd imm *) | `tADDrSPi (* Rd imm *) | `tADDspi (* imm *) + | `tSBC (* Rd Rm *) + | `tSUBi3 (* See the corresponding ADD insns. *) + | `tSUBi8 + | `tSUBrr + | `tSUBspi | `tMUL (* Rd Rn *) ] [@@deriving bin_io, compare, sexp, enumerate] diff --git a/plugins/arm_thumb/thumb_env.ml b/plugins/arm_thumb/thumb_env.ml index 07368df8c..cbacc779d 100644 --- a/plugins/arm_thumb/thumb_env.ml +++ b/plugins/arm_thumb/thumb_env.ml @@ -58,6 +58,8 @@ type half_byte let vf = Theory.Var.define bit "vf" let qf = Theory.Var.define bit "qf" let ge = Theory.Var.define half_byte "ge" +(* psuedo register storing temporary computations *) + let tmp = Theory.Var.define value "tmp" exception Unbound_Reg module Defs = Thumb_defs diff --git a/plugins/arm_thumb/thumb_flags.ml b/plugins/arm_thumb/thumb_flags.ml index 56c7be491..ba58246b6 100644 --- a/plugins/arm_thumb/thumb_flags.ml +++ b/plugins/arm_thumb/thumb_flags.ml @@ -34,7 +34,7 @@ let set_vnzf_sub s1 s2 r = let set_sub s1 s2 r = seq (set Env.cf (sle s2 s1)) - (set_vnzf_add s1 s2 r) + (set_vnzf_sub s1 s2 r) let as_bitv b = ite b (int value Bitvec.one) (int value Bitvec.zero) diff --git a/plugins/arm_thumb/thumb_mov.ml b/plugins/arm_thumb/thumb_mov.ml new file mode 100644 index 000000000..d132c3305 --- /dev/null +++ b/plugins/arm_thumb/thumb_mov.ml @@ -0,0 +1,167 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = Thumb_env.Env +module Flags = Thumb_flags.Flags + +exception Lift_Error = Thumb_defs.Lift_Error + +module Mov(Core : Theory.Core) = struct +open Core + + module Flags = Flags(Core) + + let reg = Env.load_reg + + let reg_wide = Env.load_reg_wide + + let bool_as_bitv b = ite b (int Env.value Bitvec.one) (int Env.value Bitvec.zero) + + let word_as_bitv w = (int Env.value (Bap.Std.Word.to_bitvec w)) + + let bitv_of imm = word_as_bitv (Bap.Std.Word.of_int 32 imm) + + let move_reg ?lreg:(lreg = reg) dest src = set (lreg dest) (var (lreg src)) + + let set_reg ?lreg:(lreg = reg) dest imm = + set (lreg dest) (word_as_bitv imm) + + let mover dest src = match dest, src with + | `Reg d, `Reg s -> (move_reg ~lreg:reg_wide d s) + | _ -> raise (Lift_Error "dest or src is not a register") + + let movesr dest src = match dest, src with + | `Reg d, `Reg s -> seq (move_reg d s) (Flags.set_nzf (reg d)) + | _ -> raise (Lift_Error "dest or src is not a register") + + let movei8 dest imm = match dest, imm with + | `Reg d, `Imm v -> seq (set_reg d v) (Flags.set_nzf (reg d)) + | _ -> raise (Lift_Error "incorrect operands") + + let movenot dest src = match dest, src with + | `Reg d, `Reg s -> + let (dest, src) = (reg d, reg s) in + seq + (set dest (not (var src))) + (Flags.set_nzf dest) + | _ -> raise (Lift_Error "dest or src is not a register") + + let mul dest src = match dest, src with + | `Reg d, `Reg s -> + let (dest, src) = (reg d, reg s) in + seq + (set dest (mul (var dest) (var src))) + (Flags.set_nzf dest) + | _ -> raise (Lift_Error "dest or src is not a register") + + let addi3 dest src imm = match dest, src, imm with + | `Reg d, `Reg s, `Imm v -> + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + seq + (set d (add (var s1) s2)) + (Flags.set_add (var s1) s2 d) + | _ -> raise (Lift_Error "incorrect operands") + + let subi3 dest src imm = match dest, src, imm with + | `Reg d, `Reg s, `Imm v -> + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + seq + (set d (sub (var s1) s2)) + (Flags.set_sub (var s1) s2 d) + | _ -> raise (Lift_Error "incorrect operands") + + (* a temp value is introduced here *) + let addi8 dest imm = match dest, imm with + | `Reg d, `Imm v -> + let (d, s) = (reg d, word_as_bitv v) in + seq + (seq + (set Env.tmp (var d)) + (set d (add (var d) s)) + ) + (Flags.set_add (var Env.tmp) s d) + | _ -> raise (Lift_Error "incorrect operands") + + let subi8 dest imm = match dest, imm with + | `Reg d, `Imm v -> + let (d, s) = (reg d, word_as_bitv v) in + seq + (seq + (set Env.tmp (var d)) + (set d (sub (var d) s)) + ) + (Flags.set_sub (var Env.tmp) s d) + | _ -> raise (Lift_Error "incorrect operands") + + let addrr d s1 s2 = match d, s1, s2 with + | `Reg d, `Reg s1, `Reg s2 -> + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (add (var s1) (var s2))) + (Flags.set_add (var s1) (var s2) d) + | _ -> raise (Lift_Error "operands must be registers") + + let subrr d s1 s2 = match d, s1, s2 with + | `Reg d, `Reg s1, `Reg s2 -> + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (sub (var s1) (var s2))) + (Flags.set_sub (var s1) (var s2) d) + | _ -> raise (Lift_Error "operands must be registers") + + let addhirr d s = match d, s with + | `Reg d, `Reg s -> + let (d, s) = (reg_wide d, reg_wide s) in + set d (add (var d) (var s)) + | _ -> raise (Lift_Error "operands must be registers") + + (* Rd = (PC and 0xfffffffc) + (imm << 2) *) + let adr dest imm = match dest, imm with + | `Reg d, `Imm v -> + let shift x = bitv_of 2 |> shiftl b0 x in + let (d, s) = (reg d, word_as_bitv v) in + set d (add (logand (var Env.pc) (bitv_of 0xFFFFFFFC)) (shift s)) + | _ -> raise (Lift_Error "incorrect operands") + + let addrspi dest imm = match dest, imm with + | `Reg d, `Imm v -> + let shift x = bitv_of 2 |> shiftl b0 x in + let (d, s) = (reg d, word_as_bitv v) in + set d (add (var Env.sp) (shift s)) + | _ -> raise (Lift_Error "incorrect operands") + + let addspi imm = match imm with + | `Imm v -> + let shift x = bitv_of 2 |> shiftl b0 x in + let s = word_as_bitv v in + set Env.sp (add (var Env.sp) (shift s)) + | _ -> raise (Lift_Error "imm must be an immediate") + + let subspi imm = match imm with + | `Imm v -> + let shift x = bitv_of 2 |> shiftl b0 x in + let s = word_as_bitv v in + set Env.sp (sub (var Env.sp) (shift s)) + | _ -> raise (Lift_Error "imm must be an immediate") + + let adc d s1 s2 = match d, s1, s2 with + | `Reg d, `Reg s1, `Reg s2 -> + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (add (add (var s1) (var s2)) (bool_as_bitv (var Env.cf)))) + (Flags.set_adc (var s1) (var s2) d) + | _ -> raise (Lift_Error "operands must be registers") + + let sbc d s = match d, s with + | `Reg d, `Reg s -> + let (d, s) = (reg d, reg s) in + seq + (seq + (set Env.tmp (var d)) + (set d (add (sub (var d) (var s)) (bool_as_bitv (var Env.cf)))) + ) + (Flags.set_sbc (var Env.tmp) (var s) d) + | _ -> raise (Lift_Error "operands must be registers") + +end \ No newline at end of file From 246dcae917f6353de1d7812c3077b47ba6d3212d Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Mon, 15 Jun 2020 15:48:20 +0800 Subject: [PATCH 10/25] single memory l/s instructions --- plugins/arm_thumb/thumb.ml | 45 ++++++++++++++++++++++++++++++++ plugins/arm_thumb/thumb_defs.ml | 19 +++++++++++++- plugins/arm_thumb/thumb_env.ml | 4 +++ plugins/arm_thumb/thumb_mem.ml | 46 +++++++++++++++++++++++++++++++++ plugins/arm_thumb/thumb_mov.ml | 16 ++---------- plugins/arm_thumb/thumb_util.ml | 24 +++++++++++++++++ 6 files changed, 139 insertions(+), 15 deletions(-) create mode 100644 plugins/arm_thumb/thumb_mem.ml create mode 100644 plugins/arm_thumb/thumb_util.ml diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 19417bf83..6f4617017 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -15,6 +15,10 @@ module Thumb(Core : Theory.Core) = struct module Env = Thumb_env.Env module Mov = Thumb_mov.Mov(Core) + module Mem = Thumb_mem.Mem(Core) + module Utils = Thumb_util.Utils(Core) + + open Utils let skip = perform Theory.Effect.Sort.bot let pass = perform Theory.Effect.Sort.bot @@ -58,9 +62,50 @@ module Thumb(Core : Theory.Core) = struct | `tSUBspi, [imm] -> subspi imm | _ -> pass + let lift_mem insn ops = + let open Defs in + let open Mem in + match insn, ops with + | `tLDRi, [dest; src; imm] -> + lift_mem_single dest src ~src2:imm Ld W + | `tLDRr, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 Ld W + | `tLDRpci, [dest; imm] -> + lift_mem_single dest `PC ~src2:imm Ld W + | `tLDRspi, [dest; imm] -> + lift_mem_single dest `SP ~src2:imm Ld W + | `tLDRBi, [dest; src; imm] -> + lift_mem_single dest src ~src2:imm Ld B + | `tLDRBr, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 Ld B + | `tLDRHi, [dest; src; imm] -> + lift_mem_single dest src ~src2:imm Ld H + | `tLDRHr, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 Ld H + | `tLDRSB, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 Ld B ~sign:true + | `tLDRSH, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 Ld H ~sign:true + | `tSTRi, [dest; src; imm] -> + lift_mem_single dest src ~src2:imm St W + | `tSTRr, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 St W + | `tSTRspi, [dest; imm] -> + lift_mem_single dest `SP ~src2:imm St W + | `tSTRBi, [dest; src; imm] -> + lift_mem_single dest src ~src2:imm St B + | `tSTRBr, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 St B + | `tSTRHi, [dest; src; imm] -> + lift_mem_single dest src ~src2:imm St H + | `tSTRHr, [dest; src1; src2] -> + lift_mem_single dest src1 ~src2 St H + | _ -> pass + let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = match ins with | #move_insn -> lift_move ins ops |> move + | #mem_insn -> lift_mem ins ops |> move | _ -> nop end diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index 4a58ece93..069548991 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -99,6 +99,23 @@ type mem_multi_insn = [ type mem_insn = [ + | `tLDRi + | `tLDRr + | `tLDRpci + | `tLDRspi + | `tLDRBi + | `tLDRBr + | `tLDRHi + | `tLDRHr + | `tLDRSB + | `tLDRSH + | `tSTRi + | `tSTRr + | `tSTRspi + | `tSTRBi + | `tSTRBr + | `tSTRHi + | `tSTRHr | mem_multi_insn ] [@@deriving bin_io, compare, sexp, enumerate] @@ -118,7 +135,7 @@ type insn = [ type mode_r = Offset | PreIndex | PostIndex type sign = Signed | Unsigned type operation = Ld | St -type size = B | H | W | D +type size = B | H | W [@@deriving compare] (** Types for multiple-register memory access *) diff --git a/plugins/arm_thumb/thumb_env.ml b/plugins/arm_thumb/thumb_env.ml index cbacc779d..fc6e2ed01 100644 --- a/plugins/arm_thumb/thumb_env.ml +++ b/plugins/arm_thumb/thumb_env.ml @@ -7,6 +7,7 @@ type value type byte type reg_single type half_byte +type half_word let bit : Theory.Bool.t Theory.Value.sort = Theory.Bool.t @@ -15,6 +16,9 @@ type half_byte let reg_single : reg_single Theory.Bitv.t Theory.Value.sort = Theory.Bitv.define 3 + let half_word : half_word Theory.Bitv.t Theory.Value.sort = + Theory.Bitv.define 32 + let value : value Theory.Bitv.t Theory.Value.sort = Theory.Bitv.define 32 diff --git a/plugins/arm_thumb/thumb_mem.ml b/plugins/arm_thumb/thumb_mem.ml new file mode 100644 index 000000000..7a479732e --- /dev/null +++ b/plugins/arm_thumb/thumb_mem.ml @@ -0,0 +1,46 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = Thumb_env.Env +module Defs = Thumb_defs + +exception Lift_Error = Thumb_defs.Lift_Error + +module Mem(Core : Theory.Core) = struct +open Core + + module Utils = Thumb_util.Utils(Core) + + open Utils + + let lift_mem_single ?(sign = false) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = + let open Defs in + let dest = match dest with + | `Reg r -> reg r + | _ -> raise (Lift_Error "`dest` must be a register") + in + let shift x = bitv_of 2 |> shiftl b0 x in + let address = match src1, src2 with + | `Reg s, None -> reg s |> var + | `Reg s1, Some (`Reg s2) -> + add (reg s1 |> var) (reg s2 |> var) + | `Reg s, Some (`Imm v) -> + add (reg_wide s |> var) (word_as_bitv v |> shift) + | _ -> raise (Lift_Error "Unbound memory operation mode") + in match op with + | Ld -> + let extend = if sign then signed else unsigned in + let value = match size with + | W -> loadw Env.value b0 (var Env.memory) address + | H -> loadw Env.half_word b0 (var Env.memory) address |> extend Env.value + | B -> load (var Env.memory) address |> extend Env.value + in set dest value + | St -> + let mem = match size with + | W -> storew b0 (var Env.memory) address (var dest) + | H -> storew b0 (var Env.memory) address (cast Env.half_word b0 (var dest)) + | B -> store (var Env.memory) address (cast Env.byte b0 (var dest)) + in set Env.memory mem + +end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_mov.ml b/plugins/arm_thumb/thumb_mov.ml index d132c3305..7a603e1e2 100644 --- a/plugins/arm_thumb/thumb_mov.ml +++ b/plugins/arm_thumb/thumb_mov.ml @@ -10,22 +10,10 @@ exception Lift_Error = Thumb_defs.Lift_Error module Mov(Core : Theory.Core) = struct open Core + module Utils = Thumb_util.Utils(Core) module Flags = Flags(Core) - let reg = Env.load_reg - - let reg_wide = Env.load_reg_wide - - let bool_as_bitv b = ite b (int Env.value Bitvec.one) (int Env.value Bitvec.zero) - - let word_as_bitv w = (int Env.value (Bap.Std.Word.to_bitvec w)) - - let bitv_of imm = word_as_bitv (Bap.Std.Word.of_int 32 imm) - - let move_reg ?lreg:(lreg = reg) dest src = set (lreg dest) (var (lreg src)) - - let set_reg ?lreg:(lreg = reg) dest imm = - set (lreg dest) (word_as_bitv imm) + open Utils let mover dest src = match dest, src with | `Reg d, `Reg s -> (move_reg ~lreg:reg_wide d s) diff --git a/plugins/arm_thumb/thumb_util.ml b/plugins/arm_thumb/thumb_util.ml new file mode 100644 index 000000000..8a199e31d --- /dev/null +++ b/plugins/arm_thumb/thumb_util.ml @@ -0,0 +1,24 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = Thumb_env.Env + +module Utils(Core : Theory.Core) = struct +open Core + let reg = Env.load_reg + + let reg_wide = Env.load_reg_wide + + let bool_as_bitv b = ite b (int Env.value Bitvec.one) (int Env.value Bitvec.zero) + + let word_as_bitv w = (int Env.value (Bap.Std.Word.to_bitvec w)) + + let bitv_of imm = word_as_bitv (Bap.Std.Word.of_int 32 imm) + + let move_reg ?lreg:(lreg = reg) dest src = set (lreg dest) (var (lreg src)) + + let set_reg ?lreg:(lreg = reg) dest imm = + set (lreg dest) (word_as_bitv imm) + +end \ No newline at end of file From d64507fc75a01be113b5748892568e9cca347305 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Mon, 15 Jun 2020 16:47:36 +0800 Subject: [PATCH 11/25] multiple l/s instructions --- plugins/arm_thumb/thumb.ml | 17 ++++------- plugins/arm_thumb/thumb_defs.ml | 2 ++ plugins/arm_thumb/thumb_mem.ml | 53 +++++++++++++++++++++++++++++++++ plugins/arm_thumb/thumb_util.ml | 8 +++++ 4 files changed, 69 insertions(+), 11 deletions(-) diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 6f4617017..aae11ad4b 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -20,17 +20,6 @@ module Thumb(Core : Theory.Core) = struct open Utils - let skip = perform Theory.Effect.Sort.bot - let pass = perform Theory.Effect.Sort.bot - - let nop = - KB.return @@ - Theory.Effect.empty Theory.Effect.Sort.top - - let reg = Env.load_reg - - let reg_wide = Env.load_reg_wide - let move eff = KB.Object.create Theory.Program.cls >>= fun lbl -> blk lbl eff skip @@ -100,6 +89,12 @@ module Thumb(Core : Theory.Core) = struct lift_mem_single dest src ~src2:imm St H | `tSTRHr, [dest; src1; src2] -> lift_mem_single dest src1 ~src2 St H + | `tSTMIA, dest :: src_list -> + store_multiple dest src_list + | `tPUSH, src_list -> + push_multiple src_list + | `tPOP, src_list -> + pop_multiple src_list (* TODO: PC might have been changed *) | _ -> pass let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index 069548991..e0ced6982 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -95,6 +95,8 @@ type move_insn = [ type mem_multi_insn = [ | `tSTMIA | `tLDMIA + | `tPOP + | `tPUSH ] [@@deriving bin_io, compare, sexp, enumerate] diff --git a/plugins/arm_thumb/thumb_mem.ml b/plugins/arm_thumb/thumb_mem.ml index 7a479732e..2deb71509 100644 --- a/plugins/arm_thumb/thumb_mem.ml +++ b/plugins/arm_thumb/thumb_mem.ml @@ -14,6 +14,59 @@ open Core open Utils + (* The original ARM lifter implement this in a BIL loop-style for some reason *) + let store_multiple dest src_list = + match dest with + | `Reg r -> let r = reg r in List.fold src_list ~init:pass + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (storew b0 (var Env.memory) (var r) (var src) |> set Env.memory) + (set r (add (var r) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + ) + | _ -> raise (Lift_Error "`dest` must be a register") + + let load_multiple dest src_list = + match dest with + | `Reg r -> let r = reg r in List.fold src_list ~init:pass + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (loadw Env.value b0 (var Env.memory) (var r) |> set src) + (set r (add (var r) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + ) + | _ -> raise (Lift_Error "`dest` must be a register") + (* the `R` bit is automatically resolved *) + let push_multiple src_list = + let shift x = bitv_of 2 |> shiftl b0 x in + let offset = List.length src_list |> bitv_of |> shift in + let initial = set Env.tmp (sub (var Env.sp) offset) in + seq (List.fold src_list ~init:initial + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (storew b0 (var Env.memory) (var Env.tmp) (var src) |> set Env.memory) + (set Env.tmp (add (var Env.tmp) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + )) (set Env.sp (sub (var Env.sp) offset)) + (* TODO: PC might change here *) + let pop_multiple src_list = + let initial = set Env.tmp (var Env.sp) in + seq (List.fold src_list ~init:initial + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (loadw Env.value b0 (var Env.memory) (var Env.tmp) |> set src) + (set Env.tmp (add (var Env.tmp) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + )) (set Env.sp (var Env.tmp)) + let lift_mem_single ?(sign = false) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = let open Defs in let dest = match dest with diff --git a/plugins/arm_thumb/thumb_util.ml b/plugins/arm_thumb/thumb_util.ml index 8a199e31d..f3b991cf5 100644 --- a/plugins/arm_thumb/thumb_util.ml +++ b/plugins/arm_thumb/thumb_util.ml @@ -6,6 +6,14 @@ module Env = Thumb_env.Env module Utils(Core : Theory.Core) = struct open Core + + let skip : Theory.ctrl Theory.eff = perform Theory.Effect.Sort.bot + let pass : Theory.data Theory.eff = perform Theory.Effect.Sort.bot + + let nop = + KB.return @@ + Theory.Effect.empty Theory.Effect.Sort.top + let reg = Env.load_reg let reg_wide = Env.load_reg_wide From 00b2fcd0a56cab5c87487b9a2f910c06b27b97cb Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Mon, 15 Jun 2020 19:20:23 +0800 Subject: [PATCH 12/25] complete all bitwise move-like instructions --- plugins/arm_thumb/thumb.ml | 20 +++ plugins/arm_thumb/thumb_defs.ml | 24 +++ plugins/arm_thumb/thumb_env.ml | 4 + plugins/arm_thumb/thumb_mov.ml | 265 ++++++++++++++++++++++++++++++++ 4 files changed, 313 insertions(+) diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index aae11ad4b..70900fb98 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -49,6 +49,26 @@ module Thumb(Core : Theory.Core) = struct | `tSUBi8, [dest; imm] -> subi8 dest imm | `tSUBrr, [dest; src1; src2] -> subrr dest src1 src2 | `tSUBspi, [imm] -> subspi imm + | `tAND, [dest; src] -> andrr dest src + | `tASRri, [dest; src; imm] -> asri dest src imm + | `tASRrr, [dest; src] -> asrr dest src + | `tBIC, [dest; src] -> bic dest src + | `tCMNz, [dest; src] -> cmnz dest src + | `tCMPi8, [dest; imm] -> cmpi8 dest imm + | `tCMPr, [dest; src] -> cmpr dest src + | `tCMPhir, [dest; src] -> cmphir dest src + | `tEOR, [dest; src] -> eor dest src + | `tLSLri, [dest; src; imm] -> lsli dest src imm + | `tLSLrr, [dest; src] -> lslr dest src + | `tLSRri, [dest; src; imm] -> lsri dest src imm + | `tLSRrr, [dest; src] -> lsrr dest src + | `tORR, [dest; src] -> orr dest src + | `tRSB, [dest; src; imm (* placeholder *)] -> rsb dest src imm + | `tREV, [dest; src] -> rev dest src + | `tREV16, [dest; src] -> rev16 dest src + | `tREVSH, [dest; src] -> revsh dest src + | `tROR, [dest; src] -> ror dest src + | `tTST, [dest; src] -> tst dest src | _ -> pass let lift_mem insn ops = diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index e0ced6982..8ec9513af 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -83,14 +83,38 @@ type move_insn = [ | `tADR (* Rd imm *) | `tADDrSPi (* Rd imm *) | `tADDspi (* imm *) + | `tAND + | `tASRri + | `tASRrr + | `tBIC + | `tCMNz + | `tCMPi8 + | `tCMPr + | `tCMPhir + | `tEOR + | `tLSLri + | `tLSLrr + | `tLSRri + | `tLSRrr + | `tORR + | `tRSB (* NEG *) + | `tREV + | `tREV16 + | `tREVSH + | `tROR | `tSBC (* Rd Rm *) | `tSUBi3 (* See the corresponding ADD insns. *) | `tSUBi8 | `tSUBrr | `tSUBspi + | `tTST | `tMUL (* Rd Rn *) ] [@@deriving bin_io, compare, sexp, enumerate] +type bits_insn = [ + | `NA +] + (** Rd [reglist] *) type mem_multi_insn = [ | `tSTMIA diff --git a/plugins/arm_thumb/thumb_env.ml b/plugins/arm_thumb/thumb_env.ml index fc6e2ed01..5a8d08882 100644 --- a/plugins/arm_thumb/thumb_env.ml +++ b/plugins/arm_thumb/thumb_env.ml @@ -8,10 +8,14 @@ type byte type reg_single type half_byte type half_word +type bit_val let bit : Theory.Bool.t Theory.Value.sort = Theory.Bool.t + let bit_val : bit_val Theory.Bitv.t Theory.Value.sort = + Theory.Bitv.define 1 + (** grps are defined by 3-bit indices *) let reg_single : reg_single Theory.Bitv.t Theory.Value.sort = Theory.Bitv.define 3 diff --git a/plugins/arm_thumb/thumb_mov.ml b/plugins/arm_thumb/thumb_mov.ml index 7a603e1e2..905430443 100644 --- a/plugins/arm_thumb/thumb_mov.ml +++ b/plugins/arm_thumb/thumb_mov.ml @@ -15,6 +15,8 @@ open Core open Utils + let rseq x y = seq y x + let mover dest src = match dest, src with | `Reg d, `Reg s -> (move_reg ~lreg:reg_wide d s) | _ -> raise (Lift_Error "dest or src is not a register") @@ -152,4 +154,267 @@ open Core (Flags.set_sbc (var Env.tmp) (var s) d) | _ -> raise (Lift_Error "operands must be registers") + let andrr dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + seq (set d (logand (var d) (var s))) (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + let asri dest src imm = match dest, src, imm with + | `Reg d, `Reg s, `Imm v -> + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + (if Bap.Std.Word.is_zero v then + seq + (set Env.cf (var s1 |> msb)) + (set d (ite (var s1 |> msb) (bitv_of 0xffffffff) (bitv_of 0))) + else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in + seq + (set Env.cf (nth_bit take_n (var s1))) + (set d (arshift (var s1) s2))) + |> rseq (Flags.set_nzf d) + | _ -> raise (Lift_Error "incorrect operands") + + (* ASRr has a rather complex logic, see A7.1.12 *) + let asrr dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + (seq + (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var Env.cf) + (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) + ) + (msb (var d)) + ) + ) + (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var d) + (arshift (var d) seg) + ) + (ite (msb (var d)) + (bitv_of 0xffffffff) + (bitv_of 0) + ) + ) + )) |> rseq (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + let bic dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + seq + (set d (logand (var d) (not (var s)))) + (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + let cmnz dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + seq + (set Env.tmp (add (var d) (var s))) + (Flags.set_add (var d) (var s) Env.tmp) + | _ -> raise (Lift_Error "dest or src is not a register") + + let cmpi8 dest imm = match dest, imm with + | `Reg d, `Imm v -> + let (d, s) = (reg d, word_as_bitv v) in + seq + (set Env.tmp (sub (var d) s)) + (Flags.set_sub (var d) s Env.tmp) + | _ -> raise (Lift_Error "incorrect operands") + + let cmpr dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + seq + (set Env.tmp (sub (var d) (var s))) + (Flags.set_sub (var d) (var s) Env.tmp) + | _ -> raise (Lift_Error "dest or src is not a register") + + let cmphir dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg_wide d, reg_wide s in + seq + (set Env.tmp (sub (var d) (var s))) + (Flags.set_sub (var d) (var s) Env.tmp) + | _ -> raise (Lift_Error "dest or src is not a register") + + let eor dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + seq + (set d (logxor (var d) (var s))) + (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + let lsli dest src imm = match dest, src, imm with + | `Reg d, `Reg s, `Imm v -> + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + (if Bap.Std.Word.is_zero v then + set d (var s1) + else let take_n = Bap.Std.Word.sub (Bap.Std.Word.of_int 32 32) v |> word_as_bitv in + seq + (set Env.cf (nth_bit take_n (var s1))) + (set d (shiftl b0 (var s1) s2))) + |> rseq (Flags.set_nzf d) + | _ -> raise (Lift_Error "incorrect operands") + + (* LSLr has a rather complex logic, see A7.1.39 *) + let lslr dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + (seq + (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var Env.cf) + (nth_bit (sub (bitv_of 32 |> cast Env.byte b0) seg) (var d)) + ) + (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) + (lsb (var d)) + b0 + ) + ) + ) + (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var d) + (shiftl b0 (var d) seg) + ) + (zero Env.value) + ) + )) |> rseq (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + let lsri dest src imm = match dest, src, imm with + | `Reg d, `Reg s, `Imm v -> + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + (if Bap.Std.Word.is_zero v then + seq + (set Env.cf (var s1 |> msb)) + (set d (bitv_of 0)) + else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in + seq + (set Env.cf (nth_bit take_n (var s1))) + (set d (shiftr b0 (var s1) s2))) + |> rseq (Flags.set_nzf d) + | _ -> raise (Lift_Error "incorrect operands") + + let lsrr dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + (seq + (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var Env.cf) + (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) + ) + (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) + (msb (var d)) + b0 + ) + ) + ) + (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var d) + (shiftr b0 (var d) seg) + ) + (zero Env.value) + ) + )) |> rseq (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + let orr dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + seq (set d (logor (var d) (var s))) (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + (* This is actually code named `neg Rd Rm`, but llvm encodes it as `rsb Rd Rm #0` *) + let rsb dest src imm = match dest, src, imm with + | `Reg d, `Reg s, `Imm v -> + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + seq + (set d (sub s2 (var s1))) + (Flags.set_sub s2 (var s1) d) + | _ -> raise (Lift_Error "incorrect operands") + + let rev dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + let s = var s in + let i24 = bitv_of 24 in + let i8 = bitv_of 8 in + let umask = bitv_of 0xff0000 in + let lmask = bitv_of 0xff00 in + let rev = + logor (lshift s i24) + (logor (rshift s i24) + (logor + (rshift (logand s umask) i8) + (lshift (logand s lmask) i8) + ) + ) + in set d rev + | _ -> raise (Lift_Error "dest or src is not a register") + + let rev_halfword hf = + let i8 = bitv_of 8 in + logor (lshift hf i8) (rshift hf i8) + + let rev16 dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + let s = var s in + let rev_extend v = + cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in + let i16 = bitv_of 16 in + let rev = logor + (rev_extend s) + (rshift s i16 |> rev_extend |> lshift i16) + in set d rev + | _ -> raise (Lift_Error "dest or src is not a register") + + let revsh dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + let s = var s in + let rev_extend v = + cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in + let rev = logand (rev_extend s) + (ite (cast Env.byte b0 s |> msb) + (bitv_of 0xffff0000) + (bitv_of 0) + ) + in set d rev + | _ -> raise (Lift_Error "dest or src is not a register") + + let ror dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + let seg4 = cast Env.half_byte b0 (var s) in + (seq + (set Env.cf (ite (eq seg (zero Env.byte)) + (var Env.cf) + (ite (eq seg4 (zero Env.half_byte)) + (msb (var d)) + (nth_bit (sub seg4 (bitv_of 1 |> cast Env.half_byte b0)) (var d)) + ) + ) + ) + (set d (ite (eq seg4 (zero Env.half_byte)) + (var d) + ( + let seg4_comp = sub (bitv_of 32 |> cast Env.half_byte b0) seg4 in + logand (rshift (var d) seg4) (lshift (var d) seg4_comp) + ) + ) + )) |> rseq (Flags.set_nzf d) + | _ -> raise (Lift_Error "dest or src is not a register") + + let tst dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + seq + (set Env.tmp (logand (var d) (var s))) + (Flags.set_nzf Env.tmp) + | _ -> raise (Lift_Error "dest or src is not a register") + end \ No newline at end of file From 7aa7b65396e1e4ba056a6839556366578706b3ba Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Mon, 15 Jun 2020 23:03:23 +0800 Subject: [PATCH 13/25] finished instructions def --- plugins/arm_thumb/thumb.ml | 73 +++++++++++++++++++++++++++++++-- plugins/arm_thumb/thumb_bits.ml | 37 +++++++++++++++++ plugins/arm_thumb/thumb_defs.ml | 33 +++++++++++++-- 3 files changed, 137 insertions(+), 6 deletions(-) create mode 100644 plugins/arm_thumb/thumb_bits.ml diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 70900fb98..99ca54598 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -16,6 +16,7 @@ module Thumb(Core : Theory.Core) = struct module Mov = Thumb_mov.Mov(Core) module Mem = Thumb_mem.Mem(Core) + module Bits = Thumb_bits.Bits(Core) module Utils = Thumb_util.Utils(Core) open Utils @@ -24,9 +25,9 @@ module Thumb(Core : Theory.Core) = struct KB.Object.create Theory.Program.cls >>= fun lbl -> blk lbl eff skip - let ctrl eff pc = + let ctrl eff data pc = Theory.Label.for_addr pc >>= fun lbl -> - blk lbl pass eff + blk lbl data eff let lift_move insn ops = let open Mov in @@ -111,16 +112,82 @@ module Thumb(Core : Theory.Core) = struct lift_mem_single dest src1 ~src2 St H | `tSTMIA, dest :: src_list -> store_multiple dest src_list + | `tLDMIA, dest :: src_list -> + load_multiple dest src_list | `tPUSH, src_list -> push_multiple src_list | `tPOP, src_list -> pop_multiple src_list (* TODO: PC might have been changed *) | _ -> pass + let lift_bits insn ops = + let open Bits in + match insn, ops with + | `tSXTB, [dest; src] -> sxtb dest src + | `tSXTH, [dest; src] -> sxth dest src + | `tUXTB, [dest; src] -> uxtb dest src + | `tUXTH, [dest; src] -> uxth dest src + | _ -> pass + + let bcc cond target = match cond, target with + | `Imm cond, `Imm target -> + let z = var Env.zf in + let c = var Env.cf in + let v = var Env.vf in + let n = var Env.nf in + let eq_ a b = or_ (and_ a b) (and_ (inv a) (inv b)) in + let cond_val = match Bap.Std.Word.to_int cond |> Result.ok |> Option.value_exn |> Defs.of_int_exn with + | `EQ -> z + | `NE -> inv z + | `CS -> c + | `CC -> inv c + | `MI -> n + | `PL -> inv n + | `VS -> v + | `VC -> inv v + | `HI -> and_ c (inv z) + | `LS -> or_ (inv c) z + | `GE -> eq_ n v + | `LT -> eq_ n v |> inv + | `GT -> and_ (inv z) (eq_ n v) + | `LE -> or_ z (eq_ n v |> inv) + | `AL -> b1 + in let jump_address = add (var Env.pc) (lshift (word_as_bitv target) (bitv_of 1)) in + branch cond_val + ( + jmp jump_address + ) + (skip) + | _ -> raise @@ Lift_Error "operands must be immediate" + + let lift_b ?(link = false) ?(state = false) ?(shl = true) ?offset base = + let open Defs in + let address = match base, offset with + | `Reg r, Some `Imm v -> let r = reg r in + add (var r) ((if shl then Bap.Std.Word.(lshift v (of_int 32 1)) else v) |> word_as_bitv) + | `Reg r, None -> let r = reg r in + if shl then shiftl b0 (var r) (bitv_of 2) else var r + | _ -> raise (Lift_Error "invalid operands") + in jmp address + + (* these are not entirely complete *) + let lift_branch insn ops = + let open Defs in + match insn, ops with + | `tBcc, [cond; target] -> bcc cond target + | `tB, [target] -> lift_b (`Reg `PC) ~offset:target + | `tBL, [target] -> lift_b (`Reg `PC) ~offset:target ~shl:false ~link:true + | `tBLXi, [target] -> lift_b (`Reg `PC) ~offset:target ~shl:false ~link:true ~state:true + | `tBLXr, [target] -> lift_b target ~shl:false ~link:true ~state:true + | `tBX, [target] -> lift_b target ~state:true + | _ -> skip + let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = match ins with | #move_insn -> lift_move ins ops |> move | #mem_insn -> lift_mem ins ops |> move - | _ -> nop + | #bits_insn -> lift_bits ins ops |> move + (* this is malformed for now *) + | #branch_insn -> ctrl (lift_branch ins ops) pass (Bitvec.zero) (* var Env.pc *) end diff --git a/plugins/arm_thumb/thumb_bits.ml b/plugins/arm_thumb/thumb_bits.ml new file mode 100644 index 000000000..89aaa91f3 --- /dev/null +++ b/plugins/arm_thumb/thumb_bits.ml @@ -0,0 +1,37 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = Thumb_env.Env +module Defs = Thumb_defs + +exception Lift_Error = Thumb_defs.Lift_Error + +module Bits(Core : Theory.Core) = struct +open Core + + module Utils = Thumb_util.Utils(Core) + + open Utils + + let sxtb dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + (set d (cast Env.byte b0 (var s) |> signed Env.value)) + | _ -> raise (Lift_Error "dest or src is not a register") + + let sxth dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + (set d (cast Env.half_word b0 (var s) |> signed Env.value)) + | _ -> raise (Lift_Error "dest or src is not a register") + + let uxtb dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + (set d (cast Env.byte b0 (var s) |> unsigned Env.value)) + | _ -> raise (Lift_Error "dest or src is not a register") + + let uxth dest src = match dest, src with + | `Reg d, `Reg s -> let d, s = reg d, reg s in + (set d (cast Env.half_word b0 (var s) |> unsigned Env.value)) + | _ -> raise (Lift_Error "dest or src is not a register") + +end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index 8ec9513af..bf90aa44d 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -112,8 +112,11 @@ type move_insn = [ ] [@@deriving bin_io, compare, sexp, enumerate] type bits_insn = [ - | `NA -] + | `tSXTB + | `tSXTH + | `tUXTB + | `tUXTH +] [@@deriving bin_io, compare, sexp, enumerate] (** Rd [reglist] *) type mem_multi_insn = [ @@ -146,13 +149,19 @@ type mem_insn = [ ] [@@deriving bin_io, compare, sexp, enumerate] type branch_insn = [ + | `tBcc + | `tB | `tBL + | `tBLXi + | `tBLXr + | `tBX ] [@@deriving bin_io, compare, sexp, enumerate] type insn = [ | move_insn | mem_insn | branch_insn + | bits_insn ] [@@deriving bin_io, compare, sexp, enumerate] (** Memory access operations *) @@ -179,4 +188,22 @@ type repair = [`POS | `NEG] [@@deriving compare] type shift = [`ASR | `LSL | `LSR | `ROR | `RRX] -type smul_size = BB | BT | TB | TT | D | DX | WB | WT \ No newline at end of file +type smul_size = BB | BT | TB | TT | D | DX | WB | WT + +let of_int_exn = function + | 0 -> `EQ + | 1 -> `NE + | 2 -> `CS + | 3 -> `CC + | 4 -> `MI + | 5 -> `PL + | 6 -> `VS + | 7 -> `VC + | 8 -> `HI + | 9 -> `LS + | 10 -> `GE + | 11 -> `LT + | 12 -> `GT + | 13 -> `LE + | 14 -> `AL + | n -> raise @@ Lift_Error "input is not a condition" \ No newline at end of file From 434c7726235f56ab9d8e867d8f1784e40d41f1c3 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Wed, 17 Jun 2020 15:57:30 +0800 Subject: [PATCH 14/25] code style clean-up --- plugins/radare2/radare2_main.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index 01dd69d52..d06b7fdd2 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -34,10 +34,11 @@ let provide_radare2 file = let strip str = let open String in match chop_prefix str ~prefix:"sym.imp." with | Some str -> str - | None -> str - in + | None -> str in + let open Yojson.Basic.Util in List.fold symbol_list ~init:() ~f:(fun () symbol -> - accept (Yojson.Basic.Util.to_string (extract "name" symbol) |> strip) (Yojson.Basic.Util.to_int (extract "vaddr" symbol) |> Z.of_int) + accept (to_string (extract "name" symbol) |> strip) + (to_int (extract "vaddr" symbol) |> Z.of_int) ); if Hashtbl.length funcs = 0 then warning "failed to obtain symbols"; From c5a6c1b0da83eaba5bcc23893d70918f5ce7671d Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Sun, 21 Jun 2020 22:17:44 +0800 Subject: [PATCH 15/25] refactor for new radare2-ocaml interface --- plugins/radare2/radare2_main.ml | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index d06b7fdd2..50fa4fc44 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -21,6 +21,8 @@ let provide_roots funcs = promise_property Theory.Label.is_valid; promise_property Theory.Label.is_subroutine +exception Radare2_failed + let provide_radare2 file = let funcs = Hashtbl.create (module struct type t = Z.t @@ -28,17 +30,35 @@ let provide_radare2 file = let sexp_of_t x = Sexp.Atom (Z.to_string x) end) in let accept name addr = Hashtbl.set funcs addr name in - let extract name json = Yojson.Basic.Util.member name json in + let extract name json = let open Yojson in + match json with + | `Assoc list -> + (match List.find list ~f:(fun (key, _) -> String.equal key name) with + | Some (_, v) -> v + | _ -> raise Radare2_failed) + | _ -> raise Radare2_failed in try - let symbol_list = Yojson.Basic.Util.to_list (R2.with_command_j "isj" file) in + let symbol_list = let open Yojson in + match R2.with_command_j "isj" file with + | `List list -> list + | _ -> raise Radare2_failed in let strip str = let open String in match chop_prefix str ~prefix:"sym.imp." with | Some str -> str | None -> str in - let open Yojson.Basic.Util in + let open Yojson in + let to_string json = + match json with + | `String str -> str + | _ -> raise Radare2_failed in + let to_int json = + match json with + | `Int i -> Z.of_int i + | `Intlit s -> Z.of_string s + | _ -> raise Radare2_failed in List.fold symbol_list ~init:() ~f:(fun () symbol -> accept (to_string (extract "name" symbol) |> strip) - (to_int (extract "vaddr" symbol) |> Z.of_int) + (to_int (extract "vaddr" symbol)) ); if Hashtbl.length funcs = 0 then warning "failed to obtain symbols"; From 612f15a4a860568e8891b6de7802eecf12219b72 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Sun, 21 Jun 2020 22:35:56 +0800 Subject: [PATCH 16/25] lift symbol extracting to allow partial failure --- plugins/radare2/radare2_main.ml | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index 50fa4fc44..e7695c1fd 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -34,14 +34,14 @@ let provide_radare2 file = match json with | `Assoc list -> (match List.find list ~f:(fun (key, _) -> String.equal key name) with - | Some (_, v) -> v - | _ -> raise Radare2_failed) - | _ -> raise Radare2_failed in + | Some (_, v) -> Some v + | _ -> None) + | _ -> None in try let symbol_list = let open Yojson in match R2.with_command_j "isj" file with - | `List list -> list - | _ -> raise Radare2_failed in + | `List list -> Some list + | _ -> None in let strip str = let open String in match chop_prefix str ~prefix:"sym.imp." with | Some str -> str @@ -49,17 +49,19 @@ let provide_radare2 file = let open Yojson in let to_string json = match json with - | `String str -> str - | _ -> raise Radare2_failed in + | `String str -> Some str + | _ -> None in let to_int json = match json with - | `Int i -> Z.of_int i - | `Intlit s -> Z.of_string s - | _ -> raise Radare2_failed in - List.fold symbol_list ~init:() ~f:(fun () symbol -> - accept (to_string (extract "name" symbol) |> strip) - (to_int (extract "vaddr" symbol)) - ); + | `Int i -> Z.of_int i |> Some + | `Intlit s -> Z.of_string s |> Some + | _ -> None in + Option.(symbol_list >>| List.fold ~init:() ~f:(fun () symbol -> + both + (extract "name" symbol >>= to_string >>| strip) + (extract "vaddr" symbol >>= to_int) + |> value_map ~default:() ~f:(fun (name, addr) -> accept name addr) + ) |> value ~default:()); if Hashtbl.length funcs = 0 then warning "failed to obtain symbols"; let symbolizer = Symbolizer.create @@ fun addr -> From 111df620dad329057b98a37aa81b5c4030219b2d Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Wed, 24 Jun 2020 23:45:15 +0800 Subject: [PATCH 17/25] clean-up refactor & indentation fix --- plugins/radare2/radare2_main.ml | 86 ++++++++++++++++----------------- 1 file changed, 42 insertions(+), 44 deletions(-) diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index e7695c1fd..c2538ceda 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -21,7 +21,31 @@ let provide_roots funcs = promise_property Theory.Label.is_valid; promise_property Theory.Label.is_subroutine -exception Radare2_failed +let extract_name (json : Yojson.t) = + match json with + | Yojson.(`Assoc list) -> + (match List.find list ~f:(fun (key, _) -> String.equal key "name") with + | Some (_, v) -> (match v with + | Yojson.(`String str) -> Some str + | _ -> None) + | _ -> None) + | _ -> None + +let extract_addr (json : Yojson.t) = + match json with + | Yojson.(`Assoc list) -> + (match List.find list ~f:(fun (key, _) -> String.equal key "vaddr") with + | Some (_, v) -> (match v with + | Yojson.(`Int i) -> Z.of_int i |> Some + | Yojson.(`Intlit s) -> Z.of_string s |> Some + | _ -> None) + | _ -> None) + | _ -> None + +let strip str = + match String.chop_prefix str ~prefix:"sym.imp." with + | Some str -> str + | None -> str let provide_radare2 file = let funcs = Hashtbl.create (module struct @@ -29,51 +53,25 @@ let provide_radare2 file = let compare = Z.compare and hash = Z.hash let sexp_of_t x = Sexp.Atom (Z.to_string x) end) in - let accept name addr = Hashtbl.set funcs addr name in - let extract name json = let open Yojson in - match json with - | `Assoc list -> - (match List.find list ~f:(fun (key, _) -> String.equal key name) with - | Some (_, v) -> Some v - | _ -> None) - | _ -> None in - try - let symbol_list = let open Yojson in - match R2.with_command_j "isj" file with - | `List list -> Some list - | _ -> None in - let strip str = let open String in - match chop_prefix str ~prefix:"sym.imp." with - | Some str -> str - | None -> str in - let open Yojson in - let to_string json = - match json with - | `String str -> Some str - | _ -> None in - let to_int json = - match json with - | `Int i -> Z.of_int i |> Some - | `Intlit s -> Z.of_string s |> Some - | _ -> None in - Option.(symbol_list >>| List.fold ~init:() ~f:(fun () symbol -> - both - (extract "name" symbol >>= to_string >>| strip) - (extract "vaddr" symbol >>= to_int) - |> value_map ~default:() ~f:(fun (name, addr) -> accept name addr) - ) |> value ~default:()); - if Hashtbl.length funcs = 0 - then warning "failed to obtain symbols"; - let symbolizer = Symbolizer.create @@ fun addr -> - Hashtbl.find funcs @@ - Bitvec.to_bigint (Word.to_bitvec addr) in - Symbolizer.provide agent symbolizer; - provide_roots funcs - with _ -> warning "failed to use radare2";() + let accept name addr = Hashtbl.set funcs addr name in + let symbol_list = match R2.with_command_j "isj" file with + | Yojson.(`List list) -> Some list + | s -> warning "unexpected radare2 output: %a" Yojson.pp s; None + | exception _ -> warning "failed to get symbols - radare2 command failed"; None in + Option.iter symbol_list ~f:(List.iter ~f:(fun s -> match extract_name s, extract_addr s with + | Some name, Some addr -> accept (strip name) addr + | _ -> debug "skipping json item %a" Yojson.pp s)); + if Hashtbl.length funcs = 0 + then warning "failed to obtain symbols"; + let symbolizer = Symbolizer.create @@ fun addr -> + Hashtbl.find funcs @@ + Bitvec.to_bigint (Word.to_bitvec addr) in + Symbolizer.provide agent symbolizer; + provide_roots funcs -let main = Stream.observe Project.Info.file @@ provide_radare2 +let main () = Stream.observe Project.Info.file @@ provide_radare2 let () = Config.manpage [ @@ -87,4 +85,4 @@ let () = `S "SEE ALSO"; `P "$(b,bap-plugin-objdump)(1)" ]; - Config.when_ready (fun {get=_} -> main) \ No newline at end of file + Config.when_ready (fun {get=_} -> main ()) \ No newline at end of file From 1325ade86ce0f03d1d53782d735053dacdb824e3 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Thu, 25 Jun 2020 13:38:42 +0800 Subject: [PATCH 18/25] polymorphic variant & pipe operator fix --- plugins/radare2/radare2_main.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index c2538ceda..6c50eb8e1 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -23,21 +23,21 @@ let provide_roots funcs = let extract_name (json : Yojson.t) = match json with - | Yojson.(`Assoc list) -> + | `Assoc list -> (match List.find list ~f:(fun (key, _) -> String.equal key "name") with | Some (_, v) -> (match v with - | Yojson.(`String str) -> Some str + | `String str -> Some str | _ -> None) | _ -> None) | _ -> None let extract_addr (json : Yojson.t) = match json with - | Yojson.(`Assoc list) -> + | `Assoc list -> (match List.find list ~f:(fun (key, _) -> String.equal key "vaddr") with | Some (_, v) -> (match v with - | Yojson.(`Int i) -> Z.of_int i |> Some - | Yojson.(`Intlit s) -> Z.of_string s |> Some + | `Int i -> Some (Z.of_int i) + | `Intlit s -> Some (Z.of_string s) | _ -> None) | _ -> None) | _ -> None @@ -55,12 +55,13 @@ let provide_radare2 file = end) in let accept name addr = Hashtbl.set funcs addr name in let symbol_list = match R2.with_command_j "isj" file with - | Yojson.(`List list) -> Some list + | `List list -> Some list | s -> warning "unexpected radare2 output: %a" Yojson.pp s; None | exception _ -> warning "failed to get symbols - radare2 command failed"; None in - Option.iter symbol_list ~f:(List.iter ~f:(fun s -> match extract_name s, extract_addr s with - | Some name, Some addr -> accept (strip name) addr - | _ -> debug "skipping json item %a" Yojson.pp s)); + Option.iter symbol_list + ~f:(List.iter ~f:(fun s -> match extract_name s, extract_addr s with + | Some name, Some addr -> accept (strip name) addr + | _ -> debug "skipping json item %a" Yojson.pp s)); if Hashtbl.length funcs = 0 then warning "failed to obtain symbols"; let symbolizer = Symbolizer.create @@ fun addr -> From f27131b7d79fc6c10231ec06989bbcca774954a0 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Fri, 3 Jul 2020 16:07:55 +0800 Subject: [PATCH 19/25] apply ocp-indent --- plugins/arm_thumb/thumb.ml | 120 +++---- plugins/arm_thumb/thumb_bits.ml | 22 +- plugins/arm_thumb/thumb_defs.ml | 2 +- plugins/arm_thumb/thumb_env.ml | 22 +- plugins/arm_thumb/thumb_flags.ml | 50 +-- plugins/arm_thumb/thumb_mem.ml | 164 ++++----- plugins/arm_thumb/thumb_mov.ml | 568 +++++++++++++++---------------- plugins/arm_thumb/thumb_util.ml | 28 +- 8 files changed, 488 insertions(+), 488 deletions(-) diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 99ca54598..5113db5ab 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -10,26 +10,26 @@ let package = "arm-thumb" type insns = Defs.insn * (Defs.op list) module Thumb(Core : Theory.Core) = struct - open Core - open Defs - module Env = Thumb_env.Env + open Core + open Defs + module Env = Thumb_env.Env - module Mov = Thumb_mov.Mov(Core) - module Mem = Thumb_mem.Mem(Core) - module Bits = Thumb_bits.Bits(Core) - module Utils = Thumb_util.Utils(Core) + module Mov = Thumb_mov.Mov(Core) + module Mem = Thumb_mem.Mem(Core) + module Bits = Thumb_bits.Bits(Core) + module Utils = Thumb_util.Utils(Core) - open Utils + open Utils - let move eff = + let move eff = KB.Object.create Theory.Program.cls >>= fun lbl -> blk lbl eff skip - let ctrl eff data pc = + let ctrl eff data pc = Theory.Label.for_addr pc >>= fun lbl -> blk lbl data eff - let lift_move insn ops = + let lift_move insn ops = let open Mov in match insn, ops with | `tADC, [dest; src1; src2] -> adc dest src1 src2 @@ -72,55 +72,55 @@ module Thumb(Core : Theory.Core) = struct | `tTST, [dest; src] -> tst dest src | _ -> pass - let lift_mem insn ops = + let lift_mem insn ops = let open Defs in let open Mem in match insn, ops with | `tLDRi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm Ld W + lift_mem_single dest src ~src2:imm Ld W | `tLDRr, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 Ld W + lift_mem_single dest src1 ~src2 Ld W | `tLDRpci, [dest; imm] -> - lift_mem_single dest `PC ~src2:imm Ld W + lift_mem_single dest `PC ~src2:imm Ld W | `tLDRspi, [dest; imm] -> - lift_mem_single dest `SP ~src2:imm Ld W + lift_mem_single dest `SP ~src2:imm Ld W | `tLDRBi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm Ld B + lift_mem_single dest src ~src2:imm Ld B | `tLDRBr, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 Ld B + lift_mem_single dest src1 ~src2 Ld B | `tLDRHi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm Ld H + lift_mem_single dest src ~src2:imm Ld H | `tLDRHr, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 Ld H + lift_mem_single dest src1 ~src2 Ld H | `tLDRSB, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 Ld B ~sign:true + lift_mem_single dest src1 ~src2 Ld B ~sign:true | `tLDRSH, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 Ld H ~sign:true + lift_mem_single dest src1 ~src2 Ld H ~sign:true | `tSTRi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm St W + lift_mem_single dest src ~src2:imm St W | `tSTRr, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 St W + lift_mem_single dest src1 ~src2 St W | `tSTRspi, [dest; imm] -> - lift_mem_single dest `SP ~src2:imm St W + lift_mem_single dest `SP ~src2:imm St W | `tSTRBi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm St B + lift_mem_single dest src ~src2:imm St B | `tSTRBr, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 St B + lift_mem_single dest src1 ~src2 St B | `tSTRHi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm St H + lift_mem_single dest src ~src2:imm St H | `tSTRHr, [dest; src1; src2] -> - lift_mem_single dest src1 ~src2 St H + lift_mem_single dest src1 ~src2 St H | `tSTMIA, dest :: src_list -> - store_multiple dest src_list + store_multiple dest src_list | `tLDMIA, dest :: src_list -> - load_multiple dest src_list + load_multiple dest src_list | `tPUSH, src_list -> - push_multiple src_list + push_multiple src_list | `tPOP, src_list -> - pop_multiple src_list (* TODO: PC might have been changed *) + pop_multiple src_list (* TODO: PC might have been changed *) | _ -> pass - let lift_bits insn ops = + let lift_bits insn ops = let open Bits in match insn, ops with | `tSXTB, [dest; src] -> sxtb dest src @@ -129,14 +129,14 @@ module Thumb(Core : Theory.Core) = struct | `tUXTH, [dest; src] -> uxth dest src | _ -> pass - let bcc cond target = match cond, target with + let bcc cond target = match cond, target with | `Imm cond, `Imm target -> - let z = var Env.zf in - let c = var Env.cf in - let v = var Env.vf in - let n = var Env.nf in - let eq_ a b = or_ (and_ a b) (and_ (inv a) (inv b)) in - let cond_val = match Bap.Std.Word.to_int cond |> Result.ok |> Option.value_exn |> Defs.of_int_exn with + let z = var Env.zf in + let c = var Env.cf in + let v = var Env.vf in + let n = var Env.nf in + let eq_ a b = or_ (and_ a b) (and_ (inv a) (inv b)) in + let cond_val = match Bap.Std.Word.to_int cond |> Result.ok |> Option.value_exn |> Defs.of_int_exn with | `EQ -> z | `NE -> inv z | `CS -> c @@ -152,26 +152,26 @@ module Thumb(Core : Theory.Core) = struct | `GT -> and_ (inv z) (eq_ n v) | `LE -> or_ z (eq_ n v |> inv) | `AL -> b1 - in let jump_address = add (var Env.pc) (lshift (word_as_bitv target) (bitv_of 1)) in - branch cond_val - ( - jmp jump_address - ) - (skip) + in let jump_address = add (var Env.pc) (lshift (word_as_bitv target) (bitv_of 1)) in + branch cond_val + ( + jmp jump_address + ) + (skip) | _ -> raise @@ Lift_Error "operands must be immediate" - let lift_b ?(link = false) ?(state = false) ?(shl = true) ?offset base = - let open Defs in - let address = match base, offset with - | `Reg r, Some `Imm v -> let r = reg r in - add (var r) ((if shl then Bap.Std.Word.(lshift v (of_int 32 1)) else v) |> word_as_bitv) - | `Reg r, None -> let r = reg r in - if shl then shiftl b0 (var r) (bitv_of 2) else var r - | _ -> raise (Lift_Error "invalid operands") - in jmp address - - (* these are not entirely complete *) - let lift_branch insn ops = + let lift_b ?(link = false) ?(state = false) ?(shl = true) ?offset base = + let open Defs in + let address = match base, offset with + | `Reg r, Some `Imm v -> let r = reg r in + add (var r) ((if shl then Bap.Std.Word.(lshift v (of_int 32 1)) else v) |> word_as_bitv) + | `Reg r, None -> let r = reg r in + if shl then shiftl b0 (var r) (bitv_of 2) else var r + | _ -> raise (Lift_Error "invalid operands") + in jmp address + + (* these are not entirely complete *) + let lift_branch insn ops = let open Defs in match insn, ops with | `tBcc, [cond; target] -> bcc cond target @@ -182,7 +182,7 @@ module Thumb(Core : Theory.Core) = struct | `tBX, [target] -> lift_b target ~state:true | _ -> skip - let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = + let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = match ins with | #move_insn -> lift_move ins ops |> move | #mem_insn -> lift_mem ins ops |> move diff --git a/plugins/arm_thumb/thumb_bits.ml b/plugins/arm_thumb/thumb_bits.ml index 89aaa91f3..95398f2ad 100644 --- a/plugins/arm_thumb/thumb_bits.ml +++ b/plugins/arm_thumb/thumb_bits.ml @@ -8,30 +8,30 @@ module Defs = Thumb_defs exception Lift_Error = Thumb_defs.Lift_Error module Bits(Core : Theory.Core) = struct -open Core + open Core - module Utils = Thumb_util.Utils(Core) + module Utils = Thumb_util.Utils(Core) - open Utils + open Utils - let sxtb dest src = match dest, src with + let sxtb dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.byte b0 (var s) |> signed Env.value)) + (set d (cast Env.byte b0 (var s) |> signed Env.value)) | _ -> raise (Lift_Error "dest or src is not a register") - let sxth dest src = match dest, src with + let sxth dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.half_word b0 (var s) |> signed Env.value)) + (set d (cast Env.half_word b0 (var s) |> signed Env.value)) | _ -> raise (Lift_Error "dest or src is not a register") - let uxtb dest src = match dest, src with + let uxtb dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.byte b0 (var s) |> unsigned Env.value)) + (set d (cast Env.byte b0 (var s) |> unsigned Env.value)) | _ -> raise (Lift_Error "dest or src is not a register") - let uxth dest src = match dest, src with + let uxth dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.half_word b0 (var s) |> unsigned Env.value)) + (set d (cast Env.half_word b0 (var s) |> unsigned Env.value)) | _ -> raise (Lift_Error "dest or src is not a register") end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index bf90aa44d..8557b08f7 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -35,7 +35,7 @@ type gpr_reg = [ | `R5 | `R6 | `R7 -(* all the ARM GRPs are still needed *) + (* all the ARM GRPs are still needed *) | `R8 | `R9 | `R10 diff --git a/plugins/arm_thumb/thumb_env.ml b/plugins/arm_thumb/thumb_env.ml index 5a8d08882..f0d8253a0 100644 --- a/plugins/arm_thumb/thumb_env.ml +++ b/plugins/arm_thumb/thumb_env.ml @@ -3,12 +3,12 @@ open Base open KB.Syntax module Env = struct -type value -type byte -type reg_single -type half_byte -type half_word -type bit_val + type value + type byte + type reg_single + type half_byte + type half_word + type bit_val let bit : Theory.Bool.t Theory.Value.sort = Theory.Bool.t @@ -56,21 +56,21 @@ type bit_val let lr = Theory.Var.define value "lr" let pc = Theory.Var.define value "pc" let sp = Theory.Var.define value "sp" -(* The following are temporarily not used *) + (* The following are temporarily not used *) let spsr = Theory.Var.define value "spsr" let cpsr = Theory.Var.define value "cpsr" -(* The following are individual flag *) + (* The following are individual flag *) let nf = Theory.Var.define bit "nf" let zf = Theory.Var.define bit "zf" let cf = Theory.Var.define bit "cf" let vf = Theory.Var.define bit "vf" let qf = Theory.Var.define bit "qf" let ge = Theory.Var.define half_byte "ge" -(* psuedo register storing temporary computations *) + (* psuedo register storing temporary computations *) let tmp = Theory.Var.define value "tmp" -exception Unbound_Reg -module Defs = Thumb_defs + exception Unbound_Reg + module Defs = Thumb_defs (* to elimiate ambiguity *) let load_reg_wide (op : Defs.reg) = let open Thumb_defs in diff --git a/plugins/arm_thumb/thumb_flags.ml b/plugins/arm_thumb/thumb_flags.ml index ba58246b6..f5899ec79 100644 --- a/plugins/arm_thumb/thumb_flags.ml +++ b/plugins/arm_thumb/thumb_flags.ml @@ -5,48 +5,48 @@ open KB.Syntax module Env = Thumb_env.Env module Flags(Core : Theory.Core) = struct -open Core -type value_extend + open Core + type value_extend -let value : value_extend Theory.Bitv.t Theory.Value.sort = + let value : value_extend Theory.Bitv.t Theory.Value.sort = Theory.Bitv.define 33 (* 33 bits for carry flag inspection *) -let set_nzf r = + let set_nzf r = seq - (set (Env.nf) (msb (var r))) - (set (Env.zf) (eq (var r) (int Env.value (Bitvec.zero)))) + (set (Env.nf) (msb (var r))) + (set (Env.zf) (eq (var r) (int Env.value (Bitvec.zero)))) -let set_vnzf_add s1 s2 r = + let set_vnzf_add s1 s2 r = seq - (set (Env.vf) (msb (logand (not (logxor s1 s2)) (logxor s1 (var r))))) - (set_nzf r) + (set (Env.vf) (msb (logand (not (logxor s1 s2)) (logxor s1 (var r))))) + (set_nzf r) -let set_add s1 s2 r = + let set_add s1 s2 r = seq - (set Env.cf (slt (var r) s1)) - (set_vnzf_add s1 s2 r) + (set Env.cf (slt (var r) s1)) + (set_vnzf_add s1 s2 r) -let set_vnzf_sub s1 s2 r = + let set_vnzf_sub s1 s2 r = seq - (set (Env.vf) (msb (logand (logxor s1 s2) (logxor s1 (var r))))) - (set_nzf r) + (set (Env.vf) (msb (logand (logxor s1 s2) (logxor s1 (var r))))) + (set_nzf r) -let set_sub s1 s2 r = + let set_sub s1 s2 r = seq - (set Env.cf (sle s2 s1)) - (set_vnzf_sub s1 s2 r) + (set Env.cf (sle s2 s1)) + (set_vnzf_sub s1 s2 r) -let as_bitv b = ite b (int value Bitvec.one) (int value Bitvec.zero) + let as_bitv b = ite b (int value Bitvec.one) (int value Bitvec.zero) -let set_adc s1 s2 r = + let set_adc s1 s2 r = let sum_with_carry = - let extend = cast value b0 in - add (add (extend s1) (extend s2)) (as_bitv (var Env.cf)) + let extend = cast value b0 in + add (add (extend s1) (extend s2)) (as_bitv (var Env.cf)) in seq - (set Env.cf (msb sum_with_carry)) - (set_vnzf_add s1 s2 r) + (set Env.cf (msb sum_with_carry)) + (set_vnzf_add s1 s2 r) -let set_sbc s1 s2 r = set_adc s1 (not s2) r + let set_sbc s1 s2 r = set_adc s1 (not s2) r end diff --git a/plugins/arm_thumb/thumb_mem.ml b/plugins/arm_thumb/thumb_mem.ml index 2deb71509..9c70e5551 100644 --- a/plugins/arm_thumb/thumb_mem.ml +++ b/plugins/arm_thumb/thumb_mem.ml @@ -8,92 +8,92 @@ module Defs = Thumb_defs exception Lift_Error = Thumb_defs.Lift_Error module Mem(Core : Theory.Core) = struct -open Core + open Core - module Utils = Thumb_util.Utils(Core) + module Utils = Thumb_util.Utils(Core) - open Utils + open Utils - (* The original ARM lifter implement this in a BIL loop-style for some reason *) - let store_multiple dest src_list = - match dest with - | `Reg r -> let r = reg r in List.fold src_list ~init:pass - ~f:(fun eff src -> match src with - | `Reg s -> let src = reg s in seq eff - (seq - (storew b0 (var Env.memory) (var r) (var src) |> set Env.memory) - (set r (add (var r) (bitv_of 4))) - ) - | _ -> raise (Lift_Error "`src` must be a register") - ) - | _ -> raise (Lift_Error "`dest` must be a register") + (* The original ARM lifter implement this in a BIL loop-style for some reason *) + let store_multiple dest src_list = + match dest with + | `Reg r -> let r = reg r in List.fold src_list ~init:pass + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (storew b0 (var Env.memory) (var r) (var src) |> set Env.memory) + (set r (add (var r) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + ) + | _ -> raise (Lift_Error "`dest` must be a register") - let load_multiple dest src_list = - match dest with - | `Reg r -> let r = reg r in List.fold src_list ~init:pass - ~f:(fun eff src -> match src with - | `Reg s -> let src = reg s in seq eff - (seq - (loadw Env.value b0 (var Env.memory) (var r) |> set src) - (set r (add (var r) (bitv_of 4))) - ) - | _ -> raise (Lift_Error "`src` must be a register") - ) - | _ -> raise (Lift_Error "`dest` must be a register") - (* the `R` bit is automatically resolved *) - let push_multiple src_list = - let shift x = bitv_of 2 |> shiftl b0 x in - let offset = List.length src_list |> bitv_of |> shift in - let initial = set Env.tmp (sub (var Env.sp) offset) in - seq (List.fold src_list ~init:initial - ~f:(fun eff src -> match src with - | `Reg s -> let src = reg s in seq eff - (seq - (storew b0 (var Env.memory) (var Env.tmp) (var src) |> set Env.memory) - (set Env.tmp (add (var Env.tmp) (bitv_of 4))) - ) - | _ -> raise (Lift_Error "`src` must be a register") - )) (set Env.sp (sub (var Env.sp) offset)) - (* TODO: PC might change here *) - let pop_multiple src_list = - let initial = set Env.tmp (var Env.sp) in - seq (List.fold src_list ~init:initial - ~f:(fun eff src -> match src with - | `Reg s -> let src = reg s in seq eff - (seq - (loadw Env.value b0 (var Env.memory) (var Env.tmp) |> set src) - (set Env.tmp (add (var Env.tmp) (bitv_of 4))) - ) - | _ -> raise (Lift_Error "`src` must be a register") - )) (set Env.sp (var Env.tmp)) + let load_multiple dest src_list = + match dest with + | `Reg r -> let r = reg r in List.fold src_list ~init:pass + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (loadw Env.value b0 (var Env.memory) (var r) |> set src) + (set r (add (var r) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + ) + | _ -> raise (Lift_Error "`dest` must be a register") + (* the `R` bit is automatically resolved *) + let push_multiple src_list = + let shift x = bitv_of 2 |> shiftl b0 x in + let offset = List.length src_list |> bitv_of |> shift in + let initial = set Env.tmp (sub (var Env.sp) offset) in + seq (List.fold src_list ~init:initial + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (storew b0 (var Env.memory) (var Env.tmp) (var src) |> set Env.memory) + (set Env.tmp (add (var Env.tmp) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + )) (set Env.sp (sub (var Env.sp) offset)) + (* TODO: PC might change here *) + let pop_multiple src_list = + let initial = set Env.tmp (var Env.sp) in + seq (List.fold src_list ~init:initial + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (loadw Env.value b0 (var Env.memory) (var Env.tmp) |> set src) + (set Env.tmp (add (var Env.tmp) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + )) (set Env.sp (var Env.tmp)) - let lift_mem_single ?(sign = false) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = - let open Defs in - let dest = match dest with - | `Reg r -> reg r - | _ -> raise (Lift_Error "`dest` must be a register") - in - let shift x = bitv_of 2 |> shiftl b0 x in - let address = match src1, src2 with - | `Reg s, None -> reg s |> var - | `Reg s1, Some (`Reg s2) -> - add (reg s1 |> var) (reg s2 |> var) - | `Reg s, Some (`Imm v) -> - add (reg_wide s |> var) (word_as_bitv v |> shift) - | _ -> raise (Lift_Error "Unbound memory operation mode") - in match op with - | Ld -> - let extend = if sign then signed else unsigned in - let value = match size with - | W -> loadw Env.value b0 (var Env.memory) address - | H -> loadw Env.half_word b0 (var Env.memory) address |> extend Env.value - | B -> load (var Env.memory) address |> extend Env.value - in set dest value - | St -> - let mem = match size with - | W -> storew b0 (var Env.memory) address (var dest) - | H -> storew b0 (var Env.memory) address (cast Env.half_word b0 (var dest)) - | B -> store (var Env.memory) address (cast Env.byte b0 (var dest)) - in set Env.memory mem + let lift_mem_single ?(sign = false) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = + let open Defs in + let dest = match dest with + | `Reg r -> reg r + | _ -> raise (Lift_Error "`dest` must be a register") + in + let shift x = bitv_of 2 |> shiftl b0 x in + let address = match src1, src2 with + | `Reg s, None -> reg s |> var + | `Reg s1, Some (`Reg s2) -> + add (reg s1 |> var) (reg s2 |> var) + | `Reg s, Some (`Imm v) -> + add (reg_wide s |> var) (word_as_bitv v |> shift) + | _ -> raise (Lift_Error "Unbound memory operation mode") + in match op with + | Ld -> + let extend = if sign then signed else unsigned in + let value = match size with + | W -> loadw Env.value b0 (var Env.memory) address + | H -> loadw Env.half_word b0 (var Env.memory) address |> extend Env.value + | B -> load (var Env.memory) address |> extend Env.value + in set dest value + | St -> + let mem = match size with + | W -> storew b0 (var Env.memory) address (var dest) + | H -> storew b0 (var Env.memory) address (cast Env.half_word b0 (var dest)) + | B -> store (var Env.memory) address (cast Env.byte b0 (var dest)) + in set Env.memory mem end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_mov.ml b/plugins/arm_thumb/thumb_mov.ml index 905430443..eed04f470 100644 --- a/plugins/arm_thumb/thumb_mov.ml +++ b/plugins/arm_thumb/thumb_mov.ml @@ -8,413 +8,413 @@ module Flags = Thumb_flags.Flags exception Lift_Error = Thumb_defs.Lift_Error module Mov(Core : Theory.Core) = struct -open Core + open Core - module Utils = Thumb_util.Utils(Core) - module Flags = Flags(Core) + module Utils = Thumb_util.Utils(Core) + module Flags = Flags(Core) - open Utils + open Utils - let rseq x y = seq y x + let rseq x y = seq y x - let mover dest src = match dest, src with + let mover dest src = match dest, src with | `Reg d, `Reg s -> (move_reg ~lreg:reg_wide d s) | _ -> raise (Lift_Error "dest or src is not a register") - let movesr dest src = match dest, src with + let movesr dest src = match dest, src with | `Reg d, `Reg s -> seq (move_reg d s) (Flags.set_nzf (reg d)) | _ -> raise (Lift_Error "dest or src is not a register") - let movei8 dest imm = match dest, imm with + let movei8 dest imm = match dest, imm with | `Reg d, `Imm v -> seq (set_reg d v) (Flags.set_nzf (reg d)) | _ -> raise (Lift_Error "incorrect operands") - let movenot dest src = match dest, src with + let movenot dest src = match dest, src with | `Reg d, `Reg s -> - let (dest, src) = (reg d, reg s) in - seq - (set dest (not (var src))) - (Flags.set_nzf dest) + let (dest, src) = (reg d, reg s) in + seq + (set dest (not (var src))) + (Flags.set_nzf dest) | _ -> raise (Lift_Error "dest or src is not a register") - let mul dest src = match dest, src with + let mul dest src = match dest, src with | `Reg d, `Reg s -> - let (dest, src) = (reg d, reg s) in - seq - (set dest (mul (var dest) (var src))) - (Flags.set_nzf dest) + let (dest, src) = (reg d, reg s) in + seq + (set dest (mul (var dest) (var src))) + (Flags.set_nzf dest) | _ -> raise (Lift_Error "dest or src is not a register") - let addi3 dest src imm = match dest, src, imm with + let addi3 dest src imm = match dest, src, imm with | `Reg d, `Reg s, `Imm v -> - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - seq - (set d (add (var s1) s2)) - (Flags.set_add (var s1) s2 d) + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + seq + (set d (add (var s1) s2)) + (Flags.set_add (var s1) s2 d) | _ -> raise (Lift_Error "incorrect operands") - let subi3 dest src imm = match dest, src, imm with + let subi3 dest src imm = match dest, src, imm with | `Reg d, `Reg s, `Imm v -> - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - seq - (set d (sub (var s1) s2)) - (Flags.set_sub (var s1) s2 d) + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + seq + (set d (sub (var s1) s2)) + (Flags.set_sub (var s1) s2 d) | _ -> raise (Lift_Error "incorrect operands") - (* a temp value is introduced here *) - let addi8 dest imm = match dest, imm with + (* a temp value is introduced here *) + let addi8 dest imm = match dest, imm with | `Reg d, `Imm v -> - let (d, s) = (reg d, word_as_bitv v) in - seq - (seq - (set Env.tmp (var d)) - (set d (add (var d) s)) - ) - (Flags.set_add (var Env.tmp) s d) + let (d, s) = (reg d, word_as_bitv v) in + seq + (seq + (set Env.tmp (var d)) + (set d (add (var d) s)) + ) + (Flags.set_add (var Env.tmp) s d) | _ -> raise (Lift_Error "incorrect operands") - let subi8 dest imm = match dest, imm with + let subi8 dest imm = match dest, imm with | `Reg d, `Imm v -> - let (d, s) = (reg d, word_as_bitv v) in - seq - (seq - (set Env.tmp (var d)) - (set d (sub (var d) s)) - ) - (Flags.set_sub (var Env.tmp) s d) + let (d, s) = (reg d, word_as_bitv v) in + seq + (seq + (set Env.tmp (var d)) + (set d (sub (var d) s)) + ) + (Flags.set_sub (var Env.tmp) s d) | _ -> raise (Lift_Error "incorrect operands") - let addrr d s1 s2 = match d, s1, s2 with + let addrr d s1 s2 = match d, s1, s2 with | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (add (var s1) (var s2))) - (Flags.set_add (var s1) (var s2) d) + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (add (var s1) (var s2))) + (Flags.set_add (var s1) (var s2) d) | _ -> raise (Lift_Error "operands must be registers") - let subrr d s1 s2 = match d, s1, s2 with + let subrr d s1 s2 = match d, s1, s2 with | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (sub (var s1) (var s2))) - (Flags.set_sub (var s1) (var s2) d) + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (sub (var s1) (var s2))) + (Flags.set_sub (var s1) (var s2) d) | _ -> raise (Lift_Error "operands must be registers") - let addhirr d s = match d, s with + let addhirr d s = match d, s with | `Reg d, `Reg s -> - let (d, s) = (reg_wide d, reg_wide s) in - set d (add (var d) (var s)) + let (d, s) = (reg_wide d, reg_wide s) in + set d (add (var d) (var s)) | _ -> raise (Lift_Error "operands must be registers") - (* Rd = (PC and 0xfffffffc) + (imm << 2) *) - let adr dest imm = match dest, imm with + (* Rd = (PC and 0xfffffffc) + (imm << 2) *) + let adr dest imm = match dest, imm with | `Reg d, `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let (d, s) = (reg d, word_as_bitv v) in - set d (add (logand (var Env.pc) (bitv_of 0xFFFFFFFC)) (shift s)) + let shift x = bitv_of 2 |> shiftl b0 x in + let (d, s) = (reg d, word_as_bitv v) in + set d (add (logand (var Env.pc) (bitv_of 0xFFFFFFFC)) (shift s)) | _ -> raise (Lift_Error "incorrect operands") - let addrspi dest imm = match dest, imm with + let addrspi dest imm = match dest, imm with | `Reg d, `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let (d, s) = (reg d, word_as_bitv v) in - set d (add (var Env.sp) (shift s)) + let shift x = bitv_of 2 |> shiftl b0 x in + let (d, s) = (reg d, word_as_bitv v) in + set d (add (var Env.sp) (shift s)) | _ -> raise (Lift_Error "incorrect operands") - let addspi imm = match imm with + let addspi imm = match imm with | `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let s = word_as_bitv v in - set Env.sp (add (var Env.sp) (shift s)) + let shift x = bitv_of 2 |> shiftl b0 x in + let s = word_as_bitv v in + set Env.sp (add (var Env.sp) (shift s)) | _ -> raise (Lift_Error "imm must be an immediate") - let subspi imm = match imm with + let subspi imm = match imm with | `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let s = word_as_bitv v in - set Env.sp (sub (var Env.sp) (shift s)) + let shift x = bitv_of 2 |> shiftl b0 x in + let s = word_as_bitv v in + set Env.sp (sub (var Env.sp) (shift s)) | _ -> raise (Lift_Error "imm must be an immediate") - let adc d s1 s2 = match d, s1, s2 with + let adc d s1 s2 = match d, s1, s2 with | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (add (add (var s1) (var s2)) (bool_as_bitv (var Env.cf)))) - (Flags.set_adc (var s1) (var s2) d) + let (d, s1, s2) = (reg d, reg s1, reg s2) in + seq + (set d (add (add (var s1) (var s2)) (bool_as_bitv (var Env.cf)))) + (Flags.set_adc (var s1) (var s2) d) | _ -> raise (Lift_Error "operands must be registers") - let sbc d s = match d, s with + let sbc d s = match d, s with | `Reg d, `Reg s -> - let (d, s) = (reg d, reg s) in - seq - (seq - (set Env.tmp (var d)) - (set d (add (sub (var d) (var s)) (bool_as_bitv (var Env.cf)))) - ) - (Flags.set_sbc (var Env.tmp) (var s) d) + let (d, s) = (reg d, reg s) in + seq + (seq + (set Env.tmp (var d)) + (set d (add (sub (var d) (var s)) (bool_as_bitv (var Env.cf)))) + ) + (Flags.set_sbc (var Env.tmp) (var s) d) | _ -> raise (Lift_Error "operands must be registers") - let andrr dest src = match dest, src with + let andrr dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq (set d (logand (var d) (var s))) (Flags.set_nzf d) + seq (set d (logand (var d) (var s))) (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - let asri dest src imm = match dest, src, imm with + let asri dest src imm = match dest, src, imm with | `Reg d, `Reg s, `Imm v -> - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - (if Bap.Std.Word.is_zero v then - seq - (set Env.cf (var s1 |> msb)) - (set d (ite (var s1 |> msb) (bitv_of 0xffffffff) (bitv_of 0))) - else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in - seq - (set Env.cf (nth_bit take_n (var s1))) - (set d (arshift (var s1) s2))) - |> rseq (Flags.set_nzf d) + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + (if Bap.Std.Word.is_zero v then + seq + (set Env.cf (var s1 |> msb)) + (set d (ite (var s1 |> msb) (bitv_of 0xffffffff) (bitv_of 0))) + else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in + seq + (set Env.cf (nth_bit take_n (var s1))) + (set d (arshift (var s1) s2))) + |> rseq (Flags.set_nzf d) | _ -> raise (Lift_Error "incorrect operands") - (* ASRr has a rather complex logic, see A7.1.12 *) - let asrr dest src = match dest, src with + (* ASRr has a rather complex logic, see A7.1.12 *) + let asrr dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - (seq - (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var Env.cf) - (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) - ) - (msb (var d)) + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + (seq + (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var Env.cf) + (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) ) - ) - (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var d) - (arshift (var d) seg) - ) - (ite (msb (var d)) - (bitv_of 0xffffffff) - (bitv_of 0) - ) - ) - )) |> rseq (Flags.set_nzf d) + (msb (var d)) + ) + ) + (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var d) + (arshift (var d) seg) + ) + (ite (msb (var d)) + (bitv_of 0xffffffff) + (bitv_of 0) + ) + ) + )) |> rseq (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - let bic dest src = match dest, src with + let bic dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set d (logand (var d) (not (var s)))) - (Flags.set_nzf d) + seq + (set d (logand (var d) (not (var s)))) + (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - let cmnz dest src = match dest, src with + let cmnz dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set Env.tmp (add (var d) (var s))) - (Flags.set_add (var d) (var s) Env.tmp) + seq + (set Env.tmp (add (var d) (var s))) + (Flags.set_add (var d) (var s) Env.tmp) | _ -> raise (Lift_Error "dest or src is not a register") - let cmpi8 dest imm = match dest, imm with + let cmpi8 dest imm = match dest, imm with | `Reg d, `Imm v -> - let (d, s) = (reg d, word_as_bitv v) in - seq - (set Env.tmp (sub (var d) s)) - (Flags.set_sub (var d) s Env.tmp) + let (d, s) = (reg d, word_as_bitv v) in + seq + (set Env.tmp (sub (var d) s)) + (Flags.set_sub (var d) s Env.tmp) | _ -> raise (Lift_Error "incorrect operands") - let cmpr dest src = match dest, src with + let cmpr dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set Env.tmp (sub (var d) (var s))) - (Flags.set_sub (var d) (var s) Env.tmp) + seq + (set Env.tmp (sub (var d) (var s))) + (Flags.set_sub (var d) (var s) Env.tmp) | _ -> raise (Lift_Error "dest or src is not a register") - let cmphir dest src = match dest, src with + let cmphir dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg_wide d, reg_wide s in - seq - (set Env.tmp (sub (var d) (var s))) - (Flags.set_sub (var d) (var s) Env.tmp) + seq + (set Env.tmp (sub (var d) (var s))) + (Flags.set_sub (var d) (var s) Env.tmp) | _ -> raise (Lift_Error "dest or src is not a register") - let eor dest src = match dest, src with + let eor dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set d (logxor (var d) (var s))) - (Flags.set_nzf d) + seq + (set d (logxor (var d) (var s))) + (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - let lsli dest src imm = match dest, src, imm with + let lsli dest src imm = match dest, src, imm with | `Reg d, `Reg s, `Imm v -> - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - (if Bap.Std.Word.is_zero v then - set d (var s1) - else let take_n = Bap.Std.Word.sub (Bap.Std.Word.of_int 32 32) v |> word_as_bitv in - seq - (set Env.cf (nth_bit take_n (var s1))) - (set d (shiftl b0 (var s1) s2))) - |> rseq (Flags.set_nzf d) + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + (if Bap.Std.Word.is_zero v then + set d (var s1) + else let take_n = Bap.Std.Word.sub (Bap.Std.Word.of_int 32 32) v |> word_as_bitv in + seq + (set Env.cf (nth_bit take_n (var s1))) + (set d (shiftl b0 (var s1) s2))) + |> rseq (Flags.set_nzf d) | _ -> raise (Lift_Error "incorrect operands") - (* LSLr has a rather complex logic, see A7.1.39 *) - let lslr dest src = match dest, src with + (* LSLr has a rather complex logic, see A7.1.39 *) + let lslr dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - (seq - (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var Env.cf) - (nth_bit (sub (bitv_of 32 |> cast Env.byte b0) seg) (var d)) - ) - (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) - (lsb (var d)) - b0 - ) + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + (seq + (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var Env.cf) + (nth_bit (sub (bitv_of 32 |> cast Env.byte b0) seg) (var d)) ) - ) - (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var d) - (shiftl b0 (var d) seg) - ) - (zero Env.value) + (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) + (lsb (var d)) + b0 ) - )) |> rseq (Flags.set_nzf d) + ) + ) + (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var d) + (shiftl b0 (var d) seg) + ) + (zero Env.value) + ) + )) |> rseq (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - let lsri dest src imm = match dest, src, imm with + let lsri dest src imm = match dest, src, imm with | `Reg d, `Reg s, `Imm v -> - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - (if Bap.Std.Word.is_zero v then - seq - (set Env.cf (var s1 |> msb)) - (set d (bitv_of 0)) - else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in - seq - (set Env.cf (nth_bit take_n (var s1))) - (set d (shiftr b0 (var s1) s2))) - |> rseq (Flags.set_nzf d) + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + (if Bap.Std.Word.is_zero v then + seq + (set Env.cf (var s1 |> msb)) + (set d (bitv_of 0)) + else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in + seq + (set Env.cf (nth_bit take_n (var s1))) + (set d (shiftr b0 (var s1) s2))) + |> rseq (Flags.set_nzf d) | _ -> raise (Lift_Error "incorrect operands") - let lsrr dest src = match dest, src with + let lsrr dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - (seq - (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var Env.cf) - (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) - ) - (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) - (msb (var d)) - b0 - ) + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + (seq + (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var Env.cf) + (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) ) - ) - (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var d) - (shiftr b0 (var d) seg) - ) - (zero Env.value) + (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) + (msb (var d)) + b0 ) - )) |> rseq (Flags.set_nzf d) + ) + ) + (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) + (ite (eq seg (zero Env.byte)) + (var d) + (shiftr b0 (var d) seg) + ) + (zero Env.value) + ) + )) |> rseq (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - let orr dest src = match dest, src with + let orr dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq (set d (logor (var d) (var s))) (Flags.set_nzf d) + seq (set d (logor (var d) (var s))) (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - (* This is actually code named `neg Rd Rm`, but llvm encodes it as `rsb Rd Rm #0` *) - let rsb dest src imm = match dest, src, imm with + (* This is actually code named `neg Rd Rm`, but llvm encodes it as `rsb Rd Rm #0` *) + let rsb dest src imm = match dest, src, imm with | `Reg d, `Reg s, `Imm v -> - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - seq - (set d (sub s2 (var s1))) - (Flags.set_sub s2 (var s1) d) + let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in + seq + (set d (sub s2 (var s1))) + (Flags.set_sub s2 (var s1) d) | _ -> raise (Lift_Error "incorrect operands") - let rev dest src = match dest, src with + let rev dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - let s = var s in - let i24 = bitv_of 24 in - let i8 = bitv_of 8 in - let umask = bitv_of 0xff0000 in - let lmask = bitv_of 0xff00 in - let rev = - logor (lshift s i24) - (logor (rshift s i24) - (logor - (rshift (logand s umask) i8) - (lshift (logand s lmask) i8) - ) - ) - in set d rev + let s = var s in + let i24 = bitv_of 24 in + let i8 = bitv_of 8 in + let umask = bitv_of 0xff0000 in + let lmask = bitv_of 0xff00 in + let rev = + logor (lshift s i24) + (logor (rshift s i24) + (logor + (rshift (logand s umask) i8) + (lshift (logand s lmask) i8) + ) + ) + in set d rev | _ -> raise (Lift_Error "dest or src is not a register") - let rev_halfword hf = - let i8 = bitv_of 8 in - logor (lshift hf i8) (rshift hf i8) + let rev_halfword hf = + let i8 = bitv_of 8 in + logor (lshift hf i8) (rshift hf i8) - let rev16 dest src = match dest, src with + let rev16 dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - let s = var s in - let rev_extend v = - cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in - let i16 = bitv_of 16 in - let rev = logor - (rev_extend s) - (rshift s i16 |> rev_extend |> lshift i16) - in set d rev + let s = var s in + let rev_extend v = + cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in + let i16 = bitv_of 16 in + let rev = logor + (rev_extend s) + (rshift s i16 |> rev_extend |> lshift i16) + in set d rev | _ -> raise (Lift_Error "dest or src is not a register") - let revsh dest src = match dest, src with + let revsh dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - let s = var s in - let rev_extend v = - cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in - let rev = logand (rev_extend s) - (ite (cast Env.byte b0 s |> msb) - (bitv_of 0xffff0000) - (bitv_of 0) - ) - in set d rev + let s = var s in + let rev_extend v = + cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in + let rev = logand (rev_extend s) + (ite (cast Env.byte b0 s |> msb) + (bitv_of 0xffff0000) + (bitv_of 0) + ) + in set d rev | _ -> raise (Lift_Error "dest or src is not a register") - let ror dest src = match dest, src with + let ror dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - let seg4 = cast Env.half_byte b0 (var s) in - (seq - (set Env.cf (ite (eq seg (zero Env.byte)) - (var Env.cf) - (ite (eq seg4 (zero Env.half_byte)) - (msb (var d)) - (nth_bit (sub seg4 (bitv_of 1 |> cast Env.half_byte b0)) (var d)) - ) - ) - ) - (set d (ite (eq seg4 (zero Env.half_byte)) - (var d) - ( - let seg4_comp = sub (bitv_of 32 |> cast Env.half_byte b0) seg4 in - logand (rshift (var d) seg4) (lshift (var d) seg4_comp) + let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in + let seg = cast Env.byte b0 (var s) in + let seg4 = cast Env.half_byte b0 (var s) in + (seq + (set Env.cf (ite (eq seg (zero Env.byte)) + (var Env.cf) + (ite (eq seg4 (zero Env.half_byte)) + (msb (var d)) + (nth_bit (sub seg4 (bitv_of 1 |> cast Env.half_byte b0)) (var d)) ) - ) - )) |> rseq (Flags.set_nzf d) + ) + ) + (set d (ite (eq seg4 (zero Env.half_byte)) + (var d) + ( + let seg4_comp = sub (bitv_of 32 |> cast Env.half_byte b0) seg4 in + logand (rshift (var d) seg4) (lshift (var d) seg4_comp) + ) + ) + )) |> rseq (Flags.set_nzf d) | _ -> raise (Lift_Error "dest or src is not a register") - let tst dest src = match dest, src with + let tst dest src = match dest, src with | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set Env.tmp (logand (var d) (var s))) - (Flags.set_nzf Env.tmp) + seq + (set Env.tmp (logand (var d) (var s))) + (Flags.set_nzf Env.tmp) | _ -> raise (Lift_Error "dest or src is not a register") end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_util.ml b/plugins/arm_thumb/thumb_util.ml index f3b991cf5..f7a2ade49 100644 --- a/plugins/arm_thumb/thumb_util.ml +++ b/plugins/arm_thumb/thumb_util.ml @@ -5,28 +5,28 @@ open KB.Syntax module Env = Thumb_env.Env module Utils(Core : Theory.Core) = struct -open Core + open Core - let skip : Theory.ctrl Theory.eff = perform Theory.Effect.Sort.bot - let pass : Theory.data Theory.eff = perform Theory.Effect.Sort.bot + let skip : Theory.ctrl Theory.eff = perform Theory.Effect.Sort.bot + let pass : Theory.data Theory.eff = perform Theory.Effect.Sort.bot - let nop = - KB.return @@ - Theory.Effect.empty Theory.Effect.Sort.top + let nop = + KB.return @@ + Theory.Effect.empty Theory.Effect.Sort.top - let reg = Env.load_reg + let reg = Env.load_reg - let reg_wide = Env.load_reg_wide + let reg_wide = Env.load_reg_wide - let bool_as_bitv b = ite b (int Env.value Bitvec.one) (int Env.value Bitvec.zero) + let bool_as_bitv b = ite b (int Env.value Bitvec.one) (int Env.value Bitvec.zero) - let word_as_bitv w = (int Env.value (Bap.Std.Word.to_bitvec w)) + let word_as_bitv w = (int Env.value (Bap.Std.Word.to_bitvec w)) - let bitv_of imm = word_as_bitv (Bap.Std.Word.of_int 32 imm) + let bitv_of imm = word_as_bitv (Bap.Std.Word.of_int 32 imm) - let move_reg ?lreg:(lreg = reg) dest src = set (lreg dest) (var (lreg src)) + let move_reg ?lreg:(lreg = reg) dest src = set (lreg dest) (var (lreg src)) - let set_reg ?lreg:(lreg = reg) dest imm = - set (lreg dest) (word_as_bitv imm) + let set_reg ?lreg:(lreg = reg) dest imm = + set (lreg dest) (word_as_bitv imm) end \ No newline at end of file From e99afb97a474804baf7c3e9101a2c8b14446136a Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Tue, 14 Jul 2020 18:09:15 +0800 Subject: [PATCH 20/25] thumb plugin refinement --- plugins/arm_thumb/dsl_common.ml | 146 +++++++ plugins/arm_thumb/thumb.ml | 222 +++++----- plugins/arm_thumb/thumb_bits.ml | 39 +- plugins/arm_thumb/thumb_branch.ml | 94 ++++ plugins/arm_thumb/thumb_defs.ml | 5 + plugins/arm_thumb/thumb_dsl.ml | 46 ++ plugins/arm_thumb/thumb_env.ml | 5 +- plugins/arm_thumb/thumb_flags.ml | 13 - plugins/arm_thumb/thumb_insn.ml | 36 ++ plugins/arm_thumb/thumb_mov.ml | 698 +++++++++++++----------------- 10 files changed, 775 insertions(+), 529 deletions(-) create mode 100644 plugins/arm_thumb/dsl_common.ml create mode 100644 plugins/arm_thumb/thumb_branch.ml create mode 100644 plugins/arm_thumb/thumb_dsl.ml create mode 100644 plugins/arm_thumb/thumb_insn.ml diff --git a/plugins/arm_thumb/dsl_common.ml b/plugins/arm_thumb/dsl_common.ml new file mode 100644 index 000000000..52464c97c --- /dev/null +++ b/plugins/arm_thumb/dsl_common.ml @@ -0,0 +1,146 @@ +open Bap_core_theory +open Base +open KB.Syntax +(** This is mean to design a dsl for ARM lifter *) + +(** General cpu defs. *) +module type CPU = sig + type value + type bit_val + type reg_type + type operand + val value: value Theory.Bitv.t Theory.Value.sort + val bit_val: bit_val Theory.Bitv.t Theory.Value.sort + val load_reg: reg_type -> value Theory.Bitv.t Theory.Var.t + val assert_var: operand -> value Theory.Bitv.t Theory.Var.t + val assert_val: operand -> value Theory.Bitv.t Theory.pure +end + +(** General fpu defs *) +module type FPU = sig + type operand + type value + val value : value Theory.Float.t Theory.Value.sort + val assert_var: operand -> value Theory.Float.t Theory.Var.t + val assert_val: operand -> value Theory.Float.t Theory.pure +end + +module type ValueHolder = sig + type value + val value: value Theory.Bitv.t Theory.Value.sort +end + +module DSL(Core: Theory.Core)(CPU: CPU)(V: ValueHolder) = struct + open Core + + let expand (dsl : 'a Theory.eff list) = + let bot = perform Theory.Effect.Sort.bot in + List.fold dsl ~init:bot + ~f:(fun acc current -> seq acc current) + + (** alternative of expand to enable short syntax *) + let ( !% ) = expand + + let assert_var = CPU.assert_var + + let (!$$) = assert_var + + let assert_val = CPU.assert_val + + let (!$) = assert_val + + let value_size = Theory.Bitv.size CPU.value + + let word_as_bitv w = (int CPU.value (Bap.Std.Word.to_bitvec w)) + + let bool_as_bitv b = ite b (int CPU.value Bitvec.one) (int CPU.value Bitvec.zero) + + let bool_as_bit b = ite b (int CPU.bit_val Bitvec.one) (int CPU.bit_val Bitvec.zero) + + let imm (x : int) = word_as_bitv (Bap.Std.Word.of_int value_size x) + + let (!!) = imm + + let ( := ) = set + let set_if cond dest src = dest := ite cond src (var dest) + let when_else_ (cond : bool) then_ else_ = + if cond then then_ |> expand else else_ |> expand + let when_ (cond : bool) eff = + let bot = perform Theory.Effect.Sort.bot in + when_else_ cond eff [bot] + let unless_ (cond : bool) eff = when_ (phys_equal cond false) eff + let if_else_ (cond : Theory.bool) then_ else_ = + branch cond (then_ |> expand) (else_ |> expand) + let if_ (cond : Theory.bool) then_ = + let bot = perform Theory.Effect.Sort.bot in + if_else_ cond then_ [bot] + + (** this is a static effect list generator (from core theory perspective) *) + let rec while_ (cond : 'a -> bool * 'a) (init : 'a) (perf : 'a -> 'b Theory.eff) = + match cond init with + | true, next -> [perf init] @ while_ cond next perf + | false, _ -> [perform Theory.Effect.Sort.bot] + + let foreach_ (list : 'a list) (perf : 'a -> int -> 'b Theory.eff) = + List.foldi list ~init:(perform Theory.Effect.Sort.bot) + ~f:(fun it eff item -> seq eff (perf item it)) + + let ( < ) = slt + let ( > ) = sgt + let ( <= ) = sle + let ( >= ) = sge + let ( <+ ) = ult + let ( >+ ) = ugt + let ( <=+ ) = ule + let ( >=+ ) = uge + let ( = ) = eq + let ( <> ) = neq + let ( << ) = lshift + let ( >> ) = rshift + let ( asr ) = arshift + let ( lor ) = logor + let ( land ) = logand + let ( lxor ) = logxor + let ( lnot ) = not + + let nth_bit n e = cast CPU.bit_val b0 (shiftr b0 e n) |> msb + + module Bool = struct + let ( lor ) = or_ + let ( land ) = and_ + let ( lnot ) = inv + let ( lxor ) x y = (lnot x land y) lor (x land lnot y) + let ( = ) = (lxor) + let ( <> ) x y = lnot (x = y) + end + + module Arith = struct + let distribute op x y = op (cast V.value b0 x) (cast V.value b0 y) + let ( + ) x y = distribute add x y + let ( - ) x y = distribute sub x y + let ( * ) x y = distribute mul x y + (* multiplication with signed cast *) + let ( -* ) x y = mul (signed V.value x) (signed V.value y) + let ( / ) x y = distribute div x y + let ( % ) x y = distribute modulo x y + end + + include Arith + + let extend v = cast CPU.value b0 v + let extend_to s v = cast s b0 v + let extend_signed v = signed CPU.value v + let extend_to_signed s v = signed s v + let scoped_var = Theory.Var.scoped + +end + +module DSLFP(Core : Theory.Core)(FPU: FPU) = struct + let assert_var = FPU.assert_var + + let (!$$.) = assert_var + + let assert_val = FPU.assert_val + + let (!$.) = assert_val +end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 5113db5ab..b80b6059f 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -4,6 +4,7 @@ open KB.Syntax module Defs = Thumb_defs module Flags = Thumb_flags.Flags +module Insns = Thumb_insn let package = "arm-thumb" @@ -17,7 +18,9 @@ module Thumb(Core : Theory.Core) = struct module Mov = Thumb_mov.Mov(Core) module Mem = Thumb_mem.Mem(Core) module Bits = Thumb_bits.Bits(Core) + module Branch = Thumb_branch.Branch(Core) module Utils = Thumb_util.Utils(Core) + module DSL = Thumb_dsl.Make(Core) open Utils @@ -32,50 +35,54 @@ module Thumb(Core : Theory.Core) = struct let lift_move insn ops = let open Mov in match insn, ops with - | `tADC, [dest; src1; src2] -> adc dest src1 src2 - | `tADDi3, [dest; src; imm] -> addi3 dest src imm - | `tADDi8, [dest; imm] -> addi8 dest imm - | `tADDrr, [dest; src1; src2] -> addrr dest src1 src2 - | `tADDhirr, [dest; src] -> addhirr dest src - | `tADR, [dest; imm] -> adr dest imm - | `tADDrSPi, [dest; imm] -> addrspi dest imm - | `tADDspi, [imm] -> addspi imm - | `tMOVr, [dest; src] -> mover dest src - | `tMOVSr, [dest; src] -> movesr dest src - | `tMOVi8, [dest; imm] -> movei8 dest imm - | `tMUL, [dest; src] -> mul dest src - | `tMVN, [dest; src] -> movenot dest src - | `tSBC, [dest; src] -> sbc dest src - | `tSUBi3, [dest; src; imm] -> subi3 dest src imm - | `tSUBi8, [dest; imm] -> subi8 dest imm - | `tSUBrr, [dest; src1; src2] -> subrr dest src1 src2 - | `tSUBspi, [imm] -> subspi imm - | `tAND, [dest; src] -> andrr dest src - | `tASRri, [dest; src; imm] -> asri dest src imm - | `tASRrr, [dest; src] -> asrr dest src - | `tBIC, [dest; src] -> bic dest src - | `tCMNz, [dest; src] -> cmnz dest src - | `tCMPi8, [dest; imm] -> cmpi8 dest imm - | `tCMPr, [dest; src] -> cmpr dest src - | `tCMPhir, [dest; src] -> cmphir dest src - | `tEOR, [dest; src] -> eor dest src - | `tLSLri, [dest; src; imm] -> lsli dest src imm - | `tLSLrr, [dest; src] -> lslr dest src - | `tLSRri, [dest; src; imm] -> lsri dest src imm - | `tLSRrr, [dest; src] -> lsrr dest src - | `tORR, [dest; src] -> orr dest src - | `tRSB, [dest; src; imm (* placeholder *)] -> rsb dest src imm - | `tREV, [dest; src] -> rev dest src - | `tREV16, [dest; src] -> rev16 dest src - | `tREVSH, [dest; src] -> revsh dest src - | `tROR, [dest; src] -> ror dest src - | `tTST, [dest; src] -> tst dest src - | _ -> pass - - let lift_mem insn ops = + | `tADC, [|dest; src1; src2|] -> adc dest src1 src2 + | `tADDi3, [|dest; src; imm|] -> addi3 dest src imm + | `tADDi8, [|dest; imm|] -> addi8 dest imm + | `tADDrr, [|dest; src1; src2|] -> addrr dest src1 src2 + | `tADDhirr, [|dest; src|] -> addhirr dest src + | `tADR, [|dest; imm|] -> adr dest imm + | `tADDrSPi, [|dest; imm|] -> addrspi dest imm + | `tADDspi, [|imm|] -> addspi imm + | `tMOVr, [|dest; src|] -> mover dest src + | `tMOVSr, [|dest; src|] -> movesr dest src + | `tMOVi8, [|dest; imm|] -> movei8 dest imm + | `tMUL, [|dest; src|] -> mul dest src + | `tMVN, [|dest; src|] -> movenot dest src + | `tSBC, [|dest; src|] -> sbc dest src + | `tSUBi3, [|dest; src; imm|] -> subi3 dest src imm + | `tSUBi8, [|dest; imm|] -> subi8 dest imm + | `tSUBrr, [|dest; src1; src2|] -> subrr dest src1 src2 + | `tSUBspi, [|imm|] -> subspi imm + | `tAND, [|dest; src|] -> andrr dest src + | `tASRri, [|dest; src; imm|] -> asri dest src imm + | `tASRrr, [|dest; src|] -> asrr dest src + | `tBIC, [|dest; src|] -> bic dest src + | `tCMNz, [|dest; src|] -> cmnz dest src + | `tCMPi8, [|dest; imm|] -> cmpi8 dest imm + | `tCMPr, [|dest; src|] -> cmpr dest src + | `tCMPhir, [|dest; src|] -> cmphir dest src + | `tEOR, [|dest; src|] -> eor dest src + | `tLSLri, [|dest; src; imm|] -> lsli dest src imm + | `tLSLrr, [|dest; src|] -> lslr dest src + | `tLSRri, [|dest; src; imm|] -> lsri dest src imm + | `tLSRrr, [|dest; src|] -> lsrr dest src + | `tORR, [|dest; src|] -> orr dest src + | `tRSB, [|dest; src; imm (* placeholder *)|] -> rsb dest src imm + | `tREV, [|dest; src|] -> rev dest src + | `tREV16, [|dest; src|] -> rev16 dest src + | `tREVSH, [|dest; src|] -> revsh dest src + | `tROR, [|dest; src|] -> ror dest src + | `tTST, [|dest; src|] -> tst dest src + | _ -> [] + + let lift_mem_single ?(sign = false) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = + match src2 with + | Some src2 -> Mem.lift_mem_single ~sign dest src1 ~src2 op size |> move + | None -> Mem.lift_mem_single ~sign dest src1 op size |> move + + let lift_mem insn ops addr = let open Defs in - let open Mem in - match insn, ops with + match insn, Array.to_list ops with | `tLDRi, [dest; src; imm] -> lift_mem_single dest src ~src2:imm Ld W | `tLDRr, [dest; src1; src2] -> @@ -111,83 +118,78 @@ module Thumb(Core : Theory.Core) = struct | `tSTRHr, [dest; src1; src2] -> lift_mem_single dest src1 ~src2 St H | `tSTMIA, dest :: src_list -> - store_multiple dest src_list + Mem.store_multiple dest src_list |> move | `tLDMIA, dest :: src_list -> - load_multiple dest src_list + Mem.load_multiple dest src_list |> move | `tPUSH, src_list -> - push_multiple src_list + Mem.push_multiple src_list |> move | `tPOP, src_list -> - pop_multiple src_list (* TODO: PC might have been changed *) - | _ -> pass + let has_pc = List.exists src_list + (fun s -> match s with + |`Reg `PC -> true + | _ -> false) in + let pop_eff = Mem.pop_multiple src_list in + if has_pc then + ctrl (jmp (var Env.pc)) pop_eff addr + else move pop_eff + | _ -> move pass let lift_bits insn ops = let open Bits in match insn, ops with - | `tSXTB, [dest; src] -> sxtb dest src - | `tSXTH, [dest; src] -> sxth dest src - | `tUXTB, [dest; src] -> uxtb dest src - | `tUXTH, [dest; src] -> uxth dest src - | _ -> pass - - let bcc cond target = match cond, target with - | `Imm cond, `Imm target -> - let z = var Env.zf in - let c = var Env.cf in - let v = var Env.vf in - let n = var Env.nf in - let eq_ a b = or_ (and_ a b) (and_ (inv a) (inv b)) in - let cond_val = match Bap.Std.Word.to_int cond |> Result.ok |> Option.value_exn |> Defs.of_int_exn with - | `EQ -> z - | `NE -> inv z - | `CS -> c - | `CC -> inv c - | `MI -> n - | `PL -> inv n - | `VS -> v - | `VC -> inv v - | `HI -> and_ c (inv z) - | `LS -> or_ (inv c) z - | `GE -> eq_ n v - | `LT -> eq_ n v |> inv - | `GT -> and_ (inv z) (eq_ n v) - | `LE -> or_ z (eq_ n v |> inv) - | `AL -> b1 - in let jump_address = add (var Env.pc) (lshift (word_as_bitv target) (bitv_of 1)) in - branch cond_val - ( - jmp jump_address - ) - (skip) - | _ -> raise @@ Lift_Error "operands must be immediate" - - let lift_b ?(link = false) ?(state = false) ?(shl = true) ?offset base = - let open Defs in - let address = match base, offset with - | `Reg r, Some `Imm v -> let r = reg r in - add (var r) ((if shl then Bap.Std.Word.(lshift v (of_int 32 1)) else v) |> word_as_bitv) - | `Reg r, None -> let r = reg r in - if shl then shiftl b0 (var r) (bitv_of 2) else var r - | _ -> raise (Lift_Error "invalid operands") - in jmp address + | `tSXTB, [|dest; src|] -> sxtb dest src + | `tSXTH, [|dest; src|] -> sxth dest src + | `tUXTB, [|dest; src|] -> uxtb dest src + | `tUXTH, [|dest; src|] -> uxth dest src + | _ -> [] (* these are not entirely complete *) - let lift_branch insn ops = + let lift_branch insn ops addr = let open Defs in + let open Branch in + let addr = Core.int Env.value addr in match insn, ops with - | `tBcc, [cond; target] -> bcc cond target - | `tB, [target] -> lift_b (`Reg `PC) ~offset:target - | `tBL, [target] -> lift_b (`Reg `PC) ~offset:target ~shl:false ~link:true - | `tBLXi, [target] -> lift_b (`Reg `PC) ~offset:target ~shl:false ~link:true ~state:true - | `tBLXr, [target] -> lift_b target ~shl:false ~link:true ~state:true - | `tBX, [target] -> lift_b target ~state:true - | _ -> skip - - let lift ((ins, ops) : insns) : unit Theory.Effect.t KB.t = - match ins with - | #move_insn -> lift_move ins ops |> move - | #mem_insn -> lift_mem ins ops |> move - | #bits_insn -> lift_bits ins ops |> move - (* this is malformed for now *) - | #branch_insn -> ctrl (lift_branch ins ops) pass (Bitvec.zero) (* var Env.pc *) + | `tBcc, [|cond; target|] -> tbcc cond target addr + | `tB, [|target|] -> tb target addr + | `tBL, [|target|] -> tbl target + | `tBLXi, [|target|] -> tblxi target + | `tBLXr, [|target|] -> tblxr target + | `tBX, [|target|] -> tbx target + | _ -> (skip, pass) + + let lift_with (addr : Bitvec.t) (insn : Thumb_defs.insn) + (ops : Thumb_defs.op array) = match insn with + | #move_insn -> lift_move insn ops |> DSL.expand |> move + | #mem_insn -> lift_mem insn ops addr + | #bits_insn -> lift_bits insn ops |> DSL.expand |> move + | #branch_insn -> + let (ctrl_eff, data_eff) = lift_branch insn ops addr in + ctrl ctrl_eff data_eff addr (* var Env.pc *) end + +open Bap.Std + +let run_lifter _label addr insn _mem + (lifter : Bitvec.t -> Defs.insn -> Defs.op array -> unit Theory.eff) = + match Insns.of_basic insn with + | None -> raise (Defs.Lift_Error "unknown instruction") + | Some arm_insn -> + match Insns.arm_ops (Disasm_expert.Basic.Insn.ops insn) with + | Error err -> raise (Defs.Lift_Error (Error.to_string_hum err)) + | Ok ops -> lifter addr arm_insn ops + +let provide_sematics insn effect = + KB.provide Theory.Program.Semantics.slot insn effect >>| fun () -> insn + +let lift label = + Theory.instance () >>= Theory.require >>= fun (module Core) -> + KB.collect Theory.Label.addr label >>= fun addr -> (* this is the address of the current instruction *) + KB.collect Disasm_expert.Basic.Insn.slot label >>= fun insn -> (* the LLVM provided decoding *) + KB.collect Memory.slot label >>= fun mem -> (* the memory chunk, probably not needed *) + let module Lifter = Thumb(Core) in + match addr, insn, mem with + | Some addr, Some insn, Some mem -> + run_lifter label addr insn mem Lifter.lift_with >>= fun sema -> + provide_sematics label sema + | _ -> provide_sematics label Insn.empty \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_bits.ml b/plugins/arm_thumb/thumb_bits.ml index 95398f2ad..4dcb820b9 100644 --- a/plugins/arm_thumb/thumb_bits.ml +++ b/plugins/arm_thumb/thumb_bits.ml @@ -11,27 +11,28 @@ module Bits(Core : Theory.Core) = struct open Core module Utils = Thumb_util.Utils(Core) + module DSL = Thumb_dsl.Make(Core) open Utils - let sxtb dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.byte b0 (var s) |> signed Env.value)) - | _ -> raise (Lift_Error "dest or src is not a register") - - let sxth dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.half_word b0 (var s) |> signed Env.value)) - | _ -> raise (Lift_Error "dest or src is not a register") - - let uxtb dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.byte b0 (var s) |> unsigned Env.value)) - | _ -> raise (Lift_Error "dest or src is not a register") - - let uxth dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - (set d (cast Env.half_word b0 (var s) |> unsigned Env.value)) - | _ -> raise (Lift_Error "dest or src is not a register") + let sxtb dest src = + DSL.[ + !$$dest := extend_to Env.byte !$src |> extend_signed + ] + + let sxth dest src = + DSL.[ + !$$dest := extend_to Env.half_word !$src |> extend_signed + ] + + let uxtb dest src = + DSL.[ + !$$dest := extend_to Env.byte !$src |> extend + ] + + let uxth dest src = + DSL.[ + !$$dest := extend_to Env.half_word !$src |> extend + ] end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_branch.ml b/plugins/arm_thumb/thumb_branch.ml new file mode 100644 index 000000000..0bbc01532 --- /dev/null +++ b/plugins/arm_thumb/thumb_branch.ml @@ -0,0 +1,94 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = Thumb_env.Env +module Defs = Thumb_defs + +exception Lift_Error = Thumb_defs.Lift_Error + +module Branch(Core : Theory.Core) = struct + open Core + + module Utils = Thumb_util.Utils(Core) + module DSL = Thumb_dsl.Make(Core) + + open Utils + + let tbcc cond target addr = match cond, target with + | `Imm cond, `Imm _ -> + let z = var Env.zf in + let c = var Env.cf in + let v = var Env.vf in + let n = var Env.nf in + let eq_ a b = or_ (and_ a b) (and_ (inv a) (inv b)) in + let cond = Bap.Std.Word.to_int cond |> Result.ok |> Option.value_exn |> Defs.of_int_exn in + let always_true = match cond with + | `AL -> true + | _ -> false in + let cond_val = match cond with + | `EQ -> z + | `NE -> inv z + | `CS -> c + | `CC -> inv c + | `MI -> n + | `PL -> inv n + | `VS -> v + | `VC -> inv v + | `HI -> and_ c (inv z) + | `LS -> or_ (inv c) z + | `GE -> eq_ n v + | `LT -> eq_ n v |> inv + | `GT -> and_ (inv z) (eq_ n v) + | `LE -> or_ z (eq_ n v |> inv) + | `AL -> b1 in + let jump_address = DSL.(addr + !$target << !!1) in + let eff_hold = (jmp jump_address, set Env.pc jump_address) in + if always_true then eff_hold + else ( + branch cond_val (fst eff_hold) skip, (* control effect branch *) + branch cond_val (snd eff_hold) pass (* data effect branch *) + ) + | _ -> raise @@ Lift_Error "operands must be immediate" + + let tb target addr = + (DSL.( + jmp (!$target + addr << !!1) + ), DSL.( + Env.pc := (!$target + addr << !!1) + )) + + let tbl target = + (DSL.( + jmp !$target + ), DSL.[ + Env.lr := (var Env.pc) + !!2 lor !!1; + Env.pc := !$target + ] |> DSL.expand) + + (* TODO : switch to normal mode *) + let tblxi target = + (DSL.( + jmp (!$target land !!0xfffffffc) + ), DSL.[ + Env.lr := (var Env.pc) + !!2 lor !!1; + Env.pc := (!$target land !!0xfffffffc) + ] |> DSL.expand) + + let tblxr target = + (DSL.( + jmp (!$target land !!0xfffffffe) + ), DSL.[ + Env.lr := (var Env.pc) + !!2 lor !!1; + Env.pc := (!$target land !!0xfffffffe) + ] |> DSL.expand) + + let tbx target = + (DSL.( + (* reference here is PC = Rm[31:1] << 1 *) + jmp (extract Env.value !!31 !!1 !$target << !!1) + ), DSL.( + Env.pc := (extract Env.value !!31 !!1 !$target << !!1) + )) + +end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index 8557b08f7..a8f5c508a 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -69,6 +69,11 @@ type op = [ | `Reg of reg | `Imm of word ] [@@deriving bin_io, compare, sexp] + +let assert_imm : op -> word = function + | `Imm imm -> imm + | _ -> raise (Lift_Error "immediate assertion failed") + (** all the `mov` series, registers marked with `e` means extended *) type move_insn = [ | `tMOVi8 (* Rd imm8 *) diff --git a/plugins/arm_thumb/thumb_dsl.ml b/plugins/arm_thumb/thumb_dsl.ml new file mode 100644 index 000000000..b579b4e5c --- /dev/null +++ b/plugins/arm_thumb/thumb_dsl.ml @@ -0,0 +1,46 @@ +open Bap_core_theory +open Base +open KB.Syntax + +module Env = Thumb_env.Env +module Common = Dsl_common + +exception Assert_error + +module Arm_cpu(Core : Theory.Core) = struct + open Core + include Env + let assert_val (op : operand) = match op with + | `Reg r -> load_reg r |> var + | `Imm i -> (int value (Bap.Std.Word.to_bitvec i)) + let assert_var = function + | `Reg r -> load_reg r + | `Imm _ -> raise Assert_error +end + +module Make_Extend(Core : Theory.Core)(Holder : Common.ValueHolder) = struct + open Core + module CPU = Arm_cpu(Core) + module DSL = Dsl_common.DSL(Core)(CPU)(Holder) + + include DSL + + let assert_val_wide (op : Env.operand) = match op with + | `Reg r -> Env.load_reg_wide r |> var + | `Imm _ -> assert_val op + + let (!$+) = assert_val_wide + + let assert_var_wide (op : Env.operand) = match op with + | `Reg r -> Env.load_reg_wide r + | `Imm _ -> raise Assert_error + + let (!$$+) = assert_var_wide +end + +module Make(Core : Theory.Core) = struct + module CPU_Holder = Arm_cpu(Core) + module Nested = Make_Extend(Core)(CPU_Holder) + + include Nested +end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_env.ml b/plugins/arm_thumb/thumb_env.ml index f0d8253a0..18cab9e2e 100644 --- a/plugins/arm_thumb/thumb_env.ml +++ b/plugins/arm_thumb/thumb_env.ml @@ -21,7 +21,7 @@ module Env = struct Theory.Bitv.define 3 let half_word : half_word Theory.Bitv.t Theory.Value.sort = - Theory.Bitv.define 32 + Theory.Bitv.define 16 let value : value Theory.Bitv.t Theory.Value.sort = Theory.Bitv.define 32 @@ -72,6 +72,9 @@ module Env = struct exception Unbound_Reg module Defs = Thumb_defs + type reg_type = Defs.reg + type operand = Defs.op + (* to elimiate ambiguity *) let load_reg_wide (op : Defs.reg) = let open Thumb_defs in match op with diff --git a/plugins/arm_thumb/thumb_flags.ml b/plugins/arm_thumb/thumb_flags.ml index f5899ec79..980680c7d 100644 --- a/plugins/arm_thumb/thumb_flags.ml +++ b/plugins/arm_thumb/thumb_flags.ml @@ -49,16 +49,3 @@ module Flags(Core : Theory.Core) = struct let set_sbc s1 s2 r = set_adc s1 (not s2) r end - -(* - -let set_cf_data ~imm ~data = - let value = - let width = Word.bitwidth imm in - if Word.(of_int ~width 255 >= imm && imm >= zero width) then - let width = Word.bitwidth data in - if Word.(Int_exn.(data land of_int ~width 0xf00) = zero width) - then Bil.unknown "undefined" bool_t - else Bil.int Word.b0 - else msb Bil.(int imm) in - Bil.move Env.cf value*) \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_insn.ml b/plugins/arm_thumb/thumb_insn.ml new file mode 100644 index 000000000..e9e9ec642 --- /dev/null +++ b/plugins/arm_thumb/thumb_insn.ml @@ -0,0 +1,36 @@ +open Core_kernel +open Bap.Std +open Or_error + +type t = Thumb_defs.insn [@@deriving bin_io, compare, sexp] +type regs = Thumb_defs.reg [@@deriving bin_io, compare, sexp] + +let sexpable_of_string t_of_sexp name = + try Some (t_of_sexp @@ Sexp.of_string name) + with Sexp.Of_sexp_error _ -> None + +let of_name name = + sexpable_of_string t_of_sexp name + +let of_basic insn = of_name (Disasm_expert.Basic.Insn.name insn) +let create insn = of_name (Insn.name insn) + +let create_reg reg : Thumb_defs.reg option = + sexpable_of_string regs_of_sexp (Reg.name reg) + +let create_op : op -> Thumb_defs.op option = + let open Option.Monad_infix in + function + | Op.Fmm fmm -> None (* this should be later extended *) + | Op.Reg reg -> create_reg reg >>| fun reg -> `Reg reg + | Op.Imm imm -> + Imm.to_word ~width:32 imm >>| fun imm -> `Imm imm + +let arm_ops_exn ops () = + Array.map (ops) ~f:(fun op -> + Option.value_exn + ~here:[%here] + ~error:(Error.create "unsupported operand" op Op.sexp_of_t ) + (create_op op)) + +let arm_ops ops = try_with ~backtrace:true (arm_ops_exn ops) diff --git a/plugins/arm_thumb/thumb_mov.ml b/plugins/arm_thumb/thumb_mov.ml index eed04f470..e0f6eeacc 100644 --- a/plugins/arm_thumb/thumb_mov.ml +++ b/plugins/arm_thumb/thumb_mov.ml @@ -4,6 +4,7 @@ open KB.Syntax module Env = Thumb_env.Env module Flags = Thumb_flags.Flags +module Defs = Thumb_defs exception Lift_Error = Thumb_defs.Lift_Error @@ -12,409 +13,334 @@ module Mov(Core : Theory.Core) = struct module Utils = Thumb_util.Utils(Core) module Flags = Flags(Core) + module DSL = Thumb_dsl.Make(Core) open Utils - let rseq x y = seq y x - - let mover dest src = match dest, src with - | `Reg d, `Reg s -> (move_reg ~lreg:reg_wide d s) - | _ -> raise (Lift_Error "dest or src is not a register") - - let movesr dest src = match dest, src with - | `Reg d, `Reg s -> seq (move_reg d s) (Flags.set_nzf (reg d)) - | _ -> raise (Lift_Error "dest or src is not a register") - - let movei8 dest imm = match dest, imm with - | `Reg d, `Imm v -> seq (set_reg d v) (Flags.set_nzf (reg d)) - | _ -> raise (Lift_Error "incorrect operands") - - let movenot dest src = match dest, src with - | `Reg d, `Reg s -> - let (dest, src) = (reg d, reg s) in - seq - (set dest (not (var src))) - (Flags.set_nzf dest) - | _ -> raise (Lift_Error "dest or src is not a register") - - let mul dest src = match dest, src with - | `Reg d, `Reg s -> - let (dest, src) = (reg d, reg s) in - seq - (set dest (mul (var dest) (var src))) - (Flags.set_nzf dest) - | _ -> raise (Lift_Error "dest or src is not a register") - - let addi3 dest src imm = match dest, src, imm with - | `Reg d, `Reg s, `Imm v -> - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - seq - (set d (add (var s1) s2)) - (Flags.set_add (var s1) s2 d) - | _ -> raise (Lift_Error "incorrect operands") - - let subi3 dest src imm = match dest, src, imm with - | `Reg d, `Reg s, `Imm v -> - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - seq - (set d (sub (var s1) s2)) - (Flags.set_sub (var s1) s2 d) - | _ -> raise (Lift_Error "incorrect operands") + let mover dest src = + DSL.[ + !$$+dest := !$+src + ] + + let movesr dest src = + DSL.[ + !$$dest := !$src; + Flags.set_nzf !$$dest + ] + + let movei8 dest immsrc = + DSL.[ + !$$dest := !$immsrc; + Flags.set_nzf !$$dest + ] + + let movenot dest src = + DSL.[ + !$$dest := not !$src; + Flags.set_nzf !$$dest + ] + + let mul dest src = + DSL.[ + !$$dest := !$dest * !$src; + Flags.set_nzf !$$dest + ] + + let addi3 dest src immsrc = + DSL.[ + !$$dest := !$src + !$immsrc; + Flags.set_add !$src !$immsrc !$$dest + ] + + let subi3 dest src immsrc = + DSL.[ + !$$dest := !$src + !$immsrc; + Flags.set_add !$src !$immsrc !$$dest + ] (* a temp value is introduced here *) - let addi8 dest imm = match dest, imm with - | `Reg d, `Imm v -> - let (d, s) = (reg d, word_as_bitv v) in - seq - (seq - (set Env.tmp (var d)) - (set d (add (var d) s)) - ) - (Flags.set_add (var Env.tmp) s d) - | _ -> raise (Lift_Error "incorrect operands") - - let subi8 dest imm = match dest, imm with - | `Reg d, `Imm v -> - let (d, s) = (reg d, word_as_bitv v) in - seq - (seq - (set Env.tmp (var d)) - (set d (sub (var d) s)) - ) - (Flags.set_sub (var Env.tmp) s d) - | _ -> raise (Lift_Error "incorrect operands") - - let addrr d s1 s2 = match d, s1, s2 with - | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (add (var s1) (var s2))) - (Flags.set_add (var s1) (var s2) d) - | _ -> raise (Lift_Error "operands must be registers") - - let subrr d s1 s2 = match d, s1, s2 with - | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (sub (var s1) (var s2))) - (Flags.set_sub (var s1) (var s2) d) - | _ -> raise (Lift_Error "operands must be registers") - - let addhirr d s = match d, s with - | `Reg d, `Reg s -> - let (d, s) = (reg_wide d, reg_wide s) in - set d (add (var d) (var s)) - | _ -> raise (Lift_Error "operands must be registers") + let addi8 dest immsrc = + DSL.[ + Env.tmp := !$dest; + !$$dest := !$dest + !$immsrc; + Flags.set_add (var Env.tmp) !$immsrc !$$dest + ] + + let subi8 dest immsrc = + DSL.[ + Env.tmp := !$dest; + !$$dest := !$dest - !$immsrc; + Flags.set_sub (var Env.tmp) !$immsrc !$$dest + ] + + let addrr d s1 s2 = + DSL.[ + !$$d := !$s1 + !$s2; + Flags.set_add !$s1 !$s2 !$$d + ] + + let subrr d s1 s2 = + DSL.[ + !$$d := !$s1 + !$s2; + Flags.set_sub !$s1 !$s2 !$$d + ] + + let addhirr d s = + DSL.[ + !$$+d := !$+d + !$+s; + ] (* Rd = (PC and 0xfffffffc) + (imm << 2) *) - let adr dest imm = match dest, imm with - | `Reg d, `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let (d, s) = (reg d, word_as_bitv v) in - set d (add (logand (var Env.pc) (bitv_of 0xFFFFFFFC)) (shift s)) - | _ -> raise (Lift_Error "incorrect operands") - - let addrspi dest imm = match dest, imm with - | `Reg d, `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let (d, s) = (reg d, word_as_bitv v) in - set d (add (var Env.sp) (shift s)) - | _ -> raise (Lift_Error "incorrect operands") - - let addspi imm = match imm with - | `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let s = word_as_bitv v in - set Env.sp (add (var Env.sp) (shift s)) - | _ -> raise (Lift_Error "imm must be an immediate") - - let subspi imm = match imm with - | `Imm v -> - let shift x = bitv_of 2 |> shiftl b0 x in - let s = word_as_bitv v in - set Env.sp (sub (var Env.sp) (shift s)) - | _ -> raise (Lift_Error "imm must be an immediate") - - let adc d s1 s2 = match d, s1, s2 with - | `Reg d, `Reg s1, `Reg s2 -> - let (d, s1, s2) = (reg d, reg s1, reg s2) in - seq - (set d (add (add (var s1) (var s2)) (bool_as_bitv (var Env.cf)))) - (Flags.set_adc (var s1) (var s2) d) - | _ -> raise (Lift_Error "operands must be registers") - - let sbc d s = match d, s with - | `Reg d, `Reg s -> - let (d, s) = (reg d, reg s) in - seq - (seq - (set Env.tmp (var d)) - (set d (add (sub (var d) (var s)) (bool_as_bitv (var Env.cf)))) - ) - (Flags.set_sbc (var Env.tmp) (var s) d) - | _ -> raise (Lift_Error "operands must be registers") - - let andrr dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq (set d (logand (var d) (var s))) (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") - - let asri dest src imm = match dest, src, imm with - | `Reg d, `Reg s, `Imm v -> - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - (if Bap.Std.Word.is_zero v then - seq - (set Env.cf (var s1 |> msb)) - (set d (ite (var s1 |> msb) (bitv_of 0xffffffff) (bitv_of 0))) - else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in - seq - (set Env.cf (nth_bit take_n (var s1))) - (set d (arshift (var s1) s2))) - |> rseq (Flags.set_nzf d) - | _ -> raise (Lift_Error "incorrect operands") + let adr dest immsrc = + DSL.[ + !$$dest := (var Env.pc) land (imm 0xFFFFFFFC) + !$immsrc << !!2 + ] + + let addrspi dest immsrc = + DSL.[ + !$$dest := (var Env.sp) + !$immsrc << !!2 + ] + + let addspi immsrc = + DSL.[ + Env.sp := (var Env.sp) + !$immsrc << !!2 + ] + + let subspi immsrc = + DSL.[ + Env.sp := (var Env.sp) - !$immsrc << !!2 + ] + + let adc d s1 s2 = + DSL.[ + !$$d := !$s1 + !$s2 + bool_as_bitv (var Env.cf); + Flags.set_adc !$s1 !$s2 !$$d + ] + + let sbc d s = + DSL.[ + Env.tmp := !$d; + !$$d := !$s + !$d + bool_as_bitv (var Env.cf); + Flags.set_sbc (var Env.tmp) !$s !$$s + ] + + let andrr dest src = + DSL.[ + !$$dest := !$dest land !$src; + Flags.set_nzf !$$dest + ] + + open Bap.Std + + let asri dest src srcimm = + let shift_amt = Defs.assert_imm srcimm in + DSL.[ + when_else_ (Word.is_zero shift_amt) [ + Env.cf := msb !$src; + if_else_ (msb !$src) [ + !$$dest := !!0xffffffff + ] (*else*) [ + !$$dest := !!0 + ] + ] (*else*) [ + Env.cf := nth_bit (!$srcimm - !!1) !$src; + !$$dest := !$src asr !$srcimm + ]; + Flags.set_nzf !$$dest + ] (* ASRr has a rather complex logic, see A7.1.12 *) - let asrr dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - (seq - (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var Env.cf) - (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) - ) - (msb (var d)) - ) - ) - (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var d) - (arshift (var d) seg) - ) - (ite (msb (var d)) - (bitv_of 0xffffffff) - (bitv_of 0) - ) - ) - )) |> rseq (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") - - let bic dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set d (logand (var d) (not (var s)))) - (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") - - let cmnz dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set Env.tmp (add (var d) (var s))) - (Flags.set_add (var d) (var s) Env.tmp) - | _ -> raise (Lift_Error "dest or src is not a register") - - let cmpi8 dest imm = match dest, imm with - | `Reg d, `Imm v -> - let (d, s) = (reg d, word_as_bitv v) in - seq - (set Env.tmp (sub (var d) s)) - (Flags.set_sub (var d) s Env.tmp) - | _ -> raise (Lift_Error "incorrect operands") - - let cmpr dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set Env.tmp (sub (var d) (var s))) - (Flags.set_sub (var d) (var s) Env.tmp) - | _ -> raise (Lift_Error "dest or src is not a register") - - let cmphir dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg_wide d, reg_wide s in - seq - (set Env.tmp (sub (var d) (var s))) - (Flags.set_sub (var d) (var s) Env.tmp) - | _ -> raise (Lift_Error "dest or src is not a register") - - let eor dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set d (logxor (var d) (var s))) - (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") - - let lsli dest src imm = match dest, src, imm with - | `Reg d, `Reg s, `Imm v -> - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - (if Bap.Std.Word.is_zero v then - set d (var s1) - else let take_n = Bap.Std.Word.sub (Bap.Std.Word.of_int 32 32) v |> word_as_bitv in - seq - (set Env.cf (nth_bit take_n (var s1))) - (set d (shiftl b0 (var s1) s2))) - |> rseq (Flags.set_nzf d) - | _ -> raise (Lift_Error "incorrect operands") + let asrr dest src = + let seg = DSL.(extend_to Env.byte !$src |> extend) in + DSL.[ + if_else_ (seg <+ !!32) [ + if_ (seg <> !!0) [ + Env.cf := nth_bit (seg - !!1) !$dest; + !$$dest := !$dest asr seg + ] + ] (*else*) [ + Env.cf := msb !$dest; + if_else_ (msb !$dest) [ + !$$dest := !!0xffffffff + ] (*else*) [ + !$$dest := !!0 + ] + ]; + Flags.set_nzf !$$dest + ] + + let bic dest src = + DSL.[ + !$$dest := !$dest land lnot !$src; + Flags.set_nzf !$$dest + ] + + let cmnz dest src = + DSL.[ + Env.tmp := !$dest + !$src; + Flags.set_add !$dest !$src Env.tmp + ] + + let cmpi8 dest immsrc = + DSL.[ + Env.tmp := !$dest - !$immsrc; + Flags.set_sub !$dest !$immsrc Env.tmp + ] + + let cmpr dest src = + DSL.[ + Env.tmp := !$dest - !$src; + Flags.set_sub !$dest !$src Env.tmp + ] + + let cmphir dest src = + DSL.[ + Env.tmp := !$+dest - !$+src; + Flags.set_sub !$+dest !$+src Env.tmp + ] + + let eor dest src = + DSL.[ + !$$dest := !$dest lxor !$src; + Flags.set_nzf !$$dest + ] + + let lsli dest src immsrc = + let shift_amt = Defs.assert_imm immsrc in + DSL.[ + when_else_ (Word.is_zero shift_amt) [ + !$$dest := !$src + ] (*else*) [ + Env.cf := nth_bit (!!32 - !$immsrc) !$src; + !$$dest := !$src << !$immsrc + ]; + Flags.set_nzf !$$dest + ] (* LSLr has a rather complex logic, see A7.1.39 *) - let lslr dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - (seq - (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var Env.cf) - (nth_bit (sub (bitv_of 32 |> cast Env.byte b0) seg) (var d)) - ) - (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) - (lsb (var d)) - b0 - ) - ) - ) - (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var d) - (shiftl b0 (var d) seg) - ) - (zero Env.value) - ) - )) |> rseq (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") - - let lsri dest src imm = match dest, src, imm with - | `Reg d, `Reg s, `Imm v -> - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - (if Bap.Std.Word.is_zero v then - seq - (set Env.cf (var s1 |> msb)) - (set d (bitv_of 0)) - else let take_n = Bap.Std.Word.sub v (Bap.Std.Word.of_int 32 1) |> word_as_bitv in - seq - (set Env.cf (nth_bit take_n (var s1))) - (set d (shiftr b0 (var s1) s2))) - |> rseq (Flags.set_nzf d) - | _ -> raise (Lift_Error "incorrect operands") - - let lsrr dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - (seq - (set Env.cf (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var Env.cf) - (nth_bit (sub seg (bitv_of 1 |> cast Env.byte b0)) (var d)) - ) - (ite (eq seg (bitv_of 32 |> cast Env.byte b0)) - (msb (var d)) - b0 - ) - ) - ) - (set d (ite (ult seg (bitv_of 32 |> cast Env.byte b0)) - (ite (eq seg (zero Env.byte)) - (var d) - (shiftr b0 (var d) seg) - ) - (zero Env.value) - ) - )) |> rseq (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") - - let orr dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq (set d (logor (var d) (var s))) (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") + let lslr dest src = + let seg = DSL.(extend_to Env.byte !$src |> extend) in + DSL.[ + if_else_ (seg <+ !!32) [ + if_ (seg <> !!0) [ + Env.cf := nth_bit (!!32 - seg) !$dest; + !$$dest := !$dest << seg + ] + ] (*else*) [ + if_else_ (seg = !!32) [ + Env.cf := lsb !$dest + ] (*else*) [ + Env.cf := b0 + ]; + !$$dest := !!0 + ]; + Flags.set_nzf !$$dest + ] + + let lsri dest src immsrc = + let shift_amt = Defs.assert_imm immsrc in + DSL.[ + when_else_ (Word.is_zero shift_amt) [ + Env.cf := msb !$src; + !$$dest := !!0 + ] (*else*) [ + Env.cf := nth_bit (!$immsrc - !!1) !$src; + !$$dest := !$src >> !$immsrc + ]; + Flags.set_nzf !$$dest + ] + + let lsrr dest src = + let seg = DSL.(extend_to Env.byte !$src |> extend) in + DSL.[ + if_else_ (seg <+ !!32) [ + if_ (seg <> !!0) [ + Env.cf := nth_bit (seg - !!1) !$dest; + !$$dest := !$dest >> seg + ] + ] (*else*) [ + if_else_ (seg = !!32) [ + Env.cf := msb !$dest + ] (*else*) [ + Env.cf := b0 + ]; + !$$dest := !!0 + ]; + Flags.set_nzf !$$dest + ] + + let orr dest src = + DSL.[ + !$$dest := !$dest lor !$src; + Flags.set_nzf !$$dest + ] (* This is actually code named `neg Rd Rm`, but llvm encodes it as `rsb Rd Rm #0` *) - let rsb dest src imm = match dest, src, imm with - | `Reg d, `Reg s, `Imm v -> - let (d, s1, s2) = (reg d, reg s, word_as_bitv v) in - seq - (set d (sub s2 (var s1))) - (Flags.set_sub s2 (var s1) d) - | _ -> raise (Lift_Error "incorrect operands") - - let rev dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - let s = var s in - let i24 = bitv_of 24 in - let i8 = bitv_of 8 in - let umask = bitv_of 0xff0000 in - let lmask = bitv_of 0xff00 in - let rev = - logor (lshift s i24) - (logor (rshift s i24) - (logor - (rshift (logand s umask) i8) - (lshift (logand s lmask) i8) - ) - ) - in set d rev - | _ -> raise (Lift_Error "dest or src is not a register") + let rsb dest src immsrc = + DSL.[ + !$$dest := !$immsrc - !$src; + Flags.set_sub !$immsrc !$src !$$dest + ] + + let rev dest src = + DSL.[ + !$$dest := concat Env.value [ + extract Env.byte !!7 !!0 !$src; + extract Env.byte !!15 !!8 !$src; + extract Env.byte !!23 !!16 !$src; + extract Env.byte !!31 !!24 !$src; + ] + ] let rev_halfword hf = let i8 = bitv_of 8 in logor (lshift hf i8) (rshift hf i8) - let rev16 dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - let s = var s in - let rev_extend v = - cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in - let i16 = bitv_of 16 in - let rev = logor - (rev_extend s) - (rshift s i16 |> rev_extend |> lshift i16) - in set d rev - | _ -> raise (Lift_Error "dest or src is not a register") - - let revsh dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - let s = var s in - let rev_extend v = - cast Env.half_word b0 v |> rev_halfword |> cast Env.value b0 in - let rev = logand (rev_extend s) - (ite (cast Env.byte b0 s |> msb) - (bitv_of 0xffff0000) - (bitv_of 0) - ) - in set d rev - | _ -> raise (Lift_Error "dest or src is not a register") - - let ror dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - let nth_bit n e = cast Env.bit_val b0 (shiftr b0 e n) |> msb in - let seg = cast Env.byte b0 (var s) in - let seg4 = cast Env.half_byte b0 (var s) in - (seq - (set Env.cf (ite (eq seg (zero Env.byte)) - (var Env.cf) - (ite (eq seg4 (zero Env.half_byte)) - (msb (var d)) - (nth_bit (sub seg4 (bitv_of 1 |> cast Env.half_byte b0)) (var d)) - ) - ) - ) - (set d (ite (eq seg4 (zero Env.half_byte)) - (var d) - ( - let seg4_comp = sub (bitv_of 32 |> cast Env.half_byte b0) seg4 in - logand (rshift (var d) seg4) (lshift (var d) seg4_comp) - ) - ) - )) |> rseq (Flags.set_nzf d) - | _ -> raise (Lift_Error "dest or src is not a register") - - let tst dest src = match dest, src with - | `Reg d, `Reg s -> let d, s = reg d, reg s in - seq - (set Env.tmp (logand (var d) (var s))) - (Flags.set_nzf Env.tmp) - | _ -> raise (Lift_Error "dest or src is not a register") + let rev16 dest src = + DSL.[ + !$$dest := concat Env.value [ + extract Env.byte !!23 !!16 !$src; + extract Env.byte !!31 !!24 !$src; + extract Env.byte !!7 !!0 !$src; + extract Env.byte !!15 !!8 !$src; + ] + ] + + let revsh dest src = + DSL.[ + if_else_ (msb (extend_to Env.byte !$src)) [ + !$$dest := concat Env.value [ + extend_to Env.byte !!0xff; + extend_to Env.byte !!0xff; + extract Env.byte !!7 !!0 !$src; + extract Env.byte !!15 !!8 !$src; + ] + ] (*else*) [ + !$$dest := concat Env.value [ + extend_to Env.byte !!0x00; + extend_to Env.byte !!0x00; + extract Env.byte !!7 !!0 !$src; + extract Env.byte !!15 !!8 !$src; + ] + ] + ] + + let ror dest src = + let seg4 = DSL.(extend_to Env.half_byte !$src |> extend) in + DSL.[ + if_else_ (seg4 = !!0) [ + Env.cf := msb !$dest + ] (*else*) [ + Env.cf := nth_bit (seg4 - !!1) !$dest; + !$$dest := !$dest >> seg4 lor !$dest << (!!32 - seg4) + ]; + Flags.set_nzf !$$dest + ] + + let tst dest src = + DSL.[ + Env.tmp := !$dest land !$src; + Flags.set_nzf Env.tmp + ] end \ No newline at end of file From 640c80a976ea3123f4d46de8c272b2685e9f79dc Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Tue, 14 Jul 2020 18:10:37 +0800 Subject: [PATCH 21/25] .merlin file update --- plugins/arm_thumb/.merlin | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/plugins/arm_thumb/.merlin b/plugins/arm_thumb/.merlin index 2fb3f0bc1..66b4a77b8 100644 --- a/plugins/arm_thumb/.merlin +++ b/plugins/arm_thumb/.merlin @@ -1 +1,3 @@ -REC \ No newline at end of file +REC + +B ./_build \ No newline at end of file From 6f66029a4a30aac2d976225039e298fabc8e9083 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Tue, 14 Jul 2020 18:28:14 +0800 Subject: [PATCH 22/25] ocp-indent rerun --- plugins/arm_thumb/thumb.ml | 2 +- plugins/arm_thumb/thumb_branch.ml | 48 +++++++++++++++---------------- 2 files changed, 25 insertions(+), 25 deletions(-) diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index b80b6059f..0a41a77d4 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -164,7 +164,7 @@ module Thumb(Core : Theory.Core) = struct | #bits_insn -> lift_bits insn ops |> DSL.expand |> move | #branch_insn -> let (ctrl_eff, data_eff) = lift_branch insn ops addr in - ctrl ctrl_eff data_eff addr (* var Env.pc *) + ctrl ctrl_eff data_eff addr (* var Env.pc *) end diff --git a/plugins/arm_thumb/thumb_branch.ml b/plugins/arm_thumb/thumb_branch.ml index 0bbc01532..1000001c2 100644 --- a/plugins/arm_thumb/thumb_branch.ml +++ b/plugins/arm_thumb/thumb_branch.ml @@ -53,42 +53,42 @@ module Branch(Core : Theory.Core) = struct let tb target addr = (DSL.( - jmp (!$target + addr << !!1) - ), DSL.( - Env.pc := (!$target + addr << !!1) - )) + jmp (!$target + addr << !!1) + ), DSL.( + Env.pc := (!$target + addr << !!1) + )) let tbl target = (DSL.( - jmp !$target - ), DSL.[ - Env.lr := (var Env.pc) + !!2 lor !!1; - Env.pc := !$target - ] |> DSL.expand) + jmp !$target + ), DSL.[ + Env.lr := (var Env.pc) + !!2 lor !!1; + Env.pc := !$target + ] |> DSL.expand) (* TODO : switch to normal mode *) let tblxi target = (DSL.( - jmp (!$target land !!0xfffffffc) - ), DSL.[ - Env.lr := (var Env.pc) + !!2 lor !!1; - Env.pc := (!$target land !!0xfffffffc) - ] |> DSL.expand) + jmp (!$target land !!0xfffffffc) + ), DSL.[ + Env.lr := (var Env.pc) + !!2 lor !!1; + Env.pc := (!$target land !!0xfffffffc) + ] |> DSL.expand) let tblxr target = (DSL.( - jmp (!$target land !!0xfffffffe) - ), DSL.[ - Env.lr := (var Env.pc) + !!2 lor !!1; - Env.pc := (!$target land !!0xfffffffe) - ] |> DSL.expand) + jmp (!$target land !!0xfffffffe) + ), DSL.[ + Env.lr := (var Env.pc) + !!2 lor !!1; + Env.pc := (!$target land !!0xfffffffe) + ] |> DSL.expand) let tbx target = (DSL.( - (* reference here is PC = Rm[31:1] << 1 *) - jmp (extract Env.value !!31 !!1 !$target << !!1) - ), DSL.( - Env.pc := (extract Env.value !!31 !!1 !$target << !!1) - )) + (* reference here is PC = Rm[31:1] << 1 *) + jmp (extract Env.value !!31 !!1 !$target << !!1) + ), DSL.( + Env.pc := (extract Env.value !!31 !!1 !$target << !!1) + )) end \ No newline at end of file From 8e019a0fcce40ca58c61439d3940329c82a167fb Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Wed, 15 Jul 2020 00:03:06 +0800 Subject: [PATCH 23/25] address assigned to LR should be subtracted --- plugins/arm_thumb/thumb_branch.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/arm_thumb/thumb_branch.ml b/plugins/arm_thumb/thumb_branch.ml index 1000001c2..2f761eeb1 100644 --- a/plugins/arm_thumb/thumb_branch.ml +++ b/plugins/arm_thumb/thumb_branch.ml @@ -62,7 +62,7 @@ module Branch(Core : Theory.Core) = struct (DSL.( jmp !$target ), DSL.[ - Env.lr := (var Env.pc) + !!2 lor !!1; + Env.lr := (var Env.pc) - !!2 lor !!1; Env.pc := !$target ] |> DSL.expand) @@ -71,7 +71,7 @@ module Branch(Core : Theory.Core) = struct (DSL.( jmp (!$target land !!0xfffffffc) ), DSL.[ - Env.lr := (var Env.pc) + !!2 lor !!1; + Env.lr := (var Env.pc) - !!2 lor !!1; Env.pc := (!$target land !!0xfffffffc) ] |> DSL.expand) @@ -79,7 +79,7 @@ module Branch(Core : Theory.Core) = struct (DSL.( jmp (!$target land !!0xfffffffe) ), DSL.[ - Env.lr := (var Env.pc) + !!2 lor !!1; + Env.lr := (var Env.pc) - !!2 lor !!1; Env.pc := (!$target land !!0xfffffffe) ] |> DSL.expand) From a8cd86be87b6e58955281f12fe2607574d054585 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Wed, 15 Jul 2020 00:17:44 +0800 Subject: [PATCH 24/25] register KB semantics promise --- plugins/arm_thumb/thumb.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 0a41a77d4..9b9766a72 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -163,7 +163,7 @@ module Thumb(Core : Theory.Core) = struct | #mem_insn -> lift_mem insn ops addr | #bits_insn -> lift_bits insn ops |> DSL.expand |> move | #branch_insn -> - let (ctrl_eff, data_eff) = lift_branch insn ops addr in + let ctrl_eff, data_eff = lift_branch insn ops addr in ctrl ctrl_eff data_eff addr (* var Env.pc *) end @@ -179,17 +179,14 @@ let run_lifter _label addr insn _mem | Error err -> raise (Defs.Lift_Error (Error.to_string_hum err)) | Ok ops -> lifter addr arm_insn ops -let provide_sematics insn effect = - KB.provide Theory.Program.Semantics.slot insn effect >>| fun () -> insn - -let lift label = +let () = + KB.promise Theory.Program.Semantics.slot @@ fun label -> Theory.instance () >>= Theory.require >>= fun (module Core) -> - KB.collect Theory.Label.addr label >>= fun addr -> (* this is the address of the current instruction *) KB.collect Disasm_expert.Basic.Insn.slot label >>= fun insn -> (* the LLVM provided decoding *) KB.collect Memory.slot label >>= fun mem -> (* the memory chunk, probably not needed *) let module Lifter = Thumb(Core) in - match addr, insn, mem with - | Some addr, Some insn, Some mem -> - run_lifter label addr insn mem Lifter.lift_with >>= fun sema -> - provide_sematics label sema - | _ -> provide_sematics label Insn.empty \ No newline at end of file + match insn, mem with + | Some insn, Some mem -> + let addr = Word.to_bitvec@@Memory.min_addr mem in + run_lifter label addr insn mem Lifter.lift_with + | _ -> KB.return Insn.empty \ No newline at end of file From b48931b7e4fc3efd4793eff9ab50a38560d80fd5 Mon Sep 17 00:00:00 2001 From: Phosphorus15 Date: Wed, 15 Jul 2020 23:26:07 +0800 Subject: [PATCH 25/25] now its up and working --- plugins/arm_thumb/test_sample.txt | 582 ++++++++++++++++++++++++++++++ plugins/arm_thumb/thumb.ml | 165 ++++----- plugins/arm_thumb/thumb_branch.ml | 20 +- plugins/arm_thumb/thumb_defs.ml | 2 + plugins/arm_thumb/thumb_insn.ml | 7 +- plugins/arm_thumb/thumb_mem.ml | 35 +- plugins/arm_thumb/thumb_mov.ml | 15 +- 7 files changed, 715 insertions(+), 111 deletions(-) create mode 100644 plugins/arm_thumb/test_sample.txt diff --git a/plugins/arm_thumb/test_sample.txt b/plugins/arm_thumb/test_sample.txt new file mode 100644 index 000000000..2d99b3fac --- /dev/null +++ b/plugins/arm_thumb/test_sample.txt @@ -0,0 +1,582 @@ +tADC: +4c 41 +{ + tmp := r4 + r4 := r4 + r1 + (if cf then 1 else 0) + cf := high:1[pad:33[tmp] + pad:33[r1] + (if cf then 1 else 0)] + vf := high:1[~(tmp ^ r1) & (tmp ^ r4)] + nf := high:1[r4] + zf := r4 = 0 +} +tADDi3: +4b 1d +{ + r3 := r1 + 5 + cf := r3 <$ r1 + vf := high:1[~(r1 ^ 5) & (r1 ^ r3)] + nf := high:1[r3] + zf := r3 = 0 +} +tADDi8: +11 31 +{ + tmp := r1 + r1 := r1 + 0x11 + cf := r1 <$ tmp + vf := high:1[~(tmp ^ 0x11) & (tmp ^ r1)] + nf := high:1[r1] + zf := r1 = 0 +} +tADDrr: +5d 18 +{ + r5 := r3 + r1 + cf := r5 <$ r3 + vf := high:1[~(r3 ^ r1) & (r3 ^ r5)] + nf := high:1[r5] + zf := r5 = 0 +} +tADDhirr: +cb 44 +{ + r11 := r11 + r9 +} +tADR: +11 a1 +{ + r1 := (pc & 0xFFFFFFFC) + 0x11 << 2 +} +tADDrSPi: +11 aa +{ + r2 := sp + 0x11 << 2 +} +tADDspi: +07 b0 +{ + sp := sp + 7 << 2 +} +tMOVi8: +11 27 +{ + r7 := 0x11 + nf := high:1[r7] + zf := r7 = 0 +} +tMOVr: +89 46 +{ + r9 := r1 +} +tMUL: +4f 43 +{ + r7 := r7 * r1 + nf := high:1[r7] + zf := r7 = 0 +} +tMVN: +cb 43 +{ + r3 := ~r1 + nf := high:1[r3] + zf := r3 = 0 +} +tSBC: +8b 41 +{ + tmp := r3 + r3 := r1 - r3 - (if ~cf then 1 else 0) + cf := high:1[pad:33[tmp] + pad:33[~r1] + (if cf then 1 else 0)] + vf := high:1[~(tmp ^ ~r1) & (tmp ^ r1)] + nf := high:1[r1] + zf := r1 = 0 +} +tSUBi3: +8b 1f +{ + r3 := r1 - 6 + cf := 6 <=$ r1 + vf := high:1[(r1 ^ 6) & (r1 ^ r3)] + nf := high:1[r3] + zf := r3 = 0 +} +tSUBi8: +8b 3f +{ + tmp := r7 + r7 := r7 - 0x8B + cf := 0x8B <=$ tmp + vf := high:1[(tmp ^ 0x8B) & (tmp ^ r7)] + nf := high:1[r7] + zf := r7 = 0 +} +tSUBrr: +8b 1b +{ + r3 := r1 - r6 + cf := r6 <=$ r1 + vf := high:1[(r1 ^ r6) & (r1 ^ r3)] + nf := high:1[r3] + zf := r3 = 0 +} +tSUBspi: +8b b0 +{ + sp := sp - 0xB << 2 +} +tAND: +0b 40 +{ + r3 := r3 & r1 + nf := high:1[r3] + zf := r3 = 0 +} +tASRri: +8b 10 +{ + cf := low:1[r1 >> 1] + r3 := r1 ~>> 2 + nf := high:1[r3] + zf := r3 = 0 +} +0b 10 +{ + cf := high:1[r1] + if (high:1[r1]) { + r3 := 0xFFFFFFFF + } + else { + r3 := 0 + } + nf := high:1[r3] + zf := r3 = 0 +} +tASRrr: +0b 41 +{ + if (pad:32[low:8[r1]] < 0x20) { + if (pad:32[low:8[r1]] <> 0) { + cf := low:1[r3 >> pad:32[low:8[r1]] - 1] + r3 := r3 ~>> pad:32[low:8[r1]] + } + } + else { + cf := high:1[r3] + if (high:1[r3]) { + r3 := 0xFFFFFFFF + } + else { + r3 := 0 + } + } + nf := high:1[r3] + zf := r3 = 0 +} +tBIC: +8b 43 +{ + r3 := r3 & ~r1 + nf := high:1[r3] + zf := r3 = 0 +} +tCMPi8: +11 29 +{ + tmp := r1 - 0x11 + cf := 0x11 <=$ r1 + vf := high:1[(r1 ^ 0x11) & (r1 ^ tmp)] + nf := high:1[tmp] + zf := tmp = 0 +} +tCMPr: +91 42 +{ + tmp := r1 - r2 + cf := r2 <=$ r1 + vf := high:1[(r1 ^ r2) & (r1 ^ tmp)] + nf := high:1[tmp] + zf := tmp = 0 +} +tCMPhir: +91 45 +{ + tmp := r9 - r2 + cf := r2 <=$ r9 + vf := high:1[(r9 ^ r2) & (r9 ^ tmp)] + nf := high:1[tmp] + zf := tmp = 0 +} +tEOR: +51 40 +{ + r1 := r1 ^ r2 + nf := high:1[r1] + zf := r1 = 0 +} +tLSLri: +51 00 +{ + cf := low:1[r2 >> 0x1F] + r1 := r2 << 1 + nf := high:1[r1] + zf := r1 = 0 +} +tLSLrr: +91 40 +{ + if (pad:32[low:8[r2]] < 0x20) { + if (pad:32[low:8[r2]] <> 0) { + cf := low:1[r1 >> 0x20 - pad:32[low:8[r2]]] + r1 := r1 << pad:32[low:8[r2]] + } + } + else { + if (pad:32[low:8[r2]] = 0x20) { + cf := low:1[r1] + } + else { + cf := 0 + } + r1 := 0 + } + nf := high:1[r1] + zf := r1 = 0 +} +tLSRri: +51 08 +{ + cf := low:1[r2] + r1 := r2 >> 1 + nf := high:1[r1] + zf := r1 = 0 +} +tLSRrr: +d1 40 +{ + if (pad:32[low:8[r2]] < 0x20) { + if (pad:32[low:8[r2]] <> 0) { + cf := low:1[r1 >> pad:32[low:8[r2]] - 1] + r1 := r1 >> pad:32[low:8[r2]] + } + } + else { + if (pad:32[low:8[r2]] = 0x20) { + cf := high:1[r1] + } + else { + cf := 0 + } + r1 := 0 + } + nf := high:1[r1] + zf := r1 = 0 +} +tORR: +11 43 +{ + r1 := r1 | r2 + nf := high:1[r1] + zf := r1 = 0 +} +tRSB: +51 42 +{ + r1 := -r2 + cf := r2 <=$ 0 + vf := high:1[r2 & r1] + nf := high:1[r1] + zf := r1 = 0 +} +tREV: +11 ba +{ + r1 := extract:7:0[r2].extract:15:8[r2].extract:23:16[r2].extract:31:24[r2] +} +tREV16: +51 ba +{ + r1 := extract:23:16[r2].extract:31:24[r2].extract:7:0[r2].extract:15:8[r2] +} +tREVSH: +d1 ba +{ + if (high:1[low:8[r2]]) { + r1 := 0xFF.0xFF.extract:7:0[r2].extract:15:8[r2] + } + else { + r1 := 0.0.extract:7:0[r2].extract:15:8[r2] + } +} +tROR: +d3 41 +{ + if (pad:32[low:4[r2]] = 0) { + cf := high:1[r3] + } + else { + cf := low:1[r3 >> pad:32[low:4[r2]] - 1] + r3 := r3 >> (pad:32[low:4[r2]] | r3) << 0x20 - pad:32[low:4[r2]] + } + nf := high:1[r3] + zf := r3 = 0 +} +tTST: +13 42 +{ + tmp := r3 & r2 + nf := high:1[tmp] + zf := tmp = 0 +} +-- bits instructions +tSXTB: +57 b2 +{ + r7 := extend:32[low:8[r2]] +} +tSXTH: +17 b2 +{ + r7 := extend:32[low:16[r2]] +} +tUXTB: +d7 b2 +{ + r7 := pad:32[low:8[r2]] +} +tUXTH: +97 b2 +{ + r7 := pad:32[low:16[r2]] +} +-- branch instructions (* following takes the instruction address as 0 *) +tBcc: +65 d1 +{ + if (~zf) { + pc := 0xCA + } + if (~zf) { + jmp 0xCA + } +} +7f dd +{ + if (zf | ~(nf & vf | ~nf & ~vf)) { + pc := 0xFE + } + if (zf | ~(nf & vf | ~nf & ~vf)) { + jmp 0xFE + } +} +tB: +aa e0 +{ + pc := 0x154 + jmp 0x154 +} +tBL: +01 f0 01 f8 +{ + lr := pc - 2 | 1 + pc := 0x1002 + jmp 0x1002 +} +tBLXi: +06 f0 06 e8 +{ + lr := pc - 2 | 1 + pc := 0x600C + jmp 0x600C +} +tBLXr: +d8 47 +{ + lr := pc - 2 | 1 + pc := r11 & 0xFFFFFFFE + jmp (r11 & 0xFFFFFFFE) +} +tBX: +50 47 +{ + pc := (0x7FFFFFFF & r10 >> 1) << 1 + jmp ((0x7FFFFFFF & r10 >> 1) << 1) +} +-- mem instructions +tLDRi: +8a 69 +{ + r2 := mem[r1 + 0x18, el]:u32 +} +tLDRr: +0a 59 +{ + r2 := mem[r1 + r4, el]:u32 +} +tLDRpci: +ca 4f +{ + r7 := mem[pc + 0x328, el]:u32 +} +tLDRspi: +0a 99 +{ + r1 := mem[sp + 0x28, el]:u32 +} +tLDRBi: +0a 79 +{ + r2 := pad:32[mem[r1 + 4]] +} +tLDRBi: +0a 5d +{ + r2 := pad:32[mem[r1 + r4]] +} +tLDRHi: +0a 89 +{ + r2 := pad:32[mem[r1 + 8, el]:u16] +} +tLDRHr: +0a 5b +{ + r2 := pad:32[mem[r1 + r4, el]:u16] +} +tLDRSB: +0a 57 +{ + r2 := extend:32[mem[r1 + r4]] +} +tLDRSH: +0a 5f +{ + r2 := extend:32[mem[r1 + r4, el]:u16] +} +tSTRi: +0a 67 +{ + mem := mem with [r1 + 0x70, el]:u32 <- r2 +} +tSTRr: +0a 51 +{ + mem := mem with [r1 + r4, el]:u32 <- r2 +} +tSTRspi: +0a 91 +{ + mem := mem with [sp + 0x28, el]:u32 <- r1 +} +tSTRBi: +0a 71 +{ + mem := mem with [r1 + 4] <- low:8[r2] +} +tSTRBr: +0a 55 +{ + mem := mem with [r1 + r4] <- low:8[r2] +} +tSTRHi: +0a 85 +{ + mem := mem with [r1 + 0x28, el]:u16 <- low:16[r2] +} +tSTRHr: +0a 53 +{ + mem := mem with [r1 + r4, el]:u16 <- low:16[r2] +} +-- multi mem instructions +tSTMIA_UPD: +0b c3 +{ + mem := mem with [r3, el]:u32 <- r0 + r3 := r3 + 4 + mem := mem with [r3, el]:u32 <- r1 + r3 := r3 + 4 + mem := mem with [r3, el]:u32 <- r3 + r3 := r3 + 4 +} +tLDMIA: +ab cd +{ + tmp := r5 + r0 := mem[tmp, el]:u32 + tmp := tmp + 4 + r1 := mem[tmp, el]:u32 + tmp := tmp + 4 + r3 := mem[tmp, el]:u32 + tmp := tmp + 4 + r5 := mem[tmp, el]:u32 + tmp := tmp + 4 + r7 := mem[tmp, el]:u32 + tmp := tmp + 4 + r5 := tmp +} +ab c8 +{ + tmp := r0 + r1 := mem[tmp, el]:u32 + tmp := tmp + 4 + r3 := mem[tmp, el]:u32 + tmp := tmp + 4 + r5 := mem[tmp, el]:u32 + tmp := tmp + 4 + r7 := mem[tmp, el]:u32 + tmp := tmp + 4 + r0 := tmp +} +tPUSH: +ab b5 +{ + tmp := sp - 0x18 + mem := mem with [tmp, el]:u32 <- r0 + tmp := tmp + 4 + mem := mem with [tmp, el]:u32 <- r1 + tmp := tmp + 4 + mem := mem with [tmp, el]:u32 <- r3 + tmp := tmp + 4 + mem := mem with [tmp, el]:u32 <- r5 + tmp := tmp + 4 + mem := mem with [tmp, el]:u32 <- r7 + tmp := tmp + 4 + mem := mem with [tmp, el]:u32 <- lr + tmp := tmp + 4 + sp := sp - 0x18 +} +tPOP: +ab bd +{ + tmp := sp + r0 := mem[tmp, el]:u32 + tmp := tmp + 4 + r1 := mem[tmp, el]:u32 + tmp := tmp + 4 + r3 := mem[tmp, el]:u32 + tmp := tmp + 4 + r5 := mem[tmp, el]:u32 + tmp := tmp + 4 + r7 := mem[tmp, el]:u32 + tmp := tmp + 4 + pc := mem[tmp, el]:u32 & 0xFFFFFFFE + tmp := tmp + 4 + sp := tmp + jmp pc +} +ab bc +{ + tmp := sp + r0 := mem[tmp, el]:u32 + tmp := tmp + 4 + r1 := mem[tmp, el]:u32 + tmp := tmp + 4 + r3 := mem[tmp, el]:u32 + tmp := tmp + 4 + r5 := mem[tmp, el]:u32 + tmp := tmp + 4 + r7 := mem[tmp, el]:u32 + tmp := tmp + 4 + sp := tmp +} \ No newline at end of file diff --git a/plugins/arm_thumb/thumb.ml b/plugins/arm_thumb/thumb.ml index 9b9766a72..28920ed10 100644 --- a/plugins/arm_thumb/thumb.ml +++ b/plugins/arm_thumb/thumb.ml @@ -35,95 +35,97 @@ module Thumb(Core : Theory.Core) = struct let lift_move insn ops = let open Mov in match insn, ops with - | `tADC, [|dest; src1; src2|] -> adc dest src1 src2 - | `tADDi3, [|dest; src; imm|] -> addi3 dest src imm - | `tADDi8, [|dest; imm|] -> addi8 dest imm - | `tADDrr, [|dest; src1; src2|] -> addrr dest src1 src2 - | `tADDhirr, [|dest; src|] -> addhirr dest src - | `tADR, [|dest; imm|] -> adr dest imm - | `tADDrSPi, [|dest; imm|] -> addrspi dest imm - | `tADDspi, [|imm|] -> addspi imm - | `tMOVr, [|dest; src|] -> mover dest src - | `tMOVSr, [|dest; src|] -> movesr dest src - | `tMOVi8, [|dest; imm|] -> movei8 dest imm - | `tMUL, [|dest; src|] -> mul dest src - | `tMVN, [|dest; src|] -> movenot dest src - | `tSBC, [|dest; src|] -> sbc dest src - | `tSUBi3, [|dest; src; imm|] -> subi3 dest src imm - | `tSUBi8, [|dest; imm|] -> subi8 dest imm - | `tSUBrr, [|dest; src1; src2|] -> subrr dest src1 src2 - | `tSUBspi, [|imm|] -> subspi imm - | `tAND, [|dest; src|] -> andrr dest src - | `tASRri, [|dest; src; imm|] -> asri dest src imm - | `tASRrr, [|dest; src|] -> asrr dest src - | `tBIC, [|dest; src|] -> bic dest src - | `tCMNz, [|dest; src|] -> cmnz dest src - | `tCMPi8, [|dest; imm|] -> cmpi8 dest imm - | `tCMPr, [|dest; src|] -> cmpr dest src - | `tCMPhir, [|dest; src|] -> cmphir dest src - | `tEOR, [|dest; src|] -> eor dest src - | `tLSLri, [|dest; src; imm|] -> lsli dest src imm - | `tLSLrr, [|dest; src|] -> lslr dest src - | `tLSRri, [|dest; src; imm|] -> lsri dest src imm - | `tLSRrr, [|dest; src|] -> lsrr dest src - | `tORR, [|dest; src|] -> orr dest src - | `tRSB, [|dest; src; imm (* placeholder *)|] -> rsb dest src imm - | `tREV, [|dest; src|] -> rev dest src - | `tREV16, [|dest; src|] -> rev16 dest src - | `tREVSH, [|dest; src|] -> revsh dest src - | `tROR, [|dest; src|] -> ror dest src - | `tTST, [|dest; src|] -> tst dest src + | `tADC, [|dest; _cpsr; _dest; src; _unknown; _|] -> adc dest src + | `tADDi3, [|dest; _cpsr; src; imm; _unknown; _|] -> addi3 dest src imm + | `tADDi8, [|dest; _cpsr; _dest; imm; _unknown; _|] -> addi8 dest imm + | `tADDrr, [|dest; _cpsr; src1; src2; _unknown; _|] -> addrr dest src1 src2 + | `tADDhirr, [|dest; _dest; src; _unknown; _|] -> addhirr dest src + | `tADR, [|dest; imm; _unknown; _|] -> adr dest imm + | `tADDrSPi, [|dest; `Reg `SP; imm; _unknown; _|] -> addrspi dest imm + | `tADDspi, [|`Reg `SP; _sp; imm; _unknown; _|] -> addspi imm + | `tMOVr, [|dest; src; _unknown; _|] -> mover dest src + | `tMOVSr, [|dest; _cpsr; src; _unknown; _|] -> movesr dest src (* this has been properly encoded by `tADDi3 dest #0 src` *) + | `tMOVi8, [|dest; _cpsr; imm; _unknown; _|] -> movei8 dest imm + | `tMUL, [|dest; _cpsr; src; _dest; _unknown; _|] -> mul dest src + | `tMVN, [|dest; _cpsr; src; _unknown; _|] -> movenot dest src + | `tSBC, [|dest; _cpsr; _dest; src; _unknown; _|] -> sbc dest src + | `tSUBi3, [|dest; _cpsr; src; imm; _unknown; _|] -> subi3 dest src imm + | `tSUBi8, [|dest; _cpsr; _dest; imm; _unknown; _|] -> subi8 dest imm + | `tSUBrr, [|dest; _cpsr; src1; src2; _unknown; _|] -> subrr dest src1 src2 + | `tSUBspi, [|`Reg `SP; _sp; imm; _unknown; _|] -> subspi imm + | `tAND, [|dest; _cpsr; _dest; src; _unknown; _|] -> andrr dest src + | `tASRri, [|dest; _cpsr; src; imm; _unknown; _|] -> asri dest src imm + | `tASRrr, [|dest; _cpsr; _dest; src; _unknown; _|] -> asrr dest src + | `tBIC, [|dest; _cpsr; _dest; src; _unknown; _|] -> bic dest src + | `tCMNz, [|dest; src; _unknown; _|] -> cmnz dest src (* TODO : we've got an error here *) + | `tCMPi8, [|dest; imm; _unknown; _|] -> cmpi8 dest imm + | `tCMPr, [|dest; src; _unknown; _|] -> cmpr dest src + | `tCMPhir, [|dest; src; _unknown; _|] -> cmphir dest src + | `tEOR, [|dest; _cpsr; _dest; src; _unknown; _|] -> eor dest src + | `tLSLri, [|dest; _cpsr; src; imm; _unknown; _|] -> lsli dest src imm + | `tLSLrr, [|dest; _cpsr; _dest; src; _unknown; _|] -> lslr dest src + | `tLSRri, [|dest; _cpsr; src; imm; _unknown; _|] -> lsri dest src imm + | `tLSRrr, [|dest; _cpsr; _dest; src; _unknown; _|] -> lsrr dest src + | `tORR, [|dest; _cpsr; _dest; src; _unknown; _|] -> orr dest src + | `tRSB, [|dest; _cpsr; src; _unknown; _ (* placeholder *)|] -> rsb dest src (`Imm (Bap.Std.Word.zero 32)) + | `tREV, [|dest; src; _unknown; _|] -> rev dest src + | `tREV16, [|dest; src; _unknown; _|] -> rev16 dest src + | `tREVSH, [|dest; src; _unknown; _|] -> revsh dest src + | `tROR, [|dest; _cpsr; _dest; src; _unknown; _|] -> ror dest src + | `tTST, [|dest; src; _unknown; _|] -> tst dest src | _ -> [] - let lift_mem_single ?(sign = false) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = + let lift_mem_single ?(sign = false) ?(shift_val = 2) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = match src2 with - | Some src2 -> Mem.lift_mem_single ~sign dest src1 ~src2 op size |> move - | None -> Mem.lift_mem_single ~sign dest src1 op size |> move + | Some src2 -> Mem.lift_mem_single ~sign ~shift_val dest src1 ~src2 op size |> move + | None -> Mem.lift_mem_single ~sign ~shift_val dest src1 op size |> move let lift_mem insn ops addr = let open Defs in match insn, Array.to_list ops with - | `tLDRi, [dest; src; imm] -> + | `tLDRi, [dest; src; imm; unknown; _] -> lift_mem_single dest src ~src2:imm Ld W - | `tLDRr, [dest; src1; src2] -> + | `tLDRr, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 Ld W - | `tLDRpci, [dest; imm] -> - lift_mem_single dest `PC ~src2:imm Ld W - | `tLDRspi, [dest; imm] -> - lift_mem_single dest `SP ~src2:imm Ld W - | `tLDRBi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm Ld B - | `tLDRBr, [dest; src1; src2] -> + | `tLDRpci, [dest; imm; unknown; _] -> + lift_mem_single ~shift_val:0 dest (`Reg `PC) ~src2:imm Ld W + | `tLDRspi, [dest; (`Reg `SP); imm; unknown; _] -> + lift_mem_single dest (`Reg `SP) ~src2:imm Ld W + | `tLDRBi, [dest; src; imm; unknown; _] -> + lift_mem_single ~shift_val:0 dest src ~src2:imm Ld B + | `tLDRBr, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 Ld B - | `tLDRHi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm Ld H - | `tLDRHr, [dest; src1; src2] -> + | `tLDRHi, [dest; src; imm; unknown; _] -> + lift_mem_single ~shift_val:1 dest src ~src2:imm Ld H + | `tLDRHr, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 Ld H - | `tLDRSB, [dest; src1; src2] -> + | `tLDRSB, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 Ld B ~sign:true - | `tLDRSH, [dest; src1; src2] -> + | `tLDRSH, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 Ld H ~sign:true - | `tSTRi, [dest; src; imm] -> + | `tSTRi, [dest; src; imm; unknown; _] -> lift_mem_single dest src ~src2:imm St W - | `tSTRr, [dest; src1; src2] -> + | `tSTRr, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 St W - | `tSTRspi, [dest; imm] -> - lift_mem_single dest `SP ~src2:imm St W - | `tSTRBi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm St B - | `tSTRBr, [dest; src1; src2] -> + | `tSTRspi, [dest; (`Reg `SP); imm; unknown; _] -> + lift_mem_single dest (`Reg `SP) ~src2:imm St W + | `tSTRBi, [dest; src; imm; unknown; _] -> + lift_mem_single ~shift_val:0 dest src ~src2:imm St B + | `tSTRBr, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 St B - | `tSTRHi, [dest; src; imm] -> - lift_mem_single dest src ~src2:imm St H - | `tSTRHr, [dest; src1; src2] -> + | `tSTRHi, [dest; src; imm; unknown; _] -> + lift_mem_single ~shift_val:1 dest src ~src2:imm St H + | `tSTRHr, [dest; src1; src2; unknown; _] -> lift_mem_single dest src1 ~src2 St H - | `tSTMIA, dest :: src_list -> + | `tSTMIA, dest :: _dest :: _unknown :: _nil_reg :: src_list (* looks like they should be different, but actually are the same in Thumb mode *) + | `tSTMIA_UPD, dest :: _dest :: _unknown :: _nil_reg :: src_list -> Mem.store_multiple dest src_list |> move - | `tLDMIA, dest :: src_list -> + | `tLDMIA, dest :: _unknown :: _nil_reg :: src_list (* same as stmia *) + | `tLDMIA_UPD, dest :: _unknown :: _nil_reg :: src_list -> Mem.load_multiple dest src_list |> move - | `tPUSH, src_list -> + | `tPUSH, _unknown :: _nil_reg :: src_list -> Mem.push_multiple src_list |> move - | `tPOP, src_list -> + | `tPOP, _unknown :: _nil_reg :: src_list -> let has_pc = List.exists src_list (fun s -> match s with |`Reg `PC -> true @@ -137,10 +139,10 @@ module Thumb(Core : Theory.Core) = struct let lift_bits insn ops = let open Bits in match insn, ops with - | `tSXTB, [|dest; src|] -> sxtb dest src - | `tSXTH, [|dest; src|] -> sxth dest src - | `tUXTB, [|dest; src|] -> uxtb dest src - | `tUXTH, [|dest; src|] -> uxth dest src + | `tSXTB, [|dest; src; _unknown; _|] -> sxtb dest src + | `tSXTH, [|dest; src; _unknown; _|] -> sxth dest src + | `tUXTB, [|dest; src; _unknown; _|] -> uxtb dest src + | `tUXTH, [|dest; src; _unknown; _|] -> uxth dest src | _ -> [] (* these are not entirely complete *) @@ -149,16 +151,17 @@ module Thumb(Core : Theory.Core) = struct let open Branch in let addr = Core.int Env.value addr in match insn, ops with - | `tBcc, [|cond; target|] -> tbcc cond target addr - | `tB, [|target|] -> tb target addr - | `tBL, [|target|] -> tbl target - | `tBLXi, [|target|] -> tblxi target - | `tBLXr, [|target|] -> tblxr target - | `tBX, [|target|] -> tbx target + | `tBcc, [|target; cond; _cpsr|] -> tbcc cond target addr + | `tB, [|target; _unknown; _|] -> tb target addr + | `tBL, [|_unknown; _nil_reg; target; _cpsr|] -> tbl target + | `tBLXi, [|_unknown; _nil_reg; target; _cpsr|] -> tblxi target + | `tBLXr, [|_unknown; _nil_reg; target|] -> tblxr target + | `tBX, [|target; _unknown; _|] -> tbx target | _ -> (skip, pass) let lift_with (addr : Bitvec.t) (insn : Thumb_defs.insn) - (ops : Thumb_defs.op array) = match insn with + (ops : Thumb_defs.op array) = + match insn with | #move_insn -> lift_move insn ops |> DSL.expand |> move | #mem_insn -> lift_mem insn ops addr | #bits_insn -> lift_bits insn ops |> DSL.expand |> move @@ -174,7 +177,7 @@ let run_lifter _label addr insn _mem (lifter : Bitvec.t -> Defs.insn -> Defs.op array -> unit Theory.eff) = match Insns.of_basic insn with | None -> raise (Defs.Lift_Error "unknown instruction") - | Some arm_insn -> + | Some arm_insn -> Disasm_expert.Basic.sexp_of_full_insn insn |> Sexp.to_string |> Stdio.print_endline; match Insns.arm_ops (Disasm_expert.Basic.Insn.ops insn) with | Error err -> raise (Defs.Lift_Error (Error.to_string_hum err)) | Ok ops -> lifter addr arm_insn ops diff --git a/plugins/arm_thumb/thumb_branch.ml b/plugins/arm_thumb/thumb_branch.ml index 2f761eeb1..8a3265a4f 100644 --- a/plugins/arm_thumb/thumb_branch.ml +++ b/plugins/arm_thumb/thumb_branch.ml @@ -42,7 +42,7 @@ module Branch(Core : Theory.Core) = struct | `GT -> and_ (inv z) (eq_ n v) | `LE -> or_ z (eq_ n v |> inv) | `AL -> b1 in - let jump_address = DSL.(addr + !$target << !!1) in + let jump_address = DSL.(addr + !$target) in let eff_hold = (jmp jump_address, set Env.pc jump_address) in if always_true then eff_hold else ( @@ -53,16 +53,16 @@ module Branch(Core : Theory.Core) = struct let tb target addr = (DSL.( - jmp (!$target + addr << !!1) + jmp (!$target + addr) ), DSL.( - Env.pc := (!$target + addr << !!1) + Env.pc := (!$target + addr) )) let tbl target = (DSL.( jmp !$target ), DSL.[ - Env.lr := (var Env.pc) - !!2 lor !!1; + Env.lr := ((var Env.pc) - !!2) lor !!1; Env.pc := !$target ] |> DSL.expand) @@ -71,24 +71,24 @@ module Branch(Core : Theory.Core) = struct (DSL.( jmp (!$target land !!0xfffffffc) ), DSL.[ - Env.lr := (var Env.pc) - !!2 lor !!1; + Env.lr := ((var Env.pc) - !!2) lor !!1; Env.pc := (!$target land !!0xfffffffc) ] |> DSL.expand) let tblxr target = (DSL.( - jmp (!$target land !!0xfffffffe) + jmp (!$+target land !!0xfffffffe) ), DSL.[ - Env.lr := (var Env.pc) - !!2 lor !!1; - Env.pc := (!$target land !!0xfffffffe) + Env.lr := ((var Env.pc) - !!2) lor !!1; + Env.pc := (!$+target land !!0xfffffffe) ] |> DSL.expand) let tbx target = (DSL.( (* reference here is PC = Rm[31:1] << 1 *) - jmp (extract Env.value !!31 !!1 !$target << !!1) + jmp (extract Env.value !!31 !!1 !$+target << !!1) ), DSL.( - Env.pc := (extract Env.value !!31 !!1 !$target << !!1) + Env.pc := (extract Env.value !!31 !!1 !$+target << !!1) )) end \ No newline at end of file diff --git a/plugins/arm_thumb/thumb_defs.ml b/plugins/arm_thumb/thumb_defs.ml index a8f5c508a..9838527f0 100644 --- a/plugins/arm_thumb/thumb_defs.ml +++ b/plugins/arm_thumb/thumb_defs.ml @@ -126,7 +126,9 @@ type bits_insn = [ (** Rd [reglist] *) type mem_multi_insn = [ | `tSTMIA + | `tSTMIA_UPD | `tLDMIA + | `tLDMIA_UPD | `tPOP | `tPUSH ] [@@deriving bin_io, compare, sexp, enumerate] diff --git a/plugins/arm_thumb/thumb_insn.ml b/plugins/arm_thumb/thumb_insn.ml index e9e9ec642..da2b8fb8f 100644 --- a/plugins/arm_thumb/thumb_insn.ml +++ b/plugins/arm_thumb/thumb_insn.ml @@ -9,7 +9,7 @@ let sexpable_of_string t_of_sexp name = try Some (t_of_sexp @@ Sexp.of_string name) with Sexp.Of_sexp_error _ -> None -let of_name name = +let of_name name = print_endline name; sexpable_of_string t_of_sexp name let of_basic insn = of_name (Disasm_expert.Basic.Insn.name insn) @@ -22,8 +22,9 @@ let create_op : op -> Thumb_defs.op option = let open Option.Monad_infix in function | Op.Fmm fmm -> None (* this should be later extended *) - | Op.Reg reg -> create_reg reg >>| fun reg -> `Reg reg - | Op.Imm imm -> + | Op.Reg reg -> print_endline (sexp_of_reg reg |> Sexp.to_string); + create_reg reg >>| fun reg -> `Reg reg + | Op.Imm imm -> print_endline (Imm.to_string imm); Imm.to_word ~width:32 imm >>| fun imm -> `Imm imm let arm_ops_exn ops () = diff --git a/plugins/arm_thumb/thumb_mem.ml b/plugins/arm_thumb/thumb_mem.ml index 9c70e5551..c40c0ce9f 100644 --- a/plugins/arm_thumb/thumb_mem.ml +++ b/plugins/arm_thumb/thumb_mem.ml @@ -30,15 +30,22 @@ module Mem(Core : Theory.Core) = struct let load_multiple dest src_list = match dest with - | `Reg r -> let r = reg r in List.fold src_list ~init:pass - ~f:(fun eff src -> match src with - | `Reg s -> let src = reg s in seq eff - (seq - (loadw Env.value b0 (var Env.memory) (var r) |> set src) - (set r (add (var r) (bitv_of 4))) - ) - | _ -> raise (Lift_Error "`src` must be a register") - ) + | `Reg r -> + if List.length src_list = 0 then pass + else let first_eq = [%compare.equal: Defs.op] (List.nth_exn src_list 0) dest in + let src_list = if first_eq + then List.sub src_list ~pos:1 ~len:(List.length src_list - 1) + else src_list in + let r = reg r in + seq (List.fold src_list ~init:(set Env.tmp (var r)) + ~f:(fun eff src -> match src with + | `Reg s -> let src = reg s in seq eff + (seq + (loadw Env.value b0 (var Env.memory) (var Env.tmp) |> set src) + (set Env.tmp (add (var Env.tmp) (bitv_of 4))) + ) + | _ -> raise (Lift_Error "`src` must be a register") + )) (set r (var Env.tmp)) | _ -> raise (Lift_Error "`dest` must be a register") (* the `R` bit is automatically resolved *) let push_multiple src_list = @@ -59,6 +66,14 @@ module Mem(Core : Theory.Core) = struct let initial = set Env.tmp (var Env.sp) in seq (List.fold src_list ~init:initial ~f:(fun eff src -> match src with + | `Reg `PC -> let src = reg_wide `PC in seq eff + (seq + (logand + (loadw Env.value b0 (var Env.memory) (var Env.tmp)) + (bitv_of 0xfffffffe) + |> set src) + (set Env.tmp (add (var Env.tmp) (bitv_of 4))) + ) | `Reg s -> let src = reg s in seq eff (seq (loadw Env.value b0 (var Env.memory) (var Env.tmp) |> set src) @@ -67,7 +82,7 @@ module Mem(Core : Theory.Core) = struct | _ -> raise (Lift_Error "`src` must be a register") )) (set Env.sp (var Env.tmp)) - let lift_mem_single ?(sign = false) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = + let lift_mem_single ?(sign = false) ?(shift_val = 2) dest src1 ?src2 (op : Defs.operation) (size : Defs.size) = let open Defs in let dest = match dest with | `Reg r -> reg r diff --git a/plugins/arm_thumb/thumb_mov.ml b/plugins/arm_thumb/thumb_mov.ml index e0f6eeacc..1affe4861 100644 --- a/plugins/arm_thumb/thumb_mov.ml +++ b/plugins/arm_thumb/thumb_mov.ml @@ -54,8 +54,8 @@ module Mov(Core : Theory.Core) = struct let subi3 dest src immsrc = DSL.[ - !$$dest := !$src + !$immsrc; - Flags.set_add !$src !$immsrc !$$dest + !$$dest := !$src - !$immsrc; + Flags.set_sub !$src !$immsrc !$$dest ] (* a temp value is introduced here *) @@ -81,7 +81,7 @@ module Mov(Core : Theory.Core) = struct let subrr d s1 s2 = DSL.[ - !$$d := !$s1 + !$s2; + !$$d := !$s1 - !$s2; Flags.set_sub !$s1 !$s2 !$$d ] @@ -111,16 +111,17 @@ module Mov(Core : Theory.Core) = struct Env.sp := (var Env.sp) - !$immsrc << !!2 ] - let adc d s1 s2 = + let adc d s = DSL.[ - !$$d := !$s1 + !$s2 + bool_as_bitv (var Env.cf); - Flags.set_adc !$s1 !$s2 !$$d + Env.tmp := !$d; + !$$d := !$d + !$s + bool_as_bitv (var Env.cf); + Flags.set_adc (var Env.tmp) !$s !$$d ] let sbc d s = DSL.[ Env.tmp := !$d; - !$$d := !$s + !$d + bool_as_bitv (var Env.cf); + !$$d := !$s - !$d - bool_as_bitv (var Env.cf |> inv); Flags.set_sbc (var Env.tmp) !$s !$$s ]