diff --git a/infer/lib/python/inferlib/analyze.py b/infer/lib/python/inferlib/analyze.py index b8c647c4e..de4886aa3 100644 --- a/infer/lib/python/inferlib/analyze.py +++ b/infer/lib/python/inferlib/analyze.py @@ -332,6 +332,9 @@ class AnalyzerWrapper(object): javac_original_arguments = \ self.javac.original_arguments if self.javac is not None else [] + if self.args.analyzer == config.ANALYZER_TRACING: + os.environ['INFER_LAZY_DYNAMIC_DISPATCH'] = 'Y' + if self.args.multicore == 1: analysis_start_time = time.time() analyze_cmd = infer_analyze + infer_options diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index fd93e8bd2..59698193a 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -179,11 +179,17 @@ module Node = struct let get_succs node = node.nd_succs type node = t + module NodeSet = Set.Make(struct type t = node let compare = compare end) + module NodeMap = Map.Make(struct + type t = node + let compare = compare + end) + let get_sliced_succs node f = let visited = ref NodeSet.empty in let rec slice_nodes nodes : NodeSet.t = @@ -586,15 +592,117 @@ module Node = struct let fold_node acc node = IList.fold_left (fun acc instr -> f acc node instr) acc (get_instrs node) in proc_desc_fold_nodes fold_node acc proc_desc + (* (** Set the proc desc of the node *) let node_set_proc_desc pdesc node = node.nd_proc <- Some pdesc + let remove_node cfg node = remove_node' (fun node' -> not (equal node node')) cfg node *) + + (* clone a procedure description and apply the type substitutions where + the parameters are used *) + let proc_desc_specialize_types cfg callee_proc_desc resolved_attributes substitutions = + let resolved_proc_desc = proc_desc_create cfg resolved_attributes in + let resolved_proc_name = proc_desc_get_proc_name resolved_proc_desc + and callee_start_node = proc_desc_get_start_node callee_proc_desc + and callee_exit_node = proc_desc_get_exit_node callee_proc_desc in + let convert_pvar pvar = + Sil.mk_pvar (Sil.pvar_get_name pvar) resolved_proc_name in + let convert_exp = function + | Sil.Lvar origin_pvar -> + Sil.Lvar (convert_pvar origin_pvar) + | exp -> exp in + let extract_class_name = function + | Sil.Tptr (Sil.Tstruct { Sil.struct_name }, _) when struct_name <> None -> + Mangled.to_string (Option.get struct_name) + | _ -> failwith "Expecting classname for Java types" in + let subst_map = ref Ident.IdentMap.empty in + let redirected_class_name origin_id = + try + Some (Ident.IdentMap.find origin_id !subst_map) + with Not_found -> None in + let convert_instr instrs = function + | Sil.Letderef (id, (Sil.Lvar origin_pvar as origin_exp), origin_typ, loc) -> + let (_, specialized_typ) = + let pvar_name = Sil.pvar_get_name origin_pvar in + try + IList.find + (fun (n, _) -> Mangled.equal n pvar_name) + substitutions + with Not_found -> + (pvar_name, origin_typ) in + subst_map := Ident.IdentMap.add id specialized_typ !subst_map; + Sil.Letderef (id, convert_exp origin_exp, specialized_typ, loc) :: instrs + | Sil.Letderef (id, origin_exp, origin_typ, loc) -> + Sil.Letderef (id, convert_exp origin_exp, origin_typ, loc) :: instrs + | Sil.Set (assignee_exp, origin_typ, origin_exp, loc) -> + let set_instr = + Sil.Set (convert_exp assignee_exp, origin_typ, convert_exp origin_exp, loc) in + set_instr :: instrs + | Sil.Call (return_ids, Sil.Const (Sil.Cfun callee_pname), + (Sil.Var id, _) :: origin_args, loc, call_flags) + when call_flags.Sil.cf_virtual && redirected_class_name id <> None -> + let redirected_typ = Option.get (redirected_class_name id) in + let redirected_pname = + Procname.java_replace_class + callee_pname (extract_class_name redirected_typ) + and args = + let other_args = (IList.map (fun (exp, typ) -> (convert_exp exp, typ)) origin_args) in + (Sil.Var id, redirected_typ) :: other_args in + let call_instr = + Sil.Call (return_ids, Sil.Const (Sil.Cfun redirected_pname), args, loc, call_flags) in + call_instr :: instrs + | Sil.Call (return_ids, origin_call_exp, origin_args, loc, call_flags) -> + let converted_args = IList.map (fun (exp, typ) -> (convert_exp exp, typ)) origin_args in + let call_instr = + Sil.Call (return_ids, convert_exp origin_call_exp, converted_args, loc, call_flags) in + call_instr :: instrs + | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) -> + Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind):: instrs + | Sil.Nullify (origin_pvar, loc, deallocate) -> + Sil.Nullify (convert_pvar origin_pvar, loc, deallocate) :: instrs + | Sil.Declare_locals (typed_vars, loc) -> + let new_typed_vars = IList.map (fun (pvar, typ) -> (convert_pvar pvar, typ)) typed_vars in + (Sil.Declare_locals (new_typed_vars, loc)) :: instrs + | instr -> instr :: instrs in + let convert_node_kind = function + | Start_node _ -> Start_node resolved_proc_desc + | Exit_node _ -> Exit_node resolved_proc_desc + | node_kind -> node_kind in + let node_map = ref NodeMap.empty in + let rec convert_node node = + let loc = get_loc node + and kind = convert_node_kind (get_kind node) + and instrs = + IList.fold_left convert_instr [] (get_instrs node) in + create cfg loc kind (IList.rev instrs) resolved_proc_desc (get_temps node) + and loop callee_nodes = + match callee_nodes with + | [] -> [] + | node :: other_node -> + let converted_node = + try + NodeMap.find node !node_map + with Not_found -> + let new_node = convert_node node + and successors = get_succs node + and exn_nodes = get_exn node in + node_map := NodeMap.add node new_node !node_map; + if equal node callee_start_node then + proc_desc_set_start_node resolved_proc_desc new_node; + if equal node callee_exit_node then + proc_desc_set_exit_node resolved_proc_desc new_node; + set_succs_exn new_node (loop successors) (loop exn_nodes); + new_node in + converted_node :: (loop other_node) in + ignore (loop [callee_start_node]); + pdesc_tbl_add cfg resolved_proc_name resolved_proc_desc + end (* =============== END of module Node =============== *) @@ -639,6 +747,7 @@ module Procdesc = struct let set_flag = Node.proc_desc_set_flag let set_start_node = Node.proc_desc_set_start_node let append_locals = Node.proc_desc_append_locals + let specialize_types = Node.proc_desc_specialize_types end (* =============== END of module Procdesc =============== *) @@ -1043,3 +1152,39 @@ let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg : cfg) end; save_attributes cfg; Serialization.to_file cfg_serializer filename cfg + + +(** Creates a copy of a procedure description and a list of type substitutions of the form + (name, typ) where name is a parameter. The resulting procedure CFG is isomorphic but + all the type of the parameters are replaced in the instructions according to the list. + The virtual calls are also replaced to match the parameter types *) +let specialize_types cfg callee_proc_name resolved_proc_name args = + (* TODO (#9333890): This currently only works when the callee is defined in the same file. + Add support to search for the callee procedure description in the execution environment *) + match Procdesc.find_from_name cfg resolved_proc_name with + | Some _ -> () + | None -> + begin + match Procdesc.find_from_name cfg callee_proc_name with + | None -> () + | Some callee_proc_desc -> + let callee_attributes = Procdesc.get_attributes callee_proc_desc in + let resolved_formals = + IList.fold_left2 + (fun accu (name, _) (_, arg_typ) -> (name, arg_typ) :: accu) + [] callee_attributes.ProcAttributes.formals args |> IList.rev in + let resolved_attributes = + { callee_attributes with + ProcAttributes.formals = resolved_formals; + proc_name = resolved_proc_name; + } in + AttributesTable.store_attributes resolved_attributes; + Procdesc.specialize_types cfg callee_proc_desc resolved_attributes resolved_formals; + begin + let source_file = resolved_attributes.ProcAttributes.loc.Location.file in + let source_dir = DB.source_dir_from_source_file source_file in + let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in + let save_sources = false in + store_cfg_to_file cfg_file save_sources cfg + end + end diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index 36391f073..5109fa27e 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -117,6 +117,7 @@ module Procdesc : sig (** append a list of new local variables to the existing list of local variables *) val append_locals : t -> (Mangled.t * Sil.typ) list -> unit + end (** node of the control flow graph *) @@ -314,3 +315,9 @@ val get_block_pdesc : cfg -> Mangled.t -> Procdesc.t option (** Removes seeds variables from a prop corresponding to captured variables in an objc block *) val remove_seed_captured_vars_block : Mangled.t list -> Prop.normal Prop.t -> Prop.normal Prop.t + +(** Creates a copy of a procedure description and a list of type substitutions of the form + (name, typ) where name is a parameter. The resulting procedure CFG is isomorphic but + all the type of the parameters are replaced in the instructions according to the list. + The virtual calls are also replaced to match the parameter types *) +val specialize_types : cfg -> Procname.t -> Procname.t -> (Sil.exp * Sil.typ) list -> unit diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 060c044ab..031e5a823 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -355,6 +355,11 @@ let analyze_models = from_env_variable "INFER_ANALYZE_MODELS" cost *) let sound_dynamic_dispatch = from_env_variable "INFER_SOUND_DYNAMIC_DISPATCH" +(** experimental: handle dynamic dispatch by following the JVM semantics and creating + during the symbolic excution procedure descriptions using the types information + found in the abstract state *) +let lazy_dynamic_dispatch = from_env_variable "INFER_LAZY_DYNAMIC_DISPATCH" + module Experiment = struct (** if true, a precondition with e.g. index 3 in an array does not require the caller to have index 3 too diff --git a/infer/src/backend/ident.ml b/infer/src/backend/ident.ml index 7a3f70ee0..2bdb3bf27 100644 --- a/infer/src/backend/ident.ml +++ b/infer/src/backend/ident.ml @@ -77,6 +77,12 @@ module IdentSet = Set.Make let compare = compare end) +module IdentMap = Map.Make + (struct + type t = _ident + let compare = compare + end) + module IdentHash = Hashtbl.Make(struct type t = _ident diff --git a/infer/src/backend/ident.mli b/infer/src/backend/ident.mli index aa514d2a9..ed4546af2 100644 --- a/infer/src/backend/ident.mli +++ b/infer/src/backend/ident.mli @@ -28,6 +28,9 @@ module IdentSet : Set.S with type elt = t (** Hash table with ident as key. *) module IdentHash : Hashtbl.S with type key = t +(** Map with ident as key. *) +module IdentMap : Map.S with type key = t + (** Set for fieldnames *) module FieldSet : Set.S with type elt = fieldname diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 0f19fcaf7..79fce45f4 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -45,7 +45,7 @@ type callbacks = let callbacks_ref = ref None -let set_callbacks (callbacks : callbacks) = +let set_callbacks (callbacks : callbacks) = callbacks_ref := Some callbacks let unset_callbacks () = diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index c06f873bd..f2cbfddeb 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -668,6 +668,61 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t end | _ -> failwith "A virtual call must have a receiver" + +(** Resolve the name of the procedure to call based on the type of the arguments *) +let resolve_java_pname tenv prop args pname call_flags : Procname.t = + let resolve_from_args pname args = + let parameters = Procname.java_get_parameters pname in + if IList.length args <> IList.length parameters then + pname + else + let resolved_params = + IList.fold_left2 + (fun accu (arg_exp, _) name -> + match resolve_typename prop arg_exp with + | Some class_name -> + (Procname.split_classname (Typename.name class_name)) :: accu + | None -> name :: accu) + [] args (Procname.java_get_parameters pname) |> IList.rev in + Procname.java_replace_parameters pname resolved_params in + let resolved_pname, other_args = + match args with + | [] -> pname, [] + | (first_arg, _) :: other_args when call_flags.Sil.cf_virtual -> + let resolved = + begin + match resolve_typename prop first_arg with + | Some class_name -> resolve_method tenv class_name pname + | None -> pname + end in + resolved, other_args + | _ :: other_args when Procname.is_constructor pname -> + pname, other_args + | args -> + pname, args in + resolve_from_args resolved_pname other_args + + +(** Resolved the procedure name and run the analysis of the resolved procedure + if not already analyzed *) +let resolve_and_analyze + cfg tenv caller_pdesc prop args callee_pname call_flags : Procname.t * Specs.summary option = + let resolved_pname = + (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name + whether the method is defined or generated by the specialization *) + begin + let res_pname = + resolve_java_pname tenv prop args callee_pname call_flags in + if Procname.equal res_pname callee_pname then callee_pname + else + (if not (Specs.summary_exists res_pname) then + Cfg.specialize_types cfg callee_pname res_pname args; + res_pname) + end in + Ondemand.do_analysis ~propagate_exceptions:true caller_pdesc resolved_pname; + resolved_pname, Specs.get_summary resolved_pname + + (** recognize calls to shared_ptr procedures and re-direct them to infer procedures for modelling *) let redirect_shared_ptr tenv cfg pname actual_params = let class_shared_ptr typ = @@ -678,7 +733,7 @@ let redirect_shared_ptr tenv cfg pname actual_params = | _ -> false with exn when exn_not_failure exn -> false in (* We pattern match over some specific library function, *) - (* so we make precise matching to distinghuis between *) + (* so we make precise matching to distinguish between *) (* references and pointers in C++ *) let ptr_to filter = function | Sil.Tptr (t, Sil.Pk_pointer) @@ -1080,6 +1135,29 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path when function_is_builtin callee_pname -> let sym_exe_builtin = Builtin.get_sym_exe_builtin callee_pname in sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args callee_pname loc + + | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) + when !Config.curr_language = Config.Java && Config.lazy_dynamic_dispatch -> + let norm_prop, norm_args = normalize_params pname _prop actual_params in + let exec_skip_call skipped_pname ret_type = + skip_call norm_prop path skipped_pname loc ret_ids (Some ret_type) norm_args in + let resolved_pname, summary_opt = + resolve_and_analyze cfg tenv pdesc norm_prop norm_args callee_pname call_flags in + begin + match summary_opt with + | None -> + 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 resolved_pname ret_typ + | Some summary when call_should_be_skipped resolved_pname summary -> + exec_skip_call resolved_pname summary.Specs.attributes.ProcAttributes.ret_type + | Some summary -> + sym_exec_call cfg pdesc tenv norm_prop path ret_ids norm_args summary loc + end + | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) when !Config.curr_language = Config.Java -> do_error_checks (Paths.Path.curr_node path) instr pname pdesc; diff --git a/infer/tests/codetoanalyze/java/infer/ClassCastExceptions.java b/infer/tests/codetoanalyze/java/infer/ClassCastExceptions.java index 9e7491b88..b03a95f52 100644 --- a/infer/tests/codetoanalyze/java/infer/ClassCastExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/ClassCastExceptions.java @@ -22,6 +22,10 @@ class SubClassA extends SuperClass { class SubClassB extends SuperClass { } +interface MyInterface { + public int getInt(); +} + class ImplementationOfInterface implements MyInterface { public int getInt() { @@ -35,10 +39,6 @@ class AnotherImplementationOfInterface implements MyInterface { } } -interface MyInterface { - public int getInt(); -} - public class ClassCastExceptions { diff --git a/infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java b/infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java new file mode 100644 index 000000000..62e9ceab1 --- /dev/null +++ b/infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java @@ -0,0 +1,39 @@ +/* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package codetoanalyze.java.tracing; + +class A { + + public T get() { + return new T(); + } + +} + +class B extends A { + + public T get() { + return null; + } + +} + +public class LazyDynamicDispatchExample { + + static T foo(A a) { + return a.get(); + } + + static void bar() { + B b = new B(); + foo(b).f(); + } + +} diff --git a/infer/tests/endtoend/java/comparison/ClassCastExceptionTest.java b/infer/tests/endtoend/java/comparison/ClassCastExceptionTest.java index 89299f39a..742ae0c29 100644 --- a/infer/tests/endtoend/java/comparison/ClassCastExceptionTest.java +++ b/infer/tests/endtoend/java/comparison/ClassCastExceptionTest.java @@ -43,6 +43,7 @@ public class ClassCastExceptionTest { String[] methods = { "classCastException", "classCastExceptionImplementsInterface", + "openHttpURLConnection", }; assertThat( "Results should contain " + CLASS_CAST_EXCEPTION, @@ -55,5 +56,4 @@ public class ClassCastExceptionTest { ); } - } diff --git a/infer/tests/endtoend/java/tracing/LazyDynamicDispatchTest.java b/infer/tests/endtoend/java/tracing/LazyDynamicDispatchTest.java new file mode 100644 index 000000000..b5e409e30 --- /dev/null +++ b/infer/tests/endtoend/java/tracing/LazyDynamicDispatchTest.java @@ -0,0 +1,58 @@ +/* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + + +package endtoend.java.tracing; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +import org.junit.BeforeClass; +import org.junit.Test; + +import java.io.IOException; + +import utils.InferException; +import utils.InferResults; + +public class LazyDynamicDispatchTest { + + public static final String SOURCE_FILE = + "infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java"; + + public static final String NPE = + "java.lang.NullPointerException"; + + private static InferResults inferResults; + + @BeforeClass + public static void loadResults() throws InterruptedException, IOException { + inferResults = InferResults.loadTracingResults( + LazyDynamicDispatchTest.class, + SOURCE_FILE); + } + + @Test + public void matchErrors() + throws IOException, InterruptedException, InferException { + String[] methods = { + "bar" + }; + assertThat( + "Results should contain " + NPE, + inferResults, + containsExactly( + NPE, + SOURCE_FILE, + methods + ) + ); + } + +} diff --git a/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java b/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java index fc96224ee..c30b98eaf 100644 --- a/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java @@ -34,7 +34,7 @@ public class NullPointerExceptionTest { @BeforeClass public static void loadResults() throws InterruptedException, IOException { inferResults = InferResults.loadTracingResults( - ArrayIndexOutOfBoundsExceptionTest.class, + NullPointerExceptionTest.class, SOURCE_FILE); }