Primus.InterpreterThe 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 observationclock occurs every time the machine clock changes its value.
val pc_change : Bap.Std.addr observationpc_change x happens every time a code at address x is executed.
val loading : value observationloading x happens before a value from the address x is loaded by the interpreter from the memory.
val loaded : (value * value) observationloaded (addr,value) happens after the value is loaded from the address addr.
val storing : value observationstoring x happens before a value is stored at address x
val stored : (value * value) observationstored (addr,value) happens after the value is stored at the address addr
val reading : Bap.Std.var observationreading x happens before the variable x is read from the environment.
val read : (Bap.Std.var * value) observationread (var,x) happens after a variable var is evaluated to the value x
val writing : Bap.Std.var observationwriting v happens before a value is written to the variable v
val written : (Bap.Std.var * value) observationwritten (v,x) happens after x is assigned to v
val jumping : (value * value) observationjumping (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.
constraints.
val eval_cond : value observationeval_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 d3which has three edges with constraints, correspondingly,
c1not c1 && c2not c1 && not c2 && trueof the previous conditions.
val undefined : value observationundefined x happens when a computation produces an undefined value x.
val const : value observationconst x happens when a constant x is created
val binop : ((Bap.Std.binop * value * value) * value) observationbinop ((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) observationunop ((op,x),r) happens after the unary operation op is applied to x and results r
val cast : ((Bap.Std.cast * int * value) * value) observationcast ((t,x),r) happens after x is casted to r using the casting type t
val extract : ((int * int * value) * value) observationextract ((hi,lo,x),r) happens after r is extracted from x
val concat : ((value * value) * value) observationextract ((x,y),z) happens after x is concatenated with y and produces z as a result.
val ite : ((value * value * value) * value) observationite ((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 observationan identifier of a term that will be executed next.
val leave_term : Bap.Std.tid observationan identifier of a term that just finished the execution.
val enter_pos : pos observationnew program locatio entered
val leave_pos : pos observationa program location left
val enter_sub : Bap.Std.sub Bap.Std.term observationa subroutine entered
val enter_arg : Bap.Std.arg Bap.Std.term observationa subroutine argument is entered
val enter_blk : Bap.Std.blk Bap.Std.term observationa basic block is entered
val enter_phi : Bap.Std.phi Bap.Std.term observationa phi-node is entered
val enter_def : Bap.Std.def Bap.Std.term observationa definition is entered
val enter_jmp : Bap.Std.jmp Bap.Std.term observationa jump term is entered
val leave_sub : Bap.Std.sub Bap.Std.term observationa subroutine was left
val leave_arg : Bap.Std.arg Bap.Std.term observationa subroutine argument was left
val leave_blk : Bap.Std.blk Bap.Std.term observationa basic block was left
val leave_phi : Bap.Std.phi Bap.Std.term observationa phi-node was left
val leave_def : Bap.Std.def Bap.Std.term observationa definition was left
val leave_jmp : Bap.Std.jmp Bap.Std.term observationa jump term was left
val enter_exp : Bap.Std.exp observationan expression was entered
val leave_exp : Bap.Std.exp observationan expression was left
val halting : unit observationoccurs on halt operation
val interrupt : int observationinterrupt n occurs on the machine interrupt n (aka CPU exception)
val division_by_zero : unit observationdivision_by_zero occurs just before the division by zero trap is signaled.
See the binop operation and division_by_zero_handler for more information.
val pagefault : Bap.Std.addr observationpagefault x occurs just before the pagefault trap is signaled.
See load and store operations, and pagefault_handler for more information.
val segfault : Bap.Std.addr observationcfi_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.
is raised when a computation is halted
is raised by a machine that attempts to divide by zero
is raised when a memory operation has failed.
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.
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.
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.