From 279f50eac63138b0c7d94b8197a38f96a5b0e3c9 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Thu, 16 Feb 2017 22:56:28 -0800 Subject: [PATCH] [infer][backend] make the on-demand analysis function return a summary Summary: A good first step in order to run multiple checkers together is to prevent the analysis the analysis to side effect on the summaries of the method being analyzed from disk, or the shared specs summary. The idea is that `Ondemand` creates a summary for the procedure being analyzed and only saves the summary once all the checkers have been run. The summary for the caller (i.e. the procedure being analyzed) should never be looked up from disk during the analysis. In other words, the analysis should only ever lookup the summaries of the callees and the proposed solution to enforce this is to have `Ondemand.analyze_proc_name` be the only way to lookup the summary of a procedure. Another objective is to make sure that the summaries are never saved to disk more than once. Reviewed By: sblackshear Differential Revision: D4549764 fbshipit-source-id: f0a6e21 --- infer/src/backend/interproc.ml | 2 +- infer/src/backend/ondemand.ml | 48 +++++++++++++++++++------------- infer/src/backend/ondemand.mli | 6 ++-- infer/src/backend/symExec.ml | 41 +++++++++++++-------------- infer/src/checkers/summary.ml | 2 +- infer/src/eradicate/typeCheck.ml | 2 +- 6 files changed, 55 insertions(+), 46 deletions(-) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index b89a4d53e..29e605679 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1405,7 +1405,7 @@ let interprocedural_algorithm exe_env : unit = List.filter ~f:filter_initial (Cg.get_defined_nodes call_graph) in let process_one_proc proc_name = let analyze proc_desc = - Ondemand.analyze_proc_desc ~propagate_exceptions:false proc_desc proc_desc in + ignore (Ondemand.analyze_proc_desc ~propagate_exceptions:false proc_desc proc_desc) in match Exe_env.get_proc_desc exe_env proc_name with | Some proc_desc when Config.reactive_mode (* in reactive mode, only analyze changed procedures *) diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index e94161d49..7a2b207d4 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -154,7 +154,8 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc timestamp = summary.Specs.timestamp + 1 } in Specs.add_summary callee_pname summary'; Checkers.ST.store_summary callee_pname; - Printer.write_proc_html source false callee_pdesc in + Printer.write_proc_html source false callee_pdesc; + summary' in let log_error_and_continue exn kind = Reporting.log_error callee_pname exn; @@ -165,14 +166,16 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc { prev_summary.Specs.payload with Specs.preposts = Some []; } in let new_summary = { prev_summary with Specs.stats; payload; timestamp; } in - Specs.add_summary callee_pname new_summary in + Specs.add_summary callee_pname new_summary; + new_summary in let old_state = save_global_state () in let source = preprocess () in try analyze_proc source callee_pdesc; - postprocess source; + let summary = postprocess source in restore_global_state old_state; + summary with exn -> L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.BACK TRACE@.%s@?" Procname.pp callee_pname @@ -193,32 +196,39 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc log_error_and_continue exn (FKcrash (Exn.to_string exn)) -let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc = +let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc : Specs.summary option = let callee_pname = Procdesc.get_proc_name callee_pdesc in let proc_attributes = Procdesc.get_attributes callee_pdesc in match !callbacks_ref with - | Some callbacks - when should_be_analyzed callee_pname proc_attributes -> - run_proc_analysis ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc - | _ -> () + | Some callbacks -> + if should_be_analyzed callee_pname proc_attributes then + let summary = + run_proc_analysis + ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc in + Some summary + else + Specs.get_summary callee_pname + | None -> None (** analyze_proc_name curr_pdesc proc_name performs an on-demand analysis of proc_name triggered during the analysis of curr_pname. *) -let analyze_proc_name ~propagate_exceptions curr_pdesc callee_pname = - +let analyze_proc_name ~propagate_exceptions curr_pdesc callee_pname : Specs.summary option = match !callbacks_ref with - | Some callbacks - when procedure_should_be_analyzed callee_pname -> - begin - match callbacks.get_proc_desc callee_pname with - | Some callee_pdesc -> analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc - | None -> () - end - | _ -> - () (* skipping *) + | Some callbacks -> + if procedure_should_be_analyzed callee_pname then + begin + match callbacks.get_proc_desc callee_pname with + | Some callee_pdesc -> + analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc + | None -> None + end + else + Specs.get_summary callee_pname + | None -> None + (** Find a proc desc for the procedure, perhaps loading it from disk. *) let get_proc_desc callee_pname = diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index dac0413e1..deea928d3 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -31,12 +31,14 @@ val get_proc_desc : get_proc_desc (** analyze_proc_desc curr_pdesc callee_pdesc performs an on-demand analysis of callee_pdesc triggered during the analysis of curr_pdesc. *) -val analyze_proc_desc : propagate_exceptions:bool -> Procdesc.t -> Procdesc.t -> unit +val analyze_proc_desc : + propagate_exceptions:bool -> Procdesc.t -> Procdesc.t -> Specs.summary option (** analyze_proc_name curr_pdesc proc_name performs an on-demand analysis of proc_name triggered during the analysis of curr_pdesc. *) -val analyze_proc_name : propagate_exceptions:bool -> Procdesc.t -> Procname.t -> unit +val analyze_proc_name : + propagate_exceptions:bool -> Procdesc.t -> Procname.t -> Specs.summary option (** Check if the procedure called needs to be analyzed. *) val procedure_should_be_analyzed : Procname.t -> bool diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index b1916b6b6..b532dbda5 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -636,34 +636,32 @@ let resolve_java_pname tenv prop args pname_java call_flags : Procname.java = if not already analyzed *) let resolve_and_analyze tenv caller_pdesc prop args callee_proc_name call_flags : Procname.t * Specs.summary option = - (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name + (* TODO (#15748878): Fix conflict with method overloading by encoding in the procedure name whether the method is defined or generated by the specialization *) - let analyze_ondemand resolved_pname : unit = + let analyze_ondemand resolved_pname : Specs.summary option = if Procname.equal resolved_pname callee_proc_name then Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_proc_name else (* Create the type sprecialized procedure description and analyze it directly *) - Option.iter - ~f:(fun specialized_pdesc -> - Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc) - (match Ondemand.get_proc_desc resolved_pname with - | Some resolved_proc_desc -> - Some resolved_proc_desc - | None -> - begin - Option.map - ~f:(fun callee_proc_desc -> - Cfg.specialize_types callee_proc_desc resolved_pname args) - (Ondemand.get_proc_desc callee_proc_name) - end) in + let analyze specialized_pdesc = + Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc in + let resolved_proc_desc_option = + match Ondemand.get_proc_desc resolved_pname with + | Some resolved_proc_desc -> + Some resolved_proc_desc + | None -> + (Option.map + ~f:(fun callee_proc_desc -> + Cfg.specialize_types callee_proc_desc resolved_pname args) + (Ondemand.get_proc_desc callee_proc_name)) in + Option.bind resolved_proc_desc_option analyze in let resolved_pname = match callee_proc_name with | Procname.Java callee_proc_name_java -> Procname.Java (resolve_java_pname tenv prop args callee_proc_name_java call_flags) | _ -> callee_proc_name in - analyze_ondemand resolved_pname; - resolved_pname, Specs.get_summary resolved_pname + resolved_pname, analyze_ondemand resolved_pname (** recognize calls to the constructor java.net.URL and splits the argument string @@ -1087,10 +1085,9 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let resolved_pnames = resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in let exec_one_pname pname = - Ondemand.analyze_proc_name ~propagate_exceptions:true current_pdesc pname; let exec_skip_call ret_annots ret_type = skip_call norm_prop path pname ret_annots loc ret_id (Some ret_type) url_handled_args in - match Specs.get_summary pname with + match Ondemand.analyze_proc_name ~propagate_exceptions:true current_pdesc pname with | None -> let ret_typ = Typ.java_proc_return_typ callee_pname_java in let ret_annots = load_ret_annots callee_pname in @@ -1110,8 +1107,9 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with | resolved_pname :: _ -> resolved_pname | [] -> callee_pname in - Ondemand.analyze_proc_name - ~propagate_exceptions:true current_pdesc resolved_pname; + let resolved_summary_opt = + Ondemand.analyze_proc_name + ~propagate_exceptions:true current_pdesc resolved_pname in let callee_pdesc_opt = Ondemand.get_proc_desc resolved_pname in let ret_typ_opt = Option.map ~f:Procdesc.get_ret_type callee_pdesc_opt in let sentinel_result = @@ -1120,7 +1118,6 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path (call_args prop_r callee_pname actual_params ret_id loc) else [(prop_r, path)] in let do_call (prop, path) = - let resolved_summary_opt = Specs.get_summary resolved_pname in if Option.value_map ~f:call_should_be_skipped ~default:true resolved_summary_opt then (* If it's an ObjC getter or setter, call the builtin rather than skipping *) let attrs_opt = diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml index be05f1812..3cc41fcec 100644 --- a/infer/src/checkers/summary.ml +++ b/infer/src/checkers/summary.ml @@ -46,7 +46,7 @@ module Make (H : Helper) = struct failwithf "Summary for %a should exist, but does not!@." Procname.pp pname let read_summary caller_pdesc callee_pname = - Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname; + ignore (Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname); match Specs.get_summary callee_pname with | None -> None | Some summary -> H.read_from_payload summary.Specs.payload diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 6ce0c9ac5..5a41eaeb3 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -566,7 +566,7 @@ let typecheck_instr loc, cflags) -> - Ondemand.analyze_proc_name ~propagate_exceptions:true curr_pdesc callee_pname; + ignore (Ondemand.analyze_proc_name ~propagate_exceptions:true curr_pdesc callee_pname); let callee_attributes = match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with | Some proc_attributes ->