From f5adab59eccc44da0eef5df1f5d6cc6d1cc34314 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 29 Mar 2017 19:59:57 -0700 Subject: [PATCH] [infer][checkers] Prevent the race conditions between the summaries passed as parameter to the checkers and the summaries from the specs table Summary: This is step further simplify the code to avoid cases where the summary of the procedure being analyzed can exist in two different versions: # one version is the summary passed as parameter to every checker # the other is a copy of the summary in the in-memory specs table This diff implements: # the analysis always run through the `Ondemand` module (was already the case before) # the summary of the procedure being analyzed is created at the beginning of the on-demand analysis call # all the checkers run in sequence, update their respective part of the payload and log errors to the error table # the summary is store at the end of the on-demand analysis call Reviewed By: sblackshear Differential Revision: D4787414 fbshipit-source-id: 2d115c9 --- infer/src/backend/callbacks.ml | 29 +++---------- infer/src/backend/interproc.ml | 2 +- infer/src/backend/ondemand.ml | 26 +++++------ infer/src/backend/ondemand.mli | 2 +- infer/src/backend/reporting.ml | 5 ++- .../src/bufferoverrun/bufferOverrunChecker.ml | 23 +++++----- infer/src/checkers/AbstractInterpreter.ml | 7 ++- infer/src/checkers/AbstractInterpreter.mli | 4 +- infer/src/checkers/BoundedCallTree.ml | 37 ++++++++-------- infer/src/checkers/SimpleChecker.ml | 4 +- infer/src/checkers/Siof.ml | 26 +++++------ infer/src/checkers/ThreadSafety.ml | 26 ++++------- infer/src/checkers/ThreadSafety.mli | 2 +- infer/src/checkers/annotationReachability.ml | 43 +++++++++++-------- infer/src/checkers/checkDeadCode.ml | 4 +- infer/src/checkers/checkTraceCallSequence.ml | 4 +- infer/src/checkers/checkers.ml | 22 +++++----- infer/src/checkers/printfArgs.ml | 4 +- infer/src/checkers/registerCheckers.ml | 2 +- infer/src/checkers/sqlChecker.ml | 4 +- infer/src/checkers/summary.ml | 40 +++++++---------- infer/src/checkers/summary.mli | 28 ++++++------ infer/src/eradicate/eradicate.ml | 4 +- infer/src/quandary/TaintAnalysis.ml | 18 +++----- infer/src/unit/TaintTests.ml | 4 +- .../java/quandary/UnknownCode.java | 4 +- .../codetoanalyze/java/quandary/issues.exp | 2 + 27 files changed, 174 insertions(+), 202 deletions(-) diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 771fc6ec7..cc7df3bbf 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -57,17 +57,8 @@ let get_procedure_definition exe_env proc_name = let get_language proc_name = if Typ.Procname.is_java proc_name then Config.Java else Config.Clang -let reset_summary proc_name = - match Specs.get_summary proc_name with - | Some summary -> summary - | None -> - let attributes_opt = - Specs.proc_resolve_attributes proc_name in - Specs.reset_summary proc_name attributes_opt None - - (** Invoke all registered procedure callbacks on the given procedure. *) -let iterate_procedure_callbacks exe_env caller_pname = +let iterate_procedure_callbacks exe_env summary caller_pname = let procedure_language = get_language caller_pname in Config.curr_language := procedure_language; @@ -81,12 +72,11 @@ let iterate_procedure_callbacks exe_env caller_pname = | None -> [] in - let initial_summary = reset_summary caller_pname in match get_procedure_definition exe_env caller_pname with - | None -> initial_summary + | None -> summary | Some (idenv, tenv, _, proc_desc, _) -> List.fold - ~init:initial_summary + ~init:summary ~f:(fun summary (language_opt, proc_callback) -> let language_matches = match language_opt with | Some language -> Config.equal_language language procedure_language @@ -140,12 +130,9 @@ let iterate_callbacks call_graph exe_env = (* analyze all the currently defined procedures *) Cg.get_defined_nodes call_graph in - (* Make sure summaries exists. *) - List.iter ~f:(fun p -> ignore (reset_summary p)) procs_to_analyze; - - let analyze_ondemand _ proc_desc = + let analyze_ondemand _ summary proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in - iterate_procedure_callbacks exe_env proc_name in + iterate_procedure_callbacks exe_env summary proc_name in let callbacks = { Ondemand.analyze_ondemand; @@ -193,10 +180,4 @@ let iterate_callbacks call_graph exe_env = (* Unregister callbacks *) Ondemand.unset_callbacks (); - (* Store all the summaries to disk *) - List.iter - ~f:(fun pname -> - Specs.store_summary (Specs.get_summary_unsafe "Checkers: store summaries" pname)) - procs_to_analyze; - Config.curr_language := saved_language diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 9e18756dc..22851f7a9 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1430,7 +1430,7 @@ let do_analysis_closures exe_env : Tasks.closure list = Option.bind (Specs.get_summary proc_name) (fun summary -> summary.Specs.proc_desc_option) | None -> None in - let analyze_ondemand source proc_desc = + let analyze_ondemand source _ proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in let tenv = Exe_env.get_tenv exe_env proc_name in if not (Config.eradicate || Config.checkers) && not (Procdesc.did_preanalysis proc_desc) diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 1d2fceb89..e494fcb0a 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -27,7 +27,7 @@ let dirs_to_analyze = changed_files String.Set.empty in Option.map ~f:process_changed_files SourceFile.changed_files_set -type analyze_ondemand = SourceFile.t -> Procdesc.t -> Specs.summary +type analyze_ondemand = SourceFile.t -> Specs.summary -> Procdesc.t -> Specs.summary type get_proc_desc = Typ.Procname.t -> Procdesc.t option @@ -145,9 +145,9 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc if Config.dynamic_dispatch = `Lazy then Some callee_pdesc else None in - ignore (Specs.reset_summary callee_pname attributes_opt callee_pdesc_option); + let initial_summary = Specs.reset_summary callee_pname attributes_opt callee_pdesc_option in Specs.set_status callee_pname Specs.Active; - source in + source, initial_summary in let postprocess source summary = decr nesting; @@ -156,22 +156,22 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc log_elapsed_time (); summary 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 stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in + let log_error_and_continue exn summary kind = + Reporting.log_error_from_summary summary exn; + let stats = { 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 } in + { summary.Specs.payload with Specs.preposts = Some []; } in + let new_summary = { summary with Specs.stats; payload } in Specs.store_summary new_summary; log_elapsed_time (); new_summary in let old_state = save_global_state () in - let source = preprocess () in + let source, initial_summary = preprocess () in try let summary = - analyze_proc source callee_pdesc |> postprocess source in + analyze_proc source initial_summary callee_pdesc + |> postprocess source in restore_global_state old_state; summary with exn -> @@ -188,10 +188,10 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc | SymOp.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 + log_error_and_continue exn initial_summary kind | _ -> (* this happens with assert false or some other unrecognized exception *) - log_error_and_continue exn (FKcrash (Exn.to_string exn)) + log_error_and_continue exn initial_summary (FKcrash (Exn.to_string exn)) let analyze_proc_desc ~propagate_exceptions curr_pdesc callee_pdesc : Specs.summary option = diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index 3466291b3..7569921ef 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -15,7 +15,7 @@ open! IStd will be analyzed *) val dirs_to_analyze : String.Set.t option -type analyze_ondemand = SourceFile.t -> Procdesc.t -> Specs.summary +type analyze_ondemand = SourceFile.t -> Specs.summary -> Procdesc.t -> Specs.summary type get_proc_desc = Typ.Procname.t -> Procdesc.t option diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml index 7f25cdb20..d89b34038 100644 --- a/infer/src/backend/reporting.ml +++ b/infer/src/backend/reporting.ml @@ -56,7 +56,10 @@ let log_issue_from_summary err_kind summary ?loc ?node_id ?session ?ltr ?linters let log_issue err_kind proc_name ?loc ?node_id ?session ?ltr ?linters_def_file exn = match Specs.get_summary proc_name with | Some summary -> - log_issue_from_summary err_kind summary ?loc ?node_id ?session ?ltr ?linters_def_file exn + log_issue_from_summary err_kind summary ?loc ?node_id ?session ?ltr ?linters_def_file exn; + if Config.checkers then + (* TODO (#16348004): Remove this once Specs.get_summary_unsafe is entirely removed *) + Specs.store_summary summary | None -> failwithf "Trying to report error on procedure %a, but cannot because no summary exists for this \ diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 231590858..4a221ddb5 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -18,13 +18,13 @@ module L = Logging module Dom = BufferOverrunDomain module Summary = Summary.Make (struct - type summary = Dom.Summary.t + type payload = Dom.Summary.t - let update_payload astate payload = - { payload with Specs.buffer_overrun = Some astate } + let update_payload astate (summary : Specs.summary) = + { summary with payload = { summary.payload with buffer_overrun = Some astate }} - let read_from_payload payload = - payload.Specs.buffer_overrun + let read_payload (summary : Specs.summary) = + summary.payload.buffer_overrun end) module TransferFunctions (CFG : ProcCfg.S) = @@ -319,7 +319,7 @@ struct let instantiate_cond : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list - -> Dom.Mem.t -> Summary.summary -> Location.t -> Dom.ConditionSet.t + -> Dom.Mem.t -> Summary.payload -> Location.t -> Dom.ConditionSet.t = fun tenv caller_pname callee_pdesc params caller_mem summary loc -> let callee_entry_mem = Dom.Summary.get_input summary in let callee_cond = Dom.Summary.get_cond_set summary in @@ -415,7 +415,7 @@ struct end let compute_post - : Analyzer.TransferFunctions.extras ProcData.t -> Summary.summary option + : Analyzer.TransferFunctions.extras ProcData.t -> Summary.payload option = fun { pdesc; tenv; extras = get_pdesc } -> let cfg = CFG.from_pdesc pdesc in let pdata = ProcData.make pdesc tenv get_pdesc in @@ -446,15 +446,16 @@ let checker : Callbacks.proc_callback_args -> Specs.summary = fun ({ summary } as callback) -> let proc_name = Specs.get_proc_name summary in let make_extras _ = callback.get_proc_desc in - let post = + let updated_summary : Specs.summary = Interprocedural.compute_and_store_post ~compute_post ~make_extras - callback - in + callback in + let post = + updated_summary.payload.buffer_overrun in begin match post with | Some s when Config.bo_debug >= 1 -> print_summary proc_name s | _ -> () end; - Specs.get_summary_unsafe "bufferOverrunChecker.checker" proc_name + updated_summary diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index c76fc8cd2..dd3128ce0 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -159,13 +159,12 @@ end module Interprocedural (Summ : Summary.S) = struct let compute_and_store_post - ~compute_post ~make_extras { Callbacks.proc_desc; tenv; } = + ~compute_post ~make_extras { Callbacks.proc_desc; summary; tenv; } : Specs.summary = match compute_post (ProcData.make proc_desc tenv (make_extras proc_desc)) with | Some post -> - Summ.write_summary (Procdesc.get_proc_name proc_desc) post; - Some post + Summ.update_summary post summary | None -> - None + summary end diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli index 227fc97a4..0f30441f9 100644 --- a/infer/src/checkers/AbstractInterpreter.mli +++ b/infer/src/checkers/AbstractInterpreter.mli @@ -66,8 +66,8 @@ module Interprocedural (Summary : Summary.S) : sig (** compute and return the summary for the given procedure and store it on disk using [compute_post]. *) val compute_and_store_post : - compute_post: ('a ProcData.t -> Summary.summary option) -> + compute_post: ('a ProcData.t -> Summary.payload option) -> make_extras : (Procdesc.t -> 'a) -> Callbacks.proc_callback_args -> - Summary.summary option + Specs.summary end diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml index e7c6afdb0..857c211d0 100644 --- a/infer/src/checkers/BoundedCallTree.ml +++ b/infer/src/checkers/BoundedCallTree.ml @@ -23,13 +23,16 @@ module Domain = AbstractDomain.FiniteSet(ProcnameSet) in the output directory as JSON files and *only* for those methods that will be part of the final crashcontext.json. *) module SpecSummary = Summary.Make (struct - type summary = Stacktree_j.stacktree option + type payload = Stacktree_j.stacktree - let update_payload frame payload = - { payload with Specs.crashcontext_frame = frame } + let update_payload frame (summary : Specs.summary) = + let payload = + { summary.payload with Specs.crashcontext_frame = Some frame } in + { summary with payload = payload } + + let read_payload (summary : Specs.summary) = + summary.payload.crashcontext_frame - let read_from_payload payload = - Some payload.Specs.crashcontext_frame end) type extras_t = { @@ -78,15 +81,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let callees = List.map ~f:(fun pn -> match SpecSummary.read_summary pdesc pn with - | None | Some None -> (match get_proc_desc pn with - | None -> stacktree_stub_of_procname pn - (* This can happen when the callee is in the same cluster/ buck - target, but it hasn't been checked yet. So we need both the - inter-target lookup (SpecSummary) and the intra-target - lookup (using get_proc_desc). *) - | Some callee_pdesc -> - stacktree_of_pdesc callee_pdesc "proc_start") - | Some (Some stracktree) -> stracktree ) + | None -> + (match get_proc_desc pn with + | None -> stacktree_stub_of_procname pn + (* This can happen when the callee is in the same cluster/ buck + target, but it hasn't been checked yet. So we need both the + inter-target lookup (SpecSummary) and the intra-target + lookup (using get_proc_desc). *) + | Some callee_pdesc -> + stacktree_of_pdesc callee_pdesc "proc_start") + | Some stracktree -> stracktree ) procs in stacktree_of_pdesc pdesc ~loc ~callees location_type @@ -163,8 +167,7 @@ let loaded_stacktraces = | None -> None | Some files -> Some (List.map ~f:Stacktrace.of_json_file files) -let checker { Callbacks.proc_desc; tenv; get_proc_desc } : Specs.summary = - let proc_name = Procdesc.get_proc_name proc_desc in +let checker { Callbacks.proc_desc; tenv; get_proc_desc; summary } : Specs.summary = begin match loaded_stacktraces with | None -> failwith "Missing command line option. Either \ @@ -180,4 +183,4 @@ let checker { Callbacks.proc_desc; tenv; get_proc_desc } : Specs.summary = ignore (Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras) ~initial:Domain.empty) end end; - Specs.get_summary_unsafe "BoundedCallTree.checker" proc_name + summary diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml index c0fbbdec5..6f4bd00d5 100644 --- a/infer/src/checkers/SimpleChecker.ml +++ b/infer/src/checkers/SimpleChecker.ml @@ -82,7 +82,7 @@ module Make (Spec : Spec) : S = struct module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) - let checker { Callbacks.proc_desc; tenv; } : Specs.summary = + let checker { Callbacks.proc_desc; tenv; summary } : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in let nodes = Procdesc.get_nodes proc_desc in let do_reporting node_id state = @@ -101,6 +101,6 @@ module Make (Spec : Spec) : S = struct let inv_map = Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) ~initial:Domain.empty in Analyzer.InvariantMap.iter do_reporting inv_map; - Specs.get_summary_unsafe "checker" proc_name + summary end diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 163a11e1d..9dbe5cd67 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -46,13 +46,13 @@ let is_modelled = |> QualifiedCppName.Match.match_qualifiers models_matcher module Summary = Summary.Make (struct - type summary = SiofDomain.astate + type payload = SiofDomain.astate - let update_payload astate payload = - { payload with Specs.siof = Some astate } + let update_payload astate (summary : Specs.summary) = + { summary with payload = { summary.payload with siof = Some astate }} - let read_from_payload payload = - payload.Specs.siof + let read_payload (summary : Specs.summary) = + summary.payload.siof end) module TransferFunctions (CFG : ProcCfg.S) = struct @@ -183,7 +183,7 @@ let is_foreign tu_opt (v, _) = | None -> assert false in Option.value_map ~f:(fun f -> not (is_orig_file f)) ~default:false (Pvar.get_source_file v) -let report_siof trace pdesc gname loc = +let report_siof summary trace pdesc gname loc = let tu_opt = let attrs = Procdesc.get_attributes pdesc in attrs.ProcAttributes.translation_unit in @@ -208,10 +208,9 @@ let report_siof trace pdesc gname loc = GlobalsAccesses.pp foreign_globals in description, (passthroughs, (final_sink', pt)::rest) in let ltr = SiofTrace.trace_of_error loc gname sink_path' in - let caller_pname = Procdesc.get_proc_name pdesc in let msg = Localise.to_issue_id Localise.static_initialization_order_fiasco in let exn = Exceptions.Checkers (msg, Localise.verbatim_desc description) in - Reporting.log_error caller_pname ~loc ~ltr exn in + Reporting.log_error_from_summary summary ~loc ~ltr exn in let has_foreign_sink (_, path) = List.exists @@ -224,7 +223,8 @@ let report_siof trace pdesc gname loc = |> List.filter ~f:has_foreign_sink |> List.iter ~f:report_one_path -let siof_check pdesc gname = function +let siof_check pdesc gname (summary : Specs.summary) = + match summary.payload.siof with | Some ((SiofDomain.BottomSiofTrace.NonBottom post, _)) -> let attrs = Procdesc.get_attributes pdesc in let all_globals = SiofTrace.Sinks.fold @@ -234,7 +234,7 @@ let siof_check pdesc gname = function let attrs = Procdesc.get_attributes pdesc in attrs.ProcAttributes.translation_unit in if GlobalsAccesses.exists (is_foreign tu_opt) all_globals then - report_siof post pdesc gname attrs.ProcAttributes.loc; + report_siof summary post pdesc gname attrs.ProcAttributes.loc; | Some (SiofDomain.BottomSiofTrace.Bottom, _) | None -> () @@ -244,7 +244,7 @@ let compute_post proc_data = |> Option.map ~f:SiofDomain.normalize let checker ({ Callbacks.proc_desc } as callback) : Specs.summary = - let post = + let updated_summary = Interprocedural.compute_and_store_post ~compute_post ~make_extras:ProcData.make_empty_extras @@ -253,8 +253,8 @@ let checker ({ Callbacks.proc_desc } as callback) : Specs.summary = begin match Typ.Procname.get_global_name_of_initializer pname with | Some gname -> - siof_check proc_desc gname post + siof_check proc_desc gname updated_summary | None -> () end; - Specs.get_summary_unsafe "SIOF checker" pname + updated_summary diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 5a0e0d308..1ce6dc049 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -14,13 +14,13 @@ module L = Logging module MF = MarkupFormatter module Summary = Summary.Make (struct - type summary = ThreadSafetyDomain.summary + type payload = ThreadSafetyDomain.summary - let update_payload summary payload = - { payload with Specs.threadsafety = Some summary } + let update_payload post (summary : Specs.summary) = + { summary with payload = { summary.payload with threadsafety = Some post }} - let read_from_payload payload = - payload.Specs.threadsafety + let read_payload (summary : Specs.summary) = + summary.payload.threadsafety end) let is_owned access_path attribute_map = @@ -870,18 +870,10 @@ let analyze_procedure callback = end else Some empty_post in - match - Interprocedural.compute_and_store_post - ~compute_post - ~make_extras:FormalMap.make - callback with - | Some post -> post - | None -> empty_post - -let checker ({ Callbacks.summary } as callback_args) : Specs.summary = - let proc_name = Specs.get_proc_name summary in - ignore (analyze_procedure callback_args); - Specs.get_summary_unsafe "ThreadSafety.checker" proc_name + Interprocedural.compute_and_store_post + ~compute_post + ~make_extras:FormalMap.make + callback (* we assume two access paths can alias if their access parts are equal (we ignore the base). *) let can_alias access_path1 access_path2 = diff --git a/infer/src/checkers/ThreadSafety.mli b/infer/src/checkers/ThreadSafety.mli index 926eafd0c..b6c55556b 100644 --- a/infer/src/checkers/ThreadSafety.mli +++ b/infer/src/checkers/ThreadSafety.mli @@ -9,4 +9,4 @@ val file_analysis : Callbacks.cluster_callback_t -val checker : Callbacks.proc_callback_t +val analyze_procedure : Callbacks.proc_callback_t diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index ee04cc78a..a32ecd5b3 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -73,13 +73,13 @@ module Domain = struct end module Summary = Summary.Make (struct - type summary = CallsDomain.astate + type payload = CallsDomain.astate - let update_payload call_map payload = - { payload with Specs.calls = Some call_map } + let update_payload call_map (summary : Specs.summary) = + { summary with payload = { summary.payload with calls = Some call_map }} - let read_from_payload payload = - payload.Specs.calls + let read_payload (summary : Specs.summary) = + summary.payload.calls end) (* Warning name when a performance critical method directly or indirectly @@ -161,7 +161,8 @@ let string_of_pname = Typ.Procname.to_simplified_string ~withclass:true let report_allocation_stack - src_annot pname fst_call_loc trace stack_str constructor_pname call_loc = + src_annot summary fst_call_loc trace stack_str constructor_pname call_loc = + let pname = Specs.get_proc_name summary in let final_trace = List.rev (update_trace call_loc trace) in let constr_str = string_of_pname constructor_pname in let description = @@ -173,11 +174,12 @@ let report_allocation_stack MF.pp_monospaced (stack_str ^ ("new "^constr_str)) in let exn = Exceptions.Checkers (allocates_memory, Localise.verbatim_desc description) in - Reporting.log_error pname ~loc:fst_call_loc ~ltr:final_trace exn + Reporting.log_error_from_summary summary ~loc:fst_call_loc ~ltr:final_trace exn -let report_annotation_stack src_annot snk_annot src_pname loc trace stack_str snk_pname call_loc = +let report_annotation_stack src_annot snk_annot src_summary loc trace stack_str snk_pname call_loc = + let src_pname = Specs.get_proc_name src_summary in if String.equal snk_annot dummy_constructor_annot - then report_allocation_stack src_annot src_pname loc trace stack_str snk_pname call_loc + then report_allocation_stack src_annot src_summary loc trace stack_str snk_pname call_loc else let final_trace = List.rev (update_trace call_loc trace) in let exp_pname_str = string_of_pname snk_pname in @@ -195,9 +197,9 @@ let report_annotation_stack src_annot snk_annot src_pname loc trace stack_str sn else annotation_reachability_error in let exn = Exceptions.Checkers (msg, Localise.verbatim_desc description) in - Reporting.log_error src_pname ~loc ~ltr:final_trace exn + Reporting.log_error_from_summary src_summary ~loc ~ltr:final_trace exn -let report_call_stack end_of_stack lookup_next_calls report call_site calls = +let report_call_stack summary end_of_stack lookup_next_calls report call_site calls = (* TODO: stop using this; we can use the call site instead *) let lookup_location pname = match Specs.get_summary pname with @@ -205,7 +207,7 @@ let report_call_stack end_of_stack lookup_next_calls report call_site calls = | Some summary -> summary.Specs.attributes.ProcAttributes.loc in let rec loop fst_call_loc visited_pnames (trace, stack_str) (callee_pname, call_loc) = if end_of_stack callee_pname then - report (CallSite.pname call_site) fst_call_loc trace stack_str callee_pname call_loc + report summary fst_call_loc trace stack_str callee_pname call_loc else let callee_def_loc = lookup_location callee_pname in let next_calls = lookup_next_calls callee_pname in @@ -328,7 +330,7 @@ module Interprocedural = struct let method_is_expensive tenv pname = is_modeled_expensive tenv pname || is_expensive tenv pname - let check_and_report ({ Callbacks.proc_desc; tenv; } as proc_data) : Specs.summary = + let check_and_report ({ Callbacks.proc_desc; tenv; summary } as proc_data) : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in let loc = Procdesc.get_loc proc_desc in let expensive = is_expensive tenv proc_name in @@ -344,7 +346,7 @@ module Interprocedural = struct let exn = Exceptions.Checkers (expensive_overrides_unexpensive, Localise.verbatim_desc description) in - Reporting.log_error proc_name ~loc exn in + Reporting.log_error_from_summary summary ~loc exn in if expensive then PatternMatch.override_iter check_expensive_subtyping_rules tenv proc_name; @@ -361,6 +363,7 @@ module Interprocedural = struct let f_report = report_annotation_stack src_annot.class_name snk_annot.class_name in report_call_stack + summary (method_has_annot snk_annot tenv) (lookup_annotation_calls proc_desc snk_annot) f_report @@ -380,17 +383,19 @@ module Interprocedural = struct (init_map, Domain.TrackingVar.empty) in let compute_post proc_data = Option.map ~f:fst (Analyzer.compute_post ~initial proc_data) in + let updated_summary : Specs.summary = + compute_and_store_post + ~compute_post:compute_post + ~make_extras:ProcData.make_empty_extras + proc_data in begin - match compute_and_store_post - ~compute_post:compute_post - ~make_extras:ProcData.make_empty_extras - proc_data with + match updated_summary.payload.calls with | Some call_map -> List.iter ~f:(report_src_snk_paths call_map) (src_snk_pairs ()) | None -> () end; - Specs.get_summary_unsafe "AnnotationReachability.checker" proc_name + updated_summary end diff --git a/infer/src/checkers/checkDeadCode.ml b/infer/src/checkers/checkDeadCode.ml index 2254d6e50..f6b5fc8da 100644 --- a/infer/src/checkers/checkDeadCode.ml +++ b/infer/src/checkers/checkDeadCode.ml @@ -91,7 +91,7 @@ let check_final_state tenv proc_name proc_desc final_s = end (** Simple check for dead code. *) -let callback_check_dead_code { Callbacks.proc_desc; tenv } = +let callback_check_dead_code { Callbacks.proc_desc; tenv; summary } = let proc_name = Procdesc.get_proc_name proc_desc in let module DFDead = MakeDF(struct @@ -115,4 +115,4 @@ let callback_check_dead_code { Callbacks.proc_desc; tenv } = end in do_check (); - Specs.get_summary_unsafe "callback_check_dead_code" proc_name + summary diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml index 7bf127d55..fd9cbf29e 100644 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -317,7 +317,7 @@ let check_final_state tenv proc_name proc_desc exit_node final_s = (** Check that the trace calls are balanced. This is done by using the most general control flow including exceptions. The begin() and end() function are assumed not to throw exceptions. *) -let callback_check_trace_call_sequence { Callbacks.proc_desc; idenv; tenv } = +let callback_check_trace_call_sequence { Callbacks.proc_desc; idenv; tenv; summary } = let proc_name = Procdesc.get_proc_name proc_desc in let module DFTrace = MakeDF(struct @@ -343,4 +343,4 @@ let callback_check_trace_call_sequence { Callbacks.proc_desc; idenv; tenv } = end in if not (APIs.is_begin_or_end proc_name) then do_check (); - Specs.get_summary_unsafe "callback_check_trace_call_sequence" proc_name + summary diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 84f53f1a7..8b652a2ed 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -168,11 +168,11 @@ let report_calls_and_accesses tenv callback proc_desc instr = | None -> () (** Report all field accesses and method calls of a procedure. *) -let callback_check_access { Callbacks.tenv; proc_desc; } = +let callback_check_access { Callbacks.tenv; proc_desc; summary } = Procdesc.iter_instrs (fun _ instr -> report_calls_and_accesses tenv Localise.proc_callback proc_desc instr) proc_desc; - Specs.get_summary_unsafe "callback_check_access" (Procdesc.get_proc_name proc_desc) + summary (** Report all field accesses and method calls of a class. *) @@ -317,7 +317,7 @@ let callback_check_write_to_parcel ({ Callbacks.summary } as args) = summary (** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *) -let callback_monitor_nullcheck { Callbacks.proc_desc; idenv } = +let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; summary } = let proc_name = Procdesc.get_proc_name proc_desc in let verbose = ref false in @@ -396,13 +396,13 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv } = | _ -> () in Procdesc.iter_instrs do_instr proc_desc; summary_checks_of_formals (); - Specs.get_summary_unsafe "callback_monitor_nullcheck" proc_name + summary (** Test persistent state. *) let callback_test_state { Callbacks.summary } = let proc_name = Specs.get_proc_name summary in ST.pname_add proc_name "somekey" "somevalue"; - Specs.get_summary_unsafe "callback_test_state" proc_name + summary (** Check the uses of VisibleForTesting *) let callback_checkVisibleForTesting { Callbacks.proc_desc; summary } = @@ -415,7 +415,7 @@ let callback_checkVisibleForTesting { Callbacks.proc_desc; summary } = summary (** Check for readValue and readValueAs json deserialization *) -let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; } = +let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; summary } = let proc_name = Procdesc.get_proc_name proc_desc in let verbose = true in @@ -510,7 +510,7 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; } store_return (); Procdesc.iter_instrs do_instr proc_desc; - Specs.get_summary_unsafe "callback_find_deserialization" proc_name + summary (** Check field accesses. *) let callback_check_field_access { Callbacks.proc_desc; summary } = @@ -557,7 +557,7 @@ let callback_check_field_access { Callbacks.proc_desc; summary } = summary (** Print c method calls. *) -let callback_print_c_method_calls { Callbacks.tenv; proc_desc } = +let callback_print_c_method_calls { Callbacks.tenv; proc_desc; summary } = let proc_name = Procdesc.get_proc_name proc_desc in let do_instr node = function | Sil.Call (_, Exp.Const (Const.Cfun pn), (e, _):: _, loc, _) @@ -584,10 +584,10 @@ let callback_print_c_method_calls { Callbacks.tenv; proc_desc } = description | _ -> () in Procdesc.iter_instrs do_instr proc_desc; - Specs.get_summary_unsafe "callback_print_c_method_calls" proc_name + summary (** Print access to globals. *) -let callback_print_access_to_globals { Callbacks.tenv; proc_desc } = +let callback_print_access_to_globals { Callbacks.tenv; proc_desc; summary } = let proc_name = Procdesc.get_proc_name proc_desc in let do_pvar is_read pvar loc = let description = @@ -614,4 +614,4 @@ let callback_print_access_to_globals { Callbacks.tenv; proc_desc } = Option.iter ~f:(fun pvar -> do_pvar false pvar loc) (get_global_var e) | _ -> () in Procdesc.iter_instrs do_instr proc_desc; - Specs.get_summary_unsafe "callback_print_access_to_globals" proc_name + summary diff --git a/infer/src/checkers/printfArgs.ml b/infer/src/checkers/printfArgs.ml index d6d0f7888..6cb94df7b 100644 --- a/infer/src/checkers/printfArgs.ml +++ b/infer/src/checkers/printfArgs.ml @@ -206,10 +206,10 @@ let check_printf_args_ok tenv | None -> ()) | _ -> () -let callback_printf_args { Callbacks.tenv; proc_desc } : Specs.summary = +let callback_printf_args { Callbacks.tenv; proc_desc; summary } : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in Procdesc.iter_instrs (fun n i -> check_printf_args_ok tenv n i proc_name proc_desc) proc_desc; - Specs.get_summary_unsafe "Callbacks.proc_callback_t" proc_name + summary (* let printf_signature_to_string diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index cbe75b15b..2b3d6c1f7 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -39,7 +39,7 @@ let active_procedure_checkers () = PrintfArgs.callback_printf_args, Config.checkers_enabled; AnnotationReachability.checker, Config.checkers_enabled; BufferOverrunChecker.checker, Config.bufferoverrun; - ThreadSafety.checker, Config.threadsafety || Config.checkers_enabled; + ThreadSafety.analyze_procedure, Config.threadsafety || Config.checkers_enabled; ] in (* make sure SimpleChecker.ml is not dead code *) if false then (let module SC = SimpleChecker.Make in ()); diff --git a/infer/src/checkers/sqlChecker.ml b/infer/src/checkers/sqlChecker.ml index 6d67953d4..630d0b5d0 100644 --- a/infer/src/checkers/sqlChecker.ml +++ b/infer/src/checkers/sqlChecker.ml @@ -13,7 +13,7 @@ module L = Logging (** Find SQL statements in string concatenations *) -let callback_sql { Callbacks.proc_desc; tenv } : Specs.summary = +let callback_sql { Callbacks.proc_desc; tenv; summary } : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in let verbose = false in @@ -71,4 +71,4 @@ let callback_sql { Callbacks.proc_desc; tenv } : Specs.summary = Procdesc.iter_instrs (do_instr const_map) proc_desc with _ -> () end; - Specs.get_summary_unsafe "SqlChecker.callback_sql" proc_name + summary diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml index 1c969db83..dc0887e9e 100644 --- a/infer/src/checkers/summary.ml +++ b/infer/src/checkers/summary.ml @@ -9,42 +9,34 @@ open! IStd -module type Helper = sig - type summary - (* type astate*) +module type Payload = sig + type payload - (** update the specs payload with [summary] *) - val update_payload : summary -> Specs.payload -> Specs.payload + val update_payload : payload -> Specs.summary -> Specs.summary + + val read_payload : Specs.summary -> payload option - (** extract [summmary] from the specs payload *) - val read_from_payload : Specs.payload -> summary option end module type S = sig - type summary - (* type astate*) + type payload + + val update_summary : payload -> Specs.summary -> Specs.summary - (** Write the [summary] for the procname to persistent storage. *) - val write_summary : Typ.Procname.t -> summary -> unit + val read_summary : Procdesc.t -> Typ.Procname.t -> payload option - (** read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis - to create the summary if needed *) - val read_summary : Procdesc.t -> Typ.Procname.t -> summary option end -module Make (H : Helper) = struct - type summary = H.summary +module Make (P : Payload) : S with type payload = P.payload = struct - let write_summary pname summary = - match Specs.get_summary pname with - | Some global_summary -> - let payload = H.update_payload summary global_summary.Specs.payload in - Specs.add_summary pname { global_summary with payload; } - | None -> - failwithf "Summary for %a should exist, but does not!@." Typ.Procname.pp pname + type payload = P.payload + + let update_summary payload summary = + P.update_payload payload summary let read_summary caller_pdesc callee_pname = match Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc callee_pname with | None -> None - | Some summary -> H.read_from_payload summary.Specs.payload + | Some summary -> P.read_payload summary + end diff --git a/infer/src/checkers/summary.mli b/infer/src/checkers/summary.mli index 3fb29361c..c384b8643 100644 --- a/infer/src/checkers/summary.mli +++ b/infer/src/checkers/summary.mli @@ -7,27 +7,27 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -module type Helper = sig - type summary +module type Payload = sig + type payload - (** update the specs payload with [summary] *) - val update_payload : summary -> Specs.payload -> Specs.payload + (** Uptade the corresponding part of the payload in the procedure summary *) + val update_payload : payload -> Specs.summary -> Specs.summary + + (** Read the corresponding part of the payload from the procedure summary *) + val read_payload : Specs.summary -> payload option - (** extract [summmary] from the specs payload *) - val read_from_payload : Specs.payload -> summary option end module type S = sig - type summary + type payload - (** Write the [summary] for the procname to persistent storage. Returns the summary actually - written. *) - val write_summary : Typ.Procname.t -> summary -> unit + (** Uptade the corresponding part of the payload in the procedure summary *) + val update_summary : payload -> Specs.summary -> Specs.summary - (** read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis - to create the summary if needed *) - val read_summary : Procdesc.t -> Typ.Procname.t -> summary option + (** Return the payload for the given procedure. + Runs the analysis on-demand if necessary *) + val read_summary : Procdesc.t -> Typ.Procname.t -> payload option end -module Make (H : Helper) : S with type summary = H.summary +module Make (P : Payload) : S with type payload = P.payload diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index b29f7383c..fea04f9f4 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -345,7 +345,7 @@ struct update_summary curr_pname curr_pdesc final_typestate_opt (** Entry point for the eradicate-based checker infrastructure. *) - let callback checks ({ Callbacks.proc_desc } as callback_args) : Specs.summary = + let callback checks ({ Callbacks.proc_desc; summary } as callback_args) : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in let calls_this = ref false in @@ -371,7 +371,7 @@ struct callback2 calls_this checks callback_args annotated_signature linereader loc end; - Specs.get_summary_unsafe "callback" proc_name + summary end (* MkCallback *) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 9c2cdcec7..4af1a0789 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -20,15 +20,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct module IdMapDomain = IdAccessPathMapDomain module Summary = Summary.Make(struct - type summary = QuandarySummary.t + type payload = QuandarySummary.t - let update_payload summary payload = - { payload with Specs.quandary = Some summary; } + let update_payload quandary_payload (summary : Specs.summary) = + { summary with payload = { summary.payload with quandary = Some quandary_payload }} - let read_from_payload payload = - match payload.Specs.quandary with - | None -> Some (TaintSpecification.to_summary_access_tree TaintDomain.empty) - | summary_opt -> summary_opt + let read_payload (summary : Specs.summary) = + summary.payload.quandary end) module Domain = struct @@ -505,8 +503,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct module Interprocedural = AbstractInterpreter.Interprocedural(Summary) - let checker ({ Callbacks.tenv; summary } as callback) : Specs.summary = - let proc_name = Specs.get_proc_name summary in + let checker ({ Callbacks.tenv; } as callback) : Specs.summary = (* bind parameters to a trace with a tainted source (if applicable) *) let make_initial pdesc = @@ -541,6 +538,5 @@ module Make (TaintSpecification : TaintSpec.S) = struct then failwith "Couldn't compute post" else None in let make_extras = FormalMap.make in - ignore (Interprocedural.compute_and_store_post ~compute_post ~make_extras callback); - Specs.get_summary_unsafe "taint analysis" proc_name + Interprocedural.compute_and_store_post ~compute_post ~make_extras callback end diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 4b2cf4537..647519743 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -109,9 +109,7 @@ let tests = make_load_fld ~rhs_typ:Typ.Tvoid lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) in let assert_empty = invariant "{ }" in (* hack: register an empty analyze_ondemand to prevent a crash because the callback is unset *) - let analyze_ondemand _ proc_desc = - let proc_name = Procdesc.get_proc_name proc_desc in - Specs.reset_summary proc_name None None in + let analyze_ondemand _ summary _ = summary in let get_proc_desc _ = None in let callbacks = { diff --git a/infer/tests/codetoanalyze/java/quandary/UnknownCode.java b/infer/tests/codetoanalyze/java/quandary/UnknownCode.java index 4e4edb409..e48f9e8f6 100644 --- a/infer/tests/codetoanalyze/java/quandary/UnknownCode.java +++ b/infer/tests/codetoanalyze/java/quandary/UnknownCode.java @@ -79,13 +79,13 @@ public abstract class UnknownCode { InferTaint.inferSensitiveSink(launderedSource); } - void FN_propagateViaUnknownNativeCodeBad() { + void propagateViaUnknownNativeCodeBad() { Object source = InferTaint.inferSecretSource(); Object launderedSource = nativeMethod(source); InferTaint.inferSensitiveSink(launderedSource); } - static void FN_propagateViaUnknownAbstractCodeBad() { + static void propagateViaUnknownAbstractCodeBad() { Object source = InferTaint.inferSecretSource(); Object launderedSource = nativeMethod(source); InferTaint.inferSensitiveSink(launderedSource); diff --git a/infer/tests/codetoanalyze/java/quandary/issues.exp b/infer/tests/codetoanalyze/java/quandary/issues.exp index c92ebebff..f789b8291 100644 --- a/infer/tests/codetoanalyze/java/quandary/issues.exp +++ b/infer/tests/codetoanalyze/java/quandary/issues.exp @@ -172,7 +172,9 @@ codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.callPropagateFoot codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.callUnknownSetterBad(Intent), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.propagateEmptyBad(), 6, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.propagateEmptyBad(), 7, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.propagateViaUnknownAbstractCodeBad(), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.propagateViaUnknownConstructorBad(), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] +codetoanalyze/java/quandary/UnknownCode.java, void UnknownCode.propagateViaUnknownNativeCodeBad(), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)] codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewChromeClientSinks(WebView,WebChromeClient), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsAlert(WebView,String,String,JsResult)] codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewChromeClientSinks(WebView,WebChromeClient), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsBeforeUnload(WebView,String,String,JsResult)] codetoanalyze/java/quandary/WebViews.java, void WebViews.callWebviewChromeClientSinks(WebView,WebChromeClient), 5, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to boolean WebChromeClient.onJsConfirm(WebView,String,String,JsResult)]