diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index cedb7daf9..6ceed0dd4 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -156,10 +156,6 @@ let array_level = ref 0 (** Check whether to report Analysis_stops message in user mode *) let analysis_stops = ref false -(** experimental: dynamic dispatch for interface calls only in Java. off by default because of the - cost *) -let sound_dynamic_dispatch = ref true - type os_type = Unix | Win32 | Cygwin let os_type = match Sys.os_type with @@ -367,6 +363,9 @@ let default_failure_name = "ASSERTION_FAILURE" let analyze_models = from_env_variable "INFER_ANALYZE_MODELS" +(** experimental: dynamic dispatch for interface calls only in Java. off by default because of the + cost *) +let sound_dynamic_dispatch = from_env_variable "INFER_SOUND_DYNAMIC_DISPATCH" module Experiment = struct diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index caeae9b13..ff945f75e 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -392,7 +392,10 @@ let add_dispatch_calls cfg cg tenv f_translate_typ_opt = | None -> () in let node_add_dispatch_calls caller_pname node = (* TODO: handle dynamic dispatch for virtual calls as well *) - let call_flags_is_dispatch call_flags = call_flags.Sil.cf_interface in + let call_flags_is_dispatch call_flags = + (* if sound dispatch is turned off, only consider dispatch for interface calls *) + (Config.sound_dynamic_dispatch && call_flags.Sil.cf_virtual) || + call_flags.Sil.cf_interface in let instr_is_dispatch_call = function | Sil.Call (_, _, _, _, call_flags) -> call_flags_is_dispatch call_flags | _ -> false in @@ -409,14 +412,23 @@ let add_dispatch_calls cfg cg tenv f_translate_typ_opt = let overrides = Prover.get_overrides_of tenv receiver_typ_no_ptr callee_pname in IList.sort (fun (_, p1) (_, p2) -> Procname.compare p1 p2) overrides in (match sorted_overrides with - | [] -> instr - | (_, target_pname) :: _ -> - (* TODO: do this with all possible targets. for now, it is too slow to do this, so we - just pick one target *) - Cg.add_edge cg caller_pname target_pname; - pname_translate_types target_pname; - let call_flags' = { call_flags with Sil.cf_targets = [target_pname]; } in - Sil.Call (ret_ids, call_exp, args, loc, call_flags')) + | ((_, target_pname) :: targets) as all_targets -> + let targets_to_add = + if Config.sound_dynamic_dispatch then + IList.map 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 + IList.iter + (fun target_pname -> + pname_translate_types target_pname; + Cg.add_edge cg caller_pname target_pname) + targets_to_add; + let call_flags' = { call_flags with Sil.cf_targets = targets_to_add; } in + Sil.Call (ret_ids, call_exp, args, loc, call_flags') + | [] -> instr) + | instr -> instr in let instrs = Cfg.Node.get_instrs node in if has_dispatch_call instrs then @@ -430,5 +442,6 @@ let doit ?(f_translate_typ=None) cfg cg tenv = AllPreds.mk_table cfg; Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg tenv); AllPreds.clear_table (); - if !Config.sound_dynamic_dispatch then add_dispatch_calls cfg cg tenv f_translate_typ; + if !Config.curr_language = Config.Java + then add_dispatch_calls cfg cg tenv f_translate_typ; diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 9a9492b79..f17e4da17 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -669,31 +669,65 @@ let lookup_java_typ_from_string tenv typ_str = (** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal in the signature of [pname], resolve [pname] to T_actual.[pname]. *) -let resolve_virtual_pname cfg tenv prop actuals pname call_flags : Procname.t = +let resolve_virtual_pname cfg tenv prop actuals callee_pname call_flags : Procname.t list = let resolve receiver_exp pname prop = match resolve_typename prop receiver_exp with | Some class_name -> resolve_method tenv class_name pname | None -> pname in + let get_receiver_typ pname fallback_typ = + if !Config.curr_language = Config.Java then + try + let receiver_typ_str = Procname.java_get_class pname in + Sil.Tptr (lookup_java_typ_from_string tenv receiver_typ_str, Sil.Pk_pointer) + with Cannot_convert_string_to_typ _ -> fallback_typ + else fallback_typ in let receiver_types_equal pname actual_receiver_typ = - let formal_receiver_typ = - let receiver_typ_str = Procname.java_get_class pname in - Sil.Tptr (lookup_java_typ_from_string tenv receiver_typ_str, Sil.Pk_pointer) in + (* the type of the receiver according to the function signature *) + let formal_receiver_typ = get_receiver_typ pname actual_receiver_typ in Sil.typ_equal formal_receiver_typ actual_receiver_typ in + let do_resolve called_pname receiver_exp actual_receiver_typ = + if receiver_types_equal called_pname actual_receiver_typ + then resolve receiver_exp called_pname prop + else called_pname in match actuals with | _ when not (call_flags.Sil.cf_virtual || call_flags.Sil.cf_interface) -> (* if this is not a virtual or interface call, there's no need for resolution *) - pname + [callee_pname] | (receiver_exp, actual_receiver_typ) :: _ -> - if !Config.curr_language = Config.Java && call_flags.Sil.cf_interface && - !Config.sound_dynamic_dispatch && receiver_types_equal pname actual_receiver_typ then - (* pick one implementation of the interface method and call it *) - (* TODO: consider all implementations of the interface method *) - (* TODO: do this for virtual calls as well *) - match call_flags.Sil.cf_targets with - | target :: _ -> target - | _ -> pname + 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.sound_dynamic_dispatch then + let targets = + if call_flags.Sil.cf_virtual + then + (* virtual call--either [called_pname] or an override in some subtype may be called *) + callee_pname :: call_flags.Sil.cf_targets + else + (* interface call--[called_pname] has no implementation), we don't want to consider *) + call_flags.Sil.cf_targets in (* interface call, don't want to consider *) + (* 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 = IList.filter may_dispatch_to targets in + (* make sure [resolved_pname] is not a duplicate *) + if IList.mem Procname.equal resolved_pname feasible_targets + then feasible_targets + else resolved_pname :: feasible_targets else - (* [actual_receiver_typ] <: the formal receiver_type, do resolution *) - resolve receiver_exp pname prop + begin + match call_flags.Sil.cf_targets with + | target :: _ when call_flags.Sil.cf_interface && + receiver_types_equal callee_pname actual_receiver_typ -> + (* "production mode" of dynamic dispatch for Java: unsound, but faster. the handling + is restricted to interfaces: if we can't resolve an interface call, we pick the + first implementation of the interface and call it *) + [target] + | _ -> + (* default mode for Java virtual calls: resolution only *) + [do_resolve callee_pname receiver_exp actual_receiver_typ] + end | _ -> failwith "A virtual call must have a receiver" (** recognize calls to shared_ptr procedures and re-direct them to infer procedures for modelling *) @@ -1100,33 +1134,35 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path let norm_prop, norm_args = normalize_params pname _prop actual_params in let url_handled_args = call_constructor_url_update_args callee_pname norm_args in - let resolved_pname = + let resolved_pnames = resolve_virtual_pname cfg tenv norm_prop url_handled_args callee_pname call_flags in - if !Config.ondemand_enabled then - Ondemand.do_analysis pdesc resolved_pname; - let exec_skip_call ret_type = - skip_call norm_prop path resolved_pname loc ret_ids (Some ret_type) url_handled_args in - begin - match Specs.get_summary resolved_pname with + let exec_one_pname pname = + if !Config.ondemand_enabled then + Ondemand.do_analysis pdesc pname; + let exec_skip_call ret_type = + skip_call norm_prop path pname loc ret_ids (Some ret_type) url_handled_args in + match Specs.get_summary pname with | None -> - let ret_typ_str = Procname.java_get_return_type resolved_pname in + let ret_typ_str = Procname.java_get_return_type pname in let ret_typ = match lookup_java_typ_from_string tenv ret_typ_str with | Sil.Tstruct _ as typ -> Sil.Tptr (typ, Sil.Pk_pointer) | typ -> typ in exec_skip_call ret_typ - | Some summary when call_should_be_skipped resolved_pname summary -> + | Some summary when call_should_be_skipped pname summary -> exec_skip_call summary.Specs.attributes.ProcAttributes.ret_type | Some summary -> - sym_exec_call cfg pdesc tenv norm_prop path ret_ids url_handled_args summary loc - end + sym_exec_call cfg pdesc tenv norm_prop path ret_ids url_handled_args summary loc in + IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) -> (** Generic fun call with known name *) let (prop_r, _n_actual_params) = normalize_params pname _prop actual_params in let fn, n_actual_params = handle_special_cases_call tenv cfg callee_pname _n_actual_params in let resolved_pname = - resolve_virtual_pname cfg tenv prop_r n_actual_params fn call_flags in + match resolve_virtual_pname cfg tenv prop_r n_actual_params fn call_flags with + | resolved_pname :: _ -> resolved_pname + | [] -> fn in if !Config.ondemand_enabled then Ondemand.do_analysis pdesc resolved_pname; let callee_pdesc_opt = Cfg.Procdesc.find_from_name cfg resolved_pname in