diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index db9d239ec..725e43f92 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -700,45 +700,76 @@ let add_guarded_by_constraints tenv prop lexp pdesc = end | _ -> None 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, _) = + let find_guarded_by_exp guarded_by_str0 sigma = + + let is_guarded_by_fld guarded_by_str fld _ = (* this comparison needs to be somewhat fuzzy, since programmers are free to write @GuardedBy("mLock"), @GuardedBy("MyClass.mLock"), or use other conventions *) Ident.fieldname_to_flat_string fld = guarded_by_str || - Ident.fieldname_to_string fld = guarded_by_str - in + Ident.fieldname_to_string fld = guarded_by_str in + + let get_fld_strexp_and_typ typ f flds = + let match_one (fld, strexp) = + match StructTyp.get_field_type_and_annotation ~lookup fld typ with + | Some (fld_typ, _) when f fld fld_typ -> Some (strexp, fld_typ) + | _ -> None in + IList.find_map_opt match_one flds in + + (* sometimes, programmers will write @GuardedBy("T.f") with the meaning "guarded by the field f + of the object of type T in the current state." note that this is ambiguous when there are + multiple objects of type T, but let's try to respect the intention *) + let match_on_field_type typ flds = + match string_split_character guarded_by_str0 '.' with + | Some class_part, field_part -> + let typ_matches_guarded_by _ = function + | Typ.Tptr (ptr_typ, _) -> + string_is_suffix class_part (Typ.to_string ptr_typ); + | _ -> + false in + begin + match get_fld_strexp_and_typ typ typ_matches_guarded_by flds with + | Some (Sil.Eexp (matching_exp, _), _) -> + IList.find_map_opt + (function + | Sil.Hpointsto (lhs_exp, Estruct (matching_flds, _), Sizeof (fld_typ, _, _)) + when Exp.equal lhs_exp matching_exp -> + get_fld_strexp_and_typ fld_typ (is_guarded_by_fld field_part) matching_flds + | _ -> + None) + sigma + | _ -> + None + end + | _ -> + None in + IList.find_map_opt (function | Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof (typ, _, _)) | Sil.Hpointsto (_, Sil.Eexp (Const (Cclass clazz) as lhs_exp, _), Exp.Sizeof (typ, _, _)) - when guarded_by_str_is_class guarded_by_str (Ident.name_to_string clazz) -> + when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) -> Some (Sil.Eexp (lhs_exp, Sil.inst_none), typ) | Sil.Hpointsto (_, Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> - let get_fld_strexp_and_typ f flds = - try - let fld, strexp = IList.find f flds in - begin - match StructTyp.get_field_type_and_annotation ~lookup fld typ with - | Some (fld_typ, _) -> Some (strexp, fld_typ) - | None -> None - end - with Not_found -> None in begin (* first, try to find a field that exactly matches the guarded-by string *) - match get_fld_strexp_and_typ is_guarded_by_strexp flds with - | None when guarded_by_str_is_this guarded_by_str -> + match get_fld_strexp_and_typ typ (is_guarded_by_fld guarded_by_str0) flds with + | None when guarded_by_str_is_this guarded_by_str0 -> (* if the guarded-by string is "OuterClass.this", look for "this$n" for some n. note that this is a bit sketchy when there are mutliple this$n's, but there's nothing we can do to disambiguate them. *) get_fld_strexp_and_typ - (fun (f, _) -> Ident.java_fieldname_is_outer_instance f) + typ + (fun f _ -> Ident.java_fieldname_is_outer_instance f) flds - | res -> - res + | None -> + (* can't find an exact match. try a different convention. *) + match_on_field_type typ flds + | Some _ as res_opt -> + res_opt end | Sil.Hpointsto (Lvar pvar, rhs_exp, Exp.Sizeof (typ, _, _)) - when (guarded_by_str_is_current_class_this guarded_by_str pname || - guarded_by_str_is_super_class_this guarded_by_str pname + when (guarded_by_str_is_current_class_this guarded_by_str0 pname || + guarded_by_str_is_super_class_this guarded_by_str0 pname ) && Pvar.is_this pvar -> Some (rhs_exp, typ) | _ -> diff --git a/infer/tests/build_systems/ant/issues.exp b/infer/tests/build_systems/ant/issues.exp index 5da9ddabc..a14b9619c 100644 --- a/infer/tests/build_systems/ant/issues.exp +++ b/infer/tests/build_systems/ant/issues.exp @@ -52,6 +52,8 @@ src/infer/GuardedByExample.java, String GuardedByExample$4.readFromInnerClassBad src/infer/GuardedByExample.java, void GuardedByExample$Sub.badSub(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure badSub()] src/infer/GuardedByExample.java, void GuardedByExample.badGuardedByNormalLock(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure badGuardedByNormalLock()] src/infer/GuardedByExample.java, void GuardedByExample.badGuardedByReentrantLock(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure badGuardedByReentrantLock()] +src/infer/GuardedByExample.java, void GuardedByExample.guardedByTypeSyntaxBad(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure guardedByTypeSyntaxBad()] +src/infer/GuardedByExample.java, void GuardedByExample.guardedByTypeSyntaxBad(), 2, UNSAFE_GUARDED_BY_ACCESS, [start of procedure guardedByTypeSyntaxBad()] src/infer/GuardedByExample.java, void GuardedByExample.readFAfterBlockBad(), 3, UNSAFE_GUARDED_BY_ACCESS, [start of procedure readFAfterBlockBad()] src/infer/GuardedByExample.java, void GuardedByExample.readFBad(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure readFBad()] src/infer/GuardedByExample.java, void GuardedByExample.readFBadButSuppressedOther(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure readFBadButSuppressedOther()] diff --git a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java index da3d76582..942391e10 100644 --- a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java +++ b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java @@ -19,6 +19,7 @@ import javax.annotation.concurrent.GuardedBy; import java.util.concurrent.locks.Lock; import java.util.concurrent.locks.ReentrantLock; import java.util.concurrent.locks.ReadWriteLock; +import java.util.concurrent.locks.ReentrantLock; import java.util.concurrent.locks.ReentrantReadWriteLock; import java.io.Closeable; @@ -535,4 +536,48 @@ public class GuardedByExample { guardedbyrel = 44; } + static class OtherClassWithLock { + ReentrantLock lock; + + @GuardedBy("lock") + Object guardedByLock; + + Object otherClassObject; + + void guardedInSameClassOk() { + lock.lock(); + guardedByLock = new Object(); + lock.unlock(); + } + } + + @GuardedBy("OtherClassWithLock.lock") + Object guardedByLock1; + + @GuardedBy("codetoanalyze.java.infer.GuardedByExample$OtherClassWithLock.lock") + Object guardedByLock2; + + @GuardedBy("OtherClassWithLock.otherClassObject") + Object guardedByLock3; + + OtherClassWithLock otherClass; + + void guardedByTypeSyntaxOk1() { + otherClass.lock.lock(); + guardedByLock1 = true; + guardedByLock2 = true; + otherClass.lock.unlock(); + } + + void guardedByTypeSyntaxOk2() { + synchronized (otherClass.otherClassObject) { + guardedByLock3 = true; + } + } + + void guardedByTypeSyntaxBad() { + guardedByLock1 = true; + guardedByLock2 = true; + } + } diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index b4c6c84fe..ea6653016 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -131,6 +131,8 @@ GuardedByExample.java, String GuardedByExample$4.readFromInnerClassBad2(), 1, UN GuardedByExample.java, void GuardedByExample$Sub.badSub(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure badSub()] GuardedByExample.java, void GuardedByExample.badGuardedByNormalLock(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure badGuardedByNormalLock()] GuardedByExample.java, void GuardedByExample.badGuardedByReentrantLock(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure badGuardedByReentrantLock()] +GuardedByExample.java, void GuardedByExample.guardedByTypeSyntaxBad(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure guardedByTypeSyntaxBad()] +GuardedByExample.java, void GuardedByExample.guardedByTypeSyntaxBad(), 2, UNSAFE_GUARDED_BY_ACCESS, [start of procedure guardedByTypeSyntaxBad()] GuardedByExample.java, void GuardedByExample.readFAfterBlockBad(), 3, UNSAFE_GUARDED_BY_ACCESS, [start of procedure readFAfterBlockBad()] GuardedByExample.java, void GuardedByExample.readFBad(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure readFBad()] GuardedByExample.java, void GuardedByExample.readFBadButSuppressedOther(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure readFBadButSuppressedOther()]