Package: Side effects3

.vscode/tasks.json

@@ -203,8 +203,8 @@
                 "Concurrency1",
                 "Concurrency2",
                 "Concurrency3",
-                "Concurrency4",                
-                "Concurrency5",                
+                "Concurrency4",
+                "Concurrency5",
                 "Conditionals",
                 "Const",
                 "DeadCode",
@@ -257,6 +257,7 @@
                 "Scope",
                 "SideEffects1",
                 "SideEffects2",
+                "SideEffects3",
                 "SmartPointers1",
                 "SmartPointers2",
                 "Strings",

c/common/src/codingstandards/c/Expr.qll

@@ -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()
   }
 }
 

c/common/src/codingstandards/c/Ordering.qll

@@ -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,
@@ -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.
@@ -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
+        )
       )
     }
 

c/common/src/codingstandards/c/SideEffects.qll

@@ -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;`

c/common/test/library/expr/FullExpr.expected

@@ -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 |

c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql

@@ -0,0 +1,226 @@
+/**
+ * @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) {
+  (
+    e.(VariableEffect).getAnAccess() = fe.getAChild+()
+    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
+  )
+}
+
+from
+  ConstituentExprOrdering orderingConfig, FullExpr fullExpr, VariableEffect variableEffect1,
+  VariableAccess va1, VariableAccess va2, Locatable placeHolder, string label
+where
+  not isExcluded(fullExpr, SideEffects3Package::unsequencedSideEffectsQuery()) and
+  // 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 |
+    ce.getThen().getAChild*() = va1 and ce.getElse().getAChild*() = va2
+  )
+select fullExpr, "The expression contains unsequenced $@ to $@ and $@ to $@.", variableEffect1,
+  "side effect", va1, va1.getTarget().getName(), placeHolder, label, va2, va2.getTarget().getName()

c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.expected

@@ -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 |

c/misra/test/rules/RULE-13-2/UnsequencedSideEffects.qlref

@@ -0,0 +1 @@
+rules/RULE-13-2/UnsequencedSideEffects.ql