implements AVR ABI and refines AVR targets

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