Legend:
Library
Module
Module type
Parameter
Class
Class type
Table.
Tables are used to partition memory region into a set of non-intersecting areas. Each area is associated with arbitrary value of type 'a bound to the type of the table.
All operations over tables are purely applicative, i.e. there is no observable side-effects. Although, they employ some kind of caching underneath the hood, so that they perform better if they're build once and used many times.
Tables can be also linked. For example, if you have two tables mapping the same memory region to a different sets of values, you can create a mapping from one set of values to another. See link function for mode details.
returns a new table with all mappings from the mem region mem removed
val change :
'at->mem->f:
((mem * 'a)seq->[ `rebind of mem * 'a| `update of (mem * 'a)->'a| `remove| `ignore ])->'at
change tab mem ~f function f is applied to a set of all memory regions that intersects with mem. If function f evaluates to `remap (new_mem,y) then all memory regions that have had intersections with mem will be removed from the new map and memory region new_mem will be mapped to y. If f evaluates to `remove, then the regions will be removed, and nothing will be added. If it evaluates to `skip then the table will be returned unchanged. Intersections are passed sorted in an ascending order.
link relation t t1 t2 takes two tables and returns a mapping from elements of one table to elements of other table.
Parameter t specifies a hashable typeclass of the type 'a. If type 'a implements Hashable interface, then you can obtain it with hashable function, e.g. Int.hashable with return the appropriate type class. If 'a doesn't implement Hashable, then it can be implemented manually.
Relation specifies the multiplicity of the relation between entities from table t1 to entities from table t2, and is summarized below:
one_to_many means that a particular region from table t1 can span several memory regions from table t2. Example: segments to symbols relation.
one_to_one means that for each value of type 'a there is exactly one value of type 'b. This relation should be used with caution, since it is quantified over _all_ values of type 'a. Indeed, it should be used only for cases, when it can be guaranteed, that it is impossible to create such value of type 'b, that has no correspondence in table t2. Otherwise, one_to_maybe_one relation should be used. Example: llvm machine code to assembly string relation.
one_to_maybe_one means that for each value in table t1 there exists at most one value in table t2. Example: function to symbol relation.
Examples
let mc_of_insn = link one_to:one Insn.hashable insns mcs
let syms_of_sec = link one_to:many Sec.hashable secs syms
val link : one_to:('b, 'r)r->'ahashable->'at->'bt->'a->'r
rev_map arity t tab creates a reverse mapping from values of typeclass t stored in table tab to memory regions.
Note. not every mapping is reversible, for example, trying to obtain a reverse of surjective mapping as a one-to-one mapping will result in an error. But surjective mappings can be reversed using ~one_to:many mapping. A particular example of surjective mapping is symbol tables, in a case when functions can occupy several non-contiguous regions of memory.
For example, to create a mapping from a function symbol to sequence of memory regions with it code:
This section provides a common set of iterators. Note: name iterator is used in a functional meaning, i.e., an iterator is a function that takes a data structure and another function, and applies it to all elements in some manner.
All iterators share some common part of interface that was lifted to a 'a ranged type. When you see
('a t -> f:('a -> bool) -> bool) ranged
just mentally substitute it with:
?start -> ?until -> 'a t -> f:('a -> bool) -> bool.
In other words 'f ranged just prepends ?start -> ?until -> to function with type 'f (do not forget that 'f can be an arrow type).
start and until parameters narrows iteration to some subset of table. If they are unspecified then iteration would be performed on all table entries in an ascending order of addresses. If they are specified, then if start <= until, then iteration will be performed in the same order but on a specified subset. In the case, when start > until, iteration will be performed in a decreasing order.