Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
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 .vscode/tasks.json
Original file line number Diff line number Diff line change
Expand Up @@ -203,8 +203,8 @@
"Concurrency1",
"Concurrency2",
"Concurrency3",
"Concurrency4",
"Concurrency5",
"Concurrency4",
"Concurrency5",
"Conditionals",
"Const",
"DeadCode",
Expand Down Expand Up @@ -257,6 +257,7 @@
"Scope",
"SideEffects1",
"SideEffects2",
"SideEffects3",
"SmartPointers1",
"SmartPointers2",
"Strings",
Expand Down
15 changes: 13 additions & 2 deletions c/common/src/codingstandards/c/Expr.qll
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,19 @@ import cpp
/* A full expression as defined in ISO/IEC 9899:2011 6.8 point 4 and Annex C point 1 item 5. */
class FullExpr extends Expr {
FullExpr() {
not this.getParent() instanceof Expr and
not exists(Variable v | v.getInitializer().getExpr() = this)
exists(ExprStmt s | this = s.getExpr())
or
exists(Loop l | this = l.getControllingExpr())
or
exists(ConditionalStmt s | this = s.getControllingExpr())
or
exists(ForStmt s | this = s.getUpdate())
or
exists(ReturnStmt s | this = s.getExpr())
or
this instanceof AggregateLiteral
or
this = any(Variable v).getInitializer().getExpr()
}
}

Expand Down
35 changes: 26 additions & 9 deletions c/common/src/codingstandards/c/Ordering.qll
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ module Ordering {
/**
* 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:
* - after a full declarator as described in 6.7.6 point 3.
* - 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,
Expand All @@ -28,36 +27,36 @@ module Ordering {
// before the actual call.
exists(Call call |
(
call.getAnArgument() = e1
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() = e1
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-righ evaluation and there is
// 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() = e1 and blop.getRightOperand() = e2
blop.getLeftOperand().getAChild*() = e1 and blop.getRightOperand().getAChild*() = e2
)
or
// 6.5.17 point 2 - There is a sequence pointt between the left operand and the right operand.
// 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 = e1.getParent*() and rhs = e2.getParent*()
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() = e1 and
(cond.getThen() = e2 or cond.getElse() = e2)
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.
Expand All @@ -68,6 +67,24 @@ module Ordering {
// 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
)
)
}

Expand Down
2 changes: 1 addition & 1 deletion c/common/src/codingstandards/c/SideEffects.qll
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ private class VolatileAccess extends GlobalSideEffect::Range, VariableAccess {
this.getTarget().isVolatile() and
// Exclude value computation of an lvalue expression soley used to determine the identity
// of the object. As noted in the footnote of 6.5.16 point 3 it is implementation dependend
// whether the value of the assignment expression deterived from the left operand after the assignment
// whether the value of the assignment expression derived from the left operand after the assignment
// is determined by reading the object. We assume it is not for assignments that are a child of an
// expression statement because the value is not used and is required for the compliant MISRA-C:2012 case:
// `extern volatile int v; v = v & 0x80;`
Expand Down
2 changes: 1 addition & 1 deletion c/common/test/library/expr/FullExpr.expected
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
| fullexpr.c:8:18:11:37 | temporary object |
| fullexpr.c:8:18:11:37 | {...} |
| fullexpr.c:13:3:13:5 | ... ++ |
| fullexpr.c:15:7:15:7 | i |
| fullexpr.c:17:10:17:10 | i |
Expand Down
249 changes: 249 additions & 0 deletions c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,249 @@
/**
* @id c/misra/unsequenced-side-effects
* @name RULE-13-2: The value of an expression and its persistent side effects depend on its evaluation order
* @description The value of an expression and its persistent side effects are depending on the
* evaluation order resulting in unpredictable behavior.
* @kind problem
* @precision very-high
* @problem.severity error
* @tags external/misra/id/rule-13-2
* correctness
* external/misra/obligation/required
*/

import cpp
import codingstandards.c.misra
import codingstandards.c.Expr
import codingstandards.c.SideEffects
import codingstandards.c.Ordering

class VariableEffectOrAccess extends Expr {
VariableEffectOrAccess() {
this instanceof VariableEffect or
this instanceof VariableAccess
}
}

pragma[noinline]
predicate partOfFullExpr(VariableEffectOrAccess e, FullExpr fe) {
(
exists(VariableEffect ve | e = ve and ve.getAnAccess() = fe.getAChild+() and not ve.isPartial())
or
e.(VariableAccess) = fe.getAChild+()
)
}

class ConstituentExprOrdering extends Ordering::Configuration {
ConstituentExprOrdering() { this = "ConstituentExprOrdering" }

override predicate isCandidate(Expr e1, Expr e2) {
exists(FullExpr fe |
partOfFullExpr(e1, fe) and
partOfFullExpr(e2, fe)
)
}
}

predicate sameFullExpr(FullExpr fe, VariableAccess va1, VariableAccess va2) {
partOfFullExpr(va1, fe) and
partOfFullExpr(va2, fe) and
va1 != va2 and
exists(Variable v1, Variable v2 |
// Use `pragma[only_bind_into]` to prevent CP between variable accesses.
va1.getTarget() = pragma[only_bind_into](v1) and va2.getTarget() = pragma[only_bind_into](v2)
|
v1.isVolatile() and v2.isVolatile()
or
not (v1.isVolatile() and v2.isVolatile()) and
v1 = v2
)
}

int getLeafCount(LeftRightOperation bop) {
if
not bop.getLeftOperand() instanceof BinaryOperation and
not bop.getRightOperand() instanceof BinaryOperation
then result = 2
else
if
bop.getLeftOperand() instanceof BinaryOperation and
not bop.getRightOperand() instanceof BinaryOperation
then result = 1 + getLeafCount(bop.getLeftOperand())
else
if
not bop.getLeftOperand() instanceof BinaryOperation and
bop.getRightOperand() instanceof BinaryOperation
then result = 1 + getLeafCount(bop.getRightOperand())
else result = getLeafCount(bop.getLeftOperand()) + getLeafCount(bop.getRightOperand())
}

class LeftRightOperation extends Expr {
LeftRightOperation() {
this instanceof BinaryOperation or
this instanceof AssignOperation or
this instanceof AssignExpr
}

Expr getLeftOperand() {
result = this.(BinaryOperation).getLeftOperand()
or
result = this.(AssignOperation).getLValue()
or
result = this.(AssignExpr).getLValue()
}

Expr getRightOperand() {
result = this.(BinaryOperation).getRightOperand()
or
result = this.(AssignOperation).getRValue()
or
result = this.(AssignExpr).getRValue()
}

Expr getAnOperand() {
result = getLeftOperand() or
result = getRightOperand()
}
}

int getOperandIndexIn(FullExpr fullExpr, Expr operand) {
result = getOperandIndex(fullExpr, operand)
or
fullExpr.(Call).getArgument(result).getAChild*() = operand
}

int getOperandIndex(LeftRightOperation binop, Expr operand) {
if operand = binop.getAnOperand()
then
operand = binop.getLeftOperand() and
result = 0
or
operand = binop.getRightOperand() and
result = getLeafCount(binop.getLeftOperand()) + 1
or
operand = binop.getRightOperand() and
not binop.getLeftOperand() instanceof LeftRightOperation and
result = 1
else (
// Child of left operand that is a binary operation.
result = getOperandIndex(binop.getLeftOperand(), operand)
or
// Child of left operand that is not a binary operation.
result = 0 and
not binop.getLeftOperand() instanceof LeftRightOperation and
binop.getLeftOperand().getAChild+() = operand
or
// Child of right operand and both left and right operands are binary operations.
result =
getLeafCount(binop.getLeftOperand()) + getOperandIndex(binop.getRightOperand(), operand)
or
// Child of right operand and left operand is not a binary operation.
result = 1 + getOperandIndex(binop.getRightOperand(), operand) and
not binop.getLeftOperand() instanceof LeftRightOperation
or
// Child of right operand that is not a binary operation and the left operand is a binary operation.
result = getLeafCount(binop.getLeftOperand()) + 1 and
binop.getRightOperand().getAChild+() = operand and
not binop.getRightOperand() instanceof LeftRightOperation
or
// Child of right operand that is not a binary operation and the left operand is not a binary operation.
result = 1 and
not binop.getLeftOperand() instanceof LeftRightOperation and
not binop.getRightOperand() instanceof LeftRightOperation and
binop.getRightOperand().getAChild+() = operand
)
}

predicate inConditionalThen(ConditionalExpr ce, Expr e) {
e = ce.getThen()
or
exists(Expr parent |
inConditionalThen(ce, parent) and
parent.getAChild() = e
)
}

predicate inConditionalElse(ConditionalExpr ce, Expr e) {
e = ce.getElse()
or
exists(Expr parent |
inConditionalElse(ce, parent) and
parent.getAChild() = e
)
}

predicate isUnsequencedEffect(
ConstituentExprOrdering orderingConfig, 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
// We are only interested in effects that change an object,
// i.e., exclude patterns suchs as `b->data[b->cursor++]` where `b` is considered modified and read or `foo.bar = 1` where `=` modifies to both `foo` and `bar`.
not variableEffect1.isPartial() and
variableEffect1.getAnAccess() = va1 and
(
exists(VariableEffect variableEffect2 |
not variableEffect2.isPartial() and
variableEffect2.getAnAccess() = va2 and
// If the effect is not local (happens in a different function) we use the call with the access as a proxy.
(
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
va2.getEnclosingStmt() = variableEffect2.getEnclosingStmt() and
orderingConfig.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)
)
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)
)
) and
// Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
// This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration.
getOperandIndexIn(fullExpr, va1) < getOperandIndexIn(fullExpr, va2) and
placeHolder = variableEffect2 and
label = "side effect"
)
or
placeHolder = va2 and
label = "read" and
not exists(VariableEffect variableEffect2 | variableEffect1 != variableEffect2 |
variableEffect2.getAnAccess() = va2
) and
(
va1.getEnclosingStmt() = variableEffect1.getEnclosingStmt() and
orderingConfig.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)
)
) and
// The read is not used to compute the effect on the variable.
// E.g., exclude x = x + 1
not variableEffect1.getAChild+() = va2
) and
// Both are evaluated
not exists(ConditionalExpr ce | inConditionalThen(ce, va1) and inConditionalElse(ce, va2))
}

from
ConstituentExprOrdering orderingConfig, 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)
select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
"side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName()
6 changes: 6 additions & 0 deletions c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected
Original file line number Diff line number Diff line change
@@ -0,0 +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 |
1 change: 1 addition & 0 deletions c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.qlref
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rules/RULE-13-2/UnsequencedSideEffects.ql
Loading