package binsec

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

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct