[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

@@ -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 =

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
     | [] ->

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] *)