From aa81f60e4dbf31009af422cc562625d747495355 Mon Sep 17 00:00:00 2001 From: ivg Date: Thu, 8 Jul 2021 12:43:20 -0400 Subject: [PATCH] implements AVR ABI and refines AVR targets --- lib/bap_avr/bap_avr_target.ml | 59 ++++++++++++++++++++++++++++++---- lib/bap_avr/bap_avr_target.mli | 18 ++++++++++- oasis/avr | 2 +- plugins/avr/avr_main.ml | 47 +++++++++++++++++++++++---- 4 files changed, 111 insertions(+), 15 deletions(-) diff --git a/lib/bap_avr/bap_avr_target.ml b/lib/bap_avr/bap_avr_target.ml index 21103a2afe..c6726982e1 100644 --- a/lib/bap_avr/bap_avr_target.ml +++ b/lib/bap_avr/bap_avr_target.ml @@ -8,6 +8,8 @@ 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 @@ -15,35 +17,78 @@ let bool = Theory.Bool.t let reg t n = Theory.Var.define t n -let array ?(index=string_of_int) t pref size = - List.init size ~f:(fun i -> reg t (pref ^ index i)) +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 gpr = array r8 "R" 32 +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 = List.map ~f:(reg bool) [ +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 "avr" +let parent = Theory.Target.declare ~package "avr8" ~bits:8 ~byte:8 ~endianness:Theory.Endianness.le -let atmega328 = Theory.Target.declare ~package "ATmega328" + +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" @@ -69,7 +114,7 @@ let enable_loader () = | Ok arch -> arch in KB.promise Theory.Unit.target @@ fun unit -> KB.collect Image.Spec.slot unit >>| request_arch >>| function - | Some "avr" -> atmega328 + | Some "avr" -> Gcc.mega | _ -> Theory.Target.unknown diff --git a/lib/bap_avr/bap_avr_target.mli b/lib/bap_avr/bap_avr_target.mli index 4ea548a8dd..aaa5bdc0ea 100644 --- a/lib/bap_avr/bap_avr_target.mli +++ b/lib/bap_avr/bap_avr_target.mli @@ -1,5 +1,21 @@ open Bap_core_theory -val parent : Theory.target 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 index 9144e3e84a..b8c5e3b0db 100644 --- a/oasis/avr +++ b/oasis/avr @@ -14,7 +14,7 @@ Library avr_plugin XMETADescription: provide Avr lifter Path: plugins/avr Build$: flag(everything) || flag(avr) - BuildDepends: bap-main, bap-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/avr_main.ml b/plugins/avr/avr_main.ml index 16ae77a70e..b6c6062eea 100644 --- a/plugins/avr/avr_main.ml +++ b/plugins/avr/avr_main.ml @@ -1,12 +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 = - Bap_avr_target.load (); + AT.load (); + Abi.setup (); Ok () - let () = Bap_main.Extension.declare main - ~provides:[ - "avr"; - "lifter"; - ] + ~provides:["avr"; "lifter"; "disassembler"]