Model Map.put() alongside Map.containsKey().

Summary:
public

Added special modelling for m.put(k,v) as assigning value v to map m at key k.
The modelling is analogous to the one for containsKey: the variable used to represent m.get(k) is generated, and assigned the value v.

Reviewed By: jberdine

Differential Revision: D2743844

fb-gh-sync-id: 56d3581

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
 

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

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

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

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

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

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

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<String, String> map, String key) {
+      map.put(key, "abc");
+      dontAssignNull = map.get(key);
+    }
+
+    public void putNull(java.util.Map<String, String> map, String key) {
+      map.put(key, "abc");
+      map.put(key, null);
+      dontAssignNull = map.get(key);
+    }
+
+    public void putWithContainsKey(java.util.Map<String, String> 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;

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,