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