From 96cc44f018f7d284a78550bb4284f1bfadbe21d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 5 Apr 2022 09:49:24 +0200
Subject: [PATCH] [Eva] Lattice_bounds: shares more functions between Bottom,
Top and TopBottom.
---
.../abstract_interp/lattice_bounds.ml | 57 +++++++++++--------
1 file changed, 32 insertions(+), 25 deletions(-)
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml
index be5326b31fb..e432e4e8c16 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.ml
+++ b/src/kernel_services/abstract_interp/lattice_bounds.ml
@@ -39,6 +39,9 @@ end
module Common =
struct
+
+ (* Pretty-printing *)
+
let pretty_top fmt =
Format.pp_print_string fmt (Unicode.top_string ())
@@ -50,6 +53,8 @@ struct
| `Top -> pretty_top fmt
| `Value v -> pretty_value fmt v
+ (* Datatype *)
+
let hash hash_value = function
| `Bottom -> 7
| `Top -> 13
@@ -70,6 +75,33 @@ struct
| `Top, `Value _ -> -1
| `Value _, `Top -> 1
| `Value vx, `Value vy -> compare_value vx vy
+
+ (* Tests *)
+
+ let is_bottom = function
+ | `Bottom -> true
+ | `Value _ | `Top -> false
+
+ let is_top = function
+ | `Top -> true
+ | `Value _ | `Bottom -> false
+
+ let is_included is_included x y =
+ match x, y with
+ | `Bottom, _ | _, `Top -> true
+ | _, `Bottom | `Top, _ -> false
+ | `Value vx, `Value vy -> is_included vx vy
+
+ (* Iterator *)
+ let iter f = function
+ | `Bottom | `Top -> ()
+ | `Value v -> f v
+
+ (* Conversion *)
+ let to_option = function
+ | `Bottom | `Top -> None
+ | `Value x -> Some x
+
end
module Bottom = struct
@@ -79,10 +111,6 @@ module Bottom = struct
(** Access *)
- let is_bottom = function
- | `Bottom -> true
- | `Value _ -> false
-
let non_bottom = function
| `Value v -> v
| `Bottom -> assert false
@@ -93,11 +121,6 @@ module Bottom = struct
(* Lattice operators *)
- let is_included is_included x y = match x, y with
- | `Bottom, _ -> true
- | _, `Bottom -> false
- | `Value vx, `Value vy -> is_included vx vy
-
let join join x y = match x, y with
| `Value vx, `Value vy -> `Value (join vx vy)
| `Bottom, (`Value _ as v)
@@ -114,10 +137,6 @@ module Bottom = struct
(* Iterators *)
- let iter f = function
- | `Bottom -> ()
- | `Value v -> f v
-
let fold ~bottom f = function
| `Bottom -> bottom
| `Value v -> f v
@@ -135,10 +154,6 @@ module Bottom = struct
(** Conversion *)
- let to_option = function
- | `Bottom -> None
- | `Value v -> Some v
-
let of_option = function
| None -> `Bottom
| Some v -> `Value v
@@ -227,10 +242,6 @@ struct
(** Access *)
- let is_top = function
- | `Value _ -> false
- | `Top -> true
-
let non_top = function
| `Value v -> v
| `Top -> assert false
@@ -252,10 +263,6 @@ struct
| None -> `Top
| Some x -> `Value x
- let to_option = function
- | `Top -> None
- | `Value x -> Some x
-
(** Operators *)
module Operators = struct
--
GitLab