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,