Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add MSP430 lifter. #1605

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions bap-msp430.opam
Original file line number Diff line number Diff line change
@@ -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"
17 changes: 17 additions & 0 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down
77 changes: 77 additions & 0 deletions lib/bap_msp430/bap_msp430_target.ml
Original file line number Diff line number Diff line change
@@ -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"
9 changes: 9 additions & 0 deletions lib/bap_msp430/bap_msp430_target.mli
Original file line number Diff line number Diff line change
@@ -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
6 changes: 6 additions & 0 deletions lib/bap_msp430/dune
Original file line number Diff line number Diff line change
@@ -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 ))
22 changes: 22 additions & 0 deletions plugins/msp430/dune
Original file line number Diff line number Diff line change
@@ -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)))
144 changes: 144 additions & 0 deletions plugins/msp430/msp430_main.ml
Original file line number Diff line number Diff line change
@@ -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
Empty file added plugins/msp430/msp430_main.mli
Empty file.
4 changes: 4 additions & 0 deletions plugins/msp430/semantics/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
(install
(files msp430.lisp)
(package bap-msp430)
(section (site (bap-common semantics))))
Loading
Loading