[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

@@ -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

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 add_dispatch_calls pdesc cg tenv =
-  let sound_dynamic_dispatch = policy = `Sound in
+  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,7 +59,6 @@ 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
 
 (** add instructions to perform abstraction *)
@@ -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 =
+let do_dynamic_dispatch pdesc cg tenv =
-  if policy <> `Lazy
+  let pname = Procdesc.get_proc_name pdesc in
-  then add_dispatch_calls pdesc cg tenv policy;
+  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

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

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
+  let default_mode =
-  else !dynamic_dispatch
+    match analyzer with
+    | Infer
+    | Tracing -> `Lazy
+    | Quandary -> `Sound
+    | _ -> `None in
+  Option.value ~default:default_mode !dynamic_dispatch
 
 let specs_library =
   match infer_cache with

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

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; } ->