From a1058f7d376f9f204ede155bd80db136e5739d25 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 9 Jan 2025 20:25:59 +0100
Subject: [PATCH] [Eva] In Hptmap.cached_fold, uses cache from Binary_cache.
Also take a Hptmap_sig.cache_type argument instead of ~name and ~temporary.
This is consistent with all other cached functions in hptmap.
---
src/kernel_services/abstract_interp/lmap.ml | 4 +-
.../abstract_interp/lmap_sig.ml | 2 +-
.../abstract_interp/locations.ml | 4 +-
.../abstract_interp/locations.mli | 6 +-
.../abstract_interp/map_lattice.ml | 6 +-
.../abstract_interp/map_lattice.mli | 2 +-
src/libraries/utils/binary_cache.mli | 6 --
src/libraries/utils/hptmap.ml | 70 +++++++++----------
src/libraries/utils/hptmap_sig.ml | 3 +-
src/plugins/eva/domains/equality/equality.ml | 5 +-
src/plugins/from/functionwise.ml | 4 +-
11 files changed, 47 insertions(+), 65 deletions(-)
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index b40ef8a586e..0f5c56a0959 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -745,9 +745,7 @@ struct
let iter = M.iter
- let cached_fold ~f ~cache_name ~temporary ~joiner ~empty =
- let cached_f = M.cached_fold ~f ~cache_name ~temporary ~joiner ~empty in
- fun m -> cached_f m
+ let cached_fold = M.cached_fold
let cached_map ~f ~cache ~temporary =
let cached_f = M.cached_map ~f ~cache ~temporary in
diff --git a/src/kernel_services/abstract_interp/lmap_sig.ml b/src/kernel_services/abstract_interp/lmap_sig.ml
index fb35acef317..8c39958e2a8 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.ml
+++ b/src/kernel_services/abstract_interp/lmap_sig.ml
@@ -187,8 +187,8 @@ module type S = sig
modules, as they create persistent caches. *)
val cached_fold :
+ cache:Hptmap_sig.cache_type ->
f:(Base.t -> offsetmap -> 'a) ->
- cache_name:string -> temporary:bool ->
joiner:('a -> 'a -> 'a) -> empty:'a -> map -> 'a
val cached_map :
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index ea8a60fe63e..afc8590b20d 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -272,10 +272,10 @@ 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_name:"loc_top_any_locals"
- ~temporary:false
+ ~cache
~f
~projection
~joiner:(||)
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 7e09abc3f7e..081c430c0ed 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -149,8 +149,7 @@ module Location_Bytes : sig
@raise Error_Top in the cases [Top _]. *)
val cached_fold:
- cache_name:string ->
- temporary:bool ->
+ cache:Hptmap_sig.cache_type ->
f:(Base.t -> Ival.t -> 'a) ->
projection:(Base.t -> Ival.t) ->
joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
@@ -288,8 +287,7 @@ module Zone : sig
@raise Error_Top in the case [Top Top]. *)
val cached_fold :
- cache_name:string ->
- temporary:bool ->
+ 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
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 483d860cf82..713ad30918a 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -80,7 +80,7 @@ module type MapSet_Lattice = sig
val fold_keys : (key -> 'a -> 'a) -> t -> 'a -> 'a
val fold : (key -> v -> 'a -> 'a) -> t -> 'a -> 'a
val cached_fold:
- cache_name:string -> temporary:bool ->
+ cache:Hptmap_sig.cache_type ->
f:(key -> v -> 'a) ->
projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
val for_all: (key -> v -> bool) -> t -> bool
@@ -436,8 +436,8 @@ 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_name ~temporary ~f ~projection ~joiner ~empty =
- let folded_f = KVMap.cached_fold ~cache_name ~temporary ~f ~joiner ~empty in
+ let cached_fold ~cache ~f ~projection ~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, _) ->
diff --git a/src/kernel_services/abstract_interp/map_lattice.mli b/src/kernel_services/abstract_interp/map_lattice.mli
index 1825d8dadae..1ef2068c67b 100644
--- a/src/kernel_services/abstract_interp/map_lattice.mli
+++ b/src/kernel_services/abstract_interp/map_lattice.mli
@@ -125,7 +125,7 @@ module type MapSet_Lattice = sig
val fold : (key -> v -> 'a -> 'a) -> t -> 'a -> 'a
val cached_fold:
- cache_name:string -> temporary:bool ->
+ cache:Hptmap_sig.cache_type ->
f:(key -> v -> 'a) ->
projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
diff --git a/src/libraries/utils/binary_cache.mli b/src/libraries/utils/binary_cache.mli
index 26cbfbbe786..bd063032205 100644
--- a/src/libraries/utils/binary_cache.mli
+++ b/src/libraries/utils/binary_cache.mli
@@ -24,12 +24,6 @@
you understand what happens in this module, and do not forget that
those caches are not aware of projects. *)
-val memory_footprint_var_name: string
-
-val cache_size: int
-(** Size of the caches. Controlled by environment variable
- [memory_footprint_var_name]. *)
-
module type Cacheable = sig
type t
val hash : t -> int
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 7766433682c..15a34cae3f1 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -339,42 +339,6 @@ module Shape(Key: Id_Datatype) = struct
let register_clear_cache f = clear_caches_ref := f :: !clear_caches_ref
let clear_caches () = List.iter (fun f -> f ()) !clear_caches_ref
- let cached_fold ~cache_name ~temporary ~f ~joiner ~empty =
- if debug_cache then Format.eprintf "CACHE cached_fold %s@." cache_name;
- let cache_size = Binary_cache.cache_size in
- let cache = Array.make cache_size (Empty, empty) in
- let hash t = abs (hash t mod cache_size) in
- let reset () = Array.fill cache 0 cache_size (Empty, empty) in
- if not temporary then register_clear_cache reset;
- fun m ->
- let rec traverse t =
- let mem result =
- cache.(hash t) <- (t, result);
- result
- in
- let find () =
- let t', r = cache.(hash t) in
- if equal t t' then r
- else raise Not_found
- in
- match t with
- | Empty -> empty
- | Leaf(key, value, _) ->
- (try
- find ()
- with Not_found ->
- mem (f key value)
- )
- | Branch(_p, _m, s0, s1, _) ->
- try
- find ()
- with Not_found ->
- let result0 = traverse s0 in
- let result1 = traverse s1 in
- mem (joiner result0 result1)
- in
- traverse m
-
module Cacheable (X: sig type v end) = struct
type t = (key, X.v) tree
let hash : t -> int = hash_generic
@@ -382,6 +346,26 @@ module Shape(Key: Id_Datatype) = struct
let equal : t -> t -> bool = (==)
end
+ let is_persistent_cache = function
+ | Hptmap_sig.PersistentCache _ -> true
+ | _ -> false
+
+ let make_unary_cache (type v result) empty name cache =
+ match cache with
+ | Hptmap_sig.NoCache -> (fun f x -> f x)
+ | Hptmap_sig.TemporaryCache cache_name
+ | Hptmap_sig.PersistentCache cache_name ->
+ if debug_cache
+ then Format.eprintf "Hptmap CACHE %s : %s@." name cache_name;
+ let module Arg = Cacheable (struct type nonrec v = v end) in
+ let module R = struct
+ type t = result
+ let sentinel : t = empty
+ end in
+ let module Cache = Binary_cache.Arity_One (Arg) (R) in
+ if is_persistent_cache cache then register_clear_cache Cache.clear;
+ Cache.merge
+
type ('v1, 'v2, 'result) cache_type =
| Any: ('v1, 'v2, 'result) cache_type
| Predicate: ('v1, 'v2, bool) cache_type
@@ -417,10 +401,20 @@ module Shape(Key: Id_Datatype) = struct
let module Cache = Binary_cache.Symmetric_Binary_Predicate (Arg1) in
Cache.clear, Cache.merge
in
- if cache = Hptmap_sig.PersistentCache cache_name
- then register_clear_cache clear_cache;
+ if is_persistent_cache cache then register_clear_cache clear_cache;
merge_cache
+ let cached_fold ~cache ~f ~joiner ~empty =
+ let cache_merge = make_unary_cache empty "cached_fold" cache in
+ let rec compute t = cache_merge traverse t
+ and traverse t =
+ match t with
+ | Empty -> empty
+ | Leaf (key, value, _) -> f key value
+ | Branch (_p, _m, s0, s1, _) -> joiner (compute s0) (compute s1)
+ in
+ compute
+
let fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both ~join ~empty =
let cache_merge = make_binary_cache empty "fold2" cache in
let rec compute s t = cache_merge aux s t
diff --git a/src/libraries/utils/hptmap_sig.ml b/src/libraries/utils/hptmap_sig.ml
index 1579855eb92..f53a23a5a27 100644
--- a/src/libraries/utils/hptmap_sig.ml
+++ b/src/libraries/utils/hptmap_sig.ml
@@ -118,8 +118,7 @@ module type Shape = sig
the map's ordering. *)
val cached_fold :
- cache_name:string ->
- temporary:bool ->
+ cache:cache_type ->
f:(key -> 'v -> 'b) ->
joiner:('b -> 'b -> 'b) ->
empty:'b ->
diff --git a/src/plugins/eva/domains/equality/equality.ml b/src/plugins/eva/domains/equality/equality.ml
index b621bd895d4..5101d2f13c1 100644
--- a/src/plugins/eva/domains/equality/equality.ml
+++ b/src/plugins/eva/domains/equality/equality.ml
@@ -400,12 +400,11 @@ module Set = struct
fmt map
let keys =
- let cache_name = "Equality.Set.keys" in
- let temporary = false in
+ let cache = Hptmap_sig.PersistentCache "Equality.Set.keys" in
let f k _ = if HCE.is_lval k then Leaf k else Empty in
let joiner t1 t2 = Node (t1, t2) in
let empty = Empty in
- cached_fold ~cache_name ~temporary ~f ~joiner ~empty
+ cached_fold ~cache ~f ~joiner ~empty
let lvalues_only_left =
let cache = Hptmap_sig.PersistentCache "Equality.Set.elements_only_left" in
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 8907b731dbb..de69304cdf8 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -66,9 +66,9 @@ module To_Use = struct
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_name:"from cleanup" ~temporary:true
- ~f ~joiner ~empty:Zone.bottom ~projection
+ Zone.cached_fold ~cache ~f ~joiner ~empty:Zone.bottom ~projection
in
let zone_substitution x =
try
--
GitLab