| import java.util.concurrent.locks.ReentrantLock; |
| import org.checkerframework.checker.lock.qual.GuardSatisfied; |
| import org.checkerframework.checker.lock.qual.GuardedBy; |
| import org.checkerframework.checker.lock.qual.GuardedByBottom; |
| import org.checkerframework.checker.lock.qual.GuardedByUnknown; |
| import org.checkerframework.checker.lock.qual.LockingFree; |
| import org.checkerframework.checker.lock.qual.MayReleaseLocks; |
| import org.checkerframework.checker.lock.qual.ReleasesNoLocks; |
| import org.checkerframework.dataflow.qual.Pure; |
| import org.checkerframework.dataflow.qual.SideEffectFree; |
| |
| public class LockEffectAnnotations { |
| class MyClass { |
| Object field = new Object(); |
| } |
| |
| private @GuardedBy({}) MyClass myField; |
| |
| private final ReentrantLock myLock2 = new ReentrantLock(); |
| private @GuardedBy("myLock2") MyClass x3; |
| |
| // This method does not use locks or synchronization but cannot |
| // be annotated as @SideEffectFree since it alters myField. |
| @LockingFree |
| void myMethod5() { |
| myField = new MyClass(); |
| } |
| |
| @SideEffectFree |
| int mySideEffectFreeMethod() { |
| return 0; |
| } |
| |
| @MayReleaseLocks |
| void myUnlockingMethod() { |
| myLock2.unlock(); |
| } |
| |
| @MayReleaseLocks |
| void myReleaseLocksEmptyMethod() {} |
| |
| @MayReleaseLocks |
| // :: error: (guardsatisfied.with.mayreleaselocks) |
| void methodGuardSatisfiedReceiver(@GuardSatisfied LockEffectAnnotations this) {} |
| |
| @MayReleaseLocks |
| // :: error: (guardsatisfied.with.mayreleaselocks) |
| void methodGuardSatisfiedParameter(@GuardSatisfied Object o) {} |
| |
| @MayReleaseLocks |
| void myOtherMethod() { |
| if (myLock2.tryLock()) { |
| x3.field = new Object(); // OK: the lock is held |
| myMethod5(); |
| x3.field = new Object(); // OK: the lock is still held since myMethod is locking-free |
| mySideEffectFreeMethod(); |
| x3.field = new Object(); // OK: the lock is still held since mySideEffectFreeMethod is |
| // side-effect-free |
| myUnlockingMethod(); |
| // :: error: (lock.not.held) |
| x3.field = new Object(); // ILLEGAL: myLockingMethod is not locking-free |
| } |
| if (myLock2.tryLock()) { |
| x3.field = new Object(); // OK: the lock is held |
| myReleaseLocksEmptyMethod(); |
| // :: error: (lock.not.held) |
| x3.field = new Object(); // ILLEGAL: even though myUnannotatedEmptyMethod is empty, since |
| // myReleaseLocksEmptyMethod() is annotated with @MayReleaseLocks and the Lock Checker |
| // no longer knows the state of the lock. |
| if (myLock2.isHeldByCurrentThread()) { |
| x3.field = new Object(); // OK: the lock is known to be held |
| } |
| } |
| } |
| |
| @ReleasesNoLocks |
| void innerClassTest() { |
| class InnerClass { |
| @MayReleaseLocks |
| void innerClassMethod() {} |
| } |
| |
| InnerClass ic = new InnerClass(); |
| // :: error: (method.guarantee.violated) |
| ic.innerClassMethod(); |
| } |
| |
| @MayReleaseLocks |
| synchronized void mayReleaseLocksSynchronizedMethod() {} |
| |
| @ReleasesNoLocks |
| synchronized void releasesNoLocksSynchronizedMethod() {} |
| |
| @LockingFree |
| // :: error: (lockingfree.synchronized.method) |
| synchronized void lockingFreeSynchronizedMethod() {} |
| |
| @SideEffectFree |
| // :: error: (lockingfree.synchronized.method) |
| synchronized void sideEffectFreeSynchronizedMethod() {} |
| |
| @Pure |
| // :: error: (lockingfree.synchronized.method) |
| synchronized void pureSynchronizedMethod() {} |
| |
| @MayReleaseLocks |
| void mayReleaseLocksMethodWithSynchronizedBlock() { |
| synchronized (this) { |
| } |
| } |
| |
| @ReleasesNoLocks |
| void releasesNoLocksMethodWithSynchronizedBlock() { |
| synchronized (this) { |
| } |
| } |
| |
| @LockingFree |
| void lockingFreeMethodWithSynchronizedBlock() { |
| // :: error: (synchronized.block.in.lockingfree.method) |
| synchronized (this) { |
| } |
| } |
| |
| @SideEffectFree |
| void sideEffectFreeMethodWithSynchronizedBlock() { |
| // :: error: (synchronized.block.in.lockingfree.method) |
| synchronized (this) { |
| } |
| } |
| |
| @Pure |
| void pureMethodWithSynchronizedBlock() { |
| // :: error: (synchronized.block.in.lockingfree.method) |
| synchronized (this) { |
| } |
| } |
| |
| @GuardedByUnknown class MyClass2 {} |
| |
| // :: error: (expression.unparsable) :: error: (super.invocation) |
| // :: warning: (inconsistent.constructor.type) |
| @GuardedBy("lock") class MyClass3 {} |
| |
| @GuardedBy({}) class MyClass4 {} |
| // :: error: (guardsatisfied.location.disallowed) :: error: (super.invocation) |
| // :: warning: (inconsistent.constructor.type) |
| @GuardSatisfied class MyClass5 {} |
| |
| // :: error: (super.invocation) :: warning: (inconsistent.constructor.type) |
| @GuardedByBottom class MyClass6 {} |
| } |