1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
package chapter;
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.type.invalid) :: error: (super.invocation.invalid)
// :: warning: (inconsistent.constructor.type)
@GuardedBy("lock") class MyClass3 {}
@GuardedBy({}) class MyClass4 {}
// :: error: (guardsatisfied.location.disallowed) :: error: (super.invocation.invalid)
// :: warning: (inconsistent.constructor.type)
@GuardSatisfied class MyClass5 {}
// :: error: (super.invocation.invalid) :: warning: (inconsistent.constructor.type)
@GuardedByBottom class MyClass6 {}
}
|
