Skip to content

Commit 3e3ea7d

Browse files
Implement Concurrency9 package on top of Concurrency8 work
1 parent 6ad3660 commit 3e3ea7d

File tree

54 files changed

+2824
-1090
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

54 files changed

+2824
-1090
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
import codingstandards.c.Objects
2+
3+
newtype TSubObject =
4+
TObjectRoot(ObjectIdentity i) or
5+
TObjectMember(SubObject struct, MemberVariable m) {
6+
m = struct.getType().(Struct).getAMemberVariable()
7+
} or
8+
TObjectIndex(SubObject array) { array.getType() instanceof ArrayType }
9+
10+
class SubObject extends TSubObject {
11+
string toString() {
12+
exists(ObjectIdentity i |
13+
this = TObjectRoot(i) and
14+
result = i.toString()
15+
)
16+
or
17+
exists(SubObject struct, Variable m |
18+
this = TObjectMember(struct, m) and
19+
result = struct.toString() + "." + m.getName()
20+
)
21+
or
22+
exists(SubObject array |
23+
this = TObjectIndex(array) and
24+
result = array.toString()
25+
)
26+
}
27+
28+
Type getType() {
29+
exists(ObjectIdentity i |
30+
this = TObjectRoot(i) and
31+
result = i.getType()
32+
)
33+
or
34+
exists(Variable m |
35+
this = TObjectMember(_, m) and
36+
result = m.getType()
37+
)
38+
or
39+
exists(SubObject array |
40+
this = TObjectIndex(array) and
41+
result = array.getType().(ArrayType).getBaseType()
42+
)
43+
}
44+
45+
/**
46+
* Holds for object roots and for member accesses on that root, not for array accesses.
47+
*
48+
* This is useful for cases where we do not wish to treat `x[y]` and `x[z]` as the same object.
49+
*/
50+
predicate isPrecise() {
51+
not getParent*() = TObjectIndex(_)
52+
}
53+
54+
SubObject getParent() {
55+
exists(SubObject struct, MemberVariable m |
56+
this = TObjectMember(struct, m) and
57+
result = struct
58+
)
59+
or
60+
exists(SubObject array |
61+
this = TObjectIndex(array) and
62+
result = array
63+
)
64+
}
65+
66+
Expr getAnAccess() {
67+
exists(ObjectIdentity i |
68+
this = TObjectRoot(i) and
69+
result = i.getAnAccess()
70+
)
71+
or
72+
exists(MemberVariable m |
73+
this = TObjectMember(_, m) and
74+
result = m.getAnAccess() and
75+
result.(DotFieldAccess).getQualifier() = getParent().getAnAccess()
76+
)
77+
or
78+
this = TObjectIndex(_) and
79+
result.(ArrayExpr).getArrayBase() = getParent().getAnAccess()
80+
}
81+
82+
AddressOfExpr getAnAddressOfExpr() {
83+
result.getOperand() = this.getAnAccess()
84+
}
85+
86+
ObjectIdentity getRootIdentity() {
87+
exists(ObjectIdentity i |
88+
this = TObjectRoot(i) and
89+
result = i
90+
)
91+
or
92+
result = getParent().getRootIdentity()
93+
}
94+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
import cpp
2+
import codingstandards.c.Objects
3+
import codingstandards.cpp.Concurrency
4+
import codingstandards.cpp.Type
5+
6+
signature module GlobalInitializationAnalysisConfigSig {
7+
/** A function which is not called or started as a thread */
8+
default predicate isRootFunction(Function f) {
9+
not exists(Function f2 | f2.calls(f)) and
10+
not f instanceof ThreadedFunction
11+
}
12+
13+
ObjectIdentity getAnInitializedObject(Expr e);
14+
15+
ObjectIdentity getAUsedObject(Expr e);
16+
}
17+
18+
module GlobalInitalizationAnalysis<GlobalInitializationAnalysisConfigSig Config> {
19+
final class FinalFunction = Function;
20+
21+
final class FinalExpr = Expr;
22+
23+
class RootFunction extends FinalFunction {
24+
RootFunction() { Config::isRootFunction(this) }
25+
}
26+
27+
/** A function call which initializes a mutex or a condition */
28+
class ObjectInit extends FinalExpr {
29+
ObjectIdentity owningObject;
30+
31+
ObjectInit() { owningObject = Config::getAnInitializedObject(this) }
32+
33+
ObjectIdentity getOwningObject() { result = owningObject }
34+
}
35+
36+
/**
37+
* A function argument where that argument is used as a mutex or condition object.
38+
*/
39+
class ObjectUse extends FinalExpr {
40+
ObjectIdentity owningObject;
41+
42+
ObjectUse() { owningObject = Config::getAUsedObject(this) }
43+
44+
ObjectIdentity getOwningObject() { result = owningObject }
45+
}
46+
47+
predicate requiresInitializedMutexObject(
48+
Function func, ObjectUse mutexUse, ObjectIdentity owningObject
49+
) {
50+
mutexUse.getEnclosingFunction() = func and
51+
owningObject = mutexUse.getOwningObject() and
52+
not exists(ObjectInit init |
53+
init.getEnclosingFunction() = func and
54+
init.getOwningObject() = owningObject and
55+
mutexUse.getAPredecessor+() = init
56+
)
57+
or
58+
exists(FunctionCall call |
59+
func = call.getEnclosingFunction() and
60+
requiresInitializedMutexObject(call.getTarget(), mutexUse, owningObject) and
61+
not exists(ObjectInit init |
62+
call.getAPredecessor*() = init and
63+
init.getOwningObject() = owningObject
64+
)
65+
)
66+
or
67+
exists(C11ThreadCreateCall call |
68+
func = call.getEnclosingFunction() and
69+
not owningObject.getStorageDuration().isThread() and
70+
requiresInitializedMutexObject(call.getFunction(), mutexUse, owningObject) and
71+
not exists(ObjectInit init |
72+
call.getAPredecessor*() = init and
73+
init.getOwningObject() = owningObject
74+
)
75+
)
76+
}
77+
78+
predicate uninitializedFrom(Expr e, ObjectIdentity obj, Function callRoot) {
79+
exists(ObjectUse use | use = e |
80+
obj = use.getOwningObject() and
81+
requiresInitializedMutexObject(callRoot, use, obj) and
82+
(
83+
if obj.getStorageDuration().isAutomatic()
84+
then obj.getEnclosingElement+() = callRoot
85+
else (
86+
obj.getStorageDuration().isThread() and callRoot instanceof ThreadedFunction
87+
or
88+
callRoot instanceof RootFunction
89+
)
90+
)
91+
)
92+
}
93+
}

c/common/test/includes/standard-library/stdlib.h

+1
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@ int at_quick_exit (void (*) (void));
4949
_Noreturn void quick_exit (int);
5050

5151
char *getenv (const char *);
52+
char *getenv_s (size_t *restrict len, char *restrict value, size_t valuesz, const char *restrict name);
5253

5354
int system (const char *);
5455

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
/**
2+
* @id c/misra/possible-data-race-between-threads
3+
* @name DIR-5-1: There shall be no data races between threads
4+
* @description Threads shall not access the same memory location concurrently without utilization
5+
* of thread synchronization objects.
6+
* @kind problem
7+
* @precision medium
8+
* @problem.severity error
9+
* @tags external/misra/id/dir-5-1
10+
* correctness
11+
* concurrency
12+
* external/misra/c/2012/amendment4
13+
* external/misra/obligation/required
14+
*/
15+
16+
import cpp
17+
import codingstandards.c.misra
18+
import codingstandards.c.Objects
19+
import codingstandards.c.SubObjects
20+
import codingstandards.cpp.Concurrency
21+
22+
newtype TNonReentrantOperation =
23+
TReadWrite(SubObject object) {
24+
object.getRootIdentity().getStorageDuration().isStatic()
25+
or
26+
object.getRootIdentity().getStorageDuration().isAllocated()
27+
} or
28+
TStdFunctionCall(FunctionCall call) {
29+
call.getTarget()
30+
.hasName([
31+
"setlocale", "tmpnam", "rand", "srand", "getenv", "getenv_s", "strok", "strerror",
32+
"asctime", "ctime", "gmtime", "localtime", "mbrtoc16", "c16rtomb", "mbrtoc32",
33+
"c32rtomb", "mbrlen", "mbrtowc", "wcrtomb", "mbsrtowcs", "wcsrtombs"
34+
])
35+
}
36+
37+
class NonReentrantOperation extends TNonReentrantOperation {
38+
string toString() {
39+
exists(SubObject object |
40+
this = TReadWrite(object) and
41+
result = object.toString()
42+
)
43+
or
44+
exists(FunctionCall call |
45+
this = TStdFunctionCall(call) and
46+
result = call.getTarget().getName()
47+
)
48+
}
49+
50+
Expr getARead() {
51+
exists(SubObject object |
52+
this = TReadWrite(object) and
53+
result = object.getAnAccess()
54+
)
55+
or
56+
this = TStdFunctionCall(result)
57+
}
58+
59+
Expr getAWrite() {
60+
exists(SubObject object, Assignment assignment |
61+
this = TReadWrite(object) and
62+
result = assignment and
63+
assignment.getLValue() = object.getAnAccess()
64+
)
65+
or
66+
this = TStdFunctionCall(result)
67+
}
68+
69+
string getReadString() {
70+
this = TReadWrite(_) and
71+
result = "read operation"
72+
or
73+
this = TStdFunctionCall(_) and
74+
result = "call to non-reentrant function"
75+
}
76+
77+
string getWriteString() {
78+
this = TReadWrite(_) and
79+
result = "write to object"
80+
or
81+
this = TStdFunctionCall(_) and
82+
result = "call to non-reentrant function"
83+
}
84+
85+
Element getSourceElement() {
86+
exists(SubObject object |
87+
this = TReadWrite(object) and
88+
result = object.getRootIdentity()
89+
)
90+
or
91+
this = TStdFunctionCall(result)
92+
}
93+
}
94+
95+
class WritingThread extends ThreadedFunction {
96+
NonReentrantOperation aWriteObject;
97+
Expr aWrite;
98+
99+
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%"])
104+
}
105+
106+
Expr getAWrite() { result = aWrite }
107+
}
108+
109+
class ReadingThread extends ThreadedFunction {
110+
Expr aReadExpr;
111+
112+
ReadingThread() {
113+
exists(NonReentrantOperation op |
114+
aReadExpr = op.getARead() and
115+
this.calls*(aReadExpr.getEnclosingFunction()) and
116+
not aReadExpr instanceof LockProtectedControlFlowNode
117+
)
118+
}
119+
120+
Expr getARead() { result = aReadExpr }
121+
}
122+
123+
predicate mayBeDataRace(Expr write, Expr read, NonReentrantOperation operation) {
124+
exists(WritingThread wt |
125+
wt.getAWrite() = write and
126+
write = operation.getAWrite() and
127+
exists(ReadingThread rt |
128+
read = rt.getARead() and
129+
read = operation.getARead() and
130+
(
131+
wt.isMultiplySpawned() or
132+
not wt = rt
133+
)
134+
)
135+
)
136+
}
137+
138+
from
139+
WritingThread wt, ReadingThread rt, Expr write, Expr read, NonReentrantOperation operation,
140+
string message, string writeString, string readString
141+
where
142+
not isExcluded(write, Concurrency9Package::possibleDataRaceBetweenThreadsQuery()) and
143+
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
146+
writeString = operation.getWriteString() and
147+
readString = operation.getReadString() and
148+
if wt.isMultiplySpawned()
149+
then
150+
message =
151+
"Threaded " + writeString +
152+
" $@ not synchronized, for example from thread function $@ spawned from a loop."
153+
else
154+
message =
155+
"Threaded " + writeString +
156+
" $@, for example from thread function $@, not synchronized with $@, for example from thread function $@."
157+
select write, message, operation.getSourceElement(), operation.toString(), wt, wt.getName(), read,
158+
"concurrent " + readString, rt, rt.getName()

0 commit comments

Comments
 (0)