diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli index b7e8bc2a8..0c7f150be 100644 --- a/infer/src/checkers/AbstractDomain.mli +++ b/infer/src/checkers/AbstractDomain.mli @@ -47,3 +47,7 @@ module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key include S with type astate = ValueDomain.astate Map.t end + +(** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's + true in both branches. *) +module BooleanAnd : S with type astate = bool diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 7934fe90c..454c0dd4c 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -40,21 +40,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct pathdomainstate (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) - let exec_instr ((lockstate,(readstate,writestate)) as astate) { ProcData.pdesc; } _ = - let is_unprotected lockstate = - (not (Procdesc.is_java_synchronized pdesc)) && - (ThreadSafetyDomain.LocksDomain.is_empty lockstate) - in + let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ = + let is_unprotected is_locked = + not is_locked && not (Procdesc.is_java_synchronized pdesc) in function | Sil.Call (_, Const (Cfun pn), _, _, _) -> if is_lock_procedure pn - then - ((ThreadSafetyDomain.LocksDomain.add "locked" lockstate), (readstate,writestate)) + then true, (readstate,writestate) else if is_unlock_procedure pn - then - ((ThreadSafetyDomain.LocksDomain.remove "locked" lockstate) , (readstate,writestate)) - else - astate + then false, (readstate,writestate) + else astate | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, _) -> if is_unprotected lockstate then (* abstracts no lock being held*) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 0376c6299..92c5f1b4d 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -12,7 +12,12 @@ module PPrawpath = PrettyPrintable.MakePPSet(struct let pp_element = AccessPath.pp_raw end) -module LocksDomain = AbstractDomain.FiniteSet(Utils.StringPPSet) +(** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes + the existence of one global lock. In the case that a lock is held on the access to a variable, + but the lock held is the wrong one, we will erroneously say that the access is thread-safe. + However, this coarse abstraction saves us from the complexity of tracking which locks are held + and which memory locations correspond to the same lock. *) +module LocksDomain = AbstractDomain.BooleanAnd module PathDomain = AbstractDomain.FiniteSet(PPrawpath) diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml index bd5caca74..8b3834838 100644 --- a/infer/src/checkers/abstractDomain.ml +++ b/infer/src/checkers/abstractDomain.ml @@ -142,3 +142,19 @@ module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct let pp fmt astate = M.pp ~pp_value:ValueDomain.pp fmt astate end + +module BooleanAnd = struct + type astate = bool + + let initial = false + + let (<=) ~lhs ~rhs = lhs || not rhs + + let join = (&&) + + let widen ~prev ~next ~num_iters:_ = + join prev next + + let pp fmt astate = + F.fprintf fmt "%b" astate +end diff --git a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java index 931e467b0..668af7a93 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java +++ b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java @@ -15,6 +15,8 @@ import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; +import java.util.concurrent.locks.Lock; + @Documented @Target(ElementType.TYPE) @Retention(RetentionPolicy.CLASS) @@ -43,6 +45,36 @@ public class ThreadSafeExample{ f = 24; } + Lock mLock; + + public void tsBadInOneBranch(boolean b) { + if (b) { + mLock.lock(); + } + f = 24; + if (b) { + mLock.unlock(); + } + } + + // doesn't work because we don't model lock + public void FP_tsWithLockOk() { + mLock.lock(); + f = 42; + mLock.unlock(); + } + + // doesn't work because we don't model lock + public void FP_tsWithLockBothBranchesOk(boolean b) { + if (b) { + mLock.lock(); + } else { + mLock.lock(); + } + f = 42; + mLock.unlock(); + } + } class ExtendsThreadSafeExample extends ThreadSafeExample{ diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index b54949c18..93ea1fa04 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -2,4 +2,7 @@ codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeEx Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.tsOK() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization. Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_tsWithLockBothBranchesOk(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_tsWithLockBothBranchesOk(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_tsWithLockOk(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_tsWithLockOk() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBadInOneBranch(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBadInOneBranch(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ]