-
Notifications
You must be signed in to change notification settings - Fork 62
/
Copy pathPossibleDataRaceBetweenThreads.ql
158 lines (142 loc) · 4.54 KB
/
PossibleDataRaceBetweenThreads.ql
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
156
157
158
/**
* @id c/misra/possible-data-race-between-threads
* @name DIR-5-1: There shall be no data races between threads
* @description Threads shall not access the same memory location concurrently without utilization
* of thread synchronization objects.
* @kind problem
* @precision medium
* @problem.severity error
* @tags external/misra/id/dir-5-1
* correctness
* concurrency
* external/misra/c/2012/amendment4
* external/misra/obligation/required
*/
import cpp
import codingstandards.c.misra
import codingstandards.c.Objects
import codingstandards.c.SubObjects
import codingstandards.cpp.Concurrency
newtype TNonReentrantOperation =
TReadWrite(SubObject object) {
object.getRootIdentity().getStorageDuration().isStatic()
or
object.getRootIdentity().getStorageDuration().isAllocated()
} or
TStdFunctionCall(FunctionCall call) {
call.getTarget()
.hasName([
"setlocale", "tmpnam", "rand", "srand", "getenv", "getenv_s", "strok", "strerror",
"asctime", "ctime", "gmtime", "localtime", "mbrtoc16", "c16rtomb", "mbrtoc32",
"c32rtomb", "mbrlen", "mbrtowc", "wcrtomb", "mbsrtowcs", "wcsrtombs"
])
}
class NonReentrantOperation extends TNonReentrantOperation {
string toString() {
exists(SubObject object |
this = TReadWrite(object) and
result = object.toString()
)
or
exists(FunctionCall call |
this = TStdFunctionCall(call) and
result = call.getTarget().getName()
)
}
Expr getARead() {
exists(SubObject object |
this = TReadWrite(object) and
result = object.getAnAccess()
)
or
this = TStdFunctionCall(result)
}
Expr getAWrite() {
exists(SubObject object, Assignment assignment |
this = TReadWrite(object) and
result = assignment and
assignment.getLValue() = object.getAnAccess()
)
or
this = TStdFunctionCall(result)
}
string getReadString() {
this = TReadWrite(_) and
result = "read operation"
or
this = TStdFunctionCall(_) and
result = "call to non-reentrant function"
}
string getWriteString() {
this = TReadWrite(_) and
result = "write to object"
or
this = TStdFunctionCall(_) and
result = "call to non-reentrant function"
}
Element getSourceElement() {
exists(SubObject object |
this = TReadWrite(object) and
result = object.getRootIdentity()
)
or
this = TStdFunctionCall(result)
}
}
class WritingThread extends ThreadedFunction {
NonReentrantOperation aWriteObject;
Expr aWrite;
WritingThread() {
aWrite = aWriteObject.getAWrite() and
this.calls*(aWrite.getEnclosingFunction()) and
not aWrite instanceof LockProtectedControlFlowNode and
not aWrite.getEnclosingFunction().getName().matches(["%init%", "%boot%", "%start%"])
}
Expr getAWrite() { result = aWrite }
}
class ReadingThread extends ThreadedFunction {
Expr aReadExpr;
ReadingThread() {
exists(NonReentrantOperation op |
aReadExpr = op.getARead() and
this.calls*(aReadExpr.getEnclosingFunction()) and
not aReadExpr instanceof LockProtectedControlFlowNode
)
}
Expr getARead() { result = aReadExpr }
}
predicate mayBeDataRace(Expr write, Expr read, NonReentrantOperation operation) {
exists(WritingThread wt |
wt.getAWrite() = write and
write = operation.getAWrite() and
exists(ReadingThread rt |
read = rt.getARead() and
read = operation.getARead() and
(
wt.isMultiplySpawned() or
not wt = rt
)
)
)
}
from
WritingThread wt, ReadingThread rt, Expr write, Expr read, NonReentrantOperation operation,
string message, string writeString, string readString
where
not isExcluded(write, Concurrency9Package::possibleDataRaceBetweenThreadsQuery()) and
mayBeDataRace(write, read, operation) and
wt = min(WritingThread f | f.getAWrite() = write | f order by f.getName()) and
rt = min(ReadingThread f | f.getARead() = read | f order by f.getName()) and
writeString = operation.getWriteString() and
readString = operation.getReadString() and
if wt.isMultiplySpawned()
then
message =
"Threaded " + writeString +
" $@ not synchronized, for example from thread function $@ spawned from a loop."
else
message =
"Threaded " + writeString +
" $@, for example from thread function $@, not synchronized with $@, for example from thread function $@."
select write, message, operation.getSourceElement(), operation.toString(), wt, wt.getName(), read,
"concurrent " + readString, rt, rt.getName()