pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[guarded-by] support `Classname.fieldname` syntax

Browse Source 
Summary:
Developers will sometimes write GuardedBy("T.f") with the intended semantics: "guarded by the field f of the object with type T in the current state".
We want to support this to avoid false positives.

Reviewed By: peterogithub

Differential Revision: D4197476

fbshipit-source-id: acd00d9
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent a2f9ce3f23
commit a6121a9fb0
4 changed files with 101 additions and 21 deletions
Show Stats Download Patch File Download Diff File

73
infer/src/backend/rearrange.ml
Unescape View File

@ -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)
| _ ->

2
infer/tests/build_systems/ant/issues.exp
Unescape View File

@ -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()]

45
infer/tests/codetoanalyze/java/infer/GuardedByExample.java
Unescape View File

@ -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;
}
}

2
infer/tests/codetoanalyze/java/infer/issues.exp
Unescape View File

@ -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()]

Write Preview
Loading…
Cancel
Save