Bil (bap.Bap.Std.Bil)

module Types : sig ... end

include all constructors into Bil namespace

include module type of Types
  with type cast = Types.cast
   and type binop = Types.binop
   and type unop = Types.unop
   and type typ = Types.typ
   and type var = Types.var
   and type exp = Types.exp
   and type stmt = Types.stmt

type var = Types.var

type cast = Types.cast =

| UNSIGNED
(*
0-padding widening cast.
*)
| SIGNED
(*
Sign-extending widening cast.
*)
| HIGH
(*
Narrowing cast. Keeps the high bits.
*)
| LOW
(*
Narrowing cast. Keeps the low bits.
*)

Different forms of casting

val bin_shape_cast : Core_kernel.Bin_prot.Shape.t

val bin_size_cast : cast Core_kernel.Bin_prot.Size.sizer

val bin_write_cast : cast Core_kernel.Bin_prot.Write.writer

val bin_writer_cast : cast Core_kernel.Bin_prot.Type_class.writer

val bin_read_cast : cast Core_kernel.Bin_prot.Read.reader

val __bin_read_cast__ : (int -> cast) Core_kernel.Bin_prot.Read.reader

val bin_reader_cast : cast Core_kernel.Bin_prot.Type_class.reader

val bin_cast : cast Core_kernel.Bin_prot.Type_class.t

val compare_cast : cast -> cast -> int

val sexp_of_cast : cast -> Ppx_sexp_conv_lib.Sexp.t

val cast_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> cast

type binop = Types.binop =

| PLUS
(*
Integer addition. (commutative, associative)
*)
| MINUS
(*
Subtract second integer from first.
*)
| TIMES
(*
Integer multiplication. (commutative, associative)
*)
| DIVIDE
(*
Unsigned integer division.
*)
| SDIVIDE
(*
Signed integer division.
*)
| MOD
(*
Unsigned modulus.
*)
| SMOD
(*
Signed modulus.
*)
| LSHIFT
(*
Left shift.
*)
| RSHIFT
(*
Right shift, zero padding.
*)
| ARSHIFT
(*
Right shift, sign extend.
*)
| AND
(*
Bitwise and. (commutative, associative)
*)
| OR
(*
Bitwise or. (commutative, associative)
*)
| XOR
(*
Bitwise xor. (commutative, associative)
*)
| EQ
(*
Equals. (commutative) (associative on booleans)
*)
| NEQ
(*
Not equals. (commutative) (associative on booleans)
*)
| LT
(*
Unsigned less than.
*)
| LE
(*
Unsigned less than or equal to.
*)
| SLT
(*
Signed less than.
*)
| SLE
(*
Signed less than or equal to.
*)

Binary operations implemented in the BIL

val bin_shape_binop : Core_kernel.Bin_prot.Shape.t

val bin_size_binop : binop Core_kernel.Bin_prot.Size.sizer

val bin_write_binop : binop Core_kernel.Bin_prot.Write.writer

val bin_writer_binop : binop Core_kernel.Bin_prot.Type_class.writer

val bin_read_binop : binop Core_kernel.Bin_prot.Read.reader

val __bin_read_binop__ : (int -> binop) Core_kernel.Bin_prot.Read.reader

val bin_reader_binop : binop Core_kernel.Bin_prot.Type_class.reader

val bin_binop : binop Core_kernel.Bin_prot.Type_class.t

val compare_binop : binop -> binop -> int

val sexp_of_binop : binop -> Ppx_sexp_conv_lib.Sexp.t

val binop_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> binop

type unop = Types.unop =

| NEG
(*
Negate. (2's complement)
*)
| NOT
(*
Bitwise not.(1's complement)
*)

Unary operations implemented in the IR

val bin_shape_unop : Core_kernel.Bin_prot.Shape.t

val bin_size_unop : unop Core_kernel.Bin_prot.Size.sizer

val bin_write_unop : unop Core_kernel.Bin_prot.Write.writer

val bin_writer_unop : unop Core_kernel.Bin_prot.Type_class.writer

val bin_read_unop : unop Core_kernel.Bin_prot.Read.reader

val __bin_read_unop__ : (int -> unop) Core_kernel.Bin_prot.Read.reader

val bin_reader_unop : unop Core_kernel.Bin_prot.Type_class.reader

val bin_unop : unop Core_kernel.Bin_prot.Type_class.t

val compare_unop : unop -> unop -> int

val sexp_of_unop : unop -> Ppx_sexp_conv_lib.Sexp.t

val unop_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> unop

type exp = Types.exp =

| Load of exp * exp * endian * size
(*
load from memory
*)
| Store of exp * exp * exp * endian * size
(*
store to memory
*)
| BinOp of binop * exp * exp
(*
binary operation
*)
| UnOp of unop * exp
(*
unary operation
*)
| Var of var
(*
variable
*)
| Int of word
(*
immediate value
*)
| Cast of cast * int * exp
(*
casting
*)
| Let of var * exp * exp
(*
let-binding
*)
| Unknown of string * typ
(*
unknown or undefined value
*)
| Ite of exp * exp * exp
(*
if-then-else expression
*)
| Extract of int * int * exp
(*
extract portion of word
*)
| Concat of exp * exp
(*
concatenate two words
*)

BIL expression variants

and typ = Types.typ =

| Imm of int
(*
Imm n - n-bit immediate
*)
| Mem of addr_size * size
(*
Mem (a,t) memory with a specifed addr_size
*)
| Unk

val bin_shape_exp : Core_kernel.Bin_prot.Shape.t

val bin_shape_typ : Core_kernel.Bin_prot.Shape.t

val bin_size_exp : exp Core_kernel.Bin_prot.Size.sizer

val bin_write_exp : exp Core_kernel.Bin_prot.Write.writer

val bin_writer_exp : exp Core_kernel.Bin_prot.Type_class.writer

val bin_size_typ : typ Core_kernel.Bin_prot.Size.sizer

val bin_write_typ : typ Core_kernel.Bin_prot.Write.writer

val bin_writer_typ : typ Core_kernel.Bin_prot.Type_class.writer

val bin_read_exp : exp Core_kernel.Bin_prot.Read.reader

val __bin_read_exp__ : (int -> exp) Core_kernel.Bin_prot.Read.reader

val bin_reader_exp : exp Core_kernel.Bin_prot.Type_class.reader

val bin_read_typ : typ Core_kernel.Bin_prot.Read.reader

val __bin_read_typ__ : (int -> typ) Core_kernel.Bin_prot.Read.reader

val bin_reader_typ : typ Core_kernel.Bin_prot.Type_class.reader

val bin_exp : exp Core_kernel.Bin_prot.Type_class.t

val bin_typ : typ Core_kernel.Bin_prot.Type_class.t

val compare_exp : exp -> exp -> int

val compare_typ : typ -> typ -> int

val sexp_of_exp : exp -> Ppx_sexp_conv_lib.Sexp.t

val sexp_of_typ : typ -> Ppx_sexp_conv_lib.Sexp.t

val exp_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> exp

val typ_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> typ

type stmt = Types.stmt =

| Move of var * exp
(*
assign value of expression to variable
*)
| Jmp of exp
(*
jump to absolute address
*)
| Special of string
(*
Statement with semantics not expressible in BIL
*)
| While of exp * stmt list
(*
while loops
*)
| If of exp * stmt list * stmt list
(*
if/then/else statement
*)
| CpuExn of int
(*
CPU exception
*)

val bin_shape_stmt : Core_kernel.Bin_prot.Shape.t

val bin_size_stmt : stmt Core_kernel.Bin_prot.Size.sizer

val bin_write_stmt : stmt Core_kernel.Bin_prot.Write.writer

val bin_writer_stmt : stmt Core_kernel.Bin_prot.Type_class.writer

val bin_read_stmt : stmt Core_kernel.Bin_prot.Read.reader

val __bin_read_stmt__ : (int -> stmt) Core_kernel.Bin_prot.Read.reader

val bin_reader_stmt : stmt Core_kernel.Bin_prot.Type_class.reader

val bin_stmt : stmt Core_kernel.Bin_prot.Type_class.t

val compare_stmt : stmt -> stmt -> int

val sexp_of_stmt : stmt -> Ppx_sexp_conv_lib.Sexp.t

val stmt_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> stmt

type t = stmt list

include Core_kernel.Bin_prot.Binable.S with type t := t

val bin_size_t : t Bin_prot.Size.sizer

val bin_write_t : t Bin_prot.Write.writer

val bin_read_t : t Bin_prot.Read.reader

val __bin_read_t__ : (int -> t) Bin_prot.Read.reader

val bin_shape_t : Bin_prot.Shape.t

val bin_writer_t : t Bin_prot.Type_class.writer

val bin_reader_t : t Bin_prot.Type_class.reader

val bin_t : t Bin_prot.Type_class.t

val compare : t -> t -> int

include Ppx_sexp_conv_lib.Sexpable.S with type t := t

val t_of_sexp : Sexplib0__.Sexp.t -> t

val sexp_of_t : t -> Sexplib0__.Sexp.t

type var_compare

type vars = (var, var_compare) Core_kernel.Set.t

include Regular.Std.Printable.S with type t := t

val to_string : t -> string

to_string x returns a human-readable representation of x

val str : unit -> t -> string

str () t is formatted output function that matches "%a" conversion format specifier in functions, that prints to string, e.g., sprintf, failwithf, errorf and, surprisingly all Lwt printing function, including Lwt_io.printf and logging (or any other function with type ('a,unit,string,...) formatN`. Example:

Or_error.errorf "type %a is not valid for %a"
  Type.str ty Exp.str exp

val pps : unit -> t -> string

synonym for str

val ppo : Core_kernel.Out_channel.t -> t -> unit

will print to a standard output_channel, useful for using in printf, fprintf, etc.

val pp_seq : Stdlib.Format.formatter -> t Core_kernel.Sequence.t -> unit

prints a sequence of values of type t

this will include pp function from Core that has type t printer, and can be used in Format.printf family of functions

include Core_kernel.Pretty_printer.S with type t := t

val pp : Base__.Formatter.t -> t -> unit

include Regular.Std.Data.S with type t := t

type info = string * [ `Ver of string ] * string option

name,Ver v,desc information attached to a particular reader or writer.

val version : string

Data representation version. After any change in data representation the version should be increased.

Serializers that are derived from a data representation must have the same version as a version of the data structure, from which it is derived. This kind of serializers can only read and write data of the same version.

Other serializers can actually read and write data independent on its representation version. A serializer, that can't store data of current version simply shouldn't be added to a set of serializers.

It is assumed, that if a reader and a writer has the same name and version, then whatever was written by the writer should be readable by the reader. The round-trip equality is not required, thus it is acceptable if some information is lost.

It is also possible, that a reader and a writer that has the same name are compatible. In that case it is recommended to use semantic versioning.

val size_in_bytes : ?ver:string -> ?fmt:string -> t -> int

size_in_bytes ?ver ?fmt datum returns the amount of bytes that is needed to represent datum in the given format and version

val of_bytes : ?ver:string -> ?fmt:string -> Regular.Std.bytes -> t

of_bytes ?ver ?fmt bytes deserializes a value from bytes.

val to_bytes : ?ver:string -> ?fmt:string -> t -> Regular.Std.bytes

to_bytes ?ver ?fmt datum serializes a datum to a sequence of bytes.

val blit_to_bytes : 
  ?ver:string ->
  ?fmt:string ->
  Regular.Std.bytes ->
  t ->
  int ->
  unit

blit_to_bytes ?ver ?fmt buffer datum offset copies a serialized representation of datum into a buffer, starting from the offset.

val of_bigstring : ?ver:string -> ?fmt:string -> Core_kernel.bigstring -> t

of_bigstring ?ver ?fmt buf deserializes a datum from bigstring

val to_bigstring : ?ver:string -> ?fmt:string -> t -> Core_kernel.bigstring

of_bigstring ?ver ?fmt datum serializes a datum to a sequence of bytes represented as bigstring

val blit_to_bigstring : 
  ?ver:string ->
  ?fmt:string ->
  Core_kernel.bigstring ->
  t ->
  int ->
  unit

blit_to_bigstring ?ver ?fmt buffer datum offset copies a serialized representation of datum into a buffer, starting from offset.

module Io : sig ... end

Input/Output functions for the given datum.

module Cache : sig ... end

Data cache.

val add_reader : 
  ?desc:string ->
  ver:string ->
  string ->
  t Regular.Std.reader ->
  unit

add_reader ?desc ~ver name reader registers a new reader with a provided name, version ver and optional description desc

val add_writer : 
  ?desc:string ->
  ver:string ->
  string ->
  t Regular.Std.writer ->
  unit

add_writer ?desc ~ver name writer registers a new writer with a provided name, version ver and optional description desc

val available_readers : unit -> info list

available_reader () lists available readers for the data type

val default_reader : unit -> info

default_reader returns information about default reader

val set_default_reader : ?ver:string -> string -> unit

set_default_reader ?ver name sets new default reader. If version is not specified then the latest available version is used. Raises an exception if a reader with a given name doesn't exist.

val with_reader : ?ver:string -> string -> (unit -> 'a) -> 'a

with_reader ?ver name operation temporary sets a default reader to a reader with a specified name and version. The default reader is restored after operation is finished.

val available_writers : unit -> info list

available_writer () lists available writers for the data type

val default_writer : unit -> info

default_writer returns information about the default writer

val set_default_writer : ?ver:string -> string -> unit

set_default_writer ?ver name sets new default writer. If version is not specified then the latest available version is used. Raises an exception if a writer with a given name doesn't exist.

val with_writer : ?ver:string -> string -> (unit -> 'a) -> 'a

with_writer ?ver name operation temporary sets a default writer to a writer with a specified name and version. The default writer is restored after operation is finished.

val default_printer : unit -> info option

default_writer optionally returns an information about default printer

val set_default_printer : ?ver:string -> string -> unit

set_default_printer ?ver name sets new default printer. If version is not specified then the latest available version is used. Raises an exception if a printer with a given name doesn't exist.

val with_printer : ?ver:string -> string -> (unit -> 'a) -> 'a

with_printer ?ver name operation temporary sets a default printer to a printer with a specified name and version. The default printer is restored after operation is finished.

Low level access to serializers

val find_reader : ?ver:string -> string -> t Regular.Std.reader option

find_reader ?ver name lookups a reader with a given name. If version is not specified, then a reader with maximum version is returned.

val find_writer : ?ver:string -> string -> t Regular.Std.writer option

find_writer ?ver name lookups a writer with a given name. If version is not specified, then a writer with maximum version is returned.

val domain : stmt list Bap_knowledge.Knowledge.domain

Bil is an instance of Domain.

A flat domain with the empty Bil program being the empty element.

val persistent : stmt list Bap_knowledge.Knowledge.persistent

Instance of the persistence class

val slot : 
  (Bap_core_theory.Theory.Program.Semantics.cls, stmt list)
    Bap_knowledge.Knowledge.slot

The denotation of the program semantics as a BIL program.

val code : (Bap_core_theory.Theory.program, stmt list) Bap_core_theory.KB.slot

The representation of the program as a BIL program.

since 2.3.0

val pp_binop : Stdlib.Format.formatter -> binop -> unit

printf "%a" pp_binop op prints a binary operation op.

val pp_unop : Stdlib.Format.formatter -> unop -> unit

printf "%a" pp_unop op prints an unary operation op

val pp_cast : Stdlib.Format.formatter -> cast -> unit

printf "%a" pp_cast t prints a cast type t

since 1.3

val string_of_binop : binop -> string

string_of_binop op is a textual representation of op.

since 1.3

val string_of_unop : unop -> string

string_of_unop op is a textual representation of op.

since 1.3

val string_of_cast : cast -> string

string_of_cast t is a textual representation of a cast type

since 1.3

module Infix : sig ... end

Infix operators

Brings infix operations into scope of the Bil module.

include module type of Infix

Infix operators

val (:=) : var -> exp -> stmt

x := y -> Move (x,y)

Arithmetic operations

val (+) : exp -> exp -> exp

x + y -> BinOp (PLUS,x,y)

val (-) : exp -> exp -> exp

x - y -> BinOp(MINUS,x,y)

val (*) : exp -> exp -> exp

x * y -> BinOp(TIMES,x,y)

val (/) : exp -> exp -> exp

x / y -> BinOp(DIVIDE,x,y)

val (/$) : exp -> exp -> exp

x /$ y -> BinOp(SDIVIDE,x,y)

val (mod) : exp -> exp -> exp

x mod y -> BinOp (MOD,x,y)

val (%$) : exp -> exp -> exp

x %$ y -> BinOp (SMOD,x,y)

Bit operations

val (lsl) : exp -> exp -> exp

x lsl y = BinOp (LSHIFT,x,y)

val (lsr) : exp -> exp -> exp

x lsr y = BinOp (RSHIFT,x,y)

val (asr) : exp -> exp -> exp

x asr y = BinOp (ARSHIFT,x,y)

val (land) : exp -> exp -> exp

x land y = BinOp (AND,x,y)

val (lor) : exp -> exp -> exp

x lor y = BinOp (OR,x,y)

val (lxor) : exp -> exp -> exp

x lxor y = BinOp (XOR,x,y)

val lnot : exp -> exp

lnot x = UnOp (NOT,x,y)

Equality tests

val (=) : exp -> exp -> exp

x = y -> BinOp(EQ,x,y)

val (<>) : exp -> exp -> exp

x = y -> BinOp(NEQ,x,y)

val (<) : exp -> exp -> exp

x < y -> BinOp(LT,x,y)

val (>) : exp -> exp -> exp

x > y -> Binop(LT,y,x)

val (<=) : exp -> exp -> exp

x <= y -> Binop(LE,x,y)

val (>=) : exp -> exp -> exp

x <= y -> Binop(LE,y,x)

Signed comparison

val (<$) : exp -> exp -> exp

x <$ x -> Binop(SLT,x,y)

val (>$) : exp -> exp -> exp

x >$ x -> Binop(SLT,y,x)

val (<=$) : exp -> exp -> exp

x <=$ x -> Binop(SLE,x,y)

val (>=$) : exp -> exp -> exp

x >=$ x -> Binop(SLE,y,x)

Misc operations

val (^) : exp -> exp -> exp

a ^ b -> Concat (a,b)

Functional constructors

val move : var -> exp -> stmt

move v x -> Move (v,x)

val jmp : exp -> stmt

jmp x -> Jmp x

val special : string -> stmt

special msg -> Special msg

val while_ : exp -> stmt list -> stmt

while_ cond stmts -> While (cond,stmts)

val if_ : exp -> stmt list -> stmt list -> stmt

if_ cond s1 s2 -> If(cond,s1,s2)

val cpuexn : int -> stmt

cpuexn number -> CpuExn number

val unsigned : cast

unsigned -> UNSIGNED

val signed : cast

signed -> SIGNED

val high : cast

high -> HIGH

val low : cast

low -> LOW

val plus : binop

plus -> PLUS

val minus : binop

minus -> MINUS

val times : binop

times -> TIMES

val divide : binop

divide -> DIVIDE

val sdivide : binop

sdivide -> SDIVIDE

val modulo : binop

modulo -> MOD

val smodulo : binop

smodulo -> SMOD

val lshift : binop

lshift -> LSHIFT

val rshift : binop

rshift -> RSHIFT

val arshift : binop

arshift -> ARSHIFT

val bit_and : binop

bit_and -> AND

val bit_or : binop

bit_or -> OR

val bit_xor : binop

bit_xor -> XOR

val eq : binop

eq -> EQ

val neq : binop

neq -> NEQ

val lt : binop

lt -> LT

val le : binop

le -> LE

val slt : binop

slt -> SLT

val sle : binop

sle -> SLE

val neg : unop

neg -> NEG

val not : unop

not -> NOT

val load : mem:exp -> addr:exp -> endian -> size -> exp

load ~mem ~addr endian size -> Load (mem,addr,endian,size)

val store : mem:exp -> addr:exp -> exp -> endian -> size -> exp

store ~mem ~addr exp endian size -> Store(mem,addr,endian,size)

val binop : binop -> exp -> exp -> exp

binop op x y -> BinOp(op,x,y)

val unop : unop -> exp -> exp

unop op x -> UnOp(op,x)

val var : var -> exp

var v -> Var v

val int : word -> exp

int w -> Int w

val cast : cast -> int -> exp -> exp

cast t w x -> Cast (t,w,x)

val let_ : var -> exp -> exp -> exp

let_ var value expr -> Let(var,value,expr)

val unknown : string -> typ -> exp

unknown msg typ -> Unknown(msg,typ)

val ite : if_:exp -> then_:exp -> else_:exp -> exp

ite ~if_:cond ~then_:e1 ~else_:e2 -> Ite (cond,e1,e2)

val extract : hi:int -> lo:int -> exp -> exp

extract ~hi ~lo x -> Extract (hi,lo,x)

val concat : exp -> exp -> exp

concat x y -> Concat (x,y)

BIL Helper functions

val is_referenced : var -> stmt list -> bool

is_referenced x p is true if x is referenced in some expression or statement in program p, before it is assigned.

val is_assigned : ?strict:bool -> var -> stmt list -> bool

is_assigned x p is true if there exists such Move statement, that x occurs on the left side of it. If strict is true, then only unconditional assignments are accounted. By default, strict is false

val prune_unreferenced : 
  ?such_that:(var -> bool) ->
  ?physicals:bool ->
  ?virtuals:bool ->
  stmt list ->
  stmt list

prune_unreferenced ?physicals ?virtuals ?such_that p remove all assignments to variables that are not used in the program p. This is a local optimization. The variable is unreferenced if it is not referenced in its lexical scope, or if it is referenced after the assignment. A variable is pruned only if it matches to one of the user specified kind, described below (no variable matches the default values, so by default nothing is pruned):

such_that matches a variable v for which such_that v is true;

physicals matches all physical variables (i.e., registers and memory locations). See Var.is_physical for more information. Note: passing true to this option is in general unsound, unless you're absolutely sure, that physical variables will not live out program p;

virtuals matches all virtual variables (i.e., such variables that were added to a program artificially and are not represented physically in a program). See Var.is_virtual for more information on virtual variables.

val normalize_negatives : stmt list -> stmt list

normalize_negatives p transform x + y to x - abs(y) if y < 0

val substitute : exp -> exp -> stmt list -> stmt list

substitute x y p substitutes each occurrence of expression x by expression y in program p. The mnemonic to remember the order is to recall the sed's s/in/out syntax.

val substitute_var : var -> exp -> stmt list -> stmt list

substitute_var x y p substitutes all free occurrences of variable x in program p by expression y. A variable is free if it is not bounded in a preceding statement or not bound with let expression.

val free_vars : stmt list -> vars

free_vars bil returns a set of free variables in program bil. Variable is considered free if it is not bound in a preceding statement or is not bound with let expression

val fold_consts : stmt list -> stmt list

fold_consts evaluates constant expressions and statements.

val fixpoint : (stmt list -> stmt list) -> stmt list -> stmt list

fixpoint f applies transformation f until fixpoint is reached. If the transformation orbit contains non-trivial cycles, then the transformation will stop at an arbitrary point of a cycle.

val propagate_consts : stmt list -> stmt list

propagate_consts bil propagates consts from their reaching definitions. The implementation computes reaching definition using inference style analysis, overapproximates while cycles (doesn't compute the meet-over-paths solution), and ignores memory locations.

since 1.5

val prune_dead_virtuals : stmt list -> stmt list

prune_dead_virtuals bil removes definitions of virtual variables that are not live in the provided bil program. We assume that virtual variables are used to represent temporaries, thus their removal is safe. The analysis over-approximates the while loops, and won't remove any definition that occurs in a while loop body, or which depends on it. The analysis doesn't track memory locations.

since 1.5

BIL Special values

The Special statement enables encoding of arbitrary semantics using encode attr values and decode attr to get the values back. The meaning of the attr and values is specific to the user domain.

Example, encode call "malloc", where call is the BIL attribute that denotes a call to a function. See call for more information.

module Attribute : sig ... end

BIL attributes.

val encode : 'a Attribute.t -> 'a -> stmt

encode attr value encodes value as a special statement.

since 2.3.0

val decode : 'a Attribute.t -> stmt -> 'a option

decode attr s is Some v if s is encode attr v.

since 2.3.0

val call : string Attribute.t

call is the attribute name for encoding calls.

since 2.3.0

val intrinsic : string Attribute.t

intrinsic is the attribute for intrinsic calls.

An intrinsic is a low-level, usually microarchitectural operation.

since 2.3.0

val label : string Attribute.t

label a named code location.

since 2.4.0

val goto : string Attribute.t

goto represents a control-flow transfer to a named label.

since 2.4.0

module Theory : sig ... end

Core Theory specification of BIL.

module Apply : sig ... end

Maps BIL operators to bitvectors.

type result

Result of a computation.

deprecated
Use the Primus Framework.

class type storage = object ... end

An interface to a memory storage.

module Storage : sig ... end

Predefined storage classes

type value =

| Imm of word
(*
immediate value
*)
| Mem of storage
(*
memory storage
*)
| Bot
(*
undefined value
*)

Value of a result. We slightly diverge from an operational semantics by allowing a user to provide its own storage implementation.

In operational semantics a storage is represented syntactically as

            v1 with [v2,ed] : nat <- v3,

where v1 may be either a Bot value, representing an empty memory (or an absence of knowledge), or another storage. So a well typed memory object is defined inductively as:

          Inductive memory :=
           | bot : memory
           | store : (mem : memory) (addr : value) (data : value).

That is equivalent to an assoc list. Although we provide an assoc list as storage variant (see Storage.linear), the default storage is implemented slightly more effective, and uses linear space and provides $log(N)$ lookup and update methods. Users are encouraged to provide more efficient storage implementations, for interpreters that rely heave on memory throughput.

deprecated
Use the Primus Framework

module Result : sig ... end

Result of computation.

module Trie : sig ... end

Tries on BIL.

type pass

val register_pass : ?desc:string -> string -> (t -> t) -> pass

register_pass ~desc name pass provides a pass to the BIL transformation pipeline. The BIL transformation pipeline is applied after the lifting procedure, i.e., it is embedded into each lift function of all Target modules. (You can selectively register passes based on architecture by subscribing to the Project.Info.arch variable). All passes that were in the selection provided to the select_passes are applied in the order of the selection until the fixed point is reached or a loop is detected. By default, no passes are selected. The bil plugin provides a user interface for passes selection, as well as some useful passes.

since 1.5

val select_passes : pass list -> unit

select_passes passes select the passes for the BIL transformation pipeline. See register_pass for more information about the BIL transformation pipeline.

since 1.5

val passes : unit -> pass list

passes () returns all currently registered passes.

since 1.5

module Pass : sig ... end

A BIL analysis pass