Module Path.MakeSource

Parameters

module _ : Metrics.S
module State : State.S

Signature

Main implementation of the signature S.

include S with type state = State.t and type value = State.Value.t and type model = State.Model.t and module State = State
Sourcetype t

A path.

Sourcetype state = State.t

A symbolic state (see State.S).

Sourcetype value = State.Value.t

A symbolic state (see State.VALUE).

Sourcetype model = State.Model.t

A concrete assignment (see State.MODEL)

Sourceval 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

Sourceval 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.

Sourceval 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.

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.

Sourceval 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

Sourceval predicate : t -> value list

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

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

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

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

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

Sourceval 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

Sourcetype 'a key

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

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

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

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

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

Second API (value)

Sourcemodule Value : State.VALUE with type t = value
Sourceval assign_v : t -> Binsec_kernel.Dba.Var.t -> value -> unit

Same as assign but with value input.

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

Same as load but with value input.

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

Same as store but with value input.

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

Same as memcpy but with value input.

Sourceval is_symbolic_v : t -> value -> bool

Same as is_symbolic but with value input.

Sourceval is_zero_v : t -> value -> trilean

Same as is_zero but with value input.

Sourceval assume_v : t -> value -> model option

Same as assume but with value input.

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

Same as check_sat_assuming_v but with value input.

Sourceval partition_v : t -> value -> (state, model) partition

Same as partition but with value input.

Sourceval 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.

Same as eval but with value input.

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

Same as read but with value input.

Direct manipulation (unsafe)

Sourcemodule Model : State.MODEL with type t = model and type value := value
Sourcemodule State = State

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

Sourceval models : t -> model list

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

Sourceval 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.

Sourceval state : t -> state

state p returns the symbolic state of p.

Sourceval 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.

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

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

cookie p returns the cookie of p (see State.COOKIE for more details).

Path extension

A path is a mutable table which maps typed keys to their values. Each instance of Make has its own set of keys. The current implementation requires that all keys be known (i.e. declare_field) before a path is created (create). A value can then be read with get and written with set.

Sourceval declare_field : ?copy:('a -> 'a) -> ?merge:('a -> 'a -> 'a option) -> 'a -> 'a key

declare_field ~copy ~merge default registers a new field with the initial value default, then returns the typed key to access it.

When given, the copy function will be called to initialize this field in the new path during fork.

When given, the merge function will be called to initialize this field in the new path during merge. Returning None prevents the paths to be merged.

Builder functions

Sourceval create : unit -> t

create () makes a path with all fields initialized with their default values.

Warning. It is an error to try adding more fields after calling this function.

Sourceval fork : t -> t

fork p returns a copy of p with a new identifier.

Fields are copied using the copy functions given via declare_field (default to Fun.id).

Sourceval merge : t -> t -> t option

merge p1 p2 tries to merge all the fields of p1 and p2 using the merge functions given via declare_field (default works only when values are physically equal). Returns None if any field fails to merge.