From b940c4dfacbe7a6dfe149ef508d474ec3b7ed1ae Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 14 Jun 2016 15:28:15 -0700 Subject: [PATCH] warning on guarded-by writes Differential Revision: D3390055 fbshipit-source-id: 1c68fcd --- infer/src/backend/rearrange.ml | 28 ++++++---- .../java/infer/GuardedByExample.java | 56 ++++++++++++++++++- .../endtoend/java/infer/GuardedByTest.java | 6 +- 3 files changed, 75 insertions(+), 15 deletions(-) diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index d2657929e..4c433d0c4 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -618,7 +618,6 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst = let add_guarded_by_constraints prop lexp pdesc = let excluded_guardedby_string str = str = "ui_thread" in (* don't warn on @GuardedBy("ui_thread") *) - let sigma = Prop.get_sigma prop in let extract_guarded_by_str item_annot = let annot_extract_guarded_by_str (annot, _) = if Annotations.annot_ends_with annot Annotations.guarded_by @@ -658,7 +657,7 @@ let add_guarded_by_constraints prop lexp pdesc = None) sigma in (* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *) - let enforce_guarded_access accessed_fld guarded_by_str prop = + let enforce_guarded_access_ accessed_fld guarded_by_str prop = (* return true if [pdesc] has an annotation that matches [guarded_by_str] *) let proc_has_matching_annot pdesc guarded_by_str = let proc_signature = @@ -716,21 +715,25 @@ let add_guarded_by_constraints prop lexp pdesc = lock in the current prop). so just be silent. *) (); prop in + let enforce_guarded_access fld typ prop = + match get_guarded_by_fld_str fld typ with + | Some guarded_by_fld_str -> enforce_guarded_access_ fld guarded_by_fld_str prop + | None -> prop in let check_fld_locks typ prop_acc (fld, strexp) = match strexp with - | Sil.Eexp (exp, _) when Sil.exp_equal exp lexp -> - begin - match get_guarded_by_fld_str fld typ with - | Some guarded_by_fld_str -> enforce_guarded_access fld guarded_by_fld_str prop_acc - | None -> prop_acc (* field not annotated; proceed as normal *) - end - | _ -> - prop_acc in + | Sil.Eexp (exp, _) when Sil.exp_equal exp lexp -> enforce_guarded_access fld typ prop_acc + | _ -> prop_acc in let hpred_check_flds prop_acc = function | Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _, _)) -> IList.fold_left (check_fld_locks typ) prop_acc flds | _ -> prop_acc in - IList.fold_left hpred_check_flds prop sigma + match lexp with + | Sil.Lfield (_, fld, typ) -> + (* check for direct access to field annotated with @GuardedBy *) + enforce_guarded_access fld typ prop + | _ -> + (* check for access via alias *) + IList.fold_left hpred_check_flds prop (Prop.get_sigma prop) (** Add a pointsto for [root(lexp): typ] to the iterator and to the footprint, if it's compatible with the allowed footprint @@ -1261,7 +1264,8 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc if report_deref_errors then check_dereference_error pdesc prop nlexp (State.get_loc ()); let pname = Cfg.Procdesc.get_proc_name pdesc in let prop' = - if Config.csl_analysis && !Config.footprint && Procname.is_java pname + if Config.csl_analysis && !Config.footprint && Procname.is_java pname && + not (Procname.is_constructor pname || Procname.is_class_initializer pname) then add_guarded_by_constraints prop lexp pdesc else prop in match Prop.prop_iter_create prop' with diff --git a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java index 5a33e861e..83d413d54 100644 --- a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java +++ b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java @@ -40,23 +40,54 @@ public class GuardedByExample { @GuardedBy("ui_thread") Object t = new Object(); + private static Object sLock = new Object(); + + @GuardedBy("sLock") + static Object sFld; + + static { + // don't warn on class initializer + sFld = new Object(); + } + + public GuardedByExample() { + // don't warn on reads or writes of Guarded fields in constructor + f.toString(); + g = new Object(); + } void readFBad() { this.f.toString(); } + void writeFBad() { + this.f = new Object(); + } + void readFBadWrongLock() { synchronized (mOtherLock) { this.f.toString(); // f is supposed to be protected by mLock } } + void writeFBadWrongLock() { + synchronized (mOtherLock) { + this.f = new Object(); // f is supposed to be protected by mLock + } + } + void readFAfterBlockBad() { synchronized (mLock) { } this.f.toString(); } + void writeFAfterBlockBad() { + synchronized (mLock) { + } + this.f = new Object(); + } + @GuardedBy("mOtherLock") void readFBadWrongAnnotation() { this.f.toString(); @@ -67,20 +98,34 @@ public class GuardedByExample { this.f.toString(); } - synchronized void synchronizedMethodOk() { + synchronized void synchronizedMethodReadOk() { this.g.toString(); } + synchronized void synchronizedMethodWriteOk() { + this.g = new Object(); + } + void readFOkSynchronized() { synchronized (mLock) { this.f.toString(); } } - synchronized void synchronizedMethodBad() { + void writeFOkSynchronized() { + synchronized (mLock) { + this.f = new Object(); + } + } + + synchronized void synchronizedMethodReadBad() { this.f.toString(); // f is supposed to be protected by mLock, not this } + synchronized void synchronizedMethodWriteBad() { + 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 @@ -89,6 +134,13 @@ public class GuardedByExample { 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 + } + mCopyOfG = new Object(); // ok; this doesn't change the value of g + } + void readHBad() { synchronized (mLock) { // h is not protected by mLock this.h.toString(); diff --git a/infer/tests/endtoend/java/infer/GuardedByTest.java b/infer/tests/endtoend/java/infer/GuardedByTest.java index 63b38f0ff..dc1a0f36e 100644 --- a/infer/tests/endtoend/java/infer/GuardedByTest.java +++ b/infer/tests/endtoend/java/infer/GuardedByTest.java @@ -41,10 +41,14 @@ public class GuardedByTest { throws IOException, InterruptedException, InferException { String[] methods = { "readFBad", + "writeFBad", "readFBadWrongLock", + "writeFBadWrongLock", "readFAfterBlockBad", + "writeFAfterBlockBad", "readFBadWrongAnnotation", - "synchronizedMethodBad", + "synchronizedMethodReadBad", + "synchronizedMethodWriteBad", "readGFromCopyBad", "readHBad", "readHBadSynchronizedMethodShouldntHelp",