From 389907f4da632851bee57a35f151bdcef1ed05ca Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 29 Jul 2021 12:04:52 -0700 Subject: [PATCH] [biabduction] specialise java models without non-determinism Summary: Dynamic dispatch in java requires specialisation of models. Models do not have a CFG, nor attributes, in the capture DB, so the solution til now was to get those from the summary of the model. Each code path (CFG, attributes) could introduce non-determinism by allowing summaries to mask functions in the capture DB, and doing so depending on race conditions of the analysis (whether a summary has been written or not), as well as by the fact that CFGs from the capture DB are not pre-analysed, while summary CFGs are. This diff eliminates both code path usages in specialisation by strictly separating functions into captured functions and models. Other summaries are never consulted, and thus cannot introduce non-determinism through timing. NB model specialisation for clang models has been disabled in the past. Reviewed By: da319 Differential Revision: D29915082 fbshipit-source-id: 313a60e17 --- infer/src/absint/AnalysisCallbacks.ml | 9 +++----- infer/src/absint/AnalysisCallbacks.mli | 12 ++++------- infer/src/backend/CallbackOfChecker.ml | 5 ++--- infer/src/backend/Summary.ml | 7 +++++++ infer/src/backend/Summary.mli | 2 ++ infer/src/backend/ondemand.mli | 3 --- infer/src/biabduction/SymExec.ml | 29 ++++++++++++++++---------- infer/src/biabduction/Tabulation.ml | 8 ++++++- infer/src/unit/analyzerTester.ml | 5 ++--- 9 files changed, 45 insertions(+), 35 deletions(-) diff --git a/infer/src/absint/AnalysisCallbacks.ml b/infer/src/absint/AnalysisCallbacks.ml index bc232fb2e..9ab8f00bb 100644 --- a/infer/src/absint/AnalysisCallbacks.ml +++ b/infer/src/absint/AnalysisCallbacks.ml @@ -9,11 +9,10 @@ open! IStd module L = Logging type callbacks = - { get_proc_desc_f: Procname.t -> Procdesc.t option - ; html_debug_new_node_session_f: + { html_debug_new_node_session_f: 'a. ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO] -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a - ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option } + ; get_model_proc_desc_f: Procname.t -> Procdesc.t option } let callbacks_ref : callbacks option ref = ref None @@ -27,10 +26,8 @@ let get_callbacks () = L.die InternalError "Callbacks not set" -let get_proc_desc proc_name = (get_callbacks ()).get_proc_desc_f proc_name - let html_debug_new_node_session ?kind ~pp_name node ~f = (get_callbacks ()).html_debug_new_node_session_f ?kind ~pp_name node ~f -let proc_resolve_attributes proc_name = (get_callbacks ()).proc_resolve_attributes_f proc_name +let get_model_proc_desc proc_name = (get_callbacks ()).get_model_proc_desc_f proc_name diff --git a/infer/src/absint/AnalysisCallbacks.mli b/infer/src/absint/AnalysisCallbacks.mli index 3ceb31266..d6a388fdc 100644 --- a/infer/src/absint/AnalysisCallbacks.mli +++ b/infer/src/absint/AnalysisCallbacks.mli @@ -9,8 +9,8 @@ open! IStd (** {2 Analysis API} *) -val get_proc_desc : Procname.t -> Procdesc.t option -(** set to [Ondemand.get_proc_desc] *) +val get_model_proc_desc : Procname.t -> Procdesc.t option +(** get the preanalysed procdesc of a model; raises if procname given is not a biabduction model *) val html_debug_new_node_session : ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO] @@ -20,20 +20,16 @@ val html_debug_new_node_session : -> 'a (** set to [NodePrinter.with_session] *) -val proc_resolve_attributes : Procname.t -> ProcAttributes.t option -(** set to [Summary.OnDisk.proc_resolve_attributes] *) - (** {2 Callbacks management}*) (** These callbacks are used to break the dependency cycles between some modules. Specifically, we put here functions needed for the analysis that depend on modules higher up the dependency graph than this library but whose type does not. *) type callbacks = - { get_proc_desc_f: Procname.t -> Procdesc.t option - ; html_debug_new_node_session_f: + { html_debug_new_node_session_f: 'a. ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO] -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a - ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option } + ; get_model_proc_desc_f: Procname.t -> Procdesc.t option } val set_callbacks : callbacks -> unit (** make sure this is called before starting any actual analysis *) diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index b95b45013..59ecea2d8 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -11,9 +11,8 @@ open! IStd crash) *) let () = AnalysisCallbacks.set_callbacks - { get_proc_desc_f= Ondemand.get_proc_desc - ; html_debug_new_node_session_f= NodePrinter.with_session - ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes } + { html_debug_new_node_session_f= NodePrinter.with_session + ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc } let mk_interprocedural_t ~f_analyze_dep ~get_payload exe_env summary diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 8d9c5535f..895a5706d 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -261,6 +261,13 @@ module OnDisk = struct load_summary_to_spec_table proc_name + let get_model_proc_desc model_name = + if not (BiabductionModels.mem model_name) then + Logging.die InternalError "Requested summary of model that couldn't be found: %a@\n" + Procname.pp model_name + else Option.map (get model_name) ~f:(fun (s : full_summary) -> s.proc_desc) + + (** Try to find the attributes for a defined proc. First look at specs (to get attributes computed by analysis) then look at the attributes table. If no attributes can be found, return None. *) let proc_resolve_attributes proc_name = diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index 69db5d3f8..df04fc22a 100644 --- a/infer/src/backend/Summary.mli +++ b/infer/src/backend/Summary.mli @@ -99,4 +99,6 @@ module OnDisk : sig val pp_specs_from_config : Format.formatter -> unit (** pretty print all stored summaries *) + + val get_model_proc_desc : Procname.t -> Procdesc.t option end diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index b7933f214..63b6fd430 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -9,9 +9,6 @@ open! IStd (** Module for on-demand analysis. *) -val get_proc_desc : Procname.t -> Procdesc.t option -(** Find a proc desc for the procedure, perhaps loading it from disk. *) - val analyze_proc_name : Exe_env.t -> caller_summary:Summary.t -> Procname.t -> Summary.t option (** [analyze_proc_name exe_env ~caller_summary callee_pname] performs an on-demand analysis of [callee_pname] triggered during the analysis of [caller_summary] *) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index aac955d5d..73c312c39 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -590,6 +590,17 @@ type resolve_and_analyze_result = ; resolved_procdesc_opt: Procdesc.t option ; resolved_summary_opt: (Procdesc.t * BiabductionSummary.t) option } +let get_proc_desc proc_name = + if BiabductionModels.mem proc_name then AnalysisCallbacks.get_model_proc_desc proc_name + else Procdesc.load proc_name + + +let get_attributes proc_name = + if BiabductionModels.mem proc_name then + AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes + else Attributes.load proc_name + + (** Resolve the procedure name and run the analysis of the resolved procedure if not already analyzed *) let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv} @@ -601,15 +612,15 @@ let resolve_and_analyze {InterproceduralAnalysis.analyze_dependency; proc_desc; whether the method is defined or generated by the specialization *) let analyze_ondemand resolved_pname = if Procname.equal resolved_pname callee_proc_name then - (AnalysisCallbacks.get_proc_desc callee_proc_name, analyze_dependency callee_proc_name) + (get_proc_desc callee_proc_name, analyze_dependency callee_proc_name) else (* Create the type specialized procedure description and analyze it directly *) let resolved_proc_desc_option = - match AnalysisCallbacks.get_proc_desc resolved_pname with + match get_proc_desc resolved_pname with | Some _ as resolved_proc_desc -> resolved_proc_desc | None -> - let procdesc_opt = AnalysisCallbacks.get_proc_desc callee_proc_name in + let procdesc_opt = get_proc_desc callee_proc_name in Option.map procdesc_opt ~f:(fun callee_proc_desc -> (* It is possible that the types of the arguments are not as precise as the type of the objects in the heap, so we should update them to get the best results. *) @@ -988,7 +999,7 @@ let execute_store ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv; let is_variadic_procname callee_pname = - Option.exists (AnalysisCallbacks.proc_resolve_attributes callee_pname) ~f:(fun proc_attrs -> + Option.exists (get_attributes callee_pname) ~f:(fun proc_attrs -> proc_attrs.ProcAttributes.is_variadic ) @@ -1002,9 +1013,7 @@ let resolve_and_analyze_no_dynamic_dispatch {InterproceduralAnalysis.analyze_dep callee_pname in let resolved_summary_opt = analyze_dependency resolved_pname in - { resolved_pname - ; resolved_procdesc_opt= AnalysisCallbacks.get_proc_desc resolved_pname - ; resolved_summary_opt } + {resolved_pname; resolved_procdesc_opt= get_proc_desc resolved_pname; resolved_summary_opt} let resolve_and_analyze_clang analysis_data prop_r n_actual_params callee_pname call_flags = @@ -1556,9 +1565,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots callee_pname ret_annots loc path_pos in let callee_loc_opt = - Option.map - ~f:(fun attributes -> attributes.ProcAttributes.loc) - (AnalysisCallbacks.proc_resolve_attributes callee_pname) + Option.map ~f:(fun attributes -> attributes.ProcAttributes.loc) (get_attributes callee_pname) in let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in [(prop_with_undef_attr, skip_path)] @@ -1600,7 +1607,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as builtin_args) = - match AnalysisCallbacks.proc_resolve_attributes proc_name with + match get_attributes proc_name with | Some callee_attributes -> ( match callee_attributes.ProcAttributes.sentinel_attr with | Some sentinel -> diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 307da3918..c880f2289 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -745,9 +745,15 @@ let prop_set_exn tenv pname prop se_exn = Prop.normalize tenv (Prop.set prop ~sigma:sigma') +let get_attributes proc_name = + if BiabductionModels.mem proc_name then + AnalysisCallbacks.get_model_proc_desc proc_name |> Option.map ~f:Procdesc.get_attributes + else Attributes.load proc_name + + (** Include a subtrace for a procedure call if the callee is not a model. *) let include_subtrace callee_pname = - match AnalysisCallbacks.proc_resolve_attributes callee_pname with + match get_attributes callee_pname with | Some attrs -> (not attrs.ProcAttributes.is_biabduction_model) && SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 57fbacd1f..e56f598bf 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -300,9 +300,8 @@ module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) = let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests = AnalysisCallbacks.set_callbacks - { get_proc_desc_f= Ondemand.get_proc_desc - ; html_debug_new_node_session_f= NodePrinter.with_session - ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes } ; + { html_debug_new_node_session_f= NodePrinter.with_session + ; get_model_proc_desc_f= Summary.OnDisk.get_model_proc_desc } ; let open OUnit2 in List.concat_map ~f:(fun (name, test_program) ->