switching to by-ref semantics

Reviewed By: peterogithub

Differential Revision: D3567911

fbshipit-source-id: 8852485

infer/src/backend/rearrange.ml

@@ -739,9 +739,29 @@ let add_guarded_by_constraints prop lexp pdesc =
           | _ -> false)
         (Prop.get_exp_attributes prop guarded_by_exp) in
     let should_warn pdesc =
+      (* adding this check implements "by reference" semantics for guarded-by rather than "by value"
+         semantics. if this access is through a local L or field V.f
+         (where f is not the @GuardedBy field!), we will not warn.
+      *)
+      let is_accessible_through_local_ref exp =
+        IList.exists
+          (function
+            | Sil.Hpointsto (Lvar _, Eexp (rhs_exp, _), _) ->
+                Sil.exp_equal exp rhs_exp
+            | Sil.Hpointsto (_, Estruct (flds, _), _) ->
+                IList.exists
+                  (fun (fld, strexp) -> match strexp with
+                     | Sil.Eexp (rhs_exp, _) ->
+                         Sil.exp_equal exp rhs_exp && not (Ident.fieldname_equal fld accessed_fld)
+                     | _ ->
+                         false)
+                  flds
+            | _ -> false)
+          (Prop.get_sigma prop) in
       Cfg.Procdesc.get_access pdesc <> Sil.Private &&
       not (Annotations.pdesc_has_annot pdesc Annotations.visibleForTesting) &&
-      not (Procname.java_is_access_method (Cfg.Procdesc.get_proc_name pdesc)) in
+      not (Procname.java_is_access_method (Cfg.Procdesc.get_proc_name pdesc)) &&
+      not (is_accessible_through_local_ref lexp) in
     match find_guarded_by_exp guarded_by_str (Prop.get_sigma prop) with
     | Some (Sil.Eexp (guarded_by_exp, _), typ) ->
         if is_read_write_lock typ

infer/tests/codetoanalyze/java/infer/GuardedByExample.java

@@ -141,14 +141,6 @@ public class GuardedByExample {
     this.f = new Object(); // f is supposed to be protected by mLock, not this
   }
 
-  void readGFromCopyBad() {
-    synchronized (this) {
-      mCopyOfG = g;  // these are ok: access of g guarded by this
-      g.toString();
-    }
-    mCopyOfG.toString();  // should be an error; unprotected access to pt(g)
-  }
-
   void reassignCopyOk() {
     synchronized (this) {
       mCopyOfG = g;  // these are ok: access of g guarded by this
@@ -263,6 +255,44 @@ public class GuardedByExample {
     f.toString(); // should push proof obl to caller
   }
 
+  synchronized Object returnPtG() {
+    return g;
+  }
+
+  // note: this test should raise an error under "by value" GuardedBy semantics, but not under
+  // "by reference" GuardedBy semantics
+  void readGFromCopyOk() {
+    synchronized (this) {
+      mCopyOfG = g;  // these are ok: access of g guarded by this
+      g.toString();
+    }
+    mCopyOfG.toString();  // should be an error; unprotected access to pt(g)
+  }
+
+  // another "by reference" vs "by value" test. buggy in "by value", but safe in "by reference"
+  void usePtG() {
+    Object ptG = returnPtG();
+    ptG.toString();
+  }
+
+  Object byRefTrickyBad() {
+    Object local = null;
+    synchronized(this) {
+      local = g; // we have a local pointer... to pt(G)
+    }
+    g.toString(); // ...but unsafe access is through g!
+    return local;
+  }
+
+  void byRefTrickyOk() {
+    Object local = null;
+    synchronized(this) {
+      local = g; // we have a local pointer... to pt(G)
+    }
+    local.toString(); // ...but unsafe access is through g!
+  }
+
+
   // TODO: report on these cases
   /*
   public void unguardedCallSiteBad1() {

infer/tests/endtoend/java/infer/GuardedByTest.java

@@ -49,12 +49,12 @@ public class GuardedByTest {
       "readFBadWrongAnnotation",
       "synchronizedMethodReadBad",
       "synchronizedMethodWriteBad",
-      "readGFromCopyBad",
       "readHBad",
       "readHBadSynchronizedMethodShouldntHelp",
       "synchronizedOnThisBad",
       "readFromInnerClassBad1",
       "readFromInnerClassBad2",
+      "byRefTrickyBad",
       // TODO: report these
       // "unguardedCallSiteBad1",
       // "unguardedCallSiteBad2",