[region] compute singleton & typed

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

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

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

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

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