Skip to content
Merged
Show file tree
Hide file tree
Changes from 6 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
5 changes: 3 additions & 2 deletions c/cert/src/rules/CON40-C/AtomicVariableTwiceInExpression.ql
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@

import cpp
import codingstandards.c.cert
import codingstandards.cpp.Concurrency

from MacroInvocation mi, Variable v, Locatable whereFound
where
Expand All @@ -22,13 +23,13 @@ where
// There isn't a way to safely use this construct in a way that is also
// possible the reliably detect so advise against using it.
(
mi.getMacroName() = ["atomic_store", "atomic_store_explicit"]
mi instanceof AtomicStore
or
// This construct is generally safe, but must be used in a loop. To lower
// the false positive rate we don't look at the conditions of the loop and
// instead assume if it is found in a looping construct that it is likely
// related to the safety property.
mi.getMacroName() = ["atomic_compare_exchange_weak", "atomic_compare_exchange_weak_explicit"] and
mi instanceof AtomicCompareExchange and
not exists(Loop l | mi.getAGeneratedElement().(Expr).getParent*() = l)
) and
whereFound = mi
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,28 +12,18 @@
* external/cert/obligation/rule
*/

import cpp
import codingstandards.c.cert
import cpp
import codingstandards.c.cert
import codingstandards.cpp.Concurrency


/**
* Models calls to routines in the `stdatomic` library. Note that these
* are typically implemented as macros within Clang and GCC's standard
* libraries.
*/
class SpuriouslyFailingFunctionCallType extends MacroInvocation {
SpuriouslyFailingFunctionCallType() {
getMacroName() = ["atomic_compare_exchange_weak", "atomic_compare_exchange_weak_explicit"]
}
}

from SpuriouslyFailingFunctionCallType fc
where
not isExcluded(fc, Concurrency3Package::wrapFunctionsThatCanFailSpuriouslyInLoopQuery()) and
(
exists(StmtParent sp | sp = fc.getStmt() and not sp.(Stmt).getParentStmt*() instanceof Loop)
or
exists(StmtParent sp |
sp = fc.getExpr() and not sp.(Expr).getEnclosingStmt().getParentStmt*() instanceof Loop
)
)
select fc, "Function that can spuriously fail not wrapped in a loop."
from AtomicCompareExchange ace
where
not isExcluded(ace, Concurrency3Package::wrapFunctionsThatCanFailSpuriouslyInLoopQuery()) and
(
forex(StmtParent sp | sp = ace.getStmt() | not sp.(Stmt).getParentStmt*() instanceof Loop) or
forex(Expr e | e = ace.getExpr() | not e.getEnclosingStmt().getParentStmt*()
instanceof Loop)
)
select ace, "Function that can spuriously fail not wrapped in a loop."

Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
| test.c:6:19:6:40 | ATOMIC_VAR_INIT(value) | Atomic variable possibly referred to twice in an $@. | test.c:32:3:32:10 | ... += ... | expression |
| test.c:6:19:6:40 | ATOMIC_VAR_INIT(value) | Atomic variable possibly referred to twice in an $@. | test.c:33:3:33:13 | ... = ... | expression |
| test.c:10:3:10:23 | atomic_store(a,b) | Atomic variable possibly referred to twice in an $@. | test.c:10:3:10:23 | atomic_store(a,b) | expression |
| test.c:11:3:11:35 | atomic_store_explicit(a,b,c) | Atomic variable possibly referred to twice in an $@. | test.c:11:3:11:35 | atomic_store_explicit(a,b,c) | expression |
| test.c:24:3:24:48 | atomic_compare_exchange_weak(a,b,c) | Atomic variable possibly referred to twice in an $@. | test.c:24:3:24:48 | atomic_compare_exchange_weak(a,b,c) | expression |
| test.c:25:3:26:45 | atomic_compare_exchange_weak_explicit(a,b,c,d,e) | Atomic variable possibly referred to twice in an $@. | test.c:25:3:26:45 | atomic_compare_exchange_weak_explicit(a,b,c,d,e) | expression |
| 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 |
Original file line number Diff line number Diff line change
@@ -0,0 +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(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
@@ -0,0 +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(PTR,VAL) | Atomic variable possibly referred to twice in an $@. | test.c:11:3:11:23 | atomic_store(PTR,VAL) | expression |
| test.c:12:3:12:35 | atomic_store_explicit(PTR,VAL,MO) | Atomic variable possibly referred to twice in an $@. | test.c:12:3:12:35 | atomic_store_explicit(PTR,VAL,MO) | expression |
| test.c:25:3:25:49 | atomic_compare_exchange_weak(PTR,VAL,DES) | Atomic variable possibly referred to twice in an $@. | test.c:25:3:25:49 | atomic_compare_exchange_weak(PTR,VAL,DES) | expression |
| test.c:26:3:27:42 | atomic_compare_exchange_weak_explicit(PTR,VAL,DES,SUC,FAIL) | Atomic variable possibly referred to twice in an $@. | test.c:26:3:27:42 | atomic_compare_exchange_weak_explicit(PTR,VAL,DES,SUC,FAIL) | expression |
21 changes: 11 additions & 10 deletions c/cert/test/rules/CON40-C/test.c
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
#include <stdatomic.h>
#include <stdbool.h>

static bool fl1 = ATOMIC_VAR_INIT(false);
static bool fl2 = ATOMIC_VAR_INIT(false);
static bool fl3 = ATOMIC_VAR_INIT(false);
static bool fl4 = ATOMIC_VAR_INIT(false);
static _Atomic int fl1 = ATOMIC_VAR_INIT(false);
static _Atomic int fl2 = ATOMIC_VAR_INIT(false);
static int fl2a = ATOMIC_VAR_INIT(false);
static int fl3 = ATOMIC_VAR_INIT(false);
static int fl4 = ATOMIC_VAR_INIT(false);

void f1() {
atomic_store(&fl1, 0); // NON_COMPLIANT
Expand All @@ -13,17 +14,17 @@ void f1() {

void f2() {
do {
} while (!atomic_compare_exchange_weak(&fl2, &fl2, &fl2)); // COMPLIANT
} while (!atomic_compare_exchange_weak(&fl2, &fl2a, fl2a)); // COMPLIANT

do {
} while (!atomic_compare_exchange_weak_explicit(&fl2, &fl2, &fl2, &fl2,
&fl2)); // COMPLIANT
} while (!atomic_compare_exchange_weak_explicit(&fl2, &fl2a, fl2a, 0,
0)); // COMPLIANT
}

void f3() {
atomic_compare_exchange_weak(&fl2, &fl2, &fl2); // NON_COMPLIANT
atomic_compare_exchange_weak_explicit(&fl2, &fl2, &fl2, &fl2,
&fl2); // NON_COMPLIANT
atomic_compare_exchange_weak(&fl2, &fl2a, fl2a); // NON_COMPLIANT
atomic_compare_exchange_weak_explicit(&fl2, &fl2a, fl2a, 0,
0); // NON_COMPLIANT
}

void f4() { fl3 ^= true; }
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
| test.c:5:8:5:46 | atomic_compare_exchange_weak(a,b,c) | Function that can spuriously fail not wrapped in a loop. |
| test.c:9:3:9:41 | atomic_compare_exchange_weak(a,b,c) | Function that can spuriously fail not wrapped in a loop. |
| test.c:11:8:12:47 | atomic_compare_exchange_weak_explicit(a,b,c,d,e) | Function that can spuriously fail not wrapped in a loop. |
| test.c:16:3:16: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(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. |
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
| 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. |
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
| test.c:6:8:6:46 | atomic_compare_exchange_weak(PTR,VAL,DES) | Function that can spuriously fail not wrapped in a loop. |
| test.c:10:3:10:41 | atomic_compare_exchange_weak(PTR,VAL,DES) | Function that can spuriously fail not wrapped in a loop. |
| test.c:12:8:13:47 | atomic_compare_exchange_weak_explicit(PTR,VAL,DES,SUC,FAIL) | Function that can spuriously fail not wrapped in a loop. |
| test.c:17:3:17:56 | atomic_compare_exchange_weak_explicit(PTR,VAL,DES,SUC,FAIL) | Function that can spuriously fail not wrapped in a loop. |
6 changes: 4 additions & 2 deletions c/cert/test/rules/CON41-C/test.c
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
#include "stdatomic.h"

void f1() {
int a, b, c;
_Atomic int a;
int b, c;
if (!atomic_compare_exchange_weak(&a, &b, c)) { // NON_COMPLIANT
(void)0; /* no-op */
}
Expand All @@ -17,7 +18,8 @@ void f1() {
}

void f2() {
int a, b, c;
_Atomic int a;
int b, c;
while (1 == 1) {
if (!atomic_compare_exchange_weak(&a, &b, c)) { // COMPLIANT
(void)0; /* no-op */
Expand Down
6 changes: 6 additions & 0 deletions change_notes/2023-03-06-better-modeling-of-stdatomic.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
- `CON41-C`: Refactored to address compiler compatibility issues. More accurate
modeling of cases where macros are modeled against other macros such as
`atomic_compare_exchange_weak` and `atomic_store`.
- `CON40-C`: Refactored to address compiler compatibility issues. More accurate
modeling of cases where macros are modeled against other macros such as
`atomic_compare_exchange_weak` and `atomic_store`.
42 changes: 42 additions & 0 deletions cpp/common/src/codingstandards/cpp/Concurrency.qll
Original file line number Diff line number Diff line change
Expand Up @@ -876,3 +876,45 @@ predicate getAThreadSpecificStorageDeallocationCall(C11ThreadCreateCall tcc, Dea
DataFlow::localFlow(DataFlow::exprNode(tsg), DataFlow::exprNode(dexp.getFreedExpr()))
)
}

/**
* Models calls to routines `atomic_compare_exchange_weak` and
* `atomic_compare_exchange_weak_explicit` in the `stdatomic` library.
* Note that these are typically implemented as macros within Clang and
* GCC's standard libraries.
*/
class AtomicCompareExchange extends MacroInvocation {
AtomicCompareExchange() {
getMacroName() = "atomic_compare_exchange_weak"
or
// some compilers model `atomic_compare_exchange_weak` as a macro that
// expands to `atomic_compare_exchange_weak_explicit` so this defeats that
// and other similar modeling.
getMacroName() = "atomic_compare_exchange_weak_explicit" and
not exists(MacroInvocation m |
m.getMacroName() = "atomic_compare_exchange_weak" and
m.getAnExpandedElement() = getAnExpandedElement()
)
}
}

/**
* Models calls to routines `atomic_store` and
* `atomic_store_explicit` in the `stdatomic` library.
* Note that these are typically implemented as macros within Clang and
* GCC's standard libraries.
*/
class AtomicStore extends MacroInvocation {
AtomicStore() {
getMacroName() = "atomic_store"
or
// some compilers model `atomic_compare_exchange_weak` as a macro that
// expands to `atomic_compare_exchange_weak_explicit` so this defeats that
// and other similar modeling.
getMacroName() = "atomic_store_explicit" and
not exists(MacroInvocation m |
m.getMacroName() = "atomic_store" and
m.getAnExpandedElement() = getAnExpandedElement()
)
}
}