diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 7d7d6eb10..2286acff9 100644 --- a/infer/src/backend/rearrange.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java index 84c725684..83da3e419 100644 --- a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java +++ b/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() { diff --git a/infer/tests/endtoend/java/infer/GuardedByTest.java b/infer/tests/endtoend/java/infer/GuardedByTest.java index 79ac1f8ea..6403cc31f 100644 --- a/infer/tests/endtoend/java/infer/GuardedByTest.java +++ b/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",