[thread-safety] model certain methods of Resources as @Functional

Summary: Should stop us from reporting on benign races of fields that are caching resources.

Reviewed By: peterogithub

Differential Revision: D4538037

fbshipit-source-id: 15236b4

infer/src/checkers/ThreadSafety.ml

@@ -191,14 +191,37 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Some rhs_access_path -> IdAccessPathMapDomain.add lhs_id rhs_access_path id_map
     | None -> id_map
 
-  (* like PatternMatch.override_exists, but also applies [predicate] to [pname] *)
+  let is_functional pname tenv =
-  let proc_or_override_is_annotated pname tenv predicate =
+    let proc_is_functional pn =
-    let has_return_annot pn =
+      let is_annotated_functional pn =
-      Annotations.pname_has_return_annot
+        Annotations.pname_has_return_annot
-        pn
+          pn
-        ~attrs_of_pname:Specs.proc_resolve_attributes
+          ~attrs_of_pname:Specs.proc_resolve_attributes
-        predicate in
+          Annotations.ia_is_functional in
-    has_return_annot pname || PatternMatch.override_exists has_return_annot tenv pname
+      let is_modeled_functional = function
+        | Procname.Java java_pname ->
+            begin
+              match Procname.java_get_class_name java_pname,
+                    Procname.java_get_method java_pname with
+              | "android.content.res.Resources", method_name ->
+                  (* all methods of Resources are considered @Functional except for the ones in this
+                     blacklist *)
+                  let non_functional_resource_methods = [
+                    "getAssets";
+                    "getConfiguration";
+                    "getSystem";
+                    "newTheme";
+                    "openRawResource";
+                    "openRawResourceFd"
+                  ] in
+                  not (List.mem non_functional_resource_methods method_name)
+              | _ ->
+                  false
+            end
+        | _ ->
+            false in
+      is_annotated_functional pn || is_modeled_functional pn in
+    proc_is_functional pname || PatternMatch.override_exists proc_is_functional tenv pname
 
   let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; extras; } _ =
     let is_allocation pn =
@@ -441,8 +464,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               (* writes to longs and doubles are not guaranteed to be atomic in Java, so don't
                  bother tracking whether a returned long or float value is functional *)
               astate_callee
-          | Some (ret_id, ret_typ) when
+          | Some (ret_id, ret_typ) when is_functional callee_pname tenv ->
-              proc_or_override_is_annotated callee_pname tenv Annotations.ia_is_functional ->
               let attribute_map =
                 AttributeMapDomain.add_attribute
                   (AccessPath.of_id ret_id ret_typ) Functional astate.attribute_map in

infer/tests/codetoanalyze/java/threadsafety/AndroidModels.java

@@ -0,0 +1,51 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package codetoanalyze.java.checkers;
+
+import javax.annotation.concurrent.ThreadSafe;
+
+import android.content.res.AssetManager;
+import android.content.res.Configuration;
+import android.content.res.Resources;
+import android.util.DisplayMetrics;
+
+class MyResources extends Resources {
+
+  public MyResources(AssetManager assets, DisplayMetrics metrics, Configuration config) {
+    super(assets, metrics, config);
+  }
+
+}
+
+@ThreadSafe
+public class AndroidModels {
+
+  Resources mResources;
+  MyResources mMyResources;
+
+  Object mField;
+
+  // assume that some Resources methods are annotated with @Functional
+  public void resourceMethodFunctionalOk() {
+    mField = mResources.getString(0);
+  }
+
+  // and subclasses of Resources too
+  public void customResourceMethodFunctionalOk() {
+    mField = mResources.getString(0);
+  }
+
+  // but not all of them
+  public void someResourceMethodsNotFunctionalBad() {
+    // configuration can change whenever the device rotates
+    mField = mResources.getConfiguration();
+  }
+
+}

infer/tests/codetoanalyze/java/threadsafety/issues.exp

@@ -1,3 +1,4 @@
+codetoanalyze/java/threadsafety/AndroidModels.java, void AndroidModels.someResourceMethodsNotFunctionalBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.AndroidModels.mField]
 codetoanalyze/java/threadsafety/Annotations.java, boolean Annotations.FP_functionalAcrossUnboxingOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBool]
 codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalDoubleBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mDouble]
 codetoanalyze/java/threadsafety/Annotations.java, long Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBoxedLong]