Parameter Run._

type t

A symbolic state.

include Binsec_symbolic.State.DATA with type t := t and type value := Value.t
val lookup : Binsec_kernel.Dba.Var.t -> t -> Value.t

lookup var s returns the value assigned to var in s.

  • raises Undefined

    if var is not in s.

val read : addr:Value.t -> int -> Binsec_kernel.Machine.endianness -> t -> Value.t * t

read ~addr len d s returns len bytes of the value stored at address addr in the main memory array @, together with the updated state s. The byte order is determined by the endianness d.

  • raises Undeclared

    None if there is no main memory in s (see S.declare).

val select : string -> addr:Value.t -> int -> Binsec_kernel.Machine.endianness -> t -> Value.t * t

select m ~addr len d s returns len bytes of the value stored at address addr in the memory array m, together with the updated state s. The byte order is determined by the endianness d.

  • raises Undeclared

    Some m if m is not in s (see S.declare).

val empty : unit -> t

empty creates an empty state.

val assign : Binsec_kernel.Dba.Var.t -> Value.t -> t -> t

assign var v s returns a copy of s with the value v assigned to the variable var.

val declare : array:string option -> int -> t -> t

declare ~array idx s returns a copy of s where array is a fresh mapping between addresses of idx bits to (first-order) constant.

The None represents the main memory @ (e.g. the RAM). The functions read and write operate on @.

The Some name represents a named array. The functions select and store operate on name.

val write : addr:Value.t -> Value.t -> Binsec_kernel.Machine.endianness -> t -> t

write ~addr v d s returns a copy of s where the value v is written at the address addr in the main memory. The byte order is determined by the endianness d.

  • raises Undeclared

    None if there is no main memory @ in s (see declare).

val store : string -> addr:Value.t -> Value.t -> Binsec_kernel.Machine.endianness -> t -> t

store m ~addr v s returns a copy of s where the value v is stored at the address addr in the memory array m. The byte order is determined by the endianness d.

  • raises Undeclared

    Some m if m is not in s (see declare).

val memcpy : string option -> addr:Value.t -> int -> Binsec_kernel.Loader_types.buffer -> t -> t

memcpy m ~addr len content s returns a copy of s where len bytes from the zero extended buffer content are copied to the memory array m at the address addr.

  • raises Undeclared

    m is not in s (see declare).

val merge : t -> t -> t

merge t1 t2 returns a new state with the values of both t1 and t2.

val assume : Value.t -> t -> t option

assume v s returns the a copy of the state s for which the boolean condition v has been added to the path predicate.

Returns None if the state s can infer that v always evaluates to false.

val predicate : t -> Value.t list

predicate s returns the state predicate as a list of value.

val is_symbolic : Value.t -> t -> bool

is_symbolic v s checks if the value v may depend on symbolic values.

is_zero v s checks if v may depend on symbolic values.

It returns True when the state implies v is false and False when the state implies v is true.

Otherwise, it returns !constructor-Unknown, that means that v syntactically depends on a symbolic value.

val check_sat : Cookie.t -> t -> Model.t option

check_sat c s returns a model that satisfies the predicate of s, using the configuration stored in the cookie c.

  • raises Unknown

    when no solution is found within the current resource budget (see SetSMTSolverTimeout).

val enumerate : Cookie.t -> Value.t -> ?except:Binsec_kernel.Bitvector.t list -> t -> Enumeration.t

enumerate c v ~except s returns a new enumeration for the value v, using the configuration stored in the cookie c.

The enumeration will not contain any Binsec_kernel.Bitvector present in except.

val print_smtlib : ?slice:(Value.t * string) list -> Format.formatter -> t -> unit

print_smtlib ~slice f s outputs the predicate of s in the SMTlib format in the formatter f.

If slice is given, it outputs the current mapping between values and name. Otherwise, it outputs the full mapping (variables and arrays) of s.

val pp : Format.formatter -> t -> unit

pp f s outputs the state s in the formatter f.

val more : (Value.t, t, Cookie.t, 'a) Binsec_symbolic.State.feature -> 'a option

more feature returns Some a value of type 'a; or None if the current implementation does not support the queried feature.