Module RegionSource

Interface for the Region plug-in

Each function is assigned a region map. Areas in the map represents l-values or, more generally, class of nodes. Regions are classes equivalences of nodes that represents a collection of addresses (at some program point).

Regions can be subdivided into sub-regions. Hence, given two regions, either one is included into the other, or they are separated. Hence, given two l-values, if their associated regions are separated, then they can not be aliased.

Nodes are elementary elements of a region map. Variables maps to nodes, and one can move to one node to another by struct or union field or array element. Two disting nodes might belong to the same region. However, it is possible to normalize nodes and obtain a unique identifier for all nodes in a region.

Memory Maps and Nodes

Sourcetype map
Sourcetype node
Sourceval id : node -> int

Not normalized. Two nodes in the same equivalence class may have different identifiers.

Sourceval uid : map -> node -> int

Unique id of normalized node. This can be considered the unique identifier of the region equivalence class.

Sourceval find : map -> int -> node

Returns a normalized node.

  • raises Not_found

    if not a valid node identifier.

Sourceval node : map -> node -> node

Normalized node. The returned node is the representative of the region equivalence class. There is one unique representative per equivalence class.

Sourceval nodes : map -> node list -> node list

Normalized list of nodes (normalized, uniques, sorted by id)

Region Properties

All functions in this section provide normalized nodes and shall never raise exception.

Sourceval points_to : map -> node -> node option
Sourceval pointed_by : map -> node -> node list
Sourceval size : map -> node -> int
Sourceval parents : map -> node -> node list
Sourceval labels : map -> node -> string list

Full-sized cells with unique type access

Sourceval iter : map -> (node -> unit) -> unit

Alias Analysis

Sourceval equal : map -> node -> node -> bool

equal m a b checks if nodes a and b are in the same region.

Sourceval included : map -> node -> node -> bool

include m a b checks if region a is a sub-region of b in map m.

Sourceval separated : map -> node -> node -> bool

separated m a b checks if region a and region b are disjoint. Disjoints regions a and b have the following properties:

  • a is not a sub-region of b;
  • b is not a sub-region of a;
  • two l-values respectively localized in a and b can never be aliased.
Sourceval singleton : map -> node -> bool

singleton m a returns true when node a is guaranteed to have only one single address in its equivalence class.

lval m lv is region where the address of l lives in. The returned region is normalized.

  • raises Not_found

    if the l-value is not localized in the map

exp m e is the domain of values that can computed by expression e. The domain is Some r is e has a pointer type and any pointer computed by e lives in region r. The domain is None if e has a non-pointer scalar or compound type.

  • raises Not_found

    if the l-value is not localized in the map

Low-level Navigation through Memory Maps

For optimized access, all the fonctions in this section return unnormalized nodes and may raise Not_found for not localized routes.

Unormalized.

Unormalized.

Unormalized.

Sourceval footprint : map -> node -> node list

Normalized list of leaf nodes.