From ae63dcbd93178c83693ec7c06b0105be3088c445 Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Wed, 18 Dec 2024 18:28:45 -0800 Subject: [PATCH 1/4] Implement most MISRA-C amendment4 rule amendments --- amendments.csv | 10 +- .../includes/standard-library/stdatomic.h | 74 +++++++++++++-- .../rules/readofuninitializedmemory/test.c | 2 + ...weenObjectPointerAndDifferentObjectType.ql | 6 +- ...CastRemovesConstOrVolatileQualification.ql | 4 + .../rules/RULE-13-2/UnsequencedAtomicReads.ql | 94 +++++++++++++++++++ ...CharacterSequencesAndUsedWithinAComment.ql | 33 ++++--- ...jectPointerAndDifferentObjectType.expected | 4 + c/misra/test/rules/RULE-11-3/test.c | 6 ++ ...movesConstOrVolatileQualification.expected | 4 + c/misra/test/rules/RULE-11-8/test.c | 7 ++ .../RULE-13-2/UnsequencedAtomicReads.expected | 5 + .../RULE-13-2/UnsequencedAtomicReads.qlref | 1 + .../RULE-13-2/UnsequencedSideEffects.expected | 12 +-- c/misra/test/rules/RULE-13-2/test.c | 13 +++ ...terSequencesAndUsedWithinAComment.expected | 2 + c/misra/test/rules/RULE-3-1/test.c | 15 +++ ...ment-misra-c-amendment4-rule-amendments.md | 10 ++ .../cpp/exclusions/c/SideEffects3.qll | 20 +++- .../ReadOfUninitializedMemory.qll | 2 + .../rules/readofuninitializedmemory/test.cpp | 2 + rule_packages/c/SideEffects3.json | 12 +++ 22 files changed, 307 insertions(+), 31 deletions(-) create mode 100644 c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql create mode 100644 c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected create mode 100644 c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.qlref create mode 100644 change_notes/2024-12-13-implement-misra-c-amendment4-rule-amendments.md diff --git a/amendments.csv b/amendments.csv index ce285a29ba..bb2ceac27a 100644 --- a/amendments.csv +++ b/amendments.csv @@ -11,21 +11,21 @@ c,MISRA-C-2012,Amendment3,RULE-10-7,Yes,Refine,No,Import c,MISRA-C-2012,Amendment3,RULE-10-8,Yes,Refine,No,Import c,MISRA-C-2012,Amendment3,RULE-21-11,Yes,Clarification,No,Import c,MISRA-C-2012,Amendment3,RULE-21-12,Yes,Replace,No,Easy -c,MISRA-C-2012,Amendment4,RULE-11-3,Yes,Expand,No,Easy -c,MISRA-C-2012,Amendment4,RULE-11-8,Yes,Expand,No,Easy -c,MISRA-C-2012,Amendment4,RULE-13-2,Yes,Expand,No,Very Hard +c,MISRA-C-2012,Amendment4,RULE-11-3,Yes,Expand,Yes,Easy +c,MISRA-C-2012,Amendment4,RULE-11-8,Yes,Expand,Yes,Easy +c,MISRA-C-2012,Amendment4,RULE-13-2,Yes,Expand,Yes,Very Hard c,MISRA-C-2012,Amendment4,RULE-18-6,Yes,Expand,No,Medium c,MISRA-C-2012,Amendment4,RULE-18-8,Yes,Split,Yes,Easy c,MISRA-C-2012,Corrigendum2,RULE-2-2,Yes,Clarification,No,Import c,MISRA-C-2012,Corrigendum2,RULE-2-7,Yes,Clarification,No,Import -c,MISRA-C-2012,Corrigendum2,RULE-3-1,Yes,Refine,No,Easy +c,MISRA-C-2012,Corrigendum2,RULE-3-1,Yes,Refine,Yes,Easy c,MISRA-C-2012,Corrigendum2,RULE-8-6,Yes,Clarification,No,Import c,MISRA-C-2012,Corrigendum2,RULE-8-9,Yes,Clarification,No,Import c,MISRA-C-2012,Corrigendum2,RULE-9-4,Yes,Clarification,No,Import c,MISRA-C-2012,Corrigendum2,RULE-10-1,Yes,Clarification,No,Import c,MISRA-C-2012,Corrigendum2,RULE-18-3,Yes,Clarification,No,Import c,MISRA-C-2012,Corrigendum2,RULE-1-4,Yes,Replace,No,Easy -c,MISRA-C-2012,Corrigendum2,RULE-9-1,Yes,Refine,No,Easy +c,MISRA-C-2012,Corrigendum2,RULE-9-1,Yes,Refine,Yes,Easy c,MISRA-C-2012,Corrigendum2,RULE-9-2,Yes,Refine,No,Import c,MISRA-C-2012,Corrigendum2,DIR-4-10,Yes,Clarification,No,Import c,MISRA-C-2012,Corrigendum2,RULE-7-4,Yes,Refine,No,Easy diff --git a/c/common/test/includes/standard-library/stdatomic.h b/c/common/test/includes/standard-library/stdatomic.h index 66b74ae61a..49a5b3cfcd 100644 --- a/c/common/test/includes/standard-library/stdatomic.h +++ b/c/common/test/includes/standard-library/stdatomic.h @@ -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; \ No newline at end of file +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) \ No newline at end of file diff --git a/c/common/test/rules/readofuninitializedmemory/test.c b/c/common/test/rules/readofuninitializedmemory/test.c index ce2c60484e..e76c5a22b3 100644 --- a/c/common/test/rules/readofuninitializedmemory/test.c +++ b/c/common/test/rules/readofuninitializedmemory/test.c @@ -94,4 +94,6 @@ void test_non_default_init() { static struct A ss; use_struct_A( ss); // COMPLIANT - static struct type variables are zero initialized + _Atomic int x; + use_int(x); // COMPLIANT - atomics are special, covered by other rules } \ No newline at end of file diff --git a/c/misra/src/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.ql b/c/misra/src/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.ql index 8292bd3b6f..c51ecbc81d 100644 --- a/c/misra/src/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.ql +++ b/c/misra/src/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.ql @@ -23,7 +23,11 @@ where baseTypeFrom = cast.getExpr().getType().(PointerToObjectType).getBaseType() and baseTypeTo = cast.getType().(PointerToObjectType).getBaseType() and // exception: cast to a char, signed char, or unsigned char is permitted - not baseTypeTo.stripType() instanceof CharType and + not ( + baseTypeTo.stripType() instanceof CharType and + // Exception does not apply to _Atomic types + not baseTypeFrom.hasSpecifier("atomic") + ) and ( ( baseTypeFrom.isVolatile() and not baseTypeTo.isVolatile() diff --git a/c/misra/src/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.ql b/c/misra/src/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.ql index 17b12aaf99..c0f447d5b5 100644 --- a/c/misra/src/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.ql +++ b/c/misra/src/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.ql @@ -24,5 +24,9 @@ where baseTypeFrom.isVolatile() and not baseTypeTo.isVolatile() and qualificationName = "volatile" or baseTypeFrom.isConst() and not baseTypeTo.isConst() and qualificationName = "const" + or + baseTypeFrom.hasSpecifier("atomic") and + not baseTypeTo.hasSpecifier("atomic") and + qualificationName = "atomic" ) select cast, "Cast of pointer removes " + qualificationName + " qualification from its base type." diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql b/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql new file mode 100644 index 0000000000..d7638229d6 --- /dev/null +++ b/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql @@ -0,0 +1,94 @@ +/** + * @id c/misra/unsequenced-atomic-reads + * @name RULE-13-2: The value of an atomic variable depend on its evaluation order and interleave of threads + * @description The value of an atomic variable shall not depend on evaluation order and + * interleaving of threads. + * @kind problem + * @precision very-high + * @problem.severity error + * @tags external/misra/id/rule-13-2 + * correctness + * external/misra/c/2012/amendment3 + * external/misra/obligation/required + */ + +import cpp +import semmle.code.cpp.dataflow.TaintTracking +import codingstandards.c.misra +import codingstandards.c.Ordering +import codingstandards.c.orderofevaluation.VariableAccessOrdering + +class AtomicAccessInFullExpressionOrdering extends Ordering::Configuration { + AtomicAccessInFullExpressionOrdering() { this = "AtomicAccessInFullExpressionOrdering" } + + override predicate isCandidate(Expr e1, Expr e2) { + exists(AtomicVariableAccess a, AtomicVariableAccess b, FullExpr e | a = e1 and b = e2 | + a.getTarget() = b.getTarget() and + a.(ConstituentExpr).getFullExpr() = e and + b.(ConstituentExpr).getFullExpr() = e and + not a = b + ) + } +} + +/** + * A read of a variable specified as `_Atomic`. + * + * Note, it may be accessed directly, or by passing its address into the std atomic functions. + */ +class AtomicVariableAccess extends VariableAccess { + pragma[noinline] + AtomicVariableAccess() { + getTarget().getType().hasSpecifier("atomic") + } + + /* Get the `atomic_()` call this VarAccess occurs in. */ + FunctionCall getAtomicFunctionCall() { + exists(AddressOfExpr addrParent, FunctionCall fc | + fc.getTarget().getName().matches("__c11_atomic%") and + addrParent = fc.getArgument(0) and + addrParent.getAnOperand() = this + and result = fc + ) + } + + /** + * Gets an assigned expr, either in the form `x = ` or `atomic_store(&x, )`. + */ + Expr getAnAssignedExpr() { + result = getAtomicFunctionCall().getArgument(1) + or + exists(AssignExpr assign | + assign.getLValue() = this + and result = assign.getRValue() + ) + } + + /** + * Gets the expression holding this variable access, either in the form `x` or `atomic_read(&x)`. + */ + Expr getARead() { + result = getAtomicFunctionCall() + or + result = this + } +} + +from + AtomicAccessInFullExpressionOrdering config, FullExpr e, Variable v, + AtomicVariableAccess va1, AtomicVariableAccess va2 +where + not isExcluded(e, SideEffects3Package::unsequencedAtomicReadsQuery()) and + e = va1.(ConstituentExpr).getFullExpr() and + config.isUnsequenced(va1, va2) and + v = va1.getTarget() and + v = va2.getTarget() and + // Exclude cases where the variable is assigned a value tainted by the other variable access. + not exists(Expr write | + write = va1.getAnAssignedExpr() and + TaintTracking::localTaint(DataFlow::exprNode(va2.getARead()), DataFlow::exprNode(write)) + ) and + // Impose an ordering, show the first access. + va1.getLocation().isBefore(va2.getLocation(), _) +select e, "Atomic variable $@ has a $@ that is unsequenced with $@.", + v, v.getName(), va1, "previous read", va2, "another read" diff --git a/c/misra/src/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.ql b/c/misra/src/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.ql index 6eb605dbd9..58d449a59b 100644 --- a/c/misra/src/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.ql +++ b/c/misra/src/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.ql @@ -16,27 +16,38 @@ import cpp import codingstandards.c.misra -class IllegalCCommentCharacter extends string { - IllegalCCommentCharacter() { - this = "/*" or - this = "//" - } +/* Character sequence is banned from all comment types */ +class IllegalCommentSequence extends string { + IllegalCommentSequence() { this = "/*" } } -class IllegalCPPCommentCharacter extends string { - IllegalCPPCommentCharacter() { this = "/*" } +/* A regexp to check for illegal C-style comments */ +class IllegalCCommentRegexp extends string { + IllegalCCommentRegexp() { + // Regexp to match "//" in C-style comments, which do not appear to be URLs. General format + // uses negative lookahead/lookbehind to match like `.*(? 0 + exists(IllegalCommentSequence c | illegalSequence = c | + comment.getContents().indexOf(illegalSequence) > 0 ) or - exists(IllegalCPPCommentCharacter c | illegalSequence = c | - comment.(CppStyleComment).getContents().indexOf(illegalSequence) > 0 + exists(IllegalCCommentRegexp c | illegalSequence = c.getDescription() | + comment.(CStyleComment).getContents().regexpMatch(c) ) ) select comment, "Comment contains an illegal sequence '" + illegalSequence + "'" diff --git a/c/misra/test/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.expected b/c/misra/test/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.expected index 94cf6ee635..24e6c4d5af 100644 --- a/c/misra/test/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.expected +++ b/c/misra/test/rules/RULE-11-3/CastBetweenObjectPointerAndDifferentObjectType.expected @@ -6,3 +6,7 @@ | test.c:21:3:21:16 | (int *)... | Cast performed between a pointer to object type (char) and a pointer to a different object type (int). | | test.c:22:20:22:21 | (int *)... | Cast performed between a pointer to object type (char) and a pointer to a different object type (int). | | test.c:23:3:23:18 | (long long *)... | Cast performed between a pointer to object type (int) and a pointer to a different object type (long long). | +| test.c:26:3:26:13 | (char *)... | Cast performed between a pointer to object type (_Atomic(int)) and a pointer to a different object type (char). | +| test.c:27:8:27:10 | (char *)... | Cast performed between a pointer to object type (_Atomic(int)) and a pointer to a different object type (char). | +| test.c:28:3:28:21 | (_Atomic(char) *)... | Cast performed between a pointer to object type (_Atomic(int)) and a pointer to a different object type (_Atomic(char)). | +| test.c:29:23:29:25 | (_Atomic(char) *)... | Cast performed between a pointer to object type (_Atomic(int)) and a pointer to a different object type (_Atomic(char)). | diff --git a/c/misra/test/rules/RULE-11-3/test.c b/c/misra/test/rules/RULE-11-3/test.c index 4730aeac03..0d91740438 100644 --- a/c/misra/test/rules/RULE-11-3/test.c +++ b/c/misra/test/rules/RULE-11-3/test.c @@ -21,4 +21,10 @@ void f1(void) { (int *const)v2; // NON_COMPLIANT int *const v10 = v2; // NON_COMPLIANT (long long *)v10; // NON_COMPLIANT + + _Atomic int *v11 = 0; + (char *)v11; // NON_COMPLIANT + v2 = v11; // NON_COMPLIANT + (_Atomic char *)v11; // NON_COMPLIANT + _Atomic char *v12 = v11; // NON_COMPLIANT } \ No newline at end of file diff --git a/c/misra/test/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.expected b/c/misra/test/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.expected index 48658e2176..aa7752d28a 100644 --- a/c/misra/test/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.expected +++ b/c/misra/test/rules/RULE-11-8/CastRemovesConstOrVolatileQualification.expected @@ -1,2 +1,6 @@ | test.c:4:19:4:33 | (const char *)... | Cast of pointer removes volatile qualification from its base type. | | test.c:6:13:6:21 | (char *)... | Cast of pointer removes const qualification from its base type. | +| test.c:9:3:9:11 | (char *)... | Cast of pointer removes atomic qualification from its base type. | +| test.c:10:7:10:7 | (char *)... | Cast of pointer removes atomic qualification from its base type. | +| test.c:11:3:11:17 | (const char *)... | Cast of pointer removes atomic qualification from its base type. | +| test.c:12:7:12:7 | (const char *)... | Cast of pointer removes atomic qualification from its base type. | diff --git a/c/misra/test/rules/RULE-11-8/test.c b/c/misra/test/rules/RULE-11-8/test.c index 75c7fc189a..e0e3b3a2fb 100644 --- a/c/misra/test/rules/RULE-11-8/test.c +++ b/c/misra/test/rules/RULE-11-8/test.c @@ -5,5 +5,12 @@ int f1(void) { const char *c2 = (const char *)c; // COMPLIANT char *d = (char *)c; // NON_COMPLIANT const char *e = (const char *)d; // COMPLIANT + _Atomic char *f = 0; + (char *)f; // NON_COMPLIANT + d = f; // NON_COMPLIANT + (const char *)f; // NON_COMPLIANT + e = f; // NON_COMPLIANT + (const _Atomic char *)f; // COMPLIANT + (const _Atomic char *)f; // COMPLIANT return 0; } \ No newline at end of file diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected b/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected new file mode 100644 index 0000000000..e84aef7128 --- /dev/null +++ b/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected @@ -0,0 +1,5 @@ +WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:89,31-39) +WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:89,67-75) +WARNING: module 'TaintTracking' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:89,5-18) +| test.c:44:12:44:18 | ... + ... | Atomic variable $@ has a $@ that is unsequenced with $@. | test.c:42:15:42:16 | a1 | a1 | test.c:44:12:44:13 | a1 | previous read | test.c:44:17:44:18 | a1 | another read | +| test.c:46:3:46:37 | ... + ... | Atomic variable $@ has a $@ that is unsequenced with $@. | test.c:42:15:42:16 | a1 | a1 | test.c:46:16:46:17 | a1 | previous read | test.c:46:35:46:36 | a1 | another read | diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.qlref b/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.qlref new file mode 100644 index 0000000000..46242df1b0 --- /dev/null +++ b/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.qlref @@ -0,0 +1 @@ +rules/RULE-13-2/UnsequencedAtomicReads.ql \ No newline at end of file diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected index 75bd8169ba..b6c704322c 100644 --- a/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected +++ b/c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected @@ -1,6 +1,6 @@ -| test.c:6:12:6:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:6:12:6:13 | l1 | side effect | test.c:6:12:6:13 | l1 | l1 | test.c:6:17:6:18 | l1 | side effect | test.c:6:17:6:18 | l1 | l1 | -| test.c:7:12:7:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:7:12:7:13 | l1 | side effect | test.c:7:12:7:13 | l1 | l1 | test.c:7:17:7:18 | l2 | side effect | test.c:7:17:7:18 | l2 | l2 | -| test.c:17:3:17:21 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:17:8:17:9 | l1 | side effect | test.c:17:8:17:9 | l1 | l1 | test.c:17:13:17:14 | l1 | side effect | test.c:17:13:17:14 | l1 | l1 | -| test.c:19:3:19:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:19:7:19:8 | l1 | side effect | test.c:19:7:19:8 | l1 | l1 | test.c:19:11:19:12 | l2 | side effect | test.c:19:11:19:12 | l2 | l2 | -| test.c:25:3:25:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:25:7:25:10 | ... ++ | side effect | test.c:25:7:25:8 | l8 | l8 | test.c:25:13:25:14 | l8 | read | test.c:25:13:25:14 | l8 | l8 | -| test.c:35:5:35:13 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:35:10:35:12 | ... ++ | side effect | test.c:35:10:35:10 | i | i | test.c:35:10:35:12 | ... ++ | side effect | test.c:35:10:35:10 | i | i | \ No newline at end of file +| test.c:8:12:8:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:8:12:8:13 | l1 | side effect | test.c:8:12:8:13 | l1 | l1 | test.c:8:17:8:18 | l1 | side effect | test.c:8:17:8:18 | l1 | l1 | +| test.c:9:12:9:18 | ... + ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:9:12:9:13 | l1 | side effect | test.c:9:12:9:13 | l1 | l1 | test.c:9:17:9:18 | l2 | side effect | test.c:9:17:9:18 | l2 | l2 | +| test.c:19:3:19:21 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:19:8:19:9 | l1 | side effect | test.c:19:8:19:9 | l1 | l1 | test.c:19:13:19:14 | l1 | side effect | test.c:19:13:19:14 | l1 | l1 | +| test.c:21:3:21:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:21:7:21:8 | l1 | side effect | test.c:21:7:21:8 | l1 | l1 | test.c:21:11:21:12 | l2 | side effect | test.c:21:11:21:12 | l2 | l2 | +| test.c:27:3:27:5 | call to foo | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:27:7:27:10 | ... ++ | side effect | test.c:27:7:27:8 | l8 | l8 | test.c:27:13:27:14 | l8 | read | test.c:27:13:27:14 | l8 | l8 | +| test.c:37:5:37:13 | ... = ... | The expression contains unsequenced $@ to $@ and $@ to $@. | test.c:37:10:37:12 | ... ++ | side effect | test.c:37:10:37:10 | i | i | test.c:37:10:37:12 | ... ++ | side effect | test.c:37:10:37:10 | i | i | diff --git a/c/misra/test/rules/RULE-13-2/test.c b/c/misra/test/rules/RULE-13-2/test.c index 1bebec3775..6821a37296 100644 --- a/c/misra/test/rules/RULE-13-2/test.c +++ b/c/misra/test/rules/RULE-13-2/test.c @@ -1,3 +1,5 @@ +#include + void foo(int, int); void unsequenced_sideeffects1() { @@ -34,4 +36,15 @@ void unsequenced_sideeffects2() { for (i = 0; i < 10; i++) { test(i++); // NON_COMPLIANT } +} + +void atomics() { + _Atomic int a1, a2; + int l3 = a1 + a2; // COMPLIANT + int l4 = a1 + a1; // NON_COMPLIANT + a1 = a1 + 1; // COMPLIANT + atomic_load(&a1) + atomic_load(&a1); // NON_COMPLIANT + atomic_load(&a1) + atomic_load(&a2); // COMPLIANT + atomic_store(&a1, atomic_load(&a1)); // COMPLIANT + atomic_store(&a1, a1); // COMPLIANT } \ No newline at end of file diff --git a/c/misra/test/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.expected b/c/misra/test/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.expected index 5e876cecc3..5008fb100d 100644 --- a/c/misra/test/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.expected +++ b/c/misra/test/rules/RULE-3-1/CharacterSequencesAndUsedWithinAComment.expected @@ -1,3 +1,5 @@ | test.c:9:1:9:8 | /* /* */ | Comment contains an illegal sequence '/*' | | test.c:12:1:12:8 | /* // */ | Comment contains an illegal sequence '//' | | test.c:21:1:21:7 | // /* | Comment contains an illegal sequence '/*' | +| test.c:30:1:30:27 | /* https://github.com // */ | Comment contains an illegal sequence '//' | +| test.c:33:1:33:60 | /* a://b, a://b., ://a.b, a://b., a://.b, ://, a://, ://b */ | Comment contains an illegal sequence '//' | diff --git a/c/misra/test/rules/RULE-3-1/test.c b/c/misra/test/rules/RULE-3-1/test.c index c1a135f972..ad61fd0f91 100644 --- a/c/misra/test/rules/RULE-3-1/test.c +++ b/c/misra/test/rules/RULE-3-1/test.c @@ -20,4 +20,19 @@ // NON_COMPLIANT // /* +// COMPLIANT +/* https://github.com */ + +// COMPLIANT +/* https://name-with-hyphen-and-num-12345.com */ + +// NON_COMPLIANT +/* https://github.com // */ + +// NON_COMPLIANT +/* a://b, a://b., ://a.b, a://b., a://.b, ://, a://, ://b */ + +// COMPLIANT +// https://github.com + void f(){} \ No newline at end of file diff --git a/change_notes/2024-12-13-implement-misra-c-amendment4-rule-amendments.md b/change_notes/2024-12-13-implement-misra-c-amendment4-rule-amendments.md new file mode 100644 index 0000000000..a8fbd282d8 --- /dev/null +++ b/change_notes/2024-12-13-implement-misra-c-amendment4-rule-amendments.md @@ -0,0 +1,10 @@ + - `RULE-11-3` - `CastBetweenObjectPointerAndDifferentObjectType.ql` + - Constrain exception that pointer types to may be cast to char types, so that it does not apply to atomic pointer types, in compliance with MISRA-C 2012 Amendment 4. + - `RULE-11-8` - `CastRemovesConstOrVolatileQualification.ql` + - Query expanded to detect cases of removing `_Atomic` qualification, in compliance with MISRA-C 2012 Amendment 4. + - `EXP33-C`, `RULE-9-1`, `A8-5-0`, `EXP53-CPP` - `DoNotReadUninitializedMemory.ql`, `ObjectWithAutoStorageDurationReadBeforeInit.ql`, `MemoryNotInitializedBeforeItIsRead.ql`, `DoNotReadUninitializedMemory.ql` + - Atomic local variables excluded from query results, in compliance with MISRA-C 2012 Amendment 4, and to reduce false positives in the other standards. + - `RULE-13-2` - `UnsequencedAtomicReads.ql` + - New query to find expressions which read an atomic variable more than once between sequence points, to address new case from MISRA-C 2012 Amendment 4. + - `RULE-3-1` - `CharacterSequencesAndUsedWithinAComment.ql` + - Add exception allowing URLs inside of cpp-style `/* ... */` comments, in compliance with MISRA-C 2012 Amendment 4 \ No newline at end of file diff --git a/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll b/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll index eff4f2caf9..7b01c18099 100644 --- a/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll +++ b/cpp/common/src/codingstandards/cpp/exclusions/c/SideEffects3.qll @@ -3,7 +3,9 @@ import cpp import RuleMetadata import codingstandards.cpp.exclusions.RuleMetadata -newtype SideEffects3Query = TUnsequencedSideEffectsQuery() +newtype SideEffects3Query = + TUnsequencedSideEffectsQuery() or + TUnsequencedAtomicReadsQuery() predicate isSideEffects3QueryMetadata(Query query, string queryId, string ruleId, string category) { query = @@ -14,6 +16,15 @@ predicate isSideEffects3QueryMetadata(Query query, string queryId, string ruleId "c/misra/unsequenced-side-effects" and ruleId = "RULE-13-2" and category = "required" + or + query = + // `Query` instance for the `unsequencedAtomicReads` query + SideEffects3Package::unsequencedAtomicReadsQuery() and + queryId = + // `@id` for the `unsequencedAtomicReads` query + "c/misra/unsequenced-atomic-reads" and + ruleId = "RULE-13-2" and + category = "required" } module SideEffects3Package { @@ -23,4 +34,11 @@ module SideEffects3Package { // `Query` type for `unsequencedSideEffects` query TQueryC(TSideEffects3PackageQuery(TUnsequencedSideEffectsQuery())) } + + Query unsequencedAtomicReadsQuery() { + //autogenerate `Query` type + result = + // `Query` type for `unsequencedAtomicReads` query + TQueryC(TSideEffects3PackageQuery(TUnsequencedAtomicReadsQuery())) + } } diff --git a/cpp/common/src/codingstandards/cpp/rules/readofuninitializedmemory/ReadOfUninitializedMemory.qll b/cpp/common/src/codingstandards/cpp/rules/readofuninitializedmemory/ReadOfUninitializedMemory.qll index 9de640db9c..8d701cb26c 100644 --- a/cpp/common/src/codingstandards/cpp/rules/readofuninitializedmemory/ReadOfUninitializedMemory.qll +++ b/cpp/common/src/codingstandards/cpp/rules/readofuninitializedmemory/ReadOfUninitializedMemory.qll @@ -131,6 +131,8 @@ class UninitializedVariable extends LocalVariable { // Not static or thread local, because they are not initialized with indeterminate values not isStatic() and not isThreadLocal() and + // Not atomic, which have special initialization rules + not getType().hasSpecifier("atomic") and // Not a class type, because default initialization of a class calls the default constructor // The default constructor may leave certain fields uninitialized, but that would be a separate // field-wise analysis diff --git a/cpp/common/test/rules/readofuninitializedmemory/test.cpp b/cpp/common/test/rules/readofuninitializedmemory/test.cpp index bdd3fdc203..6ed07d795f 100644 --- a/cpp/common/test/rules/readofuninitializedmemory/test.cpp +++ b/cpp/common/test/rules/readofuninitializedmemory/test.cpp @@ -121,4 +121,6 @@ void test_non_default_init() { use(slp); // COMPLIANT - static variables are zero initialized thread_local int *tlp; use(tlp); // COMPLIANT - thread local variables are zero initialized + _Atomic int ai; + use(ai); // COMPLIANT - atomics are special and not covered by this rule } \ No newline at end of file diff --git a/rule_packages/c/SideEffects3.json b/rule_packages/c/SideEffects3.json index 2bf91d77b9..369f5db9ee 100644 --- a/rule_packages/c/SideEffects3.json +++ b/rule_packages/c/SideEffects3.json @@ -16,6 +16,18 @@ "correctness", "external/misra/c/2012/third-edition-first-revision" ] + }, + { + "description": "The value of an atomic variable shall not depend on evaluation order and interleaving of threads.", + "kind": "problem", + "name": "The value of an atomic variable depend on its evaluation order and interleave of threads", + "precision": "very-high", + "severity": "error", + "short_name": "UnsequencedAtomicReads", + "tags": [ + "correctness", + "external/misra/c/2012/amendment3" + ] } ], "title": "The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders" From 8403a4bcd6d5f52afd8ab29441b33b52c002e3bd Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Wed, 18 Dec 2024 18:39:46 -0800 Subject: [PATCH 2/4] Fix format --- .../rules/RULE-13-2/UnsequencedAtomicReads.ql | 24 +++++++++---------- c/misra/test/rules/RULE-13-2/test.c | 8 +++---- 2 files changed, 15 insertions(+), 17 deletions(-) diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql b/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql index d7638229d6..68f00be15f 100644 --- a/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql +++ b/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql @@ -33,22 +33,20 @@ class AtomicAccessInFullExpressionOrdering extends Ordering::Configuration { /** * A read of a variable specified as `_Atomic`. - * + * * Note, it may be accessed directly, or by passing its address into the std atomic functions. */ class AtomicVariableAccess extends VariableAccess { pragma[noinline] - AtomicVariableAccess() { - getTarget().getType().hasSpecifier("atomic") - } + AtomicVariableAccess() { getTarget().getType().hasSpecifier("atomic") } /* Get the `atomic_()` call this VarAccess occurs in. */ FunctionCall getAtomicFunctionCall() { exists(AddressOfExpr addrParent, FunctionCall fc | fc.getTarget().getName().matches("__c11_atomic%") and addrParent = fc.getArgument(0) and - addrParent.getAnOperand() = this - and result = fc + addrParent.getAnOperand() = this and + result = fc ) } @@ -59,8 +57,8 @@ class AtomicVariableAccess extends VariableAccess { result = getAtomicFunctionCall().getArgument(1) or exists(AssignExpr assign | - assign.getLValue() = this - and result = assign.getRValue() + assign.getLValue() = this and + result = assign.getRValue() ) } @@ -75,8 +73,8 @@ class AtomicVariableAccess extends VariableAccess { } from - AtomicAccessInFullExpressionOrdering config, FullExpr e, Variable v, - AtomicVariableAccess va1, AtomicVariableAccess va2 + AtomicAccessInFullExpressionOrdering config, FullExpr e, Variable v, AtomicVariableAccess va1, + AtomicVariableAccess va2 where not isExcluded(e, SideEffects3Package::unsequencedAtomicReadsQuery()) and e = va1.(ConstituentExpr).getFullExpr() and @@ -89,6 +87,6 @@ where TaintTracking::localTaint(DataFlow::exprNode(va2.getARead()), DataFlow::exprNode(write)) ) and // Impose an ordering, show the first access. - va1.getLocation().isBefore(va2.getLocation(), _) -select e, "Atomic variable $@ has a $@ that is unsequenced with $@.", - v, v.getName(), va1, "previous read", va2, "another read" + va1.getLocation().isBefore(va2.getLocation(), _) +select e, "Atomic variable $@ has a $@ that is unsequenced with $@.", v, v.getName(), va1, + "previous read", va2, "another read" diff --git a/c/misra/test/rules/RULE-13-2/test.c b/c/misra/test/rules/RULE-13-2/test.c index 6821a37296..e1be53a037 100644 --- a/c/misra/test/rules/RULE-13-2/test.c +++ b/c/misra/test/rules/RULE-13-2/test.c @@ -40,11 +40,11 @@ void unsequenced_sideeffects2() { void atomics() { _Atomic int a1, a2; - int l3 = a1 + a2; // COMPLIANT - int l4 = a1 + a1; // NON_COMPLIANT - a1 = a1 + 1; // COMPLIANT + int l3 = a1 + a2; // COMPLIANT + int l4 = a1 + a1; // NON_COMPLIANT + a1 = a1 + 1; // COMPLIANT atomic_load(&a1) + atomic_load(&a1); // NON_COMPLIANT atomic_load(&a1) + atomic_load(&a2); // COMPLIANT atomic_store(&a1, atomic_load(&a1)); // COMPLIANT - atomic_store(&a1, a1); // COMPLIANT + atomic_store(&a1, a1); // COMPLIANT } \ No newline at end of file From 7732fd690d5704f939acc732e96581f83e00772b Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Thu, 19 Dec 2024 12:49:47 -0800 Subject: [PATCH 3/4] Fix cert test --- .../CON40-C/AtomicVariableTwiceInExpression.expected | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected b/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected index ddff311b59..42d3ea924d 100644 --- a/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected +++ b/c/cert/test/rules/CON40-C/AtomicVariableTwiceInExpression.expected @@ -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 | From 45e6b5289862db731a59e025ec5b2fab5ff8bc2a Mon Sep 17 00:00:00 2001 From: Mike Fairhurst Date: Fri, 20 Dec 2024 13:43:59 -0800 Subject: [PATCH 4/4] fix tests --- .../WrapFunctionsThatCanFailSpuriouslyInLoop.expected | 8 ++++---- .../test/rules/RULE-13-2/UnsequencedAtomicReads.expected | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected b/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected index 0c1e25cd00..b1c224173e 100644 --- a/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected +++ b/c/cert/test/rules/CON41-C/WrapFunctionsThatCanFailSpuriouslyInLoop.expected @@ -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. | diff --git a/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected b/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected index e84aef7128..2231a83735 100644 --- a/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected +++ b/c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected @@ -1,5 +1,5 @@ -WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:89,31-39) -WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:89,67-75) -WARNING: module 'TaintTracking' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:89,5-18) +WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:87,31-39) +WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:87,67-75) +WARNING: module 'TaintTracking' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:87,5-18) | test.c:44:12:44:18 | ... + ... | Atomic variable $@ has a $@ that is unsequenced with $@. | test.c:42:15:42:16 | a1 | a1 | test.c:44:12:44:13 | a1 | previous read | test.c:44:17:44:18 | a1 | another read | | test.c:46:3:46:37 | ... + ... | Atomic variable $@ has a $@ that is unsequenced with $@. | test.c:42:15:42:16 | a1 | a1 | test.c:46:16:46:17 | a1 | previous read | test.c:46:35:46:36 | a1 | another read |