Refactor Ordering from abstract classes to parametric module.

MichaelRFairhurst · MichaelRFairhurst · commit 12e6bb387a2f · 2026-02-19T16:00:20.000-08:00
Allows for code sharing between C and C++ even if the sequencing is different.

Initial implementation of split between c++14 and c++17 sequencing.
diff --git a/c/common/src/codingstandards/c/Ordering.qll b/c/common/src/codingstandards/c/Ordering.qll
@@ -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
+    )
   }
 }
diff --git a/c/common/src/codingstandards/c/orderofevaluation/VariableAccessOrdering.qll b/c/common/src/codingstandards/c/orderofevaluation/VariableAccessOrdering.qll
@@ -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]
diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql b/c/misra/src/rules/RULE-13-2/UnsequencedAtomicReads.ql
@@ -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
@@ -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
@@ -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.
diff --git a/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql b/c/misra/src/rules/RULE-13-2/UnsequencedSideEffects.ql
@@ -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)
@@ -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
@@ -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.
@@ -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.
@@ -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()
diff --git a/cpp/autosar/src/rules/A5-0-1/ExpressionShouldNotRelyOnOrderOfEvaluation.ql b/cpp/autosar/src/rules/A5-0-1/ExpressionShouldNotRelyOnOrderOfEvaluation.ql
@@ -19,15 +19,14 @@ import codingstandards.cpp.SideEffect
 import codingstandards.cpp.sideeffect.DefaultEffects
 import codingstandards.cpp.Ordering
 import codingstandards.cpp.orderofevaluation.VariableAccessOrdering
+import Ordering::Make<VariableAccessInFullExpressionOrdering> as FullExprOrdering
 
-from
-  VariableAccessInFullExpressionOrdering config, FullExpr e, VariableEffect ve, VariableAccess va1,
-  VariableAccess va2, Variable v
+from 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
+  FullExprOrdering::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 $@.",
diff --git a/cpp/common/src/codingstandards/cpp/Ordering.qll b/cpp/common/src/codingstandards/cpp/Ordering.qll
diff --git a/cpp/common/src/codingstandards/cpp/orderofevaluation/VariableAccessOrdering.qll b/cpp/common/src/codingstandards/cpp/orderofevaluation/VariableAccessOrdering.qll
