diff --git a/lib/bap_avr/bap_avr_target.ml b/lib/bap_avr/bap_avr_target.ml new file mode 100644 index 000000000..c6726982e --- /dev/null +++ b/lib/bap_avr/bap_avr_target.ml @@ -0,0 +1,124 @@ +open Core_kernel +open Bap_core_theory +module Dis = Bap.Std.Disasm_expert.Basic + + +let package = "bap" + +type r16 and r8 + +type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort +type reg = r8 Theory.Bitv.t Theory.var + + +let r16 : r16 bitv = Theory.Bitv.define 16 +let r8 : r8 bitv = Theory.Bitv.define 8 +let bool = Theory.Bool.t + +let reg t n = Theory.Var.define t n + +let array ?(rev=false) ?(start=0) ?(index=string_of_int) t pref size = + let stop = if rev then start-size else start+size in + let stride = if rev then -1 else 1 in + List.range ~stride start stop |> + List.map ~f:(fun i -> reg t (pref ^ index i)) + +let untyped = List.map ~f:Theory.Var.forget +let (@<) xs ys = untyped xs @ untyped ys + +let regs t = List.map ~f:(reg t) +let nums = array r8 "R" 24 +let wxyz = regs r8 [ + "Wlo"; "Whi"; + "Xlo"; "Xhi"; + "Ylo"; "Yhi"; + "Zlo"; "Zhi"; + ] +let gpr = nums @< wxyz +let sp = reg r16 "SP" +let flags = regs bool [ + "CF"; "ZF"; "NF"; "VF"; "SF"; "HF"; "TF"; "IF" + ] + + +let datas = Theory.Mem.define r16 r8 +let codes = Theory.Mem.define r16 r16 + +let data = reg datas "data" +let code = reg codes "code" + +let parent = Theory.Target.declare ~package "avr8" + ~bits:8 + ~byte:8 + ~endianness:Theory.Endianness.le + + +let tiny = Theory.Target.declare ~package "avr8-tiny" + ~parent + ~data + ~code + ~vars:(gpr @< [sp] @< flags @< [data] @< [code]) + +let mega = Theory.Target.declare ~package "avr8-mega" + ~parent:tiny + +let xmega = Theory.Target.declare ~package "avr8-xmega" + ~parent:mega + +module Gcc = struct + let abi = Theory.Abi.declare ~package "avr-gcc" + let wreg = regs r8 ["Whi"; "Wlo"] + let args = wreg @ array ~rev:true ~start:23 r8 "R" 16 + let rets = wreg @ array ~rev:true ~start:23 r8 "R" 6 + let regs = Theory.Role.Register.[ + [general; integer], gpr; + [function_argument], untyped args; + [function_return], untyped rets; + [stack_pointer], untyped [sp]; + [caller_saved], rets @< regs r8 ["R0"; "Xlo"; "Xhi"; "Zlo"; "Zhi"]; + [callee_saved], array ~start:1 r8 "R" 17 @< regs r8 ["Ylo"; "Yhi"]; + ] + + let target parent name = + Theory.Target.declare ~package name ~regs ~parent ~abi + + let tiny = target tiny "avr8-tiny-gcc" + let mega = target mega "avr8-mega-gcc" + let xmega = target xmega "avr8-xmega-gcc" +end + + + +let pcode = + Theory.Language.declare ~package:"bap" "pcode-avr" + +let provide_decoding () = + let open KB.Syntax in + KB.promise Theory.Label.encoding @@ fun label -> + Theory.Label.target label >>| fun t -> + if Theory.Target.belongs parent t + then pcode + else Theory.Language.unknown + +let enable_ghidra () = + Dis.register pcode @@ fun _target -> + Dis.create ~backend:"ghidra" "avr8:LE:16:atmega256" + +let enable_loader () = + let open Bap.Std in + let open KB.Syntax in + let request_arch doc = + let open Ogre.Syntax in + match Ogre.eval (Ogre.request Image.Scheme.arch) doc with + | Error _ -> None + | Ok arch -> arch in + KB.promise Theory.Unit.target @@ fun unit -> + KB.collect Image.Spec.slot unit >>| request_arch >>| function + | Some "avr" -> Gcc.mega + | _ -> Theory.Target.unknown + + +let load () = + enable_ghidra (); + enable_loader (); + provide_decoding () diff --git a/lib/bap_avr/bap_avr_target.mli b/lib/bap_avr/bap_avr_target.mli new file mode 100644 index 000000000..aaa5bdc0e --- /dev/null +++ b/lib/bap_avr/bap_avr_target.mli @@ -0,0 +1,21 @@ +open Bap_core_theory + + +val load : unit -> unit + +type r8 +type reg = r8 Theory.Bitv.t Theory.var + +val parent : Theory.target + +val tiny : Theory.target +val mega : Theory.target +val xmega : Theory.target + +module Gcc : sig + val args : reg list + val rets : reg list + val tiny : Theory.target + val mega : Theory.target + val xmega : Theory.target +end diff --git a/oasis/avr b/oasis/avr new file mode 100644 index 000000000..b8c5e3b0d --- /dev/null +++ b/oasis/avr @@ -0,0 +1,20 @@ +Flag avr + Description: Build Avr lifter + Default: false + +Library "bap-avr" + Build$: flag(everything) || flag(avr) + XMETADescription: common definitions for Avr targets + Path: lib/bap_avr + BuildDepends: core_kernel, bap-knowledge, bap-core-theory, bap, ogre + FindlibName: bap-avr + Modules: Bap_avr_target + +Library avr_plugin + XMETADescription: provide Avr lifter + Path: plugins/avr + Build$: flag(everything) || flag(avr) + BuildDepends: bap-main, bap-avr, bap, bap-core-theory + FindlibName: bap-plugin-avr + InternalModules: Avr_main + XMETAExtraLines: tags="avr, lifter, atmega" diff --git a/plugins/avr/.merlin b/plugins/avr/.merlin new file mode 100644 index 000000000..ed4f494f0 --- /dev/null +++ b/plugins/avr/.merlin @@ -0,0 +1,2 @@ +B ../../lib/bap_avr +REC \ No newline at end of file diff --git a/plugins/avr/avr_main.ml b/plugins/avr/avr_main.ml new file mode 100644 index 000000000..b6c6062ee --- /dev/null +++ b/plugins/avr/avr_main.ml @@ -0,0 +1,47 @@ +open Bap_main +open Bap_core_theory + +module AT = Bap_avr_target + +module Abi = struct + open Bap_c.Std + + module Arg = C.Abi.Arg + open Arg.Let + open Arg.Syntax + + let model = new C.Size.base `LP32 + + let define t = + C.Abi.define t model @@ fun _ {C.Type.Proto.return=r; args} -> + let* iregs = Arg.Arena.create AT.Gcc.args in + let* irets = Arg.Arena.create AT.Gcc.rets in + let pass_via regs (_,t) = + let open Arg in + choice [ + sequence [ + align_even regs; + registers regs t; + ]; + sequence [ + deplet regs; + memory t; + ] + ] in + let args = Arg.List.iter args ~f:(pass_via iregs) in + let return = match r with + | `Void -> None + | r -> Some (pass_via irets ("",r)) in + Arg.define ?return args + + let setup () = + List.iter define AT.Gcc.[tiny; mega; xmega] +end + +let main _ctxt = + AT.load (); + Abi.setup (); + Ok () + +let () = Bap_main.Extension.declare main + ~provides:["avr"; "lifter"; "disassembler"]