Skip to content

Commit

Permalink
moves knowledge base rules from the library to the plugin (BinaryAnal…
Browse files Browse the repository at this point in the history 
…ysisPlatform#1403)

They all fit nicely into the disassemble plugin and it also opens an
opportunity to introduce command-line parameters for the rules. None
are added so far, but its good to have this option.
  • Loading branch information
@ivg
ivg authored Jan 13, 2022
1 parent fb4ed64 commit cd5aeb4
Show file tree
Hide file tree
Showing 10 changed files with 292 additions and 260 deletions.
14 changes: 14 additions & 0 deletions lib/bap/bap.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6773,6 +6773,14 @@ module Std : sig
(** [ops insn] gives an access to [insn]'s operands. *)
val ops : ('a,'k) t -> op array

(** [subs insn] an array of subinstructions.
An instruction can contain subinstructions, which could be
accessed with this function. Returns an empty array if
there are no subinstructions.
@since 2.5.0 *)
val subs : ('a,'k) t -> ('a,'k) t array
end

(** Trie maps over instructions *)
Expand Down Expand Up @@ -7029,6 +7037,12 @@ module Std : sig

(** [slot] for accessing the sequence number of a subinstruction. *)
val slot : (Theory.program, t option) KB.slot


(** [fresh] evaluates to a freshly generated sequence number.
@since 2.5.0 *)
val fresh : tid knowledge
end


Expand Down
157 changes: 0 additions & 157 deletions lib/bap/bap_project.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,163 +39,6 @@ let memory_slot = KB.Class.property Theory.Unit.cls "unit-memory"
~desc:"annotated memory regions of the unit"
Memmap.domain

module Symbols = struct
open KB.Let
open KB.Syntax

module Addr = struct
include Bitvec
include Bitvec_order
include Bitvec_binprot.Functions
include Bitvec_sexp.Functions
end

type table = {
roots : Set.M(Addr).t;
names : string Map.M(Addr).t;
aliases : Set.M(String).t Map.M(Addr).t;
} [@@deriving compare, equal, bin_io, sexp]

let empty = {
roots = Set.empty (module Addr);
names = Map.empty (module Addr);
aliases = Map.empty (module Addr);
}

let slot = KB.Class.property Theory.Unit.cls
~package:"bap" "symbol-table"
~persistent:(KB.Persistent.of_binable (module struct
type t = table [@@deriving bin_io]
end)) @@
KB.Domain.flat ~empty ~equal:equal_table "symbols"

let is_ident s =
String.length s > 0 &&
(Char.is_alpha s.[0] || Char.equal s.[0] '_') &&
String.for_all s ~f:(fun c -> Char.is_alphanum c ||
Char.equal c '_')

let from_spec t =
let collect fld = Ogre.collect Ogre.Query.(select @@ from fld) in
let open Ogre.Let in
let to_addr =
let m = Bitvec.modulus (Theory.Target.code_addr_size t) in
let n = Theory.Target.code_alignment t / Theory.Target.byte t in
let mask = Int64.(lnot (of_int n - 1L)) in
fun x ->
let x = Int64.(x land mask) in
Bitvec.(int64 x mod m) in
let add_alias tab addr alias = {
tab with aliases = Map.update tab.aliases addr ~f:(function
| None -> Set.singleton (module String) alias
| Some names -> Set.add names alias)
} in
let pp_comma ppf () = Format.pp_print_string ppf ", " in
let pp_addrs =
Format.pp_print_list ~pp_sep:pp_comma Bitvec.pp
and pp_names =
Format.pp_print_list ~pp_sep:pp_comma Format.pp_print_string in
let* roots =
let+ roots =
let* starts = collect Image.Scheme.code_start in
let* values = collect Image.Scheme.symbol_value in
let+ entry = Ogre.request Image.Scheme.entry_point in
let roots = Seq.append starts (Seq.map ~f:fst values) in
match entry with
| None -> roots
| Some entry -> Seq.cons entry roots in
Seq.fold roots ~init:(Set.empty (module Bitvec_order))
~f:(fun xs x -> Set.add xs (to_addr x)) in
let+ named_symbols = collect Image.Scheme.named_symbol in
let init = {empty with roots},
Bap_relation.empty Bitvec.compare String.compare in
Seq.fold named_symbols ~init ~f:(fun (tab,rel) (data,name) ->
let addr = to_addr data in
if Set.mem roots addr && is_ident name
then tab,Bap_relation.add rel (to_addr data) name
else add_alias tab addr name, rel) |> fun (table,rel) ->
Bap_relation.matching rel table
~saturated:(fun k v t -> {
t with names = Map.add_exn t.names k v
})
~unmatched:(fun reason t -> match reason with
| Non_injective_fwd (addrs,name) ->
info "the symbol %s has ambiguous addresses: %a@\n"
name pp_addrs addrs;
t
| Non_injective_bwd (names,addr) ->
info "the symbol at %a has ambiguous names: %a@\n"
Bitvec.pp addr pp_names names;
t)

let build_table t spec = match Ogre.eval (from_spec t) spec with
| Ok x -> x
| Error err ->
invalid_argf "Malformed ogre specification: %s"
(Error.to_string_hum err) ()

let collect_inputs from obj f =
KB.collect Theory.Label.unit obj >>=? fun unit ->
KB.collect Theory.Label.addr obj >>=? fun addr ->
let+ data = KB.collect from unit in
f data addr

let promised_table : unit =
KB.promise slot @@ fun unit ->
let* t = KB.collect Theory.Unit.target unit in
let+ s = KB.collect Image.Spec.slot unit in
build_table t s

let promised_roots : unit =
KB.Rule.(begin
declare "provides roots" |>
require Image.Spec.slot |>
provide Theory.Label.is_subroutine |>
comment "computes roots from spec";
end);
KB.promise Theory.Label.is_subroutine @@ fun obj ->
collect_inputs slot obj @@ fun {roots} addr ->
Option.some_if (Set.mem roots addr) true


let names_agent = KB.Agent.register
~package:"bap" "specification-provider"
~desc:"provides names obtained from the image specification."

let promised_names : unit =
KB.Rule.(begin
declare "provides names" |>
require Image.Spec.slot |>
provide Theory.Label.possible_name |>
comment "computes symbol names from spec";
end);
KB.propose names_agent Theory.Label.possible_name @@ fun obj ->
collect_inputs slot obj @@ fun {names} addr ->
Map.find names addr


let promised_aliases : unit =
KB.Rule.(begin
declare "provides aliases" |>
require Image.Spec.slot |>
provide Theory.Label.possible_name |>
comment "computes symbol aliases (names) from spec";
end);
KB.promise Theory.Label.aliases @@ fun obj ->
let* unit = KB.collect Theory.Label.unit obj in
let* addr = KB.collect Theory.Label.addr obj in
match unit,addr with
| None,_|_,None -> KB.return (Set.empty (module String))
| Some unit, Some addr ->
let+ {aliases} = KB.collect slot unit in
match Map.find aliases addr with
| None -> Set.empty (module String)
| Some aliases -> aliases
end




let with_filename spec target _code memory path f =
let open KB.Syntax in
let width = Theory.Target.code_addr_size target in
Expand Down
14 changes: 9 additions & 5 deletions lib/bap_disasm/bap_disasm_basic.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ module Insn = struct
encoding : string;
code : int;
name : string;
asm : bytes;
asm : string;
kinds: kind list;
opers: Op.t array;
subs : ins_info array;
Expand All @@ -342,14 +342,18 @@ module Insn = struct

let name {name = x} = x
let code op = op.code
let asm x = Bytes.to_string x.asm
let asm x = x.asm
let ops x = x.opers
let kinds x = x.kinds
let subs x = x.subs
let is op x =
let equal x y = Kind.compare x y = 0 in
List.mem ~equal op.kinds x

let normalize_asm asm =
String.substr_replace_all asm ~pattern:"\t"
~with_:" " |> String.strip

let rec create ?parent ~asm ~kinds dis ~insn =
let subs = Hashtbl.create (module Int) in
let opers =
Expand Down Expand Up @@ -379,8 +383,8 @@ module Insn = struct
if asm then
let data = Bytes.create (C.insn_asm_size !!dis ~insn) in
C.insn_asm_copy !!dis ~insn data;
data
else Bytes.empty in
normalize_asm @@ Bytes.to_string data
else "" in
let kinds =
if kinds then
List.fold Kind.all ~init:[] ~f:(fun ks k ->
Expand Down Expand Up @@ -416,7 +420,7 @@ let sexp_of_full_insn = sexp_of_insn
let compare_full_insn i1 i2 =
let open Insn in
let r1 = Int.compare i1.code i2.code in
if r1 <> 0 then Bytes.compare i1.asm i2.asm
if r1 <> 0 then String.compare i1.asm i2.asm
else r1


Expand Down
57 changes: 2 additions & 55 deletions lib/bap_disasm/bap_disasm_insn.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,11 +82,6 @@ end
type t = Theory.Semantics.t
type op = Op.t [@@deriving bin_io, compare, sexp]

let normalize_asm asm =
String.substr_replace_all asm ~pattern:"\t"
~with_:" " |> String.strip


module Slot = struct
type 'a t = (Theory.Effect.cls, 'a) KB.slot
let empty = "#undefined"
Expand All @@ -111,19 +106,6 @@ module Slot = struct
~public:true
~desc:"an assembly string"

let provide_asm : unit =
KB.Rule.(begin
declare ~package:"bap" "asm-of-basic" |>
require Insn.slot |>
provide asm |>
comment "provides the assembly string";
end);
let open KB.Syntax in
KB.promise Theory.Semantics.slot @@ fun label ->
let+ insn = label-->?Insn.slot in
KB.Value.put asm Theory.Semantics.empty @@
normalize_asm @@ Insn.asm insn

let sexp_of_op = function
| Op.Reg r -> Sexp.Atom (Reg.name r)
| Op.Imm w -> sexp_of_int64 (Imm.to_int64 w)
Expand Down Expand Up @@ -307,7 +289,7 @@ let write init ops =
let set_basic effect insn : t =
write effect Slot.[
name <-- Insn.name insn;
asm <-- normalize_asm (Insn.asm insn);
asm <-- Insn.asm insn;
ops <-- Some (Insn.ops insn);
]

Expand Down Expand Up @@ -337,7 +319,7 @@ let should = must
let shouldn't = mustn't

let name = KB.Value.get Slot.name
let asm = KB.Value.get Slot.asm
let asm = KB.Value.get Slot.asm
let bil insn = KB.Value.get Bil.slot insn
let ops s = match KB.Value.get Slot.ops s with
| None -> [||]
Expand Down Expand Up @@ -447,41 +429,6 @@ module Seqnum = struct
let fresh = KB.Syntax.(freshnum >>= label)
end



let provide_sequence_semantics () =
let open KB.Syntax in
KB.promise Theory.Semantics.slot @@ fun obj ->
KB.collect Insn.slot obj >>= function
| None -> !!Theory.Semantics.empty
| Some insn when not (String.equal (Insn.name insn) "seq") ->
!!Theory.Semantics.empty
| Some insn -> match Insn.subs insn with
| [||] -> !!Theory.Semantics.empty
| subs ->
Theory.instance () >>= Theory.require >>= fun (module CT) ->
let subs = Array.to_list subs |>
List.map ~f:(fun sub ->
Seqnum.fresh >>| fun lbl ->
lbl,sub) in
KB.all subs >>=
KB.List.map ~f:(fun (obj,sub) ->
KB.provide Insn.slot obj (Some sub) >>= fun () ->
KB.collect Theory.Semantics.slot obj >>= fun sema ->
let nil = Theory.Effect.empty Theory.Effect.Sort.bot in
CT.seq (CT.blk obj !!nil !!nil) !!sema) >>=
KB.List.reduce ~f:(fun s1 s2 -> CT.seq !!s1 !!s2) >>| function
| None -> empty
| Some sema -> with_basic sema insn

let () =
let open KB.Rule in
declare "sequential-instruction" |>
require Insn.slot |>
provide Theory.Semantics.slot |>
comment "computes sequential instructions semantics";
provide_sequence_semantics ()

let () =
Data.Write.create ~pp:Adt.pp () |>
add_writer ~desc:"Abstract Data Type pretty printing format"
Expand Down
1 change: 1 addition & 0 deletions lib/bap_disasm/bap_disasm_insn.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ module Seqnum : sig
type t = int
val label : ?package:string -> t -> Theory.Label.t KB.t
val slot : (Theory.program, t option) KB.slot
val fresh : tid KB.t
end

module Slot : sig
Expand Down
28 changes: 0 additions & 28 deletions lib/bap_image/bap_memory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -446,7 +446,6 @@ include Printable.Make(struct

let hexdump t = Format.asprintf "%a" pp_hex t


let domain = KB.Domain.optional "mem"
~equal:(fun x y ->
Addr.equal x.addr y.addr &&
Expand All @@ -457,30 +456,3 @@ let slot = KB.Class.property ~package:"bap"
Theory.Program.cls "mem" domain
~public:true
~desc:"a memory region occupied by the program"

let () =
let open KB.Syntax in
KB.promise Theory.Label.addr @@ fun label ->
KB.collect slot label >>|? fun mem ->
Some (Addr.to_bitvec (min_addr mem))

let () =
KB.Rule.(begin
declare ~package:"bap" "code-of-mem" |>
require slot |>
provide Theory.Semantics.code |>
comment "extracts the memory contents"
end);
let open KB.Syntax in
KB.promise Theory.Semantics.slot @@ fun label ->
let+ {data; off; size} = label-->?slot in
let empty = KB.Value.empty Theory.Semantics.cls in
KB.Value.put Theory.Semantics.code empty @@
Some (Bigstring.to_string ~pos:off ~len:size data)

let () =
let open KB.Rule in
declare ~package:"bap" "addr-of-mem" |>
require slot |>
provide Theory.Label.addr |>
comment "addr of the first byte"
11 changes: 0 additions & 11 deletions lib/bap_types/bap_arch.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,17 +84,6 @@ module T = struct
Theory.Unit.cls "unit-arch" domain
~persistent

let _arch_of_unit_ : unit =
KB.Rule.(declare ~package:"bap" "arch-of-unit" |>
require Theory.Label.unit |>
require unit_slot |>
provide slot |>
comment "propagates arch from the unit");
let open KB.Syntax in
KB.promise slot @@ fun obj ->
KB.collect Theory.Label.unit obj >>= function
| None -> KB.return `unknown
| Some unit -> KB.collect unit_slot unit
end

include T
Expand Down
Loading

0 comments on commit cd5aeb4

Please sign in to comment.