From f26fe75cd3deb9100b82ba2d87199d665e622fe2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 4 Oct 2024 11:06:52 +0200
Subject: [PATCH] [region] improved API

---
 src/plugins/region/Region.ml     | 33 +++++++++---
 src/plugins/region/Region.mli    | 93 +++++++++++++++++++++++---------
 src/plugins/region/analysis.ml   |  5 +-
 src/plugins/region/memory.ml     | 40 +++++---------
 src/plugins/region/memory.mli    |  4 +-
 src/plugins/wp/RegionAnalysis.ml | 14 ++---
 6 files changed, 119 insertions(+), 70 deletions(-)

diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index ff076f6d491..4c912d7a61b 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -24,11 +24,28 @@
 (* --- Region Analysis API                                                --- *)
 (* -------------------------------------------------------------------------- *)
 
-let get_map kf = (Code.domain kf).map
-let get_id n = Memory.id n
-let get_uid m n = Memory.id @@ Memory.node m n
-let get_node m id = Memory.node m @@ Memory.forge id
-
-include Memory
-
-let iter = Memory.iter_node
+type map = Memory.map
+type node = Memory.node
+let map kf = (Code.domain kf).map
+let id n = Memory.id n
+let uid m n = Memory.id @@ Memory.node m n
+let iter = Memory.iter
+let find m id = Memory.node m @@ Memory.forge id
+let node = Memory.node
+let nodes = Memory.nodes
+let equal = Memory.equal
+let included = Memory.included
+let separated = Memory.separated
+let roots = Memory.roots
+let labels = Memory.labels
+let reads = Memory.reads
+let writes = Memory.writes
+let shifts = Memory.shifts
+let parents m n = Memory.nodes m @@ Memory.parents m n
+let points_to m n = Option.map (Memory.node m) @@ Memory.points_to m n
+let pointed_by m n = Memory.nodes m @@ Memory.pointed_by m n
+let lval m l = Memory.node m @@ Memory.lval m l
+let exp m e = Option.map (Memory.node m) @@ Memory.exp m e
+let cvar = Memory.cvar
+let field = Memory.field
+let index = Memory.index
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index 77756abb09f..baedc6b4030 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Interface for the Region plug-in.
+(** {1 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
@@ -29,7 +29,7 @@
     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.
+        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
@@ -38,45 +38,90 @@
     a region.
 *)
 
-
 open Cil_types
 
+(** {2 Memory Maps and Nodes} *)
+
 type map
 type node
-val get_map : kernel_function -> map
-val get_id : node -> int
-val get_uid : map -> node -> int
-val get_node : map -> int -> node
+val map : kernel_function -> map
+
+(** Not normalized.
+    Two nodes in the same equivalence class may have different identifiers. *)
+val id : node -> int
+
+(** Unique id of normalized node.
+    This can be considered the unique identifier of the region equivalence
+    class. *)
+val uid : map -> node -> int
+
+(** Returns a normalized node.
+    @raises Not_found if not a valid node identifier. *)
+val find : map -> int -> node
 
-(** Normalize node *)
+(** Normalized node.
+    The returned node is the representative of the region equivalence class.
+    There is one unique representative per equivalence class. *)
 val node : map -> node -> node
 
-(** Normalize set of nodes *)
+(** Normalized list of nodes (normalized, uniques, sorted by id) *)
 val nodes : map -> node list -> node list
 
-(** Nodes are in the same region *)
+(** {2 Region Properties}
+
+    All functions in this section provide normalized nodes
+    and shall never raise exception. *)
+
+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 labels: map -> node -> string list
+val reads : map -> node -> typ list
+val writes : map -> node -> typ list
+val shifts : map -> node -> typ list
+val iter : map -> (node -> unit) -> unit
+
+(** {2 Alias Analysis} *)
+
+(** [equal m a b] checks if nodes [a] and [b] are in the same region. *)
 val equal : map -> node -> node -> bool
 
-(** First belongs to last *)
+(** [include m a b] checks if region [a] is a sub-region of [b] in map [m]. *)
 val included : map -> node -> node -> bool
 
-(** Nodes can not be aliased *)
+(** [separated m a b] checks if region [a] and region [b] are disjoint.
+    Disjoints regions [a] and [b] have the following properties:
+    - [a] is {i not} a sub-region of [b];
+    - [b] is {i not} a sub-region of [a];
+    - two l-values respectively localized in [a] and [b]
+      can {i never} 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
-
+(** [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 *)
 val lval : map -> lval -> node
+
+(** [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
+*)
 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
+(** {2 Low-level Navigation through Memory Maps}
 
-val iter : map -> (node -> unit) -> unit (** Iter over all regions *)
+    For optimized access, all the fonctions in this section return
+    unnormalized nodes and may raise [Not_found] for not localized routes. *)
 
-val reads : map -> node -> typ list
-val writes : map -> node -> typ list
-val shifts : map -> node -> typ list
+(** Unormalized. @raises Not_found *)
+val cvar : map -> varinfo -> node
+
+(** Unormalized. @raises Not_found *)
+val field : map -> node -> fieldinfo -> node
+
+(** Unormalized. @raises Not_found *)
+val index : map -> node -> typ -> node
diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
index b64c6571bc8..252bb026bd0 100644
--- a/src/plugins/region/analysis.ml
+++ b/src/plugins/region/analysis.ml
@@ -59,11 +59,12 @@ let get kf =
     Options.result "@[<v 2>Function %a:%t@]@."
       Kernel_function.pretty kf
       begin fun fmt ->
-        Memory.iter domain.map
+        List.iter
           begin fun r ->
             Format.pp_print_newline fmt () ;
             Memory.pp_region fmt r ;
-          end
+          end @@
+        Memory.regions domain.map
       end ;
     domain
 
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 2e500375c14..048e7ed6ee1 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -314,6 +314,8 @@ let make_range (m: map) fields Ranges.{ length ; offset ; data } : range =
   }
 
 let make_region (m: map) (n: node) (r: chunk) : region =
+  let types = types r in
+  let sizeof = sizeof r.clayout in
   let fields = fields r.clayout in
   {
     node = n ;
@@ -323,58 +325,42 @@ let make_region (m: map) (n: node) (r: chunk) : region =
     reads = Access.Set.elements r.creads ;
     writes = Access.Set.elements r.cwrites ;
     shifts = Access.Set.elements r.cshifts ;
-    types = types r ;
-    sizeof = sizeof r.clayout ;
-    fields ; ranges = List.map (make_range m fields) @@ ranges r.clayout ;
+    types ; sizeof ; fields ;
+    ranges = List.map (make_range m fields) (ranges r.clayout) ;
     pointed = Option.map (node m) (pointed r.clayout) ;
   }
 
 let region map n = make_region map n (get map n)
 
-let rec walk h m f n =
+let rec walk h m (f: node -> unit) n =
   let n = Ufind.find m.store n in
   let id = Store.id n in
   try Hashtbl.find h id with Not_found ->
     Hashtbl.add h id () ;
+    f n ;
     let r = Ufind.get m.store n in
-    f (make_region m n r) ;
     match r.clayout with
     | Blob -> ()
     | Cell(_,p) -> Option.iter (walk h m f) p
     | Compound(_,_,rg) -> Ranges.iter (walk h m f) rg
 
-let iter (m:map) (f: region -> unit) =
+let iter (m:map) (f: node -> unit) =
   let h = Hashtbl.create 0 in
   Vmap.iter (fun _x n -> walk h m f n) m.roots
 
-let rec walk_node h m (f: node -> unit) n =
-  let n = Ufind.find m.store n in
-  let id = Store.id n in
-  try Hashtbl.find h id with Not_found ->
-    Hashtbl.add h id () ;
-    f n ;
-    let r = Ufind.get m.store n in
-    match r.clayout with
-    | Blob -> ()
-    | Cell(_,p) -> Option.iter (walk_node h m f) p
-    | Compound(_,_,rg) -> Ranges.iter (walk_node h m f) rg
-
-let iter_node (m:map) (f: node -> unit) =
-  let h = Hashtbl.create 0 in
-  Vmap.iter (fun _x n -> walk_node h m f n) m.roots
-
 let regions map =
   let pool = ref [] in
-  iter map (fun r -> pool := r :: !pool) ;
+  iter map (fun r -> pool := region map r :: !pool) ;
   List.rev !pool
 
-
 let parents (m: map) (r: node) =
-  let chunk = Ufind.get m.store r in
-  nodes m chunk.cparents
+  nodes m (Ufind.get m.store r).cparents
 
 let roots (m: map) (r: node) =
-  let chunk = Ufind.get m.store r in Vset.elements chunk.croots
+  Vset.elements (Ufind.get m.store r).croots
+
+let labels (m: map) (r: node) =
+  Lset.elements (Ufind.get m.store r).clabels
 
 (* -------------------------------------------------------------------------- *)
 (* --- Merge                                                              --- *)
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index af3cd23eb70..4e8f5c4da4b 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -70,12 +70,12 @@ val equal : map -> node -> node -> bool
 val node : map -> node -> node
 val nodes : map -> node list -> node list
 
-val iter : map -> (region -> unit) -> unit
-val iter_node : map -> (node -> unit) -> unit
+val iter : 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 labels : map -> node -> string list
 
 val new_chunk : map -> ?size:int -> ?ptr:node -> ?pointed:node -> unit -> node
 val add_root : map -> Cil_types.varinfo -> node
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index 25811dce3fc..cb4b7e03ab2 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -74,7 +74,7 @@ struct
   type region = Region.node
 
   let get_map () = match WpContext.get_scope () with
-    | WpContext.Kf f   -> Region.get_map f
+    | WpContext.Kf f   -> Region.map f
     | WpContext.Global -> Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] get_map: No global region analysis yet"
 
   let null () : region =
@@ -83,19 +83,19 @@ struct
     Wp_parameters.not_yet_implemented "[WP/RegionAnalysis.ml] null: cannot create null region"
 
 
-  let id_of_region region = Region.get_uid (get_map ()) region
+  let id_of_region region = Region.uid (get_map ()) region
 
   let region_of_id id =
-    try Some (Region.get_node (get_map ()) id)
+    try Some (Region.find (get_map ()) id)
     with Not_found -> None
 
-  let hash = Region.get_id
+  let hash = Region.id
 
-  let equal r1 r2 = (Region.get_id r1 = Region.get_id r2)
+  let equal r1 r2 = (Region.id r1 = Region.id r2)
 
-  let compare r1 r2 = Int.compare (Region.get_id r1) (Region.get_id r2)
+  let compare r1 r2 = Int.compare (Region.id r1) (Region.id r2)
 
-  let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.get_id r
+  let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
 
   type primitive = | Int of c_int | Float of c_float | Ptr
   type kind = Single of primitive | Many of primitive | Garbled
-- 
GitLab