[thread-safety] don't warn on accesses to fields assigned to @Functional calls

Summary:
This diff adds a set of access paths holding a value returned from a method annotated with Functional to the domain.
If a "functional" value is written to a field, we won't count that right as an unprotected access.

The idea is to be able to use the Functional annotation to get rid of benign race false positive, such as:

```
Functional T iAlwaysReturnTheSameThing();

T mCache;

T memoizedGetter() {
  if (mCache == null) {
    mCache = iAlwaysReturnTheSameThing();
  }
  return mCache;
}
```

Although there is a write-write race on `mCache`, we don't care because it will be assigned to the same value regardless of which writer wins.

Reviewed By: peterogithub

Differential Revision: D4476492

fbshipit-source-id: cfa5dfc

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

@@ -0,0 +1,42 @@
+/*
+ * Copyright (c) 2004 - 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;
+
+/** Annotation for methods that always return the same value. The annotation is inherited by
+  * overrides of methods.
+  *
+  * This annotation is used to suppress benign race warnings on fields assigned to methods annotated
+  * with @Functional in the thread-safety analysis. For example:
+  *
+  * T mField;
+  * @Functional T someMethod();
+  * public void getField() {
+  *   if (mField == null) {
+  *     mField = someMethod();
+  *  }
+  *  return mField;
+  * }
+  *
+  * Normally, we'd report that the access to mField is unsafe, but we won't report here because of
+  * the @Functional annotation.
+  *
+  * If the return value of the annotated function is a double or long, the annotation will be
+  * ignored because writes to doubles/longs are not guaranteed to be atomic. That is, if type T was
+  * `long` in the example above, the write-write race on mField would no longer be benign.
+*/
+
+@Target({ElementType.METHOD})
+@Retention(RetentionPolicy.CLASS)
+public @interface Functional {}

infer/src/checkers/ThreadSafety.ml

@@ -65,7 +65,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     with Not_found -> None
 
   let is_owned access_path owned_set =
-    Domain.OwnershipDomain.mem access_path owned_set
+    Domain.AccessPathSetDomain.mem access_path owned_set
 
   let is_initializer tenv proc_name =
     Procname.is_constructor proc_name ||
@@ -118,6 +118,15 @@ 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 proc_or_override_is_annotated pname tenv predicate =
+    let has_return_annot pn =
+      Annotations.pname_has_return_annot
+        pn
+        ~attrs_of_pname:Specs.proc_resolve_attributes
+        predicate in
+    has_return_annot pname || PatternMatch.override_exists has_return_annot tenv pname
+
   let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; extras; } _ =
     let pname = Procdesc.get_proc_name pdesc in
     let is_allocation pn =
@@ -164,32 +173,31 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         begin
           match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with
           | Some lhs_access_path ->
-              let owned = OwnershipDomain.add lhs_access_path astate.owned in
+              let owned = AccessPathSetDomain.add lhs_access_path astate.owned in
               { astate with owned; }
           | None ->
               astate
         end
-    | Sil.Call (ret_opt, Const (Cfun pn), actuals, loc, _) ->
-        begin
+    | Sil.Call (ret_opt, Const (Cfun callee_pname), actuals, loc, _) ->
+        let astate_callee =
           (* assuming that modeled procedures do not have useful summaries *)
-          match get_lock_model pn with
+          match get_lock_model callee_pname with
           | Lock ->
               { astate with locks = true; }
           | Unlock ->
               { astate with locks = false; }
           | NoEffect ->
-              if is_unprotected astate.locks && is_container_write pn tenv
+              if is_unprotected astate.locks && is_container_write callee_pname tenv
               then
                 match actuals with
                 | (receiver_exp, receiver_typ) :: _ ->
-                    add_container_write pn loc receiver_exp receiver_typ astate
+                    add_container_write callee_pname loc receiver_exp receiver_typ astate
                 | [] ->
                     failwithf
                       "Call to %a is marked as a container write, but has no receiver"
-                      Procname.pp pn
+                      Procname.pp callee_pname
               else
-                begin
-                  match Summary.read_summary pdesc pn with
+                match Summary.read_summary pdesc callee_pname with
                 | Some (callee_locks,
                         callee_reads,
                         callee_conditional_writes,
@@ -201,7 +209,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                          (e.g., constructors that access static fields) *)
                       if is_unprotected locks'
                       then
-                          let call_site = CallSite.make pn loc in
+                        let call_site = CallSite.make callee_pname loc in
                         (* add the conditional writes rooted in the callee formal at [index] to
                            the current state *)
                         let add_conditional_writes
@@ -267,13 +275,26 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                         astate in
                     let owned = match ret_opt with
                       | Some (ret_id, ret_typ) when is_retval_owned ->
-                            OwnershipDomain.add (AccessPath.of_id ret_id ret_typ) astate'.owned
+                          AccessPathSetDomain.add (AccessPath.of_id ret_id ret_typ) astate'.owned
                       | _ ->
                           astate'.owned in
                     { astate' with locks = locks'; owned; }
                 | None ->
-                      astate
-                end
+                    astate in
+        begin
+          match ret_opt with
+          | Some (_, (Typ.Tint ILong | Tfloat FDouble)) ->
+              (* 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
+              proc_or_override_is_annotated callee_pname tenv Annotations.ia_is_functional ->
+              let functional =
+                AccessPathSetDomain.add
+                  (AccessPath.of_id ret_id ret_typ) astate_callee.functional in
+              { astate_callee with functional; }
+          | _ ->
+              astate_callee
         end
 
     | Sil.Store (Exp.Lvar lhs_pvar, lhs_typ, rhs_exp, _) when Pvar.is_frontend_tmp lhs_pvar ->
@@ -284,10 +305,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let get_formal_index exp typ = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
           | Some (base, _) -> FormalMap.get_formal_index base extras
           | None -> None in
+        let is_marked_functional exp typ functional_set =
+          match AccessPath.of_lhs_exp exp typ ~f_resolve_id with
+          | Some access_path -> AccessPathSetDomain.mem access_path functional_set
+          | None -> false in
         let conditional_writes, unconditional_writes =
           match lhs_exp with
           | Lfield (base_exp, _, typ)
-            when is_unprotected astate.locks -> (* abstracts no lock being held *)
+            when is_unprotected astate.locks (* abstracts no lock being held *) &&
+                 not (is_marked_functional rhs_exp lhs_typ astate.functional) ->
               begin
                 match get_formal_index base_exp typ with
                 | Some formal_index ->
@@ -321,20 +347,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               end
           | _ ->
               astate.conditional_writes, astate.unconditional_writes in
-        (* if rhs is owned, propagate ownership to lhs. otherwise, remove lhs from ownership set
-           (since it may have previously held an owned memory loc and is now being reassigned *)
-        let owned =
-          match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id,
-                AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id with
+
+        (* if rhs is owned/functional, propagate to lhs. otherwise, remove lhs from
+           ownership/functional set (since it may have previously held an owned/functional memory
+           loc and is now being reassigned *)
+        let lhs_access_path_opt = AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id in
+        let rhs_access_path_opt = AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id in
+        let update_access_path_set access_path_set =
+          match lhs_access_path_opt, rhs_access_path_opt with
           | Some lhs_access_path, Some rhs_access_path ->
-              if OwnershipDomain.mem rhs_access_path astate.owned
-              then OwnershipDomain.add lhs_access_path astate.owned
-              else OwnershipDomain.remove lhs_access_path astate.owned
+              if AccessPathSetDomain.mem rhs_access_path access_path_set
+              then AccessPathSetDomain.add lhs_access_path access_path_set
+              else AccessPathSetDomain.remove lhs_access_path access_path_set
           | Some lhs_access_path, None ->
-              OwnershipDomain.remove lhs_access_path astate.owned
+              AccessPathSetDomain.remove lhs_access_path access_path_set
           | _ ->
-              astate.owned in
-        { astate with conditional_writes; unconditional_writes; owned; }
+              access_path_set in
+        let owned = update_access_path_set astate.owned in
+        let functional = update_access_path_set astate.functional in
+        { astate with conditional_writes; unconditional_writes; owned; functional; }
 
     | Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) ->
         let id_map = analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate in
@@ -344,15 +375,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               add_path_to_state rhs_exp typ loc astate.reads astate.id_map astate.owned pname tenv
           | _ ->
               astate.reads in
-        (* if rhs is owned, propagate ownership to lhs *)
-        let owned =
+
+        (* if rhs is owned/functional, propagate to lhs *)
+        let owned, functional =
           match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with
-          | Some rhs_access_path
-            when OwnershipDomain.mem rhs_access_path astate.owned ->
-              OwnershipDomain.add (AccessPath.of_id lhs_id rhs_typ) astate.owned
+          | Some rhs_access_path ->
+              let propagate_to_lhs access_path_set =
+                if AccessPathSetDomain.mem rhs_access_path access_path_set
+                then AccessPathSetDomain.add (AccessPath.of_id lhs_id rhs_typ) access_path_set
+                else access_path_set in
+              propagate_to_lhs astate.owned, propagate_to_lhs astate.functional
           | _ ->
-              astate.owned in
-        { astate with Domain.reads; id_map; owned; }
+              astate.owned, astate.functional in
+        { astate with Domain.reads; id_map; owned; functional; }
 
     | Sil.Remove_temps (ids, _) ->
         let id_map =
@@ -484,7 +519,7 @@ let make_results_table get_proc_desc file_env =
                   AccessPath.of_pvar
                     (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc))
                     (Procdesc.get_ret_type pdesc) in
-                let return_is_owned = OwnershipDomain.mem return_var_ap owned in
+                let return_is_owned = AccessPathSetDomain.mem return_var_ap owned in
                 Some (locks, reads, conditional_writes, unconditional_writes, return_is_owned)
             | None ->
                 None

infer/src/checkers/ThreadSafetyDomain.ml

@@ -11,7 +11,7 @@ open! IStd
 
 module F = Format
 
-module OwnershipDomain = AbstractDomain.InvertedSet(AccessPath.RawSet)
+module AccessPathSetDomain = AbstractDomain.InvertedSet(AccessPath.RawSet)
 
 module TraceElem = struct
   module Kind = AccessPath.Raw
@@ -62,7 +62,8 @@ type astate =
     conditional_writes : ConditionalWritesDomain.astate;
     unconditional_writes : PathDomain.astate;
     id_map : IdAccessPathMapDomain.astate;
-    owned : OwnershipDomain.astate;
+    owned : AccessPathSetDomain.astate;
+    functional : AccessPathSetDomain.astate;
   }
 
 
@@ -75,8 +76,9 @@ let empty =
   let conditional_writes = ConditionalWritesDomain.empty in
   let unconditional_writes = PathDomain.empty in
   let id_map = IdAccessPathMapDomain.empty in
-  let owned = OwnershipDomain.empty in
-  { locks; reads; conditional_writes; unconditional_writes; id_map; owned; }
+  let owned = AccessPathSetDomain.empty in
+  let functional = AccessPathSetDomain.empty in
+  { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; }
 
 let (<=) ~lhs ~rhs =
   if phys_equal lhs rhs
@@ -87,7 +89,7 @@ let (<=) ~lhs ~rhs =
     ConditionalWritesDomain.(<=) ~lhs:lhs.conditional_writes ~rhs:rhs.conditional_writes &&
     PathDomain.(<=) ~lhs:lhs.unconditional_writes ~rhs:rhs.unconditional_writes &&
     IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map &&
-    OwnershipDomain.(<=) ~lhs:lhs.owned ~rhs:rhs.owned
+    AccessPathSetDomain.(<=) ~lhs:lhs.owned ~rhs:rhs.owned
 
 let join astate1 astate2 =
   if phys_equal astate1 astate2
@@ -101,8 +103,9 @@ let join astate1 astate2 =
     let unconditional_writes =
       PathDomain.join astate1.unconditional_writes astate2.unconditional_writes in
     let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in
-    let owned = OwnershipDomain.join astate1.owned astate2.owned in
-    { locks; reads; conditional_writes; unconditional_writes; id_map; owned; }
+    let owned = AccessPathSetDomain.join astate1.owned astate2.owned in
+    let functional = AccessPathSetDomain.join astate1.functional astate2.functional in
+    { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; }
 
 let widen ~prev ~next ~num_iters =
   if phys_equal prev next
@@ -117,8 +120,10 @@ let widen ~prev ~next ~num_iters =
     let unconditional_writes =
       PathDomain.widen ~prev:prev.unconditional_writes ~next:next.unconditional_writes ~num_iters in
     let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in
-    let owned = OwnershipDomain.widen ~prev:prev.owned ~next:next.owned ~num_iters in
-    { locks; reads; conditional_writes; unconditional_writes; id_map; owned; }
+    let owned = AccessPathSetDomain.widen ~prev:prev.owned ~next:next.owned ~num_iters in
+    let functional =
+      AccessPathSetDomain.widen ~prev:prev.functional ~next:next.functional ~num_iters in
+    { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; }
 
 let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retval_owned) =
   F.fprintf
@@ -130,13 +135,15 @@ let pp_summary fmt (locks, reads, conditional_writes, unconditional_writes, retv
     PathDomain.pp unconditional_writes
     retval_owned
 
-let pp fmt { locks; reads; conditional_writes; unconditional_writes; id_map; owned; } =
+let pp fmt { locks; reads; conditional_writes; unconditional_writes; id_map; owned; functional; } =
   F.fprintf
     fmt
-    "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Owned: %a"
+    "Locks: %a Reads: %a Conditional Writes: %a Unconditional Writes: %a Id Map: %a Owned: %a\
+     Functional: %a"
     LocksDomain.pp locks
     PathDomain.pp reads
     ConditionalWritesDomain.pp conditional_writes
     PathDomain.pp unconditional_writes
     IdAccessPathMapDomain.pp id_map
-    OwnershipDomain.pp owned
+    AccessPathSetDomain.pp owned
+    AccessPathSetDomain.pp functional

infer/src/checkers/ThreadSafetyDomain.mli

@@ -11,7 +11,7 @@ open! IStd
 
 module F = Format
 
-module OwnershipDomain : module type of AbstractDomain.InvertedSet (AccessPath.RawSet)
+module AccessPathSetDomain : module type of AbstractDomain.InvertedSet (AccessPath.RawSet)
 
 module TraceElem : TraceElem.S with module Kind = AccessPath.Raw
 
@@ -55,8 +55,10 @@ type astate =
     (** access paths written outside of synchronization *)
     id_map : IdAccessPathMapDomain.astate;
     (** map used to decompile temporary variables into access paths *)
-    owned : OwnershipDomain.astate;
+    owned : AccessPathSetDomain.astate;
     (** access paths that must be owned by the current function *)
+    functional : AccessPathSetDomain.astate;
+    (** access paths holding values returned from a call marked with @Functional *)
   }
 
 (** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of a

infer/src/checkers/annotations.ml

@@ -27,6 +27,7 @@ let expensive = "Expensive"
 let false_on_null = "FalseOnNull"
 let for_ui_thread = "ForUiThread"
 let for_non_ui_thread = "ForNonUiThread"
+let functional = "Functional"
 let guarded_by = "GuardedBy"
 let ignore_allocations = "IgnoreAllocations"
 let initializer_ = "Initializer"
@@ -198,6 +199,9 @@ let ia_is_verify ia =
 let ia_is_expensive ia =
   ia_ends_with ia expensive
 
+let ia_is_functional ia =
+  ia_ends_with ia functional
+
 let ia_is_performance_critical ia =
   ia_ends_with ia performance_critical
 

infer/src/checkers/annotations.mli

@@ -93,6 +93,7 @@ val ia_is_present : Annot.Item.t -> bool
 val ia_is_true_on_null : Annot.Item.t -> bool
 val ia_is_verify : Annot.Item.t -> bool
 val ia_is_expensive : Annot.Item.t -> bool
+val ia_is_functional : Annot.Item.t -> bool
 val ia_is_performance_critical : Annot.Item.t -> bool
 val ia_is_no_allocation : Annot.Item.t -> bool
 val ia_is_ignore_allocations : Annot.Item.t -> bool

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

@@ -19,6 +19,7 @@ import javax.annotation.concurrent.ThreadSafe;
 import android.support.annotation.UiThread;
 
 import com.facebook.infer.annotation.AssumeThreadSafe;
+import com.facebook.infer.annotation.Functional;
 import com.facebook.infer.annotation.ThreadConfined;
 
 /** tests for classes and method annotations that are meaningful w.r.t thread-safety */
@@ -48,8 +49,13 @@ import com.facebook.infer.annotation.ThreadConfined;
 @interface OnUnmount {
 }
 
+interface FunctionalInterface {
+
+  @Functional Object method();
+}
+
 @ThreadSafe
-class Annotations {
+class Annotations implements FunctionalInterface {
   Object f;
 
   @UiThread
@@ -134,4 +140,54 @@ class Annotations {
     this.f = new Object();
   }
 
+  @Functional native Object returnFunctional1();
+  @Functional Object returnFunctional2() { return null; }
+  // marked @Functional in interface
+  @Override public Object method() { return null; }
+
+  Object mAssignToFunctional;
+
+  public Object functionalOk1() {
+    if (mAssignToFunctional == null) {
+      mAssignToFunctional = returnFunctional1();
+    }
+    return mAssignToFunctional;
+  }
+
+  public Object functionalOk2() {
+    if (mAssignToFunctional == null) {
+      mAssignToFunctional = returnFunctional2();
+    }
+    return mAssignToFunctional;
+  }
+
+  public Object functionalOk3() {
+    if (mAssignToFunctional == null) {
+      mAssignToFunctional = method();
+    }
+    return mAssignToFunctional;
+  }
+
+  @Functional native double returnDouble();
+  @Functional native long returnLong();
+
+  double mDouble;
+  long mLong;
+
+  // writes to doubles are not atomic on all platforms, so this is not a benign race
+  public double functionalDoubleBad() {
+    if (mDouble == 0.0) {
+      mDouble = returnDouble();
+    }
+    return mDouble;
+  }
+
+  // writes to longs are not atomic on all platforms, so this is not a benign race
+  public long functionaLongBad() {
+    if (mLong == 0L) {
+      mLong = returnLong();
+    }
+    return mLong;
+  }
+
 }

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

@@ -1,3 +1,5 @@
+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.functionaLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong]
 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/Builders.java, Builders$Obj Builders.buildThenMutateBad(Builders$Obj), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Builders$Obj.g]