diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk index 73de1f4ccd11e615ff64beaf883f4d27fb07e54d..311e93d2fb203b40dea323be6128198e1fff2770 100644 --- a/share/analysis-scripts/analysis.mk +++ b/share/analysis-scripts/analysis.mk @@ -125,6 +125,7 @@ EVAFLAGS ?= \ -no-deps-print -no-calldeps-print \ -eva-warn-key garbled-mix=active,garbled-mix:write=active \ -calldeps -from-verbose 0 \ + -cache-size 8 \ $(if $(EVABUILTINS), -eva-builtin=$(call fc_list,$(EVABUILTINS)),) \ $(if $(EVAUSESPECS), -eva-use-spec $(call fc_list,$(EVAUSESPECS)),) WPFLAGS ?= diff --git a/share/analysis-scripts/prologue.mk b/share/analysis-scripts/prologue.mk index 7a3b4d65cac3a0aba3a51d5175b8ad983024266d..60f7a93e163747327dce030d27fea6005b42705a 100644 --- a/share/analysis-scripts/prologue.mk +++ b/share/analysis-scripts/prologue.mk @@ -26,11 +26,6 @@ # Note: this variable must be defined before including any files makefile_dir := $(dir $(lastword $(MAKEFILE_LIST))) -## Useful definitions (to be overridden later if needed) - -# Improves analysis time, at the cost of extra memory usage -export FRAMA_C_MEMORY_FOOTPRINT = 8 - # analysis.mk contains the main rules and targets include $(makefile_dir)/analysis.mk 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..91f61c4ddc07b1d34bb1ec56f8221d70145682bd 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 cached_f = - cached_fold - ~cache_name:"loc_top_any_locals" - ~temporary:false - ~f - ~projection - ~joiner:(||) - ~empty:false - in + let cache = Hptmap_sig.PersistentCache "loc_top_any_locals" 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 7e09abc3f7e61ad4c9abc41bba2fd28a9c7f6aed..8e953c90d33e7688179e7c4fb0e8813001ae4c37 100644 --- a/src/kernel_services/abstract_interp/locations.mli +++ b/src/kernel_services/abstract_interp/locations.mli @@ -149,10 +149,8 @@ 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 (** Cached version of [fold_i], for advanced users *) @@ -288,10 +286,8 @@ 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 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 483d860cf828de81c3cbcf4b7c860fbaac29e8df..d2e1cb5b28c7824e34c40216726b6c719ef8be0e 100644 --- a/src/kernel_services/abstract_interp/map_lattice.ml +++ b/src/kernel_services/abstract_interp/map_lattice.ml @@ -80,9 +80,8 @@ 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 -> - f:(key -> v -> 'a) -> - projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a + cache:Hptmap_sig.cache_type -> + 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_name ~temporary ~f ~projection ~joiner ~empty = - let folded_f = KVMap.cached_fold ~cache_name ~temporary ~f ~joiner ~empty in + 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 1825d8dadae768fcc181afa24fa881de46601b42..20d149828f25dbb0898dd5d1eb9033e74acbf1ea 100644 --- a/src/kernel_services/abstract_interp/map_lattice.mli +++ b/src/kernel_services/abstract_interp/map_lattice.mli @@ -125,9 +125,8 @@ module type MapSet_Lattice = sig val fold : (key -> v -> 'a -> 'a) -> t -> 'a -> 'a val cached_fold: - cache_name:string -> temporary:bool -> - f:(key -> v -> 'a) -> - projection:(key -> v) -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a + cache:Hptmap_sig.cache_type -> + 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/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index cabf7da511dff86c26e4bad9b233f28758968337..88e6d32d72ecbf5d8912c5d5d18d6c1a0f80b71f 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -1847,14 +1847,27 @@ module MemoryFootprint = end) let () = MemoryFootprint.set_range ~min:1 ~max:10 -(* ************************************************************************* *) -(** {2 Other options} *) -(* ************************************************************************* *) - -[@@@warning "-60"] -(* Warning: these options are parsed and used directly from Cmdline *) +let () = Parameter_customize.set_group performance +let () = Parameter_customize.do_not_reset_on_copy () +module CacheSize = + Int + (struct + let module_name = "CacheSize" + let default = 2 + let option_name = "-cache-size" + let arg_name = "n" + let help = + "Control the amount of memory allocated to some internal caches. \ + Must be between 1 and 10; default value is 2. \ + Each increase of 1 doubles the size of these caches. \ + Small values are most suitable for the analysis of small programs \ + (less than 1000 lines). Higher values (around 7-8) can speed up the \ + analysis of large code bases." + end) +let () = CacheSize.set_range ~min:1 ~max:10 +let () = CacheSize.add_update_hook (fun _ i -> Binary_cache.set_cache_size i) -let () = Parameter_customize.set_group project +let () = Parameter_customize.set_group performance let () = Parameter_customize.set_negative_option_name "" let () = Parameter_customize.set_cmdline_stage Cmdline.Early module Deterministic = @@ -1866,6 +1879,10 @@ module Deterministic = let help = "" end) +(* ************************************************************************* *) +(** {2 Other options} *) +(* ************************************************************************* *) + let () = Parameter_customize.set_group checks let () = Parameter_customize.do_not_projectify () let () = Parameter_customize.set_negative_option_name "" @@ -1879,8 +1896,6 @@ module Permissive = "perform less verifications on validity of command-line options" end) -[@@@warning "+60"] - (* Local Variables: compile-command: "make -C ../../.." diff --git a/src/libraries/utils/binary_cache.ml b/src/libraries/utils/binary_cache.ml index 97b3f40d131d027345ee0f2dd05d4f7b9f1ec6d8..24eaa41957a5c07eddbd2e2acd2facc7af5c1c7c 100644 --- a/src/libraries/utils/binary_cache.ml +++ b/src/libraries/utils/binary_cache.ml @@ -20,25 +20,15 @@ (* *) (**************************************************************************) -let memory_footprint_var_name = "FRAMA_C_MEMORY_FOOTPRINT" - -let memory_footprint = - let error () = - Cmdline.Kernel_log.error - "@[Bad value for environment variable@ %s.@ Expected value: \ - integer between@ 1 and 10.@ Using@ default value@ of 2.@]" - memory_footprint_var_name; - 2 - in - try - let i = int_of_string (Sys.getenv memory_footprint_var_name) in - if i <= 0 || i > 10 then error () - else i - with - | Not_found -> 2 - | Failure _ -> error () - -let cache_size = 1 lsl (8 + memory_footprint) +let compute_cache_size i = 1 lsl (8 + i) +let default_value = 2 + +(* Should not be used to create cache before the value from -cache-size + has been set. *) +let cache_size = ref (compute_cache_size default_value) + +(* Set by the kernel, according to the -cache-size parameter. *) +let set_cache_size i = cache_size := compute_cache_size i (** The caches of this module are lazy, for two reasons: @@ -55,7 +45,6 @@ let cache_size = 1 lsl (8 + memory_footprint) (This is not perfect: once a lazy cache has been forced, each 'clear' operation becomes costly again.) *) -let (!!) = Lazy.force module type Cacheable = sig @@ -163,18 +152,23 @@ end module Symmetric_Binary (H: Cacheable) (R: Result) = struct - let size = cache_size - let cache = lazy (Array_3.make size H.sentinel H.sentinel R.sentinel) - let mask = pred size + let create () = + let size = !cache_size in + let array = Array_3.make size H.sentinel H.sentinel R.sentinel in + array, pred size + + let cache = lazy (create ()) let clear () = if Lazy.is_val cache then - Array_3.clear !!cache H.sentinel H.sentinel R.sentinel + let array, _ = Lazy.force cache in + Array_3.clear array H.sentinel H.sentinel R.sentinel let hash = H.hash let merge f a0 a1 = + let array, mask = Lazy.force cache in let a0', a1', h0, h1 = let h0 = hash a0 in let h1 = hash a1 in @@ -185,106 +179,114 @@ struct let has = h1 lsl 5 - h1 + h0 in let has = has land mask in - - if H.equal (Array_3.get0 !!cache has) a0' - && H.equal (Array_3.get1 !!cache has) a1' - then begin - (* Format.printf "Cache O@."; *) - Array_3.get2 !!cache has - end + if H.equal (Array_3.get0 array has) a0' + && H.equal (Array_3.get1 array has) a1' + then + Array_3.get2 array has else let result = f a0 a1 in - (* Format.printf "Cache N@."; *) - Array_3.set !!cache has a0' a1' result; + Array_3.set array has a0' a1' result; result end module Arity_One (H: Cacheable) (R: Result) = struct - let size = cache_size - let cache = lazy (Array_2.make size H.sentinel R.sentinel) - let mask = pred size + (* Creates the array used for the cache, and the mask to be used on keys + according to the array size. *) + let create () = + let size = !cache_size in + let array = Array_2.make size H.sentinel R.sentinel in + array, pred size + + let cache = lazy (create ()) let clear () = if Lazy.is_val cache then - Array_2.clear !!cache H.sentinel R.sentinel + let array, _ = Lazy.force cache in + Array_2.clear array H.sentinel R.sentinel let merge f a0 = + let array, mask = Lazy.force cache in let h0 = H.hash a0 in let has = h0 land mask in - if H.equal (Array_2.get0 !!cache has) a0 - then begin - (* Format.printf "Cache O@."; *) - Array_2.get1 !!cache has - end + if H.equal (Array_2.get0 array has) a0 + then + Array_2.get1 array has else let result = f a0 in - (* Format.printf "Cache N@."; *) - Array_2.set !!cache has a0 result; + Array_2.set array has a0 result; result end module Arity_Two (H0: Cacheable) (H1: Cacheable) (R: Result) = struct - let size = cache_size - let cache = lazy (Array_3.make size H0.sentinel H1.sentinel R.sentinel) - let mask = pred size + (* Creates the array used for the cache, and the mask to be used on keys + according to the array size. *) + let create () = + let size = !cache_size in + let array = Array_3.make size H0.sentinel H1.sentinel R.sentinel in + array, pred size + + let cache = lazy (create ()) let clear () = if Lazy.is_val cache then - Array_3.clear !!cache H0.sentinel H1.sentinel R.sentinel + let array, _ = Lazy.force cache in + Array_3.clear array H0.sentinel H1.sentinel R.sentinel let merge f a0 a1 = + let array, mask = Lazy.force cache in let h0 = H0.hash a0 in let h1 = H1.hash a1 in let has = h1 lsl 5 - h1 + h0 in let has = has land mask in - - if H0.equal (Array_3.get0 !!cache has) a0 - && H1.equal (Array_3.get1 !!cache has) a1 - then begin - (* Format.printf "Cache O@."; *) - Array_3.get2 !!cache has - end + if H0.equal (Array_3.get0 array has) a0 + && H1.equal (Array_3.get1 array has) a1 + then + Array_3.get2 array has else let result = f a0 a1 in - (* Format.printf "Cache N@."; *) - Array_3.set !!cache has a0 a1 result; + Array_3.set array has a0 a1 result; result end module Arity_Three (H0: Cacheable) (H1: Cacheable) (H2: Cacheable) (R: Result) = struct - let size = cache_size - let cache = - lazy (Array_4.make size H0.sentinel H1.sentinel H2.sentinel R.sentinel) - let mask = pred size + + (* Creates the array used for the cache, and the mask to be used on keys + according to the array size. *) + let create () = + let size = !cache_size in + let array = + Array_4.make size H0.sentinel H1.sentinel H2.sentinel R.sentinel + in + array, pred size + + let cache = lazy (create ()) let clear () = if Lazy.is_val cache then - Array_4.clear !!cache H0.sentinel H1.sentinel H2.sentinel R.sentinel + let array, _ = Lazy.force cache in + Array_4.clear array H0.sentinel H1.sentinel H2.sentinel R.sentinel let merge f a0 a1 a2 = + let array, mask = Lazy.force cache in let h0 = H0.hash a0 in let h1 = H1.hash a1 in let h2 = H2.hash a2 in let has = h0 + 117 * h1 + 2375 * h2 in let has = has land mask in - - if H0.equal (Array_4.get0 !!cache has) a0 - && H1.equal (Array_4.get1 !!cache has) a1 - && H2.equal (Array_4.get2 !!cache has) a2 - then begin - (* Format.printf "Cache O@."; *) - Array_4.get3 !!cache has - end + if H0.equal (Array_4.get0 array has) a0 + && H1.equal (Array_4.get1 array has) a1 + && H2.equal (Array_4.get2 array has) a2 + then + Array_4.get3 array has else let result = f a0 a1 a2 in - (* Format.printf "Cache N@."; *) - Array_4.set !!cache has a0 a1 a2 result; + Array_4.set array has a0 a1 a2 result; result end @@ -320,55 +322,65 @@ end module Binary_Predicate (H0: Cacheable) (H1: Cacheable) = struct - let size = cache_size - let cache = lazy (Array_2.make size H0.sentinel H1.sentinel) - let result = lazy (Array_Bit.make size) - let mask = pred size + + (* Creates two arrays (one for the arguments, one for the boolean result), + and the mask to be used on keys according to the array size. *) + let create () = + let size = !cache_size in + let array_args = Array_2.make size H0.sentinel H1.sentinel in + let array_result = Array_Bit.make size in + array_args, array_result, pred size + + let cache = lazy (create ()) let clear () = if Lazy.is_val cache then - Array_2.clear !!cache H0.sentinel H1.sentinel; - if Lazy.is_val result then - Array_Bit.clear !!result + let array_args, array_result, _ = Lazy.force cache in + Array_2.clear array_args H0.sentinel H1.sentinel; + Array_Bit.clear array_result let merge f a0 a1 = + let array_args, array_result, mask = Lazy.force cache in let has = let h0 = H0.hash a0 in let h1 = H1.hash a1 in 599 * h0 + h1 in let has = has land mask in - - if H0.equal (Array_2.get0 !!cache has) a0 - && H1.equal (Array_2.get1 !!cache has) a1 - then begin - (* Format.printf "Cache O@."; *) - Array_Bit.get !!result has - end + if H0.equal (Array_2.get0 array_args has) a0 + && H1.equal (Array_2.get1 array_args has) a1 + then + Array_Bit.get array_result has else let r = f a0 a1 in - (* Format.printf "Cache N@."; *) - Array_2.set !!cache has a0 a1; - Array_Bit.set !!result has r; + Array_2.set array_args has a0 a1; + Array_Bit.set array_result has r; r end module Symmetric_Binary_Predicate (H0: Cacheable) = struct - let size = cache_size - let cache = lazy (Array_2.make size H0.sentinel H0.sentinel) - let result = lazy (Array_Bit.make size) - let mask = pred size + + (* Creates two arrays (one for the arguments, one for the boolean result), + and the mask to be used on keys according to the array size. *) + let create () = + let size = !cache_size in + let array_args = Array_2.make size H0.sentinel H0.sentinel in + let array_result = Array_Bit.make size in + array_args, array_result, pred size + + let cache = lazy (create ()) let clear () = if Lazy.is_val cache then - Array_2.clear !!cache H0.sentinel H0.sentinel; - if Lazy.is_val result then - Array_Bit.clear !!result + let array_args, array_result, _ = Lazy.force cache in + Array_2.clear array_args H0.sentinel H0.sentinel; + Array_Bit.clear array_result let hash = H0.hash let merge f a0 a1 = + let array_args, array_result, mask = Lazy.force cache in let a0, a1, h0, h1 = let h0 = hash a0 in let h1 = hash a1 in @@ -379,18 +391,14 @@ struct let has = h1 lsl 5 - h1 + h0 in let has = has land mask in - - if H0.equal (Array_2.get0 !!cache has) a0 - && H0.equal (Array_2.get1 !!cache has) a1 - then begin - (* Format.printf "Cache O@."; *) - Array_Bit.get !!result has - end + if H0.equal (Array_2.get0 array_args has) a0 + && H0.equal (Array_2.get1 array_args has) a1 + then + Array_Bit.get array_result has else let r = f a0 a1 in - (* Format.printf "Cache N@."; *) - Array_2.set !!cache has a0 a1; - Array_Bit.set !!result has r; + Array_2.set array_args has a0 a1; + Array_Bit.set array_result has r; r end diff --git a/src/libraries/utils/binary_cache.mli b/src/libraries/utils/binary_cache.mli index 26cbfbbe786abb6b5fcdf103043b15f0ed47f96e..8bdf6b25361ebf9cab9e72420721464a1f50bf4f 100644 --- a/src/libraries/utils/binary_cache.mli +++ b/src/libraries/utils/binary_cache.mli @@ -24,11 +24,9 @@ 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]. *) +(** [set_cache_size n] sets the size cache to 2^(8+n). + Does not resize already created caches. *) +val set_cache_size: int -> unit module type Cacheable = sig type t 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..730527d6683647f52e77f1399b1cc961e5357cf2 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_name:"from cleanup" ~temporary:true - ~f ~joiner ~empty:Zone.bottom ~projection + Zone.cached_fold ~cache ~f ~joiner ~empty:Zone.bottom in let zone_substitution x = try diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t index 936b5c2b4d211b3752646aae45cb0632350e66be..c1ea52b1202a07498a027c651632c54d4d3ea4cc 100644 --- a/tests/fc_script/make-wrapper.t/run.t +++ b/tests/fc_script/make-wrapper.t/run.t @@ -11,7 +11,7 @@ verbose output for Make. [kernel] Parsing make-wrapper.c (with preprocessing) [kernel] Parsing make-wrapper2.c (with preprocessing) - Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix=active,garbled-mix:write=active -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort + Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix=active,garbled-mix:write=active -calldeps -from-verbose 0 -cache-size 8 -eva-warn-key builtins:missing-spec=abort [eva] Analyzing a complete application starting at main [eva:recursion] make-wrapper.c:17: