diff --git a/lib/bap_avr/bap_avr_target.ml b/lib/bap_avr/bap_avr_target.ml index 4e2009654b..21103a2afe 100644 --- a/lib/bap_avr/bap_avr_target.ml +++ b/lib/bap_avr/bap_avr_target.ml @@ -1,5 +1,7 @@ open Core_kernel open Bap_core_theory +module Dis = Bap.Std.Disasm_expert.Basic + let package = "bap" @@ -36,12 +38,42 @@ let parent = Theory.Target.declare ~package "avr" ~byte:8 ~endianness:Theory.Endianness.le - let atmega328 = Theory.Target.declare ~package "ATmega328" ~parent ~data ~code ~vars:(gpr @< [sp] @< flags @< [data] @< [code]) +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" -> atmega328 + | _ -> Theory.Target.unknown + -let llvm_avr16 = Theory.Language.declare ~package "llvm-avr16" +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 index b255d24cb6..4ea548a8dd 100644 --- a/lib/bap_avr/bap_avr_target.mli +++ b/lib/bap_avr/bap_avr_target.mli @@ -1,18 +1,5 @@ open Bap_core_theory val parent : Theory.target -val atmega328 : Theory.target -val llvm_avr16 : Theory.language -type r16 and r8 - -type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort - -val r16 : r16 bitv -val r8 : r8 bitv - -val code : (r16, r16) Theory.Mem.t Theory.var -val data : (r16, r8) Theory.Mem.t Theory.var -val gpr : r8 Theory.Bitv.t Theory.var list -val sp : r16 Theory.Bitv.t Theory.var -val flags : Theory.Bool.t Theory.var list +val load : unit -> unit diff --git a/oasis/avr b/oasis/avr index 6a4542bda0..9144e3e84a 100644 --- a/oasis/avr +++ b/oasis/avr @@ -6,7 +6,7 @@ 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 + BuildDepends: core_kernel, bap-knowledge, bap-core-theory, bap, ogre FindlibName: bap-avr Modules: Bap_avr_target @@ -14,9 +14,7 @@ Library avr_plugin XMETADescription: provide Avr lifter Path: plugins/avr Build$: flag(everything) || flag(avr) - BuildDepends: core_kernel, ppx_jane, ogre, - bap-core-theory, bap-knowledge, bap-main, - bap, bap-avr, bitvec + BuildDepends: bap-main, bap-avr FindlibName: bap-plugin-avr - InternalModules: Avr_main, Avr_lifter + InternalModules: Avr_main XMETAExtraLines: tags="avr, lifter, atmega" diff --git a/plugins/avr/avr_lifter.ml b/plugins/avr/avr_lifter.ml deleted file mode 100644 index 740baf3837..0000000000 --- a/plugins/avr/avr_lifter.ml +++ /dev/null @@ -1,156 +0,0 @@ -open Core_kernel -open Bap_core_theory -open Bap.Std - -open KB.Syntax -include Bap_main.Loggers() - -module Target = Bap_avr_target -module MC = Disasm_expert.Basic - -type r1 -type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort - -let r1 : r1 bitv = Theory.Bitv.define 1 - -let make_regs regs = - let regs = - List.mapi regs ~f:(fun i r -> (i,r)) |> - Map.of_alist_exn (module Int) in - Map.find_exn regs - -let gpr = make_regs Target.gpr -let regnum s = Scanf.sscanf s "R%d" ident - -let require_gpr insn pos f = - match (MC.Insn.ops insn).(pos) with - | Op.Reg r -> f (gpr (regnum (Reg.name r))) - | _ -> KB.return Insn.empty - -let require_imm insn pos f = - match (MC.Insn.ops insn).(pos) with - | Op.Imm x -> f (Option.value_exn (Imm.to_int x)) - | _ -> KB.return Insn.empty - -let hf = Theory.Var.define r1 "HF" -let cf = Theory.Var.define r1 "CF" -let nf = Theory.Var.define r1 "NF" -let vf = Theory.Var.define r1 "VF" -let sf = Theory.Var.define r1 "SF" -let zf = Theory.Var.define r1 "ZF" - -module M8 = Bitvec.M8 - -module Avr(CT : Theory.Core) = struct - open Target - let rec seq = function - | [] -> CT.perform Theory.Effect.Sort.bot - | [x] -> x - | x :: xs -> CT.seq x @@ seq xs - - let const x = CT.int r8 (M8.int x) - - let bit0 = CT.int r1 (Bitvec.M1.bool false) - let bit1 = CT.int r1 (Bitvec.M1.bool true) - let flag x = CT.ite x bit1 bit0 - - let nth x n = - CT.(extract r1 (const n) (const n) x) - - let data xs = - KB.Object.create Theory.Program.cls >>= fun lbl -> - CT.blk lbl (seq xs) (seq []) - - let (&&) = CT.logand - let (||) = CT.logor - let not = CT.not - - let bit reg n body = - nth CT.(var reg) n >>= fun expr -> - Theory.Var.scoped r1 @@ fun v -> - CT.let_ v !!expr (body (CT.var v)) - - let halfcarry ~r ~rd ~rr = - bit r 3 @@ fun r3 -> - bit rd 3 @@ fun rd3 -> - bit rr 3 @@ fun rr3 -> - rd3 && rr3 || rr3 && not r3 || not r3 && rd3 - - let fullcarry ~r ~rd ~rr = - bit r 7 @@ fun r7 -> - bit rd 7 @@ fun rd7 -> - bit rr 7 @@ fun rr7 -> - rd7 && rr7 || rr7 && not r7 || r7 && not rd7 - - let overflow ~r ~rd ~rr = - bit r 7 @@ fun r7 -> - bit rd 7 @@ fun rd7 -> - bit rr 7 @@ fun rr7 -> - rd7 && rr7 && not r7 || not rd7 && not rr7 && r7 - - - let with_result rd f = - Theory.Var.fresh (Theory.Var.sort rd) >>= fun v -> - f v >>= fun effs -> - data (effs @ CT.[set rd (var v)]) - - let (:=) = CT.set - let (+) = CT.add - - - let adc insn = - require_gpr insn 1 @@ fun rd -> - require_gpr insn 2 @@ fun rr -> - with_result rd @@ fun r -> - KB.return @@ - CT.[ - r := var rd + var rr + unsigned r8 (var cf); - hf := halfcarry ~r ~rd ~rr; - nf := nth (var r) 7; - vf := overflow ~r ~rd ~rr; - sf := var nf || var vf; - zf := flag (is_zero (var r)); - cf := fullcarry ~r ~rd ~rr; - ] - - - let add insn = - require_gpr insn 1 @@ fun rd -> - require_gpr insn 2 @@ fun rr -> - with_result rd @@ fun r -> - KB.return @@ - CT.[ - r := var rd + var rr; - hf := halfcarry ~r ~rd ~rr; - nf := nth (var r) 7; - vf := overflow ~r ~rd ~rr; - sf := var nf || var vf; - zf := flag (is_zero (var r)); - cf := fullcarry ~r ~rd ~rr; - ] - - let ldi insn = - require_gpr insn 0 @@ fun rd -> - require_imm insn 1 @@ fun k -> - data [ - rd := const k - ] -end - -let lifter label : unit Theory.eff = - KB.collect MC.Insn.slot label >>= function - | None -> KB.return Insn.empty - | Some insn -> - Theory.instance () >>= Theory.require >>= fun (module Core) -> - let module Avr = Avr(Core) in - let open Avr in - insn |> match MC.Insn.name insn with - | "ADCRdRr" -> adc - | "ADDRdRr" -> add - | "LDIRdK" -> ldi - | code -> - info "unsupported opcode: %s" code; - fun _ -> KB.return Insn.empty - -let load () = - KB.promise Theory.Semantics.slot lifter diff --git a/plugins/avr/avr_lifter.mli b/plugins/avr/avr_lifter.mli deleted file mode 100644 index a58d3a6dae..0000000000 --- a/plugins/avr/avr_lifter.mli +++ /dev/null @@ -1 +0,0 @@ -val load : unit -> unit diff --git a/plugins/avr/avr_main.ml b/plugins/avr/avr_main.ml index c6397d02ab..16ae77a70e 100644 --- a/plugins/avr/avr_main.ml +++ b/plugins/avr/avr_main.ml @@ -1,53 +1,12 @@ open Bap_main -open Bap.Std -open Bap_core_theory -open KB.Syntax -module CT = Theory - -include Bap_main.Loggers() - -module Target = Bap_avr_target -module Dis = Disasm_expert.Basic - -let provide_decoding () = - KB.promise CT.Label.encoding @@ fun label -> - CT.Label.target label >>| fun t -> - if CT.Target.belongs Target.parent t - then Target.llvm_avr16 - else CT.Language.unknown - -let enable_llvm () = - Dis.register Target.llvm_avr16 @@ fun _target -> - Dis.create ~backend:"llvm" "avr" - -let enable_loader () = - let request_arch doc = - let open Ogre.Syntax in - match Ogre.eval (Ogre.request Image.Scheme.arch) doc with - | Error _ -> assert false (* nothing could go wrong here! *) - | Ok arch -> arch in - KB.promise CT.Unit.target @@ fun unit -> - KB.collect Image.Spec.slot unit >>| request_arch >>| function - | Some "avr" -> Target.atmega328 - | _ -> CT.Target.unknown - let main _ctxt = - enable_llvm (); - enable_loader (); - provide_decoding (); - Avr_lifter.load (); + Bap_avr_target.load (); Ok () -(* semantic tags that describe what our plugin is providing, - setting them is important not only for introspection but - for the proper function of the cache subsystem. -*) -let provides = [ - "avr"; - "lifter"; -] -(* finally, let's register our extension and call the main function *) let () = Bap_main.Extension.declare main - ~provides + ~provides:[ + "avr"; + "lifter"; + ]