From e4b4d6a670c68e13d68a32375614158d3472efad Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 27 May 2024 12:34:11 +0200
Subject: [PATCH] [region] ranges & region map
---
src/plugins/region/ranges.ml | 67 +++++++++++++++++++++++++++++++++++
src/plugins/region/ranges.mli | 31 ++++++++++++++++
src/plugins/region/rmap.ml | 43 ++++++++++++++++++++++
src/plugins/region/rmap.mli | 25 +++++++++++++
4 files changed, 166 insertions(+)
create mode 100644 src/plugins/region/ranges.ml
create mode 100644 src/plugins/region/ranges.mli
create mode 100644 src/plugins/region/rmap.ml
create mode 100644 src/plugins/region/rmap.mli
diff --git a/src/plugins/region/ranges.ml b/src/plugins/region/ranges.ml
new file mode 100644
index 00000000000..0283685ee42
--- /dev/null
+++ b/src/plugins/region/ranges.ml
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let (+.) = Int64.add
+let (-.) = Int64.sub
+
+(* -------------------------------------------------------------------------- *)
+(* --- Range Maps --- *)
+(* -------------------------------------------------------------------------- *)
+
+type 'a range = {
+ offset: int64 ;
+ length: int64 ;
+ data: 'a ;
+}
+
+type 'a t = R of 'a range list (* sorted, no-overlap *)
+
+let empty = R []
+
+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
+ if a' <= b.offset then
+ a :: merge f wa rb
+ else
+ if b' < a.offset then
+ b :: merge f ra wb
+ else
+ let offset = min a.offset b.offset in
+ 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
+
+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
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/ranges.mli b/src/plugins/region/ranges.mli
new file mode 100644
index 00000000000..bebb3b61227
--- /dev/null
+++ b/src/plugins/region/ranges.mli
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val ( +. ) : int64 -> int64 -> int64
+val ( -. ) : 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
diff --git a/src/plugins/region/rmap.ml b/src/plugins/region/rmap.ml
new file mode 100644
index 00000000000..6fe58f06b57
--- /dev/null
+++ b/src/plugins/region/rmap.ml
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+module Ufind = UnionFind.StoreMap
+
+[@@@ warning "-69"]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Maps --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* All offsets in bits *)
+
+type node = region Ufind.rref
+
+and region = {
+ parents: node list ;
+ roots: logic_var list ;
+ size: int64 ;
+ layout: node Ranges.t option ;
+}
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/rmap.mli b/src/plugins/region/rmap.mli
new file mode 100644
index 00000000000..4b4baad836e
--- /dev/null
+++ b/src/plugins/region/rmap.mli
@@ -0,0 +1,25 @@
+
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type node
+type region
--
GitLab