From 489c55487bfeb1e147f3be558d3b5b4bc16035db Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 29 Jul 2021 12:05:01 -0700 Subject: [PATCH] [ondemand] only look at capture DB or model summaries for CFGs Summary: Ondemand should not analyse a pre-analysed CFG so we should never load a summary to get its CFG in Ondemand. The only exception is if the function is a model, where its (pre-analysed) CFG only lives in a summary. This diff eliminates the general look for a summary and only uses it if the function is a model, otherwise it looks in the capture DB. Reviewed By: da319 Differential Revision: D29932885 fbshipit-source-id: 781ddf51d --- infer/src/backend/ondemand.ml | 5 ++--- infer/src/istd/IList.ml | 2 -- infer/src/istd/IList.mli | 4 ---- 3 files changed, 2 insertions(+), 9 deletions(-) diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index fbef91a49..0f9f37516 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -297,9 +297,8 @@ let register_callee ?caller_summary callee_pname = let get_proc_desc callee_pname = - IList.force_until_first_some - [ lazy (Procdesc.load callee_pname) - ; lazy (Option.map ~f:Summary.get_proc_desc (Summary.OnDisk.get callee_pname)) ] + if BiabductionModels.mem callee_pname then Summary.OnDisk.get_model_proc_desc callee_pname + else Procdesc.load callee_pname let analyze_callee exe_env ?caller_summary callee_pname = diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index 9f8146e7d..1741194e1 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -182,8 +182,6 @@ let remove_first = fun list ~f -> aux list ~f [] -let force_until_first_some lazies = List.find_map lazies ~f:Lazy.force - let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf = let rec aux n = function | [] -> diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 0abba83db..6c070f855 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -46,10 +46,6 @@ val opt_cons : 'a option -> 'a list -> 'a list val remove_first : 'a list -> f:('a -> bool) -> 'a list option -val force_until_first_some : 'a option lazy_t list -> 'a option -(** [force_until_first_some xs] forces the computation of each element of [xs] and returns the first - that matches (Some _); or, if no such element exists, it returns None. *) - val eval_until_first_some : (unit -> 'a option) list -> 'a option (** given a list of functions taking unit, evaluate and return the first one to return [Some x] *)