bap-std 2.2.0 · OCaml Package

Main BIL module.

The module specifies Binary Instruction Language (BIL). A language to define a semantics of instructions. The semantics of the BIL language is defined at [1].

The language is defined using algebraic types. For each BIL constructor a smart constructor is defined with the same (if syntax allows) name. This allows to use BIL as a DSL embedded into OCaml:

Bil.([
  v := src lsr i32 1;
  r := src;
  s := i32 31;
  while_ (var v <> i32 0) [
    r := var r lsl i32 1;
    r := var r lor (var v land i32 1);
    v := var v lsr i32 1;
    s := var s - i32 1;
  ];
  dst := var r lsl var s;
])

where i32 is defined as let i32 x = Bil.int (Word.of_int ~width:32 x) and v,r,s are some variables of type var; and src, dst are expressions of type exp.

@see <https://github.com/BinaryAnalysisPlatform/bil/releases/download/v0.1/bil.pdf> [1]: BIL Semantics.

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

val str : unit -> t -> string

val pps : unit -> t -> string

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

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

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

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

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

val version : string

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

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

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

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

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

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

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

module Io : sig ... end

module Cache : sig ... end

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

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

val available_readers : unit -> info list

val default_reader : unit -> info

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

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

val available_writers : unit -> info list

val default_writer : unit -> info

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

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

val default_printer : unit -> info option

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

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

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

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

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 BIL property

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

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

package bap-std