package bap-primus

  1. Overview
  2. Docs
package bap-primus
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Primus.Interpreter

The Interpreter.

The Interpreter is the core component of the Primus Machine. It provides lots of observations, giving other components an ability to track every event that happens during the program evaluation. The components can affect the results of evaluation in a limited way, by affecting the state of the components that are used by the Interpreter, name the Environment and the Memory.

Note: we the observation (x,y,z) notation in the documentation to denote an observation of a value represented with the (x,y,z) tuple, that in fact corresponds to observation >>> fun (x,y,z) -> ...

val clock : Time.t observation

clock occurs every time the machine clock changes its value.

val pc_change : Bap.Std.addr observation

pc_change x happens every time a code at address x is executed.

val loading : value observation

loading x happens before a value from the address x is loaded by the interpreter from the memory.

val loaded : (value * value) observation

loaded (addr,value) happens after the value is loaded from the address addr.

val storing : value observation

storing x happens before a value is stored at address x

val stored : (value * value) observation

stored (addr,value) happens after the value is stored at the address addr

val reading : Bap.Std.var observation

reading x happens before the variable x is read from the environment.

read (var,x) happens after a variable var is evaluated to the value x

val writing : Bap.Std.var observation

writing v happens before a value is written to the variable v

val written : (Bap.Std.var * value) observation

written (v,x) happens after x is assigned to v

val jumping : (value * value) observation

jumping (cond,dest) happens just before a jump to dest is taken under the specified condition cond. Note: the cond expression is always true and is computed from the path constraints of all outcoming edges of a block.

  • since 1.5.0
  • since 2.2.0 the condition is built from all edge

constraints.

val eval_cond : value observation

eval_cond c occurs on every decision making operation.

The conditional expression is a one bit wide bitvector could be true or false (contrary to the jumping observation).

The eval_cond observation is posted for all outcoming edges of a basic block with proper edge constraints.

For example, for a block

 when c1 goto d1
 when c2 goto d2
         goto d3

which has three edges with constraints, correspondingly,

  • c1
  • not c1 && c2
  • not c1 && not c2 && true
  • since 1.5.0 introduced
  • since 2.1.0 is posted by [branch] and [repeat] operations
  • since 2.2.0 the condition is a disjunction of negations

of the previous conditions.

val undefined : value observation

undefined x happens when a computation produces an undefined value x.

val const : value observation

const x happens when a constant x is created

val binop : ((Bap.Std.binop * value * value) * value) observation

binop ((op,x,y),r) happens after the binary operation op is applied to values x and y and evaluates to r

val unop : ((Bap.Std.unop * value) * value) observation

unop ((op,x),r) happens after the unary operation op is applied to x and results r

val cast : ((Bap.Std.cast * int * value) * value) observation

cast ((t,x),r) happens after x is casted to r using the casting type t

val extract : ((int * int * value) * value) observation

extract ((hi,lo,x),r) happens after r is extracted from x

val concat : ((value * value) * value) observation

extract ((x,y),z) happens after x is concatenated with y and produces z as a result.

val ite : ((value * value * value) * value) observation

ite ((cond, yes, no), res) happens after the ite expression that corresponds to ite(cond, yes, no) is evaluated to res.

val enter_term : Bap.Std.tid observation

an identifier of a term that will be executed next.

val leave_term : Bap.Std.tid observation

an identifier of a term that just finished the execution.

val enter_pos : pos observation

new program locatio entered

val leave_pos : pos observation

a program location left

a subroutine entered

a subroutine argument is entered

a basic block is entered

a phi-node is entered

a definition is entered

a jump term is entered

a subroutine was left

a subroutine argument was left

a basic block was left

a phi-node was left

a definition was left

a jump term was left

val enter_exp : Bap.Std.exp observation

an expression was entered

val leave_exp : Bap.Std.exp observation

an expression was left

val halting : unit observation

occurs on halt operation

val interrupt : int observation

interrupt n occurs on the machine interrupt n (aka CPU exception)

val division_by_zero : unit observation

division_by_zero occurs just before the division by zero trap is signaled.

See the binop operation and division_by_zero_handler for more information.

  • since 1.5
val pagefault : Bap.Std.addr observation

pagefault x occurs just before the pagefault trap is signaled.

See load and store operations, and pagefault_handler for more information.

  • since 1.5
val segfault : Bap.Std.addr observation

cfi_violation x occurs when the CFI is not preserved. The control flow integrity (CFI) is violated when a call doesn't return to an expected place. This might be an indicator of malicious code or an improper control flow graph.

After the observation is made the cfi_violation trap is signaled, which could be handled via the cfi_violation_handler.

  • since 1.7
type exn +=
  1. | Halt

is raised when a computation is halted

type exn +=
  1. | Division_by_zero

is raised by a machine that attempts to divide by zero

type exn +=
  1. | Segmentation_fault of Bap.Std.addr

is raised when a memory operation has failed.

val pagefault_handler : string

pagefault_hanlder is a trap handler that is invoked when the Pagefault exception is raised by the machine memory component. If the handler is provided via the Linker, then it is invoked, otherwise a segmentation fault is raised. If the handler returns normally then the faulty operation is repeated.

Note, page faults are usually handled together with the pagefault observation.

  • since 1.5
val division_by_zero_handler : string

division_by_zero_hanlder is a trap handler for the Division_by_zero exception. If it is linked into the machine, then it will be invoked when the division by zero trap is signaled. If it returns normally, then the result of the faulty operation is undefined.

  • since 1.5
val cfi_violation_handler : string

division_by_zero is the name of a trap handler for the Cfi_violation exception. If it is linked into the machine, then it will be invoked when the cfi-violation trap is signaled. If it returns normally, then the result of the faulty operation is undefined.

module Make (Machine : Machine.S) : sig ... end

Make(Machine) makes an interpreter that computes in the given Machine.