Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Concurrency7 package #799

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions c/common/test/includes/standard-library/stdatomic.h
Original file line number Diff line number Diff line change
Expand Up @@ -5,5 +5,6 @@
#define atomic_store(a, b) 0
#define atomic_store_explicit(a, b, c) 0
#define ATOMIC_VAR_INIT(value) (value)
#define atomic_init __c11_atomic_init
#define atomic_is_lock_free(obj) __c11_atomic_is_lock_free(sizeof(*(obj)))
typedef _Atomic(int) atomic_int;
74 changes: 74 additions & 0 deletions c/misra/src/rules/RULE-21-26/TimedlockOnInappropriateMutexType.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
/**
* @id c/misra/timedlock-on-inappropriate-mutex-type
* @name RULE-21-26: The Standard Library function mtx_timedlock() shall only be invoked on mutexes of type mtx_timed
* @description The Standard Library function mtx_timedlock() shall only be invoked on mutex objects
* of appropriate mutex type.
* @kind path-problem
* @precision high
* @problem.severity error
* @tags external/misra/id/rule-21-26
* correctness
* concurrency
* external/misra/c/2012/amendment4
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import semmle.code.cpp.dataflow.new.DataFlow

class MutexTimed extends EnumConstant {
MutexTimed() { hasName("mtx_timed") }
}

class MutexInitCall extends FunctionCall {
Expr mutexExpr;
Expr mutexTypeExpr;

MutexInitCall() {
getTarget().hasName("mtx_init") and
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could mtx_init be a macro?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It isn't in glibc or in clang stdc, but it is on FreeBSD.

Should we assume that if it is a macro, it expands to a simple wrapper function, e.g., #define mtx_init(a, b) __f((a), (b))? FWIW, that isn't the case on FreeBSD, which passes mutexTypeExpr into a function call for the second arg.

mutexExpr = getArgument(0) and
mutexTypeExpr = getArgument(1)
}

predicate isTimedMutexType() {
exists(EnumConstantAccess baseTypeAccess |
(
baseTypeAccess = mutexTypeExpr
or
baseTypeAccess = mutexTypeExpr.(BinaryBitwiseOperation).getAnOperand()
) and
baseTypeAccess.getTarget() instanceof MutexTimed
)
or
mutexTypeExpr.getValue().toInt() = any(MutexTimed m).getValue().toInt()
}

Expr getMutexExpr() { result = mutexExpr }
}

module MutexTimedlockFlowConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node node) {
exists(MutexInitCall init |
node.asDefiningArgument() = init.getMutexExpr() and not init.isTimedMutexType()
)
}

predicate isSink(DataFlow::Node node) {
exists(FunctionCall fc |
fc.getTarget().hasName("mtx_timedlock") and
node.asIndirectExpr() = fc.getArgument(0)
)
}
}

module Flow = DataFlow::Global<MutexTimedlockFlowConfig>;

import Flow::PathGraph

from Flow::PathNode source, Flow::PathNode sink
where
not isExcluded(sink.getNode().asExpr(),
Concurrency7Package::timedlockOnInappropriateMutexTypeQuery()) and
Flow::flowPath(source, sink)
select sink.getNode(), source, sink, "Call to mtx_timedlock with mutex not of type 'mtx_timed'."
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add a message link to the source - perhaps make the link mutex in the message? Otherwise users have to know to click into the path viewer in GitHub to see the source.

75 changes: 75 additions & 0 deletions c/misra/src/rules/RULE-9-7/UninitializedAtomicObject.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
/**
* @id c/misra/uninitialized-atomic-object
* @name RULE-9-7: Atomic objects shall be appropriately initialized before being accessed
* @description Atomic objects that do not have static storage duration shall be initialized with a
* value or by using 'atomic_init()'.
* @kind problem
* @precision high
* @problem.severity warning
* @tags external/misra/id/rule-9-7
* concurrency
* external/misra/c/2012/amendment4
* external/misra/obligation/mandatory
*/

import cpp
import codingstandards.c.misra
import semmle.code.cpp.controlflow.Dominance

class ThreadSpawningFunction extends Function {
ThreadSpawningFunction() {
this.hasName("pthread_create")
or
this.hasName("thrd_create")
or
exists(FunctionCall fc |
fc.getTarget() instanceof ThreadSpawningFunction and
fc.getEnclosingFunction() = this
)
}
}

class AtomicInitAddressOfExpr extends FunctionCall {
Expr addressedExpr;

AtomicInitAddressOfExpr() {
exists(AddressOfExpr addrOf |
getArgument(0) = addrOf and
addrOf.getOperand() = addressedExpr and
getTarget().getName() = "__c11_atomic_init"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this name required by the standard? If not, we need to confirm it's used by all our supported compilers, or use a different approach (identify the function call wrapped by the macro atomic_init?)

)
}

Expr getAddressedExpr() { result = addressedExpr }
}

ControlFlowNode getARequiredInitializationPoint(LocalScopeVariable v) {
result = v.getParentScope().(BlockStmt).getFollowingStmt()
or
exists(DeclStmt decl |
decl.getADeclaration() = v and
result =
any(FunctionCall fc |
fc.getTarget() instanceof ThreadSpawningFunction and
fc.getEnclosingBlock().getEnclosingBlock*() = v.getParentScope() and
fc.getAPredecessor*() = decl
)
)
}

from VariableDeclarationEntry decl, Variable v
where
not isExcluded(decl, Concurrency7Package::uninitializedAtomicObjectQuery()) and
v = decl.getVariable() and
v.getUnderlyingType().hasSpecifier("atomic") and
not v.isTopLevel() and
not exists(v.getInitializer()) and
exists(ControlFlowNode missingInitPoint |
missingInitPoint = getARequiredInitializationPoint(v) and
not exists(AtomicInitAddressOfExpr initialization |
initialization.getAddressedExpr().(VariableAccess).getTarget() = v and
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need to consider non-local initialization? e.g. a function that takes the address and initializes the variable?

dominates(initialization, missingInitPoint)
)
)
select decl,
"Atomic object '" + v.getName() + "' has no initializer or corresponding use of 'atomic_init()'."
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
edges
| test.c:10:24:10:24 | *m | test.c:10:43:10:43 | *m | provenance | |
| test.c:13:12:13:14 | mtx_init output argument | test.c:14:17:14:19 | *& ... | provenance | |
| test.c:13:12:13:14 | mtx_init output argument | test.c:15:14:15:16 | *& ... | provenance | |
| test.c:15:14:15:16 | *& ... | test.c:10:24:10:24 | *m | provenance | |
| test.c:17:12:17:14 | mtx_init output argument | test.c:18:17:18:19 | *& ... | provenance | |
| test.c:17:12:17:14 | mtx_init output argument | test.c:19:14:19:16 | *& ... | provenance | |
| test.c:19:14:19:16 | *& ... | test.c:10:24:10:24 | *m | provenance | |
| test.c:30:12:30:14 | mtx_init output argument | test.c:31:17:31:19 | *& ... | provenance | |
| test.c:30:12:30:14 | mtx_init output argument | test.c:32:14:32:16 | *& ... | provenance | |
| test.c:32:14:32:16 | *& ... | test.c:10:24:10:24 | *m | provenance | |
| test.c:42:12:42:16 | mtx_init output argument | test.c:42:13:42:14 | *l3 [post update] [m] | provenance | |
| test.c:42:13:42:14 | *l3 [post update] [m] | test.c:43:18:43:19 | *l3 [m] | provenance | |
| test.c:42:13:42:14 | *l3 [post update] [m] | test.c:44:15:44:16 | *l3 [m] | provenance | |
| test.c:43:18:43:19 | *l3 [m] | test.c:43:17:43:21 | *& ... | provenance | |
| test.c:44:14:44:18 | *& ... | test.c:10:24:10:24 | *m | provenance | |
| test.c:44:15:44:16 | *l3 [m] | test.c:44:14:44:18 | *& ... | provenance | |
nodes
| test.c:10:24:10:24 | *m | semmle.label | *m |
| test.c:10:43:10:43 | *m | semmle.label | *m |
| test.c:13:12:13:14 | mtx_init output argument | semmle.label | mtx_init output argument |
| test.c:14:17:14:19 | *& ... | semmle.label | *& ... |
| test.c:15:14:15:16 | *& ... | semmle.label | *& ... |
| test.c:17:12:17:14 | mtx_init output argument | semmle.label | mtx_init output argument |
| test.c:18:17:18:19 | *& ... | semmle.label | *& ... |
| test.c:19:14:19:16 | *& ... | semmle.label | *& ... |
| test.c:30:12:30:14 | mtx_init output argument | semmle.label | mtx_init output argument |
| test.c:31:17:31:19 | *& ... | semmle.label | *& ... |
| test.c:32:14:32:16 | *& ... | semmle.label | *& ... |
| test.c:42:12:42:16 | mtx_init output argument | semmle.label | mtx_init output argument |
| test.c:42:13:42:14 | *l3 [post update] [m] | semmle.label | *l3 [post update] [m] |
| test.c:43:17:43:21 | *& ... | semmle.label | *& ... |
| test.c:43:18:43:19 | *l3 [m] | semmle.label | *l3 [m] |
| test.c:44:14:44:18 | *& ... | semmle.label | *& ... |
| test.c:44:15:44:16 | *l3 [m] | semmle.label | *l3 [m] |
subpaths
#select
| 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'. |
| 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'. |
| 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'. |
| 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'. |
| 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'. |
| 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'. |
| 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'. |
| 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'. |
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rules/RULE-21-26/TimedlockOnInappropriateMutexType.ql
45 changes: 45 additions & 0 deletions c/misra/test/rules/RULE-21-26/test.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
#include "threads.h"

mtx_t g1;
mtx_t g2;
mtx_t g3;
mtx_t g4;

struct timespec ts = {0, 0};

void doTimeLock(mtx_t *m) { mtx_timedlock(m, &ts); }

void main(void) {
mtx_init(&g1, mtx_plain);
mtx_timedlock(&g1, &ts); // NON-COMPLIANT
doTimeLock(&g1); // NON-COMPLIANT

mtx_init(&g2, mtx_plain | mtx_recursive);
mtx_timedlock(&g2, &ts); // NON-COMPLIANT
doTimeLock(&g2); // NON-COMPLIANT

mtx_init(&g3, mtx_timed);
mtx_timedlock(&g3, &ts); // COMPLIANT
doTimeLock(&g3); // COMPLIANT

mtx_init(&g4, mtx_timed | mtx_recursive);
mtx_timedlock(&g4, &ts); // COMPLIANT
doTimeLock(&g4); // COMPLIANT

mtx_t l1;
mtx_init(&l1, mtx_plain);
mtx_timedlock(&l1, &ts); // NON-COMPLIANT
doTimeLock(&l1); // NON-COMPLIANT

mtx_t l2;
mtx_init(&l2, mtx_timed);
mtx_timedlock(&l2, &ts); // COMPLIANT
doTimeLock(&l2); // COMPLIANT

struct s {
mtx_t m;
} l3;
mtx_init(&l3.m, mtx_plain);
mtx_timedlock(&l3.m, &ts); // NON-COMPLIANT
doTimeLock(&l3.m); // NON-COMPLIANT
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
| test.c:22:15:22:16 | definition of l3 | Atomic object 'l3' has no initializer or corresponding use of 'atomic_init()'. |
| test.c:25:15:25:16 | definition of l4 | Atomic object 'l4' has no initializer or corresponding use of 'atomic_init()'. |
| test.c:29:15:29:16 | definition of l5 | Atomic object 'l5' has no initializer or corresponding use of 'atomic_init()'. |
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rules/RULE-9-7/UninitializedAtomicObject.ql
34 changes: 34 additions & 0 deletions c/misra/test/rules/RULE-9-7/test.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
#include "stdatomic.h"
#include "threads.h"

_Atomic int g1; // COMPLIANT
_Atomic int g2 = 0; // COMPLIANT

void f_thread(void *x);

void f_starts_thread() {
thrd_t t;
thrd_create(&t, f_thread, 0);
}

void main() {
_Atomic int l1 = 1; // COMPLIANT
f_starts_thread();

_Atomic int l2; // COMPLIANT
atomic_init(&l2, 0);
f_starts_thread();

_Atomic int l3; // NON-COMPLIANT
f_starts_thread();

_Atomic int l4; // NON-COMPLIANT
f_starts_thread();
atomic_init(&l4, 0);

_Atomic int l5; // NON-COMPLIANT
if (g1 == 0) {
atomic_init(&l5, 0);
}
f_starts_thread();
}
44 changes: 44 additions & 0 deletions cpp/common/src/codingstandards/cpp/exclusions/c/Concurrency7.qll
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
//** THIS FILE IS AUTOGENERATED, DO NOT MODIFY DIRECTLY. **/
import cpp
import RuleMetadata
import codingstandards.cpp.exclusions.RuleMetadata

newtype Concurrency7Query =
TUninitializedAtomicObjectQuery() or
TTimedlockOnInappropriateMutexTypeQuery()

predicate isConcurrency7QueryMetadata(Query query, string queryId, string ruleId, string category) {
query =
// `Query` instance for the `uninitializedAtomicObject` query
Concurrency7Package::uninitializedAtomicObjectQuery() and
queryId =
// `@id` for the `uninitializedAtomicObject` query
"c/misra/uninitialized-atomic-object" and
ruleId = "RULE-9-7" and
category = "mandatory"
or
query =
// `Query` instance for the `timedlockOnInappropriateMutexType` query
Concurrency7Package::timedlockOnInappropriateMutexTypeQuery() and
queryId =
// `@id` for the `timedlockOnInappropriateMutexType` query
"c/misra/timedlock-on-inappropriate-mutex-type" and
ruleId = "RULE-21-26" and
category = "required"
}

module Concurrency7Package {
Query uninitializedAtomicObjectQuery() {
//autogenerate `Query` type
result =
// `Query` type for `uninitializedAtomicObject` query
TQueryC(TConcurrency7PackageQuery(TUninitializedAtomicObjectQuery()))
}

Query timedlockOnInappropriateMutexTypeQuery() {
//autogenerate `Query` type
result =
// `Query` type for `timedlockOnInappropriateMutexType` query
TQueryC(TConcurrency7PackageQuery(TTimedlockOnInappropriateMutexTypeQuery()))
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import Concurrency2
import Concurrency3
import Concurrency4
import Concurrency5
import Concurrency7
import Contracts1
import Contracts2
import Contracts3
Expand Down Expand Up @@ -87,6 +88,7 @@ newtype TCQuery =
TConcurrency3PackageQuery(Concurrency3Query q) or
TConcurrency4PackageQuery(Concurrency4Query q) or
TConcurrency5PackageQuery(Concurrency5Query q) or
TConcurrency7PackageQuery(Concurrency7Query q) or
TContracts1PackageQuery(Contracts1Query q) or
TContracts2PackageQuery(Contracts2Query q) or
TContracts3PackageQuery(Contracts3Query q) or
Expand Down Expand Up @@ -163,6 +165,7 @@ predicate isQueryMetadata(Query query, string queryId, string ruleId, string cat
isConcurrency3QueryMetadata(query, queryId, ruleId, category) or
isConcurrency4QueryMetadata(query, queryId, ruleId, category) or
isConcurrency5QueryMetadata(query, queryId, ruleId, category) or
isConcurrency7QueryMetadata(query, queryId, ruleId, category) or
isContracts1QueryMetadata(query, queryId, ruleId, category) or
isContracts2QueryMetadata(query, queryId, ruleId, category) or
isContracts3QueryMetadata(query, queryId, ruleId, category) or
Expand Down
Loading
Loading