package cbat-vsa

  1. Overview
  2. Docs

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 = {
  1. addr_width : int;
  2. addressable_width : int;
}
include Bap.Std.Value.S with type t := t
val __bin_read_t__ : (int -> t) Core_kernel.Std.Bin_prot.Read.reader
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