diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index f236171a3028096c948ed6c465f9bab4a979becd..f7b0628225193fc8fb2837dfe0d1925ce94a7423 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -36,12 +36,14 @@ let nodes = Memory.nodes
let equal = Memory.equal
let included = Memory.included
let separated = Memory.separated
+let singleton = Memory.singleton
let size = Memory.size
let roots = Memory.roots
let labels = Memory.labels
let reads = Memory.reads
let writes = Memory.writes
let shifts = Memory.shifts
+let typed = Memory.typed
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
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index c17d49d53195ff92cb7185c9d0118f1d2a898759..46e3997e0d8e2c8d3e72a5c19dcfbfafa1c6fb85 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -82,6 +82,10 @@ 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 typed : map -> node -> typ option
+(** Full-sized cells with unique type access *)
+
val iter : map -> (node -> unit) -> unit
(** {2 Alias Analysis} *)
@@ -101,6 +105,11 @@ val included : map -> node -> node -> bool
*)
val separated : map -> node -> node -> bool
+
+(** [singleton m a] returns [true] when node [a] is guaranteed to have only
+ one single address in its equivalence class. *)
+val singleton : map -> node -> bool
+
(** [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 *)
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 1a51e063d1a6ac70f11c147d11d4294039137c95..c9c75368a2f3d5f72a2cca07cc06b09aa7b230b5 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -630,16 +630,55 @@ let included map source target : bool =
let separated map r1 r2 =
not (included map r1 r2) && not (included map r2 r1)
+let single_path m r0 r s =
+ match (Ufind.get m.store r0).clayout with
+ | Blob -> true
+ | Cell(s0,_) -> s = s0
+ | Compound(_,_,R rgs) ->
+ List.for_all
+ (fun (rg : node Ranges.range) ->
+ not (Ufind.eq m.store r rg.data) || rg.length = s
+ ) rgs
+
+let rec singleton m r =
+ let node = Ufind.get m.store r in
+ (* normalized parents *)
+ match nodes m node.cparents with
+ | [] -> Vset.cardinal node.croots = 1
+ | [r0] ->
+ Vset.is_empty node.croots &&
+ single_path m r0 r (sizeof node.clayout) &&
+ singleton m r0
+ | _ -> false
+
(* -------------------------------------------------------------------------- *)
-let reads (m : map) (r:node) =
+let reads (m:map) (r:node) =
let node = Ufind.get m.store r in
List.map Access.typeof @@ Access.Set.elements node.creads
-let writes (m : map) (r:node) =
+let writes (m:map) (r:node) =
let node = Ufind.get m.store r in
List.map Access.typeof @@ Access.Set.elements node.cwrites
-let shifts (m : map) (r:node) =
+let shifts (m:map) (r:node) =
let node = Ufind.get m.store r in
List.map Access.typeof @@ Access.Set.elements node.cshifts
+
+let typed (m:map) (r:node) =
+ let types = ref None in
+ let node = Ufind.get m.store r in
+ let size = sizeof node.clayout in
+ try
+ let check acs =
+ let t = Access.typeof acs in
+ if Cil.bitsSizeOf t > size then raise Exit ;
+ match !types with
+ | None -> types := Some t
+ | Some t0 -> if not @@ Cil_datatype.Typ.equal t0 t then raise Exit
+ in
+ Access.Set.iter check node.creads ;
+ Access.Set.iter check node.cwrites ;
+ Access.Set.iter check node.cshifts ;
+ !types
+ with Exit -> None
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 5485a5c974f8b2fae7c525d2077d0ab0a246c5d3..ea7949d6ed68e8dec78a71b7799140cf93534367 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -105,7 +105,9 @@ val pointed_by : map -> node -> node list
val included : map -> node -> node -> bool
val separated : map -> node -> node -> bool
+val singleton : map -> node -> bool
val reads : map -> node -> typ list
val writes : map -> node -> typ list
val shifts : map -> node -> typ list
+val typed : map -> node -> typ option
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index aa173e616e704583942284c957949188fdc2e7ee..008824f22d3745c7d4ae35baaa1d7967ffbd2892 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -46,50 +46,33 @@ struct
let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
end
-let types map r =
- let module Tset = Cil_datatype.Typ.Set in
- let pool = ref Tset.empty in
- let add ty = pool := Tset.add ty !pool in
- List.iter add @@ Region.reads map r ;
- List.iter add @@ Region.writes map r ;
- List.iter add @@ Region.shifts map r ;
- Tset.elements !pool
-
-let rec singleton map r =
- match Region.parents map r with
- | [] -> List.length @@ Region.roots map r = 1
- | [r] -> Region.roots map r = [] && singleton map r
- | _ -> false
-
(* Keeping track of the decision to apply which memory model to each region *)
module Kind = WpContext.Generator(Type)
(struct
- (* Data : WpContext.Data with type key = Key.t *)
- type key = region
- type data = MemRegion.kind
+ open MemRegion
let name = "Wp.RegionAnalysis.Kind"
+ type key = region
+ type data = kind
+ let kind map r p = if Region.singleton map r then Single p else Many p
let compile r =
- let open MemRegion in
let map = get_map () in
- match types map r with
- | [ty] when Cil.bitsSizeOf ty >= Region.size map r ->
+ match Region.typed map r with
+ | Some ty ->
begin
- let pkind p = if singleton map r then Single p else Many p in
match Ctypes.object_of ty with
- | C_int i -> pkind (Int i)
- | C_float f -> pkind (Float f)
- | C_pointer _ -> pkind Ptr
+ | C_int i -> kind map r (Int i)
+ | C_float f -> kind map r (Float f)
+ | C_pointer _ -> kind map r Ptr
| _ -> Garbled
end
- | _ -> Garbled
+ | None -> Garbled
end)
module Name = WpContext.Generator(Type)
(struct
- (* Data : WpContext.Data with type key = Key.t *)
+ let name = "Wp.RegionAnalysis.Name"
type key = region
type data = string option
- let name = "Wp.RegionAnalysis.Name"
let compile r =
let map = get_map () in
match Region.labels map r with