From f519d3e183231f5c944e1589ef4d276e6d17cf71 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Apr 2020 03:00:01 -0700 Subject: [PATCH] Interproc free of SummaryReporting Summary: most progress Reviewed By: mityal Differential Revision: D21261644 fbshipit-source-id: 8da2a8401 --- infer/src/biabduction/State.ml | 7 +++--- infer/src/biabduction/State.mli | 5 ++-- infer/src/biabduction/interproc.ml | 40 ++++++++++++++++-------------- 3 files changed, 27 insertions(+), 25 deletions(-) diff --git a/infer/src/biabduction/State.ml b/infer/src/biabduction/State.ml index fbbd34b4e..6457668b7 100644 --- a/infer/src/biabduction/State.ml +++ b/infer/src/biabduction/State.ml @@ -233,10 +233,9 @@ let mark_instr_fail exn = fs.instr_fail <- fs.instr_fail + 1 -type log_issue = - Procname.t -> ?node:Procdesc.Node.t -> ?loc:Location.t -> ?ltr:Errlog.loc_trace -> exn -> unit +type log_issue = ?node:Procdesc.Node.t -> ?loc:Location.t -> ?ltr:Errlog.loc_trace -> exn -> unit -let process_execution_failures (log_issue : log_issue) pname = +let process_execution_failures (log_issue : log_issue) = let do_failure _ fs = (* L.out "Node:%a node_ok:%d node_fail:%d@." Procdesc.Node.pp node fs.node_ok fs.node_fail; *) match (fs.node_ok, fs.first_failure) with @@ -244,7 +243,7 @@ let process_execution_failures (log_issue : log_issue) pname = let error = Exceptions.recognize_exception exn in let desc' = Localise.verbatim_desc ("exception: " ^ error.name.IssueType.unique_id) in let exn' = Exceptions.Analysis_stops (desc', error.ocaml_pos) in - log_issue pname ~loc ~node ~ltr:loc_trace exn' + log_issue ~loc ~node ~ltr:loc_trace exn' | _ -> () in diff --git a/infer/src/biabduction/State.mli b/infer/src/biabduction/State.mli index f0ac66954..c38e63098 100644 --- a/infer/src/biabduction/State.mli +++ b/infer/src/biabduction/State.mli @@ -58,10 +58,9 @@ val mk_find_duplicate_nodes : Procdesc.t -> Procdesc.Node.t -> Procdesc.NodeSet. (** Create a function to find duplicate nodes. A node is a duplicate of another one if they have the same kind and location and normalized (w.r.t. renaming of let - bound ids) list of instructions. *) -type log_issue = - Procname.t -> ?node:Procdesc.Node.t -> ?loc:Location.t -> ?ltr:Errlog.loc_trace -> exn -> unit +type log_issue = ?node:Procdesc.Node.t -> ?loc:Location.t -> ?ltr:Errlog.loc_trace -> exn -> unit -val process_execution_failures : log_issue -> Procname.t -> unit +val process_execution_failures : log_issue -> unit (** Process the failures during symbolic execution of a procedure *) val reset : unit -> unit diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 7e4a40099..71d7a4477 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -385,7 +385,8 @@ let do_symbolic_execution ({InterproceduralAnalysis.tenv; _} as analysis_data) p pset -let forward_tabulate ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_cfg summary wl = +let forward_tabulate ({InterproceduralAnalysis.proc_desc; err_log; tenv; _} as analysis_data) + proc_cfg summary wl = let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let handle_exn_node curr_node exn = Exceptions.print_exception_html "Failure of symbolic execution: " exn ; @@ -401,7 +402,8 @@ let forward_tabulate ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_c L.d_strln "SIL INSTR:" ; Procdesc.Node.d_instrs ~highlight:(AnalysisState.get_instr ()) curr_node ; L.d_ln () ; - SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ; + let attrs = Procdesc.get_attributes proc_desc in + BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Error exn ; State.mark_instr_fail exn in let exe_iter f pathset = @@ -476,9 +478,9 @@ let forward_tabulate ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_c (** Remove locals and formals, and check if the address of a stack variable is left in the result *) -let remove_locals_formals_and_check tenv proc_cfg p = +let remove_locals_formals_and_check {InterproceduralAnalysis.proc_desc; err_log; tenv; _} proc_cfg p + = let pdesc = ProcCfg.Exceptional.proc_desc proc_cfg in - let pname = Procdesc.get_proc_name pdesc in let pvars, p' = PropUtil.remove_locals_formals tenv pdesc p in let check_pvar pvar = if not (Pvar.is_frontend_tmp pvar) then @@ -486,17 +488,18 @@ let remove_locals_formals_and_check tenv proc_cfg p = let dexp_opt, _ = Errdesc.vpath_find tenv p (Exp.Lvar pvar) in let desc = Errdesc.explain_stack_variable_address_escape loc pvar dexp_opt in let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in - SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn + let attrs = Procdesc.get_attributes proc_desc in + BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning exn in List.iter ~f:check_pvar pvars ; p' (** Collect the analysis results for the exit node. *) -let collect_analysis_result tenv wl proc_cfg : Paths.PathSet.t = +let collect_analysis_result analysis_data wl proc_cfg : Paths.PathSet.t = let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in let exit_node_id = ProcCfg.Exceptional.Node.id exit_node in let pathset = htable_retrieve wl.Worklist.path_set_visited exit_node_id in - Paths.PathSet.map (remove_locals_formals_and_check tenv proc_cfg) pathset + Paths.PathSet.map (remove_locals_formals_and_check analysis_data proc_cfg) pathset let vset_add_path vset path = @@ -528,7 +531,8 @@ let compute_visited vset = (* Extract specs from a pathset, after the footprint phase. The postconditions will be thrown away by the re-execution phase, but they are first used to detect custom errors. *) -let extract_specs analysis_data tenv pdesc pathset : Prop.normal BiabductionSummary.spec list = +let extract_specs ({InterproceduralAnalysis.tenv; _} as analysis_data) pdesc pathset : + Prop.normal BiabductionSummary.spec list = if not !BiabductionConfig.footprint then L.die InternalError "Interproc.extract_specs should not be used for footprint but not for re-execution, because \ @@ -577,7 +581,7 @@ let extract_specs analysis_data tenv pdesc pathset : Prop.normal BiabductionSumm let collect_postconditions analysis_data wl tenv proc_cfg : Paths.PathSet.t * BiabductionSummary.Visitedset.t = let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in - let pathset = collect_analysis_result tenv wl proc_cfg in + let pathset = collect_analysis_result analysis_data wl proc_cfg in (* Assuming C++ developers use RAII, remove resources from the constructor posts *) let pathset = match pname with @@ -756,7 +760,7 @@ type exe_phase = [do, get_results] where [go ()] performs the analysis phase and [get_results ()] returns the results computed. This function is architected so that [get_results ()] can be called even after [go ()] was interrupted by and exception. *) -let perform_analysis_phase ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) +let perform_analysis_phase ({InterproceduralAnalysis.proc_desc; err_log; tenv} as analysis_data) (proc_cfg : ProcCfg.Exceptional.t) summary_opt : exe_phase = let pname = Procdesc.get_proc_name proc_desc in let start_node = ProcCfg.Exceptional.start_node proc_cfg in @@ -792,18 +796,18 @@ let perform_analysis_phase ({InterproceduralAnalysis.proc_desc; tenv} as analysi forward_tabulate analysis_data proc_cfg summary_opt wl in let get_results (wl : Worklist.t) () = + let attrs = Procdesc.get_attributes proc_desc in State.process_execution_failures - (SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning) - pname ; - let results = collect_analysis_result tenv wl proc_cfg in + (BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Warning) ; + let results = collect_analysis_result analysis_data wl proc_cfg in let specs = - try extract_specs analysis_data tenv (ProcCfg.Exceptional.proc_desc proc_cfg) results + try extract_specs analysis_data (ProcCfg.Exceptional.proc_desc proc_cfg) results with Exceptions.Leak _ -> let exn = Exceptions.Internal_error (Localise.verbatim_desc "Leak_while_collecting_specs_after_footprint") in - SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ; + BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Error exn ; (* returning no specs *) [] in (specs, BiabductionSummary.FOOTPRINT) @@ -912,15 +916,15 @@ let is_unavoidable tenv pre = false -let report_custom_errors {InterproceduralAnalysis.proc_desc; tenv} summary = +let report_custom_errors {InterproceduralAnalysis.proc_desc; err_log; tenv} summary = let error_preconditions, all_post_error = custom_error_preconditions summary in let report (pre, custom_error) = if all_post_error || is_unavoidable tenv pre then let loc = Procdesc.get_loc proc_desc in - let pname = Procdesc.get_proc_name proc_desc in let err_desc = Localise.desc_custom_error loc in let exn = Exceptions.Custom_error (custom_error, err_desc) in - SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn + let attrs = Procdesc.get_attributes proc_desc in + BiabductionReporting.log_issue_deprecated_using_state attrs err_log Exceptions.Error exn in List.iter ~f:report error_preconditions