From 2d7c68c879829429cead4ad0bd4f63cee1b6f1de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Fri, 22 Nov 2024 14:56:59 +0100
Subject: [PATCH] [region] footprint: requested modifs
---
src/plugins/region/Region.ml | 6 +-----
src/plugins/region/Region.mli | 8 +------
src/plugins/region/memory.ml | 40 +++++++++++++++--------------------
src/plugins/region/memory.mli | 7 +-----
4 files changed, 20 insertions(+), 41 deletions(-)
diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index 13b4e0e96b3..2de827b21b9 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -52,8 +52,4 @@ 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
-
-
-module SNode = Memory.SNode
-
-let footprint m r : SNode.t = Memory.footprint m r
+let footprint = Memory.footprint
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index b47ad1a987a..0d60818d1b3 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -67,12 +67,6 @@ val node : map -> node -> node
(** Normalized list of nodes (normalized, uniques, sorted by id) *)
val nodes : map -> node list -> node list
-(** Node sets *)
-module SNode : sig
- val update_map : map -> unit
- include Set.S with type elt = node
-end
-
(** {2 Region Properties}
All functions in this section provide normalized nodes
@@ -144,4 +138,4 @@ val field : map -> node -> fieldinfo -> node
val index : map -> node -> typ -> node
(** Unormalized. *)
-val footprint : map -> node -> SNode.t
+val footprint : map -> node -> node list
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index e6506aedefa..fb6df27c6e5 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -180,17 +180,10 @@ let update (m: map) (n: node) (f: chunk -> chunk) =
(* --- Nodes Set --- *)
(* -------------------------------------------------------------------------- *)
-module SNode = struct
- let map : map ref = ref (create ())
- let update_map m = map := m
-
- include Set.Make(struct
- type t = node
- let compare r1 r2 =
- if equal !map r1 r2 then 0
- else id (node !map r1) - id (node !map r2)
- end)
-end
+module SNode = Set.Make(struct
+ type t = node
+ let compare r1 r2 = Int.compare (id r1) (id r2)
+ end)
(* -------------------------------------------------------------------------- *)
(* --- Chunk Constructors --- *)
@@ -473,19 +466,20 @@ let field (m: map) (r: node) (fd: fieldinfo) : node =
move m r p s
else r
-let footprint (m: map) (r: node) : SNode.t =
- SNode.update_map m ;
+let footprint (m: map) (r: node) : node list =
try
- let leafs = ref SNode.empty in
- let rec store_leafs (r: node) : unit =
- let rg = (* raises Not_found *) Ufind.get m.store r in
- match rg.clayout with
- | Blob | Cell (_,_) -> leafs := SNode.add r !leafs
- | Compound (_, _, range) ->
- Ranges.iter store_leafs range
- in store_leafs r ;
- !leafs
- with Not_found -> SNode.empty
+ let visited = ref SNode.empty (* set of visited&normalized nodes *) in
+ let leafs = ref [] (* lsit of leafs *) in
+ let rec visit (r: node) : unit =
+ let n = node m r in (* normalized node *)
+ if SNode.mem n !visited then () else
+ let _ = visited := SNode.add n !visited in
+ let rg = (* raises Not_found *) Ufind.get m.store n in
+ match rg.clayout with
+ | Compound (_, _, range) -> Ranges.iter visit range
+ | Blob | Cell (_,_) -> leafs := n :: !leafs
+ in visit r ; !leafs
+ with Not_found -> []
let index (m : map) (r: node) (ty:typ) : node =
move m r 0 (Cil.bitsSizeOf ty)
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index b2b99b5edda..58ef65cf88e 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -109,12 +109,7 @@ val ranges : map -> node -> range list
val points_to : map -> node -> node option
val pointed_by : map -> node -> node list
-module SNode : sig
- val update_map : map -> unit
- include Set.S with type elt = node
-end
-
-val footprint : map -> node -> SNode.t
+val footprint : map -> node -> node list
val included : map -> node -> node -> bool
val separated : map -> node -> node -> bool
--
GitLab