diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index fe4352cc959f36b1c87ef12f103476dbd992e1d7..b16d41ed66f3665af3b98c7c2296825a839aed73 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -27,118 +27,232 @@
open Cil_types
-type region = Memory.region
-module R : Qed.Collection.S with type t = region =
- Qed.Collection.Make(struct
- type t = region
- let hash r = Memory.id r.Memory.node
- let equal r1 r2 = (hash r1 == hash r2)
- let compare r1 r2 = (hash r1) - (hash r2)
- end)
+module Node = struct
+ type node = Memory.node
+ type map = Code.domain
-type map = Code.domain
+ (* API GETTERS *)
+ let get_map (f:kernel_function) : map = Code.domain f
-(* API GETTERS *)
-let get_map (f:kernel_function) : map = Code.domain f
+ let get_id map node = Memory.id (Memory.node map.Code.map node)
+ let get_node map id = Memory.node map.Code.map @@ Memory.forge id
-let get_id _map region = Memory.id region.Memory.node
-let get_region map id =
- try Some (Memory.region map.Code.map @@ Memory.forge id)
- with Not_found -> None
+ let cvar (map:map) (var:varinfo) =
+ Memory.node map.Code.map (Memory.lval map.Code.map ((Var var), NoOffset))
+ let field (map:map) (node:node) (field:fieldinfo) =
+ Memory.node map.Code.map
+ @@ Memory.offset map.Code.map node (Field (field, NoOffset))
-let cvar (map:map) (var:varinfo) =
- try Some (Memory.region map.Code.map (Memory.lval map.Code.map ((Var var), NoOffset)))
- with Not_found -> None
+ let shift (_map:map) node (_ty:typ) = (* TODO *) node
-let field (map:map) (region:region) (field:fieldinfo) =
- try Some (Memory.region map.Code.map (Memory.offset map.Code.map region.node (Field (field, NoOffset))))
- with Not_found -> None
-let shift (_map:map) region (_ty:typ) = (* TODO *)
- try Some region
- with Not_found -> None
+ let base_addr _map node = (* TODO *) node
-let base_addr _map region = (* TODO *) region
+ (* API POINTERS *)
+ let points_to (map:map) (node:node) : node option =
+ Option.map (Memory.node map.Code.map)
+ @@ Memory.cpointed map.map node
+ let pointed_by (map:map) (node:node) : node list =
+ List.map (Memory.node map.Code.map)
+ @@ Memory.cpointed_by map.Code.map node
-(* API POINTERS *)
-let points_to (map:map) (region:region) : region option =
- Option.map (Memory.region map.Code.map) @@ Memory.cpointed map.map region.Memory.node
-let pointed_by (map:map) (region:region) : region list =
- List.map (Memory.region map.Code.map) @@ Memory.cpointed_by map.Code.map region.Memory.node
+ (* COMPARATOR *)
+ let equal map r1 r2 = Memory.eq_node map.Code.map r1 r2
-(* COMPARATOR *)
-let equal map r1 r2 = get_id map r1 == get_id map r2
+ module Reachable = struct
+ module Imap = Map.Make(Int)
-module Reachable = struct
+ let is_reachable map source target : bool =
+ let q = Queue.create () in
+ let exception Reached in
+ try
+ let push r =
+ if equal map target r then raise Reached else Queue.push r q
+ in
+ push source ;
+ let visited = ref Imap.empty in
+ while true do (*not !accessible && not @@ Queue.is_empty q do *)
+ let node = Queue.pop q in
+ if equal map target node then raise Exit else
+ if not @@ Imap.mem (get_id map node) !visited then begin
+ visited := Imap.add (get_id map node) node !visited ;
+ List.iter push (Memory.parents map.Code.map node)
+ end
+ done ;
+ false
+ with
+ | Queue.Empty -> false
+ | Reached -> true
- module Imap = Map.Make(Int)
+ end
- let is_reachable map source target =
- let accessible = ref false in
- let q = Queue.create () in
- Queue.push source q ;
- let visited = ref Imap.empty in
- while not !accessible && not @@ Queue.is_empty q do
- let region = Queue.pop q in
- if not @@ Imap.mem (get_id map region) !visited then begin
- visited := Imap.add (get_id map region) region !visited ;
- List.iter (fun r -> Queue.push (Memory.region map r) q) region.Memory.parents ;
- accessible := equal map target region ;
- end
- done;
- !accessible
+ let included map r1 r2 : bool = Reachable.is_reachable map r1 r2
+
+ let separated map r1 r2 =
+ not (Reachable.is_reachable map r1 r2)
+ && not (Reachable.is_reachable map r2 r1)
+
+
+
+ (* API ITERATOR *)
+ let iter (map:map) (f:node -> unit) : unit =
+ Memory.iter_node map.map f
+
+
+ (* API PRINTER *)
+ let pp_node fmt node : unit = Memory.pp_node fmt node
+
+
+
+
+ (* API ACCESS *)
+ type acs = {
+ acs_read : typ list;
+ acs_write : typ list;
+ acs_shift : typ list;
+ }
+ let empty_acs = {
+ acs_read = [];
+ acs_write = [];
+ acs_shift = [];
+ }
+
+ let accesses (m: map) (r:node) : acs =
+ let acs_read, acs_write, acs_shift = Memory.accesses m.Code.map r in
+ { acs_read ; acs_write ; acs_shift }
end
-let included map r1 r2 : bool = Reachable.is_reachable map.Code.map r1 r2
+
+module Region = struct
+ type region = Memory.region
+
+
+ type map = Code.domain
+
+
+
+ (* API GETTERS *)
+ let get_map (f:kernel_function) : map = Code.domain f
+
+
+
+ let get_id map region = Node.get_id map region.Memory.node
+ let get_region map id =
+ try Some (Memory.region map.Code.map @@ Node.get_node map id)
+ with Not_found -> None
-let separated map r1 r2 =
- not (Reachable.is_reachable map.Code.map r1 r2)
- && not (Reachable.is_reachable map.Code.map r2 r1)
+ let cvar (map:map) (var:varinfo) =
+ try Some (Memory.region map.Code.map @@ Node.cvar map var)
+ with Not_found -> None
+ let field (map:map) (region:region) (field:fieldinfo) =
+ try Some (Memory.region map.Code.map @@ Node.field map region.Memory.node field)
+ with Not_found -> None
-(* API ITERATOR *)
-let iter (map:map) (f:region -> unit) : unit =
- Memory.iter map.map f
+ let shift (map:map) region (ty:typ) = (* TODO *)
+ try Some (Memory.region map.Code.map @@ Node.shift map region.Memory.node ty)
+ with Not_found -> None
-(* API PRINTER *)
-let pp_region fmt region : unit = Memory.pp_region fmt region
+ let base_addr _map region = (* TODO *) region
+ (* API POINTERS *)
+ let points_to (map:map) (region:region) : region option =
+ Option.map (Memory.region map.Code.map)
+ @@ Memory.cpointed map.map region.Memory.node
-(* API ACCESS *)
-type acs = {
- acs_read : typ list;
- acs_write : typ list;
- acs_shift : typ list;
-}
-let empty_acs = {
- acs_read = [];
- acs_write = [];
- acs_shift = [];
-}
+ let pointed_by (map:map) (region:region) : region list =
+ List.map (Memory.region map.Code.map)
+ @@ Memory.cpointed_by map.Code.map region.Memory.node
-let accesses (region:region) : acs =
- {
- acs_read = List.map Access.typeof region.Memory.reads ;
- acs_write = List.map Access.typeof region.Memory.writes ;
- acs_shift = List.map Access.typeof region.Memory.shifts ;
+
+ (* COMPARATOR *)
+ let equal map r1 r2 = Node.equal map r1.Memory.node r2.Memory.node
+
+
+ module Reachable = struct
+
+ module Imap = Map.Make(Int)
+
+ let is_reachable map source target : bool =
+ let q = Queue.create () in
+ let exception Reached in
+ try
+ let push r =
+ if equal map target r then raise Reached else Queue.push r q
+ in
+ push source ;
+ let visited = ref Imap.empty in
+ while true do (*not !accessible && not @@ Queue.is_empty q do *)
+ let region = Queue.pop q in
+ if equal map target region then raise Exit else
+ if not @@ Imap.mem (get_id map region) !visited then begin
+ visited := Imap.add (get_id map region) region !visited ;
+ List.iter (fun r -> push (Memory.region map.Code.map r)) region.Memory.parents
+ end
+ done ;
+ false
+ with
+ | Queue.Empty -> false
+ | Reached -> true
+
+ end
+
+ let included map r1 r2 : bool = Reachable.is_reachable map r1 r2
+
+
+ let separated map r1 r2 =
+ not (Reachable.is_reachable map r1 r2)
+ && not (Reachable.is_reachable map r2 r1)
+
+
+
+ (* API ITERATOR *)
+ let iter (map:map) (f:region -> unit) : unit =
+ Memory.iter map.map f
+
+
+ (* API PRINTER *)
+ let pp_region fmt region : unit = Memory.pp_region fmt region
+
+
+
+
+ (* API ACCESS *)
+ type acs = {
+ acs_read : typ list;
+ acs_write : typ list;
+ acs_shift : typ list;
+ }
+ let empty_acs = {
+ acs_read = [];
+ acs_write = [];
+ acs_shift = [];
}
+
+ let accesses (region:region) : acs =
+ {
+ acs_read = List.map Access.typeof region.Memory.reads ;
+ acs_write = List.map Access.typeof region.Memory.writes ;
+ acs_shift = List.map Access.typeof region.Memory.shifts ;
+ }
+end
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index 2382e98dc2c239fe8c65d1ebfdf49999e49af7df..8630768bdae1d984baee2740a27002d0313abe6a 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -26,47 +26,99 @@
open Cil_types
+(* Lower level API - more efficient *)
+module Node : sig
+ (* General type *)
+ type node
+ type map
+
+ (* API GETTERS *)
+ val get_map : kernel_function -> map
+
+ val get_id : map -> node -> int
+ val get_node : map -> int -> node
+
+ val cvar : map -> varinfo -> node
+ val field : map -> node -> fieldinfo -> node
+ val shift : map -> node -> typ -> node
+
+ val base_addr : map -> node -> node
+
+
+ (* API POINTERS *)
+ val points_to : map -> node -> node option
+ val pointed_by : map -> node -> node list
+
+
+ (* COMPARATOR *)
+ val separated : map -> node -> node -> bool
+ val included : map -> node -> node -> bool
+ val equal : map -> node -> node -> bool
+
+ (* API ITERATOR *)
+ val iter : map -> (node -> unit) -> unit
+
+
+ (* API PRINTER *)
+ val pp_node : Format.formatter -> node -> unit
+
+
+ (* API ACCESS *)
+ type acs = {
+ acs_read : typ list;
+ acs_write : typ list;
+ acs_shift : typ list;
+ }
+ val empty_acs : acs
+ val accesses : map -> node -> acs
+end
+
+
+
+
+(* High level API *)
+module Region : sig
(* General type *)
-type region
-module R : Qed.Collection.S with type t = region
-type map
+ type region
+ type map
-(* API GETTERS *)
-val get_map : kernel_function -> map
+ (* API GETTERS *)
+ val get_map : kernel_function -> map
-val get_id : map -> region -> int
-val get_region : map -> int -> region option
+ val get_id : map -> region -> int
+ val get_region : map -> int -> region option
-val cvar : map -> varinfo -> region option
-val field : map -> region -> fieldinfo -> region option
-val shift : map -> region -> typ -> region option
+ val cvar : map -> varinfo -> region option
+ val field : map -> region -> fieldinfo -> region option
+ val shift : map -> region -> typ -> region option
-val base_addr : map -> region -> region
+ val base_addr : map -> region -> region
-(* API POINTERS *)
-val points_to : map -> region -> region option
-val pointed_by : map -> region -> region list
+ (* API POINTERS *)
+ val points_to : map -> region -> region option
+ val pointed_by : map -> region -> region list
-(* COMPARATOR *)
-val separated : map -> region -> region -> bool
-val included : map -> region -> region -> bool
-val equal : map -> region -> region -> bool
+ (* COMPARATOR *)
+ val separated : map -> region -> region -> bool
+ val included : map -> region -> region -> bool
+ val equal : map -> region -> region -> bool
-(* API ITERATOR *)
-val iter : map -> (region -> unit) -> unit
+ (* API ITERATOR *)
+ val iter : map -> (region -> unit) -> unit
-(* API PRINTER *)
-val pp_region : Format.formatter -> region -> unit
+ (* API PRINTER *)
+ val pp_region : Format.formatter -> region -> unit
-(* API ACCESS *)
-type acs = {
- acs_read : typ list;
- acs_write : typ list;
- acs_shift : typ list;
-}
-val empty_acs : acs
-val accesses : region -> acs
+ (* API ACCESS *)
+ type acs = {
+ acs_read : typ list;
+ acs_write : typ list;
+ acs_shift : typ list;
+ }
+ val empty_acs : acs
+ val accesses : region -> acs
+end
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 75e38fe59f741ce83d5372aa25de9312107470a2..99689473aa6378639597b8926bb6343c2a131695 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -344,11 +344,32 @@ let iter (m:map) (f: region -> 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) ;
List.rev !pool
+
+let parents (m: map) (r: node) =
+ let node = Ufind.get m.store r in
+ nodes m node.cparents
+
(* -------------------------------------------------------------------------- *)
(* --- Merge --- *)
(* -------------------------------------------------------------------------- *)
@@ -535,13 +556,27 @@ let cpointed_by m r =
let rg = Ufind.get m.store r in
rg.cpointed_by
+let cvar (m: map) (v: varinfo) : node =
+ Ufind.find m.store @@ Vmap.find v m.roots
+
+let field (m: map) (r: node) (fd: fieldinfo) : node =
+ if fd.fcomp.cstruct then
+ let _, rgs = cranges m r in
+ let (p,w) = Cil.fieldBitsOffset fd in
+ let rg = Ranges.find p rgs in
+ if rg.offset <= p && p+w <= rg.offset + rg.length then
+ Ufind.find m.store rg.data
+ else raise Not_found
+ else r
+
+
let rec lval (m: map) (lv: lval) : node =
let h = host m (fst lv) in
offset m h (snd lv)
and host (m: map) (h: lhost) : node =
match h with
- | Var x -> Ufind.find m.store @@ Vmap.find x m.roots
+ | Var x -> cvar m x
| Mem e ->
match exp m e with
| None -> raise Not_found
@@ -551,13 +586,7 @@ and offset (m: map) (r: node) (ofs: offset) : node =
match ofs with
| NoOffset -> Ufind.find m.store r
| Field (fd, ofs) ->
- if fd.fcomp.cstruct then
- let _, rgs = cranges m r in
- let (p,w) = Cil.fieldBitsOffset fd in
- let rg = Ranges.find p rgs in
- if rg.offset <= p && p+w <= rg.offset + rg.length then
- offset m rg.data ofs
- else raise Not_found
+ if fd.fcomp.cstruct then offset m (field m r fd) ofs
else r
| Index (_, ofs) ->
let s, rgs = cranges m r in
@@ -577,3 +606,12 @@ and exp (m: map) (e: exp) : node option =
| UnOp (_, _, _) | BinOp (_, _, _, _) -> None
(* -------------------------------------------------------------------------- *)
+
+
+let eq_node (m: map) = Ufind.eq m.store
+
+let accesses (m : map) (r:node) =
+ let node = Ufind.get m.store r in
+ List.map Access.typeof @@ Access.Set.elements node.creads,
+ List.map Access.typeof @@ Access.Set.elements node.cwrites,
+ List.map Access.typeof @@ Access.Set.elements node.cshifts
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index e7679c176ebb9fb064217f3c9dcda0f27aac43d0..a9f9ac08fe8062cc57f147f265bf4bb01603728e 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -70,8 +70,10 @@ 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 region : map -> node -> region
val regions : map -> region list
+val parents : map -> node -> node list
val new_chunk : map -> ?size:int -> ?ptr:node -> ?ptrby:node -> unit -> node
val add_root : map -> Cil_types.varinfo -> node
@@ -97,3 +99,11 @@ val cpointed_by : map -> node -> node list
(** @raise Not_found *)
val exp : map -> exp -> node option
+
+(** @raise Not_found *)
+val field : map -> node -> fieldinfo -> node
+val cvar : map -> varinfo -> node
+
+val eq_node : map -> node -> node -> bool
+
+val accesses : map -> node -> typ list * typ list * typ list