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 Concurrency6 package -- split out Concurrency7 #791

Open
wants to merge 6 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
39 changes: 6 additions & 33 deletions c/cert/src/rules/CON39-C/ThreadWasPreviouslyJoinedOrDetached.ql
Original file line number Diff line number Diff line change
Expand Up @@ -14,37 +14,10 @@

import cpp
import codingstandards.c.cert
import codingstandards.cpp.Concurrency
import codingstandards.cpp.rules.joinordetachthreadonlyonce.JoinOrDetachThreadOnlyOnce

// OK
// 1) Thread calls detach parent DOES NOT call join
// 2) Parent calls join, thread does NOT call detach()
// NOT OK
// 1) Thread calls detach, parent calls join
// 2) Thread calls detach twice, parent does not call join
// 3) Parent calls join twice, thread does not call detach
from C11ThreadCreateCall tcc
where
not isExcluded(tcc, Concurrency5Package::threadWasPreviouslyJoinedOrDetachedQuery()) and
// Note: These cases can be simplified but they are presented like this for clarity
// case 1 - calls to `thrd_join` and `thrd_detach` within the parent or
// within the parent / child CFG.
exists(C11ThreadWait tw, C11ThreadDetach dt |
tw = getAThreadContextAwareSuccessor(tcc) and
dt = getAThreadContextAwareSuccessor(tcc)
)
or
// case 2 - multiple calls to `thrd_detach` within the threaded CFG.
exists(C11ThreadDetach dt1, C11ThreadDetach dt2 |
dt1 = getAThreadContextAwareSuccessor(tcc) and
dt2 = getAThreadContextAwareSuccessor(tcc) and
not dt1 = dt2
)
or
// case 3 - multiple calls to `thrd_join` within the threaded CFG.
exists(C11ThreadWait tw1, C11ThreadWait tw2 |
tw1 = getAThreadContextAwareSuccessor(tcc) and
tw2 = getAThreadContextAwareSuccessor(tcc) and
not tw1 = tw2
)
select tcc, "Thread may call join or detach after the thread is joined or detached."
class ThreadWasPreviouslyJoinedOrDetachedQuery extends JoinOrDetachThreadOnlyOnceSharedQuery {
ThreadWasPreviouslyJoinedOrDetachedQuery() {
this = Concurrency5Package::threadWasPreviouslyJoinedOrDetachedQuery()
}
}

This file was deleted.

Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
c/common/test/rules/joinordetachthreadonlyonce/JoinOrDetachThreadOnlyOnce.ql
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
| test.c:7:18:7:39 | ATOMIC_VAR_INIT(value) | Atomic variable possibly referred to twice in an $@. | test.c:33:3:33:10 | ... += ... | expression |
| test.c:7:18:7:39 | ATOMIC_VAR_INIT(value) | Atomic variable possibly referred to twice in an $@. | test.c:34:3:34:13 | ... = ... | expression |
| test.c:11:3:11:23 | atomic_store(a,b) | Atomic variable possibly referred to twice in an $@. | test.c:11:3:11:23 | atomic_store(a,b) | expression |
| test.c:12:3:12:35 | atomic_store_explicit(a,b,c) | Atomic variable possibly referred to twice in an $@. | test.c:12:3:12:35 | atomic_store_explicit(a,b,c) | expression |
| test.c:25:3:25:49 | atomic_compare_exchange_weak(a,b,c) | Atomic variable possibly referred to twice in an $@. | test.c:25:3:25:49 | atomic_compare_exchange_weak(a,b,c) | expression |
| test.c:26:3:27:42 | atomic_compare_exchange_weak_explicit(a,b,c,d,e) | Atomic variable possibly referred to twice in an $@. | test.c:26:3:27:42 | atomic_compare_exchange_weak_explicit(a,b,c,d,e) | expression |
| test.c:11:3:11:23 | atomic_store(object,desired) | Atomic variable possibly referred to twice in an $@. | test.c:11:3:11:23 | atomic_store(object,desired) | expression |
| test.c:12:3:12:23 | atomic_store_explicit | Atomic variable possibly referred to twice in an $@. | test.c:12:3:12:23 | atomic_store_explicit | expression |
| test.c:25:3:25:49 | atomic_compare_exchange_weak(object,expected,desired) | Atomic variable possibly referred to twice in an $@. | test.c:25:3:25:49 | atomic_compare_exchange_weak(object,expected,desired) | expression |
| test.c:26:3:26:39 | atomic_compare_exchange_weak_explicit | Atomic variable possibly referred to twice in an $@. | test.c:26:3:26:39 | atomic_compare_exchange_weak_explicit | expression |
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
| test.c:6:8:6:46 | atomic_compare_exchange_weak(a,b,c) | Function that can spuriously fail not wrapped in a loop. |
| test.c:10:3:10:41 | atomic_compare_exchange_weak(a,b,c) | Function that can spuriously fail not wrapped in a loop. |
| test.c:12:8:13:47 | atomic_compare_exchange_weak_explicit(a,b,c,d,e) | Function that can spuriously fail not wrapped in a loop. |
| test.c:17:3:17:56 | atomic_compare_exchange_weak_explicit(a,b,c,d,e) | Function that can spuriously fail not wrapped in a loop. |
| test.c:6:8:6:46 | atomic_compare_exchange_weak(object,expected,desired) | Function that can spuriously fail not wrapped in a loop. |
| test.c:10:3:10:41 | atomic_compare_exchange_weak(object,expected,desired) | Function that can spuriously fail not wrapped in a loop. |
| test.c:12:8:12:44 | atomic_compare_exchange_weak_explicit | Function that can spuriously fail not wrapped in a loop. |
| test.c:17:3:17:39 | atomic_compare_exchange_weak_explicit | Function that can spuriously fail not wrapped in a loop. |
74 changes: 67 additions & 7 deletions c/common/test/includes/standard-library/stdatomic.h
Original file line number Diff line number Diff line change
@@ -1,9 +1,69 @@
#define atomic_compare_exchange_weak(a, b, c) 0
#define atomic_compare_exchange_weak_explicit(a, b, c, d, e) 0
#define atomic_load(a) 0
#define atomic_load_explicit(a, b)
#define atomic_store(a, b) 0
#define atomic_store_explicit(a, b, c) 0
#define ATOMIC_VAR_INIT(value) (value)
#define atomic_is_lock_free(obj) __c11_atomic_is_lock_free(sizeof(*(obj)))
typedef _Atomic(int) atomic_int;
typedef _Atomic(int) atomic_int;

#define __ATOMIC_RELAXED 0
#define __ATOMIC_CONSUME 1
#define __ATOMIC_ACQUIRE 2
#define __ATOMIC_RELEASE 3
#define __ATOMIC_ACQ_REL 4
#define __ATOMIC_SEQ_CST 5

typedef enum memory_order {
memory_order_relaxed = __ATOMIC_RELAXED,
memory_order_consume = __ATOMIC_CONSUME,
memory_order_acquire = __ATOMIC_ACQUIRE,
memory_order_release = __ATOMIC_RELEASE,
memory_order_acq_rel = __ATOMIC_ACQ_REL,
memory_order_seq_cst = __ATOMIC_SEQ_CST
} memory_order;

void atomic_thread_fence(memory_order);
void atomic_signal_fence(memory_order);

#define atomic_thread_fence(order) __c11_atomic_thread_fence(order)
#define atomic_signal_fence(order) __c11_atomic_signal_fence(order)

#define atomic_store(object, desired) __c11_atomic_store(object, desired, __ATOMIC_SEQ_CST)
#define atomic_store_explicit __c11_atomic_store

#define atomic_load(object) __c11_atomic_load(object, __ATOMIC_SEQ_CST)
#define atomic_load_explicit __c11_atomic_load

#define atomic_exchange(object, desired) __c11_atomic_exchange(object, desired, __ATOMIC_SEQ_CST)
#define atomic_exchange_explicit __c11_atomic_exchange

#define atomic_compare_exchange_strong(object, expected, desired) __c11_atomic_compare_exchange_strong(object, expected, desired, __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST)
#define atomic_compare_exchange_strong_explicit __c11_atomic_compare_exchange_strong

#define atomic_compare_exchange_weak(object, expected, desired) __c11_atomic_compare_exchange_weak(object, expected, desired, __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST)
#define atomic_compare_exchange_weak_explicit __c11_atomic_compare_exchange_weak

#define atomic_fetch_add(object, operand) __c11_atomic_fetch_add(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_add_explicit __c11_atomic_fetch_add

#define atomic_fetch_sub(object, operand) __c11_atomic_fetch_sub(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_sub_explicit __c11_atomic_fetch_sub

#define atomic_fetch_or(object, operand) __c11_atomic_fetch_or(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_or_explicit __c11_atomic_fetch_or

#define atomic_fetch_xor(object, operand) __c11_atomic_fetch_xor(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_xor_explicit __c11_atomic_fetch_xor

#define atomic_fetch_and(object, operand) __c11_atomic_fetch_and(object, operand, __ATOMIC_SEQ_CST)
#define atomic_fetch_and_explicit __c11_atomic_fetch_and

typedef struct atomic_flag { _Atomic(_Bool) _Value; } atomic_flag;

_Bool atomic_flag_test_and_set(volatile atomic_flag *);
_Bool atomic_flag_test_and_set_explicit(volatile atomic_flag *, memory_order);

void atomic_flag_clear(volatile atomic_flag *);
void atomic_flag_clear_explicit(volatile atomic_flag *, memory_order);

#define atomic_flag_test_and_set(object) __c11_atomic_exchange(&(object)->_Value, 1, __ATOMIC_SEQ_CST)
#define atomic_flag_test_and_set_explicit(object, order) __c11_atomic_exchange(&(object)->_Value, 1, order)

#define atomic_flag_clear(object) __c11_atomic_store(&(object)->_Value, 0, __ATOMIC_SEQ_CST)
#define atomic_flag_clear_explicit(object, order) __c11_atomic_store(&(object)->_Value, 0, order)
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
// GENERATED FILE - DO NOT MODIFY
import codingstandards.cpp.rules.joinordetachthreadonlyonce.JoinOrDetachThreadOnlyOnce

class TestFileQuery extends JoinOrDetachThreadOnlyOnceSharedQuery, TestQuery { }
25 changes: 25 additions & 0 deletions c/misra/src/rules/DIR-5-2/NotNoDeadlocksBetweenThreads.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
/**
* @id c/misra/not-no-deadlocks-between-threads
* @name DIR-5-2: There shall be no deadlocks between threads
* @description Circular waits leading to thread deadlocks may be avoided by locking in a predefined
* order.
* @kind problem
* @precision very-high
* @problem.severity error
* @tags external/misra/id/dir-5-2
* external/misra/c/2012/amendment4
* correctness
* concurrency
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import codingstandards.cpp.rules.preventdeadlockbylockinginpredefinedorder.PreventDeadlockByLockingInPredefinedOrder

class NotNoDeadlocksBetweenThreadsQuery extends PreventDeadlockByLockingInPredefinedOrderSharedQuery
{
NotNoDeadlocksBetweenThreadsQuery() {
this = Concurrency6Package::notNoDeadlocksBetweenThreadsQuery()
}
}
29 changes: 29 additions & 0 deletions c/misra/src/rules/DIR-5-3/BannedDynamicThreadCreation.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
/**
* @id c/misra/banned-dynamic-thread-creation
* @name DIR-5-3: There shall be no dynamic thread creation
* @description Creating threads outside of a well-defined program start-up phase creates
* uncertainty in program behavior and concurrency overhead costs.
* @kind problem
* @precision low
* @problem.severity error
* @tags external/misra/id/dir-5-3
* external/misra/c/2012/amendment4
* external/misra/c/audit
* correctness
* maintainability
* concurrency
* performance
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import codingstandards.cpp.Concurrency

from CThreadCreateCall tc, Function enclosingFunction
where
not isExcluded(tc, Concurrency6Package::bannedDynamicThreadCreationQuery()) and
enclosingFunction = tc.getEnclosingFunction() and
not enclosingFunction.getName() = "main"
select tc, "Possible dynamic creation of thread outside initialization in function '$@'.",
enclosingFunction, enclosingFunction.toString()
45 changes: 45 additions & 0 deletions c/misra/src/rules/DIR-5-3/ThreadCreatedByThread.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
/**
* @id c/misra/thread-created-by-thread
* @name DIR-5-3: Threads shall not be created by other threads
* @description Creating threads within threads creates uncertainty in program behavior and
* concurrency overhead costs.
* @kind problem
* @precision high
* @problem.severity error
* @tags external/misra/id/dir-5-3
* external/misra/c/2012/amendment4
* correctness
* maintainability
* concurrency
* performance
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import codingstandards.cpp.Concurrency

Function callers(Function f) { result = f.getACallToThisFunction().getEnclosingFunction() }

class ThreadReachableFunction extends Function {
/* The root threaded function from which this function is reachable */
Function threadRoot;

ThreadReachableFunction() {
exists(CThreadCreateCall tc |
tc.getFunction() = callers*(this) and
threadRoot = tc.getFunction()
)
}

/* Get the root threaded function from which this function is reachable */
Function getThreadRoot() { result = threadRoot }
}

from CThreadCreateCall tc, ThreadReachableFunction enclosingFunction, Function threadRoot
where
not isExcluded(tc, Concurrency6Package::threadCreatedByThreadQuery()) and
enclosingFunction = tc.getEnclosingFunction() and
threadRoot = enclosingFunction.getThreadRoot()
select tc, "Thread creation call reachable from threaded function '$@'.", threadRoot,
threadRoot.toString()
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
/**
* @id c/misra/atomic-aggregate-object-directly-accessed
* @name RULE-12-6: Structure and union members of atomic objects shall not be directly accessed
* @description Accessing a member of an atomic structure or union results in undefined behavior.
* @kind problem
* @precision very-high
* @problem.severity error
* @tags external/misra/id/rule-12-6
* external/misra/c/2012/amendment4
* correctness
* concurrency
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra

from Expr expr, Field field
where
not isExcluded(expr, Concurrency6Package::atomicAggregateObjectDirectlyAccessedQuery()) and
not expr.isUnevaluated() and
(
exists(FieldAccess fa |
expr = fa and
fa.getQualifier().getUnderlyingType().hasSpecifier("atomic") and
field = fa.getTarget()
)
or
exists(PointerFieldAccess fa |
expr = fa and
fa.getQualifier().getUnderlyingType().(PointerType).getBaseType().hasSpecifier("atomic") and
field = fa.getTarget()
)
)
select expr, "Invalid access to member '$@' on atomic struct or union.", field, field.getName()
Loading
Loading