github · lcartey · Mar 8, 2023 · Mar 6, 2023 · Mar 6, 2023 · Mar 6, 2023
diff --git a/c/cert/src/rules/CON40-C/AtomicVariableTwiceInExpression.ql b/c/cert/src/rules/CON40-C/AtomicVariableTwiceInExpression.ql
@@ -14,6 +14,7 @@
 
 import cpp
 import codingstandards.c.cert
+import codingstandards.cpp.Concurrency
 
 from MacroInvocation mi, Variable v, Locatable whereFound
 where
@@ -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

diff --git a/c/cert/src/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.ql b/c/cert/src/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.ql
@@ -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."
+
diff --git a/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected b/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected
@@ -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 |
diff --git a/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected.clang b/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected.clang
@@ -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 |
diff --git a/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected.gcc b/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected.gcc
@@ -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 |
diff --git a/c/cert/test/rules/CON40-C/test.c b/c/cert/test/rules/CON40-C/test.c
@@ -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
@@ -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; }

diff --git a/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected b/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected
@@ -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. |
diff --git a/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected.clang b/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected.clang
@@ -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. |
diff --git a/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected.gcc b/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected.gcc
@@ -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. |
diff --git a/c/cert/test/rules/CON41-C/test.c b/c/cert/test/rules/CON41-C/test.c
@@ -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 */
   }
@@ -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 */

diff --git a/change_notes/2023-03-06-better-modeling-of-stdatomic.md b/change_notes/2023-03-06-better-modeling-of-stdatomic.md
@@ -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`.
diff --git a/cpp/common/src/codingstandards/cpp/Concurrency.qll b/cpp/common/src/codingstandards/cpp/Concurrency.qll
@@ -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()
+    )
+  }
+}