Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Fixes for #1224, 1150, 1223, 1151 compiler compatibility issues#240

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 ourterms of service andprivacy statement. We’ll occasionally send you account related emails.

Already on GitHub?Sign in to your account

Merged
lcartey merged 8 commits intomainfromjsinglet/1224-1150-1223-1151
Mar 8, 2023
Merged
Show file tree
Hide file tree
Changes fromall 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
View file
Open in desktop
Original file line numberDiff line numberDiff 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
View file
Open in desktop
Original file line numberDiff line numberDiff 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."

View file
Open in desktop
Original file line numberDiff line numberDiff 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 |
View file
Open in desktop
Original file line numberDiff line numberDiff 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 |
View file
Open in desktop
Original file line numberDiff line numberDiff 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 deletionsc/cert/test/rules/CON40-C/test.c
View file
Open in desktop
Original file line numberDiff line numberDiff 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
View file
Open in desktop
Original file line numberDiff line numberDiff 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. |
View file
Open in desktop
Original file line numberDiff line numberDiff 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. |
View file
Open in desktop
Original file line numberDiff line numberDiff 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 deletionsc/cert/test/rules/CON41-C/test.c
View file
Open in desktop
Original file line numberDiff line numberDiff 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 deletionschange_notes/2023-03-06-better-modeling-of-stdatomic.md
View file
Open in desktop
Original file line numberDiff line numberDiff 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 deletionscpp/common/src/codingstandards/cpp/Concurrency.qll
View file
Open in desktop
Original file line numberDiff line numberDiff 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()
)
}
}
[8]ページ先頭
©2009-2025 Movatter.jp