From be69df124e023fe33e797175246f43bd0f1b2bd6 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Fri, 17 Jan 2025 13:27:33 +0100
Subject: [PATCH] [Kernel] Removing zip from Lattice_bounds
---
src/kernel_services/abstract_interp/lattice_bounds.mli | 6 ------
src/plugins/eva/contexts/context_product.ml | 2 +-
src/plugins/eva/domains/multidim/segmentation.ml | 6 +++---
3 files changed, 4 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.mli b/src/kernel_services/abstract_interp/lattice_bounds.mli
index 9b444d32611..faba7e98261 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.mli
+++ b/src/kernel_services/abstract_interp/lattice_bounds.mli
@@ -63,9 +63,6 @@ module Bottom : sig
(* Iterators *)
val iter : ('a -> unit) -> 'a t -> unit
- (* Combination *)
- val zip : 'a t -> 'b t -> ('a * 'b) t (* `Bottom if any is `Bottom *)
-
(** In a lattice where the elements are lists of non-bottom values,
the empty list is the bottom case. *)
@@ -113,9 +110,6 @@ module Top : sig
(* Iterators *)
val iter : ('a -> unit) -> 'a t -> unit
- (** Combination *)
- val zip : 'a t -> 'b t -> ('a * 'b) t (* `Top if any is `Top *)
-
(** Conversion *)
val to_option : 'a t -> 'a option
val of_option : 'a option -> 'a t
diff --git a/src/plugins/eva/contexts/context_product.ml b/src/plugins/eva/contexts/context_product.ml
index 4ca41b8fdc1..072bb1824f8 100644
--- a/src/plugins/eva/contexts/context_product.ml
+++ b/src/plugins/eva/contexts/context_product.ml
@@ -24,5 +24,5 @@ module Make (L : Abstract_context.S) (R : Abstract_context.S) = struct
type t = L.t * R.t
let top = (L.top, R.top)
let narrow (l, r) (l', r') =
- Lattice_bounds.Bottom.zip (L.narrow l l') (R.narrow r r')
+ Lattice_bounds.Bottom.product (L.narrow l l') (R.narrow r r')
end
diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml
index 3df764821ef..88ec2cac45d 100644
--- a/src/plugins/eva/domains/multidim/segmentation.ml
+++ b/src/plugins/eva/domains/multidim/segmentation.ml
@@ -304,14 +304,14 @@ struct
let lower_bound ~oracle b1 b2 =
if b1 == b2 || eq b1 b2 then `Value b1 else
- let+ i1,i2 = Top.zip
+ let+ i1,i2 = Top.product
(lower_integer ~oracle:(oracle Left) b1)
(lower_integer ~oracle:(oracle Right) b2) in
Const (Integer.min i1 i2)
let upper_bound ~oracle b1 b2 =
if b1 == b2 || eq b1 b2 then `Value b1 else
- let+ i1,i2 = Top.zip
+ let+ i1,i2 = Top.product
(upper_integer ~oracle:(oracle Left) b1)
(upper_integer ~oracle:(oracle Right) b2) in
Const (Integer.max i1 i2)
@@ -510,7 +510,7 @@ struct
let hull ~oracle (m : t) : (bound * bound) or_top =
let l = m.start and u = last_bound m.segments in
- Top.zip (B.lower_const ~oracle l) (B.upper_const ~oracle u)
+ Top.product (B.lower_const ~oracle l) (B.upper_const ~oracle u)
let is_empty_segment ~oracle l u =
let open (val (B.operators oracle)) in
--
GitLab