diff --git a/infer/src/backend/procname.ml b/infer/src/backend/procname.ml index 86dd55003..8c45db973 100644 --- a/infer/src/backend/procname.ml +++ b/infer/src/backend/procname.ml @@ -234,13 +234,18 @@ let java_get_method = function | _ -> assert false (** Replace the method of a java procname. *) -let java_replace_method p mname = match p with - | Java_method p -> Java_method { p with method_name = mname } +let java_replace_method j mname = match j with + | Java_method j -> Java_method { j with method_name = mname } | _ -> assert false (** Replace the return type of a java procname. *) let java_replace_return_type p ret_type = match p with - | Java_method p -> Java_method { p with return_type = Some ret_type } + | Java_method j -> Java_method { j with return_type = Some ret_type } + | _ -> assert false + +(** 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 (** Return the method of a objc/c++ procname. *) @@ -257,6 +262,11 @@ let java_get_return_type = function (** Return the parameters of a java procname. *) let java_get_parameters = function + | Java_method j -> j.parameters + | _ -> assert false + +(** Return the parameters of a java procname as strings. *) +let java_get_parameters_as_strings = function | Java_method j -> IList.map (fun param -> java_type_to_string param Verbose) j.parameters | _ -> assert false diff --git a/infer/src/backend/procname.mli b/infer/src/backend/procname.mli index c5a3af8fc..40f73ad90 100644 --- a/infer/src/backend/procname.mli +++ b/infer/src/backend/procname.mli @@ -66,6 +66,9 @@ val java_replace_class : t -> string -> t (** Replace the method of a java procname. *) val java_replace_method : t -> string -> t +(** Replace the parameters of a java procname. *) +val java_replace_parameters : t -> java_type list -> t + (** Replace the method of a java procname. *) val java_replace_return_type : t -> java_type -> t @@ -97,7 +100,10 @@ val java_replace_method : t -> string -> t val java_get_return_type : t -> string (** Return the parameters of a java procedure name. *) -val java_get_parameters : t -> string list +val java_get_parameters : t -> java_type list + +(** Return the parameters of a java procname as strings. *) +val java_get_parameters_as_strings : t -> string list (** Return true if the java procedure is static *) val java_is_static : t -> bool diff --git a/infer/src/checkers/modelTables.ml b/infer/src/checkers/modelTables.ml index 9f34d22bb..51f005b85 100644 --- a/infer/src/checkers/modelTables.ml +++ b/infer/src/checkers/modelTables.ml @@ -103,6 +103,13 @@ let containsKey_list = n1, "java.util.Map.containsKey(java.lang.Object):boolean"; ] +(** Models for Map.put *) +let mapPut_list = + [ + cp, "com.google.common.collect.ImmutableMap.put(java.lang.Object,java.lang.Object):java.lang.Object"; + cp, "java.util.Map.put(java.lang.Object,java.lang.Object):java.lang.Object"; + ] + (** Models for @Strict annotations *) let annotated_list_strict = [ @@ -237,6 +244,7 @@ let check_not_null_table, check_not_null_parameter_table = let check_state_table = mk_table check_state_list let check_argument_table = mk_table check_argument_list let containsKey_table = mk_table containsKey_list +let mapPut_table = mk_table mapPut_list let optional_get_table = mk_table optional_get_list let optional_isPresent_table = mk_table optional_isPresent_list let true_on_null_table = mk_table true_on_null_list diff --git a/infer/src/checkers/modelTables.mli b/infer/src/checkers/modelTables.mli index 8be6008f1..26a8976cd 100644 --- a/infer/src/checkers/modelTables.mli +++ b/infer/src/checkers/modelTables.mli @@ -22,6 +22,7 @@ val check_not_null_parameter_table : (string, int) Hashtbl.t val check_state_table : model_table_t val check_argument_table : model_table_t val containsKey_table : model_table_t +val mapPut_table : model_table_t val optional_get_table : model_table_t val optional_isPresent_table : model_table_t val true_on_null_table : model_table_t diff --git a/infer/src/checkers/models.ml b/infer/src/checkers/models.ml index af2c714ba..4d1049a52 100644 --- a/infer/src/checkers/models.ml +++ b/infer/src/checkers/models.ml @@ -193,3 +193,7 @@ let is_true_on_null proc_name = (** Check if the procedure is Map.containsKey(). *) let is_containsKey proc_name = table_has_procedure containsKey_table proc_name + +(** Check if the procedure is Map.put(). *) +let is_mapPut proc_name = + table_has_procedure mapPut_table proc_name diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index 70d23d7ce..8c4ca2aa7 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -722,6 +722,45 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc end | _ -> typestate' in + (** Handle m.put(k,v) as assignment pvar = v for the pvar associated to m.get(k) *) + let do_map_put typestate' = + (* Get the proc name for map.get() from map.put() *) + let pname_get_from_pname_put pname_put = + let object_t = (Some "java.lang", "Object") in + let parameters = [object_t] in + Procname.java_replace_parameters + (Procname.java_replace_return_type + (Procname.java_replace_method pname_put "get") + object_t) + parameters in + match call_params with + | ((_, Sil.Lvar pv_map), typ_map) :: + ((_, exp_key), typ_key) :: + ((_, exp_value), typ_value) :: _ -> + (* Convert the dexp for k to the dexp for m.get(k) *) + let convert_dexp_key_to_dexp_get = function + | Some dexp_key -> + let pname_get = pname_get_from_pname_put callee_pname in + let dexp_get = Sil.Dconst (Sil.Cfun pname_get) in + let dexp_map = Sil.Dpvar pv_map in + let args = [dexp_map; dexp_key] in + let call_flags = { Sil.cf_default with Sil.cf_virtual = true } in + Some (Sil.Dretcall (dexp_get, args, loc, call_flags)) + | _ -> None in + begin + match ComplexExpressions.exp_to_string_map_dexp + convert_dexp_key_to_dexp_get node exp_key with + | Some map_get_str -> + let pvar_map_get = Sil.mk_pvar (Mangled.from_string map_get_str) curr_pname in + TypeState.add_pvar + pvar_map_get + (typecheck_expr_simple typestate' exp_value typ_value TypeOrigin.Undef loc) + typestate' + | None -> + typestate' + end + | _ -> + typestate' in let typestate2 = if not is_anonymous_inner_class_constructor then @@ -777,7 +816,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc typestate2 else if Procname.java_get_method callee_pname = "checkNotNull" - && Procname.java_is_vararg callee_pname + && Procname.java_is_vararg callee_pname then let last_parameter = IList.length call_params in do_preconditions_check_not_null @@ -787,6 +826,8 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc else if Models.is_check_state callee_pname || Models.is_check_argument callee_pname then do_preconditions_check_state typestate2 + else if Models.is_mapPut callee_pname then + do_map_put typestate2 else typestate2 end else typestate1 in diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 9f5bc46ee..2195993a0 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -274,7 +274,7 @@ let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv = | None -> failwith ("Failed to look up typ " ^ typ_str) in let ret_type = lookup_typ (Procname.java_get_return_type proc_name) in let formals = - let param_strs = Procname.java_get_parameters proc_name in + let param_strs = Procname.java_get_parameters_as_strings proc_name in IList.fold_right (fun typ_str params -> ("", lookup_typ typ_str) :: params) param_strs [] in let proc_attributes = { (ProcAttributes.default proc_name Config.Java) with diff --git a/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java b/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java index d25b7a91d..5f14cfd8e 100644 --- a/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java +++ b/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java @@ -364,6 +364,29 @@ class NestedFieldAccess { } } + // Test Map.put() + class TestPut { + String dontAssignNull = ""; + + public void putConstString(java.util.Map map, String key) { + map.put(key, "abc"); + dontAssignNull = map.get(key); + } + + public void putNull(java.util.Map map, String key) { + map.put(key, "abc"); + map.put(key, null); + dontAssignNull = map.get(key); + } + + public void putWithContainsKey(java.util.Map map, String key) { + if (!map.containsKey(key)) { + map.put(key, "abc"); + } + dontAssignNull= map.get(key); + } + } + // support assignments of null to @InjectView fields, generated by butterknife class SupportButterKnife { @InjectView String s; diff --git a/infer/tests/endtoend/java/eradicate/FieldNotNullableTest.java b/infer/tests/endtoend/java/eradicate/FieldNotNullableTest.java index ca79986ae..d80e4c880 100644 --- a/infer/tests/endtoend/java/eradicate/FieldNotNullableTest.java +++ b/infer/tests/endtoend/java/eradicate/FieldNotNullableTest.java @@ -48,6 +48,7 @@ public class FieldNotNullableTest { "NestedBAD1", "NestedBAD2", "NestedBAD3", + "putNull", }; assertThat( "Results should contain " + FIELD_NOT_NULLABLE,