package cbat-vsa

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

x17, 0x2e, 0x45
x5, 0x7, 0xe
x1, 0x2, 0x4
x1, 0x2, 0x3, 0x4
x15, 0x17, 0x1e, 0x25, 0x27, 0x2e, 0x35, 0x37, 0x3e, 0x45, 0x47, 0x4e

cbat-plugin-value-set
- Cbat_value_set_plugin
  - Cmdline
  - Config
cbat-value-set

Legend:
Library
Module
Module type
Parameter
Class
Class type

Cbat_ai_memmap Represents memory as an interval tree from ranges of addresses to CLPs with an endianness. Note that, while BAP breaks up its memory into constant size (usually 8-bit) regions, this module does not. This is because n*k-bit CLPs cannot be well-represented as k n-bit CLPs. For example, take the set

x17, 0x2e, 0x45

which can be represented exactly as a 3-element CLP with a constant step of 0x17. If we divide it into two 4-bit sets, we get

x5, 0x7, 0xe

for the lower bits and

x1, 0x2, 0x4

for the upper ones. However, this latter set cannot be represented by a CLP since it has a variable step. The closest approximation is

x1, 0x2, 0x3, 0x4

. We then lose even more precision when attempting to read back an 8-bit word from these 4-bit cells. Since it is no longer clear which element from the low set corresponds to each element from the high set, the best a general algorithm can do is to guess the following set:

x15, 0x17, 0x1e, 0x25, 0x27, 0x2e, 0x35, 0x37, 0x3e, 0x45, 0x47, 0x4e

Again, this set cannot be represented accurately by a CLP. The best we can do is the interval 0x15,0x4e which has cardinality 0x39 = 57, whereas our initial set had cardinality 3. Since fixed-size memory cells handle larger data so badly, this module attempts to keep data stored at the greatest bitwidth possible.

module WordSet = Cbat_clp_set_composite

module Key : sig ... end

module Val : sig ... end

type t

type idx = {

addr_width : int;
addressable_width : int;

}

include Bap.Std.Value.S with type t := t

val bin_t : t Core_kernel.Std.Bin_prot.Type_class.t

val bin_read_t : t Core_kernel.Std.Bin_prot.Read.reader

val __bin_read_t__ : (int -> t) Core_kernel.Std.Bin_prot.Read.reader

val bin_reader_t : t Core_kernel.Std.Bin_prot.Type_class.reader

val bin_size_t : t Core_kernel.Std.Bin_prot.Size.sizer

val bin_write_t : t Core_kernel.Std.Bin_prot.Write.writer

val bin_writer_t : t Core_kernel.Std.Bin_prot.Type_class.writer

val bin_shape_t : Core_kernel.Std.Bin_prot.Shape.t

val compare : t -> t -> int

val t_of_sexp : Sexplib.Sexp.t -> t

val sexp_of_t : t -> Sexplib.Sexp.t

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

include Cbat_map_lattice.S_indexed
  with module Val := Val
   and module Key := Key
   and type t := t
   and type idx := idx

val get_idx : t -> idx

val top : idx -> t

val bottom : idx -> t

val meet : t -> t -> t

val join : t -> t -> t

val widen_join : t -> t -> t

val precedes : t -> t -> bool

val equal : t -> t -> bool

val meet_add : t -> key:Key.t -> data:Val.t -> t

val join_add : t -> key:Key.t -> data:Val.t -> t

val add : t -> key:Key.t -> data:Val.t -> t

val find : Val.idx -> t -> Key.t -> Val.t