[region] terminating merge, int sizes

src/plugins/region/memory.ml

@@ -37,8 +37,8 @@ type node = region Ufind.rref
 
 and layout =
   | Blob
-  | Cell of int64 * node option
-  | Compound of int64 * node Ranges.t
+  | Cell of int * node option
+  | Compound of int * node Ranges.t
 
 and region = {
   parents: node list ;
@@ -70,11 +70,7 @@ let copy m = {
   index = m.index ;
 }
 
-let sizeof_ptr () = Int64.of_int @@ Cil.bitsSizeOf Cil.voidPtrType
-let sizeof_typ ty = Int64.of_int @@ Cil.bitsSizeOf ty
-
-let sizeof_layout = function
-  | Blob -> Int64.zero | Cell(s,_) | Compound(s,_) -> s
+let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_) -> s
 
 let empty = {
   parents = [] ;
@@ -88,10 +84,17 @@ let empty = {
 let cell (m: map) ?size ?ptr () =
   let layout = match size, ptr with
     | None, None -> Blob
-    | None, Some _ -> Cell(sizeof_ptr (),ptr)
+    | 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,13 +120,14 @@ let root (m: map) v =
 
 type queue = (node * node) Queue.t
 
+let ranges ~size = function
+  | None -> Ranges.empty
+  | Some r -> Ranges.range ~length:size r
+
 let merge_node (m: map) (q: queue) (a: node) (b: node) : node =
   if not @@ Ufind.eq m.store a b then Queue.push (a,b) q ; min a b
 
-let merge_inode (m: map) (q: queue) (a: node) (b: node) : unit =
-  ignore @@ merge_node m q a b
-
-let merge_ptr (m: map) (q: queue)
+let merge_opt (m: map) (q: queue)
     (pa : node option) (pb : node option) : node option =
   match pa, pb with
   | None, p | p, None -> p
@@ -132,40 +136,44 @@ let merge_ptr (m: map) (q: queue)
 let merge_range (m: map) (q: queue) (ra : range) (rb : range) : node =
   let na = ra.data in
   let nb = rb.data in
-  let ma = Ranges.( ra.offset +. ra.length ) in
-  let mb = Ranges.( rb.offset +. rb.length ) in
-  let dp = Ranges.( ra.offset -. rb.offset ) in
-  let dq = Ranges.( ma -. mb ) in
-  let sa = sizeof_layout (region m na).layout in
-  let sb = sizeof_layout (region m nb).layout in
+  let ma = ra.offset + ra.length in
+  let mb = rb.offset + rb.length in
+  let dp = ra.offset - rb.offset in
+  let dq = ma - mb in
+  let sa = sizeof (region m na).layout in
+  let sb = sizeof (region m nb).layout in
   let size = Ranges.(sa %. sb %. dp %. dq) in
   let data = merge_node m q na nb in
   if size = sa && size = sb then data else
     merge_node m q (cell m ~size ()) data
 
 let merge_ranges (m: map) (q: queue)
-    (sa : int64) (wa : node Ranges.t)
-    (sb : int64) (wb : node Ranges.t)
+    (sa : int) (wa : node Ranges.t)
+    (sb : int) (wb : node Ranges.t)
   : layout =
   if sa = sb then
     Compound(sa, Ranges.merge (merge_range m q) wa wb)
   else
     let size = Ranges.gcd sa sb in
-    let r = cell m ~size () in
-    Ranges.iter (merge_inode m q r) wa ;
-    Ranges.iter (merge_inode m q r) wb ;
-    let rg = Ranges.{ offset = Int64.zero ; length = size ; data = r } in
-    Compound(size, Ranges.singleton rg )
+    let ra = Ranges.squash (merge_node m q) wa in
+    let rb = Ranges.squash (merge_node m q) wb in
+    Compound(size, ranges ~size @@ merge_opt m q ra rb)
 
 let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout =
   match a, b with
   | Blob, c | c, Blob -> c
-  | Cell(sa,pa) , Cell(sb,pb) -> Cell(Ranges.gcd sa sb, merge_ptr m q pa pb)
+
+  | Cell(sa,pa) , Cell(sb,pb) -> Cell(Ranges.gcd sa sb, merge_opt m q pa pb)
+
   | Compound(sa,wa), Compound(sb,wb) -> merge_ranges m q sa wa sb wb
-  | Compound(sr,wr), Cell(sx,px)
-  | Cell(sx,px), Compound(sr,wr) ->
-    let data = cell m ~size:sx ?ptr:px () in
-    let wx = Ranges.singleton { offset = Int64.zero ; length = sx ; data } in
+
+  | Compound(sr,wr), Cell(sx,None) | Cell(sx,None), Compound(sr,wr) ->
+    let size = Ranges.gcd sx sr in
+    Compound(size, ranges ~size @@ Ranges.squash (merge_node m q) wr)
+
+  | Compound(sr,wr), Cell(sx,Some ptr) | Cell(sx,Some ptr), Compound(sr,wr) ->
+    let rp = cell m ~size:sx ~ptr () in
+    let wx = Ranges.range ~length:sx rp in
     merge_ranges m q sx wx sr wr
 
 let merge_region (m: map) (q: queue) (a : region) (b : region) : region = {

src/plugins/region/memory.mli

@@ -26,8 +26,8 @@ type node
 
 and layout =
   | Blob
-  | Cell of int64 * node option
-  | Compound of int64 * node Ranges.t
+  | Cell of int * node option
+  | Compound of int * node Ranges.t
 
 type region = private {
   parents: node list ;
@@ -44,7 +44,9 @@ val create : unit -> map
 val copy : map -> map
 
 val root : map -> Cil_types.varinfo -> node
-val cell : map -> ?size:int64 -> ?ptr:node -> unit -> node
+val cell : map -> ?size:int -> ?ptr:node -> unit -> node
+val range : map -> size:int -> offset:int -> length:int -> data:node -> node
+
 val node : map -> node -> node
 val nodes : map -> node list -> node list
 val region : map -> node -> region
@@ -53,7 +55,4 @@ val read : map -> node -> Access.acs -> unit
 val write : map -> node -> Access.acs -> unit
 val shift : map -> node -> Access.acs -> unit
 val points_to : map -> node -> node -> unit
-
-val sizeof_ptr : unit -> int64
-val sizeof_typ : Cil_types.typ -> int64
-val sizeof_layout : layout -> int64
+val sizeof : layout -> int

src/plugins/region/ranges.ml

@@ -21,12 +21,10 @@
 (**************************************************************************)
 
 let rec gcd a b =
-  if a = Int64.zero then Int64.abs b else
-  if b = Int64.zero then Int64.abs a else
-    gcd b (Int64.rem a b)
+  if a = 0 then abs b else
+  if b = 0 then abs a else
+    gcd b (a mod b)
 
-let (+.) = Int64.add
-let (-.) = Int64.sub
 let (%.) = gcd
 
 (* -------------------------------------------------------------------------- *)
@@ -34,8 +32,8 @@ let (%.) = gcd
 (* -------------------------------------------------------------------------- *)
 
 type 'a range = {
-  offset: int64 ;
-  length: int64 ;
+  offset: int ;
+  length: int ;
   data: 'a ;
 }
 
@@ -43,12 +41,17 @@ type 'a t = R of 'a range list (* sorted, no-overlap *)
 
 let empty = R []
 
-let singleton r = R [r]
+let singleton r =
+  if not (0 <= r.offset && 0 < r.length) then
+    raise (Invalid_argument "Region.Ranges.singleton") ;
+  R [r]
 
-let rec find (k: int64) = function
+let range ?(offset=0) ?(length=1) data = singleton { offset ; length ; data }
+
+let rec find (k: int) = function
   | [] -> raise Not_found
   | ({ offset ; length } as r) :: rs ->
-    if offset <= k && k <= offset +. length then r else find k rs
+    if offset <= k && k <= offset + length then r else find k rs
 
 let find k (R rs) = find k rs
 
@@ -56,8 +59,8 @@ let rec merge f ra rb =
   match ra, rb with
   | [], rs | rs, [] -> rs
   | a :: wa, b :: wb ->
-    let a' = a.offset +. a.length in
-    let b' = b.offset +. b.length in
+    let a' = a.offset + a.length in
+    let b' = b.offset + b.length in
     if a' <= b.offset then
       a :: merge f wa rb
     else
@@ -65,7 +68,7 @@ let rec merge f ra rb =
       b :: merge f ra wb
     else
       let offset = min a.offset b.offset in
-      let length = max a' b' -. offset in
+      let length = max a' b' - offset in
       let data = f a b in
       let r = { offset ; length ; data } in
       if a' < b'
@@ -74,6 +77,10 @@ let rec merge f ra rb =
 
 let merge f (R x) (R y) = R (merge f x y)
 
+let squash f = function
+  | R [] -> None
+  | R (x::xs) -> Some (List.fold_left (fun w r -> f w r.data) x.data xs)
+
 let iteri f (R xs) = List.iter f xs
 let iter f (R xs) = List.iter (fun r -> f r.data) xs
 

src/plugins/region/ranges.mli

@@ -20,19 +20,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val gcd : int64 -> int64 -> int64
+val gcd : int -> int -> int
+val (%.) : int -> int -> int (** gcd *)
 
-val ( +. ) : int64 -> int64 -> int64
-val ( -. ) : int64 -> int64 -> int64
-val ( %. ) : int64 -> int64 -> int64 (** gcd *)
-
-type 'a range = { offset : int64; length : int64; data : 'a; }
+type 'a range = { offset : int; length : int; data : 'a; }
 type 'a t = private R of 'a range list (* sorted, no overlap *)
 
 val empty : 'a t
 val singleton : 'a range -> 'a t
+val range : ?offset:int -> ?length:int -> 'a -> 'a t
 val merge : ('a range -> 'a range -> 'a) -> 'a t -> 'a t -> 'a t
+val squash : ('a -> 'a -> 'a) -> 'a t -> 'a option
 
-val find : int64 -> 'a t -> 'a range
+val find : int -> 'a t -> 'a range
 val iter : ('a -> unit) -> 'a t -> unit
 val iteri : ('a range -> unit) -> 'a t -> unit