[thread-safety] new SynchronizedCollection annotation

Summary:
For collections whose type does not express that the collection is thread-safe (e.g., `Collections.syncrhonizedMap` and friends).
If you annotate a field holding one of these collections, we won't warn when you mutate the collection.

Reviewed By: jeremydubreil

Differential Revision: D4763565

fbshipit-source-id: 58b487a

infer/annotations/src/main/java/com/facebook/infer/annotation/SynchronizedCollection.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 analysis that a collection is thread-safe when this information is not already
+ * reflected in the collection's type. For example:
+ * private {@literal @SynchronizedCollection} Map mMap = Collections.synchronizedMap(...);
+ */
+
+@Target({ ElementType.FIELD })
+@Retention(RetentionPolicy.CLASS)
+public @interface SynchronizedCollection {
+}

infer/src/checkers/ThreadSafety.ml

@@ -318,9 +318,36 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           PatternMatch.supertype_exists tenv is_container_write_ typename &&
           not (PatternMatch.supertype_exists tenv is_threadsafe_collection typename)
       | _ -> false in
-    let add_container_write callee_pname actuals ~f_resolve_id callee_loc =
+    let add_container_write callee_pname actuals ~f_resolve_id callee_loc tenv =
       match actuals with
       | (receiver_exp, receiver_typ) :: _ ->
+          (* return true if field pointing to container is marked @SyncrhonizedContainer *)
+          let is_synchronized_container ((_, base_typ), accesses) =
+            let is_annotated_synchronized base_typename container_field tenv =
+              match Tenv.lookup tenv base_typename with
+              | Some base_typ ->
+                  Annotations.field_has_annot
+                    container_field
+                    base_typ Annotations.ia_is_synchronized_collection
+              | None ->
+                  false in
+            match List.rev accesses with
+            | AccessPath.FieldAccess base_field ::
+              AccessPath.FieldAccess container_field :: _->
+                let base_typename =
+                  Typ.Name.Java.from_string (Fieldname.java_get_class base_field) in
+                is_annotated_synchronized base_typename container_field tenv
+            | [AccessPath.FieldAccess container_field] ->
+                begin
+                  match base_typ with
+                  | Typ.Tstruct base_typename | Tptr (Tstruct base_typename, _) ->
+                      is_annotated_synchronized base_typename container_field tenv
+                  | _ ->
+                      false
+                end
+            | _ ->
+                false in
+
           (* create a dummy write that represents mutating the contents of the container *)
           let open Domain in
           let dummy_fieldname =
@@ -329,12 +356,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           let dummy_access_exp = Exp.Lfield (receiver_exp, dummy_fieldname, receiver_typ) in
           let callee_accesses =
             match AccessPath.of_lhs_exp dummy_access_exp receiver_typ ~f_resolve_id with
-            | Some container_ap ->
+            | Some container_ap
+              when not (is_synchronized_container (AccessPath.Raw.truncate container_ap)) ->
                 AccessDomain.add_access
                   (Unprotected (Some 0))
                   (make_access container_ap Write callee_loc)
                   AccessDomain.empty
-            | None ->
+            | _ ->
                 AccessDomain.empty in
           Some (false, false, callee_accesses, AttributeSetDomain.empty)
       | _ ->
@@ -344,7 +372,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let get_summary caller_pdesc callee_pname actuals ~f_resolve_id callee_loc tenv =
       if is_container_write callee_pname tenv
       then
-        add_container_write callee_pname actuals ~f_resolve_id callee_loc
+        add_container_write callee_pname actuals ~f_resolve_id callee_loc tenv
       else
         Summary.read_summary caller_pdesc callee_pname in
     (* return true if the given procname boxes a primitive type into a reference type *)

infer/src/checkers/annotations.ml

@@ -50,8 +50,9 @@ let present = "Present"
 let privacy_source = "PrivacySource"
 let privacy_sink = "PrivacySink"
 let propagates_nullable = "PropagatesNullable"
-let strict = "com.facebook.infer.annotation.Strict"
 let returns_ownership = "ReturnsOwnership"
+let synchronized_collection = "SynchronizedCollection"
+let strict = "com.facebook.infer.annotation.Strict"
 let suppress_lint = "SuppressLint"
 let suppress_view_nullability = "SuppressViewNullability"
 let thread_confined = "ThreadConfined"
@@ -142,6 +143,9 @@ let ia_is_false_on_null ia =
 let ia_is_returns_ownership ia =
   ia_ends_with ia returns_ownership
 
+let ia_is_synchronized_collection ia =
+  ia_ends_with ia synchronized_collection
+
 let ia_is_true_on_null ia =
   ia_ends_with ia true_on_null
 

infer/src/checkers/annotations.mli

@@ -78,9 +78,10 @@ val ia_is_integrity_source : Annot.Item.t -> bool
 val ia_is_integrity_sink : Annot.Item.t -> bool
 val ia_is_guarded_by : Annot.Item.t -> bool
 val ia_is_not_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_synchronized_collection : Annot.Item.t -> bool
+val ia_is_thread_confined : Annot.Item.t -> bool
+val ia_is_ui_thread : 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

@@ -13,13 +13,17 @@ import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.Map;
 
 import android.support.annotation.UiThread;
 
-import com.facebook.infer.annotation.ThreadSafe;
 import com.facebook.infer.annotation.Functional;
-import com.facebook.infer.annotation.ThreadConfined;
 import com.facebook.infer.annotation.ReturnsOwnership;
+import com.facebook.infer.annotation.SynchronizedCollection;
+import com.facebook.infer.annotation.ThreadConfined;
+import com.facebook.infer.annotation.ThreadSafe;
 
 /** tests for classes and method annotations that are meaningful w.r.t thread-safety */
 
@@ -342,4 +346,15 @@ class Annotations implements Interface {
     c.writeOk();
   }
 
+  @SynchronizedCollection
+  private final Map<Object,Object> mSynchronizedMap = Collections.synchronizedMap(new HashMap());
+
+  public void synchronizedMapOk1() {
+    mSynchronizedMap.put(new Object(), new Object());
+  }
+
+  public void synchronizedMapOk2(Annotations a) {
+    a.mSynchronizedMap.put(new Object(), new Object());
+  }
+
 }