Skip to content

Commit 4ac7c5c

Browse files
lcarteylcartey
authored
Merge pull request #799 from github/michaelrfairhurst/implement-concurrency7-package
Implement Concurrency7 package
2 parents 2526a88 + 3eecfa0 commit 4ac7c5c

File tree

14 files changed

+503
-6
lines changed

14 files changed

+503
-6
lines changed

‎c/common/test/includes/standard-library/stdatomic.h

+1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
#define ATOMIC_VAR_INIT(value) (value)
2+
#define atomic_init __c11_atomic_init
23
#define atomic_is_lock_free(obj) __c11_atomic_is_lock_free(sizeof(*(obj)))
34
typedef _Atomic(int) atomic_int;
45

‎c/misra/src/rules/RULE-21-26/TimedlockOnInappropriateMutexType.ql

+76
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
/**
2+
* @id c/misra/timedlock-on-inappropriate-mutex-type
3+
* @name RULE-21-26: The Standard Library function mtx_timedlock() shall only be invoked on mutexes of type mtx_timed
4+
* @description The Standard Library function mtx_timedlock() shall only be invoked on mutex objects
5+
* of appropriate mutex type.
6+
* @kind path-problem
7+
* @precision high
8+
* @problem.severity error
9+
* @tags external/misra/id/rule-21-26
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 semmle.code.cpp.dataflow.new.DataFlow
19+
20+
class MutexTimed extends EnumConstant {
21+
MutexTimed() { hasName("mtx_timed") }
22+
}
23+
24+
class MutexInitCall extends FunctionCall {
25+
Expr mutexExpr;
26+
Expr mutexTypeExpr;
27+
28+
MutexInitCall() {
29+
getTarget().hasName("mtx_init") and
30+
mutexExpr = getArgument(0) and
31+
mutexTypeExpr = getArgument(1)
32+
}
33+
34+
predicate isTimedMutexType() {
35+
exists(EnumConstantAccess baseTypeAccess |
36+
(
37+
baseTypeAccess = mutexTypeExpr
38+
or
39+
baseTypeAccess = mutexTypeExpr.(BinaryBitwiseOperation).getAnOperand()
40+
) and
41+
baseTypeAccess.getTarget() instanceof MutexTimed
42+
)
43+
or
44+
mutexTypeExpr.getValue().toInt() = any(MutexTimed m).getValue().toInt()
45+
}
46+
47+
Expr getMutexExpr() { result = mutexExpr }
48+
}
49+
50+
module MutexTimedlockFlowConfig implements DataFlow::ConfigSig {
51+
predicate isSource(DataFlow::Node node) {
52+
exists(MutexInitCall init |
53+
node.asDefiningArgument() = init.getMutexExpr() and not init.isTimedMutexType()
54+
)
55+
}
56+
57+
predicate isSink(DataFlow::Node node) {
58+
exists(FunctionCall fc |
59+
fc.getTarget().hasName("mtx_timedlock") and
60+
node.asIndirectExpr() = fc.getArgument(0)
61+
)
62+
}
63+
}
64+
65+
module Flow = DataFlow::Global<MutexTimedlockFlowConfig>;
66+
67+
import Flow::PathGraph
68+
69+
from Flow::PathNode source, Flow::PathNode sink
70+
where
71+
not isExcluded(sink.getNode().asExpr(),
72+
Concurrency7Package::timedlockOnInappropriateMutexTypeQuery()) and
73+
Flow::flowPath(source, sink)
74+
select sink.getNode(), source, sink,
75+
"Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'.", source.getNode(),
76+
"initialized"

‎c/misra/src/rules/RULE-9-7/UninitializedAtomicObject.ql

+72
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
/**
2+
* @id c/misra/uninitialized-atomic-object
3+
* @name RULE-9-7: Atomic objects shall be appropriately initialized before being accessed
4+
* @description Atomic objects that do not have static storage duration shall be initialized with a
5+
* value or by using 'atomic_init()'.
6+
* @kind problem
7+
* @precision high
8+
* @problem.severity warning
9+
* @tags external/misra/id/rule-9-7
10+
* concurrency
11+
* external/misra/c/2012/amendment4
12+
* external/misra/obligation/mandatory
13+
*/
14+
15+
import cpp
16+
import codingstandards.c.misra
17+
import codingstandards.cpp.StdFunctionOrMacro
18+
import semmle.code.cpp.controlflow.Dominance
19+
20+
class ThreadSpawningFunction extends Function {
21+
ThreadSpawningFunction() {
22+
this.hasName("pthread_create")
23+
or
24+
this.hasName("thrd_create")
25+
or
26+
exists(FunctionCall fc |
27+
fc.getTarget() instanceof ThreadSpawningFunction and
28+
fc.getEnclosingFunction() = this
29+
)
30+
}
31+
}
32+
33+
class AtomicInitAddressOfExpr extends AddressOfExpr {
34+
AtomicInitAddressOfExpr() { exists(AtomicInitCall c | this = c.getArgument(0)) }
35+
}
36+
37+
ControlFlowNode getARequiredInitializationPoint(LocalScopeVariable v) {
38+
result = v.getParentScope().(BlockStmt).getFollowingStmt()
39+
or
40+
exists(DeclStmt decl |
41+
decl.getADeclaration() = v and
42+
result =
43+
any(FunctionCall fc |
44+
fc.getTarget() instanceof ThreadSpawningFunction and
45+
fc.getEnclosingBlock().getEnclosingBlock*() = v.getParentScope() and
46+
fc.getAPredecessor*() = decl
47+
)
48+
)
49+
}
50+
51+
from VariableDeclarationEntry decl, Variable v
52+
where
53+
not isExcluded(decl, Concurrency7Package::uninitializedAtomicObjectQuery()) and
54+
v = decl.getVariable() and
55+
v.getUnderlyingType().hasSpecifier("atomic") and
56+
not v.isTopLevel() and
57+
not exists(v.getInitializer()) and
58+
exists(ControlFlowNode missingInitPoint |
59+
missingInitPoint = getARequiredInitializationPoint(v) and
60+
// Check for `atomic_init(&v)`
61+
not exists(AtomicInitAddressOfExpr initialization |
62+
initialization.getOperand().(VariableAccess).getTarget() = v and
63+
dominates(initialization, missingInitPoint)
64+
) and
65+
// Check for `unknown_func(&v)` which may call `atomic_init` on `v`.
66+
not exists(FunctionCall fc |
67+
fc.getAnArgument().(AddressOfExpr).getOperand().(VariableAccess).getTarget() = v and
68+
dominates(fc, missingInitPoint)
69+
)
70+
)
71+
select decl,
72+
"Atomic object '" + v.getName() + "' has no initializer or corresponding use of 'atomic_init()'."

‎c/misra/test/rules/RULE-21-26/TimedlockOnInappropriateMutexType.expected

+45
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
edges
2+
| test.c:10:24:10:24 | *m | test.c:10:43:10:43 | *m | provenance | |
3+
| test.c:13:12:13:14 | mtx_init output argument | test.c:14:17:14:19 | *& ... | provenance | |
4+
| test.c:13:12:13:14 | mtx_init output argument | test.c:15:14:15:16 | *& ... | provenance | |
5+
| test.c:15:14:15:16 | *& ... | test.c:10:24:10:24 | *m | provenance | |
6+
| test.c:17:12:17:14 | mtx_init output argument | test.c:18:17:18:19 | *& ... | provenance | |
7+
| test.c:17:12:17:14 | mtx_init output argument | test.c:19:14:19:16 | *& ... | provenance | |
8+
| test.c:19:14:19:16 | *& ... | test.c:10:24:10:24 | *m | provenance | |
9+
| test.c:30:12:30:14 | mtx_init output argument | test.c:31:17:31:19 | *& ... | provenance | |
10+
| test.c:30:12:30:14 | mtx_init output argument | test.c:32:14:32:16 | *& ... | provenance | |
11+
| test.c:32:14:32:16 | *& ... | test.c:10:24:10:24 | *m | provenance | |
12+
| test.c:42:12:42:16 | mtx_init output argument | test.c:42:13:42:14 | *l3 [post update] [m] | provenance | |
13+
| test.c:42:13:42:14 | *l3 [post update] [m] | test.c:43:18:43:19 | *l3 [m] | provenance | |
14+
| test.c:42:13:42:14 | *l3 [post update] [m] | test.c:44:15:44:16 | *l3 [m] | provenance | |
15+
| test.c:43:18:43:19 | *l3 [m] | test.c:43:17:43:21 | *& ... | provenance | |
16+
| test.c:44:14:44:18 | *& ... | test.c:10:24:10:24 | *m | provenance | |
17+
| test.c:44:15:44:16 | *l3 [m] | test.c:44:14:44:18 | *& ... | provenance | |
18+
nodes
19+
| test.c:10:24:10:24 | *m | semmle.label | *m |
20+
| test.c:10:43:10:43 | *m | semmle.label | *m |
21+
| test.c:13:12:13:14 | mtx_init output argument | semmle.label | mtx_init output argument |
22+
| test.c:14:17:14:19 | *& ... | semmle.label | *& ... |
23+
| test.c:15:14:15:16 | *& ... | semmle.label | *& ... |
24+
| test.c:17:12:17:14 | mtx_init output argument | semmle.label | mtx_init output argument |
25+
| test.c:18:17:18:19 | *& ... | semmle.label | *& ... |
26+
| test.c:19:14:19:16 | *& ... | semmle.label | *& ... |
27+
| test.c:30:12:30:14 | mtx_init output argument | semmle.label | mtx_init output argument |
28+
| test.c:31:17:31:19 | *& ... | semmle.label | *& ... |
29+
| test.c:32:14:32:16 | *& ... | semmle.label | *& ... |
30+
| test.c:42:12:42:16 | mtx_init output argument | semmle.label | mtx_init output argument |
31+
| test.c:42:13:42:14 | *l3 [post update] [m] | semmle.label | *l3 [post update] [m] |
32+
| test.c:43:17:43:21 | *& ... | semmle.label | *& ... |
33+
| test.c:43:18:43:19 | *l3 [m] | semmle.label | *l3 [m] |
34+
| test.c:44:14:44:18 | *& ... | semmle.label | *& ... |
35+
| test.c:44:15:44:16 | *l3 [m] | semmle.label | *l3 [m] |
36+
subpaths
37+
#select
38+
| test.c:10:43:10:43 | *m | test.c:13:12:13:14 | mtx_init output argument | test.c:10:43:10:43 | *m | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:13:12:13:14 | mtx_init output argument | initialized |
39+
| test.c:10:43:10:43 | *m | test.c:17:12:17:14 | mtx_init output argument | test.c:10:43:10:43 | *m | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:17:12:17:14 | mtx_init output argument | initialized |
40+
| test.c:10:43:10:43 | *m | test.c:30:12:30:14 | mtx_init output argument | test.c:10:43:10:43 | *m | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:30:12:30:14 | mtx_init output argument | initialized |
41+
| test.c:10:43:10:43 | *m | test.c:42:12:42:16 | mtx_init output argument | test.c:10:43:10:43 | *m | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:42:12:42:16 | mtx_init output argument | initialized |
42+
| test.c:14:17:14:19 | *& ... | test.c:13:12:13:14 | mtx_init output argument | test.c:14:17:14:19 | *& ... | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:13:12:13:14 | mtx_init output argument | initialized |
43+
| test.c:18:17:18:19 | *& ... | test.c:17:12:17:14 | mtx_init output argument | test.c:18:17:18:19 | *& ... | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:17:12:17:14 | mtx_init output argument | initialized |
44+
| test.c:31:17:31:19 | *& ... | test.c:30:12:30:14 | mtx_init output argument | test.c:31:17:31:19 | *& ... | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:30:12:30:14 | mtx_init output argument | initialized |
45+
| test.c:43:17:43:21 | *& ... | test.c:42:12:42:16 | mtx_init output argument | test.c:43:17:43:21 | *& ... | Call to mtx_timedlock with mutex which is $@ without flag 'mtx_timed'. | test.c:42:12:42:16 | mtx_init output argument | initialized |

‎c/misra/test/rules/RULE-21-26/TimedlockOnInappropriateMutexType.qlref

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/RULE-21-26/TimedlockOnInappropriateMutexType.ql

‎c/misra/test/rules/RULE-21-26/test.c

+45
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
#include "threads.h"
2+
3+
mtx_t g1;
4+
mtx_t g2;
5+
mtx_t g3;
6+
mtx_t g4;
7+
8+
struct timespec ts = {0, 0};
9+
10+
void doTimeLock(mtx_t *m) { mtx_timedlock(m, &ts); }
11+
12+
void main(void) {
13+
mtx_init(&g1, mtx_plain);
14+
mtx_timedlock(&g1, &ts); // NON-COMPLIANT
15+
doTimeLock(&g1); // NON-COMPLIANT
16+
17+
mtx_init(&g2, mtx_plain | mtx_recursive);
18+
mtx_timedlock(&g2, &ts); // NON-COMPLIANT
19+
doTimeLock(&g2); // NON-COMPLIANT
20+
21+
mtx_init(&g3, mtx_timed);
22+
mtx_timedlock(&g3, &ts); // COMPLIANT
23+
doTimeLock(&g3); // COMPLIANT
24+
25+
mtx_init(&g4, mtx_timed | mtx_recursive);
26+
mtx_timedlock(&g4, &ts); // COMPLIANT
27+
doTimeLock(&g4); // COMPLIANT
28+
29+
mtx_t l1;
30+
mtx_init(&l1, mtx_plain);
31+
mtx_timedlock(&l1, &ts); // NON-COMPLIANT
32+
doTimeLock(&l1); // NON-COMPLIANT
33+
34+
mtx_t l2;
35+
mtx_init(&l2, mtx_timed);
36+
mtx_timedlock(&l2, &ts); // COMPLIANT
37+
doTimeLock(&l2); // COMPLIANT
38+
39+
struct s {
40+
mtx_t m;
41+
} l3;
42+
mtx_init(&l3.m, mtx_plain);
43+
mtx_timedlock(&l3.m, &ts); // NON-COMPLIANT
44+
doTimeLock(&l3.m); // NON-COMPLIANT
45+
}

‎c/misra/test/rules/RULE-9-7/UninitializedAtomicObject.expected

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
| test.c:24:15:24:16 | definition of l3 | Atomic object 'l3' has no initializer or corresponding use of 'atomic_init()'. |
2+
| test.c:27:15:27:16 | definition of l4 | Atomic object 'l4' has no initializer or corresponding use of 'atomic_init()'. |
3+
| test.c:31:15:31:16 | definition of l5 | Atomic object 'l5' has no initializer or corresponding use of 'atomic_init()'. |
4+
| test.c:41:15:41:16 | definition of l7 | Atomic object 'l7' has no initializer or corresponding use of 'atomic_init()'. |

‎c/misra/test/rules/RULE-9-7/UninitializedAtomicObject.qlref

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
rules/RULE-9-7/UninitializedAtomicObject.ql

‎c/misra/test/rules/RULE-9-7/test.c

+46
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
#include "stdatomic.h"
2+
#include "threads.h"
3+
4+
_Atomic int g1; // COMPLIANT
5+
_Atomic int g2 = 0; // COMPLIANT
6+
7+
void f_thread(void *x);
8+
9+
void f_starts_thread() {
10+
thrd_t t;
11+
thrd_create(&t, f_thread, 0);
12+
}
13+
14+
void f_may_initialize_argument(void *p1) {}
15+
16+
void main() {
17+
_Atomic int l1 = 1; // COMPLIANT
18+
f_starts_thread();
19+
20+
_Atomic int l2; // COMPLIANT
21+
atomic_init(&l2, 0);
22+
f_starts_thread();
23+
24+
_Atomic int l3; // NON-COMPLIANT
25+
f_starts_thread();
26+
27+
_Atomic int l4; // NON-COMPLIANT
28+
f_starts_thread();
29+
atomic_init(&l4, 0);
30+
31+
_Atomic int l5; // NON-COMPLIANT
32+
if (g1 == 0) {
33+
atomic_init(&l5, 0);
34+
}
35+
f_starts_thread();
36+
37+
_Atomic int l6; // COMPLIANT
38+
f_may_initialize_argument(&l6);
39+
f_starts_thread();
40+
41+
_Atomic int l7; // NON_COMPLIANT
42+
if (g1 == 0) {
43+
f_may_initialize_argument(&l7);
44+
}
45+
f_starts_thread();
46+
}

0 commit comments

Comments
 (0)