From d7f112a6403edb213ad6cc78611f5e4125dfd14b Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Tue, 27 Dec 2016 14:37:03 -0800 Subject: [PATCH] [infer][java] choose the dynamic dispatch handling mode from the command line Summary: This more easily allow to switch between the different modes for handeling dynamic dispatch Reviewed By: sblackshear Differential Revision: D4367556 fbshipit-source-id: 795d2c4 --- infer/src/backend/interproc.ml | 2 +- infer/src/backend/preanal.ml | 15 ++++++++------- infer/src/backend/preanal.mli | 2 +- infer/src/base/Config.ml | 18 ++++++++++++------ infer/src/base/Config.mli | 7 ++++--- infer/src/quandary/TaintAnalysis.ml | 2 +- 6 files changed, 27 insertions(+), 19 deletions(-) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 1124acbe9..56424d60e 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1485,7 +1485,7 @@ let do_analysis exe_env = 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 + Preanal.do_dynamic_dispatch proc_desc (Exe_env.get_cg exe_env) tenv end; let summaryfp = Config.run_in_footprint_mode (analyze_proc source exe_env) proc_desc in diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index e77596270..635226787 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -11,8 +11,8 @@ open! IStd (** mutate the cfg/cg to add dynamic dispatch handling *) -let add_dispatch_calls pdesc cg tenv policy = - let sound_dynamic_dispatch = policy = `Sound in +let add_dispatch_calls pdesc cg tenv = + let sound_dynamic_dispatch = (Config.dynamic_dispatch = `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 *) @@ -59,8 +59,7 @@ let add_dispatch_calls pdesc cg tenv policy = IList.map replace_dispatch_calls instrs |> Procdesc.Node.replace_instrs node in let pname = Procdesc.get_proc_name pdesc in - if Procname.is_java pname then - Procdesc.iter_nodes (node_add_dispatch_calls pname) pdesc + Procdesc.iter_nodes (node_add_dispatch_calls pname) pdesc (** add instructions to perform abstraction *) let add_abstraction_instructions pdesc = @@ -313,7 +312,9 @@ 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; +let do_dynamic_dispatch pdesc cg tenv = + let pname = Procdesc.get_proc_name pdesc in + if Procname.is_java pname && + (Config.dynamic_dispatch = `Interface || Config.dynamic_dispatch = `Sound) + then add_dispatch_calls pdesc cg tenv; Procdesc.signal_did_preanalysis pdesc diff --git a/infer/src/backend/preanal.mli b/infer/src/backend/preanal.mli index 601ccae1f..8948643b5 100644 --- a/infer/src/backend/preanal.mli +++ b/infer/src/backend/preanal.mli @@ -21,4 +21,4 @@ val do_liveness : Procdesc.t -> Tenv.t -> unit 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 +val do_dynamic_dispatch : Procdesc.t -> Cg.t -> Tenv.t -> unit diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 6235b43ee..dd44a2b35 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -216,9 +216,10 @@ let whitelisted_cpp_classes = [ ] type dynamic_dispatch_policy = [ - | `Lazy - | `Sound | `None + | `Interface + | `Sound + | `Lazy ] (** Compile time configuration values *) @@ -739,12 +740,12 @@ and dotty_cfg_libs = "Print the cfg of the code coming from the libraries" and dynamic_dispatch = - CLOpt.mk_symbol ~long:"dynamic-dispatch" ~default:`None + CLOpt.mk_symbol_opt ~long:"dynamic-dispatch" "Specify treatment of dynamic dispatch in Java code: 'none' treats dynamic dispatch as a call \ to unknown code, 'lazy' follows the JVM semantics and creates procedure descriptions during \ symbolic execution using the type information found in the abstract state; 'sound' is \ significantly more computationally expensive" - ~symbols:[("none", `None); ("lazy", `Lazy); ("sound", `Sound)] + ~symbols:[("none", `None); ("interface", `Interface); ("sound", `Sound); ("lazy", `Lazy)] and enable_checks = CLOpt.mk_string_list ~deprecated:["enable_checks"] ~long:"enable-checks" ~meta:"error name" @@ -1566,8 +1567,13 @@ let clang_frontend_action_string = @ (if clang_frontend_do_lint then ["linting"] else [])) let dynamic_dispatch = - if analyzer = Tracing || analyzer = Infer then `Lazy - else !dynamic_dispatch + let default_mode = + match analyzer with + | Infer + | Tracing -> `Lazy + | Quandary -> `Sound + | _ -> `None in + Option.value ~default:default_mode !dynamic_dispatch let specs_library = match infer_cache with diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 20e8d475b..aca39f71f 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -36,9 +36,10 @@ val ml_bucket_symbols : type os_type = Unix | Win32 | Cygwin type dynamic_dispatch_policy = [ - | `Lazy - | `Sound | `None + | `Interface + | `Sound + | `Lazy ] (** Constant configuration values *) @@ -175,7 +176,7 @@ val dependency_mode : bool val developer_mode : bool val disable_checks : string list val dotty_cfg_libs : bool -val dynamic_dispatch : [ `None | `Lazy | `Sound ] +val dynamic_dispatch : [ `None | `Interface | `Sound | `Lazy ] val enable_checks : string list val eradicate : bool val eradicate_condition_redundant : bool diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index ad8052a66..be20cb3af 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -520,7 +520,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct 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; + Preanal.do_dynamic_dispatch proc_data.pdesc (Cg.create None) proc_data.tenv; end; match Analyzer.compute_post proc_data with | Some { access_tree; } ->