C++: Fix FP on CWE-193 by blocking flow through back-edges of phi nodes.

cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll

@@ -49,6 +49,46 @@ module ProductFlow {
       this.isSinkPair(sink1, sink2)
     }
 
+    /**
+     * Holds if data flow through `node` is prohibited through the first projection of the product
+     * dataflow graph when the flow state is `state`.
+     */
+    predicate isBarrier1(DataFlow::Node node, DataFlow::FlowState state) {
+      isBarrier1(node) and state = ""
+    }
+
+    /**
+     * Holds if data flow through `node` is prohibited through the second projection of the product
+     * dataflow graph when the flow state is `state`.
+     */
+    predicate isBarrier2(DataFlow::Node node, DataFlow::FlowState state) {
+      isBarrier2(node) and state = ""
+    }
+
+    /**
+     * Holds if data flow through `node` is prohibited through the first projection of the product
+     * dataflow graph.
+     */
+    predicate isBarrier1(DataFlow::Node node) { none() }
+
+    /**
+     * Holds if data flow through `node` is prohibited through the second projection of the product
+     * dataflow graph.
+     */
+    predicate isBarrier2(DataFlow::Node node) { none() }
+
+    /**
+     * Holds if data flow out of `node` is prohibited in the first projection of the product
+     * dataflow graph.
+     */
+    predicate isBarrierOut1(DataFlow::Node node) { none() }
+
+    /**
+     * Holds if data flow out of `node` is prohibited in the second projection of the product
+     * dataflow graph.
+     */
+    predicate isBarrierOut2(DataFlow::Node node) { none() }
+
     predicate hasFlowPath(
       DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1,
       DataFlow2::PathNode sink2
@@ -70,6 +110,14 @@ module ProductFlow {
       override predicate isSink(DataFlow::Node sink, string state) {
         exists(Configuration conf | conf.isSinkPair(sink, state, _, _))
       }
+
+      override predicate isBarrier(DataFlow::Node node, string state) {
+        exists(Configuration conf | conf.isBarrier1(node, state))
+      }
+
+      override predicate isBarrierOut(DataFlow::Node node) {
+        exists(Configuration conf | conf.isBarrierOut1(node))
+      }
     }
 
     class Conf2 extends DataFlow2::Configuration {
@@ -87,6 +135,14 @@ module ProductFlow {
           conf.isSinkPair(sink1, _, sink, state) and any(Conf1 c).hasFlow(_, sink1)
         )
       }
+
+      override predicate isBarrier(DataFlow::Node node, string state) {
+        exists(Configuration conf | conf.isBarrier2(node, state))
+      }
+
+      override predicate isBarrierOut(DataFlow::Node node) {
+        exists(Configuration conf | conf.isBarrierOut2(node))
+      }
     }
   }
 

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll

@@ -416,6 +416,21 @@ class SsaPhiNode extends Node, TSsaPhiNode {
   final override Location getLocationImpl() { result = phi.getBasicBlock().getLocation() }
 
   override string toStringImpl() { result = "Phi" }
+
+  /**
+   * Gets a node that is used as input to this phi node.
+   * `fromBackEdge` is true if data flows along a back-edge,
+   * and `false` otherwise.
+   */
+  final Node getAnInput(boolean fromBackEdge) {
+    localFlowStep(result, this) and
+    if phi.getBasicBlock().dominates(getBasicBlock(result))
+    then fromBackEdge = true
+    else fromBackEdge = false
+  }
+
+  /** Gets a node that is used as input to this phi node. */
+  final Node getAnInput() { result = this.getAnInput(_) }
 }
 
 /**

cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll

@@ -301,7 +301,12 @@ private predicate defToNode(Node nodeFrom, Def def) {
   nodeHasInstruction(nodeFrom, def.getDefiningInstruction(), def.getIndirectionIndex())
 }
 
-private predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse) {
+/**
+ * INTERNAL: Do not use.
+ *
+ * Holds if `nodeFrom` is the node that correspond to the definition or use `defOrUse`.
+ */
+predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse) {
   // Node -> Def
   defToNode(nodeFrom, defOrUse)
   or

cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql

@@ -128,6 +128,10 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration {
       state2 = delta.toString()
     )
   }
+
+  override predicate isBarrierOut2(DataFlow::Node node) {
+    node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
+  }
 }
 
 pragma[nomagic]
@@ -154,11 +158,11 @@ predicate pointerAddInstructionHasOperands(
  */
 pragma[nomagic]
 predicate pointerAddInstructionHasBounds(
-  PointerAddInstruction pai, DataFlow::Node sink1, Instruction sink2, int delta
+  PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
 ) {
   exists(Instruction right |
     pointerAddInstructionHasOperands(pai, sink1.asInstruction(), right) and
-    bounded(right, sink2, delta)
+    bounded(right, sink2.asInstruction(), delta)
   )
 }
 
@@ -171,7 +175,7 @@ predicate pointerAddInstructionHasBounds(
 predicate isSinkImpl(
   PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
 ) {
-  pointerAddInstructionHasBounds(pai, sink1, sink2.asInstruction(), delta)
+  pointerAddInstructionHasBounds(pai, sink1, sink2, delta)
 }
 
 /**

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerDeref.expected

@@ -678,12 +678,6 @@ edges
 | test.cpp:213:6:213:6 | Load | test.cpp:213:5:213:13 | Store: ... = ... |
 | test.cpp:213:6:213:6 | Load | test.cpp:213:5:213:13 | Store: ... = ... |
 | test.cpp:221:17:221:22 | call to malloc | test.cpp:222:5:222:5 | Load |
-| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
-| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
-| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
-| test.cpp:222:5:222:5 | Load | test.cpp:222:5:222:12 | access to array |
-| test.cpp:222:5:222:12 | access to array | test.cpp:222:5:222:18 | Store: ... = ... |
-| test.cpp:222:5:222:12 | access to array | test.cpp:222:5:222:18 | Store: ... = ... |
 #select
 | test.cpp:6:14:6:15 | Load: * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:6:14:6:15 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
 | test.cpp:8:14:8:21 | Load: * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:8:14:8:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
@@ -702,4 +696,3 @@ edges
 | test.cpp:171:9:171:14 | Store: ... = ... | test.cpp:143:18:143:23 | call to malloc | test.cpp:171:9:171:14 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:143:18:143:23 | call to malloc | call to malloc | test.cpp:144:29:144:32 | size | size |
 | test.cpp:201:5:201:19 | Store: ... = ... | test.cpp:194:23:194:28 | call to malloc | test.cpp:201:5:201:19 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:194:23:194:28 | call to malloc | call to malloc | test.cpp:195:21:195:23 | len | len |
 | test.cpp:213:5:213:13 | Store: ... = ... | test.cpp:205:23:205:28 | call to malloc | test.cpp:213:5:213:13 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:205:23:205:28 | call to malloc | call to malloc | test.cpp:206:21:206:23 | len | len |
-| test.cpp:222:5:222:18 | Store: ... = ... | test.cpp:221:17:221:22 | call to malloc | test.cpp:222:5:222:18 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:221:17:221:22 | call to malloc | call to malloc | test.cpp:222:7:222:11 | ... - ... | ... - ... |

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp

@@ -219,6 +219,6 @@ void test14(unsigned long n, char *p) {
   while (unknown()) {
     n++;
     p = (char *)malloc(n);
-    p[n - 1] = 'a'; // GOOD [FALSE POSITIVE]
+    p[n - 1] = 'a'; // GOOD
   }
-}
+}