Add MSP430 lifter.

bap-msp430.opam

@@ -0,0 +1,42 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "BAP MSP430 support package"
+maintainer: ["Ivan Gotovchits <[email protected]>"]
+authors: ["The BAP Team"]
+license: "MIT"
+tags: ["bap" "bap-plugin" "msp430"]
+homepage: "https://github.com/BinaryAnalysisPlatform/bap"
+bug-reports: "https://github.com/BinaryAnalysisPlatform/bap/issues"
+depends: [
+  "dune" {>= "3.1"}
+  "bap-abi" {= version}
+  "bap-api" {= version}
+  "bap-common" {= version}
+  "bap-core-theory" {= version}
+  "bap-c" {= version}
+  "bap-knowledge" {= version}
+  "bap-std" {= version}
+  "core_kernel" {>= "v0.14" & < "v0.16"}
+  "monads" {= version}
+  "ogre" {= version}
+  "ppx_bap" {= version}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/BinaryAnalysisPlatform/bap.git"

dune-project

@@ -1211,6 +1211,23 @@ between the sets.")
   (ogre (= :version))
   (ppx_bap (= :version))))
 
+(package
+ (name bap-msp430)
+ (synopsis "BAP MSP430 support package")
+ (tags (bap bap-plugin msp430))
+ (depends
+  (bap-abi (= :version))
+  (bap-api (= :version))
+  (bap-common (= :version))
+  (bap-core-theory (= :version))
+  (bap-c (= :version))
+  (bap-knowledge (= :version))
+  (bap-std (= :version))
+  (core_kernel (and (>= v0.14) (< v0.16)))
+  (monads (= :version))
+  (ogre (= :version))
+  (ppx_bap (= :version))))  
+
 (package
  (name bap-run)
  (synopsis "BAP Primus Framework frontend")

lib/bap_msp430/bap_msp430_target.ml

@@ -0,0 +1,77 @@
+open Core_kernel[@@warning "-D"]
+open Bap_core_theory
+
+let package = "bap"
+
+type r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+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 untyped = List.map ~f:Theory.Var.forget
+let (@<) xs ys = untyped xs @ untyped ys
+
+
+let regs = [
+   "r0";  "r1";  "r2";  "r3";  "r4";  "r5"; "r6"; "r7"; "r8"; "r9"; 
+  "r10"; "r11"; "r12"; "r13"; "r14"; "r15"
+]
+
+let cf = reg bool "C"
+let zf = reg bool "Z"
+let nf = reg bool "N"
+let vf = reg bool "V"
+
+let status_reg = [nf; zf; cf; vf]
+
+let array t = List.map regs ~f:(reg t)
+let vars p t = List.init 16 ~f:(fun i -> reg t (sprintf "%c%d" p  i))
+
+(*
+let parent = Theory.Target.declare ~package "msp430"
+    ~endianness:Theory.Endianness.le *)
+
+let select xs ~mask =
+  let mask = Set.of_list (module Int) mask in
+  List.filteri xs ~f:(fun i _ -> Set.mem mask i)
+
+let msp430 =
+  let mems = Theory.Mem.define r16 r8 in
+  let mem = reg mems "mem" in
+  (*let pc = reg r16 "PC" in *PC is at r0 *)
+  let ints = untyped@@vars 'R' r16 in
+  let vars = ints (*@< flts @< [pc]*) @< status_reg @< [mem] in
+  let bits = Theory.Bitv.size r16 in
+  let r i = select ints ~mask:i in
+  Theory.Target.declare ~package "msp430" (*~parent*)
+    ~endianness:Theory.Endianness.le
+    ~bits
+    ~code:mem
+    ~data:mem
+    ~vars
+    ~regs:Theory.Role.Register.[
+        [general; integer], ints;
+        (*[general; floating], flts;*)
+        (*[constant; zero; pseudo], x[0];*)
+        (*[pseudo], untyped@@[pc];*)
+        (*[function_argument], x(10--17) @ f(10--17);
+        [function_return], x(10--12) @ f(10--12);
+        [link], x[1];*)
+        [stack_pointer], r[1];
+        (*[thread], x[3];*)
+        (*[caller_saved], x[1] @ x(5--7) @ x(10--17) @ x(28--31) @
+                        f(0--7) @ f(10--17) @ f(28--31);
+        [callee_saved], x[2] @ x(8--9) @ x(18--27) @
+                        f(8--9) @ f(18--27);*)
+        [status; integer], untyped status_reg;
+        [carry_flag], untyped [cf];
+        [sign_flag], untyped [nf];
+        [zero_flag], untyped [zf];
+        [overflow_flag], untyped [vf];
+      ]
+
+let llvm16 = Theory.Language.declare ~package "llvm-msp430"

lib/bap_msp430/bap_msp430_target.mli

@@ -0,0 +1,9 @@
+open Bap_core_theory
+
+
+type r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+val msp430 : Theory.Target.t
+val llvm16 : Theory.Language.t

lib/bap_msp430/dune

@@ -0,0 +1,6 @@
+(library
+  (name bap_msp430)
+  (public_name bap-msp430)
+  (preprocess (pps ppx_bap))
+  (wrapped false)
+  (libraries bap-core-theory bap-knowledge core_kernel ))

plugins/msp430/dune

@@ -0,0 +1,22 @@
+(library
+ (name bap_msp430_plugin)
+ (public_name bap-msp430.plugin)
+ (preprocess (pps ppx_bap))
+ (libraries
+   bap
+   bap-abi
+   bap-api
+   bap-c
+   bap-core-theory
+   bap-knowledge
+   bap-main
+   bap-msp430
+   core_kernel
+   monads
+   ogre))
+
+(plugin
+ (name msp430)
+ (package bap-msp430)
+ (libraries bap-msp430.plugin)
+ (site (bap-common plugins)))

plugins/msp430/msp430_main.ml

@@ -0,0 +1,144 @@
+open Core_kernel[@@warning "-D"]
+open Bap_main
+open Bap.Std
+open Bap_core_theory
+open KB.Syntax
+module CT = Theory
+
+include Bap_main.Loggers()
+
+module Target = Bap_msp430_target
+module Dis = Disasm_expert.Basic
+
+type Extension.Error.t += Unknown_backend of string
+
+let provides = [
+  "semantics";
+  "lifter";
+  "msp430";
+]
+
+let use_llvm_decoding () =
+  KB.promise CT.Label.encoding @@ fun label ->
+  CT.Label.target label >>| fun t ->
+  if CT.Target.belongs Target.msp430 t
+  then Target.llvm16
+  else CT.Language.unknown
+
+
+let enable_llvm () =
+  Dis.register Target.llvm16 @@ fun _ ->
+  Dis.create (*TODO - find these out ~attrs:"+a,+c,+d,+m"*) ~backend:"llvm" "msp430"
+
+(*
+let pcode = Theory.Language.declare ~package:"bap" "pcode-msp430"
+
+let enable_pcode () =
+  Dis.register pcode @@begin fun t ->
+    Dis.create ~backend:"ghidra" @@ sprintf "msp430:LE:%d:default"
+      (Theory.Target.bits t)
+  end;
+  KB.promise Theory.Label.encoding @@begin fun label ->
+    Theory.Label.target label >>| fun t ->
+    if Theory.Target.belongs Target.parent t
+    then pcode
+    else Theory.Language.unknown
+  end
+*)
+
+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
+    | Ok arch -> arch in
+  KB.promise CT.Unit.target @@ fun unit ->
+  KB.collect Image.Spec.slot unit >>| request_arch >>| function
+  | Some "msp430" -> Target.msp430
+  | _ -> CT.Target.unknown
+
+module Abi = struct
+  open Bap_c.Std
+  open Bap.Std
+
+  module Arg = C.Abi.Arg
+  open Arg.Let
+  open Arg.Syntax
+
+  let is_floating = function
+    | `Basic {C.Type.Spec.t=#C.Type.real} -> true
+    | _ -> false
+
+  let data_model t =
+    let bits = Theory.Target.bits t in
+    new C.Size.base (if bits = 32 then `ILP32 else `LP64)
+
+  let define t =
+    let model = data_model t in
+    C.Abi.define t model @@ fun _ {C.Type.Proto.return=r; args} ->
+    let* iargs = Arg.Arena.iargs t in
+    let* irets = Arg.Arena.irets t in
+    let* fargs = Arg.Arena.fargs t in
+    let* frets = Arg.Arena.frets t in
+
+    (* integer calling convention *)
+    let integer regs t =
+      Arg.count regs t >>= function
+      | None -> Arg.reject ()
+      | Some 1 -> Arg.choice [
+          Arg.register regs t;
+          Arg.memory t;
+        ]
+      | Some 2 -> Arg.choice [
+          Arg.sequence [
+            Arg.align_even regs;
+            Arg.registers ~limit:2 regs t;
+          ];
+          Arg.split_with_memory regs t;
+          Arg.memory t;
+        ]
+      | Some _ -> Arg.reference regs t in
+
+    (* floating-point calling convention *)
+    let float iregs fregs t =
+      Arg.count fregs t >>= function
+      | Some 1 -> Arg.choice [
+          Arg.register fregs t;
+          Arg.register iregs t;
+          Arg.memory t;
+        ]
+      | _ -> integer iregs t in
+
+    let arg iregs fregs r =
+      if is_floating r
+      then float iregs fregs r
+      else integer iregs r in
+
+    Arg.define ?return:(match r with
+        | `Void -> None
+        | r -> Some (arg irets frets r))
+      (Arg.List.iter args ~f:(fun (_,t) ->
+           arg iargs fargs t));
+end
+
+
+let backend =
+  let open Extension in
+  Configuration.parameter Type.(some string) "backend"
+
+let main ctxt =
+  enable_loader ();
+  Abi.define Target.msp430;
+  match Extension.Configuration.get ctxt backend with
+  | Some "llvm" | None ->
+    use_llvm_decoding ();
+    enable_llvm ();
+    Ok ()
+(*| Some "ghidra" ->
+    enable_pcode ();
+    Ok ()*)
+  | Some s -> Error (Unknown_backend s)
+
+let () = Bap_main.Extension.declare main
+    ~doc:"provides msp430 semantics"
+    ~provides

plugins/msp430/semantics/dune

@@ -0,0 +1,4 @@
+(install
+ (files msp430.lisp)
+ (package bap-msp430)
+ (section (site (bap-common semantics))))