From a71fec7991061d1b86b8686d03d14e7ec6d29a12 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 27 May 2024 17:29:19 +0200
Subject: [PATCH] [region] merge draft
---
src/plugins/region/ranges.ml | 24 +++++---
src/plugins/region/ranges.mli | 5 +-
src/plugins/region/rmap.ml | 103 ++++++++++++++++++++++++++++++++--
src/plugins/region/rmap.mli | 28 ++++++++-
src/plugins/region/store.ml | 49 ++++++++++++++++
src/plugins/region/store.mli | 32 +++++++++++
6 files changed, 226 insertions(+), 15 deletions(-)
create mode 100644 src/plugins/region/store.ml
create mode 100644 src/plugins/region/store.mli
diff --git a/src/plugins/region/ranges.ml b/src/plugins/region/ranges.ml
index 0283685ee42..8ab1aa1fe4c 100644
--- a/src/plugins/region/ranges.ml
+++ b/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
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/ranges.mli b/src/plugins/region/ranges.mli
index bebb3b61227..e7c05ad1e71 100644
--- a/src/plugins/region/ranges.mli
+++ b/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
diff --git a/src/plugins/region/rmap.ml b/src/plugins/region/rmap.ml
index 6fe58f06b57..26dd76be23f 100644
--- a/src/plugins/region/rmap.ml
+++ b/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
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/rmap.mli b/src/plugins/region/rmap.mli
index 4b4baad836e..00e7d1e0812 100644
--- a/src/plugins/region/rmap.mli
+++ b/src/plugins/region/rmap.mli
@@ -1,4 +1,3 @@
-
(**************************************************************************)
(* *)
(* 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
diff --git a/src/plugins/region/store.ml b/src/plugins/region/store.ml
new file mode 100644
index 00000000000..268871b817a
--- /dev/null
+++ b/src/plugins/region/store.ml
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/plugins/region/store.mli b/src/plugins/region/store.mli
new file mode 100644
index 00000000000..badfeb9ac5e
--- /dev/null
+++ b/src/plugins/region/store.mli
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(* *)
+(* 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
--
GitLab