From e3e80dd2f03df8ca90959a5d30b41ea9db3b0986 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Tue, 24 May 2016 05:21:56 -0700
Subject: [PATCH] don't report on private unguarded accesses

Reviewed By: jvillard

Differential Revision: D3334391

fbshipit-source-id: a5079b5
---
 infer/src/backend/rearrange.ml                | 21 +++++----
 .../java/infer/GuardedByExample.java          | 45 ++++++++++++++++---
 .../endtoend/java/infer/GuardedByTest.java    |  4 ++
 3 files changed, 56 insertions(+), 14 deletions(-)

diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 414f8c0d6..52e2431a8 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -676,25 +676,28 @@ let add_guarded_by_constraints prop lexp pdesc =
           (* TODO: materialize [fld], but don't add [fld] to the footprint. *)
           prop
         else
-        if proc_has_matching_annot pdesc guarded_by_str
+          (* we don't know if we have the lock or not. *)
+        if Cfg.Procdesc.get_access pdesc <> Sil.Private
         then
-          (* procedure is annotated and holding the same lock as the field. add locked proof
-             obligation to the current *)
-          (* TODO: materialize [fld], but don't add [fld] to the footprint. *)
-          let locked_attr = Sil.Const (Cattribute Alocked) in
-          Prop.conjoin_neq ~footprint:true guarded_by_exp locked_attr prop
-        else
           begin
-            (* lock is not held. warn *)
+            (* non-private method; can't ensure that the lock is held. warn. *)
             warn pdesc accessed_fld guarded_by_str;
             prop
           end
+        else
+          (* private method. add locked proof obligation to [pdesc] *)
+          let locked_attr = Sil.Const (Cattribute Alocked) in
+          Prop.conjoin_neq ~footprint:true guarded_by_exp locked_attr prop
     | _ ->
         if not (proc_has_matching_annot pdesc guarded_by_str)
         then
           (* can't find the object the annotation refers to, and procedure is not annotated. warn *)
           warn pdesc accessed_fld guarded_by_str
-        else ();(* TODO: add proof obligation here *)
+        else
+          (* procedure has same GuardedBy annotation as the field. we would like to add a proof
+             obligation, but we can't (because we can't find an expression corresponding to the
+             lock in the current prop). so just be silent. *)
+          ();
         prop in
   let check_fld_locks typ prop_acc (fld, strexp) = match strexp with
     | Sil.Eexp (exp, _) when Sil.exp_equal exp lexp ->
diff --git a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java
index 45b9e5105..bf6c4ca55 100644
--- a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java
+++ b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java
@@ -63,11 +63,6 @@ public class GuardedByExample {
     this.f.toString();
   }
 
-  @GuardedBy("this")
-  void guardedByThisOk() {
-    this.g.toString();
-  }
-
   synchronized void synchronizedMethodOk() {
     this.g.toString();
   }
@@ -100,4 +95,44 @@ public class GuardedByExample {
     this.h.toString(); // h is not protected by this
   }
 
+  private void privateUnguardedAccess() {
+    // not protected, but safe if all call sites guard the access to f
+    this.g.toString();
+  }
+
+  public void guardedCallSite1() {
+    synchronized (this) {
+      privateUnguardedAccess(); // should not warn; lock is held
+    }
+  }
+
+  public synchronized void guardedCallSite2() {
+    privateUnguardedAccess(); // should not warn; lock is held
+  }
+
+  private void wrapper() {
+    privateUnguardedAccess(); // should not warn, just propagate the proof obl
+  }
+
+  public void guardedCallSite3() {
+    synchronized (this) {
+      wrapper(); // should not  warn
+    }
+  }
+
+  // TODO: report on these cases
+  /*
+  public void unguardedCallSiteBad1() {
+    privateUnguardedAccess(); // should warn; lock is not held
+  }
+
+  protected void unguardedCallSiteBad2() {
+    privateUnguardedAccess(); // should warn; lock is not held
+  }
+
+  void unguardedCallSiteBad3() {
+    privateUnguardedAccess(); // should warn; lock is not held
+  }
+  */
+
 }
diff --git a/infer/tests/endtoend/java/infer/GuardedByTest.java b/infer/tests/endtoend/java/infer/GuardedByTest.java
index 4bd7a336e..63b38f0ff 100644
--- a/infer/tests/endtoend/java/infer/GuardedByTest.java
+++ b/infer/tests/endtoend/java/infer/GuardedByTest.java
@@ -48,6 +48,10 @@ public class GuardedByTest {
       "readGFromCopyBad",
       "readHBad",
       "readHBadSynchronizedMethodShouldntHelp",
+      // TODO: report these
+      // "unguardedCallSiteBad1",
+      // "unguardedCallSiteBad2",
+      // "unguardedCallSiteBad3",
     };
     assertThat(
         "Results should contain " + UNSAFE_GUARDED_BY_ACCESS,