diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml index 8d9d7f5ab5be0dbe7418a7151fc83b915376049e..9017bdeb5e771beaff7f609cf5206724f37dafb5 100644 --- a/src/plugins/region/Region.ml +++ b/src/plugins/region/Region.ml @@ -54,7 +54,9 @@ let index (_:map) (_:region) (_:typ) : region = (* TODO *) raise Not_found let points_to (map:map) (region:region) : region option = Option.map (Memory.region map.map) @@ Memory.cpointed map.map region.Memory.node -let pointed_by (_:map) (_:region) : region list = (* TODO *) [] +let pointed_by (map:map) (region:region) : region list = + List.map (Memory.region map.map) @@ Memory.cpointed_by map.map region.Memory.node -let iter (_:map) (_:region -> unit) : unit = (* TODO *) () +let iter (map:map) (f:region -> unit) : unit = + Memory.iter map.map f diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index e10914c98ebc6e5503c32ea4d5adc40d65b3a869..f21e7b3a523fe88a3edd0fff74641767800f035a 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -49,6 +49,7 @@ and chunk = { cwrites: Access.Set.t ; cshifts: Access.Set.t ; clayout: layout ; + cpointed_by : node list; } type rg = node Ranges.range @@ -149,6 +150,7 @@ let empty = { cwrites = Access.Set.empty ; cshifts = Access.Set.empty ; clayout = Blob ; + cpointed_by = [] ; } (* -------------------------------------------------------------------------- *) @@ -176,13 +178,17 @@ let update (m: map) (n: node) (f: chunk -> chunk) = (* --- Chunk Constructors --- *) (* -------------------------------------------------------------------------- *) -let new_chunk (m: map) ?(size=0) ?ptr () = +let new_chunk (m: map) ?(size=0) ?ptr ?ptrby () = failwith_locked m "Region.Memory.new_chunk" ; let clayout = match ptr with | None -> if size = 0 then Blob else Cell(size,None) | Some _ -> Cell(Ranges.gcd size (Cil.bitsSizeOf Cil_const.voidPtrType), ptr) - in Ufind.make m.store { empty with clayout } + in let cpointed_by = + match ptrby with + | None -> [] + | Some ptr -> [ptr] + in Ufind.make m.store { empty with clayout ; cpointed_by } let new_range (m: map) ?(fields=Fields.empty) ~size ~offset ~length data : node = failwith_locked m "Region.Memory.new_range" ; @@ -419,6 +425,7 @@ let merge_region (m: map) (q: queue) (a : chunk) (b : chunk) : chunk = { cwrites = Access.Set.union a.cwrites b.cwrites ; cshifts = Access.Set.union a.cshifts b.cshifts ; clayout = merge_layout m q a.clayout b.clayout ; + cpointed_by = List.append a.cpointed_by b.cpointed_by ; } let do_merge (m: map) (q: queue) (a: node) (b: node): unit = @@ -471,7 +478,7 @@ let add_index (m:map) (r:node) (ty:typ) (n:int) : node = let add_points_to (m: map) (a: node) (b : node) = failwith_locked m "Region.Memory.points_to" ; - ignore @@ merge m a @@ new_chunk m ~ptr:b () + ignore @@ merge m a @@ new_chunk m ~ptr:b ~ptrby:a () let add_value (m:map) (rv:node) (ty:typ) : node option = if Cil.isPointerType ty then @@ -524,6 +531,10 @@ let cpointed m r = | Blob | Compound _ | Cell(_,None) -> None | Cell(_,Some r) -> Some (Ufind.find m.store r) +let cpointed_by m r = + let rg = Ufind.get m.store r in + rg.cpointed_by + let rec lval (m: map) (lv: lval) : node = let h = host m (fst lv) in offset m h (snd lv) diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli index 4aab36af2c15eeb885575745ac413a3b4cbfa13d..e7679c176ebb9fb064217f3c9dcda0f27aac43d0 100644 --- a/src/plugins/region/memory.mli +++ b/src/plugins/region/memory.mli @@ -73,7 +73,7 @@ val iter : map -> (region -> unit) -> unit val region : map -> node -> region val regions : map -> region list -val new_chunk : map -> ?size:int -> ?ptr:node -> unit -> node +val new_chunk : map -> ?size:int -> ?ptr:node -> ?ptrby:node -> unit -> node val add_root : map -> Cil_types.varinfo -> node val add_label : map -> string -> node val add_field : map -> node -> fieldinfo -> node @@ -93,6 +93,7 @@ val merge_copy : map -> l:node -> r:node -> unit val lval : map -> lval -> node val offset : map -> node -> offset -> node val cpointed : map -> node -> node option +val cpointed_by : map -> node -> node list (** @raise Not_found *) val exp : map -> exp -> node option