diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index b40ef8a586ef013d0fae248b9c98d1c099fb991a..0f5c56a0959d97126f77f8d1a270c038a755aa21 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 fb35acef3172caa2a1de9706e24f09d9461daa93..8c39958e2a8f817b3bc577f4a9ac6b6806d6c605 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 ea8a60fe63e983d82ff09a51f8af5d723ba90d99..afc8590b20d27070a5f7842c12c4dc86fb642035 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 7e09abc3f7e61ad4c9abc41bba2fd28a9c7f6aed..081c430c0ed2cba6c6342f95ab7290889ba7abba 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 483d860cf828de81c3cbcf4b7c860fbaac29e8df..713ad30918a9507f8649def90b1a3bd815e0d644 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 1825d8dadae768fcc181afa24fa881de46601b42..1ef2068c67b7212b05c03ee0b68f2efa4158c13f 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 26cbfbbe786abb6b5fcdf103043b15f0ed47f96e..bd06303220591ccf119761273821d8c10abe14da 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 7766433682c661555a31392920d1d112d28675f3..15a34cae3f11f18749e5ac1888fac60544bc10d7 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 1579855eb92d871a42a69ea461bd1e3ab23664e7..f53a23a5a27b233a91334da8d7bb1e4bb32854cc 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 b621bd895d4020ce4f85c454df80844b815caccb..5101d2f13c1dc39d5df6b43e5763e3c336d84b9c 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 8907b731dbbc2ac05953d066fd67ec442d89eb87..de69304cdf86af51a3b79d44b076cb2868bafd6d 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