Skip to content

Commit 9ff699b

Browse files
MichaelRFairhurstMichaelRFairhurst
committed
Implement Concurrency7 package
1 parent 85036d5 commit 9ff699b

File tree

13 files changed

+371
-2
lines changed

13 files changed

+371
-2
lines changed

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,6 @@
55
#define atomic_store(a, b) 0
66
#define atomic_store_explicit(a, b, c) 0
77
#define ATOMIC_VAR_INIT(value) (value)
8+
#define atomic_init __c11_atomic_init
89
#define atomic_is_lock_free(obj) __c11_atomic_is_lock_free(sizeof(*(obj)))
910
typedef _Atomic(int) atomic_int;

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

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
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, "Call to mtx_timedlock with mutex not of type 'mtx_timed'."

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

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
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 semmle.code.cpp.controlflow.Dominance
18+
19+
class ThreadSpawningFunction extends Function {
20+
ThreadSpawningFunction() {
21+
this.hasName("pthread_create") or
22+
this.hasName("thrd_create") or
23+
exists(FunctionCall fc |
24+
fc.getTarget() instanceof ThreadSpawningFunction and
25+
fc.getEnclosingFunction() = this)
26+
}
27+
}
28+
29+
class AtomicInitAddressOfExpr extends FunctionCall {
30+
Expr addressedExpr;
31+
32+
AtomicInitAddressOfExpr() {
33+
exists(AddressOfExpr addrOf |
34+
getArgument(0) = addrOf and
35+
addrOf.getOperand() = addressedExpr and
36+
getTarget().getName() = "__c11_atomic_init"
37+
)
38+
}
39+
40+
Expr getAddressedExpr() {
41+
result = addressedExpr
42+
}
43+
}
44+
45+
ControlFlowNode getARequiredInitializationPoint(LocalScopeVariable v) {
46+
result = v.getParentScope().(BlockStmt).getFollowingStmt()
47+
or
48+
exists(DeclStmt decl |
49+
decl.getADeclaration() = v and
50+
result = any(FunctionCall fc
51+
| fc.getTarget() instanceof ThreadSpawningFunction and
52+
fc.getEnclosingBlock().getEnclosingBlock*() = v.getParentScope() and
53+
fc.getAPredecessor*() = decl
54+
)
55+
)
56+
}
57+
58+
from VariableDeclarationEntry decl, Variable v
59+
where
60+
not isExcluded(decl, Concurrency7Package::uninitializedAtomicObjectQuery()) and
61+
v = decl.getVariable() and
62+
v.getUnderlyingType().hasSpecifier("atomic") and
63+
not v.isTopLevel() and
64+
not exists(v.getInitializer()) and
65+
exists(ControlFlowNode missingInitPoint |
66+
missingInitPoint = getARequiredInitializationPoint(v)
67+
and not exists(AtomicInitAddressOfExpr initialization |
68+
initialization.getAddressedExpr().(VariableAccess).getTarget() = v and
69+
dominates(initialization, missingInitPoint)
70+
)
71+
)
72+
select decl,
73+
"Atomic object '" + v.getName() + "' has no initializer or corresponding use of 'atomic_init()'."

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

Lines changed: 45 additions & 0 deletions
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 not of type 'mtx_timed'. |
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 not of type 'mtx_timed'. |
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 not of type 'mtx_timed'. |
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 not of type 'mtx_timed'. |
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 not of type 'mtx_timed'. |
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 not of type 'mtx_timed'. |
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 not of type 'mtx_timed'. |
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 not of type 'mtx_timed'. |

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

Lines changed: 1 addition & 0 deletions
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

Lines changed: 45 additions & 0 deletions
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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
| test.c:22:15:22:16 | definition of l3 | Atomic object 'l3' has no initializer or corresponding use of 'atomic_init()'. |
2+
| test.c:25:15:25:16 | definition of l4 | Atomic object 'l4' has no initializer or corresponding use of 'atomic_init()'. |
3+
| test.c:29:15:29:16 | definition of l5 | Atomic object 'l5' has no initializer or corresponding use of 'atomic_init()'. |

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

Lines changed: 1 addition & 0 deletions
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

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
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 main() {
15+
_Atomic int l1 = 1; // COMPLIANT
16+
f_starts_thread();
17+
18+
_Atomic int l2; // COMPLIANT
19+
atomic_init(&l2, 0);
20+
f_starts_thread();
21+
22+
_Atomic int l3; // NON-COMPLIANT
23+
f_starts_thread();
24+
25+
_Atomic int l4; // NON-COMPLIANT
26+
f_starts_thread();
27+
atomic_init(&l4, 0);
28+
29+
_Atomic int l5; // NON-COMPLIANT
30+
if (g1 == 0) {
31+
atomic_init(&l5, 0);
32+
}
33+
f_starts_thread();
34+
}

‎cpp/common/src/codingstandards/cpp/exclusions/c/Concurrency7.qll

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY. **/
2+
import cpp
3+
import RuleMetadata
4+
import codingstandards.cpp.exclusions.RuleMetadata
5+
6+
newtype Concurrency7Query =
7+
TUninitializedAtomicObjectQuery() or
8+
TTimedlockOnInappropriateMutexTypeQuery()
9+
10+
predicate isConcurrency7QueryMetadata(Query query, string queryId, string ruleId, string category) {
11+
query =
12+
// `Query` instance for the `uninitializedAtomicObject` query
13+
Concurrency7Package::uninitializedAtomicObjectQuery() and
14+
queryId =
15+
// `@id` for the `uninitializedAtomicObject` query
16+
"c/misra/uninitialized-atomic-object" and
17+
ruleId = "RULE-9-7" and
18+
category = "mandatory"
19+
or
20+
query =
21+
// `Query` instance for the `timedlockOnInappropriateMutexType` query
22+
Concurrency7Package::timedlockOnInappropriateMutexTypeQuery() and
23+
queryId =
24+
// `@id` for the `timedlockOnInappropriateMutexType` query
25+
"c/misra/timedlock-on-inappropriate-mutex-type" and
26+
ruleId = "RULE-21-26" and
27+
category = "required"
28+
}
29+
30+
module Concurrency7Package {
31+
Query uninitializedAtomicObjectQuery() {
32+
//autogenerate `Query` type
33+
result =
34+
// `Query` type for `uninitializedAtomicObject` query
35+
TQueryC(TConcurrency7PackageQuery(TUninitializedAtomicObjectQuery()))
36+
}
37+
38+
Query timedlockOnInappropriateMutexTypeQuery() {
39+
//autogenerate `Query` type
40+
result =
41+
// `Query` type for `timedlockOnInappropriateMutexType` query
42+
TQueryC(TConcurrency7PackageQuery(TTimedlockOnInappropriateMutexTypeQuery()))
43+
}
44+
}

‎cpp/common/src/codingstandards/cpp/exclusions/c/RuleMetadata.qll

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ import Concurrency2
1111
import Concurrency3
1212
import Concurrency4
1313
import Concurrency5
14+
import Concurrency7
1415
import Contracts1
1516
import Contracts2
1617
import Contracts3
@@ -87,6 +88,7 @@ newtype TCQuery =
8788
TConcurrency3PackageQuery(Concurrency3Query q) or
8889
TConcurrency4PackageQuery(Concurrency4Query q) or
8990
TConcurrency5PackageQuery(Concurrency5Query q) or
91+
TConcurrency7PackageQuery(Concurrency7Query q) or
9092
TContracts1PackageQuery(Contracts1Query q) or
9193
TContracts2PackageQuery(Contracts2Query q) or
9294
TContracts3PackageQuery(Contracts3Query q) or
@@ -163,6 +165,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
163165
isConcurrency3QueryMetadata(query, queryId, ruleId, category) or
164166
isConcurrency4QueryMetadata(query, queryId, ruleId, category) or
165167
isConcurrency5QueryMetadata(query, queryId, ruleId, category) or
168+
isConcurrency7QueryMetadata(query, queryId, ruleId, category) or
166169
isContracts1QueryMetadata(query, queryId, ruleId, category) or
167170
isContracts2QueryMetadata(query, queryId, ruleId, category) or
168171
isContracts3QueryMetadata(query, queryId, ruleId, category) or

0 commit comments

Comments
 (0)