Skip to content
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
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,14 @@ import codingstandards.c.cert
import codingstandards.cpp.SideEffect
import codingstandards.c.Ordering
import codingstandards.c.orderofevaluation.VariableAccessOrdering
import Ordering::Make<VariableAccessInFullExpressionOrdering> as FullExpressionOrdering

from
VariableAccessInFullExpressionOrdering config, FullExpr e, ScalarVariable v, VariableEffect ve,
VariableAccess va1, VariableAccess va2
from FullExpr e, ScalarVariable v, VariableEffect ve, VariableAccess va1, VariableAccess va2
where
not isExcluded(e, SideEffects1Package::dependenceOnOrderOfScalarEvaluationForSideEffectsQuery()) and
e = va1.(ConstituentExpr).getFullExpr() and
va1 = ve.getAnAccess() and
config.isUnsequenced(va1, va2) and
FullExpressionOrdering::isUnsequenced(va1, va2) and
v = va1.getTarget()
select e, "Scalar object referenced by $@ has a $@ that is unsequenced in relative to another $@.",
v, v.getName(), ve, "side-effect", va2, "side-effect or value computation"
159 changes: 73 additions & 86 deletions c/common/src/codingstandards/c/Ordering.qll
Original file line number Diff line number Diff line change
@@ -1,97 +1,84 @@
import cpp
import codingstandards.cpp.SideEffect
import codingstandards.c.Expr
import codingstandards.cpp.Variable

module Ordering {
abstract class Configuration extends string {
bindingset[this]
Configuration() { any() }
private import codingstandards.cpp.Ordering as CppCommonOrdering
import CppCommonOrdering::OrderingBase

abstract predicate isCandidate(Expr e1, Expr e2);
module CConfigBase {
class EvaluationNode = Expr;

/**
* Holds if `e1` is sequenced before `e2` as defined by Annex C in ISO/IEC 9899:2011
* This limits to expression and we do not consider the sequence points that are not amenable to modelling:
* - before a library function returns (see 7.1.4 point 3).
* - after the actions associated with each formatted I/O function conversion specifier (see 7.21.6 point 1 & 7.29.2 point 1).
* - between the expr before and after a call to a comparison function,
* between any call to a comparison function, and any movement of the objects passed
* as arguments to that call (see 7.22.5 point 5).
*/
predicate isSequencedBefore(Expr e1, Expr e2) {
isCandidate(e1, e2) and
not e1 = e2 and
pragma[inline]
Expr toExpr(Expr e) { result = e }

pragma[inline]
predicate sequencingEdge(Expr e1, Expr e2) { c11Ordering(e1, e2) }
}

pragma[inline]
predicate c11Ordering(Expr e1, Expr e2) {
// 6.5.2.2 point 10 - The evaluation of the function designator and the actual arguments are sequenced
// before the actual call.
exists(Call call |
(
// 6.5.2.2 point 10 - The evaluation of the function designator and the actual arguments are sequenced
// before the actual call.
exists(Call call |
(
call.getAnArgument().getAChild*() = e1
or
// Postfix expression designating the called function
// We current only handle call through function pointers because the postfix expression
// of regular function calls is not available. That is, identifying `f` in `f(...)`
call.(ExprCall).getExpr().getAChild*() = e1
) and
call.getTarget() = e2.getEnclosingFunction()
)
or
// 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-right evaluation and there is
// a sequence point between the first and second operand if the latter is evaluated.
exists(BinaryLogicalOperation blop |
blop instanceof LogicalAndExpr or blop instanceof LogicalOrExpr
|
blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2
)
or
// 6.5.17 point 2 - There is a sequence point between the left operand and the right operand.
exists(CommaExpr ce, Expr lhs, Expr rhs |
lhs = ce.getLeftOperand() and
rhs = ce.getRightOperand()
|
lhs.getAChild*() = e1 and rhs.getAChild*() = e2
)
call.getAnArgument().getAChild*() = e1
or
// 6.5.15 point 4 - There is a sequence point between the first operand and the evaluation of the second or third.
exists(ConditionalExpr cond |
cond.getCondition().getAChild*() = e1 and
(cond.getThen().getAChild*() = e2 or cond.getElse().getAChild*() = e2)
)
or
// Between the evaluation of a full expression and the next to be evaluated full expression.
// Note we don't strictly check if `e2` is the next to be evaluated full expression and rely on the
// `isCandidate` configuration to minimze the scope or related full expressions.
e1 instanceof FullExpr and e2 instanceof FullExpr
or
// The side effect of updating the stored value of the left operand is sequenced after the value computations of the left and right operands.
// See 6.5.16
e2.(Assignment).getAnOperand().getAChild*() = e1
or
// There is a sequence point after a full declarator as described in 6.7.6 point 3.
exists(DeclStmt declStmt, int i, int j | i < j |
declStmt
.getDeclarationEntry(i)
.(VariableDeclarationEntry)
.getVariable()
.getInitializer()
.getExpr()
.getAChild*() = e1 and
declStmt
.getDeclarationEntry(j)
.(VariableDeclarationEntry)
.getVariable()
.getInitializer()
.getExpr()
.getAChild*() = e2
)
)
}

predicate isUnsequenced(Expr e1, Expr e2) {
isCandidate(e1, e2) and
not isSequencedBefore(e1, e2) and
not isSequencedBefore(e2, e1)
}
// Postfix expression designating the called function
// We current only handle call through function pointers because the postfix expression
// of regular function calls is not available. That is, identifying `f` in `f(...)`
call.(ExprCall).getExpr().getAChild*() = e1
) and
call.getTarget() = e2.getEnclosingFunction()
)
or
// 6.5.13 point 4 & 6.5.14 point 4 - The operators guarantee left-to-right evaluation and there is
// a sequence point between the first and second operand if the latter is evaluated.
exists(BinaryLogicalOperation blop |
blop instanceof LogicalAndExpr or blop instanceof LogicalOrExpr
|
blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2
)
or
// 6.5.17 point 2 - There is a sequence point between the left operand and the right operand.
exists(CommaExpr ce, Expr lhs, Expr rhs |
lhs = ce.getLeftOperand() and
rhs = ce.getRightOperand()
|
lhs.getAChild*() = e1 and rhs.getAChild*() = e2
)
or
// 6.5.15 point 4 - There is a sequence point between the first operand and the evaluation of the second or third.
exists(ConditionalExpr cond |
cond.getCondition().getAChild*() = e1 and
(cond.getThen().getAChild*() = e2 or cond.getElse().getAChild*() = e2)
)
or
// Between the evaluation of a full expression and the next to be evaluated full expression.
// Note we don't strictly check if `e2` is the next to be evaluated full expression and rely on the
// `isCandidate` configuration to minimze the scope or related full expressions.
e1 instanceof FullExpr and e2 instanceof FullExpr
or
// The side effect of updating the stored value of the left operand is sequenced after the value computations of the left and right operands.
// See 6.5.16
e2.(Assignment).getAnOperand().getAChild*() = e1
or
// There is a sequence point after a full declarator as described in 6.7.6 point 3.
exists(DeclStmt declStmt, int i, int j | i < j |
declStmt
.getDeclarationEntry(i)
.(VariableDeclarationEntry)
.getVariable()
.getInitializer()
.getExpr()
.getAChild*() = e1 and
declStmt
.getDeclarationEntry(j)
.(VariableDeclarationEntry)
.getVariable()
.getInitializer()
.getExpr()
.getAChild*() = e2
)
}
}
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
import cpp
import codingstandards.c.Ordering
import codingstandards.c.SideEffects

class VariableAccessInFullExpressionOrdering extends Ordering::Configuration {
VariableAccessInFullExpressionOrdering() { this = "VariableAccessInFullExpressionOrdering" }
module VariableAccessInFullExpressionOrdering implements Ordering::ConfigSig {
import Ordering::CConfigBase

override predicate isCandidate(Expr e1, Expr e2) { isCandidate(_, e1, e2) }
predicate isCandidate(Expr e1, Expr e2) { isCandidate(_, e1, e2) }
}

pragma[noinline]
Expand Down
14 changes: 8 additions & 6 deletions c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,10 @@ import codingstandards.c.Ordering
import codingstandards.c.orderofevaluation.VariableAccessOrdering
import codingstandards.cpp.StdFunctionOrMacro

class AtomicAccessInFullExpressionOrdering extends Ordering::Configuration {
AtomicAccessInFullExpressionOrdering() { this = "AtomicAccessInFullExpressionOrdering" }
module AtomicAccessInFullExpressionOrdering implements Ordering::ConfigSig {
import Ordering::CConfigBase

override predicate isCandidate(Expr e1, Expr e2) {
predicate isCandidate(Expr e1, Expr e2) {
exists(AtomicVariableAccess a, AtomicVariableAccess b, FullExpr e | a = e1 and b = e2 |
a.getTarget() = b.getTarget() and
a.getARead().(ConstituentExpr).getFullExpr() = e and
Expand Down Expand Up @@ -91,9 +91,11 @@ class AtomicVariableAccess extends VariableAccess {
}
}

import Ordering::Make<AtomicAccessInFullExpressionOrdering> as AtomicOrdering

from
AtomicAccessInFullExpressionOrdering config, FullExpr e, Variable v, AtomicVariableAccess va1,
AtomicVariableAccess va2, Expr va1Read, Expr va2Read
FullExpr e, Variable v, AtomicVariableAccess va1, AtomicVariableAccess va2, Expr va1Read,
Expr va2Read
where
not isExcluded(e, SideEffects3Package::unsequencedAtomicReadsQuery()) and
va1Read = va1.getARead() and
Expand All @@ -103,7 +105,7 @@ where
// for instance in gcc where atomic functions expand to StmtExprs, which have clear sequences.
// In this case, the result of `getARead()` for a pair of atomic function calls may be
// unsequenced even though the `VariableAccess`es within those calls are not.
config.isUnsequenced(va1Read, va2Read) and
AtomicOrdering::isUnsequenced(va1Read, va2Read) and
v = va1.getTarget() and
v = va2.getTarget() and
// Exclude cases where the variable is assigned a value tainted by the other variable access.
Expand Down
28 changes: 15 additions & 13 deletions c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@ predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) {
)
}

class ConstituentExprOrdering extends Ordering::Configuration {
ConstituentExprOrdering() { this = "ConstituentExprOrdering" }
module ConstituentExprOrderingConfig implements Ordering::ConfigSig {
import Ordering::CConfigBase

override predicate isCandidate(Expr e1, Expr e2) {
predicate isCandidate(Expr e1, Expr e2) {
exists(FullExpr fe |
partOfFullExpr(e1, fe) and
partOfFullExpr(e2, fe)
Expand Down Expand Up @@ -172,9 +172,11 @@ predicate inConditionalElse(ConditionalExpr ce, Expr e) {
)
}

import Ordering::Make<ConstituentExprOrderingConfig> as ConstituentExprOrdering

predicate isUnsequencedEffect(
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
FullExpr fullExpr, VariableEffect variableEffect1, VariableAccess va1, VariableAccess va2,
Locatable placeHolder, string label
) {
// The two access are scoped to the same full expression.
sameFullExpr(fullExpr, va1, va2) and
Expand All @@ -190,22 +192,22 @@ predicate isUnsequencedEffect(
(
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
orderingConfig.isUnsequenced(variableEffect1, variableEffect2)
ConstituentExprOrdering::isUnsequenced(variableEffect1, variableEffect2)
or
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
not va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
exists(Call call |
call.getAnArgument() = va2 and call.getEnclosingStmt() = va1.getEnclosingStmt()
|
orderingConfig.isUnsequenced(variableEffect1, call)
ConstituentExprOrdering::isUnsequenced(variableEffect1, call)
)
or
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
exists(Call call |
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
|
orderingConfig.isUnsequenced(call, variableEffect2)
ConstituentExprOrdering::isUnsequenced(call, variableEffect2)
)
) and
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
Expand All @@ -222,13 +224,13 @@ predicate isUnsequencedEffect(
) and
(
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
orderingConfig.isUnsequenced(variableEffect1, va2)
ConstituentExprOrdering::isUnsequenced(variableEffect1, va2)
or
not va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
exists(Call call |
call.getAnArgument() = va1 and call.getEnclosingStmt() = va2.getEnclosingStmt()
|
orderingConfig.isUnsequenced(call, va2)
ConstituentExprOrdering::isUnsequenced(call, va2)
)
) and
// The read is not used to compute the effect on the variable.
Expand All @@ -240,10 +242,10 @@ predicate isUnsequencedEffect(
}

from
ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
FullExpr fullExpr, VariableEffect variableEffect1, VariableAccess va1, VariableAccess va2,
Locatable placeHolder, string label
where
not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and
isUnsequencedEffect(orderingConfig, fullExpr, variableEffect1, va1, va2, placeHolder, label)
isUnsequencedEffect(fullExpr, variableEffect1, va1, va2, placeHolder, label)
select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
"side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName()
6 changes: 3 additions & 3 deletions c/misra/test/rules/RULE-13-2/UnsequencedAtomicReads.expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:112,31-39)
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:112,67-75)
WARNING: module 'TaintTracking' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:112,5-18)
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:114,31-39)
WARNING: module 'DataFlow' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:114,67-75)
WARNING: module 'TaintTracking' has been deprecated and may be removed in future (UnsequencedAtomicReads.ql:114,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 |
5 changes: 5 additions & 0 deletions change_notes/2026-2-20-update-expression-sequencing.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
- `A5-0-1`, `EXP50-CPP` - `ExpressionShouldNotRelyONOrderOfEvaluation.ql`, `DoNotDependOnTheOrderOfScalarObjectEvaluationForSideEffects.ql`:
- Fixed a bug where some sequenced operations were not detected as such due to an error in the "candidate selection" process. This could have complex effects on results, but should mostly fix false positives. Some unsequenced operations that previously reported one alert may now report two, due to the extra candidates being considered.
- Sequencing between full expressions no longer requires that the expressions are sequential; expressions in separate if statements, for instance, are not necessarily sequential, but they are still ordered. It is unclear if this change will have any effect on results, but it should be more accurate to the standard.
- `RULE-13-2`, `A5-0-1`, `EXP50-CPP`, `EXP30-C` - `UnsequencedSideEffects.ql`, `UnsequencedAtomicReads.ql`, `ExpressionShouldNotRelyONOrderOfEvaluation.ql`, `DoNotDependOnTheOrderOfScalarObjectEvaluationForSideEffects.ql`, `DependenceOnOrderOfScalarEvaluationForSideEffects.ql`:
- Implementation of ordering has been refactored to share more code across specifications (C11-C17, C++14, and C++17 sequencing rules). No change in results is expected from this refactor.
Original file line number Diff line number Diff line change
Expand Up @@ -15,20 +15,21 @@

import cpp
import codingstandards.cpp.autosar
import codingstandards.cpp.SideEffect
import codingstandards.cpp.sideeffect.DefaultEffects
import codingstandards.cpp.rules.expressionwithunsequencedsideeffects.ExpressionWithUnsequencedSideEffects
import codingstandards.cpp.Ordering
import codingstandards.cpp.orderofevaluation.VariableAccessOrdering
import Ordering::Make<Cpp14VariableAccessInFullExpressionOrdering> as FullExprOrdering

from
VariableAccessInFullExpressionOrdering config, FullExpr e, VariableEffect ve, VariableAccess va1,
VariableAccess va2, Variable v
where
not isExcluded(e, OrderOfEvaluationPackage::expressionShouldNotRelyOnOrderOfEvaluationQuery()) and
e = va1.(ConstituentExpr).getFullExpr() and
va1 = ve.getAnAccess() and
config.isUnsequenced(va1, va2) and
v = va1.getTarget()
select e,
"The evaluation is depended on the order of evaluation of $@, that is modified by $@ and $@, that both access $@.",
va1, "sub-expression", ve, "expression", va2, "sub-expression", v, v.getName()
module ExpressionShouldNotRelyOnOrderOfEvaluationConfig implements
ExpressionWithUnsequencedSideEffectsConfigSig
{
Query getQuery() {
result = OrderOfEvaluationPackage::expressionShouldNotRelyOnOrderOfEvaluationQuery()
}

predicate isUnsequenced(VariableAccess va1, VariableAccess va2) {
FullExprOrdering::isUnsequenced(va1, va2)
}
}

import ExpressionWithUnsequencedSideEffects<ExpressionShouldNotRelyOnOrderOfEvaluationConfig>
Loading
Loading