diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index 98b06b38d6a1d1845152e5575ccf81c641f0c1fb..ddfa1d76b1362a2ec67b60467543039be9c13b88 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -93,20 +93,6 @@ let empty = { layout = Blob ; } -let cell (m: map) ?size ?ptr () = - let layout = match size, ptr with - | None, None -> Blob - | None, Some _ -> Cell(Cil.bitsSizeOf Cil.voidPtrType,ptr) - | Some s, _ -> Cell(s,ptr) - in Ufind.make m.store { empty with layout } - -let range (m: map) ~size ~offset ~length ~data : node = - let last = offset + length in - if not (0 <= offset && offset < last && last <= size) then - raise (Invalid_argument "Region.Memory.range") ; - let layout = Compound(size, Ranges.singleton { offset ; length ; data }) in - Ufind.make m.store { empty with layout } - (* -------------------------------------------------------------------------- *) (* --- Map --- *) (* -------------------------------------------------------------------------- *) @@ -117,14 +103,37 @@ let node map node = let nodes map ns = Store.list @@ List.map (node map) ns +(* -------------------------------------------------------------------------- *) +(* --- Constructors --- *) +(* -------------------------------------------------------------------------- *) + let region map node = try Ufind.get map.store node with Not_found -> empty +let cell (m: map) ?size ?ptr ?root () = + let layout = match size, ptr with + | None, None -> Blob + | None, Some _ -> Cell(Cil.bitsSizeOf Cil.voidPtrType,ptr) + | Some s, _ -> Cell(s,ptr) in + let roots = match root with None -> [] | Some v -> [v] in + Ufind.make m.store { empty with layout ; roots } + +let update (m: map) (n: node) (f: region -> region) = + let r = region m n in Ufind.set m.store n (f r) + +let range (m: map) ~size ~offset ~length ~data : node = + let last = offset + length in + if not (0 <= offset && offset < last && last <= size) then + raise (Invalid_argument "Region.Memory.range") ; + let layout = Compound(size, Ranges.singleton { offset ; length ; data }) in + let n = Ufind.make m.store { empty with layout } in + update m data (fun r -> { r with parents = n :: r.parents }) ; n + let root (m: map) v = try Vmap.find v m.index with Not_found -> - let r = cell m () in - m.index <- Vmap.add v r m.index ; r + let n = cell m ~root:v () in + m.index <- Vmap.add v n m.index ; n (* -------------------------------------------------------------------------- *) (* --- Merge --- *) diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli index 39bf48579446f8818b8b1c47779926ccd7d9a48f..924c8518f29e034d24c74c43ff4b7bc15d5e1d10 100644 --- a/src/plugins/region/memory.mli +++ b/src/plugins/region/memory.mli @@ -49,7 +49,7 @@ val create : unit -> map val copy : map -> map val root : map -> Cil_types.varinfo -> node -val cell : map -> ?size:int -> ?ptr:node -> unit -> node +val cell : map -> ?size:int -> ?ptr:node -> ?root:varinfo -> unit -> node val range : map -> size:int -> offset:int -> length:int -> data:node -> node val node : map -> node -> node