Module Binsec.Smt_model

Internal model representation

Model types

type t
type address = Bitvector.t
type identifier = string
val empty : t

Constructors

Empty model. * *

val extract : Smtlib.model -> t

extract model extracts relevant information in SMT-LIB model concerning registers and memory values. This function takes into account the various "model dialects" spoken by:

  • Z3;
  • CVC4;
  • Boolector
val extract_value : ('a * Smtlib.constant) -> Bitvector.t

extract_value value extracts the value returned by (get-value) the same * way extract returns the model returned by (get-model). * This function currently only supports bitvectors

val yices_extract : string -> t

yices_extract s extracts the same information as extract but for a yices-smt2 produced model yices-smt2 models use another syntax and are parsed on their own s is expected to be the raw string of the model and not, for example, a filename

Create from scratch

val create : ?len:int -> unit -> t
val add_var : t -> string -> Bitvector.t -> unit
val add_memcell : t -> Bitvector.t -> Bitvector.t -> unit
val add_memory_term : t -> (Smtlib.term * Smtlib.term) list -> unit

Pretty-printer

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

Accessors

val find_variable : t -> identifier -> Bitvector.t option

find_register model name finds the bitvector value of register name in the model

val find_address_contents : t -> address -> Bitvector.t option

find_address_contents model addr find the (byte-sized) value of address addr from the model.

val find_address_content : t -> address -> Size.Byte.t -> Machine.endianness -> Bitvector.t option

Not yet implemented

val variables : t -> identifier list

get_register model gets the list of registers of this model

val memory_addresses : t -> address list

get_register model gets the list of addresses with specific values of this model

val memory_bindings : t -> (address * Bitvector.t) array

get_register model gets the list of pair address/value of this model

val is_memory_set : t -> address -> bool

is_memory_set model address checks if the given address is present in the memory of this model

val filter : ?keep_default:bool -> addr_p:(Bitvector.t -> bool) -> var_p:(string -> bool) -> t -> t

filter ?keep_default ~addr_p ~var_p model creates a new model m with the following properties:

  • m has the same default value for memory adresses than model if keep_default is true (default is false)
  • m keeps from model all addresses verifying the predicate addr_p and all the variable names verifying var_p