diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli index e54782c9d8da43e61b74efe2449db39b03849a03..68c04c93ee0a56e85db49f7521231c011df0da71 100644 --- a/src/plugins/region/Region.mli +++ b/src/plugins/region/Region.mli @@ -20,36 +20,62 @@ (* *) (**************************************************************************) -(** Interface for the Region plug-in. *) +(** 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 {i 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. +*) open Cil_types -type node type map - +type node val get_map : kernel_function -> map val get_id : map -> node -> int val get_node : map -> int -> node +(** Normalize node *) val node : map -> node -> node + +(** Normalize set of nodes *) val nodes : map -> node list -> node list +(** Nodes are in the same region *) +val equal : map -> node -> node -> bool + +(** First belongs to last *) +val included : map -> node -> node -> bool + +(** Nodes can not be aliased *) +val separated : map -> node -> node -> bool + val cvar : map -> varinfo -> node val field : map -> node -> fieldinfo -> node val index : map -> node -> typ -> node +val lval : map -> lval -> node +val exp : map -> exp -> node option + val points_to : map -> node -> node option val pointed_by : map -> node -> node list +val parents : map -> node -> node list +val roots : map -> node -> varinfo list -val equal : map -> node -> node -> bool -val separated : map -> node -> node -> bool -val included : map -> node -> node -> bool - -val iter : map -> (node -> unit) -> unit +val iter : map -> (node -> unit) -> unit (** Iter over all regions *) val reads : map -> node -> typ list val writes : map -> node -> typ list val shifts : map -> node -> typ list - -val pp_node : Format.formatter -> node -> unit diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index 5e6f6c6e262c424bb3342390e8a1592edaaad1b5..2e500375c1477b1120217c34329a90e3a89e4960 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -370,8 +370,11 @@ let regions map = let parents (m: map) (r: node) = - let node = Ufind.get m.store r in - nodes m node.cparents + let chunk = Ufind.get m.store r in + nodes m chunk.cparents + +let roots (m: map) (r: node) = + let chunk = Ufind.get m.store r in Vset.elements chunk.croots (* -------------------------------------------------------------------------- *) (* --- Merge --- *) diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli index cdd2ae7c65a10412209c06fbac7be8f736ffb30d..af3cd23eb708edc8f8bc11a89ee58c3abaea3ab3 100644 --- a/src/plugins/region/memory.mli +++ b/src/plugins/region/memory.mli @@ -75,6 +75,7 @@ val iter_node : map -> (node -> unit) -> unit val region : map -> node -> region val regions : map -> region list val parents : map -> node -> node list +val roots : map -> node -> varinfo list val new_chunk : map -> ?size:int -> ?ptr:node -> ?pointed:node -> unit -> node val add_root : map -> Cil_types.varinfo -> node