[thread-safety] Add @ReturnsOwnership annotation for methods and handle it in the thread-safety analysis

Reviewed By: jeremydubreil

Differential Revision: D4538654

fbshipit-source-id: e5889ac

infer/annotations/com/facebook/infer/annotation/ReturnsOwnership.java

@@ -0,0 +1,26 @@
+/*
+ * 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 com.facebook.infer.annotation;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Tell the thread-safety analysis that this method transfers ownership of its return value to its
+ * caller. Ownership means that the caller is allowed to both read and write the value outside of
+ * synchronization. The annotated method should not retain any references to the value.
+ * This annotation is trusted for now, but may be checked eventually.
+ */
+@Target(ElementType.METHOD)
+@Retention(RetentionPolicy.CLASS)
+public @interface ReturnsOwnership {
+}

infer/src/checkers/ThreadSafety.ml

@@ -189,37 +189,42 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Some rhs_access_path -> IdAccessPathMapDomain.add lhs_id rhs_access_path id_map
     | None -> id_map
 
-  let is_functional pname tenv =
+  let has_return_annot predicate pn =
-    let proc_is_functional pn =
+    Annotations.pname_has_return_annot
-      let is_annotated_functional pn =
+      pn
-        Annotations.pname_has_return_annot
+      ~attrs_of_pname:Specs.proc_resolve_attributes
-          pn
+      predicate
-          ~attrs_of_pname:Specs.proc_resolve_attributes
+
-          Annotations.ia_is_functional in
+  (* like PatternMatch.override_exists, but also applies [predicate] to [pname] *)
-      let is_modeled_functional = function
+  let proc_or_override_exists pname tenv (predicate : Procname.t -> bool) =
-        | Procname.Java java_pname ->
+    predicate pname || PatternMatch.override_exists predicate tenv pname
-            begin
+
-              match Procname.java_get_class_name java_pname,
+  let is_functional pname =
-                    Procname.java_get_method java_pname with
+    let is_annotated_functional =
-              | "android.content.res.Resources", method_name ->
+      has_return_annot Annotations.ia_is_functional in
-                  (* all methods of Resources are considered @Functional except for the ones in this
+    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 = [
+                let non_functional_resource_methods = [
-                    "getAssets";
+                  "getAssets";
-                    "getConfiguration";
+                  "getConfiguration";
-                    "getSystem";
+                  "getSystem";
-                    "newTheme";
+                  "newTheme";
-                    "openRawResource";
+                  "openRawResource";
-                    "openRawResourceFd"
+                  "openRawResourceFd"
-                  ] in
+                ] in
-                  not (List.mem non_functional_resource_methods method_name)
+                not (List.mem non_functional_resource_methods method_name)
-              | _ ->
+            | _ ->
-                  false
+                false
-            end
+          end
-        | _ ->
+      | _ ->
-            false in
+          false in
-      is_annotated_functional pn || is_modeled_functional pn in
+    is_annotated_functional pname || is_modeled_functional pname
-    proc_is_functional pname || PatternMatch.override_exists proc_is_functional tenv pname
 
   let acquires_ownership pname tenv =
     let is_allocation pn =
@@ -475,10 +480,18 @@ 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 is_functional callee_pname tenv ->
+          | Some (ret_id, ret_typ) ->
+              let add_if_annotated predicate attribute attribute_map =
+                if proc_or_override_exists callee_pname tenv predicate
+                then
+                  AttributeMapDomain.add_attribute
+                    (AccessPath.of_id ret_id ret_typ) attribute attribute_map
+                else attribute_map in
               let attribute_map =
-                AttributeMapDomain.add_attribute
+                add_if_annotated is_functional Functional astate_callee.attribute_map
-                  (AccessPath.of_id ret_id ret_typ) Functional astate.attribute_map in
+                |> add_if_annotated
+                  (has_return_annot Annotations.ia_is_returns_ownership)
+                  Domain.Attribute.unconditionally_owned in
               { astate_callee with attribute_map; }
           | _ ->
               astate_callee

infer/src/checkers/annotations.ml

@@ -51,6 +51,7 @@ let present = "Present"
 let privacy_source = "PrivacySource"
 let privacy_sink = "PrivacySink"
 let strict = "com.facebook.infer.annotation.Strict"
+let returns_ownership = "ReturnsOwnership"
 let suppress_lint = "SuppressLint"
 let suppress_view_nullability = "SuppressViewNullability"
 let thread_confined = "ThreadConfined"
@@ -144,6 +145,9 @@ let ia_is_nonnull ia =
 let ia_is_false_on_null ia =
   ia_ends_with ia false_on_null
 
+let ia_is_returns_ownership ia =
+  ia_ends_with ia returns_ownership
+
 let ia_is_true_on_null ia =
   ia_ends_with ia true_on_null
 

infer/src/checkers/annotations.mli

@@ -82,6 +82,7 @@ val ia_is_thread_safe_method : Annot.Item.t -> bool
 val ia_is_assume_thread_safe : Annot.Item.t -> bool
 val ia_is_ui_thread : Annot.Item.t -> bool
 val ia_is_thread_confined : Annot.Item.t -> bool
+val ia_is_returns_ownership : Annot.Item.t -> bool
 val ia_is_volatile : Annot.Item.t -> bool
 
 (** return true if the given predicate evaluates to true on an annotation of one of [pdesc]'s

infer/tests/codetoanalyze/java/threadsafety/Annotations.java

@@ -21,6 +21,7 @@ import android.support.annotation.UiThread;
 import com.facebook.infer.annotation.AssumeThreadSafe;
 import com.facebook.infer.annotation.Functional;
 import com.facebook.infer.annotation.ThreadConfined;
+import com.facebook.infer.annotation.ReturnsOwnership;
 
 /** tests for classes and method annotations that are meaningful w.r.t thread-safety */
 
@@ -49,13 +50,14 @@ import com.facebook.infer.annotation.ThreadConfined;
 @interface OnUnmount {
 }
 
-interface FunctionalInterface {
+interface Interface {
 
-  @Functional Object method();
+  @Functional Object functionalMethod();
+  @ReturnsOwnership Obj returnsOwnershipMethod();
 }
 
 @ThreadSafe
-class Annotations implements FunctionalInterface {
+class Annotations implements Interface {
   Object f;
 
   @UiThread
@@ -96,10 +98,6 @@ class Annotations implements FunctionalInterface {
     }
   }
 
-  static class Obj {
-    Object fld;
-  }
-
   @ThreadConfined(ThreadConfined.ANY) Obj encapsulatedField;
 
   public void mutateConfinedFieldDirectlyOk() {
@@ -111,7 +109,7 @@ class Annotations implements FunctionalInterface {
   }
 
   public void mutateSubfieldOfConfinedBad() {
-    this.encapsulatedField.fld = new Object();
+    this.encapsulatedField.f = new Object();
   }
 
   @ThreadConfined("some_custom_string")
@@ -147,7 +145,7 @@ class Annotations implements FunctionalInterface {
   @Functional native Object returnFunctional1();
   @Functional Object returnFunctional2() { return null; }
   // marked @Functional in interface
-  @Override public Object method() { return null; }
+  @Override public Object functionalMethod() { return null; }
 
   Object mAssignToFunctional;
 
@@ -167,7 +165,7 @@ class Annotations implements FunctionalInterface {
 
   public Object functionalOk3() {
     if (mAssignToFunctional == null) {
-      mAssignToFunctional = method();
+      mAssignToFunctional = functionalMethod();
     }
     return mAssignToFunctional;
   }
@@ -273,4 +271,19 @@ class Annotations implements FunctionalInterface {
     mInt = returnNonFunctionalInt() + returnInt();
   }
 
+  @ReturnsOwnership native Obj returnsOwned();
+
+  @Override
+  public native Obj returnsOwnershipMethod(); // marked @ReturnsOwnership in interface
+
+  void mutateAnnotatedOwnedOk() {
+    Obj owned = returnsOwned();
+    owned.f = new Object();
+  }
+
+  void mutateAnnotatedOverrideOwnedOk() {
+    Obj owned = returnsOwnershipMethod();
+    owned.f = new Object();
+  }
+
 }

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

@@ -6,7 +6,7 @@ codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionaLong
 codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.functionalAndNonfunctionalBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mInt]
 codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateOffUiThreadBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.f]
-codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Annotations$Obj.fld]
+codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Obj.f]
 codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.buildThenMutateBad(Builders$Obj), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Builders$Obj.g]
 codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.mutateBad(Builders$Obj), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Builders$Obj.g]
 codetoanalyze/java/threadsafety/Constructors.java, Constructors Constructors.singletonBad(), 2, THREAD_SAFETY_VIOLATION, [call to Constructors.<init>(Object),access to Constructors.staticField]