package bap-std

  1. Overview
  2. Docs
package bap-std
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 exp = Types.exp and type stmt = Types.stmt
type cast = Types.cast =
  1. | UNSIGNED
    (*

    0-padding widening cast.

    *)
  2. | SIGNED
    (*

    Sign-extending widening cast.

    *)
  3. | HIGH
    (*

    Narrowning cast. Keeps the high bits.

    *)
  4. | LOW
    (*

    Narrowing cast. Keeps the low bits.

    *)

Different forms of casting

include sig ... end
val cast_of_sexp : Sexplib.Sexp.t -> cast
val sexp_of_cast : cast -> Sexplib.Sexp.t
val compare_cast : cast -> cast -> int
val bin_cast : cast Core_kernel.Std.Bin_prot.Type_class.t
val bin_read_cast : cast Core_kernel.Std.Bin_prot.Read.reader
val __bin_read_cast__ : (int -> cast) Core_kernel.Std.Bin_prot.Read.reader
val bin_reader_cast : cast Core_kernel.Std.Bin_prot.Type_class.reader
val bin_size_cast : cast Core_kernel.Std.Bin_prot.Size.sizer
val bin_write_cast : cast Core_kernel.Std.Bin_prot.Write.writer
val bin_writer_cast : cast Core_kernel.Std.Bin_prot.Type_class.writer
type binop = Types.binop =
  1. | PLUS
    (*

    Integer addition. (commutative, associative)

    *)
  2. | MINUS
    (*

    Subtract second integer from first.

    *)
  3. | TIMES
    (*

    Integer multiplication. (commutative, associative)

    *)
  4. | DIVIDE
    (*

    Unsigned integer division.

    *)
  5. | SDIVIDE
    (*

    Signed integer division.

    *)
  6. | MOD
    (*

    Unsigned modulus.

    *)
  7. | SMOD
    (*

    Signed modulus.

    *)
  8. | LSHIFT
    (*

    Left shift.

    *)
  9. | RSHIFT
    (*

    Right shift, zero padding.

    *)
  10. | ARSHIFT
    (*

    Right shift, sign extend.

    *)
  11. | AND
    (*

    Bitwise and. (commutative, associative)

    *)
  12. | OR
    (*

    Bitwise or. (commutative, associative)

    *)
  13. | XOR
    (*

    Bitwise xor. (commutative, associative)

    *)
  14. | EQ
    (*

    Equals. (commutative) (associative on booleans)

    *)
  15. | NEQ
    (*

    Not equals. (commutative) (associative on booleans)

    *)
  16. | LT
    (*

    Unsigned less than.

    *)
  17. | LE
    (*

    Unsigned less than or equal to.

    *)
  18. | SLT
    (*

    Signed less than.

    *)
  19. | SLE
    (*

    Signed less than or equal to.

    *)

Binary operations implemented in the BIL

include sig ... end
val binop_of_sexp : Sexplib.Sexp.t -> binop
val sexp_of_binop : binop -> Sexplib.Sexp.t
val compare_binop : binop -> binop -> int
val bin_binop : binop Core_kernel.Std.Bin_prot.Type_class.t
val bin_read_binop : binop Core_kernel.Std.Bin_prot.Read.reader
val __bin_read_binop__ : (int -> binop) Core_kernel.Std.Bin_prot.Read.reader
val bin_reader_binop : binop Core_kernel.Std.Bin_prot.Type_class.reader
val bin_size_binop : binop Core_kernel.Std.Bin_prot.Size.sizer
val bin_write_binop : binop Core_kernel.Std.Bin_prot.Write.writer
val bin_writer_binop : binop Core_kernel.Std.Bin_prot.Type_class.writer
type unop = Types.unop =
  1. | NEG
    (*

    Negate. (2's complement)

    *)
  2. | NOT
    (*

    Bitwise not.(1's complement)

    *)

Unary operations implemented in the IR

include sig ... end
val unop_of_sexp : Sexplib.Sexp.t -> unop
val sexp_of_unop : unop -> Sexplib.Sexp.t
val compare_unop : unop -> unop -> int
val bin_unop : unop Core_kernel.Std.Bin_prot.Type_class.t
val bin_read_unop : unop Core_kernel.Std.Bin_prot.Read.reader
val __bin_read_unop__ : (int -> unop) Core_kernel.Std.Bin_prot.Read.reader
val bin_reader_unop : unop Core_kernel.Std.Bin_prot.Type_class.reader
val bin_size_unop : unop Core_kernel.Std.Bin_prot.Size.sizer
val bin_write_unop : unop Core_kernel.Std.Bin_prot.Write.writer
val bin_writer_unop : unop Core_kernel.Std.Bin_prot.Type_class.writer
type exp = Types.exp =
  1. | Load of exp * exp * endian * size
    (*

    load from memory

    *)
  2. | Store of exp * exp * exp * endian * size
    (*

    store to memory

    *)
  3. | BinOp of binop * exp * exp
    (*

    binary operation

    *)
  4. | UnOp of unop * exp
    (*

    unary operation

    *)
  5. | Var of var
    (*

    variable

    *)
  6. | Int of word
    (*

    immediate value

    *)
  7. | Cast of cast * int * exp
    (*

    casting

    *)
  8. | Let of var * exp * exp
    (*

    let-binding

    *)
  9. | Unknown of string * typ
    (*

    unknown or undefined value

    *)
  10. | Ite of exp * exp * exp
    (*

    if-then-else expression

    *)
  11. | Extract of int * int * exp
    (*

    extract portion of word

    *)
  12. | Concat of exp * exp
    (*

    concatenate two words

    *)

BIL expression variants

include sig ... end
val exp_of_sexp : Sexplib.Sexp.t -> exp
val sexp_of_exp : exp -> Sexplib.Sexp.t
val compare_exp : exp -> exp -> int
val bin_exp : exp Core_kernel.Std.Bin_prot.Type_class.t
val bin_read_exp : exp Core_kernel.Std.Bin_prot.Read.reader
val __bin_read_exp__ : (int -> exp) Core_kernel.Std.Bin_prot.Read.reader
val bin_reader_exp : exp Core_kernel.Std.Bin_prot.Type_class.reader
val bin_size_exp : exp Core_kernel.Std.Bin_prot.Size.sizer
val bin_write_exp : exp Core_kernel.Std.Bin_prot.Write.writer
val bin_writer_exp : exp Core_kernel.Std.Bin_prot.Type_class.writer
type stmt = Types.stmt =
  1. | Move of var * exp
    (*

    assign value of expression to variable

    *)
  2. | Jmp of exp
    (*

    jump to absolute address

    *)
  3. | Special of string
    (*

    Statement with semantics not expressible in BIL

    *)
  4. | While of exp * stmt list
    (*

    while loops

    *)
  5. | If of exp * stmt list * stmt list
    (*

    if/then/else statement

    *)
  6. | CpuExn of int
    (*

    CPU exception

    *)
include sig ... end
val stmt_of_sexp : Sexplib.Sexp.t -> stmt
val sexp_of_stmt : stmt -> Sexplib.Sexp.t
val compare_stmt : stmt -> stmt -> int
val bin_stmt : stmt Core_kernel.Std.Bin_prot.Type_class.t
val bin_read_stmt : stmt Core_kernel.Std.Bin_prot.Read.reader
val __bin_read_stmt__ : (int -> stmt) Core_kernel.Std.Bin_prot.Read.reader
val bin_reader_stmt : stmt Core_kernel.Std.Bin_prot.Type_class.reader
val bin_size_stmt : stmt Core_kernel.Std.Bin_prot.Size.sizer
val bin_write_stmt : stmt Core_kernel.Std.Bin_prot.Write.writer
val bin_writer_stmt : stmt Core_kernel.Std.Bin_prot.Type_class.writer
type t = stmt list
include sig ... end
val t_of_sexp : Sexplib.Sexp.t -> t
val sexp_of_t : t -> Sexplib.Sexp.t
val compare : t -> t -> int
val bin_t : t Core_kernel.Std.Bin_prot.Type_class.t
val bin_read_t : t Core_kernel.Std.Bin_prot.Read.reader
val __bin_read_t__ : (int -> t) Core_kernel.Std.Bin_prot.Read.reader
val bin_reader_t : t Core_kernel.Std.Bin_prot.Type_class.reader
val bin_size_t : t Core_kernel.Std.Bin_prot.Size.sizer
val bin_write_t : t Core_kernel.Std.Bin_prot.Write.writer
val bin_writer_t : t Core_kernel.Std.Bin_prot.Type_class.writer
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.Std.out_channel -> t -> unit
val pp_seq : Format.formatter -> t Core_kernel.Std.Sequence.t -> unit
val pp : Format.formatter -> 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.Std.bigstring -> t
val to_bigstring : ?ver:string -> ?fmt:string -> t -> Core_kernel.Std.bigstring
val blit_to_bigstring : ?ver:string -> ?fmt:string -> Core_kernel.Std.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
module Infix : sig ... end

Infix operators

Bring 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 occures 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 occurences 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 -> Var.Set.t

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 evaluate constant expressions. Note: this function performs only one step, and has no loops, it is supposed to be run using a fixpoint combinator.

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.

type result

Result of a computation.

class type storage = object ... end

An interface to a memory storage.

module Storage : sig ... end

Predefined storage classes

type value =
  1. | Imm of word
    (*

    immediate value

    *)
  2. | Mem of storage
    (*

    memory storage

    *)
  3. | 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.

module Result : sig ... end

Result of computation.

module Trie : sig ... end

Tries on BIL.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct