From bf0fa55a4595679da72682d5ee217ecbca93dfc7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= <ezgi@fb.com>
Date: Fri, 19 Mar 2021 10:19:12 -0700
Subject: [PATCH] [immutability] Add support for modifications to Litho's
 Immutable Maps

Reviewed By: skcho

Differential Revision: D27008496

fbshipit-source-id: b4f4198b6
---
 Makefile                                      |  1 +
 infer/src/checkers/impurity.ml                |  2 +-
 infer/src/checkers/impurityDomain.ml          | 27 ++++++++++++-------
 .../java/fb-immutability/.inferconfig         |  1 +
 .../java/fb-immutability/Makefile             | 15 +++++++++++
 5 files changed, 36 insertions(+), 10 deletions(-)
 create mode 100644 infer/tests/codetoanalyze/java/fb-immutability/.inferconfig
 create mode 100644 infer/tests/codetoanalyze/java/fb-immutability/Makefile

diff --git a/Makefile b/Makefile
index 466ea8682..476f3e322 100644
--- a/Makefile
+++ b/Makefile
@@ -196,6 +196,7 @@ COST_TESTS += java_fb-performance
 DIRECT_TESTS += \
   java_fb-config-impact \
   java_fb-gk-interaction \
+  java_fb-immutability \
   java_fb-performance
 endif
 
diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml
index 1b2352080..3f2c24849 100644
--- a/infer/src/checkers/impurity.ml
+++ b/infer/src/checkers/impurity.ml
@@ -129,7 +129,7 @@ let get_modified_params pname post_stack pre_heap post formals =
             BaseMemory.Edges.fold edges_pre ~init:acc ~f:(fun acc (access, (addr, _)) ->
                 add_to_modified pname ~pvar ~access ~addr pre_heap post acc )
         | None ->
-            debug "The address is not materialized in in pre-heap." ;
+            debug "The address %a is not materialized in pre-heap.\n" AbstractValue.pp addr ;
             acc )
       | _ ->
           acc )
diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml
index 6ab4c743d..dda198c49 100644
--- a/infer/src/checkers/impurityDomain.ml
+++ b/infer/src/checkers/impurityDomain.ml
@@ -50,21 +50,30 @@ let pure =
   ; exited= Exited.bottom }
 
 
+let implements_immutable_map tenv = function
+  | Typ.JavaClass java_class_name ->
+      JavaClassName.to_string java_class_name
+      |> PatternMatch.Java.implements_xmob_utils "ImmutableIntHashMap" tenv
+  | _ ->
+      false
+
+
 let filter_modifies_immutable tenv ~f =
   ModifiedVarMap.filter (fun _pvar ModifiedAccess.{ordered_access_list} ->
       List.exists ordered_access_list ~f:(fun access ->
           match access with
           | HilExp.Access.FieldAccess fname ->
               let class_name = Fieldname.get_class_name fname in
-              Tenv.lookup tenv class_name
-              |> Option.exists ~f:(fun mstruct ->
-                     f mstruct
-                     |> List.exists ~f:(fun (fieldname, _typ, annot) ->
-                            String.equal
-                              (Fieldname.get_field_name fieldname)
-                              (Fieldname.get_field_name fname)
-                            && Annotations.ia_has_annotation_with annot (fun annot ->
-                                   Annotations.annot_ends_with annot Annotations.immutable ) ) )
+              implements_immutable_map tenv class_name
+              || Tenv.lookup tenv class_name
+                 |> Option.exists ~f:(fun mstruct ->
+                        f mstruct
+                        |> List.exists ~f:(fun (fieldname, _typ, annot) ->
+                               String.equal
+                                 (Fieldname.get_field_name fieldname)
+                                 (Fieldname.get_field_name fname)
+                               && Annotations.ia_has_annotation_with annot (fun annot ->
+                                      Annotations.annot_ends_with annot Annotations.immutable ) ) )
           | _ ->
               false ) )
 
diff --git a/infer/tests/codetoanalyze/java/fb-immutability/.inferconfig b/infer/tests/codetoanalyze/java/fb-immutability/.inferconfig
new file mode 100644
index 000000000..5202d3bca
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/fb-immutability/.inferconfig
@@ -0,0 +1 @@
+{"pulse-model-return-first-arg": ".*ImmutableIntHashMap.duplicate\\(\\)\\|.*IntHashMap.moveToImmutable\\(\\)"}
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/fb-immutability/Makefile b/infer/tests/codetoanalyze/java/fb-immutability/Makefile
new file mode 100644
index 000000000..e73badb3f
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/fb-immutability/Makefile
@@ -0,0 +1,15 @@
+# Copyright (c) Facebook, Inc. and its affiliates.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+
+TESTS_DIR = ../../..
+
+ANALYZER = checkers
+INFER_OPTIONS = --impurity-only --report-immutable-modifications --disable-issue-type IMPURE_FUNCTION \
+  --disable-issue-type NULLPTR_DEREFERENCE --report-force-relative-path
+
+INFERPRINT_OPTIONS = --issues-tests
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make