From 86304b3d9c9e3b6b9b8930c4aa290f5c847dea6c Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Wed, 16 Mar 2016 12:01:02 -0700 Subject: [PATCH] Prevent assert false from occurring on Java functions in Procname. Summary:public Assert false have been observed in Procname when analyzing some C projects. This diff changes the Procname API to make it safe for Java: the java functions in the module don't assert false now. This takes care of the errors observed in C projects. The new API forces changes throughout the codebase. In particular, the constant propagation module was making assumptions that it would only be executed on Java code, triggering assert false on C. Now it is safe. For the remaining functions in the Procname module, those for other languages, a special assert false in Utils is used to print stack traces. This is for future debugging. Reviewed By: sblackshear Differential Revision: D3054077 fb-gh-sync-id: a77f1d7 shipit-source-id: a77f1d7 --- infer/src/backend/callbacks.ml | 8 +- infer/src/backend/inferconfig.ml | 116 +++++---- infer/src/backend/interproc.ml | 10 +- infer/src/backend/localise.ml | 18 +- infer/src/backend/localise.mli | 3 +- infer/src/backend/preanal.ml | 25 +- infer/src/backend/procname.ml | 241 ++++++++++-------- infer/src/backend/procname.mli | 35 ++- infer/src/backend/sil.ml | 7 +- infer/src/backend/symExec.ml | 111 ++++---- infer/src/backend/taint.ml | 13 +- infer/src/backend/utils.ml | 6 + infer/src/backend/utils.mli | 3 + infer/src/checkers/callbackChecker.ml | 17 +- infer/src/checkers/checkTraceCallSequence.ml | 25 +- infer/src/checkers/checkers.ml | 101 ++++++-- infer/src/checkers/constantPropagation.ml | 23 +- .../checkers/fragmentRetainsViewChecker.ml | 18 +- infer/src/checkers/patternMatch.ml | 62 +++-- infer/src/checkers/patternMatch.mli | 9 +- infer/src/checkers/performanceCritical.ml | 32 ++- infer/src/checkers/sqlChecker.ml | 51 ++-- infer/src/eradicate/eradicate.ml | 18 +- infer/src/eradicate/eradicateChecks.ml | 4 +- infer/src/eradicate/typeCheck.ml | 15 +- infer/src/eradicate/typeErr.ml | 58 +++-- infer/src/harness/androidFramework.ml | 57 +++-- infer/src/harness/androidFramework.mli | 7 +- infer/src/harness/harness.ml | 25 +- infer/src/harness/inhabit.ml | 20 +- infer/src/harness/inhabit.mli | 2 +- infer/src/java/jAnnotation.ml | 4 +- infer/src/java/jAnnotation.mli | 2 +- infer/src/java/jContext.mli | 2 +- infer/src/java/jTrans.ml | 42 +-- infer/src/java/jTransType.ml | 4 +- infer/src/java/jTransType.mli | 6 +- 37 files changed, 748 insertions(+), 452 deletions(-) diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index ccff7cefe..40bbf95d2 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -140,9 +140,11 @@ let iterate_callbacks store_summary call_graph exe_env = let saved_language = !Config.curr_language in let cluster_id proc_name = - match get_language proc_name with - | Config.Java -> Procname.java_get_class proc_name - | _ -> "unknown" in + match proc_name with + | Procname.Java pname_java -> + Procname.java_get_class pname_java + | _ -> + "unknown" in let cluster proc_names = let cluster_map = IList.fold_left diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml index 6aba8ed27..a50d7e450 100644 --- a/infer/src/backend/inferconfig.ml +++ b/infer/src/backend/inferconfig.ml @@ -57,22 +57,22 @@ let is_matching patterns = type method_pattern = { - class_name : string; - method_name : string option; - parameters : (string list) option - } + class_name : string; + method_name : string option; + parameters : (string list) option +} - let default_method_pattern = { - class_name = ""; - method_name = None; - parameters = None - } +let default_method_pattern = { + class_name = ""; + method_name = None; + parameters = None +} - let default_source_contains = "" +let default_source_contains = "" - type pattern = - | Method_pattern of Config.language * method_pattern - | Source_contains of Config.language * string +type pattern = + | Method_pattern of Config.language * method_pattern + | Source_contains of Config.language * string let language_of_string json_key = function | "Java" -> Config.Java @@ -85,8 +85,8 @@ let detect_language json_key assoc = ("No language found for " ^ json_key ^ " in " ^ Config.inferconfig_file) | (key, `String s) :: _ when key = "language" -> language_of_string json_key s - | _:: tl -> loop tl in - loop assoc + | _:: tl -> loop tl in + loop assoc (* Detect the kind of pattern, method pattern or pattern based on the content of the source file. Detecting the kind of patterns in a first step makes it easier to parse the parts of the @@ -98,49 +98,49 @@ let detect_pattern json_key assoc = let rec loop = function | [] -> failwith ("Unknown pattern for " ^ json_key ^ " in " ^ Config.inferconfig_file) - | (key, _) :: _ when is_method_pattern key -> - Method_pattern (language, default_method_pattern) - | (key, _) :: _ when is_source_contains key -> - Source_contains (language, default_source_contains) - | _:: tl -> loop tl in - loop assoc + | (key, _) :: _ when is_method_pattern key -> + Method_pattern (language, default_method_pattern) + | (key, _) :: _ when is_source_contains key -> + Source_contains (language, default_source_contains) + | _:: tl -> loop tl in + loop assoc (* Translate a JSON entry into a matching pattern *) let create_pattern json_key (assoc : (string * Yojson.Basic.json) list) = - let collect_params l = - let collect accu = function - | `String s -> s:: accu - | _ -> failwith ("Unrecognised parameters in " ^ Yojson.Basic.to_string (`Assoc assoc)) in - IList.rev (IList.fold_left collect [] l) in - let create_method_pattern assoc = - let loop mp = function - | (key, `String s) when key = "class" -> - { mp with class_name = s } - | (key, `String s) when key = "method" -> - { mp with method_name = Some s } - | (key, `List l) when key = "parameters" -> - { mp with parameters = Some (collect_params l) } - | (key, _) when key = "language" -> mp - | _ -> failwith ("Fails to parse " ^ Yojson.Basic.to_string (`Assoc assoc)) in - IList.fold_left loop default_method_pattern assoc - and create_string_contains assoc = - let loop sc = function + let collect_params l = + let collect accu = function + | `String s -> s:: accu + | _ -> failwith ("Unrecognised parameters in " ^ Yojson.Basic.to_string (`Assoc assoc)) in + IList.rev (IList.fold_left collect [] l) in + let create_method_pattern assoc = + let loop mp = function + | (key, `String s) when key = "class" -> + { mp with class_name = s } + | (key, `String s) when key = "method" -> + { mp with method_name = Some s } + | (key, `List l) when key = "parameters" -> + { mp with parameters = Some (collect_params l) } + | (key, _) when key = "language" -> mp + | _ -> failwith ("Fails to parse " ^ Yojson.Basic.to_string (`Assoc assoc)) in + IList.fold_left loop default_method_pattern assoc + and create_string_contains assoc = + let loop sc = function | (key, `String pattern) when key = "source_contains" -> pattern | (key, _) when key = "language" -> sc | _ -> failwith ("Fails to parse " ^ Yojson.Basic.to_string (`Assoc assoc)) in IList.fold_left loop default_source_contains assoc in match detect_pattern json_key assoc with - | Method_pattern (language, _) -> - Method_pattern (language, create_method_pattern assoc) - | Source_contains (language, _) -> - Source_contains (language, create_string_contains assoc) + | Method_pattern (language, _) -> + Method_pattern (language, create_method_pattern assoc) + | Source_contains (language, _) -> + Source_contains (language, create_string_contains assoc) (* Translate all the JSON entries into matching patterns *) let rec translate json_key accu (json : Yojson.Basic.json) : pattern list = match json with | `Assoc l -> (create_pattern json_key l):: accu | `List l -> IList.fold_left (translate json_key) accu l - | _ -> assert false + | _ -> assert false (* Creates a list of matching patterns for the given inferconfig file *) let load_patterns json_key inferconfig = @@ -154,12 +154,13 @@ let load_patterns json_key inferconfig = (* Check if a proc name is matching the name given as string *) let match_method language proc_name method_name = not (SymExec.function_is_builtin proc_name) && - match language with - | Config.Java -> - Procname.java_get_method proc_name = method_name - | Config.C_CPP -> - Procname.c_get_method proc_name = method_name - + match proc_name with + | Procname.Java pname_java -> + Procname.java_get_method pname_java = method_name + | _ -> + if language = Config.C_CPP + then Procname.c_get_method proc_name = method_name + else false (* Module to create matcher based on strings present in the source file *) module FileContainsStringMatcher = struct @@ -229,9 +230,9 @@ struct StringMap.add pattern.class_name (pattern:: previous) map) StringMap.empty m_patterns in - fun _ proc_name -> - let class_name = Procname.java_get_class proc_name - and method_name = Procname.java_get_method proc_name in + let do_java pname_java = + let class_name = Procname.java_get_class pname_java + and method_name = Procname.java_get_method pname_java in try let class_patterns = StringMap.find class_name pattern_map in IList.exists @@ -240,7 +241,14 @@ struct | None -> true | Some m -> string_equal m method_name) class_patterns - with Not_found -> false + with Not_found -> false in + + fun _ proc_name -> + match proc_name with + | Procname.Java pname_java -> + do_java pname_java + | _ -> + false let create_file_matcher patterns = let s_patterns, m_patterns = diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 3f076e9ed..10dccb974 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1138,9 +1138,13 @@ let report_runtime_exceptions tenv pdesc summary = (Specs.get_attributes summary).ProcAttributes.access = Sil.Public in let is_main = is_public_method - && Procname.is_java pname - && Procname.java_is_static pname - && (Procname.java_get_method pname) = "main" in + && + (match pname with + | Procname.Java pname_java -> + Procname.java_is_static pname + && (Procname.java_get_method pname_java) = "main" + | _ -> + false) in let is_annotated = let proc_attributes = Specs.pdesc_resolve_attributes pdesc in let annotated_signature = Annotations.get_annotated_signature proc_attributes in diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 37b359289..64c265aed 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -250,10 +250,12 @@ let format_field f = then Ident.java_fieldname_get_field f else Ident.fieldname_to_string f -let format_method m = - if !Config.curr_language = Config.Java - then Procname.java_get_method m - else Procname.to_string m +let format_method pname = + match pname with + | Procname.Java pname_java -> + Procname.java_get_method pname_java + | _ -> + Procname.to_string pname let mem_dyn_allocated = "memory dynamically allocated" let lock_acquired = "lock acquired" @@ -412,7 +414,13 @@ let desc_context_leak pname context_typ fieldname leak_path : error_desc = else (IList.fold_left leak_path_entry_to_str "" leak_path) ^ " Leaked " in path_prefix ^ context_str in let preamble = - let pname_str = Procname.java_get_class pname ^ "." ^ Procname.java_get_method pname in + let pname_str = match pname with + | Procname.Java pname_java -> + Printf.sprintf "%s.%s" + (Procname.java_get_class pname_java) + (Procname.java_get_method pname_java) + | _ -> + "" in "Context " ^ context_str ^ "may leak during method " ^ pname_str ^ ":\n" in { no_desc with descriptions = [preamble; leak_root; path_str] } diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index 224690479..9338d3c9f 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -206,7 +206,8 @@ val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc val java_unchecked_exn_desc : Procname.t -> Typename.t -> string -> error_desc val desc_context_leak : - Procname.t -> Sil.typ -> Ident.fieldname -> (Ident.fieldname option * Sil.typ) list -> error_desc + Procname.t -> Sil.typ -> Ident.fieldname -> + (Ident.fieldname option * Sil.typ) list -> error_desc val desc_fragment_retains_view : Sil.typ -> Ident.fieldname -> Sil.typ -> Procname.t -> error_desc diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 93da4c117..e80ea74b5 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -358,17 +358,20 @@ let add_dispatch_calls cfg cg tenv f_translate_typ_opt = let pname_translate_types pname = match f_translate_typ_opt with | Some f_translate_typ -> - if Procname.is_java pname then - let param_type_strs = - IList.map Procname.java_type_to_string (Procname.java_get_parameters pname) in - let receiver_type_str = Procname.java_get_class pname in - let return_type_str = Procname.java_get_return_type pname in - IList.iter - (fun typ_str -> f_translate_typ tenv typ_str) - (return_type_str :: (receiver_type_str :: param_type_strs)) - else - (* TODO: support this for C/CPP/Obj-C *) - () + (match pname with + | Procname.Java pname_java -> + let param_type_strs = + IList.map Procname.java_type_to_string (Procname.java_get_parameters pname) in + let receiver_type_str = Procname.java_get_class pname_java in + let return_type_str = Procname.java_get_return_type pname_java in + IList.iter + (fun typ_str -> f_translate_typ tenv typ_str) + (return_type_str :: (receiver_type_str :: param_type_strs)) + | Procname.C _ + | Procname.ObjC_Cpp _ + | Procname.Block _ -> + (* TODO: support this for C/CPP/Obj-C *) + ()) | None -> () in let node_add_dispatch_calls caller_pname node = (* TODO: handle dynamic dispatch for virtual calls as well *) diff --git a/infer/src/backend/procname.ml b/infer/src/backend/procname.ml index 77ccddbbf..00ced2df4 100644 --- a/infer/src/backend/procname.ml +++ b/infer/src/backend/procname.ml @@ -19,8 +19,8 @@ type method_kind = | Static (* in Java, procedures called with invokestatic *) | Non_Static (* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface *) -(* java_signature extends base_signature with a classname and a package *) -type java_signature = { +(* java procedure name *) +type java = { class_name: java_type; return_type: java_type option; (* option because constructors have no return type *) method_name: string; @@ -42,22 +42,26 @@ let objc_method_kind_of_bool is_instance = else Class_objc_method (* C++/ObjC method signature *) -type c_method_signature = { +type objc_cpp_method = { class_name: string; method_name: string; mangled: string option; } +type block = string + +type c_function = string * (string option) + type t = - | Java_method of java_signature + | Java of java (* a pair (plain, mangled optional) for standard C function *) - | C_function of string * (string option) + | C of c_function (* structure with class name and method name for methods in Objective C and C++ *) - | ObjC_Cpp_method of c_method_signature + | ObjC_Cpp of objc_cpp_method - | ObjC_block of string + | Block of block (* Defines the level of verbosity of some to_string functions *) type detail_level = @@ -66,7 +70,7 @@ type detail_level = | Simple -let empty = ObjC_block "" +let empty = Block "" let is_verbose v = @@ -132,13 +136,13 @@ let java_return_type_compare jr1 jr2 = | Some _, None -> 1 | Some jt1 , Some jt2 -> java_type_compare jt1 jt2 -(** Compare java signatures. *) -let java_sig_compare (js1: java_signature) (js2 : java_signature) = - string_compare js1.method_name js2.method_name - |> next java_type_list_compare js1.parameters js2.parameters - |> next java_type_compare js1.class_name js2.class_name - |> next java_return_type_compare js1.return_type js2.return_type - |> next method_kind_compare js1.kind js2.kind +(** Compare java procedure names. *) +let java_compare (j1: java) (j2 : java) = + string_compare j1.method_name j2.method_name + |> next java_type_list_compare j1.parameters j2.parameters + |> next java_type_compare j1.class_name j2.class_name + |> next java_return_type_compare j1.return_type j2.return_type + |> next method_kind_compare j1.kind j2.kind let c_function_mangled_compare mangled1 mangled2 = match mangled1, mangled2 with @@ -159,23 +163,22 @@ let c_meth_sig_compare osig1 osig2 = let split_classname package_classname = string_split_character package_classname '.' -let from_string_c_fun (s: string) = C_function (s, None) +let from_string_c_fun (s: string) = C (s, None) -let mangled_c_fun (plain: string) (mangled: string) = C_function (plain, Some mangled) +let mangled_c_fun (plain: string) (mangled: string) = C (plain, Some mangled) -(** Creates a java procname, given classname, return type, method name and its parameters *) -let mangled_java class_name ret_type method_name params _kind = - Java_method { - class_name = class_name; - return_type = ret_type; - method_name = method_name; - parameters = params; - kind = _kind +let java class_name return_type method_name parameters kind = + { + class_name; + return_type; + method_name; + parameters; + kind; } (** Create an objc procedure name from a class_name and method_name. *) let mangled_c_method class_name method_name mangled = - ObjC_Cpp_method { + ObjC_Cpp { class_name = class_name; method_name = method_name; mangled = mangled; @@ -183,99 +186,115 @@ let mangled_c_method class_name method_name mangled = (** Create an objc procedure name from a class_name and method_name. *) let mangled_objc_block name = - ObjC_block name + Block name let is_java = function - | Java_method _ -> true + | Java _ -> true | _ -> false let is_c_method = function - | ObjC_Cpp_method _ -> true + | ObjC_Cpp _ -> true | _ -> false (** Replace package and classname of a java procname. *) let java_replace_class p package_classname = match p with - | Java_method j -> Java_method { j with class_name = (split_classname package_classname) } - | _ -> assert false + | Java j -> + Java { j with class_name = (split_classname package_classname) } + | _ -> + Utils.assert_false __POS__ (** Replace the class name of an objc procedure name. *) let c_method_replace_class t class_name = match t with - | ObjC_Cpp_method osig -> ObjC_Cpp_method { osig with class_name = class_name } - | _ -> assert false + | ObjC_Cpp osig -> + ObjC_Cpp { osig with class_name = class_name } + | _ -> + Utils.assert_false __POS__ (** Get the class name of a Objective-C/C++ procedure name. *) let c_get_class t = match t with - | ObjC_Cpp_method osig -> osig.class_name - | _ -> assert false + | ObjC_Cpp osig -> + osig.class_name + | _ -> + Utils.assert_false __POS__ (** Return the package.classname of a java procname. *) -let java_get_class = function - | Java_method j -> java_type_to_string j.class_name - | _ -> assert false +let java_get_class (j : java) = + java_type_to_string j.class_name (** Return the class name of a java procedure name. *) -let java_get_simple_class = function - | Java_method j -> snd j.class_name - | _ -> assert false +let java_get_simple_class (j : java) = + snd j.class_name (** Return the package of a java procname. *) -let java_get_package = function - | Java_method j -> fst j.class_name - | _ -> assert false +let java_get_package (j : java) = + fst j.class_name (** Return the method of a java procname. *) -let java_get_method = function - | Java_method j -> j.method_name - | _ -> assert false +let java_get_method (j : java) = + j.method_name (** Replace the method of a java procname. *) let java_replace_method j mname = match j with - | Java_method j -> Java_method { j with method_name = mname } - | _ -> assert false + | Java j -> + Java { j with method_name = mname } + | _ -> + Utils.assert_false __POS__ (** Replace the return type of a java procname. *) let java_replace_return_type p ret_type = match p with - | Java_method j -> Java_method { j with return_type = Some ret_type } - | _ -> assert false + | Java j -> + Java { j with return_type = Some ret_type } + | _ -> + Utils.assert_false __POS__ (** Replace the parameters of a java procname. *) let java_replace_parameters p parameters = match p with - | Java_method j -> Java_method { j with parameters } - | _ -> assert false + | Java j -> + Java { j with parameters } + | _ -> + Utils.assert_false __POS__ (** Return the method of a objc/c++ procname. *) let c_get_method = function - | ObjC_Cpp_method name -> name.method_name - | C_function (name, _) -> name - | ObjC_block name -> name - | _ -> assert false + | ObjC_Cpp name -> + name.method_name + | C (name, _) -> + name + | Block name -> + name + | _ -> + Utils.assert_false __POS__ (** Return the return type of a java procname. *) -let java_get_return_type = function - | Java_method j -> java_return_type_to_string j Verbose - | _ -> assert false +let java_get_return_type (j : java) = + java_return_type_to_string j Verbose (** Return the parameters of a java procname. *) let java_get_parameters = function - | Java_method j -> j.parameters - | _ -> assert false + | Java j -> + j.parameters + | _ -> + Utils.assert_false __POS__ (** Return the parameters of a java procname as strings. *) let java_get_parameters_as_strings = function - | Java_method j -> + | Java j -> IList.map (fun param -> java_type_to_string param) j.parameters - | _ -> assert false + | _ -> + Utils.assert_false __POS__ (** Return true if the java procedure is static *) let java_is_static = function - | Java_method j -> j.kind = Static - | _ -> assert false + | Java j -> + j.kind = Static + | _ -> + Utils.assert_false __POS__ (** Prints a string of a java procname with the given level of verbosity *) -let java_to_string ?(withclass = false) (j : java_signature) verbosity = +let java_to_string ?(withclass = false) (j : java) verbosity = match verbosity with | Verbose | Non_verbose -> (* if verbose, then package.class.method(params): rtype, @@ -303,7 +322,7 @@ let java_to_string ?(withclass = false) (j : java_signature) verbosity = | _ -> "..." in let method_name = if j.method_name = "" then - java_get_simple_class (Java_method j) + java_get_simple_class j else cls_prefix ^ j.method_name in method_name ^ "(" ^ params ^ ")" @@ -319,25 +338,25 @@ let is_anonymous_inner_class_name class_name = (** Check if the procedure belongs to an anonymous inner class. *) let java_is_anonymous_inner_class = function - | Java_method j -> is_anonymous_inner_class_name (snd j.class_name) + | Java j -> is_anonymous_inner_class_name (snd j.class_name) | _ -> false (** Check if the last parameter is a hidden inner class, and remove it if present. This is used in private constructors, where a proxy constructor is generated with an extra parameter and calls the normal constructor. *) let java_remove_hidden_inner_class_parameter = function - | Java_method js -> + | Java js -> (match IList.rev js.parameters with | (_, s) :: par' -> if is_anonymous_inner_class_name s - then Some (Java_method { js with parameters = IList.rev par'}) + then Some (Java { js with parameters = IList.rev par'}) else None | [] -> None) | _ -> None (** Check if the procedure name is an anonymous inner class constructor. *) let java_is_anonymous_inner_class_constructor = function - | Java_method js -> + | Java js -> let _, name = js.class_name in is_anonymous_inner_class_name name | _ -> false @@ -345,7 +364,7 @@ let java_is_anonymous_inner_class_constructor = function (** Check if the procedure name is an acess method (e.g. access$100 used to access private members from a nested class. *) let java_is_access_method = function - | Java_method js -> + | Java js -> (match string_split_character js.method_name '$' with | Some "access", s -> let is_int = @@ -357,7 +376,7 @@ let java_is_access_method = function (** Check if the proc name has the type of a java vararg. Note: currently only checks that the last argument has type Object[]. *) let java_is_vararg = function - | Java_method js -> + | Java js -> begin match (IList.rev js.parameters) with | (_,"java.lang.Object[]") :: _ -> true @@ -367,31 +386,31 @@ let java_is_vararg = function (** [is_constructor pname] returns true if [pname] is a constructor *) let is_constructor = function - | Java_method js -> js.method_name = "" - | ObjC_Cpp_method name -> + | Java js -> js.method_name = "" + | ObjC_Cpp name -> (name.method_name = "new") || string_is_prefix "init" name.method_name | _ -> false (** [is_objc_dealloc pname] returns true if [pname] is the dealloc method in Objective-C *) let is_objc_dealloc = function - | ObjC_Cpp_method name -> name.method_name = "dealloc" + | ObjC_Cpp name -> name.method_name = "dealloc" | _ -> false let java_is_close = function - | Java_method js -> js.method_name = "close" + | Java js -> js.method_name = "close" | _ -> false (** [is_class_initializer pname] returns true if [pname] is a class initializer *) let is_class_initializer = function - | Java_method js -> js.method_name = "" + | Java js -> js.method_name = "" | _ -> false (** [is_infer_undefined pn] returns true if [pn] is a special Infer undefined proc *) let is_infer_undefined pn = match pn with - | Java_method _ -> + | Java j -> let regexp = Str.regexp "com.facebook.infer.models.InferUndefined" in - Str.string_match regexp (java_get_class pn) 0 + Str.string_match regexp (java_get_class j) 0 | _ -> (* TODO: add cases for obj-c, c, c++ *) false @@ -419,28 +438,31 @@ let c_method_to_string osig detail_level = (** Very verbose representation of an existing Procname.t *) let to_unique_id pn = match pn with - | Java_method j -> java_to_string j Verbose - | C_function (c1, c2) -> to_readable_string (c1, c2) true - | ObjC_Cpp_method osig -> c_method_to_string osig Verbose - | ObjC_block name -> name + | Java j -> java_to_string j Verbose + | C (c1, c2) -> to_readable_string (c1, c2) true + | ObjC_Cpp osig -> c_method_to_string osig Verbose + | Block name -> name (** Convert a proc name to a string for the user to see *) let to_string p = match p with - | Java_method j -> (java_to_string j Non_verbose) - | C_function (c1, c2) -> + | Java j -> (java_to_string j Non_verbose) + | C (c1, c2) -> to_readable_string (c1, c2) false - | ObjC_Cpp_method osig -> c_method_to_string osig Non_verbose - | ObjC_block name -> name + | ObjC_Cpp osig -> c_method_to_string osig Non_verbose + | Block name -> name (** Convenient representation of a procname for external tools (e.g. eclipse plugin) *) let to_simplified_string ?(withclass = false) p = match p with - | Java_method j -> (java_to_string ~withclass j Simple) - | C_function (c1, c2) -> + | Java j -> + (java_to_string ~withclass j Simple) + | C (c1, c2) -> to_readable_string (c1, c2) false ^ "()" - | ObjC_Cpp_method osig -> c_method_to_string osig Simple - | ObjC_block _ -> "block" + | ObjC_Cpp osig -> + c_method_to_string osig Simple + | Block _ -> + "block" (** Convert a proc name to a filename *) let to_filename (pn : proc_name) = @@ -450,22 +472,31 @@ let to_filename (pn : proc_name) = let pp f pn = F.fprintf f "%s" (to_string pn) -(** Compare function for Procname.t types *) -(* These rules create an ordered set of procnames grouped with the following priority (lowest to highest): *) +(** Compare function for Procname.t types. + These rules create an ordered set of procnames grouped with the following + priority (lowest to highest): *) let compare pn1 pn2 = match pn1, pn2 with - | Java_method j1, Java_method j2 -> java_sig_compare j1 j2 - | Java_method _, _ -> -1 - | _, Java_method _ -> 1 - | C_function (c1, c2), C_function (c3, c4) -> (* Compare C_function types *) + | Java j1, Java j2 -> + java_compare j1 j2 + | Java _, _ -> + -1 + | _, Java _ -> + 1 + | C (c1, c2), C (c3, c4) -> (* Compare C_function types *) string_compare c1 c3 |> next mangled_compare c2 c4 - | C_function _, _ -> -1 - | _, C_function _ -> 1 - | ObjC_block s1, ObjC_block s2 -> (* Compare ObjC_block types *) + | C _, _ -> + -1 + | _, C _ -> + 1 + | Block s1, Block s2 -> (* Compare ObjC_block types *) string_compare s1 s2 - | ObjC_block _, _ -> -1 - | _, ObjC_block _ -> 1 - | ObjC_Cpp_method osig1, ObjC_Cpp_method osig2 -> c_meth_sig_compare osig1 osig2 + | Block _, _ -> + -1 + | _, Block _ -> + 1 + | ObjC_Cpp osig1, ObjC_Cpp osig2 -> + c_meth_sig_compare osig1 osig2 let equal pn1 pn2 = compare pn1 pn2 = 0 diff --git a/infer/src/backend/procname.mli b/infer/src/backend/procname.mli index 8c5f2c176..e94419368 100644 --- a/infer/src/backend/procname.mli +++ b/infer/src/backend/procname.mli @@ -10,8 +10,24 @@ (** Module for Procedure Names *) +(** Type of java procedure names *) +type java + +(** Type of C function names *) +type c_function + +(** Type of Objective C and C++ method names *) +type objc_cpp_method + +(** Type of Objective C block names *) +type block + (** Type of procedure names *) -type t +type t = + | Java of java + | C of c_function + | ObjC_Cpp of objc_cpp_method + | Block of block type java_type = string option * string @@ -40,12 +56,13 @@ val equal : t -> t -> bool (** Convert a string to a proc name *) val from_string_c_fun : string -> t +(** Create a Java procedure name from its + class_name method_name args_type_name return_type_name method_kind *) +val java : java_type -> java_type option -> string -> java_type list -> method_kind -> java + (** Create a C++ procedure name from plain and mangled name *) val mangled_c_fun : string -> string -> t -(** Create a Java procedure name from its class_name method_name args_type_name return_type_name method_kind *) -val mangled_java : java_type -> java_type option -> string -> java_type list -> method_kind -> t - (** Create an objc procedure name from a class_name and method_name. *) val mangled_c_method : string -> string -> string option -> t @@ -74,16 +91,16 @@ val c_method_replace_class : t -> string -> t val c_get_class : t -> string (** Return the class name of a java procedure name. *) -val java_get_class : t -> string +val java_get_class : java -> string (** Return the simple class name of a java procedure name. *) -val java_get_simple_class : t -> string +val java_get_simple_class : java -> string (** Return the package name of a java procedure name. *) -val java_get_package : t -> string option +val java_get_package : java -> string option (** Return the method name of a java procedure name. *) -val java_get_method : t -> string +val java_get_method : java -> string (** Return the method of a objc/c++ procname. *) val c_get_method : t -> string @@ -92,7 +109,7 @@ val c_get_method : t -> string val java_replace_method : t -> string -> t (** Return the return type of a java procedure name. *) -val java_get_return_type : t -> string +val java_get_return_type : java -> string (** Return the parameters of a java procedure name. *) val java_get_parameters : t -> java_type list diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index b01332920..a32898602 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -1878,7 +1878,12 @@ let rec dexp_to_string = function else (pp_comma_seq) pp_arg fmt des in let pp_fun fmt = function | Dconst (Cfun pname) -> - let s = (if Procname.is_java pname then Procname.java_get_method else Procname.to_string) pname in + let s = + match pname with + | Procname.Java pname_java -> + Procname.java_get_method pname_java + | _ -> + Procname.to_string pname in F.fprintf fmt "%s" s | de -> F.fprintf fmt "%s" (dexp_to_string de) in let receiver, args' = match args with diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index cfface97b..1b2ff89e4 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -616,12 +616,14 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t | 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 + match pname with + | Procname.Java pname_java -> + (try + let receiver_typ_str = Procname.java_get_class pname_java in + Sil.Tptr (lookup_java_typ_from_string tenv receiver_typ_str, Sil.Pk_pointer) + with Cannot_convert_string_to_typ _ -> fallback_typ) + | _ -> + fallback_typ in let receiver_types_equal pname actual_receiver_typ = (* the type of the receiver according to the function signature *) let formal_receiver_typ = get_receiver_typ pname actual_receiver_typ in @@ -740,8 +742,11 @@ let resolve_and_analyze (** recognize calls to the constructor java.net.URL and splits the argument string to be only the protocol. *) let call_constructor_url_update_args pname actual_params = - let url_pname = Procname.mangled_java - ((Some "java.net"), "URL") None "" [(Some "java.lang"), "String"] Procname.Non_Static in + let url_pname = + Procname.Java + (Procname.java + ((Some "java.net"), "URL") None "" + [(Some "java.lang"), "String"] Procname.Non_Static) in if (Procname.equal url_pname pname) then (match actual_params with | [this; (Sil.Const (Sil.Cstr s), atype)] -> @@ -975,28 +980,28 @@ let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp else [prop_] (** Execute [instr] with a symbolic heap [prop].*) -let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path +let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path : (Prop.normal Prop.t * Paths.Path.t) list = - let pname = Cfg.Procdesc.get_proc_name pdesc in + let current_pname = Cfg.Procdesc.get_proc_name current_pdesc in State.set_instr _instr; (* mark instruction last seen *) - State.set_prop_tenv_pdesc prop_ tenv pdesc; (* mark prop,tenv,pdesc last seen *) + State.set_prop_tenv_pdesc prop_ tenv current_pdesc; (* mark prop,tenv,pdesc last seen *) SymOp.pay(); (* pay one symop *) let ret_old_path pl = (* return the old path unchanged *) IList.map (fun p -> (p, path)) pl in let skip_call prop path callee_pname loc ret_ids ret_typ_opt actual_args = let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in - Reporting.log_info pname exn; + Reporting.log_info current_pname exn; L.d_strln ("Undefined function " ^ Procname.to_string callee_pname ^ ", returning undefined value."); - (match Specs.get_summary pname with + (match Specs.get_summary current_pname with | None -> () | Some summary -> Specs.CallStats.trace summary.Specs.stats.Specs.call_stats callee_pname loc (Specs.CallStats.CR_skip) !Config.footprint); call_unknown_or_scan - tenv false pdesc prop path ret_ids ret_typ_opt actual_args callee_pname loc in + tenv false current_pdesc prop path ret_ids ret_typ_opt actual_args callee_pname loc in let instr = match _instr with | Sil.Call (ret, exp, par, loc, call_flags) -> let exp' = Prop.exp_normalize_prop prop_ exp in @@ -1011,10 +1016,10 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path | _ -> _instr in match instr with | Sil.Letderef (id, rhs_exp, typ, loc) -> - execute_letderef pname pdesc tenv id rhs_exp typ loc prop_ + execute_letderef current_pname current_pdesc tenv id rhs_exp typ loc prop_ |> ret_old_path | Sil.Set (lhs_exp, typ, rhs_exp, loc) -> - execute_set pname pdesc tenv lhs_exp typ rhs_exp loc prop_ + execute_set current_pname current_pdesc tenv lhs_exp typ rhs_exp loc prop_ |> ret_old_path | Sil.Prune (cond, loc, true_branch, ik) -> let prop__ = Prop.nullify_exp_with_objc_null prop_ cond in @@ -1037,8 +1042,8 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path let desc = Errdesc.explain_condition_always_true_false i cond node loc in let exn = Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), __POS__) in - let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in - Reporting.log_warning pname ~pre: pre_opt exn + let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop current_pname) in + Reporting.log_warning current_pname ~pre: pre_opt exn | Sil.BinOp ((Sil.Eq | Sil.Ne), lhs, rhs) when true_branch && !Config.footprint && not (is_comparison_to_nil rhs) -> (* iOS: check that NSNumber *'s are not used in conditionals without comparing to nil *) @@ -1058,19 +1063,19 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path let node = State.get_node () in let desc = Errdesc.explain_bad_pointer_comparison lhs node loc in let exn = Exceptions.Bad_pointer_comparison (desc, __POS__) in - Reporting.log_warning pname exn + Reporting.log_warning current_pname exn | _ -> () in if not !Config.report_runtime_exceptions then - check_already_dereferenced pname cond prop__; + check_already_dereferenced current_pname cond prop__; check_condition_always_true_false (); - let n_cond, prop = exp_norm_check_arith pname prop__ cond in + let n_cond, prop = exp_norm_check_arith current_pname prop__ cond in ret_old_path (Propset.to_proplist (prune_prop n_cond prop)) | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), args, loc, _) when function_is_builtin callee_pname -> let sym_exe_builtin = Builtin.get_sym_exe_builtin callee_pname in sym_exe_builtin { - pdesc; + pdesc = current_pdesc; instr; tenv; prop_; @@ -1080,17 +1085,19 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path proc_name = 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 + | Sil.Call (ret_ids, + Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)), + actual_params, loc, call_flags) + when Config.lazy_dynamic_dispatch -> + let norm_prop, norm_args = normalize_params current_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 tenv pdesc norm_prop norm_args callee_pname call_flags in + resolve_and_analyze tenv current_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_str = Procname.java_get_return_type callee_pname_java 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) @@ -1099,24 +1106,29 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path | 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 pdesc tenv norm_prop path ret_ids norm_args summary loc + sym_exec_call current_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; - let norm_prop, norm_args = normalize_params pname prop_ actual_params in + | Sil.Call (ret_ids, + Sil.Const (Sil.Cfun ((Procname.Java _) as callee_pname)), + actual_params, loc, call_flags) -> + do_error_checks (Paths.Path.curr_node path) instr current_pname current_pdesc; + let norm_prop, norm_args = normalize_params current_pname prop_ actual_params in let url_handled_args = call_constructor_url_update_args callee_pname norm_args in let resolved_pnames = resolve_virtual_pname tenv norm_prop url_handled_args callee_pname call_flags in let exec_one_pname pname = - Ondemand.analyze_proc_name ~propagate_exceptions:true pdesc pname; + Ondemand.analyze_proc_name ~propagate_exceptions:true current_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 pname in + let ret_typ_str = match pname with + | Procname.Java pname_java -> + Procname.java_get_return_type pname_java + | _ -> + "unknown_return_type" 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) @@ -1125,18 +1137,18 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path | Some summary when call_should_be_skipped pname summary -> exec_skip_call summary.Specs.attributes.ProcAttributes.ret_type | Some summary -> - sym_exec_call pdesc tenv norm_prop path ret_ids url_handled_args summary loc in + sym_exec_call current_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 (prop_r, n_actual_params) = normalize_params current_pname prop_ actual_params in let resolved_pname = match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with | resolved_pname :: _ -> resolved_pname | [] -> callee_pname in - Ondemand.analyze_proc_name ~propagate_exceptions:true pdesc resolved_pname; + Ondemand.analyze_proc_name ~propagate_exceptions:true current_pdesc resolved_pname; let callee_pdesc_opt = Ondemand.get_proc_desc resolved_pname in @@ -1144,7 +1156,7 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path let sentinel_result = if !Config.curr_language = Config.C_CPP then sym_exe_check_variadic_sentinel_if_present - { Builtin.pdesc; + { Builtin.pdesc = current_pdesc; instr; tenv; prop_ = prop_r; @@ -1171,18 +1183,20 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path match objc_property_accessor with | Some objc_property_accessor -> handle_objc_method_call - n_actual_params n_actual_params prop tenv ret_ids pdesc callee_pname loc path + n_actual_params n_actual_params prop tenv ret_ids + current_pdesc callee_pname loc path (sym_exec_objc_accessor objc_property_accessor ret_typ_opt) | None -> skip_call prop path resolved_pname loc ret_ids ret_typ_opt n_actual_params else - sym_exec_call pdesc tenv prop path ret_ids n_actual_params (Option.get summary) loc in + sym_exec_call + current_pdesc tenv prop path ret_ids n_actual_params (Option.get summary) loc in IList.flatten (IList.map do_call sentinel_result) | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *) - let (prop_r, n_actual_params) = normalize_params pname prop_ actual_params in + let (prop_r, n_actual_params) = normalize_params current_pname prop_ actual_params in if call_flags.Sil.cf_is_objc_block then - Rearrange.check_call_to_objc_block_error pdesc prop_r fun_exp loc; - Rearrange.check_dereference_error pdesc prop_r fun_exp loc; + Rearrange.check_call_to_objc_block_error current_pdesc prop_r fun_exp loc; + Rearrange.check_dereference_error current_pdesc prop_r fun_exp loc; if call_flags.Sil.cf_noreturn then begin L.d_str "Unknown function pointer with noreturn attribute "; Sil.d_exp fun_exp; L.d_strln ", diverging."; execute_diverge prop_r path @@ -1190,7 +1204,7 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path L.d_str "Unknown function pointer "; Sil.d_exp fun_exp; L.d_strln ", returning undefined value."; let callee_pname = Procname.from_string_c_fun "__function_pointer__" in call_unknown_or_scan - tenv false pdesc prop_r path ret_ids None n_actual_params callee_pname loc + tenv false current_pdesc prop_r path ret_ids None n_actual_params callee_pname loc end | Sil.Nullify (pvar, _, deallocate) -> begin @@ -1212,13 +1226,14 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path | Sil.Abstract _ -> let node = State.get_node () in let blocks_nullified = get_blocks_nullified node in - IList.iter (check_block_retain_cycle tenv pname prop_) blocks_nullified; + IList.iter (check_block_retain_cycle tenv current_pname prop_) blocks_nullified; if Prover.check_inconsistency prop_ then ret_old_path [] else - ret_old_path [Abs.remove_redundant_array_elements pname tenv - (Abs.abstract pname tenv prop_)] + ret_old_path + [Abs.remove_redundant_array_elements current_pname tenv + (Abs.abstract current_pname tenv prop_)] | Sil.Remove_temps (temps, _) -> ret_old_path [Prop.exist_quantify (Sil.fav_from_list temps) prop_] | Sil.Declare_locals (ptl, _) -> @@ -1236,7 +1251,7 @@ let rec sym_exec tenv pdesc _instr (prop_: Prop.normal Prop.t) path | Sil.Stackop _ -> (* this should be handled at the propset level *) assert false | Sil.Goto_node (node_e, _) -> - let n_node_e, prop = exp_norm_check_arith pname prop_ node_e in + let n_node_e, prop = exp_norm_check_arith current_pname prop_ node_e in begin match n_node_e with | Sil.Const (Sil.Cint i) -> diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index 51d41c8c2..7a1642758 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -127,12 +127,13 @@ let functions_with_tainted_params = [ (* turn string specificiation of Java method into a procname *) let java_method_to_procname java_method = - Procname.mangled_java - (Procname.split_classname java_method.classname) - (Some (Procname.split_classname java_method.ret_type)) - java_method.method_name - (IList.map Procname.split_classname java_method.params) - (if java_method.is_static then Procname.Static else Procname.Non_Static) + Procname.Java + (Procname.java + (Procname.split_classname java_method.classname) + (Some (Procname.split_classname java_method.ret_type)) + java_method.method_name + (IList.map Procname.split_classname java_method.params) + (if java_method.is_static then Procname.Static else Procname.Non_Static)) (* turn string specificiation of an objc method into a procname *) let objc_method_to_procname objc_method = diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 446920ff5..69e3694d2 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -983,3 +983,9 @@ let run_in_footprint_mode f x = let run_with_abs_val_equal_zero f x = set_reference_and_call_function Config.abs_val 0 f x + +let assert_false ((file, lnum, cnum, _) as ml_loc) = + Printf.eprintf "\nASSERT FALSE %s\nCALL STACK\n%s\n%!" + (ml_loc_to_string ml_loc) + (Printexc.raw_backtrace_to_string (Printexc.get_callstack 1000)); + raise (Assert_failure (file, lnum, cnum)) diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index 823a0fdeb..bc843701f 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -375,3 +375,6 @@ val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b (** [set_reference_and_call_function ref val f x] calls f x with ref set to val. Restore the initial value also in case of exception. *) val set_reference_and_call_function : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c + +(** Pritn stack trace and throw assert false *) +val assert_false : ml_loc -> 'a diff --git a/infer/src/checkers/callbackChecker.ml b/infer/src/checkers/callbackChecker.ml index 7817603cc..2a3247d27 100644 --- a/infer/src/checkers/callbackChecker.ml +++ b/infer/src/checkers/callbackChecker.ml @@ -61,11 +61,11 @@ let do_eradicate_check ({ Callbacks.get_proc_desc } as callback_args) = (** if [procname] belongs to an Android lifecycle type, save the set of callbacks registered in * [procname]. in addition, if [procname] is a special "destroy" /"cleanup" method, save the set of * fields that are nullified *) -let callback_checker_main - ({ Callbacks.proc_desc; proc_name; tenv } as callback_args) = +let callback_checker_main_java + proc_name_java ({ Callbacks.proc_desc; tenv } as callback_args) = let typename = Typename.TN_csu - (Csu.Class Csu.Java, Mangled.from_string (Procname.java_get_class proc_name)) in + (Csu.Class Csu.Java, Mangled.from_string (Procname.java_get_class proc_name_java)) in match Sil.tenv_lookup tenv typename with | Some ({ struct_name = Some _; def_methods } as struct_typ) -> let typ = Sil.Tstruct struct_typ in @@ -93,7 +93,7 @@ let callback_checker_main !registered_callback_procs registered_callback_typs in registered_callback_procs := registered_callback_procs'; - let _ = if AndroidFramework.is_destroy_method proc_name then + let _ = if AndroidFramework.is_destroy_method callback_args.Callbacks.proc_name then (* compute the set of fields nullified by this procedure *) (* TODO (t4959422): get fields that are nullified in callees of the destroy method *) fields_nullified := @@ -101,3 +101,12 @@ let callback_checker_main if done_checking (IList.length def_methods) then do_eradicate_check callback_args | _ -> () + + +let callback_checker_main + ({ Callbacks.proc_name } as callback_args) = + match proc_name with + | Procname.Java pname_java -> + callback_checker_main_java pname_java callback_args + | _ -> + () diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml index 4f3081045..a1c2219fb 100644 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -43,11 +43,17 @@ let report_warning description pn pd loc = (** Tracing APIs. *) module APIs = struct let method_match pn pkgname cname mname = - Procname.is_java pn && - Procname.java_get_method pn = mname && - (match pkgname with - | "" -> Procname.java_get_simple_class pn = cname - | _ -> Procname.java_get_class pn = pkgname ^ "." ^ cname) + match pn with + | Procname.Java pn_java -> + Procname.java_get_method pn_java = mname + && + (match pkgname with + | "" -> + Procname.java_get_simple_class pn_java = cname + | _ -> + Procname.java_get_class pn_java = pkgname ^ "." ^ cname) + | _ -> + false let is_begin pn = let filter (pkgname, cname, begin_name, _) = method_match pn pkgname cname begin_name in IList.exists filter tracing_methods @@ -181,14 +187,19 @@ module Automaton = struct (** Transfer function for a procedure call. *) let do_call caller_pn caller_pd callee_pn (s : State.t) loc : State.t = + let method_name () = match callee_pn with + | Procname.Java pname_java -> + Procname.java_get_method pname_java + | _ -> + Procname.to_simplified_string callee_pn in if APIs.is_begin callee_pn then begin - if verbose then L.stderr " calling %s@." (Procname.java_get_method callee_pn); + if verbose then L.stderr " calling %s@." (method_name ()); State.incr s end else if APIs.is_end callee_pn then begin - if verbose then L.stderr " calling %s@." (Procname.java_get_method callee_pn); + if verbose then L.stderr " calling %s@." (method_name ()); if State.has_zero s then report_warning "too many end/stop" caller_pn caller_pd loc; State.decr s end diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 972ce9862..6077fc133 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -190,11 +190,13 @@ let callback_check_cluster_access all_procs get_proc_desc _ = (IList.map get_proc_desc all_procs) (** Looks for writeToParcel methods and checks whether read is in reverse *) -let callback_check_write_to_parcel { Callbacks.proc_desc; proc_name; idenv; get_proc_desc } = +let callback_check_write_to_parcel_java + pname_java ({ Callbacks.proc_desc; idenv; get_proc_desc } as args) = let verbose = ref false in let is_write_to_parcel this_expr this_type = - let method_match () = Procname.java_get_method proc_name = "writeToParcel" in + let method_match () = + Procname.java_get_method pname_java = "writeToParcel" in let expr_match () = Sil.exp_is_this this_expr in let type_match () = let class_name = @@ -204,7 +206,8 @@ let callback_check_write_to_parcel { Callbacks.proc_desc; proc_name; idenv; get_ let is_parcel_constructor proc_name = Procname.is_constructor proc_name && - PatternMatch.has_formal_method_argument_type_names proc_desc proc_name ["android.os.Parcel"] in + PatternMatch.has_formal_method_argument_type_names + proc_desc pname_java ["android.os.Parcel"] in let parcel_constructors = function | Sil.Tptr (Sil.Tstruct { Sil.def_methods }, _) -> @@ -216,41 +219,60 @@ let callback_check_write_to_parcel { Callbacks.proc_desc; proc_name; idenv; get_ let is_serialization_node node = match Cfg.Node.get_callees node with | [] -> false - | [proc_name] -> - let class_name = Procname.java_get_class proc_name in - let method_name = Procname.java_get_method proc_name in + | [Procname.Java pname_java] -> + let class_name = Procname.java_get_class pname_java in + let method_name = Procname.java_get_method pname_java in (try - class_name = "android.os.Parcel" && (String.sub method_name 0 5 = "write" || String.sub method_name 0 4 = "read") + class_name = "android.os.Parcel" && + (String.sub method_name 0 5 = "write" + || + String.sub method_name 0 4 = "read") with Invalid_argument _ -> false) | _ -> assert false in - let is_inverse rc wc = - let rn = Procname.java_get_method rc in - let wn = Procname.java_get_method wc in - let postfix_length = String.length wn - 5 in (* covers writeList <-> readArrayList etc. *) - try - String.sub rn (String.length rn - postfix_length) postfix_length = String.sub wn 5 postfix_length - with Invalid_argument _ -> false in + let is_inverse rc_ wc_ = match rc_, wc_ with + | Procname.Java rc, Procname.Java wc -> + let rn = Procname.java_get_method rc in + let wn = Procname.java_get_method wc in + let postfix_length = String.length wn - 5 in (* covers writeList <-> readArrayList etc. *) + (try + String.sub rn (String.length rn - postfix_length) postfix_length = + String.sub wn 5 postfix_length + with Invalid_argument _ -> false) + | _ -> + false in let node_to_call_desc node = match Cfg.Node.get_callees node with | [desc] -> desc | _ -> assert false in - let r_call_descs = IList.map node_to_call_desc (IList.filter is_serialization_node (Cfg.Procdesc.get_sliced_slope r_desc is_serialization_node)) in - let w_call_descs = IList.map node_to_call_desc (IList.filter is_serialization_node (Cfg.Procdesc.get_sliced_slope w_desc is_serialization_node)) in + let r_call_descs = + IList.map node_to_call_desc + (IList.filter is_serialization_node + (Cfg.Procdesc.get_sliced_slope r_desc is_serialization_node)) in + let w_call_descs = + IList.map node_to_call_desc + (IList.filter is_serialization_node + (Cfg.Procdesc.get_sliced_slope w_desc is_serialization_node)) in let rec check_match = function | rc:: rcs, wc:: wcs -> if not (is_inverse rc wc) then - L.stdout "Serialization missmatch in %a for %a and %a@." Procname.pp proc_name Procname.pp rc Procname.pp wc + L.stdout "Serialization missmatch in %a for %a and %a@." + Procname.pp args.Callbacks.proc_name + Procname.pp rc + Procname.pp wc else check_match (rcs, wcs) | rc:: _, [] -> - L.stdout "Missing write in %a: for %a@." Procname.pp proc_name Procname.pp rc + L.stdout "Missing write in %a: for %a@." + Procname.pp args.Callbacks.proc_name Procname.pp rc | _, wc:: _ -> - L.stdout "Missing read in %a: for %a@." Procname.pp proc_name Procname.pp wc - | _ -> () in + L.stdout "Missing read in %a: for %a@." + Procname.pp args.Callbacks.proc_name Procname.pp wc + | _ -> + () in check_match (r_call_descs, w_call_descs) in @@ -258,19 +280,32 @@ let callback_check_write_to_parcel { Callbacks.proc_desc; proc_name; idenv; get_ | Sil.Call (_, Sil.Const (Sil.Cfun _), (_this_exp, this_type):: _, _, _) -> let this_exp = Idenv.expand_expr idenv _this_exp in if is_write_to_parcel this_exp this_type then begin - if !verbose then L.stdout "Serialization check for %a@." Procname.pp proc_name; + if !verbose then + L.stdout "Serialization check for %a@." + Procname.pp args.Callbacks.proc_name; try match parcel_constructors this_type with | x :: _ -> (match get_proc_desc x with | Some x_proc_desc -> check x_proc_desc proc_desc | None -> raise Not_found) - | _ -> L.stdout "No parcel constructor found for %a@." Procname.pp proc_name - with Not_found -> if !verbose then L.stdout "Methods not available@." + | _ -> + L.stdout "No parcel constructor found for %a@." + Procname.pp args.Callbacks.proc_name + with Not_found -> + if !verbose then L.stdout "Methods not available@." end | _ -> () in Cfg.Procdesc.iter_instrs do_instr proc_desc +(** Looks for writeToParcel methods and checks whether read is in reverse *) +let callback_check_write_to_parcel ({ Callbacks.proc_name } as args) = + match proc_name with + | Procname.Java pname_java -> + callback_check_write_to_parcel_java pname_java args + | _ -> + () + (** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *) let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } = let verbose = ref false in @@ -295,9 +330,12 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } = let is_formal_param exp = IList.exists (equal_formal_param exp) (Lazy.force class_formal_names) in - let is_nullcheck pn = - PatternMatch.java_proc_name_with_class_method - pn "com.google.common.base.Preconditions" "checkNotNull" in + let is_nullcheck pn = match pn with + | Procname.Java pn_java -> + PatternMatch.java_proc_name_with_class_method + pn_java "com.google.common.base.Preconditions" "checkNotNull" + | _ -> + false in let checks_to_formals = ref Sil.ExpSet.empty in @@ -333,7 +371,16 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } = | Sil.Call (_, Sil.Const (Sil.Cfun pn), (_arg1, _):: _, _, _) when is_nullcheck pn -> let arg1 = Idenv.expand_expr idenv _arg1 in if is_formal_param arg1 then handle_check_of_formal arg1; - if !verbose then L.stdout "call in %s %s: %a with first arg: %a@." (Procname.java_get_class proc_name) (Procname.java_get_method proc_name) (Sil.pp_instr pe_text) instr (Sil.pp_exp pe_text) arg1 + if !verbose then + (match proc_name with + | Procname.Java pname_java -> + L.stdout "call in %s %s: %a with first arg: %a@." + (Procname.java_get_class pname_java) + (Procname.java_get_method pname_java) + (Sil.pp_instr pe_text) instr + (Sil.pp_exp pe_text) arg1 + | _ -> + ()) | _ -> () in Cfg.Procdesc.iter_instrs do_instr proc_desc; summary_checks_of_formals () diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml index 3a240396a..8cc760e97 100644 --- a/infer/src/checkers/constantPropagation.ml +++ b/infer/src/checkers/constantPropagation.ml @@ -55,6 +55,17 @@ module ConstantFlow = Dataflow.MakeDF(struct constants (ConstantMap.add key value ConstantMap.empty) in + let has_class pn name = match pn with + | Procname.Java pn_java -> + Procname.java_get_class pn_java = name + | _ -> + false in + let has_method pn name = match pn with + | Procname.Java pn_java -> + Procname.java_get_method pn_java = name + | _ -> + false in + match instr with | Sil.Letderef (i, Sil.Lvar p, _, _) -> (* tmp = var *) update (Sil.Var i) (ConstantMap.find (Sil.Lvar p) constants) constants @@ -67,18 +78,18 @@ module ConstantFlow = Dataflow.MakeDF(struct (* Handle propagation of string with StringBuilder. Does not handle null case *) | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var sb, _):: [], _, _) - when Procname.java_get_class pn = "java.lang.StringBuilder" - && Procname.java_get_method pn = "" -> (* StringBuilder. *) + when has_class pn "java.lang.StringBuilder" + && has_method pn "" -> (* StringBuilder. *) update (Sil.Var sb) (Some (Sil.Cstr "")) constants | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: [], _, _) - when Procname.java_get_class pn = "java.lang.StringBuilder" - && Procname.java_get_method pn = "toString" -> (* StringBuilder.toString *) + when has_class pn "java.lang.StringBuilder" + && has_method pn "toString" -> (* StringBuilder.toString *) update (Sil.Var i) (ConstantMap.find (Sil.Var i1) constants) constants | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], _, _) - when Procname.java_get_class pn = "java.lang.StringBuilder" - && Procname.java_get_method pn = "append" -> (* StringBuilder.append *) + when has_class pn "java.lang.StringBuilder" + && has_method pn "append" -> (* StringBuilder.append *) (match ConstantMap.find (Sil.Var i1) constants, ConstantMap.find (Sil.Var i2) constants with diff --git a/infer/src/checkers/fragmentRetainsViewChecker.ml b/infer/src/checkers/fragmentRetainsViewChecker.ml index 19cf9327c..ccefa360b 100644 --- a/infer/src/checkers/fragmentRetainsViewChecker.ml +++ b/infer/src/checkers/fragmentRetainsViewChecker.ml @@ -18,10 +18,11 @@ let report_error fragment_typ fld fld_typ pname pdesc = let loc = Cfg.Procdesc.get_loc pdesc in Reporting.log_error pname ~loc:(Some loc) exn -let callback_fragment_retains_view { Callbacks.proc_desc; proc_name; tenv } = +let callback_fragment_retains_view_java + pname_java { Callbacks.proc_desc; tenv } = (* TODO: complain if onDestroyView is not defined, yet the Fragment has View fields *) (* TODO: handle fields nullified in callees in the same file *) - let is_on_destroy_view = Procname.java_get_method proc_name = "onDestroyView" in + let is_on_destroy_view = Procname.java_get_method pname_java = "onDestroyView" in (* this is needlessly complicated because field types are Tvars instead of Tstructs *) let fld_typ_is_view = function | Sil.Tptr (Sil.Tvar tname, _) -> @@ -37,7 +38,7 @@ let callback_fragment_retains_view { Callbacks.proc_desc; proc_name; tenv } = Typename.equal fld_classname class_typename && fld_typ_is_view fld_typ in if is_on_destroy_view then begin - let class_typename = Typename.Java.from_string (Procname.java_get_class proc_name) in + let class_typename = Typename.Java.from_string (Procname.java_get_class pname_java) in match Sil.tenv_lookup tenv class_typename with | Some ({ Sil.struct_name = Some _; instance_fields } as struct_typ) when AndroidFramework.is_fragment (Sil.Tstruct struct_typ) tenv -> @@ -48,7 +49,16 @@ let callback_fragment_retains_view { Callbacks.proc_desc; proc_name; tenv } = IList.iter (fun (fname, fld_typ, _) -> if not (Ident.FieldSet.mem fname fields_nullified) then - report_error (Sil.Tstruct struct_typ) fname fld_typ proc_name proc_desc) + report_error + (Sil.Tstruct struct_typ) fname fld_typ + (Procname.Java pname_java) proc_desc) declared_view_fields | _ -> () end + +let callback_fragment_retains_view ({ Callbacks.proc_name } as args) = + match proc_name with + | Procname.Java pname_java -> + callback_fragment_retains_view_java pname_java args + | _ -> + () diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index b4d539dc7..1a48e423a 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -28,10 +28,10 @@ let type_is_object = function Mangled.equal name object_name | _ -> false -let java_proc_name_with_class_method pn class_with_path method_name = +let java_proc_name_with_class_method pn_java class_with_path method_name = (try - Procname.java_get_class pn = class_with_path && - Procname.java_get_method pn = method_name + Procname.java_get_class pn_java = class_with_path && + Procname.java_get_method pn_java = method_name with _ -> false) let is_direct_subtype_of this_type super_type_name = @@ -197,15 +197,15 @@ let has_formal_proc_argument_type_names proc_desc argument_type_names = IList.length formals = IList.length argument_type_names && IList.for_all2 equal_formal_arg formals argument_type_names -let has_formal_method_argument_type_names cfg proc_name argument_type_names = +let has_formal_method_argument_type_names cfg pname_java argument_type_names = has_formal_proc_argument_type_names - cfg ((Procname.java_get_class proc_name):: argument_type_names) + cfg ((Procname.java_get_class pname_java):: argument_type_names) -let is_getter proc_name = - Str.string_match (Str.regexp "get*") (Procname.java_get_method proc_name) 0 +let is_getter pname_java = + Str.string_match (Str.regexp "get*") (Procname.java_get_method pname_java) 0 -let is_setter proc_name = - Str.string_match (Str.regexp "set*") (Procname.java_get_method proc_name) 0 +let is_setter pname_java = + Str.string_match (Str.regexp "set*") (Procname.java_get_method pname_java) 0 (** Returns the signature of a field access (class name, field name, field type name) *) let get_java_field_access_signature = function @@ -217,12 +217,14 @@ let get_java_field_access_signature = function argument type names and return type name) *) let get_java_method_call_formal_signature = function | Sil.Call (_, Sil.Const (Sil.Cfun pn), (_, tt):: args, _, _) -> - (try - let arg_names = IList.map (function | _, t -> get_type_name t) args in - let rt_name = Procname.java_get_return_type pn in - let m_name = Procname.java_get_method pn in - Some (get_type_name tt, m_name, arg_names, rt_name) - with _ -> None) + (match pn with + | Procname.Java pn_java -> + let arg_names = IList.map (function | _, t -> get_type_name t) args in + let rt_name = Procname.java_get_return_type pn_java in + let m_name = Procname.java_get_method pn_java in + Some (get_type_name tt, m_name, arg_names, rt_name) + | _ -> + None) | _ -> None @@ -265,8 +267,12 @@ let method_is_initializer match get_this_type proc_attributes with | Some this_type -> if type_has_initializer tenv this_type then - let mname = Procname.java_get_method (proc_attributes.ProcAttributes.proc_name) in - IList.exists (string_equal mname) initializer_methods + match proc_attributes.ProcAttributes.proc_name with + | Procname.Java pname_java -> + let mname = Procname.java_get_method pname_java in + IList.exists (string_equal mname) initializer_methods + | _ -> + false else false | None -> false @@ -326,14 +332,20 @@ let proc_iter_overridden_methods f tenv proc_name = def_methods | _ -> () in - if Procname.is_java proc_name then - let type_name = - let class_name = Procname.java_get_class proc_name in - Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string class_name) in - match Sil.tenv_lookup tenv type_name with - | Some curr_struct_typ -> - IList.iter (do_super_type tenv) (type_get_direct_supertypes (Sil.Tstruct curr_struct_typ)) - | None -> () + match proc_name with + | Procname.Java pname_java -> + let type_name = + let class_name = Procname.java_get_class pname_java in + Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string class_name) in + (match Sil.tenv_lookup tenv type_name with + | Some curr_struct_typ -> + IList.iter + (do_super_type tenv) + (type_get_direct_supertypes (Sil.Tstruct curr_struct_typ)) + | None -> + ()) + | _ -> + () (* Only java supported at the moment *) (** return the set of instance fields that are assigned to a null literal in [procdesc] *) let get_fields_nullified procdesc = diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli index 3ec90341f..e45cfc8e4 100644 --- a/infer/src/checkers/patternMatch.mli +++ b/infer/src/checkers/patternMatch.mli @@ -35,16 +35,17 @@ val get_type_name : Sil.typ -> string (** Get the type names of a variable argument *) val get_vararg_type_names : Cfg.Node.t -> Sil.pvar -> string list -val has_formal_method_argument_type_names : Cfg.Procdesc.t -> Procname.t -> string list -> bool +val has_formal_method_argument_type_names : + Cfg.Procdesc.t -> Procname.java -> string list -> bool (** Check if the method is one of the known initializer methods. *) val method_is_initializer : Sil.tenv -> ProcAttributes.t -> bool (** Is this a getter proc name? *) -val is_getter : Procname.t -> bool +val is_getter : Procname.java -> bool (** Is this a setter proc name? *) -val is_setter : Procname.t -> bool +val is_setter : Procname.java -> bool (** Is the type a direct subtype of *) val is_direct_subtype_of : Sil.typ -> Typename.t -> bool @@ -55,7 +56,7 @@ val java_get_const_type_name : Sil.const -> string (** Get the values of a vararg parameter given the pvar used to assign the elements. *) val java_get_vararg_values : Cfg.Node.t -> Sil.pvar -> Idenv.t -> Sil.exp list -val java_proc_name_with_class_method : Procname.t -> string -> string -> bool +val java_proc_name_with_class_method : Procname.java -> string -> string -> bool (** Return the callees that satisfy [filter]. *) val proc_calls : diff --git a/infer/src/checkers/performanceCritical.ml b/infer/src/checkers/performanceCritical.ml index 01d6140d5..e4196b15e 100644 --- a/infer/src/checkers/performanceCritical.ml +++ b/infer/src/checkers/performanceCritical.ml @@ -33,11 +33,14 @@ let is_modeled_expensive = let matcher = lazy (let config_file = Inferconfig.inferconfig () in Inferconfig.ModeledExpensiveMatcher.load_matcher config_file) in - fun tenv proc_name -> - not (SymExec.function_is_builtin proc_name) && - let classname = - Typename.Java.from_string (Procname.java_get_class proc_name) in - (Lazy.force matcher) (AndroidFramework.is_subclass tenv classname) proc_name + fun tenv proc_name -> match proc_name with + | Procname.Java proc_name_java -> + not (SymExec.function_is_builtin proc_name) && + let classname = + Typename.Java.from_string (Procname.java_get_class proc_name_java) in + (Lazy.force matcher) (AndroidFramework.is_subclass tenv classname) proc_name + | _ -> + false let check_attributes check attributes = @@ -119,14 +122,17 @@ let method_calls_expensive tenv pname = || calls_expensive () -let is_allocator tenv pname = - let is_throwable () = - let class_name = - Typename.Java.from_string (Procname.java_get_class pname) in - AndroidFramework.is_throwable tenv class_name in - Procname.is_constructor pname - && not (SymExec.function_is_builtin pname) - && not (is_throwable ()) +let is_allocator tenv pname = match pname with + | Procname.Java pname_java -> + let is_throwable () = + let class_name = + Typename.Java.from_string (Procname.java_get_class pname_java) in + AndroidFramework.is_throwable tenv class_name in + Procname.is_constructor pname + && not (SymExec.function_is_builtin pname) + && not (is_throwable ()) + | _ -> + false let method_allocates tenv pname = diff --git a/infer/src/checkers/sqlChecker.ml b/infer/src/checkers/sqlChecker.ml index 458866871..5cb6d13d5 100644 --- a/infer/src/checkers/sqlChecker.ml +++ b/infer/src/checkers/sqlChecker.ml @@ -25,26 +25,39 @@ let callback_sql { Callbacks.proc_desc; proc_name } = IList.map Str.regexp_case_fold _sql_start in (* Check for SQL string concatenations *) - let do_instr const_map node = function - | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], l, _) - when Procname.java_get_class pn = "java.lang.StringBuilder" - && Procname.java_get_method pn = "append" -> - let rvar1 = Sil.Var i1 in - let rvar2 = Sil.Var i2 in + let do_instr const_map node instr = + let do_call pn_java i1 i2 l = + if Procname.java_get_class pn_java = "java.lang.StringBuilder" + && Procname.java_get_method pn_java = "append" + then begin - let matches s r = Str.string_match r s 0 in - match const_map node rvar1, const_map node rvar2 with - | Some (Sil.Cstr ""), Some (Sil.Cstr s2) -> - if IList.exists (matches s2) sql_start then - begin - L.stdout - "%s%s@." - "Possible SQL query using string concatenation. " - "Please consider using a prepared statement instead."; - let linereader = Printer.LineReader.create () in - L.stdout "%a@." (Checkers.PP.pp_loc_range linereader 2 2) l - end - | _ -> () + let rvar1 = Sil.Var i1 in + let rvar2 = Sil.Var i2 in + begin + let matches s r = Str.string_match r s 0 in + match const_map node rvar1, const_map node rvar2 with + | Some (Sil.Cstr ""), Some (Sil.Cstr s2) -> + if IList.exists (matches s2) sql_start then + begin + L.stdout + "%s%s@." + "Possible SQL query using string concatenation. " + "Please consider using a prepared statement instead."; + let linereader = Printer.LineReader.create () in + L.stdout "%a@." (Checkers.PP.pp_loc_range linereader 2 2) l + end + | _ -> () + end + end in + + match instr with + | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], l, _) -> + begin + match pn with + | Procname.Java pn_java -> + do_call pn_java i1 i2 l + | _ -> + () end | _ -> () in diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 723ee8ba4..b7a11f173 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -195,9 +195,11 @@ struct let is_private = callee_attributes.ProcAttributes.access = Sil.Private in let same_class = - let get_class_opt pn = - if Procname.is_java pn then Some (Procname.java_get_class pn) - else None in + let get_class_opt pn = match pn with + | Procname.Java pn_java -> + Some (Procname.java_get_class pn_java) + | _ -> + None in get_class_opt init_pn = get_class_opt callee_pn in is_private && same_class in let private_called = PatternMatch.proc_calls @@ -257,6 +259,12 @@ struct IList.iter do_proc (get_procs_in_file curr_pname); IList.rev !res + let get_class pn = match pn with + | Procname.Java pn_java -> + Some (Procname.java_get_class pn_java) + | _ -> + None + (** Typestates after the current procedure and all initializer procedures. *) let final_initializer_typestates_lazy = lazy begin @@ -269,7 +277,7 @@ struct pname_and_pdescs_with (function (pname, proc_attributes) -> is_initializer proc_attributes && - Procname.java_get_class pname = Procname.java_get_class curr_pname) in + get_class pname = get_class curr_pname) in final_typestates ((curr_pname, curr_pdesc) :: initializers_current_class) end @@ -281,7 +289,7 @@ struct pname_and_pdescs_with (fun (pname, _) -> Procname.is_constructor pname && - Procname.java_get_class pname = Procname.java_get_class curr_pname) in + get_class pname = get_class curr_pname) in final_typestates constructors_current_class end diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index 6df3ccd65..b3c61a659 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -50,7 +50,8 @@ let get_field_annotation fn typ = else ia in Some (t, ia') -let report_error = TypeErr.report_error Checkers.ST.report_error +let report_error = + TypeErr.report_error Checkers.ST.report_error let explain_expr node e = match Errdesc.exp_rv_dexp node e with @@ -516,7 +517,6 @@ let check_call_parameters implemented interfaces *) let check_overridden_annotations find_canonical_duplicate tenv proc_name proc_desc annotated_signature = - let start_node = Cfg.Procdesc.get_start_node proc_desc in let loc = Cfg.Node.get_loc start_node in diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 6d0621109..0d18f1b46 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -384,8 +384,12 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc | _ -> default in let constructor_check_calls_this calls_this pn = - if Procname.java_get_class curr_pname = Procname.java_get_class pn - then calls_this := true in + match curr_pname, pn with + | Procname.Java curr_pname_java, Procname.Java pn_java -> + if Procname.java_get_class curr_pname_java = Procname.java_get_class pn_java + then calls_this := true + | _ -> + () in (* Drops hidden and synthetic parameters which we do not check in a call. *) let drop_unchecked_params calls_this proc_attributes params = @@ -796,13 +800,18 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc get_proc_desc curr_pname curr_pdesc extension instr etl' in TypeState.set_extension typestate1 extension' else typestate1 in + let has_method pn name = match pn with + | Procname.Java pn_java -> + Procname.java_get_method pn_java = name + | _ -> + false in if Models.is_check_not_null callee_pname then do_preconditions_check_not_null (Models.get_check_not_null_parameter callee_pname) false (* is_vararg *) typestate2 else - if Procname.java_get_method callee_pname = "checkNotNull" + if has_method callee_pname "checkNotNull" && Procname.java_is_vararg callee_pname then let last_parameter = IList.length call_params in diff --git a/infer/src/eradicate/typeErr.ml b/infer/src/eradicate/typeErr.ml index 8333b6af1..2e87b9e61 100644 --- a/infer/src/eradicate/typeErr.ml +++ b/infer/src/eradicate/typeErr.ml @@ -303,10 +303,16 @@ type st_report_error = unit (** Report an error right now. *) -let report_error_now (st_report_error : st_report_error) node err_instance loc proc_name : unit = +let report_error_now + (st_report_error : st_report_error) node err_instance loc pname : unit = let demo_mode = true in let do_print_base ew_string kind_s s = - L.stdout "%s %s in %s %s@." ew_string kind_s (Procname.java_get_method proc_name) s in + let mname = match pname with + | Procname.Java pname_java -> + Procname.java_get_method pname_java + | _ -> + Procname.to_simplified_string pname in + L.stdout "%s %s in %s %s@." ew_string kind_s mname s in let do_print ew_string kind_s s = L.stdout "%s:%d " (DB.source_file_to_string loc.Location.file) loc.Location.line; do_print_base ew_string kind_s s in @@ -335,7 +341,14 @@ let report_error_now (st_report_error : st_report_error) node err_instance loc p None | Field_not_initialized (fn, pn) -> let constructor_name = - if Procname.is_constructor pn then "the constructor" else Procname.java_get_method pn in + if Procname.is_constructor pn + then "the constructor" + else + match pn with + | Procname.Java pn_java -> + Procname.java_get_method pn_java + | _ -> + Procname.to_simplified_string pn in true, "ERADICATE_FIELD_NOT_INITIALIZED", P.sprintf @@ -377,7 +390,14 @@ let report_error_now (st_report_error : st_report_error) node err_instance loc p origin_loc | Field_over_annotated (fn, pn) -> let constructor_name = - if Procname.is_constructor pn then "the constructor" else Procname.java_get_method pn in + if Procname.is_constructor pn + then "the constructor" + else + match pn with + | Procname.Java pn_java -> + Procname.java_get_method pn_java + | _ -> + Procname.to_simplified_string pn in true, "ERADICATE_FIELD_OVER_ANNOTATED", P.sprintf @@ -432,13 +452,14 @@ let report_error_now (st_report_error : st_report_error) node err_instance loc p n s origin_desc - | Annotations.Present -> "ERADICATE_PARAMETER_VALUE_ABSENT", - P.sprintf - "`%s` needs a present value in parameter %d but argument `%s` can be absent. %s" - (Procname.to_simplified_string pn) - n - s - origin_desc in + | Annotations.Present -> + "ERADICATE_PARAMETER_VALUE_ABSENT", + P.sprintf + "`%s` needs a present value in parameter %d but argument `%s` can be absent. %s" + (Procname.to_simplified_string pn) + n + s + origin_desc in true, kind_s, description, @@ -492,19 +513,20 @@ let report_error_now (st_report_error : st_report_error) node err_instance loc p | n -> (string_of_int n)^"th" in false, "ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION", - P.sprintf "%s parameter `%s` of method `%s` is not `@Nullable` but is declared `@Nullable` in the parent class method `%s`." + P.sprintf + "%s parameter `%s` of method `%s` is not `@Nullable` but is declared `@Nullable`\ + in the parent class method `%s`." (translate_position pos) param_name (Procname.to_simplified_string ~withclass: true pn) (Procname.to_simplified_string ~withclass: true opn), None, None, - None - in + None in let ew_string = if is_err then "Error" else "Warning" in (if demo_mode then do_print_demo else do_print) ew_string kind_s description; let always_report = Strict.err_instance_get_strict err_instance <> None in st_report_error - proc_name + pname (Cfg.Node.get_proc_desc node) kind_s loc @@ -518,12 +540,12 @@ let report_error_now (st_report_error : st_report_error) node err_instance loc p (** Report an error unless is has been reported already, or unless it's a forall error since it requires waiting until the end of the analysis and be printed by flush. *) -let report_error st_report_error find_canonical_duplicate node - err_instance instr_ref_opt loc proc_name = +let report_error (st_report_error : st_report_error) find_canonical_duplicate node + err_instance instr_ref_opt loc pname_java = let should_report_now = add_err find_canonical_duplicate err_instance instr_ref_opt loc in if should_report_now then - report_error_now st_report_error node err_instance loc proc_name + report_error_now st_report_error node err_instance loc pname_java (** Report the forall checks at the end of the analysis and reset the error table *) let report_forall_checks_and_reset st_report_error proc_name = diff --git a/infer/src/harness/androidFramework.ml b/infer/src/harness/androidFramework.ml index 127bf378d..6a62d269c 100644 --- a/infer/src/harness/androidFramework.ml +++ b/infer/src/harness/androidFramework.ml @@ -23,12 +23,14 @@ let is_known_callback_register_method proc_str = StringSet.mem proc_str callback let on_destroy = "onDestroy" let on_destroy_view = "onDestroyView" -(** return true if [procname] is a special lifecycle cleanup method *) -let is_destroy_method procname = - if Procname.is_java procname then - let method_name = Procname.java_get_method procname in - string_equal method_name on_destroy || string_equal method_name on_destroy_view - else false +(** return true if [pname] is a special lifecycle cleanup method *) +let is_destroy_method pname = + match pname with + | Procname.Java pname_java -> + let method_name = Procname.java_get_method pname_java in + string_equal method_name on_destroy || string_equal method_name on_destroy_view + | _ -> + false let android_lifecycles = let android_content = "android.content" in @@ -314,19 +316,20 @@ let is_android_lib_class class_name = let class_str = Typename.name class_name in string_is_prefix "android" class_str || string_is_prefix "com.android" class_str -(** returns an option containing the var name and type of a callback registered by [procname], None - if no callback is registered *) -let get_callback_registered_by procname args tenv = +(** returns an option containing the var name and type of a callback registered by [procname], + None if no callback is registered *) +let get_callback_registered_by (pname_java : Procname.java) args tenv = (* TODO (t4565077): this check should be replaced with a membership check in a hardcoded list of * Android callback registration methods *) (* for now, we assume a method is a callback registration method if it is a setter and has a * callback class as a non - receiver argument *) let is_callback_register_like = let has_non_this_callback_arg args = IList.length args > 1 in - let has_registery_name procname = - Procname.is_java procname && (PatternMatch.is_setter procname || - is_known_callback_register_method (Procname.java_get_method procname)) in - has_registery_name procname && has_non_this_callback_arg args in + let has_registery_name () = + PatternMatch.is_setter pname_java || + is_known_callback_register_method (Procname.java_get_method pname_java) in + has_registery_name () && + has_non_this_callback_arg args in let is_ptr_to_callback_class typ tenv = match typ with | Sil.Tptr (typ, Sil.Pk_pointer) -> is_callback_class typ tenv | _ -> false in @@ -342,11 +345,17 @@ let get_callback_registered_by procname args tenv = (** return a list of typ's corresponding to callback classes registered by [procdesc] *) let get_callbacks_registered_by_proc procdesc tenv = let collect_callback_typs callback_typs _ instr = match instr with - | Sil.Call([], Sil.Const (Sil.Cfun callee), args, _, _) -> + | Sil.Call ([], Sil.Const (Sil.Cfun callee), args, _, _) -> begin - match get_callback_registered_by callee args tenv with - | Some (_, callback_typ) -> callback_typ :: callback_typs - | None -> callback_typs + match callee with + | Procname.Java callee_java -> + begin + match get_callback_registered_by callee_java args tenv with + | Some (_, callback_typ) -> callback_typ :: callback_typs + | None -> callback_typs + end + | _ -> + callback_typs end | _ -> callback_typs in Cfg.Procdesc.fold_instrs collect_callback_typs [] procdesc @@ -359,7 +368,11 @@ let get_lifecycle_for_framework_typ_opt lifecycle_typ lifecycle_proc_strs tenv = (* TODO (t4645631): collect the procedures for which is_java is returning false *) let lookup_proc lifecycle_proc = IList.find (fun decl_proc -> - Procname.is_java decl_proc && lifecycle_proc = Procname.java_get_method decl_proc + match decl_proc with + | Procname.Java decl_proc_java -> + lifecycle_proc = Procname.java_get_method decl_proc_java + | _ -> + false ) def_methods in (* convert each of the framework lifecycle proc strings to a lifecycle method procname *) let lifecycle_procs = @@ -402,11 +415,3 @@ let is_throwable tenv typename = let non_stub_android_jar () = let root_dir = Filename.dirname (Filename.dirname Sys.executable_name) in IList.fold_left Filename.concat root_dir ["lib"; "java"; "android"; "android-19.jar"] - -(* -(** returns true if [procname] is a method that registers a callback *) -let is_callback_register_method procname args tenv = - match get_callback_registered_by procname args tenv with - | Some _ -> true - | None -> false -*) diff --git a/infer/src/harness/androidFramework.mli b/infer/src/harness/androidFramework.mli index be5f9ab32..6f7e5e309 100644 --- a/infer/src/harness/androidFramework.mli +++ b/infer/src/harness/androidFramework.mli @@ -35,9 +35,10 @@ val is_fragment : Sil.typ -> Sil.tenv -> bool (** return true if [procname] is a special lifecycle cleanup method *) val is_destroy_method : Procname.t -> bool -(** returns an option containing the var name and type of a callback registered by [procname], None - if no callback is registered *) -val get_callback_registered_by : Procname.t -> (Sil.exp * Sil.typ) list -> Sil.tenv -> (Sil.exp * Sil.typ) option +(** returns an option containing the var name and type of a callback registered by [procname], + None if no callback is registered *) +val get_callback_registered_by : + Procname.java -> (Sil.exp * Sil.typ) list -> Sil.tenv -> (Sil.exp * Sil.typ) option (** return a list of typ's corresponding to callback classes registered by [procdesc] *) val get_callbacks_registered_by_proc : Cfg.Procdesc.t -> Sil.tenv -> Sil.typ list diff --git a/infer/src/harness/harness.ml b/infer/src/harness/harness.ml index 8356577b9..10ee694cc 100644 --- a/infer/src/harness/harness.ml +++ b/infer/src/harness/harness.ml @@ -55,9 +55,13 @@ let extract_callbacks procdesc cfg_file cfg tenv harness_lvar callback_fields = else typ_str in Mangled.from_string (pretty_typ_str ^ "[line " ^ Location.to_string loc ^ "]") in let create_instrumentation_fields created_flds node instr = match instr with - | Sil.Call([], Sil.Const (Sil.Cfun callee), args, loc, _) -> + | Sil.Call ([], Sil.Const (Sil.Cfun callee), args, loc, _) + when Procname.is_java callee -> + let callee_java = match callee with + | Procname.Java callee_java -> callee_java + | _ -> assert false in begin - match AndroidFramework.get_callback_registered_by callee args tenv with + match AndroidFramework.get_callback_registered_by callee_java args tenv with | Some (cb_obj, (Sil.Tptr (cb_typ, Sil.Pk_pointer) as ptr_to_cb_typ)) -> let callback_fld_name = create_descriptive_callback_name ptr_to_cb_typ loc in let created_fld = Ident.create_fieldname callback_fld_name generated_field_offset in @@ -79,7 +83,8 @@ let extract_callbacks procdesc cfg_file cfg tenv harness_lvar callback_fields = (created_fld, ptr_to_cb_typ, mk_field_write) :: created_flds | _ -> created_flds end - | _ -> created_flds in + | _ -> + created_flds in Cfg.Procdesc.fold_instrs create_instrumentation_fields callback_fields procdesc (** find all of the callbacks registered by methods in [lifecycle_trace *) @@ -135,7 +140,8 @@ let try_create_lifecycle_trace typ lifecycle_typ lifecycle_procs tenv = match ty global static fields belong to the harness so that they are easily callable, and return a list of the (field, typ) pairs that we have created for this purpose *) let extract_callbacks lifecycle_trace harness_procname proc_file_map tenv = - let harness_name = Mangled.from_string (Procname.to_string harness_procname) in + let harness_name = + Mangled.from_string (Procname.to_string (Procname.Java harness_procname)) in let registered_cbs = find_registered_callbacks lifecycle_trace harness_name proc_file_map tenv in let fields = IList.map (fun (fld, typ, _) -> (fld, typ, [])) registered_cbs in @@ -147,7 +153,7 @@ let extract_callbacks lifecycle_trace harness_procname proc_file_map tenv = csu = Csu.Class Csu.Java; struct_name = Some harness_name; superclasses = []; - def_methods = [harness_procname]; + def_methods = [Procname.Java harness_procname]; struct_annotations = []; } in let harness_typ = Sil.Tstruct harness_struct_typ in @@ -186,7 +192,14 @@ let create_android_harness proc_file_map tenv = * inhabitation module to create a harness for us *) let harness_procname = let harness_cls_name = PatternMatch.get_type_name typ in - Procname.mangled_java (None, harness_cls_name) None "InferGeneratedHarness" [] Procname.Static in + let pname = + Procname.Java + (Procname.java + (None, harness_cls_name) None + "InferGeneratedHarness" [] Procname.Static) in + match pname with + | Procname.Java harness_procname -> harness_procname + | _ -> assert false in let callback_fields = extract_callbacks lifecycle_trace harness_procname proc_file_map tenv in Inhabit.inhabit_trace diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index f5d7fca77..8db6d268c 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -28,7 +28,7 @@ type env = { instrs : Sil.instr list; (* set of types currently being inhabited. consult to prevent infinite recursion *) cur_inhabiting : TypSet.t; pc : Location.t; - harness_name : Procname.t } + harness_name : Procname.java } (** add an instruction to the env, update tmp_vars, and bump the pc *) let env_add_instr instr tmp_vars env = @@ -125,14 +125,18 @@ let rec inhabit_typ typ proc_file_map env = (* try to get the unqualified name as a class (e.g., Object for java.lang.Object so we * we can use it as a descriptive local variable name in the harness *) let typ_class_name = - if Procname.is_java constructor then Procname.java_get_simple_class constructor - else create_fresh_local_name () in + match constructor with + | Procname.Java pname_java -> + Procname.java_get_simple_class pname_java + | _ -> + create_fresh_local_name () in (env, Mangled.from_string typ_class_name) | [] -> (env, Mangled.from_string (create_fresh_local_name ())) in (* add the instructions *& local = [allocated_obj_exp]; id = *& local, where local and id are * both fresh. the only point of this is to add a descriptive local name that makes error * reports from the harness look nicer -- it's not necessary to make symbolic execution work *) - let fresh_local_exp = Sil.Lvar (Sil.mk_pvar typ_class_name env.harness_name) in + let fresh_local_exp = + Sil.Lvar (Sil.mk_pvar typ_class_name (Procname.Java env.harness_name)) in let write_to_local_instr = Sil.Set (fresh_local_exp, ptr_to_typ, allocated_obj_exp, env.pc) in let env' = env_add_instr write_to_local_instr [] env in @@ -249,8 +253,10 @@ let write_harness_to_file harness_instrs harness_file = (** add the harness proc to the cg and make sure its callees can be looked up by sym execution *) let add_harness_to_cg harness_name harness_node cg = - Cg.add_defined_node cg harness_name; - IList.iter (fun p -> Cg.add_edge cg harness_name p) (Cfg.Node.get_callees harness_node) + Cg.add_defined_node cg (Procname.Java harness_name); + IList.iter + (fun p -> Cg.add_edge cg (Procname.Java harness_name) p) + (Cfg.Node.get_callees harness_node) (** create and fill the appropriate nodes and add them to the harness cfg. also add the harness * proc to the cg *) @@ -265,7 +271,7 @@ let setup_harness_cfg harness_name env source_dir cg = let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in let procdesc = let proc_attributes = - { (ProcAttributes.default harness_name Config.Java) with + { (ProcAttributes.default (Procname.Java harness_name) Config.Java) with ProcAttributes.is_defined = true; loc = env.pc; } in diff --git a/infer/src/harness/inhabit.mli b/infer/src/harness/inhabit.mli index ecf505e70..fc8ab3d97 100644 --- a/infer/src/harness/inhabit.mli +++ b/infer/src/harness/inhabit.mli @@ -15,7 +15,7 @@ type callback_trace = (Sil.exp * Sil.typ) list (** create a procedure named harness_name that calls each of the methods in trace in the specified order with the specified receiver and add it to the execution environment *) -val inhabit_trace : lifecycle_trace -> callback_trace -> Procname.t -> +val inhabit_trace : lifecycle_trace -> callback_trace -> Procname.java -> DB.source_file Procname.Map.t -> unit val source_dir_from_name : Procname.t -> DB.source_file Procname.Map.t -> DB.source_dir diff --git a/infer/src/java/jAnnotation.ml b/infer/src/java/jAnnotation.ml index 4b32888e4..806925b16 100644 --- a/infer/src/java/jAnnotation.ml +++ b/infer/src/java/jAnnotation.ml @@ -57,12 +57,12 @@ let translate_item avlist : Sil.item_annotation = (** Translate a method annotation. *) -let translate_method proc_name ann : Sil.method_annotation = +let translate_method proc_name_java ann : Sil.method_annotation = let global_ann = ann.Javalib.ma_global in let param_ann = ann.Javalib.ma_parameters in let ret_item = let base_annotations = translate_item global_ann in - if is_suppress_warnings_annotated proc_name then + if is_suppress_warnings_annotated (Procname.Java proc_name_java) then suppress_warnings :: base_annotations else base_annotations in let param_items = IList.map translate_item param_ann in diff --git a/infer/src/java/jAnnotation.mli b/infer/src/java/jAnnotation.mli index 0853e9072..be5f1eb5d 100644 --- a/infer/src/java/jAnnotation.mli +++ b/infer/src/java/jAnnotation.mli @@ -15,4 +15,4 @@ open Javalib_pack val translate_item : (JBasics.annotation * Javalib.visibility) list -> Sil.item_annotation (** Translate a method annotation. *) -val translate_method : Procname.t -> Javalib.method_annotations -> Sil.method_annotation +val translate_method : Procname.java -> Javalib.method_annotations -> Sil.method_annotation diff --git a/infer/src/java/jContext.mli b/infer/src/java/jContext.mli index 5cf1970cc..f1178fa12 100644 --- a/infer/src/java/jContext.mli +++ b/infer/src/java/jContext.mli @@ -118,7 +118,7 @@ val reset_pvar_type : t -> unit val reset_exn_node_table : unit -> unit (** adds the exception node for a given method *) -val add_exn_node : Procname.Hash.key -> Cfg.Node.t -> unit +val add_exn_node : Procname.t -> Cfg.Node.t -> unit (** returns the exception node of a given method *) val get_exn_node : Cfg.Procdesc.t -> Cfg.Node.t option diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index f0fe3e7aa..6b5c137aa 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -28,12 +28,13 @@ let init_loc_map : Location.t JBasics.ClassMap.t ref = ref JBasics.ClassMap.empt (** Fix the line associated to a method definition. Since Sawja often reports a method off by a few lines, we search backwards for a line where the method name is. *) -let fix_method_definition_line linereader proc_name loc = +let fix_method_definition_line linereader proc_name_java loc = + let proc_name = Procname.Java proc_name_java in let method_name = if Procname.is_constructor proc_name then let inner_class_name cname = snd (string_split_character cname '$') in - inner_class_name (Procname.java_get_simple_class proc_name) - else Procname.java_get_method proc_name in + inner_class_name (Procname.java_get_simple_class proc_name_java) + else Procname.java_get_method proc_name_java in let regex = Str.regexp (Str.quote method_name) in let method_is_defined_here linenum = match Printer.LineReader.from_file_linenum_original linereader loc.Location.file linenum with @@ -265,7 +266,8 @@ let create_local_procdesc program linereader cfg tenv node m = meth_kind = JContext.Init && not (JTransStaticField.has_static_final_fields node)) then - let proc_name = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in + let proc_name_java = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in + let proc_name = Procname.Java proc_name_java in let create_new_procdesc () = let trans_access = function | `Default -> Sil.Default @@ -278,7 +280,7 @@ let create_local_procdesc program linereader cfg tenv node m = let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in let method_annotation = - JAnnotation.translate_method proc_name am.Javalib.am_annotations in + JAnnotation.translate_method proc_name_java am.Javalib.am_annotations in let procdesc = let proc_attributes = { (ProcAttributes.default proc_name Config.Java) with @@ -303,7 +305,7 @@ let create_local_procdesc program linereader cfg tenv node m = | Javalib.ConcreteMethod cm when is_java_native cm -> let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in let method_annotation = - JAnnotation.translate_method proc_name cm.Javalib.cm_annotations in + JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in let proc_attributes = { (ProcAttributes.default proc_name Config.Java) with ProcAttributes.access = trans_access cm.Javalib.cm_access; @@ -320,10 +322,10 @@ let create_local_procdesc program linereader cfg tenv node m = let locals, formals = locals_formals program tenv cn impl meth_kind in let loc_start = let loc = (get_location impl 0 JContext.Normal cn) in - fix_method_definition_line linereader proc_name loc in + fix_method_definition_line linereader proc_name_java loc in let loc_exit = (get_location impl (Array.length (JBir.code impl) - 1) JContext.Normal cn) in let method_annotation = - JAnnotation.translate_method proc_name cm.Javalib.cm_annotations in + JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in update_constr_loc cn ms loc_start; update_init_loc cn ms loc_exit; let procdesc = @@ -354,7 +356,8 @@ let create_local_procdesc program linereader cfg tenv node m = with JBir.Subroutine -> L.err "create_local_procdesc raised JBir.Subroutine on %a@." Procname.pp proc_name in match lookup_procdesc cfg proc_name with - | Unknown -> create_new_procdesc () + | Unknown -> + create_new_procdesc () | Created defined_status -> begin match defined_status with @@ -370,10 +373,10 @@ let create_external_procdesc program cfg tenv cn ms kind = | None -> Sil.Tvoid | Some vt -> JTransType.value_type program tenv vt in let formals = formals_from_signature program tenv cn ms kind in - let proc_name = JTransType.get_method_procname cn ms kind in + let proc_name_java = JTransType.get_method_procname cn ms kind in ignore ( let proc_attributes = - { (ProcAttributes.default proc_name Config.Java) with + { (ProcAttributes.default (Procname.Java proc_name_java) Config.Java) with ProcAttributes.formals; ret_type = return_type; } in @@ -381,8 +384,8 @@ let create_external_procdesc program cfg tenv cn ms kind = (** returns the procedure description of the given method and creates it if it hasn't been created before *) let rec get_method_procdesc program cfg tenv cn ms kind = - let procname = JTransType.get_method_procname cn ms kind in - match lookup_procdesc cfg procname with + let procname_java = JTransType.get_method_procname cn ms kind in + match lookup_procdesc cfg (Procname.Java procname_java) with | Unknown -> create_external_procdesc program cfg tenv cn ms kind; get_method_procdesc program cfg tenv cn ms kind @@ -588,8 +591,10 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_ expr_list in let callee_procname = let proc = Procname.from_string_c_fun (JBasics.ms_name ms) in - if JBasics.cn_equal cn' JConfig.infer_builtins_cl && SymExec.function_is_builtin proc then proc - else JTransType.get_method_procname cn' ms method_kind in + if JBasics.cn_equal cn' JConfig.infer_builtins_cl && + SymExec.function_is_builtin proc + then proc + else Procname.Java (JTransType.get_method_procname cn' ms method_kind) in let call_idl, call_instrs = let callee_fun = Sil.Const (Sil.Cfun callee_procname) in let return_type = @@ -787,8 +792,11 @@ let rec instruction context pc instr : translation = Cfg.Node.create cfg (get_location (JContext.get_impl context) pc meth_kind cn) node_kind sil_instrs (JContext.get_procdesc context) temps in let return_not_null () = - (match_never_null loc.Location.file proc_name - || IList.exists (fun p -> Procname.equal p proc_name) JTransType.never_returning_null) in + match_never_null loc.Location.file proc_name + || + IList.exists + (fun pnj -> Procname.equal (Procname.Java pnj) proc_name) + JTransType.never_returning_null in let trans_monitor_enter_exit context expr pc loc builtin node_desc = let ids, instrs, sil_expr, sil_type = expression context pc expr in let builtin_const = Sil.Const (Sil.Cfun builtin) in diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 5cc115b8a..08d7e024a 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -193,7 +193,7 @@ let get_method_kind m = if Javalib.is_static_method m then Procname.Static else let get_method_procname cn ms kind = let return_type_name, method_name, args_type_name = method_signature_names ms in let class_name = cn_to_java_type cn in - Procname.mangled_java class_name return_type_name method_name args_type_name kind + Procname.java class_name return_type_name method_name args_type_name kind let get_class_procnames cn node = let collect jmethod procnames = @@ -338,7 +338,7 @@ and create_sil_type program tenv cn = super_classname :: interface_list in (super_classname_list, nonstatic_fields, static_fields, item_annotation) in let classname = Mangled.from_string (JBasics.cn_name cn) in - let def_methods = get_class_procnames cn node in + let def_methods = IList.map (fun j -> Procname.Java j) (get_class_procnames cn node) in Sil.Tstruct { Sil.instance_fields; static_fields; diff --git a/infer/src/java/jTransType.mli b/infer/src/java/jTransType.mli index 078bf5fe5..0d9037266 100644 --- a/infer/src/java/jTransType.mli +++ b/infer/src/java/jTransType.mli @@ -23,8 +23,8 @@ val create_fieldname : JBasics.class_name -> JBasics.field_signature -> Ident.fi val get_method_kind : JCode.jcode Javalib.jmethod -> Procname.method_kind (** returns a procedure name based on the class name and the method's signature. *) -val get_method_procname : JBasics.class_name -> JBasics.method_signature -> Procname.method_kind -> - Procname.t +val get_method_procname : + JBasics.class_name -> JBasics.method_signature -> Procname.method_kind -> Procname.java (** [get_class_type_no_pointer program tenv cn] returns the sil type representation of the class without the pointer part *) @@ -90,4 +90,4 @@ val cn_to_java_type : JBasics.class_name -> Procname.java_type val add_models_types : Sil.tenv -> unit (** list of methods that are never returning null *) -val never_returning_null : Procname.t list +val never_returning_null : Procname.java list