From 33f9a2f86498aa36360423be234566e4b4c14b9d Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Mon, 1 May 2017 12:42:06 -0700 Subject: [PATCH] [infer][backend] remove the unsafe function Specs.get_specs Summary: Now, all the summary access functions in the module `Specs` are of the form: `Specs.summary -> 'a`. This is a step toward making the analysis flow stateless. Reviewed By: sblackshear Differential Revision: D4976126 fbshipit-source-id: 28b6da1 --- infer/src/backend/interproc.ml | 38 +++++++++++++++++---------------- infer/src/backend/printer.ml | 5 ++++- infer/src/backend/specs.ml | 8 ------- infer/src/backend/specs.mli | 3 --- infer/src/backend/tabulation.ml | 2 +- 5 files changed, 25 insertions(+), 31 deletions(-) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 0deb31111..487269803 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -205,7 +205,8 @@ let do_meet_pre tenv pset = (** Find the preconditions in the current spec table, apply meet then join, and return the joined preconditions *) -let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list = +let collect_preconditions tenv summary : Prop.normal Specs.Jprop.t list = + let proc_name = Specs.get_proc_name summary in let collect_do_abstract_one tenv prop = if !Config.footprint then @@ -217,7 +218,7 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list = let pres = List.map ~f:(fun spec -> Specs.Jprop.to_prop spec.Specs.pre) - (Specs.get_specs proc_name) in + (Specs.get_specs_from_payload summary) in let pset = Propset.from_proplist tenv pres in let pset' = let f p = Prop.prop_normal_vars_to_primed_vars tenv p in @@ -983,9 +984,9 @@ type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.p 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 tenv (pname : Typ.Procname.t) (pdesc : Procdesc.t) source +let perform_analysis_phase tenv (summary : Specs.summary) (pdesc : Procdesc.t) source : exe_phase = - let summary = Specs.get_summary_unsafe "perform_analysis_phase" pname in + let pname = Specs.get_proc_name summary in let start_node = Procdesc.get_start_node pdesc in let compute_footprint () : exe_phase = @@ -993,7 +994,7 @@ let perform_analysis_phase tenv (pname : Typ.Procname.t) (pdesc : Procdesc.t) so let init_prop = initial_prop_from_emp tenv pdesc in (* use existing pre's (in recursion some might exist) as starting points *) let init_props_from_pres = - let specs = Specs.get_specs pname in + let specs = Specs.get_specs_from_payload summary in (* rename spec vars to footrpint vars, and copy current to footprint *) let mk_init precondition = initial_prop_from_pre tenv pdesc (Specs.Jprop.to_prop precondition) in @@ -1040,7 +1041,7 @@ let perform_analysis_phase tenv (pname : Typ.Procname.t) (pdesc : Procdesc.t) so let candidate_preconditions = List.map ~f:(fun spec -> spec.Specs.pre) - (Specs.get_specs pname) in + (Specs.get_specs_from_payload summary) in let valid_specs = ref [] in let go () = L.out "@.#### Start: Re-Execution for %a ####@." Typ.Procname.pp pname; @@ -1207,10 +1208,10 @@ module SpecMap = Caml.Map.Make (struct end) (** Update the specs of the current proc after the execution of one phase *) -let update_specs tenv proc_name phase (new_specs : Specs.NormSpec.t list) +let update_specs tenv prev_summary phase (new_specs : Specs.NormSpec.t list) : Specs.NormSpec.t list * bool = let new_specs = Specs.normalized_specs_to_specs new_specs in - let old_specs = Specs.get_specs proc_name in + let old_specs = Specs.get_specs_from_payload prev_summary in let changed = ref false in let current_specs = ref @@ -1270,9 +1271,9 @@ let update_specs tenv proc_name phase (new_specs : Specs.NormSpec.t list) !res,!changed (** update a summary after analysing a procedure *) -let update_summary tenv prev_summary specs phase proc_name res = +let update_summary tenv prev_summary specs phase res = let normal_specs = List.map ~f:(Specs.spec_normalize tenv) specs in - let new_specs, _ = update_specs tenv proc_name phase normal_specs in + let new_specs, _ = update_specs tenv prev_summary phase normal_specs in let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in let stats_failure = match res with | None -> prev_summary.Specs.stats.Specs.stats_failure @@ -1301,12 +1302,12 @@ let analyze_proc source exe_env proc_desc : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env proc_name in reset_global_values proc_desc; - let go, get_results = perform_analysis_phase tenv proc_name proc_desc source in + let summary = Specs.get_summary_unsafe "analyze_proc" proc_name in + let go, get_results = perform_analysis_phase tenv summary proc_desc source in let res = Timeout.exe_timeout go () in let specs, phase = get_results () in - let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in let updated_summary = - update_summary tenv prev_summary specs phase proc_name res in + update_summary tenv summary specs phase res in if Config.curr_language_is Config.Clang && Config.report_custom_error then report_custom_errors tenv updated_summary; if Config.curr_language_is Config.Java && Config.report_runtime_exceptions then @@ -1343,7 +1344,7 @@ let transition_footprint_re_exe tenv proc_name joined_pres = (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for the procedures enabled after the analysis of [proc_name] *) let perform_transition exe_env tenv proc_name source = - let transition () = + let transition summary = (* disable exceptions for leaks and protect against any other errors *) let joined_pres = let allow_leak = !Config.allow_leak in @@ -1359,7 +1360,7 @@ let perform_transition exe_env tenv proc_name source = apply_start_node (do_before_node source 0); try Config.allow_leak := true; - let res = collect_preconditions tenv proc_name in + let res = collect_preconditions tenv summary in Config.allow_leak := allow_leak; apply_start_node (do_after_node source); res @@ -1374,7 +1375,7 @@ let perform_transition exe_env tenv proc_name source = transition_footprint_re_exe tenv proc_name joined_pres in match Specs.get_summary proc_name with | Some summary when Specs.equal_phase (Specs.get_phase summary) Specs.FOOTPRINT -> - transition () + transition summary | _ -> () @@ -1501,8 +1502,9 @@ let visited_and_total_nodes ~filter cfg = let print_stats_cfg proc_shadowed source cfg = let err_table = Errlog.create_err_table () in let filter pdesc = - let pname = Procdesc.get_proc_name pdesc in - Specs.summary_exists pname && Specs.get_specs pname <> [] in + match Specs.get_summary (Procdesc.get_proc_name pdesc) with + | None -> false + | Some summary -> Specs.get_specs_from_payload summary <> [] in let nodes_visited, nodes_total = visited_and_total_nodes ~filter cfg in let num_proc = ref 0 in let num_nospec_noerror_proc = ref 0 in diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index b16aea593..10428a844 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -554,7 +554,10 @@ let write_html_file linereader filename procs = ~f:(fun n -> match Procdesc.Node.get_kind n with | Procdesc.Node.Start_node proc_name -> - let num_specs = List.length (Specs.get_specs proc_name) in + let num_specs = + match Specs.get_summary proc_name with + | None -> 0 + | Some summary -> List.length (Specs.get_specs_from_payload summary) in let label = (Escape.escape_xml (Typ.Procname.to_string proc_name)) ^ ": " ^ diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 4ff29c96b..a3c8b99a1 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -667,14 +667,6 @@ let get_flag summary key = Some (Hashtbl.find proc_flags key) with Not_found -> None -(** Return the specs for the proc in the spec table *) -let get_specs proc_name = - match get_summary proc_name with - | None -> - failwithf "Specs.get_specs: %a not found" Typ.Procname.pp proc_name - | Some summary -> - get_specs_from_payload summary - (** Return the current phase for the proc *) let get_phase summary = summary.phase diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index e668400df..fc8af6bdd 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -191,9 +191,6 @@ val get_phase : summary -> phase (** Return the signature of a procedure declaration as a string *) val get_signature : summary -> string -(** Return the specs for the proc in the spec table *) -val get_specs : Typ.Procname.t -> Prop.normal spec list - (** Get the specs from the payload of the summary. *) val get_specs_from_payload : summary -> Prop.normal spec list diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 51a2a6789..f7f6324bd 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -123,7 +123,7 @@ let spec_find_rename trace_call summary let count = ref 0 in let f spec = incr count; (!count, spec_rename_vars proc_name spec) in - let specs = Specs.get_specs proc_name in + let specs = Specs.get_specs_from_payload summary in let formals = Specs.get_formals summary in if List.is_empty specs then begin