From 7a1e901c8331e11841e50b5c36a697cf827a54b4 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 4 Mar 2020 07:44:28 -0800 Subject: [PATCH] [inferbo] Keep only one invariant map in the cache Summary: Invariant map of Inferbo, a map from node to abstract memory, is used in other checkers. In order to avoid duplicated Inferbo analyses, it caches calculated invariant maps independently to summary DB. The reason is that Inferbo's summary contains one abstract memory of the exit node, rather than a map from all nodes to abstract memories. This diff changes it to keep only one invariant map at a time. Since registered checkers are applied to the same function one by one, usually the singleton cache should be enough to avoid the duplicated Inferbo running. (I can think of a corner case when multiple checkers depend on Inferbo's results and Inferbo's modeled functions are different to that of them, but it should work in most of the cases.) Reviewed By: jvillard Differential Revision: D20248172 fbshipit-source-id: db86655d0 --- .../bufferoverrun/bufferOverrunAnalysis.ml | 25 +++++++------------ 1 file changed, 9 insertions(+), 16 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 350f33def..18ed86a61 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -456,23 +456,17 @@ let compute_invariant_map : let cached_compute_invariant_map = - (* Use a weak Hashtbl to prevent memory leaks (GC unnecessarily keeps invariant maps around) *) - let module WeakInvMapHashTbl = Caml.Weak.Make (struct - type t = Procname.t * invariant_map option - - let equal (pname1, _) (pname2, _) = Procname.equal pname1 pname2 - - let hash (pname, _) = Hashtbl.hash pname - end) in - let inv_map_cache = WeakInvMapHashTbl.create 100 in + let cache = ref None in + let cache_get pname = + Option.bind !cache ~f:(fun (pname', inv_map) -> + Option.some_if (Procname.equal pname pname') inv_map ) + in + let cache_set pname inv_map = cache := Some (pname, inv_map) in fun summary tenv integer_type_widths -> let pname = Summary.get_proc_name summary in - match WeakInvMapHashTbl.find_opt inv_map_cache (pname, None) with - | Some (_, Some inv_map) -> + match cache_get pname with + | Some inv_map -> inv_map - | Some (_, None) -> - (* this should never happen *) - assert false | None -> let get_summary callee_pname = Payload.read ~caller_summary:summary ~callee_pname in let get_formals callee_pname = @@ -481,8 +475,7 @@ let cached_compute_invariant_map = let inv_map = compute_invariant_map summary tenv integer_type_widths get_summary get_formals in - WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) ; - inv_map + cache_set pname inv_map ; inv_map let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_summary =