diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 6a1b8655d..fcfec6656 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -95,7 +95,7 @@ struct module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig)) let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial = - Preanal.do_preanalysis pdesc None tenv ; + Preanal.do_preanalysis pdesc tenv ; let initial' = (initial, IdAccessPathMapDomain.empty) in Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial') diff --git a/infer/src/backend/InferAnalyze.ml b/infer/src/backend/InferAnalyze.ml index 66475b327..e7921dec8 100644 --- a/infer/src/backend/InferAnalyze.ml +++ b/infer/src/backend/InferAnalyze.ml @@ -145,8 +145,6 @@ let main ~changed_files ~makefile = ~f:(fun cl -> DB.string_crc_has_extension ~ext:"java" (DB.source_dir_to_string cl)) all_clusters) in - L.debug Analysis Quiet "Dynamic dispatch mode: %s@." - Config.(string_of_dynamic_dispatch dynamic_dispatch) ; print_legend () ; if Config.per_procedure_parallelism && not (Lazy.force is_java) then ( (* Java uses ZipLib which is incompatible with forking *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 827d261ac..c271cac3c 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1277,10 +1277,10 @@ let perform_transition proc_cfg tenv proc_name = () -let analyze_procedure_aux cg_opt tenv proc_desc = +let analyze_procedure_aux tenv proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in - Preanal.do_preanalysis proc_desc cg_opt tenv ; + Preanal.do_preanalysis proc_desc tenv ; let summaryfp = Config.run_in_footprint_mode (analyze_proc tenv) proc_cfg in Specs.add_summary proc_name summaryfp ; perform_transition proc_cfg tenv proc_name ; @@ -1292,8 +1292,7 @@ let analyze_procedure_aux cg_opt tenv proc_desc = let analyze_procedure {Callbacks.summary; proc_desc; tenv} : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in Specs.add_summary proc_name summary ; - ( try ignore (analyze_procedure_aux None tenv proc_desc) with exn -> + ( try ignore (analyze_procedure_aux tenv proc_desc) with exn -> reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ; Reporting.log_error_deprecated proc_name exn ) ; Specs.get_summary_unsafe __FILE__ proc_name - diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 7d7c3d1e8..34045c106 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -12,67 +12,6 @@ open! IStd open! PVariant module L = Logging -(** mutate the cfg/cg to add dynamic dispatch handling *) -let add_dispatch_calls pdesc cg tenv = - let sound_dynamic_dispatch = Config.(equal_dynamic_dispatch 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 *) - 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 - | _ -> - false - in - let has_dispatch_call instrs = List.exists ~f:instr_is_dispatch_call instrs in - let replace_dispatch_calls = function - | Sil.Call - ( ret_id - , (Exp.Const Const.Cfun callee_pname as call_exp) - , ((_, receiver_typ) :: _ as args) - , loc - , call_flags ) as instr - when call_flags_is_dispatch call_flags - -> ( - (* the frontend should not populate the list of targets *) - assert (List.is_empty call_flags.CallFlags.cf_targets) ; - let receiver_typ_no_ptr = - match receiver_typ.Typ.desc with Typ.Tptr (typ', _) -> typ' | _ -> receiver_typ - in - let sorted_overrides = - let overrides = Prover.get_overrides_of tenv receiver_typ_no_ptr callee_pname in - List.sort ~cmp:(fun (_, p1) (_, p2) -> Typ.Procname.compare p1 p2) overrides - in - match sorted_overrides with - | (_, target_pname) :: _ as all_targets -> - let targets_to_add = - if sound_dynamic_dispatch then List.map ~f:snd all_targets - else - (* if sound dispatch is turned off, consider only the first target. we do this - because choosing all targets is too expensive for everyday use *) - [target_pname] - in - List.iter - ~f:(fun target_pname -> Cg.add_edge cg caller_pname target_pname) - targets_to_add ; - let call_flags' = {call_flags with CallFlags.cf_targets= targets_to_add} in - Sil.Call (ret_id, call_exp, args, loc, call_flags') - | [] -> - instr ) - | instr -> - instr - in - let instrs = Procdesc.Node.get_instrs node in - if has_dispatch_call instrs then List.map ~f:replace_dispatch_calls instrs - |> Procdesc.Node.replace_instrs node - in - let pname = Procdesc.get_proc_name pdesc in - Procdesc.iter_nodes (node_add_dispatch_calls pname) pdesc - - (** add instructions to perform abstraction *) let add_abstraction_instructions pdesc = let open Procdesc in @@ -258,20 +197,6 @@ let do_abstraction pdesc = Procdesc.signal_did_preanalysis pdesc -(** add possible dynamic dispatch targets to the call_flags of each call site *) -let do_dynamic_dispatch pdesc cg tenv = - ( match Config.dynamic_dispatch with - | Interface | Sound -> - let pname = Procdesc.get_proc_name pdesc in - if Typ.Procname.is_java pname then add_dispatch_calls pdesc cg tenv - | NoDynamicDispatch | Lazy -> - () ) ; - Procdesc.signal_did_preanalysis pdesc - - -let do_preanalysis pdesc cg_opt tenv = - if not (Procdesc.did_preanalysis pdesc) then ( - do_liveness pdesc tenv ; - do_abstraction pdesc ; - Option.iter cg_opt ~f:(fun cg -> do_dynamic_dispatch pdesc cg tenv) ) +let do_preanalysis pdesc tenv = + if not (Procdesc.did_preanalysis pdesc) then ( do_liveness pdesc tenv ; do_abstraction pdesc ) diff --git a/infer/src/backend/preanal.mli b/infer/src/backend/preanal.mli index ac5e4ace4..fdb62159d 100644 --- a/infer/src/backend/preanal.mli +++ b/infer/src/backend/preanal.mli @@ -10,5 +10,5 @@ open! IStd -val do_preanalysis : Procdesc.t -> Cg.t option -> Tenv.t -> unit +val do_preanalysis : Procdesc.t -> Tenv.t -> unit (** Various preanalysis passes for transforming the IR in useful ways *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index cfb7123df..812ce26ad 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -614,26 +614,6 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Typ.Procna 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.(equal_dynamic_dispatch dynamic_dispatch Sound) then - let targets = - if call_flags.CallFlags.cf_virtual then - (* virtual call--either [called_pname] or an override in some subtype may be called *) - callee_pname :: call_flags.CallFlags.cf_targets - else - (* interface call--[called_pname] has no implementation), we don't want to consider *) - call_flags.CallFlags.cf_targets - (* interface call, don't want to consider *) - in - (* return true if (receiver typ of [target_pname]) <: [actual_receiver_typ] *) - let may_dispatch_to target_pname = - let target_receiver_typ = get_receiver_typ target_pname actual_receiver_typ in - Prover.Subtyping_check.check_subtype tenv target_receiver_typ actual_receiver_typ - in - let resolved_pname = do_resolve callee_pname receiver_exp actual_receiver_typ in - let feasible_targets = List.filter ~f:may_dispatch_to targets in - (* make sure [resolved_pname] is not a duplicate *) - if List.mem ~equal:Typ.Procname.equal feasible_targets resolved_pname then feasible_targets - else resolved_pname :: feasible_targets else let resolved_target = do_resolve callee_pname receiver_exp actual_receiver_typ in match call_flags.CallFlags.cf_targets with @@ -1193,7 +1173,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path exec_builtin (call_args prop_ callee_pname actual_params ret_id loc) | None -> match callee_pname with - | Java callee_pname_java when Config.(equal_dynamic_dispatch dynamic_dispatch Lazy) + | Java callee_pname_java when Config.dynamic_dispatch -> ( let norm_prop, norm_args' = normalize_params tenv current_pname prop_ actual_params in let norm_args = call_constructor_url_update_args callee_pname norm_args' in diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 64caccfaa..82a4de13c 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -399,19 +399,6 @@ let whitelisted_cpp_classes = ; other_whitelisted_cpp_classes ] -type dynamic_dispatch = NoDynamicDispatch | Interface | Sound | Lazy [@@deriving compare] - -let equal_dynamic_dispatch = [%compare.equal : dynamic_dispatch] - -let string_to_dynamic_dispatch = - [("none", NoDynamicDispatch); ("interface", Interface); ("sound", Sound); ("lazy", Lazy)] - - -let string_of_dynamic_dispatch ddp = - List.find_exn ~f:(fun (_, ddp') -> equal_dynamic_dispatch ddp ddp') string_to_dynamic_dispatch - |> fst - - let pp_version fmt () = F.fprintf fmt "Infer version %s@\nCopyright 2009 - present Facebook. All Rights Reserved." Version.versionString @@ -1201,12 +1188,6 @@ and dump_duplicate_symbols = "Dump all symbols with the same name that are defined in more than one file." -and dynamic_dispatch = - 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:string_to_dynamic_dispatch - - and eradicate_condition_redundant = CLOpt.mk_bool ~long:"eradicate-condition-redundant" "Condition redundant warnings" @@ -2753,17 +2734,12 @@ let clang_frontend_action_string = let dynamic_dispatch = - let default_mode = - match analyzer with - | Checkers when biabduction -> - Lazy - | Checkers when quandary -> - Sound - | _ -> - NoDynamicDispatch - in - Option.value ~default:default_mode !dynamic_dispatch + CLOpt.mk_bool ~long:"dynamic-dispatch" ~default:biabduction + "Specify treatment of dynamic dispatch in Java code: false 'none' treats dynamic dispatch as a call to unknown code and true triggers lazy dynamic dispatch. The latter mode follows the JVM semantics and creates procedure descriptions during symbolic execution using the type information found in the abstract state" + ~in_help:CLOpt.([(Analyze, manual_java)]) + +let dynamic_dispatch = !dynamic_dispatch let specs_library = match infer_cache with diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 4d8199dbb..b28cd38fa 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -70,12 +70,6 @@ type compilation_database_dependencies = | NoDeps [@@deriving compare] -type dynamic_dispatch = NoDynamicDispatch | Interface | Sound | Lazy [@@deriving compare] - -val equal_dynamic_dispatch : dynamic_dispatch -> dynamic_dispatch -> bool - -val string_of_dynamic_dispatch : dynamic_dispatch -> string - type build_system = | BAnalyze | BAnt @@ -384,7 +378,7 @@ val dotty_cfg_libs : bool val dump_duplicate_symbols : bool -val dynamic_dispatch : dynamic_dispatch +val dynamic_dispatch : bool val eradicate : bool diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 43dffd698..479a83b2d 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -546,7 +546,7 @@ let checker : Callbacks.proc_callback_args -> Specs.summary = fun {proc_desc; tenv; summary; get_proc_desc} -> let proc_name = Specs.get_proc_name summary in let proc_data = ProcData.make proc_desc tenv get_proc_desc in - Preanal.do_preanalysis proc_desc None tenv ; + Preanal.do_preanalysis proc_desc tenv ; match compute_post proc_data with | Some post -> if Config.bo_debug >= 1 then print_summary proc_name post ; diff --git a/infer/tests/codetoanalyze/java/checkers/Makefile b/infer/tests/codetoanalyze/java/checkers/Makefile index 72d4c9dfe..80737490e 100644 --- a/infer/tests/codetoanalyze/java/checkers/Makefile +++ b/infer/tests/codetoanalyze/java/checkers/Makefile @@ -9,7 +9,7 @@ TESTS_DIR = ../../.. ANALYZER = checkers INFER_OPTIONS = \ - --debug-exceptions --dynamic-dispatch none --no-default-checkers \ + --debug-exceptions --no-default-checkers \ --annotation-reachability --fragment-retains-view --immutable-cast --printf-args --quandary \ --suggest-nullable --check-nullable --racerd \