C++: Remove the ad-hoc code for keeping track of increments/decrements on pointers in the 'cpp/overrun-write' query.

Author: MathiasVP

cpp/ql/src/Security/CWE/CWE-119/OverrunWriteProductFlow.ql

@@ -88,81 +88,14 @@ module ValidState {
 
     predicate isSink(DataFlow::Node sink) { isSinkPairImpl(_, _, sink, _, _) }
 
-    predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
-      isAdditionalFlowStep2(node1, node2, _)
-    }
-
-    predicate includeHiddenNodes() { any() }
+    predicate isBarrierOut(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
   }
 
   private import DataFlow::Global<ValidStateConfig>
 
-  private predicate inLoop(PathNode n) { n.getASuccessor+() = n }
-
-  /**
-   * Holds if `value` is a possible offset for `n`.
-   *
-   * To ensure termination, we limit `value` to be in the
-   * range `[-2, 2]` if the node is part of a loop. Without
-   * this restriction we wouldn't terminate on an example like:
-   * ```cpp
-   * while(unknown()) { size++; }
-   * ```
-   */
-  private predicate validStateImpl(PathNode n, int value) {
-    // If the dataflow node depends recursively on itself we restrict the range.
-    (inLoop(n) implies value = [-2 .. 2]) and
-    (
-      // For the dataflow source we have an allocation such as `malloc(size + k)`,
-      // and the value of the flow-state is then `k`.
-      hasSize(_, n.getNode(), value)
-      or
-      // For a dataflow sink any `value` that is strictly smaller than the delta
-      // needs to be a valid flow-state. That is, for a snippet like:
-      // ```
-      // p = b ? new char[size] : new char[size + 1];
-      // memset(p, 0, size + 2);
-      // ```
-      // the valid flow-states at the `memset` must include the set `{0, 1}` since the
-      // flow-state at `new char[size]` is `0`, and the flow-state at `new char[size + 1]`
-      // is `1`.
-      //
-      // So we find a valid flow-state at the sink's predecessor, and use the definition
-      // of our sink predicate to compute the valid flow-states at the sink.
-      exists(int delta, PathNode n0 |
-        n0.getASuccessor() = n and
-        validStateImpl(n0, value) and
-        isSinkPairImpl(_, _, n.getNode(), delta, _) and
-        delta > value
-      )
-      or
-      // For a non-source and non-sink node there is two cases to consider.
-      // 1. A node where we have to update the flow-state, or
-      // 2. A node that doesn't update the flow-state.
-      //
-      // For case 1, we compute the new flow-state by adding the constant operand of the
-      // `AddInstruction` to the flow-state of any predecessor node.
-      // For case 2 we simply propagate the valid flow-states from the predecessor node to
-      // the next one.
-      exists(PathNode n0, DataFlow::Node node0, DataFlow::Node node, int value0 |
-        n0.getASuccessor() = n and
-        validStateImpl(n0, value0) and
-        node = n.getNode() and
-        node0 = n0.getNode()
-      |
-        exists(int delta |
-          isAdditionalFlowStep2(node0, node, delta) and
-          value0 = value + delta
-        )
-        or
-        not isAdditionalFlowStep2(node0, node, _) and
-        value = value0
-      )
-    )
-  }
-
-  predicate validState(DataFlow::Node n, int value) {
-    validStateImpl(any(PathNode pn | pn.getNode() = n), value)
+  predicate validState(DataFlow::Node source, DataFlow::Node sink, int value) {
+    hasSize(_, source, value) and
+    flow(source, sink)
   }
 }
 
@@ -213,16 +146,6 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
   }
 
   predicate isBarrierOut2(DataFlow::Node node) { DataFlow::flowsToBackEdge(node) }
-
-  predicate isAdditionalFlowStep2(
-    DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
-  ) {
-    validState(node2, state2) and
-    exists(int delta |
-      isAdditionalFlowStep2(node1, node2, delta) and
-      state1 = state2 + delta
-    )
-  }
 }
 
 module StringSizeFlow = ProductFlow::GlobalWithState<StringSizeConfig>;

cpp/ql/test/query-tests/Security/CWE/CWE-119/SAMATE/OverrunWriteProductFlow.expected

@@ -12,19 +12,6 @@ edges
 | test.cpp:42:13:42:15 | *str [string] | test.cpp:42:18:42:23 | string | provenance |  |
 | test.cpp:72:17:72:19 | *str [string] | test.cpp:72:22:72:27 | string | provenance |  |
 | test.cpp:80:17:80:19 | *str [string] | test.cpp:80:22:80:27 | string | provenance |  |
-| test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | provenance |  |
-| test.cpp:90:5:90:7 | *str [post update] [string] | test.cpp:91:5:91:7 | *str [string] | provenance |  |
-| test.cpp:90:5:90:34 | ... = ... | test.cpp:90:5:90:7 | *str [post update] [string] | provenance |  |
-| test.cpp:90:19:90:24 | call to malloc | test.cpp:90:5:90:34 | ... = ... | provenance |  |
-| test.cpp:91:5:91:7 | *str [string] | test.cpp:92:12:92:14 | *str [string] | provenance |  |
-| test.cpp:92:12:92:14 | *str [string] | test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:99:13:99:15 | *str [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:129:17:129:19 | *str [string] | provenance |  |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | test.cpp:137:17:137:19 | *str [string] | provenance |  |
-| test.cpp:99:13:99:15 | *str [string] | test.cpp:99:18:99:23 | string | provenance |  |
-| test.cpp:129:17:129:19 | *str [string] | test.cpp:129:22:129:27 | string | provenance |  |
-| test.cpp:137:17:137:19 | *str [string] | test.cpp:137:22:137:27 | string | provenance |  |
 | test.cpp:147:5:147:7 | *str [post update] [string] | test.cpp:148:5:148:7 | *str [string] | provenance |  |
 | test.cpp:147:5:147:34 | ... = ... | test.cpp:147:5:147:7 | *str [post update] [string] | provenance |  |
 | test.cpp:147:19:147:24 | call to malloc | test.cpp:147:5:147:34 | ... = ... | provenance |  |
@@ -46,12 +33,6 @@ edges
 | test.cpp:199:17:199:19 | *str [string] | test.cpp:199:22:199:27 | string | provenance |  |
 | test.cpp:203:17:203:19 | *str [string] | test.cpp:203:22:203:27 | string | provenance |  |
 | test.cpp:207:17:207:19 | *str [string] | test.cpp:207:22:207:27 | string | provenance |  |
-| test.cpp:214:24:214:24 | p | test.cpp:216:10:216:10 | p | provenance |  |
-| test.cpp:220:27:220:54 | call to malloc | test.cpp:220:27:220:54 | call to malloc | provenance |  |
-| test.cpp:220:27:220:54 | call to malloc | test.cpp:222:15:222:20 | buffer | provenance |  |
-| test.cpp:222:15:222:20 | buffer | test.cpp:214:24:214:24 | p | provenance |  |
-| test.cpp:228:27:228:54 | call to malloc | test.cpp:228:27:228:54 | call to malloc | provenance |  |
-| test.cpp:228:27:228:54 | call to malloc | test.cpp:232:10:232:15 | buffer | provenance |  |
 | test.cpp:235:40:235:45 | buffer | test.cpp:236:5:236:26 | ... = ... | provenance |  |
 | test.cpp:236:5:236:9 | *p_str [post update] [string] | test.cpp:235:27:235:31 | *p_str [Return] [string] | provenance |  |
 | test.cpp:236:5:236:9 | *p_str [post update] [string] | test.cpp:235:27:235:31 | *p_str [string] | provenance |  |
@@ -64,8 +45,6 @@ edges
 | test.cpp:243:12:243:14 | *str [string] | test.cpp:243:12:243:21 | string | provenance |  |
 | test.cpp:249:14:249:33 | call to my_alloc | test.cpp:249:14:249:33 | call to my_alloc | provenance |  |
 | test.cpp:249:14:249:33 | call to my_alloc | test.cpp:250:12:250:12 | p | provenance |  |
-| test.cpp:256:5:256:25 | ... = ... | test.cpp:257:12:257:12 | p | provenance |  |
-| test.cpp:256:9:256:25 | call to malloc | test.cpp:256:5:256:25 | ... = ... | provenance |  |
 | test.cpp:262:15:262:30 | call to malloc | test.cpp:262:15:262:30 | call to malloc | provenance |  |
 | test.cpp:262:15:262:30 | call to malloc | test.cpp:266:12:266:12 | p | provenance |  |
 | test.cpp:264:9:264:30 | ... = ... | test.cpp:266:12:266:12 | p | provenance |  |
@@ -87,20 +66,6 @@ nodes
 | test.cpp:72:22:72:27 | string | semmle.label | string |
 | test.cpp:80:17:80:19 | *str [string] | semmle.label | *str [string] |
 | test.cpp:80:22:80:27 | string | semmle.label | string |
-| test.cpp:88:11:88:30 | **mk_string_t_plus_one [string] | semmle.label | **mk_string_t_plus_one [string] |
-| test.cpp:90:5:90:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
-| test.cpp:90:5:90:34 | ... = ... | semmle.label | ... = ... |
-| test.cpp:90:19:90:24 | call to malloc | semmle.label | call to malloc |
-| test.cpp:91:5:91:7 | *str [string] | semmle.label | *str [string] |
-| test.cpp:92:12:92:14 | *str [string] | semmle.label | *str [string] |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | semmle.label | *call to mk_string_t_plus_one [string] |
-| test.cpp:96:21:96:40 | *call to mk_string_t_plus_one [string] | semmle.label | *call to mk_string_t_plus_one [string] |
-| test.cpp:99:13:99:15 | *str [string] | semmle.label | *str [string] |
-| test.cpp:99:18:99:23 | string | semmle.label | string |
-| test.cpp:129:17:129:19 | *str [string] | semmle.label | *str [string] |
-| test.cpp:129:22:129:27 | string | semmle.label | string |
-| test.cpp:137:17:137:19 | *str [string] | semmle.label | *str [string] |
-| test.cpp:137:22:137:27 | string | semmle.label | string |
 | test.cpp:147:5:147:7 | *str [post update] [string] | semmle.label | *str [post update] [string] |
 | test.cpp:147:5:147:34 | ... = ... | semmle.label | ... = ... |
 | test.cpp:147:19:147:24 | call to malloc | semmle.label | call to malloc |
@@ -123,14 +88,6 @@ nodes
 | test.cpp:203:22:203:27 | string | semmle.label | string |
 | test.cpp:207:17:207:19 | *str [string] | semmle.label | *str [string] |
 | test.cpp:207:22:207:27 | string | semmle.label | string |
-| test.cpp:214:24:214:24 | p | semmle.label | p |
-| test.cpp:216:10:216:10 | p | semmle.label | p |
-| test.cpp:220:27:220:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:220:27:220:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:222:15:222:20 | buffer | semmle.label | buffer |
-| test.cpp:228:27:228:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:228:27:228:54 | call to malloc | semmle.label | call to malloc |
-| test.cpp:232:10:232:15 | buffer | semmle.label | buffer |
 | test.cpp:235:27:235:31 | *p_str [Return] [string] | semmle.label | *p_str [Return] [string] |
 | test.cpp:235:27:235:31 | *p_str [string] | semmle.label | *p_str [string] |
 | test.cpp:235:40:235:45 | buffer | semmle.label | buffer |
@@ -145,9 +102,6 @@ nodes
 | test.cpp:249:14:249:33 | call to my_alloc | semmle.label | call to my_alloc |
 | test.cpp:249:14:249:33 | call to my_alloc | semmle.label | call to my_alloc |
 | test.cpp:250:12:250:12 | p | semmle.label | p |
-| test.cpp:256:5:256:25 | ... = ... | semmle.label | ... = ... |
-| test.cpp:256:9:256:25 | call to malloc | semmle.label | call to malloc |
-| test.cpp:257:12:257:12 | p | semmle.label | p |
 | test.cpp:262:15:262:30 | call to malloc | semmle.label | call to malloc |
 | test.cpp:262:15:262:30 | call to malloc | semmle.label | call to malloc |
 | test.cpp:264:9:264:30 | ... = ... | semmle.label | ... = ... |
@@ -163,9 +117,6 @@ subpaths
 | test.cpp:42:5:42:11 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:42:18:42:23 | string | This write may overflow $@ by 1 element. | test.cpp:42:18:42:23 | string | string |
 | test.cpp:72:9:72:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:72:22:72:27 | string | This write may overflow $@ by 1 element. | test.cpp:72:22:72:27 | string | string |
 | test.cpp:80:9:80:15 | call to strncpy | test.cpp:18:19:18:24 | call to malloc | test.cpp:80:22:80:27 | string | This write may overflow $@ by 2 elements. | test.cpp:80:22:80:27 | string | string |
-| test.cpp:99:5:99:11 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:99:18:99:23 | string | This write may overflow $@ by 1 element. | test.cpp:99:18:99:23 | string | string |
-| test.cpp:129:9:129:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:129:22:129:27 | string | This write may overflow $@ by 1 element. | test.cpp:129:22:129:27 | string | string |
-| test.cpp:137:9:137:15 | call to strncpy | test.cpp:90:19:90:24 | call to malloc | test.cpp:137:22:137:27 | string | This write may overflow $@ by 2 elements. | test.cpp:137:22:137:27 | string | string |
 | test.cpp:152:5:152:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:152:18:152:23 | string | This write may overflow $@ by 1 element. | test.cpp:152:18:152:23 | string | string |
 | test.cpp:154:5:154:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:154:18:154:23 | string | This write may overflow $@ by 1 element. | test.cpp:154:18:154:23 | string | string |
 | test.cpp:156:5:156:11 | call to strncpy | test.cpp:147:19:147:24 | call to malloc | test.cpp:156:18:156:23 | string | This write may overflow $@ by 2 elements. | test.cpp:156:18:156:23 | string | string |