Prevent assert false from occurring on Java functions in Procname.

Summary:public
Assert false have been observed in Procname when analyzing some C projects.
This diff changes the Procname API to make it safe for Java: the java functions in the module don't assert false now. This takes care of the errors observed in C projects.
The new API forces changes throughout the codebase. In particular, the constant propagation module was making assumptions that it would only be executed on Java code, triggering assert false on C. Now it is safe.
For the remaining functions in the Procname module, those for other languages, a special assert false in Utils is used to print stack traces. This is for future debugging.

Reviewed By: sblackshear

Differential Revision: D3054077

fb-gh-sync-id: a77f1d7
shipit-source-id: a77f1d7
master
Cristiano Calcagno 9 years ago committed by Facebook Github Bot 2
parent 4384870b44
commit 86304b3d9c

@ -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

@ -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 =

@ -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

@ -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] }

@ -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

@ -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 *)

@ -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 = "<init>" 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 = "<init>"
| ObjC_Cpp_method name ->
| Java js -> js.method_name = "<init>"
| 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 = "<clinit>"
| Java js -> js.method_name = "<clinit>"
| _ -> 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

@ -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

@ -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

@ -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 "<init>" [(Some "java.lang"), "String"] Procname.Non_Static in
let url_pname =
Procname.Java
(Procname.java
((Some "java.net"), "URL") None "<init>"
[(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) ->

@ -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 =

@ -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))

@ -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

@ -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
| _ ->
()

@ -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

@ -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 ()

@ -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 = "<init>" -> (* StringBuilder.<init> *)
when has_class pn "java.lang.StringBuilder"
&& has_method pn "<init>" -> (* StringBuilder.<init> *)
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

@ -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
| _ ->
()

@ -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 =

@ -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 :

@ -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 =

@ -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

@ -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

@ -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

@ -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

@ -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 =

@ -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
*)

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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;

@ -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

Loading…
Cancel
Save