Module Formula.Model

Internal model representation

Model types

type t
type identifier = string
val empty : t

Constructors

Empty model.

val extract : Binsec_smtlib__.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 : Binsec_smtlib__.Smtlib.constant -> Binsec_base.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 -> Binsec_base.Bitvector.t -> unit
val add_memcell : t -> Binsec_base.Bitvector.t -> Binsec_base.Bitvector.t -> unit
val add_memory_term : t -> (Binsec_smtlib__.Smtlib.term * Binsec_smtlib__.Smtlib.term) list -> unit

Pretty-printer

val pp : Format.formatter -> t -> unit
val pp_with_sections : (Binsec_base.Virtual_address.t -> string option) -> Format.formatter -> t -> unit

Accessors

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

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

val find_address_contents : t -> address -> Binsec_base.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 -> Binsec_base.Size.Byte.t -> Binsec_base.Machine.endianness -> Binsec_base.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 * Binsec_base.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:(Binsec_base.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