From df257da918cffd0f3d8231c17f3339414b567549 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 21 Jun 2016 07:08:33 -0700 Subject: [PATCH] supporting @GuardedBy(MyClass.class) idiom Reviewed By: peterogithub Differential Revision: D3459531 fbshipit-source-id: 6e47c51 --- infer/src/backend/rearrange.ml | 26 +++++++++++++++---- .../java/infer/GuardedByExample.java | 17 ++++++++++++ .../endtoend/java/infer/GuardedByTest.java | 1 + 3 files changed, 39 insertions(+), 5 deletions(-) diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index ba2f15ea7..9c8a33a82 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -616,6 +616,7 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst = (** If [lexp] is an access to a field that is annotated with @GuardedBy, add constraints to [prop] expressing the safety conditions for the access. Complain if these conditions cannot be met. *) let add_guarded_by_constraints prop lexp pdesc = + let pname = Cfg.Procdesc.get_proc_name pdesc in let excluded_guardedby_string str = str = "ui_thread" in (* don't warn on @GuardedBy("ui_thread") *) let extract_guarded_by_str item_annot = @@ -637,6 +638,13 @@ let add_guarded_by_constraints prop lexp pdesc = | _ -> None in let guarded_by_str_is_this guarded_by_str = guarded_by_str = "this" in + let guarded_by_str_is_class guarded_by_str class_str = + string_is_suffix guarded_by_str (class_str ^ ".class") in + let guarded_by_str_is_current_class guarded_by_str = function + | Procname.Java java_pname -> + (* programmers write @GuardedBy("MyClass.class") when the field is guarded by the class *) + guarded_by_str_is_class guarded_by_str (Procname.java_get_class_name java_pname) + | _ -> false in (* find A.guarded_by_fld_str |-> B and return Some B, or None if there is no such hpred *) let find_guarded_by_exp guarded_by_str sigma = let is_guarded_by_strexp (fld, _) = @@ -646,6 +654,9 @@ let add_guarded_by_constraints prop lexp pdesc = Ident.fieldname_to_string fld = guarded_by_str in IList.find_map_opt (function + | Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Sil.Sizeof (typ, _, _)) + when guarded_by_str_is_class guarded_by_str (Ident.name_to_string clazz) -> + Some (Sil.Eexp (lhs_exp, Sil.inst_none), typ) | Sil.Hpointsto (_, Estruct (flds, _), Sil.Sizeof (typ, _, _)) -> begin try @@ -675,8 +686,10 @@ let add_guarded_by_constraints prop lexp pdesc = (* the lock is not held, but the procedure is annotated with @GuardedBy *) proc_guarded_by_str = guarded_by_str | None -> false in - let warn pdesc accessed_fld guarded_by_str = - let pname = Cfg.Procdesc.get_proc_name pdesc in + let is_synchronized_on_class guarded_by_str = + guarded_by_str_is_current_class guarded_by_str pname && + Cfg.Procdesc.is_java_synchronized pdesc && Procname.java_is_static pname in + let warn accessed_fld guarded_by_str = let loc = State.get_loc () in let err_desc = Localise.desc_unsafe_guarded_by_access pname accessed_fld guarded_by_str loc in @@ -692,6 +705,8 @@ let add_guarded_by_constraints prop lexp pdesc = let has_lock guarded_by_exp = (* procedure is synchronized and guarded by this *) (guarded_by_str_is_this guarded_by_str && Cfg.Procdesc.is_java_synchronized pdesc) || + (guarded_by_str_is_current_class guarded_by_str pname && + Cfg.Procdesc.is_java_synchronized pdesc && Procname.java_is_static pname) || (* or the prop says we already have the lock *) IList.exists (function @@ -715,7 +730,7 @@ let add_guarded_by_constraints prop lexp pdesc = then begin (* non-private method; can't ensure that the lock is held. warn. *) - warn pdesc accessed_fld guarded_by_str; + warn accessed_fld guarded_by_str; prop end else @@ -723,10 +738,11 @@ let add_guarded_by_constraints prop lexp 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) + if not (proc_has_matching_annot pdesc guarded_by_str + || is_synchronized_on_class 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 + warn accessed_fld guarded_by_str 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 diff --git a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java index 5e38d065e..239164dbd 100644 --- a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java +++ b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java @@ -55,6 +55,9 @@ public class GuardedByExample { @GuardedBy("sLock") static Object sFld; + @GuardedBy("GuardedByExample.class") + static Object sGuardedByClass; + static { // don't warn on class initializer sFld = new Object(); @@ -196,6 +199,20 @@ public class GuardedByExample { } } + synchronized static void staticSynchronizedOk() { + sGuardedByClass.toString(); + } + + static void synchronizeOnClassOk() { + synchronized(GuardedByExample.class) { + sGuardedByClass.toString(); // should not warn here + } + } + + void synchronizedOnThisBad() { + sGuardedByClass.toString(); + } + // 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 dc1a0f36e..855af967c 100644 --- a/infer/tests/endtoend/java/infer/GuardedByTest.java +++ b/infer/tests/endtoend/java/infer/GuardedByTest.java @@ -52,6 +52,7 @@ public class GuardedByTest { "readGFromCopyBad", "readHBad", "readHBadSynchronizedMethodShouldntHelp", + "synchronizedOnThisBad", // TODO: report these // "unguardedCallSiteBad1", // "unguardedCallSiteBad2",