Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ghidra-based AVR Lifter #1228

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
124 changes: 124 additions & 0 deletions lib/bap_avr/bap_avr_target.ml
Original file line number Diff line number Diff line change
@@ -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 ()
21 changes: 21 additions & 0 deletions lib/bap_avr/bap_avr_target.mli
Original file line number Diff line number Diff line change
@@ -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
20 changes: 20 additions & 0 deletions oasis/avr
Original file line number Diff line number Diff line change
@@ -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"
2 changes: 2 additions & 0 deletions plugins/avr/.merlin
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
B ../../lib/bap_avr
REC
47 changes: 47 additions & 0 deletions plugins/avr/avr_main.ml
Original file line number Diff line number Diff line change
@@ -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"]