Update EXP43-C query and test

Replace local with global data-flow.
Modify the query implementation to detect violations of aliasing at block rather than statement scope as defined in the standard.

Author: Nikita Kraiouchkine

c/cert/src/rules/EXP43-C/RestrictPointerReferencesOverlappingObject.ql

@@ -39,8 +39,26 @@ Variable getAddressOfExprTargetBase(AddressOfExpr expr) {
   result = expr.getOperand().(VariableAccess).getTarget()
 }
 
+/**
+ * A data-flow configuration for tracking flow from an assignment or initialization to
+ * an assignment to an `AssignmentOrInitializationToRestrictPtrValueExpr`.
+ */
+class AssignedValueToRestrictPtrValueConfiguration extends DataFlow::Configuration {
+  AssignedValueToRestrictPtrValueConfiguration() {
+    this = "AssignmentOrInitializationToRestrictPtrValueConfiguration"
+  }
+
+  override predicate isSource(DataFlow::Node source) {
+    exists(Variable v | source.asExpr() = v.getAnAssignedValue())
+  }
+
+  override predicate isSink(DataFlow::Node sink) {
+    sink.asExpr() instanceof AssignmentOrInitializationToRestrictPtrValueExpr
+  }
+}
+
 from
-  AssignmentOrInitializationToRestrictPtrValueExpr source,
+  AssignedValueToRestrictPtrValueConfiguration config, DataFlow::Node sourceValue,
   AssignmentOrInitializationToRestrictPtrValueExpr expr,
   AssignmentOrInitializationToRestrictPtrValueExpr pre_expr
 where
@@ -49,23 +67,14 @@ where
     // If the same expressions flows to two unique `AssignmentOrInitializationToRestrictPtrValueExpr`
     // in the same block, then the two variables point to the same (overlapping) object
     expr.getEnclosingBlock() = pre_expr.getEnclosingBlock() and
-    strictlyDominates(pre_expr, expr) and
     (
-      dominates(source, pre_expr) and
-      DataFlow::localExprFlow(source, expr) and
-      DataFlow::localExprFlow(source, pre_expr)
+      config.hasFlow(sourceValue, DataFlow::exprNode(pre_expr)) and
+      config.hasFlow(sourceValue, DataFlow::exprNode(expr))
       or
       // Expressions referring to the address of the same variable can also result in aliasing
-      getAddressOfExprTargetBase(expr) = getAddressOfExprTargetBase(pre_expr) and
-      source =
-        any(AddressOfExpr ao | getAddressOfExprTargetBase(ao) = getAddressOfExprTargetBase(expr))
+      getAddressOfExprTargetBase(expr) = getAddressOfExprTargetBase(pre_expr)
     ) and
-    // But only if there is no intermediate assignment that could change the value of one of the variables
-    not exists(AssignmentOrInitializationToRestrictPtrValueExpr mid |
-      strictlyDominates(mid, expr) and
-      strictlyDominates(pre_expr, mid) and
-      not DataFlow::localExprFlow(source, mid)
-    )
+    strictlyDominates(pragma[only_bind_out](pre_expr), pragma[only_bind_out](expr))
     or
     // Two restrict-qualified pointers in the same scope assigned to each other
     expr.(VariableAccess).getTarget().getType().hasSpecifier("restrict") and

c/cert/test/rules/EXP43-C/RestrictPointerReferencesOverlappingObject.expected

@@ -1,6 +1,8 @@
 | test.c:18:22:18:23 | i2 | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:18:17:18:18 | i3 | i3 |
 | test.c:19:8:19:9 | g2 | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:5:15:5:16 | g1 | g1 |
 | test.c:20:8:20:9 | i2 | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:16:17:16:18 | i1 | i1 |
+| test.c:27:10:27:11 | g1 | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:23:19:23:20 | i5 | i5 |
 | test.c:28:10:28:11 | g1 | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:22:19:22:20 | i4 | i4 |
 | test.c:39:22:39:26 | & ... | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:39:17:39:18 | px | px |
+| test.c:45:10:45:14 | & ... | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:42:19:42:20 | pz | pz |
 | test.c:46:10:46:14 | & ... | Assignment to restrict-qualified pointer $@ results in pointer aliasing. | test.c:41:19:41:20 | py | py |

c/cert/test/rules/EXP43-C/test.c

@@ -24,7 +24,7 @@ void test_global_local() {
     int *restrict i6;
     i4 = g1;        // COMPLIANT
     i4 = (void *)0; // COMPLIANT
-    i5 = g1;        // COMPLIANT
+    i5 = g1;        // NON_COMPLIANT - block rather than statement scope matters
     i4 = g1;        // NON_COMPLIANT
     i6 = g2;        // COMPLIANT
   }
@@ -42,7 +42,7 @@ void test_structs() {
     int *restrict pz;
     py = &v1.y; // COMPLIANT
     py = (int *)0;
-    pz = &v1.z; // COMPLIANT
+    pz = &v1.z; // NON_COMPLIANT - block rather than statement scope matters
     py = &v1.y; // NON_COMPLIANT
   }
 }