@@ -103,6 +103,7 @@ module Monitors {
103103 )
104104 }
105105
106+ /** Gets the control flow node that must dominate `e` when `e` is synchronized on a lock. */
106107 ControlFlowNode getNodeToBeDominated ( Expr e ) {
107108 // If `e` is the LHS of an assignment, use the control flow node for the assignment
108109 exists ( Assignment asgn | asgn .getDest ( ) = e | result = asgn .getControlFlowNode ( ) )
@@ -153,13 +154,13 @@ module Modification {
153154
154155/** Holds if the type `t` is thread-safe. */
155156predicate isThreadSafeType ( Type t ) {
156- t .getErasure ( ) .getName ( ) .matches ( [ "Atomic%" , "Concurrent%" ] )
157+ t .( RefType ) . getSourceDeclaration ( ) .getName ( ) .matches ( [ "Atomic%" , "Concurrent%" ] )
157158 or
158- t .getErasure ( ) .getName ( ) in [ "ThreadLocal" ]
159+ t .( RefType ) . getSourceDeclaration ( ) .getName ( ) in [ "ThreadLocal" ]
159160 or
160161 // Anything in `java.itul.concurrent` is thread safe.
161162 // See https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/package-summary.html#MemoryVisibility
162- t .getTypeDescriptor ( ) . matches ( "Ljava/ util/ concurrent/%;" )
163+ t .( RefType ) . getPackage ( ) . getName ( ) = "java. util. concurrent"
163164 or
164165 t instanceof ClassAnnotatedAsThreadSafe
165166}
@@ -170,27 +171,38 @@ predicate isThreadSafeInitializer(Expr e) {
170171}
171172
172173/**
173- * A field access that is exposed to potential data races.
174+ * A field that is exposed to potential data races.
174175 * We require the field to be in a class that is annotated as `@ThreadSafe`.
175176 */
176- class ExposedFieldAccess extends FieldAccess {
177- ExposedFieldAccess ( ) {
178- this .getField ( ) = any ( ClassAnnotatedAsThreadSafe c ) . getAField ( ) and
179- not this .getField ( ) . isVolatile ( ) and
177+ class ExposedField extends Field {
178+ ExposedField ( ) {
179+ this .getDeclaringType ( ) instanceof ClassAnnotatedAsThreadSafe and
180+ not this .isVolatile ( ) and
180181 // field is not a lock
181- not isLockType ( this .getField ( ) . getType ( ) ) and
182+ not isLockType ( this .getType ( ) ) and
182183 // field is not thread-safe
183- not isThreadSafeType ( this .getField ( ) . getType ( ) ) and
184- not isThreadSafeType ( this .getField ( ) . getInitializer ( ) .getType ( ) ) and
184+ not isThreadSafeType ( this .getType ( ) ) and
185+ not isThreadSafeType ( this .getInitializer ( ) .getType ( ) ) and
185186 // the initializer guarantees thread safety
186- not isThreadSafeInitializer ( this .getField ( ) .getInitializer ( ) ) and
187+ not isThreadSafeInitializer ( this .getInitializer ( ) )
188+ }
189+ }
190+
191+ /**
192+ * A field access that is exposed to potential data races.
193+ * We require the field to be in a class that is annotated as `@ThreadSafe`.
194+ */
195+ class ExposedFieldAccess extends FieldAccess {
196+ ExposedFieldAccess ( ) {
197+ // access is to an exposed field
198+ this .getField ( ) instanceof ExposedField and
187199 // access is not the initializer of the field
188200 not this .( VarWrite ) .getASource ( ) = this .getField ( ) .getInitializer ( ) and
189201 // access not in a constructor
190202 not this .getEnclosingCallable ( ) = this .getField ( ) .getDeclaringType ( ) .getAConstructor ( ) and
191203 // not a field on a local variable
192204 not this .getQualifier + ( ) .( VarAccess ) .getVariable ( ) instanceof LocalVariableDecl and
193- // not the variable mention in a synchronized statement
205+ // not the variable mentioned in a synchronized statement
194206 not this = any ( SynchronizedStmt sync ) .getExpr ( )
195207 }
196208}
0 commit comments