diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 5b84667c9..1124acbe9 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1478,11 +1478,15 @@ let do_analysis exe_env = 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) + if not (Config.eradicate || Config.checkers) && not (Procdesc.did_preanalysis proc_desc) then (* Eradicate and the checkers don't need the Nullify/Remove_temps/Abstract instructions that the preanalysis inserts. *) - Preanal.doit proc_desc (Exe_env.get_cg exe_env) tenv; + begin + Preanal.do_liveness proc_desc tenv; + Preanal.do_abstraction proc_desc; + Preanal.do_dynamic_dispatch proc_desc (Exe_env.get_cg exe_env) tenv `None + end; let summaryfp = Config.run_in_footprint_mode (analyze_proc source exe_env) proc_desc in Specs.add_summary proc_name summaryfp; diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index d0e2e657e..e77596270 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -11,11 +11,12 @@ open! IStd (** mutate the cfg/cg to add dynamic dispatch handling *) -let add_dispatch_calls pdesc cg tenv ~handle_dynamic_dispatch = +let add_dispatch_calls pdesc cg tenv policy = + let sound_dynamic_dispatch = policy = `Sound in let node_add_dispatch_calls caller_pname node = let call_flags_is_dispatch call_flags = (* if sound dispatch is turned off, only consider dispatch for interface calls *) - (handle_dynamic_dispatch && call_flags.CallFlags.cf_virtual) || + (sound_dynamic_dispatch && call_flags.CallFlags.cf_virtual) || call_flags.CallFlags.cf_interface in let instr_is_dispatch_call = function | Sil.Call (_, _, _, _, call_flags) -> call_flags_is_dispatch call_flags @@ -39,7 +40,7 @@ let add_dispatch_calls pdesc cg tenv ~handle_dynamic_dispatch = (match sorted_overrides with | ((_, target_pname) :: _) as all_targets -> let targets_to_add = - if handle_dynamic_dispatch then + if sound_dynamic_dispatch then IList.map snd all_targets else (* if sound dispatch is turned off, consider only the first target. we do this @@ -302,19 +303,17 @@ let do_copy_propagation pdesc tenv = let do_liveness pdesc tenv = let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in - LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) + let liveness_inv_map = + LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) in + if Config.copy_propagation then do_copy_propagation pdesc tenv; + add_nullify_instrs pdesc tenv liveness_inv_map; + Procdesc.signal_did_preanalysis pdesc -let doit ?(handle_dynamic_dispatch= (Config.dynamic_dispatch = `Sound)) pdesc cg tenv = - if not (Procdesc.did_preanalysis pdesc) - then - begin - Procdesc.signal_did_preanalysis pdesc; - if Config.copy_propagation then do_copy_propagation pdesc tenv; - let liveness_inv_map = do_liveness pdesc tenv in - if Config.dynamic_dispatch <> `Lazy && Config.copy_propagation - then remove_dead_frontend_stores pdesc liveness_inv_map; - add_nullify_instrs pdesc tenv liveness_inv_map; - if Config.dynamic_dispatch <> `Lazy - then add_dispatch_calls ~handle_dynamic_dispatch pdesc cg tenv; - add_abstraction_instructions pdesc; - end +let do_abstraction pdesc = + add_abstraction_instructions pdesc; + Procdesc.signal_did_preanalysis pdesc + +let do_dynamic_dispatch pdesc cg tenv policy = + if policy <> `Lazy + then add_dispatch_calls pdesc cg tenv policy; + Procdesc.signal_did_preanalysis pdesc diff --git a/infer/src/backend/preanal.mli b/infer/src/backend/preanal.mli index b7b8a523b..601ccae1f 100644 --- a/infer/src/backend/preanal.mli +++ b/infer/src/backend/preanal.mli @@ -10,7 +10,15 @@ open! IStd -(** Preanalysis for eliminating dead local variables *) +(** Various preanalysis passes for transforming the IR in useful ways *) -(** Perform liveness analysis *) -val doit : ?handle_dynamic_dispatch:bool -> Procdesc.t -> Cg.t -> Tenv.t -> unit +(** perform liveness analysis and insert Nullify/Remove_temps instructions into the IR to make it + easy for analyses to do abstract garbage collection *) +val do_liveness : Procdesc.t -> Tenv.t -> unit + +(** add Abstract instructions into the IR to give hints about when abstraction should be + performed *) +val do_abstraction : Procdesc.t -> unit + +(** add possible dynamic dispatch targets to the call_flags of each call site *) +val do_dynamic_dispatch : Procdesc.t -> Cg.t -> Tenv.t -> Config.dynamic_dispatch_policy -> unit diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 9726279f8..8542d9475 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -215,6 +215,11 @@ let whitelisted_cpp_classes = [ ["std"; "__normal_iterator"]; (* libstdc++ internal name of vector iterator *) ] +type dynamic_dispatch_policy = [ + | `Lazy + | `Sound + | `None +] (** Compile time configuration values *) diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 48a059292..20e8d475b 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -35,6 +35,11 @@ val ml_bucket_symbols : type os_type = Unix | Win32 | Cygwin +type dynamic_dispatch_policy = [ + | `Lazy + | `Sound + | `None +] (** Constant configuration values *) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 3a741b765..09a5e09a3 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -517,7 +517,12 @@ module Make (TaintSpecification : TaintSpec.S) = struct let checker callback = let compute_post (proc_data : formal_map ProcData.t) = - Preanal.doit ~handle_dynamic_dispatch:true proc_data.pdesc (Cg.create None) proc_data.tenv; + if not (Procdesc.did_preanalysis proc_data.pdesc) + then + begin + Preanal.do_liveness proc_data.pdesc proc_data.tenv; + Preanal.do_dynamic_dispatch proc_data.pdesc (Cg.create None) proc_data.tenv `Sound; + end; match Analyzer.compute_post proc_data with | Some { access_tree; } -> Some (make_summary proc_data.extras access_tree)