implements AVR ABI and refines AVR targets

Author: ivg

lib/bap_avr/bap_avr_target.ml

@@ -8,42 +8,87 @@ 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 ?(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
 
 

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

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"

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"]