From be905cb5f75fd88034151a8018eda9c5f4e1769e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 9 Jan 2025 23:18:04 +0100
Subject: [PATCH] [Eva] In map_lattice, removes undocumented argument
projection of cached_fold.
---
src/kernel_services/abstract_interp/locations.ml | 10 +---------
src/kernel_services/abstract_interp/locations.mli | 2 --
src/kernel_services/abstract_interp/map_lattice.ml | 10 +++-------
src/kernel_services/abstract_interp/map_lattice.mli | 3 +--
src/plugins/from/functionwise.ml | 3 +--
5 files changed, 6 insertions(+), 22 deletions(-)
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index afc8590b20d..91f61c4ddc0 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -271,16 +271,8 @@ module Location_Bytes = struct
let contains_addresses_of_any_locals =
let f base _offsets = Base.is_any_formal_or_local base in
- let projection _base = Ival.top in
let cache = Hptmap_sig.PersistentCache "loc_top_any_locals" in
- let cached_f =
- cached_fold
- ~cache
- ~f
- ~projection
- ~joiner:(||)
- ~empty:false
- in
+ let cached_f = cached_fold ~cache ~f ~joiner:(||) ~empty:false in
fun loc ->
try
cached_f loc
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 081c430c0ed..8e953c90d33 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -151,7 +151,6 @@ module Location_Bytes : sig
val cached_fold:
cache:Hptmap_sig.cache_type ->
f:(Base.t -> Ival.t -> 'a) ->
- projection:(Base.t -> Ival.t) ->
joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
(** Cached version of [fold_i], for advanced users *)
@@ -289,7 +288,6 @@ module Zone : sig
val cached_fold :
cache:Hptmap_sig.cache_type ->
f:(Base.t -> Int_Intervals.t -> 'b) ->
- projection:(Base.t -> Int_Intervals.t) ->
joiner:('b -> 'b -> 'b) -> empty:'b -> t -> 'b
val fold2_join_heterogeneous:
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 713ad30918a..d2e1cb5b28c 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -81,8 +81,7 @@ module type MapSet_Lattice = sig
val fold : (key -> v -> 'a -> 'a) -> t -> 'a -> 'a
val cached_fold:
cache:Hptmap_sig.cache_type ->
- f:(key -> v -> 'a) ->
- projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
+ f:(key -> v -> 'a) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
val for_all: (key -> v -> bool) -> t -> bool
val exists: (key -> v -> bool) -> t -> bool
val pretty_debug : Format.formatter -> t -> unit
@@ -436,15 +435,12 @@ module Make_MapSet_Lattice
| Top (s, _) -> KSet.fold (fun x acc -> f x Value.top acc) s acc
| Map m -> KVMap.fold f m acc
- let cached_fold ~cache ~f ~projection ~joiner ~empty =
+ let cached_fold ~cache ~f ~joiner ~empty =
let folded_f = KVMap.cached_fold ~cache ~f ~joiner ~empty in
function
| Top (KSet.Top, _) -> raise Abstract_interp.Error_Top
| Top (KSet.Set s, _) ->
- let f_base base acc =
- let total_itvs = projection base in
- joiner (f base total_itvs) acc
- in
+ let f_base base acc = joiner (f base Value.top) acc in
KSet.O.fold f_base s empty
| Map m -> folded_f m
diff --git a/src/kernel_services/abstract_interp/map_lattice.mli b/src/kernel_services/abstract_interp/map_lattice.mli
index 1ef2068c67b..20d149828f2 100644
--- a/src/kernel_services/abstract_interp/map_lattice.mli
+++ b/src/kernel_services/abstract_interp/map_lattice.mli
@@ -126,8 +126,7 @@ module type MapSet_Lattice = sig
val cached_fold:
cache:Hptmap_sig.cache_type ->
- f:(key -> v -> 'a) ->
- projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
+ f:(key -> v -> 'a) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
(** [for_all p t] checks if all binding of [t] satisfy [p] . Always false if
[t] is top. *)
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index de69304cdf8..730527d6683 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -65,10 +65,9 @@ module To_Use = struct
else Zone.bottom
in
let joiner = Zone.join in
- let projection _ = Int_Intervals.top in
let cache = Hptmap_sig.TemporaryCache "from cleanup" in
let zone_substitution =
- Zone.cached_fold ~cache ~f ~joiner ~empty:Zone.bottom ~projection
+ Zone.cached_fold ~cache ~f ~joiner ~empty:Zone.bottom
in
let zone_substitution x =
try
--
GitLab