@@ -47,7 +47,7 @@ class NonReentrantOperation extends TNonReentrantOperation {
4747 )
4848 }
4949
50- Expr getARead ( ) {
50+ Expr getAReadExpr ( ) {
5151 exists ( SubObject object |
5252 this = TReadWrite ( object ) and
5353 result = object .getAnAccess ( )
@@ -56,7 +56,7 @@ class NonReentrantOperation extends TNonReentrantOperation {
5656 this = TStdFunctionCall ( result )
5757 }
5858
59- Expr getAWrite ( ) {
59+ Expr getAWriteExpr ( ) {
6060 exists ( SubObject object , Assignment assignment |
6161 this = TReadWrite ( object ) and
6262 result = assignment and
@@ -94,39 +94,43 @@ class NonReentrantOperation extends TNonReentrantOperation {
9494
9595class WritingThread extends ThreadedFunction {
9696 NonReentrantOperation aWriteObject ;
97- Expr aWrite ;
97+ Expr aWriteExpr ;
9898
9999 WritingThread ( ) {
100- aWrite = aWriteObject .getAWrite ( ) and
101- this .calls * ( aWrite .getEnclosingFunction ( ) ) and
102- not aWrite instanceof LockProtectedControlFlowNode and
103- not aWrite .getEnclosingFunction ( ) .getName ( ) .matches ( [ "%init%" , "%boot%" , "%start%" ] )
100+ aWriteExpr = aWriteObject .getAWriteExpr ( ) and
101+ // This function directly contains the write expression, or transitively calls the function
102+ // that contains the write expression.
103+ this .calls * ( aWriteExpr .getEnclosingFunction ( ) ) and
104+ // The write isn't synchronized with a mutex or condition object.
105+ not aWriteExpr instanceof LockProtectedControlFlowNode and
106+ // The write doesn't seem to be during a special initialization phase of the program.
107+ not aWriteExpr .getEnclosingFunction ( ) .getName ( ) .matches ( [ "%init%" , "%boot%" , "%start%" ] )
104108 }
105109
106- Expr getAWrite ( ) { result = aWrite }
110+ Expr getAWriteExpr ( ) { result = aWriteExpr }
107111}
108112
109113class ReadingThread extends ThreadedFunction {
110114 Expr aReadExpr ;
111115
112116 ReadingThread ( ) {
113117 exists ( NonReentrantOperation op |
114- aReadExpr = op .getARead ( ) and
118+ aReadExpr = op .getAReadExpr ( ) and
115119 this .calls * ( aReadExpr .getEnclosingFunction ( ) ) and
116120 not aReadExpr instanceof LockProtectedControlFlowNode
117121 )
118122 }
119123
120- Expr getARead ( ) { result = aReadExpr }
124+ Expr getAReadExpr ( ) { result = aReadExpr }
121125}
122126
123127predicate mayBeDataRace ( Expr write , Expr read , NonReentrantOperation operation ) {
124128 exists ( WritingThread wt |
125- wt .getAWrite ( ) = write and
126- write = operation .getAWrite ( ) and
129+ wt .getAWriteExpr ( ) = write and
130+ write = operation .getAWriteExpr ( ) and
127131 exists ( ReadingThread rt |
128- read = rt .getARead ( ) and
129- read = operation .getARead ( ) and
132+ read = rt .getAReadExpr ( ) and
133+ read = operation .getAReadExpr ( ) and
130134 (
131135 wt .isMultiplySpawned ( ) or
132136 not wt = rt
@@ -141,18 +145,18 @@ from
141145where
142146 not isExcluded ( write , Concurrency9Package:: possibleDataRaceBetweenThreadsQuery ( ) ) and
143147 mayBeDataRace ( write , read , operation ) and
144- wt = min ( WritingThread f | f .getAWrite ( ) = write | f order by f .getName ( ) ) and
145- rt = min ( ReadingThread f | f .getARead ( ) = read | f order by f .getName ( ) ) and
148+ wt = min ( WritingThread f | f .getAWriteExpr ( ) = write | f order by f .getName ( ) ) and
149+ rt = min ( ReadingThread f | f .getAReadExpr ( ) = read | f order by f .getName ( ) ) and
146150 writeString = operation .getWriteString ( ) and
147151 readString = operation .getReadString ( ) and
148152 if wt .isMultiplySpawned ( )
149153 then
150154 message =
151155 "Threaded " + writeString +
152- " $@ not synchronized, for example from thread function $@ spawned from a loop."
156+ " $@ not synchronized from thread function $@ spawned from a loop."
153157 else
154158 message =
155159 "Threaded " + writeString +
156- " $@, for example from thread function $@, not synchronized with $@, for example from thread function $@."
160+ " $@ from thread function $@ is not synchronized with $@ from thread function $@."
157161select write , message , operation .getSourceElement ( ) , operation .toString ( ) , wt , wt .getName ( ) , read ,
158162 "concurrent " + readString , rt , rt .getName ( )
0 commit comments