[region] documentation

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

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                                                              --- *)

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