[region] merge draft

src/plugins/region/ranges.ml

@@ -23,6 +23,11 @@
 let (+.) = Int64.add
 let (-.) = Int64.sub
 
+let rec gcd a b =
+  if a = Int64.zero then b else
+  if b = Int64.zero then a else
+    gcd b (Int64.rem a b)
+
 (* -------------------------------------------------------------------------- *)
 (* --- Range Maps                                                         --- *)
 (* -------------------------------------------------------------------------- *)
@@ -37,6 +42,13 @@ type 'a t = R of 'a range list (* sorted, no-overlap *)
 
 let empty = R []
 
+let rec find (k: int64) = function
+  | [] -> raise Not_found
+  | ({ offset ; length } as r) :: rs ->
+    if offset <= k && k <= offset +. length then r else find k rs
+
+let find k (R rs) = find k rs
+
 let rec merge f ra rb =
   match ra, rb with
   | [], rs | rs, [] -> rs
@@ -53,15 +65,13 @@ let rec merge f ra rb =
       let length = max a' b' -. offset in
       let data = f a.data b.data in
       let r = { offset ; length ; data } in
-      merge f (r::ra) rb
+      if a' < b'
+      then merge f ra (r::rb)
+      else merge f (r::ra) rb
 
 let merge f (R x) (R y) = R (merge f x y)
 
-let rec find (k: int64) = function
-  | [] -> raise Not_found
-  | ({ offset ; length } as r) :: rs ->
-    if offset <= k && k <= offset +. length then r else find k rs
-
-let find k (R rs) = find k rs
+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

@@ -22,10 +22,13 @@
 
 val ( +. ) : int64 -> int64 -> int64
 val ( -. ) : int64 -> int64 -> int64
+val gcd : int64 -> int64 -> int64
 
 type 'a range = { offset : int64; length : int64; data : 'a; }
 type 'a t = private R of 'a range list (* sorted, no overlap *)
 
 val empty : 'a t
-val merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
 val find : int64 -> 'a t -> 'a range
+val merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+val iter : ('a -> unit) -> 'a t -> unit
+val iteri : ('a range -> unit) -> 'a t -> unit

src/plugins/region/rmap.ml

@@ -21,23 +21,116 @@
 (**************************************************************************)
 
 open Cil_types
-module Ufind = UnionFind.StoreMap
-
-[@@@ warning "-69"]
+open Cil_datatype
+module Ufind = UnionFind.Make(Store)
+module Vmap = Varinfo.Map
 
 (* -------------------------------------------------------------------------- *)
 (* --- Region Maps                                                        --- *)
 (* -------------------------------------------------------------------------- *)
 
+[@@@ warning "-37"]
+
 (* All offsets in bits *)
 
 type node = region Ufind.rref
 
+and layout =
+  | Blob
+  | Atom
+  | AtomPtr of node
+  | Compound of node Ranges.t
+
 and region = {
   parents: node list ;
-  roots: logic_var list ;
+  roots: varinfo list ;
   size: int64 ;
-  layout: node Ranges.t option ;
+  layout: layout ;
+}
+
+type map = {
+  store: region Ufind.store ;
+  mutable index: node Vmap.t ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Constructors                                                       --- *)
+(* -------------------------------------------------------------------------- *)
+
+let create () = {
+  store = Ufind.new_store () ;
+  index = Vmap.empty ;
+}
+
+let copy m = {
+  store = Ufind.copy m.store ;
+  index = m.index ;
+}
+
+let blob () = {
+  parents = [] ;
+  roots = [] ;
+  size = Int64.zero ;
+  layout = Blob ;
 }
 
+let node map node =
+  try Ufind.find map.store node
+  with Not_found -> node
+
+let nodes map ns = Store.list @@ List.map (node map) ns
+
+let region map node =
+  try Ufind.get map.store node
+  with Not_found -> blob ()
+
+let root (m: map) lv =
+  try Vmap.find lv m.index with Not_found ->
+    let r = Ufind.make m.store (blob ()) in
+    m.index <- Vmap.add lv r m.index ; r
+
+(* -------------------------------------------------------------------------- *)
+(* --- Merge                                                              --- *)
+(* -------------------------------------------------------------------------- *)
+
+type queue = (node * node) Queue.t
+
+let qmerge (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 lmerge (m: map) (q: queue) (r: node) (a : layout) (b : layout) : layout =
+  match a, b with
+  | Blob, c | c, Blob -> c
+  | Atom, c | c, Atom -> c
+  | AtomPtr a, AtomPtr b -> AtomPtr (qmerge m q a b)
+  | Compound u, Compound v -> Compound (Ranges.merge (qmerge m q) u v)
+  | AtomPtr a, Compound w | Compound w, AtomPtr a ->
+    Ranges.iter (fun s -> ignore @@ qmerge m q r s) w ; AtomPtr a
+
+let rmerge (m: map) (q: queue) (r: node) (a : region) (b : region) : region = {
+  parents = nodes m (Store.bag a.parents b.parents) ;
+  roots = Store.bag a.roots b.roots ;
+  size = Ranges.gcd a.size b.size ;
+  layout = lmerge m q r a.layout b.layout ;
+}
+
+let umerge (m: map) (q: queue) (a: node) (b: node): unit =
+  begin
+    let ra = Ufind.get m.store a in
+    let rb = Ufind.get m.store b in
+    let r = Ufind.union m.store a b in
+    let rc = rmerge m q r ra rb in
+    Ufind.set m.store r rc ;
+  end
+
+let merge (m: map) (a: node) (b: node) : node =
+  if Ufind.eq m.store a b then Ufind.find m.store a else
+    let q = Queue.create () in
+    umerge m q a b ;
+    while not @@ Queue.is_empty q do
+      let a,b = Queue.pop q in
+      umerge m q a b ;
+    done ;
+    Ufind.find m.store a
+
 (* -------------------------------------------------------------------------- *)

src/plugins/region/rmap.mli

-
 (**************************************************************************)
 (*                                                                        *)
 (*  This file is part of Frama-C.                                         *)
@@ -21,5 +20,30 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Cil_types
+
 type node
-type region
+
+type layout =
+  | Blob
+  | Atom
+  | AtomPtr of node
+  | Compound of node Ranges.t
+
+type region = private {
+  parents: node list ;
+  roots: varinfo list ;
+  size: int64 ;
+  layout: layout ;
+}
+
+type map
+
+val create : unit -> map
+val copy : map -> map
+
+val root : map -> Cil_types.varinfo -> node
+val node : map -> node -> node
+val nodes : map -> node list -> node list
+val region : map -> node -> region
+val merge : map -> node -> node -> node

src/plugins/region/store.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2024                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- UnionFind Store with explicit integer keys                         --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Imap = Map.Make(Int)
+
+type 'a rref = int
+type 'a store = 'a Imap.t ref
+
+let new_store () = ref Imap.empty
+let copy r = ref !r
+let rid = ref 0
+let make s v =
+  let k = incr rid ; !rid in
+  s := Imap.add k v !s ; k
+
+let get s k = Imap.find k !s
+let set s k v = s := Imap.add k v !s
+
+let eq _s i j = (i == j)
+
+let id x = x
+let list = List.sort_uniq Int.compare
+let rec bag a b =
+  match a, b with
+  | [], c | c, [] -> c
+  | x::xs, y::ys -> x :: y :: bag xs ys

src/plugins/region/store.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2024                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include UnionFind.STORE
+
+(** Global unique identifier *)
+val id : 'a rref -> int
+
+(** Unordered union *)
+val bag: 'a list -> 'a list -> 'a list
+
+(** Sorted, unique *)
+val list : 'a rref list -> 'a rref list