package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module E.Path

type t

A path.

type state

A symbolic state (see State.S).

A symbolic state (see State.VALUE).

type model

A concrete assignment (see State.MODEL)

val id : t -> int

id p returns the unique identifier of the path p.

addr p returns the current program counter of the path p.

State update

val symbolize : t -> Binsec_kernel.Dba.Var.t -> unit

symbolize p v assigns the variable v with a new symbolic value.

Each call to symbolize records the new value on top of the symbols history.

assign p v e assigns the variable v with the expression e.

val clobber : t -> Binsec_kernel.Dba.Var.t -> unit

assign p v e assigns the variable v with a new symbolic value.

Clobbered variables are expected to not be used by the program and are not recorded in the symbols history.

load p v m ~addr d assigns the variable v with the bytes read at the address addr from the memory array m.

When m is None, the load is performed from the main memory @.

The bit size of v should be a multiple of the size of a byte (8). The byte order is determined by the endianness d.

val store : t -> string option -> addr:Binsec_kernel.Dba.Expr.t -> Binsec_kernel.Dba.Expr.t -> Binsec_kernel.Machine.endianness -> unit

store p m ~addr e d writes the expression e at the address addr in the memory array m.

When m is None, the write is performed in the main memory @.

The bit size of e should be a multiple of the size of a byte (8). The byte order is determined by the endianness d.

val memcpy : t -> string option -> addr:Binsec_kernel.Dba.Expr.t -> int -> Binsec_kernel.Loader_types.buffer -> unit

memcpy p m ~addr len content initializes the memory array m at the address addr with len bytes from the zero extended buffer content.

When m is None, the write is performed in the main memory @.

Predicate query

val predicate : t -> value list

predicate p returns the path predicate as a list of boolean value.

val is_symbolic : t -> Binsec_kernel.Dba.Expr.t -> bool

is_symbolic p e checks if the expression e may depend on symbolic values.

When it returns false, the path predicate of p implies that e has a single value. This value can be obtained via eval.

Otherwise, it means that e syntactically depends on a symbolic value. Use enumerate with n = 2 to prove or disprove that it can take several values.

is_zero p e checks if the boolean expression e may depend on symbolic values.

It returns True when the path predicate implies e is false and False when the path predicate implies e is true.

Otherwise, it returns Unknown, that means that e syntactically depends on a symbolic value. Use enumerate with n = 2 to prove or disprove that it can take several values.

val assume : t -> Binsec_kernel.Dba.Expr.t -> model option

assume p e tests if the condition e can be true. If so, it returns a witness model (Some) and updates the symbolic predicate. Otherwise, nothing is updated and it returns None.

  • raises State.Unknown

    when the symboloc engine fails to give an answer.

val check_sat_assuming : t -> ?retain:bool -> Binsec_kernel.Dba.Expr.t -> model option

check_sat_assuming p ~retain e tests if the condition e can be true. If so, it returns a witness model (Some), otherwise, it returns None.

If retain is true (default), the model is saved into the path p.

  • raises State.Unknown

    when the symbolic engine fails to give an answer.

partition p e tests if the condition e can be true and update its internal symbolic state accordingly.

It returns True when the path predicate implies e is true and False when the path predicate implies e is false.

It returns Trueish when the path predicate allows e to be true but may allow false too, and Falsish when the path predicate allows e to be false but may allow true too. The returned state can be used to check the other assumption.

It returns Split when the path predicate allows e to be both true and false. The current path keeps models for which e evaluates to true (same as assume) while the returned state comes with a list of models for which e evaluates to false.

val enumerate : t -> ?retain:bool -> ?n:int -> ?accumulator:model Binsec_kernel.Bitvector.Map.t -> ?assuming:Binsec_kernel.Dba.Expr.t -> Binsec_kernel.Dba.Expr.t -> model Binsec_kernel.Bitvector.Map.t

enumerate p ~retain ~n ~accumulator ~assuming e lists the possible values of the expression e.

It returns a map of up to n new possible values that are not already present in accumulator, together with their respective model witnesses. When n is omitted, the enumeration is unbounded.

The new models satisfy the predicate assuming when present.

If retain is true (default), new models are saved into the path p.

  • raises State.Unknown

    when the symbolic engine fails to give an answer.

val check_model : t -> ?retain:bool -> model -> bool

check_model p ~retain m returns true if the model m is a witness for the path predicate of p.

If retain is true (default), the model is saved into the path p when the function returns true.

Evaluation

eval p e evaluates the expression e in the last witness model.

The returned values are consistent with each other as long as the witness model is not updated via assume, check_sat_assuming, enumerate, check_model or partition.

val get_value : t -> Binsec_kernel.Dba.Expr.t -> value

get_value p e evaluates the expression e to its symbolic value.

val lookup : t -> Binsec_kernel.Dba.Var.t -> value

lookup p v evaluates the content of the variable v to its symbolic value.

val read : t -> string option -> addr:Binsec_kernel.Dba.Expr.t -> int -> Binsec_kernel.Machine.endianness -> value

read p m ~addr n d reads the content of the memory array m at the address addr.

When m is None, the load is performed from the main memory.

Returns a value of n bytes. The byte order is determined by the endianness d.

symbols p returns the (reverse) history of symbols created by symbolize.

Custom storage

type 'a key

A key entry associated to a value of type 'a.

val get : t -> 'a key -> 'a

get p k returns the associated value of the key k.

val set : t -> 'a key -> 'a -> unit

set p k v replaces the associated value of the key k by v.

Second API (value)

val assign_v : t -> Binsec_kernel.Dba.Var.t -> value -> unit

Same as assign but with value input.

val load_v : t -> Binsec_kernel.Dba.Var.t -> string option -> addr:value -> Binsec_kernel.Machine.endianness -> unit

Same as load but with value input.

val store_v : t -> string option -> addr:value -> value -> Binsec_kernel.Machine.endianness -> unit

Same as store but with value input.

val memcpy_v : t -> string option -> addr:value -> int -> Binsec_kernel.Loader_types.buffer -> unit

Same as memcpy but with value input.

val is_symbolic_v : t -> value -> bool

Same as is_symbolic but with value input.

val is_zero_v : t -> value -> Binsec_symbolic.Path.trilean

Same as is_zero but with value input.

val assume_v : t -> value -> model option

Same as assume but with value input.

val check_sat_assuming_v : t -> ?retain:bool -> value -> model option

Same as check_sat_assuming_v but with value input.

val partition_v : t -> value -> (state, model) Binsec_symbolic.Path.partition

Same as partition but with value input.

val enumerate_v : t -> ?retain:bool -> ?n:int -> ?accumulator:model Binsec_kernel.Bitvector.Map.t -> ?assuming:value -> value -> model Binsec_kernel.Bitvector.Map.t

Same as enumerate but with value input.

val eval_v : t -> value -> Binsec_kernel.Bitvector.t

Same as eval but with value input.

val read_v : t -> string option -> addr:value -> int -> Binsec_kernel.Machine.endianness -> value

Same as read but with value input.

Direct manipulation (unsafe)

module Model : Binsec_symbolic.State.MODEL with type t = model and type value := value
module State : Binsec_symbolic.State.S with type t = state and type Value.t = value and type Model.t = model
val set_pc : t -> Binsec_kernel.Virtual_address.t -> unit

set_pc p v replaces the current program counter of p by v.

val models : t -> model list

models p returns the list of the witness models of p.

val set_models : t -> model list -> unit

set_models p l replaces the witness models of p by the ones in l.

Warning. It is the caller responsibility to ensure that l is non-empty and that each model in l is consistent with the current symbolic state state.

val state : t -> state

state p returns the symbolic state of p.

val set_state : t -> state -> unit

set_state p s replaces the symbolic state of p by s.

Warning. It is the caller responsibility to ensure that each model in models is consistent with the new symbolic state s.

val transform_state : t -> (state -> state) -> unit

transform_state p f is equivalent to set_state p (f (state p)).