bap-primus

The BAP Microexecution Framework
IN THIS PACKAGE

Parameters

Signature

type 'a m = 'a Machine.t
val time : Time.t m

time returns the value of the machine clock.

  • since 2.1.0

halt halts the machine by raise the Halt exception.

val interrupt : int -> unit m

interrupt n interrupts the computation with cpuexn n

val pc : Bap.Std.addr m

pc current value of a program counter.

val pos : pos m

pos m current program position.

val sub : Bap.Std.sub Bap.Std.term -> unit m

sub x computes the subroutine x.

val blk : Bap.Std.blk Bap.Std.term -> unit m

blk x interprets the block x.

val exp : Bap.Std.exp -> value m

exp x returns a value of x.

val get : Bap.Std.var -> value m

get var reads var

val set : Bap.Std.var -> value -> unit m

set var x sets var to x

val binop : Bap.Std.binop -> value -> value -> value m

binop op x y computes a binary operation op on x and y.

If binop op x y will involve the division by zero, then the division by zero trap is signaled. If the division_by_zero_handler is provided, (i.e., is linked) then it will be invoked. If it returns normally, then the result of the binop op x y is undefined. Otherwise, the Division_by_zero machine exception is raised.

val unop : Bap.Std.unop -> value -> value m

unop op x computes an unary operation op on x

val cast : Bap.Std.cast -> int -> value -> value m

cast t n x casts n bits of x using a casting type t

val concat : value -> value -> value m

concat x y computes a concatenation of x and y

val extract : hi:int -> lo:int -> value -> value m

extract ~hi ~lo x extracts bits from lo to hi from x.

val const : Bap.Std.word -> value m

const x computes the constant expression x

val ite : value -> value -> value -> value m

ite c x y if c evals to b1 then x else y

load a d s computes a load operation, that loads a word of size s using an order specified by the endianness d from address a.

If the address a is not mapped, then a pagefault trap is signaled. If the pagefault_hanlder is provided, then it is invoked and the load operation repeats. Note, the handler either shall not return or ensure that the second attempt would be successful. If no handler is linked, then the segmentation fault machine exception is raised.

val store : value -> value -> Bap.Std.endian -> Bap.Std.size -> unit m

store a x d s computes a store operation, that stores at the address a the word x of size s, using an ordering specified by the endianness d.

If a is not mapped or not writable then the pagefault trap is invoked. If the handler is provided, then it is invoked and the operation is repeated. Otherwise the Segmentation_fault machine exception is raised.

val branch : value -> 'a m -> 'a m -> 'a m

branch cnd yes no if cnd evaluates to zero then yes else no.

val repeat : value m -> 'a m -> value m

repeat cnd body evaluates body until cnd evaluates to zero. Returns the value of cnd.