[config] Dynamic dispatch methods are mutually exclusive

Summary:
Change command line options for dynamic dispatch to capture that the
alternatives are mutually exclusive.

Reviewed By: jeremydubreil

Differential Revision: D4074540

fbshipit-source-id: c329717

infer/src/backend/interproc.ml

@@ -1460,7 +1460,7 @@ let do_analysis exe_env =
       { (Cfg.Procdesc.get_attributes pdesc) with
         ProcAttributes.err_log = static_err_log; } in
     let proc_desc_option =
-      if Config.dynamic_dispatch_lazy
+      if Config.dynamic_dispatch = `Lazy
       then Some pdesc
       else None in
     Specs.init_summary (dep, nodes, proc_flags, calls, None, attributes, proc_desc_option) in
@@ -1478,7 +1478,7 @@ let do_analysis exe_env =
     let get_proc_desc proc_name =
       match Exe_env.get_proc_desc exe_env proc_name with
       | Some pdesc -> Some pdesc
-      | None when Config.dynamic_dispatch_lazy ->
+      | None when Config.dynamic_dispatch = `Lazy ->
           Option.map_default
             (fun summary -> summary.Specs.proc_desc_option)
             None

infer/src/backend/ondemand.ml

@@ -137,7 +137,7 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
       Cg.add_defined_node cg callee_pname;
       cg in
     let callee_pdesc_option =
-      if Config.dynamic_dispatch_lazy
+      if Config.dynamic_dispatch = `Lazy
       then Some callee_pdesc
       else None in
     Specs.reset_summary call_graph callee_pname attributes_opt callee_pdesc_option;

infer/src/backend/preanal.ml

@@ -289,17 +289,17 @@ 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 doit ?(handle_dynamic_dispatch=Config.dynamic_dispatch_sound) pdesc cg tenv =
+let doit ?(handle_dynamic_dispatch= (Config.dynamic_dispatch = `Sound)) pdesc cg tenv =
   if not (Cfg.Procdesc.did_preanalysis pdesc)
   then
     begin
       Cfg.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 not Config.dynamic_dispatch_lazy && Config.copy_propagation
+      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 not Config.dynamic_dispatch_lazy
+      if Config.dynamic_dispatch <> `Lazy
       then add_dispatch_calls ~handle_dynamic_dispatch pdesc cg tenv;
       add_abstraction_instructions pdesc;
     end

infer/src/backend/symExec.ml

@@ -553,7 +553,7 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t
       if !Config.curr_language <> Config.Java then
         (* default mode for Obj-C/C++/Java virtual calls: resolution only *)
         [do_resolve callee_pname receiver_exp actual_receiver_typ]
-      else if Config.dynamic_dispatch_sound then
+      else if Config.dynamic_dispatch = `Sound then
         let targets =
           if call_flags.CallFlags.cf_virtual
           then
@@ -1059,7 +1059,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
   | Sil.Call (ret_id,
               Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
               actual_params, loc, call_flags)
-    when Config.dynamic_dispatch_lazy ->
+    when Config.dynamic_dispatch = `Lazy ->
       let norm_prop, norm_args =
         normalize_params
           tenv

infer/src/base/Config.ml

@@ -807,16 +807,13 @@ and dotty_cfg_libs =
   CLOpt.mk_bool ~deprecated:["dotty_no_cfg_libs"] ~long:"dotty-cfg-libs" ~default:true
     "Print the cfg of the code coming from the libraries"
 
-and dynamic_dispatch_lazy =
-  CLOpt.mk_bool ~long:"dynamic-dispatch-lazy"
-    ~exes:CLOpt.[Java]
-    "Handle dynamic dispatch by following the JVM semantics and creating procedure descriptions \
-     during the symbolic execution using the type information found in the abstract state"
-
-and dynamic_dispatch_sound =
-  CLOpt.mk_bool ~long:"dynamic-dispatch-sound"
-    ~exes:CLOpt.[Java]
-    "Dynamic dispatch for interface calls in Java"
+and dynamic_dispatch =
+  CLOpt.mk_symbol ~long:"dynamic-dispatch" ~default:`None
+    "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)]
 
 and enable_checks =
   CLOpt.mk_string_list ~deprecated:["enable_checks"] ~long:"enable-checks" ~meta:"error name"
@@ -1502,8 +1499,7 @@ and dependency_mode = !dependencies
 and developer_mode = !developer_mode
 and disable_checks = !disable_checks
 and dotty_cfg_libs = !dotty_cfg_libs
-and dynamic_dispatch_lazy = (!dynamic_dispatch_lazy || !analyzer = Some Tracing)
-and dynamic_dispatch_sound = !dynamic_dispatch_sound
+and dynamic_dispatch = if !analyzer = Some Tracing then `Lazy else !dynamic_dispatch
 and enable_checks = !enable_checks
 and eradicate = !eradicate
 and eradicate_condition_redundant = !eradicate_condition_redundant

infer/src/base/Config.mli

@@ -179,8 +179,7 @@ val dependency_mode : bool
 val developer_mode : bool
 val disable_checks : string list
 val dotty_cfg_libs : bool
-val dynamic_dispatch_lazy : bool
-val dynamic_dispatch_sound : bool
+val dynamic_dispatch : [ `None | `Lazy | `Sound ]
 val enable_checks : string list
 val eradicate : bool
 val eradicate_condition_redundant : bool