@@ -44,11 +44,11 @@ predicate isThreadSafeType(Type t) {
4444
4545/** Holds if the expression `e` is a thread-safe initializer. */
4646predicate isThreadSafeInitializer ( Expr e ) {
47- e . ( Call )
48- . getCallee ( )
49- . getSourceDeclaration ( )
50- . getQualifiedName ( )
51- . matches ( "java.util.Collections.synchronized%" )
47+ exists ( string name |
48+ e . ( Call ) . getCallee ( ) . getSourceDeclaration ( ) . hasQualifiedName ( "java.util" , "Collections" , name )
49+ |
50+ name . matches ( "synchronized%" )
51+ )
5252}
5353
5454/**
@@ -132,7 +132,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
132132 * Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the method `m`.
133133 * We maintain the invariant that `m = e.getEnclosingCallable()`.
134134 */
135- predicate unlocked_access ( ExposedField f , Expr e , Method m , ExposedFieldAccess a , boolean write ) {
135+ predicate unlockedAccess ( ExposedField f , Expr e , Method m , ExposedFieldAccess a , boolean write ) {
136136 m .getDeclaringType ( ) = this and
137137 (
138138 // base case
@@ -143,7 +143,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
143143 ( if Modification:: isModifying ( a ) then write = true else write = false )
144144 or
145145 // recursive case
146- exists ( MethodCall c , Expr e0 , Method m0 | this .unlocked_access ( f , e0 , m0 , a , write ) |
146+ exists ( MethodCall c , Expr e0 , Method m0 | this .unlockedAccess ( f , e0 , m0 , a , write ) |
147147 m = c .getEnclosingCallable ( ) and
148148 not m0 .isPublic ( ) and
149149 c .getCallee ( ) .getSourceDeclaration ( ) = m0 and
@@ -154,38 +154,38 @@ class ClassAnnotatedAsThreadSafe extends Class {
154154 }
155155
156156 /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the method `m`. */
157- predicate has_unlocked_access ( ExposedField f , Expr e , Method m , boolean write ) {
158- this .unlocked_access ( f , e , m , _, write )
157+ predicate hasUnlockedAccess ( ExposedField f , Expr e , Method m , boolean write ) {
158+ this .unlockedAccess ( f , e , m , _, write )
159159 }
160160
161161 /** Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the public method `m`. */
162- predicate unlocked_public_access (
162+ predicate unlockedPublicAccess (
163163 ExposedField f , Expr e , Method m , ExposedFieldAccess a , boolean write
164164 ) {
165- this .unlocked_access ( f , e , m , a , write ) and
165+ this .unlockedAccess ( f , e , m , a , write ) and
166166 m .isPublic ( ) and
167167 not Monitors:: locallyMonitors ( e , _)
168168 }
169169
170170 /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the public method `m`. */
171- predicate has_unlocked_public_access ( ExposedField f , Expr e , Method m , boolean write ) {
172- this .unlocked_public_access ( f , e , m , _, write )
171+ predicate hasUnlockedPublicAccess ( ExposedField f , Expr e , Method m , boolean write ) {
172+ this .unlockedPublicAccess ( f , e , m , _, write )
173173 }
174174
175175 // Cases where all accesses to a field are protected by exactly one monitor
176176 //
177177 /**
178178 * Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the method `m`.
179179 */
180- predicate has_onelocked_access (
180+ predicate hasOnelockedAccess (
181181 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
182182 ) {
183183 //base
184- this .has_unlocked_access ( f , e , m , write ) and
184+ this .hasUnlockedAccess ( f , e , m , write ) and
185185 Monitors:: locallyMonitors ( e , monitor )
186186 or
187187 // recursive case
188- exists ( MethodCall c , Method m0 | this .has_onelocked_access ( f , _, m0 , write , monitor ) |
188+ exists ( MethodCall c , Method m0 | this .hasOnelockedAccess ( f , _, m0 , write , monitor ) |
189189 m = c .getEnclosingCallable ( ) and
190190 not m0 .isPublic ( ) and
191191 c .getCallee ( ) .getSourceDeclaration ( ) = m0 and
@@ -197,34 +197,33 @@ class ClassAnnotatedAsThreadSafe extends Class {
197197 }
198198
199199 /** Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the public method `m`. */
200- predicate has_onelocked_public_access (
200+ predicate hasOnelockedPublicAccess (
201201 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
202202 ) {
203- this .has_onelocked_access ( f , e , m , write , monitor ) and
203+ this .hasOnelockedAccess ( f , e , m , write , monitor ) and
204204 m .isPublic ( ) and
205- not this .has_unlocked_public_access ( f , e , m , write )
205+ not this .hasUnlockedPublicAccess ( f , e , m , write )
206206 }
207207
208208 /** Holds if the field `f` has more than one access, all locked by a single monitor, but different monitors are used. */
209- predicate single_monitor_mismatch ( ExposedField f ) {
210- 2 <=
211- strictcount ( Monitors:: Monitor monitor | this .has_onelocked_public_access ( f , _, _, _, monitor ) )
209+ predicate singleMonitorMismatch ( ExposedField f ) {
210+ 2 <= strictcount ( Monitors:: Monitor monitor | this .hasOnelockedPublicAccess ( f , _, _, _, monitor ) )
212211 }
213212
214213 // Cases where all accesses to a field are protected by at least one monitor
215214 //
216215 /** Holds if the class has an access, locked by at least one monitor, to the field `f` via the expression `e` in the method `m`. */
217- predicate has_onepluslocked_access (
216+ predicate hasOnepluslockedAccess (
218217 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
219218 ) {
220219 //base
221- this .has_onelocked_access ( f , e , m , write , monitor ) and
222- not this .single_monitor_mismatch ( f ) and
223- not this .has_unlocked_public_access ( f , _, _, _)
220+ this .hasOnelockedAccess ( f , e , m , write , monitor ) and
221+ not this .singleMonitorMismatch ( f ) and
222+ not this .hasUnlockedPublicAccess ( f , _, _, _)
224223 or
225224 // recursive case
226225 exists ( MethodCall c , Method m0 , Monitors:: Monitor monitor0 |
227- this .has_onepluslocked_access ( f , _, m0 , write , monitor0 ) and
226+ this .hasOnepluslockedAccess ( f , _, m0 , write , monitor0 ) and
228227 m = c .getEnclosingCallable ( ) and
229228 not m0 .isPublic ( ) and
230229 c .getCallee ( ) .getSourceDeclaration ( ) = m0 and
@@ -238,27 +237,27 @@ class ClassAnnotatedAsThreadSafe extends Class {
238237 }
239238
240239 /** Holds if the class has a write access to the field `f` that can be reached via a public method. */
241- predicate has_public_write_access ( ExposedField f ) {
242- this .has_unlocked_public_access ( f , _, _, true )
240+ predicate hasPublicWriteAccess ( ExposedField f ) {
241+ this .hasUnlockedPublicAccess ( f , _, _, true )
243242 or
244- this .has_onelocked_public_access ( f , _, _, true , _)
243+ this .hasOnelockedPublicAccess ( f , _, _, true , _)
245244 or
246245 exists ( Method m | m .getDeclaringType ( ) = this and m .isPublic ( ) |
247- this .has_onepluslocked_access ( f , _, m , true , _)
246+ this .hasOnepluslockedAccess ( f , _, m , true , _)
248247 )
249248 }
250249
251250 /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the method `m`. */
252- predicate escapes_monitor (
251+ predicate escapesMonitor (
253252 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
254253 ) {
255254 //base
256- this .has_onepluslocked_access ( f , _, _, _, monitor ) and
257- this .has_unlocked_access ( f , e , m , write ) and
255+ this .hasOnepluslockedAccess ( f , _, _, _, monitor ) and
256+ this .hasUnlockedAccess ( f , e , m , write ) and
258257 not Monitors:: locallyMonitors ( e , monitor )
259258 or
260259 // recursive case
261- exists ( MethodCall c , Method m0 | this .escapes_monitor ( f , _, m0 , write , monitor ) |
260+ exists ( MethodCall c , Method m0 | this .escapesMonitor ( f , _, m0 , write , monitor ) |
262261 m = c .getEnclosingCallable ( ) and
263262 not m0 .isPublic ( ) and
264263 c .getCallee ( ) .getSourceDeclaration ( ) = m0 and
@@ -269,17 +268,17 @@ class ClassAnnotatedAsThreadSafe extends Class {
269268 }
270269
271270 /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the public method `m`. */
272- predicate escapes_monitor_public (
271+ predicate escapesMonitorPublic (
273272 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
274273 ) {
275- this .escapes_monitor ( f , e , m , write , monitor ) and
274+ this .escapesMonitor ( f , e , m , write , monitor ) and
276275 m .isPublic ( )
277276 }
278277
279278 /** Holds if no monitor protects all accesses to the field `f`. */
280- predicate not_fully_monitored ( ExposedField f ) {
281- forex ( Monitors:: Monitor monitor | this .has_onepluslocked_access ( f , _, _, _, monitor ) |
282- this .escapes_monitor_public ( f , _, _, _, monitor )
279+ predicate notFullyMonitored ( ExposedField f ) {
280+ forex ( Monitors:: Monitor monitor | this .hasOnepluslockedAccess ( f , _, _, _, monitor ) |
281+ this .escapesMonitorPublic ( f , _, _, _, monitor )
283282 )
284283 }
285284}
0 commit comments