From 793911c847ac93241da23fb07589e7db07fc851a Mon Sep 17 00:00:00 2001 From: jrm Date: Wed, 9 Mar 2016 16:33:47 -0800 Subject: [PATCH] Add the possibility to analyze procedure descriptions on-demand without serialization Summary:public In order to implement the lazy dynamic dispatch algorithm, we need to generate a procedure description based on the types encountered during the symbolic execution. This diff adds support for analyzing such a prodecure description directly, without having to first serialize it to disk, which is slow and not necessary. Reviewed By: cristianoc Differential Revision: D3028226 fb-gh-sync-id: 1b2360e shipit-source-id: 1b2360e --- infer/src/backend/cfg.ml | 45 ++--- infer/src/backend/cfg.mli | 3 +- infer/src/backend/interproc.ml | 27 ++- infer/src/backend/ondemand.ml | 203 ++++++++++++---------- infer/src/backend/ondemand.mli | 13 +- infer/src/backend/symExec.ml | 41 ++--- infer/src/checkers/performanceCritical.ml | 8 +- infer/src/eradicate/eradicate.ml | 17 +- infer/src/eradicate/typeCheck.ml | 2 +- 9 files changed, 181 insertions(+), 178 deletions(-) diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index 7edfc23e3..eb7c72938 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -701,7 +701,7 @@ module Node = struct new_node in converted_node :: (loop other_node) in ignore (loop [callee_start_node]); - pdesc_tbl_add cfg resolved_proc_name resolved_proc_desc + resolved_proc_desc end (* =============== END of module Node =============== *) @@ -1151,30 +1151,21 @@ let specialize_types caller_cfg callee_proc_name resolved_proc_name args = (** TODO (#9333890): This currently only works when the callee is defined in the same file. Add support to search for the callee procedure description in the execution environment *) match Procdesc.find_from_name caller_cfg resolved_proc_name with - | Some _ -> () + | Some pdesc -> Some pdesc | None -> - begin - match Procdesc.find_from_name caller_cfg callee_proc_name with - | None -> () - | Some callee_proc_desc -> - let callee_attributes = Procdesc.get_attributes callee_proc_desc in - let resolved_formals = - IList.fold_left2 - (fun accu (name, _) (_, arg_typ) -> (name, arg_typ) :: accu) - [] callee_attributes.ProcAttributes.formals args |> IList.rev in - let resolved_attributes = - { callee_attributes with - ProcAttributes.formals = resolved_formals; - proc_name = resolved_proc_name; - } in - AttributesTable.store_attributes resolved_attributes; - Procdesc.specialize_types - caller_cfg callee_proc_desc resolved_attributes resolved_formals; - begin - let source_file = resolved_attributes.ProcAttributes.loc.Location.file in - let source_dir = DB.source_dir_from_source_file source_file in - let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in - let save_sources = false in - store_cfg_to_file cfg_file save_sources caller_cfg - end - end + Option.map + (fun callee_proc_desc -> + let callee_attributes = Procdesc.get_attributes callee_proc_desc in + let resolved_formals = + IList.fold_left2 + (fun accu (name, _) (_, arg_typ) -> (name, arg_typ) :: accu) + [] callee_attributes.ProcAttributes.formals args |> IList.rev in + let resolved_attributes = + { callee_attributes with + ProcAttributes.formals = resolved_formals; + proc_name = resolved_proc_name; + } in + AttributesTable.store_attributes resolved_attributes; + Procdesc.specialize_types + caller_cfg callee_proc_desc resolved_attributes resolved_formals) + (Procdesc.find_from_name caller_cfg callee_proc_name) diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index 67d8a560d..c8e3de0de 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -317,4 +317,5 @@ val remove_seed_captured_vars_block : Mangled.t list -> Prop.normal Prop.t -> Pr (name, typ) where name is a parameter. The resulting procedure CFG is isomorphic but all the type of the parameters are replaced in the instructions according to the list. The virtual calls are also replaced to match the parameter types *) -val specialize_types : cfg -> Procname.t -> Procname.t -> (Sil.exp * Sil.typ) list -> unit +val specialize_types : + cfg -> Procname.t -> Procname.t -> (Sil.exp * Sil.typ) list -> Procdesc.t option diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index ca6e1c714..c3ca5beb1 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1280,7 +1280,7 @@ let interprocedural_algorithm exe_env : unit = let process_one_proc proc_name = match to_analyze proc_name with | Some pdesc -> - Ondemand.do_analysis ~propagate_exceptions:false pdesc proc_name + Ondemand.analyze_proc_name ~propagate_exceptions:false pdesc proc_name | None -> () in IList.iter process_one_proc procs_to_analyze @@ -1323,20 +1323,17 @@ let do_analysis exe_env = let get_proc_desc proc_name = let callee_cfg = Exe_env.get_cfg exe_env proc_name in Cfg.Procdesc.find_from_name callee_cfg proc_name in - let analyze_ondemand proc_name = - match get_proc_desc proc_name with - | Some proc_desc -> - let summaryfp = - run_in_footprint_mode (analyze_proc exe_env) proc_desc in - Specs.add_summary proc_name summaryfp; - - perform_transition exe_env proc_name; - - let summaryre = - run_in_re_execution_mode (analyze_proc exe_env) proc_desc in - Specs.add_summary proc_name summaryre - | None -> - () in + let analyze_ondemand proc_desc = + let proc_name = Cfg.Procdesc.get_proc_name proc_desc in + let summaryfp = + run_in_footprint_mode (analyze_proc exe_env) proc_desc in + Specs.add_summary proc_name summaryfp; + + perform_transition exe_env proc_name; + + let summaryre = + run_in_re_execution_mode (analyze_proc exe_env) proc_desc in + Specs.add_summary proc_name summaryre in { Ondemand.analyze_ondemand; get_cfg; diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 589f65559..77f012058 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -39,7 +39,7 @@ let read_dirs_to_analyze () = let dirs_to_analyze = lazy (read_dirs_to_analyze ()) -type analyze_ondemand = Procname.t -> unit +type analyze_ondemand = Cfg.Procdesc.t -> unit type get_cfg = Procname.t -> Cfg.cfg option @@ -62,21 +62,24 @@ let unset_callbacks () = let nesting = ref 0 +let should_be_analyzed proc_attributes proc_name = + let currently_analyzed () = + Specs.summary_exists proc_name && + Specs.is_active proc_name in + let already_analyzed () = + match Specs.get_summary proc_name with + | Some summary -> + Specs.get_timestamp summary > 0 + | None -> + false in + proc_attributes.ProcAttributes.is_defined && (* we have the implementation *) + not (currently_analyzed ()) && (* avoid infinite loops *) + not (already_analyzed ()) (* avoid re-analysis of the same procedure *) + let procedure_should_be_analyzed proc_name = match AttributesTable.load_attributes proc_name with | Some proc_attributes -> - let currently_analyzed = - Specs.summary_exists proc_name && - Specs.is_active proc_name in - let already_analyzed = match Specs.get_summary proc_name with - | Some summary -> - Specs.get_timestamp summary > 0 - | None -> - false in - - proc_attributes.ProcAttributes.is_defined && (* we have the implementation *) - not currently_analyzed && (* avoid infinite loops *) - not already_analyzed (* avoid re-analysis of the same procedure *) + should_be_analyzed proc_attributes proc_name | None -> false @@ -117,86 +120,102 @@ let restore_global_state st = State.restore_state st.symexec_state; Timeout.resume_previous_timeout () -(** do_analysis curr_pdesc proc_name - performs an on-demand analysis of proc_name - triggered during the analysis of curr_pname. *) -let do_analysis ~propagate_exceptions curr_pdesc callee_pname = + +let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc = let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in + let callee_pname = Cfg.Procdesc.get_proc_name callee_pdesc in + + (** Dot means start of a procedure *) + L.log_progress_procedure (); + if trace () then L.stderr "[%d] run_proc_analysis %a -> %a@." + !nesting + Procname.pp curr_pname + Procname.pp callee_pname; + + let preprocess () = + incr nesting; + let attributes_opt = + Specs.proc_resolve_attributes callee_pname in + Option.may + (fun attribute -> + DB.current_source := attribute.ProcAttributes.loc.Location.file; + let attribute_pname = attribute.ProcAttributes.proc_name in + if not (Procname.equal callee_pname attribute_pname) then + failwith ("ERROR: "^(Procname.to_string callee_pname) + ^" not equal to "^(Procname.to_string attribute_pname))) + attributes_opt; + let call_graph = + let cg = Cg.create () in + Cg.add_defined_node cg callee_pname; + cg in + Specs.reset_summary call_graph callee_pname attributes_opt; + Specs.set_status callee_pname Specs.ACTIVE in + + let postprocess () = + decr nesting; + let summary = Specs.get_summary_unsafe "ondemand" callee_pname in + let summary' = + { summary with + Specs.status = Specs.INACTIVE; + timestamp = summary.Specs.timestamp + 1 } in + Specs.add_summary callee_pname summary'; + Checkers.ST.store_summary callee_pname; + Printer.proc_write_log false callee_pdesc in + + let log_error_and_continue exn kind = + Reporting.log_error callee_pname exn; + let prev_summary = Specs.get_summary_unsafe "Ondemand.do_analysis" callee_pname in + let timestamp = max 1 (prev_summary.Specs.timestamp) in + let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in + let payload = + { 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 + + let old_state = save_global_state () in + preprocess (); + try + analyze_proc callee_pdesc; + postprocess (); + restore_global_state old_state; + with exn -> + L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.CALL STACK@.%s@.BACK TRACE@.%s@." + Procname.pp callee_pname + (Printexc.to_string exn) + (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000)) + (Printexc.get_backtrace ()); + restore_global_state old_state; + if propagate_exceptions + then + raise exn + else + match exn with + | Analysis_failure_exe kind -> + (* in production mode, log the timeout/crash and continue with the summary we had before + the failure occurred *) + log_error_and_continue exn kind + | _ -> + (* this happens with assert false or some other unrecognized exception *) + log_error_and_continue exn (FKcrash (Printexc.to_string exn)) + + +let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc = + let callee_pname = Cfg.Procdesc.get_proc_name callee_pdesc in + let proc_attributes = Cfg.Procdesc.get_attributes callee_pdesc in + match !callbacks_ref with + | Some callbacks + when should_be_analyzed proc_attributes callee_pname -> + run_proc_analysis + ~propagate_exceptions callbacks.analyze_ondemand curr_pdesc callee_pdesc + | _ -> () + - let really_do_analysis callee_pdesc analyze_proc = - (** Dot means start of a procedure *) - L.log_progress_procedure (); - if trace () then L.stderr "[%d] really_do_analysis %a -> %a@." - !nesting - Procname.pp curr_pname - Procname.pp callee_pname; - - let preprocess () = - incr nesting; - let attributes_opt = - Specs.proc_resolve_attributes callee_pname in - Option.may - (fun attribute -> - DB.current_source := attribute.ProcAttributes.loc.Location.file; - let attribute_pname = attribute.ProcAttributes.proc_name in - if not (Procname.equal callee_pname attribute_pname) then - failwith ("ERROR: "^(Procname.to_string callee_pname) - ^" not equal to "^(Procname.to_string attribute_pname))) - attributes_opt; - let call_graph = - let cg = Cg.create () in - Cg.add_defined_node cg callee_pname; - cg in - Specs.reset_summary call_graph callee_pname attributes_opt; - Specs.set_status callee_pname Specs.ACTIVE in - - let postprocess () = - decr nesting; - let summary = Specs.get_summary_unsafe "ondemand" callee_pname in - let summary' = - { summary with - Specs.status = Specs.INACTIVE; - timestamp = summary.Specs.timestamp + 1 } in - Specs.add_summary callee_pname summary'; - Checkers.ST.store_summary callee_pname; - Printer.proc_write_log false callee_pdesc in - - let log_error_and_continue exn kind = - Reporting.log_error callee_pname exn; - let prev_summary = Specs.get_summary_unsafe "Ondemand.do_analysis" callee_pname in - let timestamp = max 1 (prev_summary.Specs.timestamp) in - let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in - let payload = - { 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 - - let old_state = save_global_state () in - preprocess (); - try - analyze_proc callee_pname; - postprocess (); - restore_global_state old_state; - with exn -> - L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.CALL STACK@.%s@.BACK TRACE@.%s@." - Procname.pp callee_pname - (Printexc.to_string exn) - (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000)) - (Printexc.get_backtrace ()); - restore_global_state old_state; - if propagate_exceptions - then - raise exn - else - match exn with - | Analysis_failure_exe kind -> - (* in production mode, log the timeout/crash and continue with the summary we had before - the failure occurred *) - log_error_and_continue exn kind - | _ -> - (* this happens with assert false or some other unrecognized exception *) - log_error_and_continue exn (FKcrash (Printexc.to_string exn)) in + +(** 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 = match !callbacks_ref with | Some callbacks @@ -204,7 +223,7 @@ let do_analysis ~propagate_exceptions curr_pdesc callee_pname = begin match callbacks.get_proc_desc callee_pname with | Some callee_pdesc -> - really_do_analysis callee_pdesc callbacks.analyze_ondemand + analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc | None -> () end diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index a4a681795..2c20500f5 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -12,7 +12,7 @@ (** Optional set of source dirs to analyze in on-demand mode. *) val dirs_to_analyze : StringSet.t option Lazy.t -type analyze_ondemand = Procname.t -> unit +type analyze_ondemand = Cfg.Procdesc.t -> unit type get_cfg = Procname.t -> Cfg.cfg option @@ -28,10 +28,15 @@ type callbacks = (** Find a cfg for the procedure, perhaps loading it from disk. *) val get_cfg : get_cfg -(** do_analysis curr_pdesc proc_name +(** 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 -> Cfg.Procdesc.t -> Cfg.Procdesc.t -> unit + +(** analyze_proc_name curr_pdesc proc_name performs an on-demand analysis of proc_name - triggered during the analysis of curr_pname. *) -val do_analysis : propagate_exceptions:bool -> Cfg.Procdesc.t -> Procname.t -> unit + triggered during the analysis of curr_pdesc. *) +val analyze_proc_name : propagate_exceptions:bool -> Cfg.Procdesc.t -> Procname.t -> unit (** 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 2c3cdf373..95d69fed6 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -716,27 +716,23 @@ let resolve_java_pname tenv prop args pname call_flags : Procname.t = if not already analyzed *) let resolve_and_analyze tenv caller_pdesc prop args callee_pname call_flags : Procname.t * Specs.summary option = - let resolved_pname = - (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name - whether the method is defined or generated by the specialization *) - let res_pname = - resolve_java_pname tenv prop args callee_pname call_flags in - if Procname.equal res_pname callee_pname - then - callee_pname + (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name + whether the method is defined or generated by the specialization *) + let analyze_ondemand caller_cfg resolved_pname : unit = + if Procname.equal resolved_pname callee_pname then + Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_pname else - begin - if not (Specs.summary_exists res_pname) then - begin - match Ondemand.get_cfg (Cfg.Procdesc.get_proc_name caller_pdesc) with - | Some caller_cfg -> - Cfg.specialize_types caller_cfg callee_pname res_pname args - | None -> - () - end; - res_pname - end in - Ondemand.do_analysis ~propagate_exceptions:true caller_pdesc resolved_pname; + (* Create the type sprecialized procedure description and analyze it directly *) + Option.may + (fun specialized_pdesc -> + Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc) + (Cfg.specialize_types caller_cfg callee_pname resolved_pname args) in + let resolved_pname = + resolve_java_pname tenv prop args callee_pname call_flags in + Option.may + (fun caller_cfg -> + analyze_ondemand caller_cfg resolved_pname) + (Ondemand.get_cfg (Cfg.Procdesc.get_proc_name caller_pdesc)); resolved_pname, Specs.get_summary resolved_pname @@ -1083,7 +1079,6 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path proc_name = callee_pname; loc; } - | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) when !Config.curr_language = Config.Java && Config.lazy_dynamic_dispatch -> let norm_prop, norm_args = normalize_params pname prop_ actual_params in @@ -1115,7 +1110,7 @@ let rec sym_exec tenv 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.do_analysis ~propagate_exceptions:true pdesc pname; + Ondemand.analyze_proc_name ~propagate_exceptions:true pdesc pname; let exec_skip_call ret_type = skip_call norm_prop path pname loc ret_ids (Some ret_type) url_handled_args in match Specs.get_summary pname with @@ -1140,7 +1135,7 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path | resolved_pname :: _ -> resolved_pname | [] -> callee_pname in - Ondemand.do_analysis ~propagate_exceptions:true pdesc resolved_pname; + Ondemand.analyze_proc_name ~propagate_exceptions:true pdesc resolved_pname; let callee_pdesc_opt = match Ondemand.get_cfg pname with diff --git a/infer/src/checkers/performanceCritical.ml b/infer/src/checkers/performanceCritical.ml index ff8ebec92..db2f95b09 100644 --- a/infer/src/checkers/performanceCritical.ml +++ b/infer/src/checkers/performanceCritical.ml @@ -159,7 +159,7 @@ let collect_calls tenv caller_pdesc checked_pnames call_summary (pname, _) = if Procname.Set.mem pname !checked_pnames then call_summary else begin - Ondemand.do_analysis ~propagate_exceptions:true caller_pdesc pname; + Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc pname; checked_pnames := Procname.Set.add pname !checked_pnames; let call_loc = lookup_location pname in let updated_expensive_calls = @@ -317,10 +317,8 @@ let check_one_procedure tenv pname pdesc = let callback_performance_checker { Callbacks.get_cfg; get_proc_desc; proc_desc; proc_name; tenv } = let callbacks = - let analyze_ondemand pn = - match get_proc_desc pn with - | None -> () - | Some pd -> check_one_procedure tenv pn pd in + let analyze_ondemand pdesc = + check_one_procedure tenv (Cfg.Procdesc.get_proc_name pdesc) pdesc in { Ondemand.analyze_ondemand; get_cfg; diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index b4b1ce7ec..282fd1b94 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -394,16 +394,13 @@ let callback_eradicate check_ret_type = []; } in let callbacks = - let analyze_ondemand pname = - match get_proc_desc pname with - | None -> () - | Some pdesc -> - let idenv_pname = Idenv.create_from_idenv idenv pdesc in - Main.callback checks - { callback_args with - Callbacks.idenv = idenv_pname; - proc_name = pname; - proc_desc = pdesc; } in + let analyze_ondemand pdesc = + let idenv_pname = Idenv.create_from_idenv idenv pdesc in + Main.callback checks + { callback_args with + Callbacks.idenv = idenv_pname; + proc_name = (Cfg.Procdesc.get_proc_name pdesc); + proc_desc = pdesc; } in { Ondemand.analyze_ondemand; get_cfg; diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 9cf04be33..6d0621109 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -556,7 +556,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc typestate (* skip othe builtins *) | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags) when Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname <> None -> - Ondemand.do_analysis ~propagate_exceptions:true curr_pdesc callee_pname; + 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 -> proc_attributes