03-Promising-semantics.md

Promising semantics

You can use KB.promise to promise values for slots. Whenever you use KB.collect to retrieve the data in a slot, BAP will trigger all the promises, in order to compute the best information at that time.

However, if you use KB.provide to fill a slot, then BAP will consider that to be the definitive value for that slot. If you use KB.collect after that, BAP will not trigger any of the promises.

Various parts of BAP's inner plumbing relies on promises associated with the semantics slot. Whenever you want to provide semantics, it is therefore best to use KB.promise. If you use KB.provide to put semantics into Theory.Semantics.slot, you may prevent other promises from firing.

Example

In a new folder somewhere, create a file called main.ml with the following:

open Bap.Std

module T = Bap_core_theory.Theory
module KB = Bap_core_theory.KB

open KB.Let

let () = match Bap_main.init () with
  | Ok () -> ()
  | Error _ -> failwith "Error initializing BAP"

Add a function that generates semantics (an empty block):

let provide_semantics (label : T.Label.t) : 'a T.effect KB.t =
  let* (module CT) = T.current in
  let nop = T.Effect.Sort.data "NOP" in
  let data = KB.return (T.Effect.empty nop) in
  let ctrl = KB.return (T.Effect.empty T.Effect.Sort.fall) in
  CT.blk label data ctrl

Register this function as a promise for T.Semantics.slot:

let () = KB.promise T.Semantics.slot provide_semantics

Next, add a function that creates a compilation unit:

let create_compilation_unit (target : T.Target.t) : T.Unit.t KB.t =
  let* comp_unit = KB.Object.create T.Unit.cls in
  let* () = KB.provide T.Unit.target comp_unit target in
  KB.return comp_unit

Add a function that creates a program label and adds the compilation unit to it:

let create_program (addr : Bitvec.t) (target : T.Target.t) : T.Label.t KB.t =
  let* label = T.Label.for_addr addr in
  let* comp_unit = create_compilation_unit target in
  let* () = KB.provide T.Label.unit label (Some comp_unit) in
  KB.return label

Notice that no semantics have been provided (instead, they have been promised).

Now, create a program, and use Toplevel.eval to evaluate its semantics:

let () =
  let target = T.Target.read "bap:armv7+le" in
  let addr = Bitvec.(int 0x10400 mod m32) in
  let label = create_program addr target in
  let program = Toplevel.eval T.Semantics.slot label in
  Format.printf "%a\n%!" KB.Value.pp program

When Toplevel.eval runs, it will collect the semantics for the given label, and that will trigger the promise registered above.

To summarize, the entire main.ml file looks like this:

open Bap.Std

module T = Bap_core_theory.Theory
module KB = Bap_core_theory.KB

open KB.Let

let () = match Bap_main.init () with
  | Ok () -> ()
  | Error _ -> failwith "Error initializing BAP"

let provide_semantics (label : T.Label.t) : 'a T.effect KB.t =
  let* (module CT) = T.current in
  let nop = T.Effect.Sort.data "NOP" in
  let data = KB.return (T.Effect.empty nop) in
  let ctrl = KB.return (T.Effect.empty T.Effect.Sort.fall) in
  CT.blk label data ctrl

let () = KB.promise T.Semantics.slot provide_semantics

let create_compilation_unit (target : T.Target.t) : T.Unit.t KB.t =
  let* comp_unit = KB.Object.create T.Unit.cls in
  let* () = KB.provide T.Unit.target comp_unit target in
  KB.return comp_unit

let create_program (addr : Bitvec.t) (target : T.Target.t) : T.Label.t KB.t =
  let* label = T.Label.for_addr addr in
  let* comp_unit = create_compilation_unit target in
  let* () = KB.provide T.Label.unit label (Some comp_unit) in
  KB.return label

let () =
  let target = T.Target.read "bap:armv7+le" in
  let addr = Bitvec.(int 0x10400 mod m32) in
  let label = create_program addr target in
  let program = Toplevel.eval T.Semantics.slot label in
  Format.printf "%a\n%!" KB.Value.pp program

Add a dune file:

(executable
  (name main)
  (libraries findlib.dynload bap))

Add a Makefile:

EXE := main.exe


#####################################################
# DEFAULT
#####################################################

.DEFAULT_GOAL := all

all: clean run


#####################################################
# THE EXE
#####################################################

.PHONY: clean
clean:
        dune clean

build:
        dune build ./$(EXE)

run: build
        dune exec ./$(EXE)

Run the program:

make

It will print out the snapshot:

(bap:ir-graph "00000009:
                ")
 (bap:insn-dests (()))
 (bap:bir (%00000009))
 (bap:bil "{
             label(%00000009)
           }"))

Clean up:

make clean