C++: Let data flow past definition by reference

This commit changes how data flow works in the following code.

    MyType x = source();
    defineByReference(&x);
    sink(x);

The question here is whether there should be flow from `source` to
`sink`. Such flow is desirable if `defineByReference` doesn't write to
all of `x`, but it's undesirable if `defineByReference` is a typical
init function in `C` that writes to every field or if
`defineByReference` is `memcpy` or `memset` on the full range.

Before 1.20.0, there would be flow from `source` to `sink` in case `x`
happened to be modeled with `BlockVar` but not in case `x` happened to
be modelled with SSA. The choice of modelling depends on an analysis of
how `x` is used elsewhere in the function, and it's supposed to be an
internal implementation detail that there are two ways to model
variables. In 1.20.0, I changed the `BlockVar` behavior so it worked the
same as SSA, never allowing that flow. It turns out that this change
broke a customer's query.

This commit reverts `BlockVar` to its old behavior of letting flow
propagate past the `defineByReference` call and then regains consistency
by changing all variables that are ever defined by reference to be
modelled with `BlockVar` instead of SSA. This means we now get too much
flow in certain cases, but that appears to be better overall than
getting too little flow. See also the discussion in CPP-336.

Author: jbj

cpp/ql/src/semmle/code/cpp/dataflow/internal/FlowVar.qll

@@ -93,9 +93,17 @@ module FlowVar_internal {
    * - Supporting fields, globals and statics like the Java SSA library does.
    * - Supporting all local variables, even if their address is taken by
    *   address-of, reference assignments, or lambdas.
+   * - Understanding that assignment to a field of a local struct is a
+   *   definition of the struct but not a complete overwrite. This is what the
+   *   IR library uses chi nodes for.
    */
   predicate fullySupportedSsaVariable(Variable v) {
     v = any(SsaDefinition def).getAVariable() and
+    // After `foo(&x.field)` we need for there to be two definitions of `x`:
+    // the one that existed before the call to `foo` and the def-by-ref from
+    // the call. It's fundamental in SSA that each use is only associated with
+    // one def, so we can't easily get this effect with SSA.
+    not definitionByReference(v.getAnAccess(), _) and
     // SSA variables do not exist before their first assignment, but one
     // feature of this data flow library is to track where uninitialized data
     // ends up.
@@ -183,8 +191,7 @@ module FlowVar_internal {
     }
 
     override predicate definedByReference(Expr arg) {
-      definitionByReference(v.getAnAccess(), arg) and
-      arg = def.getDefinition()
+      none() // Not supported for SSA. See `fullySupportedSsaVariable`.
     }
 
     override predicate definedByInitialValue(LocalScopeVariable param) {
@@ -204,8 +211,6 @@ module FlowVar_internal {
       this.definedByExpr(_, _)
       or
       this.definedByInitialValue(_)
-      or
-      this.definedByReference(_)
     }
 
     /**
@@ -236,10 +241,7 @@ module FlowVar_internal {
     BlockVar() { this = TBlockVar(sbb, v) }
 
     override VariableAccess getAnAccess() {
-      exists(SubBasicBlock reached |
-        reached = getAReachedBlockVarSBB(this) and
-        variableAccessInSBB(v, reached, result)
-      )
+      variableAccessInSBB(v, getAReachedBlockVarSBB(this), result)
     }
 
     override predicate definedByInitialValue(LocalScopeVariable lsv) {
@@ -401,8 +403,7 @@ module FlowVar_internal {
       mid = getAReachedBlockVarSBB(start) and
       result = mid.getASuccessor() and
       not skipLoop(mid, result, sbbDef, v) and
-      not assignmentLikeOperation(result, v, _) and
-      not blockVarDefinedByReference(result, v, _)
+      not assignmentLikeOperation(result, v, _)
     )
   }
 
@@ -413,12 +414,6 @@ module FlowVar_internal {
     va.getTarget() = v and
     va = sbb.getANode() and
     not overwrite(va, _)
-    or
-    // Allow flow into a `VariableAccess` that is used as definition by
-    // reference. This flow is blocked by `getAReachedBlockVarSBB` because
-    // flow should not propagate past that.
-    va = sbb.getASuccessor().(VariableAccess) and
-    blockVarDefinedByReference(va, v, _)
   }
 
   /**
@@ -516,9 +511,6 @@ module FlowVar_internal {
    */
   predicate overwrite(VariableAccess va, ControlFlowNode node) {
     va = node.(AssignExpr).getLValue()
-    or
-    va = node and
-    definitionByReference(node, _)
   }
 
   /**

cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow.expected

@@ -1,11 +1,16 @@
 | example.c:15:37:15:37 | b | example.c:19:6:19:6 | b |
 | example.c:15:44:15:46 | pos | example.c:24:24:24:26 | pos |
 | example.c:15:44:15:46 | pos | example.c:28:23:28:25 | pos |
+| example.c:17:19:17:22 | {...} | example.c:24:2:24:7 | coords |
 | example.c:17:19:17:22 | {...} | example.c:24:13:24:18 | coords |
+| example.c:17:19:17:22 | {...} | example.c:26:2:26:7 | coords |
+| example.c:17:19:17:22 | {...} | example.c:26:19:26:24 | coords |
 | example.c:24:13:24:30 | ... = ... | example.c:24:2:24:30 | ... = ... |
 | example.c:24:24:24:30 | ... + ... | example.c:24:13:24:30 | ... = ... |
 | example.c:26:13:26:16 | call to getX | example.c:26:2:26:25 | ... = ... |
 | example.c:26:18:26:24 | ref arg & ... | example.c:26:2:26:7 | coords |
+| example.c:26:18:26:24 | ref arg & ... | example.c:26:19:26:24 | coords |
+| example.c:28:22:28:25 | ref arg & ... | example.c:28:23:28:25 | pos |
 | test.cpp:6:12:6:17 | call to source | test.cpp:7:8:7:9 | t1 |
 | test.cpp:6:12:6:17 | call to source | test.cpp:8:8:8:9 | t1 |
 | test.cpp:6:12:6:17 | call to source | test.cpp:9:8:9:9 | t1 |
@@ -31,14 +36,22 @@
 | test.cpp:24:10:24:11 | t2 | test.cpp:26:8:26:9 | t1 |
 | test.cpp:430:48:430:54 | source1 | test.cpp:432:17:432:23 | source1 |
 | test.cpp:431:12:431:13 | 0 | test.cpp:432:11:432:13 | tmp |
+| test.cpp:431:12:431:13 | 0 | test.cpp:432:33:432:35 | tmp |
+| test.cpp:431:12:431:13 | 0 | test.cpp:433:8:433:10 | tmp |
 | test.cpp:432:10:432:13 | & ... | test.cpp:432:3:432:8 | call to memcpy |
+| test.cpp:432:10:432:13 | ref arg & ... | test.cpp:432:11:432:13 | tmp |
+| test.cpp:432:10:432:13 | ref arg & ... | test.cpp:432:33:432:35 | tmp |
 | test.cpp:432:10:432:13 | ref arg & ... | test.cpp:433:8:433:10 | tmp |
 | test.cpp:432:17:432:23 | source1 | test.cpp:432:10:432:13 | ref arg & ... |
 | test.cpp:436:53:436:59 | source1 | test.cpp:439:17:439:23 | source1 |
 | test.cpp:436:66:436:66 | b | test.cpp:441:7:441:7 | b |
 | test.cpp:437:12:437:13 | 0 | test.cpp:438:19:438:21 | tmp |
 | test.cpp:437:12:437:13 | 0 | test.cpp:439:11:439:13 | tmp |
+| test.cpp:437:12:437:13 | 0 | test.cpp:439:33:439:35 | tmp |
+| test.cpp:437:12:437:13 | 0 | test.cpp:440:8:440:10 | tmp |
+| test.cpp:437:12:437:13 | 0 | test.cpp:442:10:442:12 | tmp |
 | test.cpp:439:10:439:13 | & ... | test.cpp:439:3:439:8 | call to memcpy |
+| test.cpp:439:10:439:13 | ref arg & ... | test.cpp:439:11:439:13 | tmp |
 | test.cpp:439:10:439:13 | ref arg & ... | test.cpp:439:33:439:35 | tmp |
 | test.cpp:439:10:439:13 | ref arg & ... | test.cpp:440:8:440:10 | tmp |
 | test.cpp:439:10:439:13 | ref arg & ... | test.cpp:442:10:442:12 | tmp |

cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp

@@ -443,17 +443,17 @@ void flowThroughMemcpy_blockvar_with_local_flow(int source1, int b) {
   }
 }
 
-void cleanedByMemcpy_ssa(int clean1) {
+void cleanedByMemcpy_ssa(int clean1) { // currently modeled with BlockVar, not SSA
   int tmp;
   memcpy(&tmp, &clean1, sizeof tmp);
-  sink(tmp); // clean
+  sink(tmp); // clean [FALSE POSITIVE]
 }
 
 void cleanedByMemcpy_blockvar(int clean1) {
   int tmp;
   int *capture = &tmp;
   memcpy(&tmp, &clean1, sizeof tmp);
-  sink(tmp); // clean
+  sink(tmp); // clean [FALSE POSITIVE]
 }
 
 void intRefSource(int &ref_source);

cpp/ql/test/library-tests/dataflow/dataflow-tests/test.expected

@@ -30,10 +30,17 @@
 | test.cpp:433:8:433:10 | tmp | test.cpp:430:48:430:54 | source1 |
 | test.cpp:440:8:440:10 | tmp | test.cpp:436:53:436:59 | source1 |
 | test.cpp:442:10:442:12 | tmp | test.cpp:436:53:436:59 | source1 |
+| test.cpp:449:8:449:10 | tmp | test.cpp:447:7:447:9 | tmp |
+| test.cpp:456:8:456:10 | tmp | test.cpp:453:7:453:9 | tmp |
+| test.cpp:466:8:466:12 | local | test.cpp:464:7:464:11 | local |
 | test.cpp:466:8:466:12 | local | test.cpp:465:16:465:20 | ref arg local |
+| test.cpp:472:8:472:12 | local | test.cpp:470:7:470:11 | local |
 | test.cpp:472:8:472:12 | local | test.cpp:471:20:471:25 | ref arg & ... |
+| test.cpp:478:8:478:12 | local | test.cpp:476:7:476:11 | local |
 | test.cpp:478:8:478:12 | local | test.cpp:477:20:477:24 | ref arg local |
+| test.cpp:485:8:485:12 | local | test.cpp:483:7:483:11 | local |
 | test.cpp:485:8:485:12 | local | test.cpp:484:18:484:23 | ref arg & ... |
+| test.cpp:491:8:491:12 | local | test.cpp:489:7:489:11 | local |
 | test.cpp:491:8:491:12 | local | test.cpp:490:18:490:22 | ref arg local |
 | true_upon_entry.cpp:21:8:21:8 | x | true_upon_entry.cpp:17:11:17:16 | call to source |
 | true_upon_entry.cpp:29:8:29:8 | x | true_upon_entry.cpp:27:9:27:14 | call to source |

cpp/ql/test/library-tests/dataflow/dataflow-tests/test_diff.expected

@@ -11,10 +11,17 @@
 | test.cpp:430:48:430:54 | test.cpp:433:8:433:10 | AST only |
 | test.cpp:436:53:436:59 | test.cpp:440:8:440:10 | AST only |
 | test.cpp:436:53:436:59 | test.cpp:442:10:442:12 | AST only |
+| test.cpp:447:7:447:9 | test.cpp:449:8:449:10 | AST only |
+| test.cpp:453:7:453:9 | test.cpp:456:8:456:10 | AST only |
+| test.cpp:464:7:464:11 | test.cpp:466:8:466:12 | AST only |
 | test.cpp:465:16:465:20 | test.cpp:466:8:466:12 | AST only |
+| test.cpp:470:7:470:11 | test.cpp:472:8:472:12 | AST only |
 | test.cpp:471:20:471:25 | test.cpp:472:8:472:12 | AST only |
+| test.cpp:476:7:476:11 | test.cpp:478:8:478:12 | AST only |
 | test.cpp:477:20:477:24 | test.cpp:478:8:478:12 | AST only |
+| test.cpp:483:7:483:11 | test.cpp:485:8:485:12 | AST only |
 | test.cpp:484:18:484:23 | test.cpp:485:8:485:12 | AST only |
+| test.cpp:489:7:489:11 | test.cpp:491:8:491:12 | AST only |
 | test.cpp:490:18:490:22 | test.cpp:491:8:491:12 | AST only |
 | true_upon_entry.cpp:9:11:9:16 | true_upon_entry.cpp:13:8:13:8 | IR only |
 | true_upon_entry.cpp:62:11:62:16 | true_upon_entry.cpp:66:8:66:8 | IR only |

cpp/ql/test/library-tests/dataflow/dataflow-tests/uninitialized.expected

@@ -1,4 +1,20 @@
 | test.cpp:75:7:75:8 | u1 | test.cpp:76:8:76:9 | u1 |
 | test.cpp:83:7:83:8 | u2 | test.cpp:84:13:84:14 | u2 |
 | test.cpp:83:7:83:8 | u2 | test.cpp:85:8:85:9 | u2 |
+| test.cpp:447:7:447:9 | tmp | test.cpp:448:11:448:13 | tmp |
+| test.cpp:447:7:447:9 | tmp | test.cpp:449:8:449:10 | tmp |
 | test.cpp:453:7:453:9 | tmp | test.cpp:454:19:454:21 | tmp |
+| test.cpp:453:7:453:9 | tmp | test.cpp:455:11:455:13 | tmp |
+| test.cpp:453:7:453:9 | tmp | test.cpp:456:8:456:10 | tmp |
+| test.cpp:464:7:464:11 | local | test.cpp:465:16:465:20 | local |
+| test.cpp:464:7:464:11 | local | test.cpp:466:8:466:12 | local |
+| test.cpp:470:7:470:11 | local | test.cpp:471:21:471:25 | local |
+| test.cpp:470:7:470:11 | local | test.cpp:472:8:472:12 | local |
+| test.cpp:476:7:476:11 | local | test.cpp:477:20:477:24 | local |
+| test.cpp:476:7:476:11 | local | test.cpp:478:8:478:12 | local |
+| test.cpp:476:7:476:11 | local | test.cpp:479:9:479:13 | local |
+| test.cpp:483:7:483:11 | local | test.cpp:484:19:484:23 | local |
+| test.cpp:483:7:483:11 | local | test.cpp:485:8:485:12 | local |
+| test.cpp:489:7:489:11 | local | test.cpp:490:18:490:22 | local |
+| test.cpp:489:7:489:11 | local | test.cpp:491:8:491:12 | local |
+| test.cpp:489:7:489:11 | local | test.cpp:492:9:492:13 | local |

cpp/ql/test/library-tests/dataflow/taint-tests/localTaint.expected

@@ -128,13 +128,24 @@
 | taint.cpp:164:19:164:24 | call to source | taint.cpp:168:8:168:14 | tainted |  |
 | taint.cpp:164:19:164:24 | call to source | taint.cpp:172:18:172:24 | tainted |  |
 | taint.cpp:165:22:165:25 | {...} | taint.cpp:170:10:170:15 | buffer |  |
+| taint.cpp:165:22:165:25 | {...} | taint.cpp:171:8:171:13 | buffer |  |
+| taint.cpp:165:22:165:25 | {...} | taint.cpp:172:10:172:15 | buffer |  |
+| taint.cpp:165:22:165:25 | {...} | taint.cpp:173:8:173:13 | buffer |  |
 | taint.cpp:165:24:165:24 | 0 | taint.cpp:165:22:165:25 | {...} | TAINT |
 | taint.cpp:170:10:170:15 | buffer | taint.cpp:170:3:170:8 | call to strcpy |  |
+| taint.cpp:170:10:170:15 | ref arg buffer | taint.cpp:170:10:170:15 | buffer |  |
 | taint.cpp:170:10:170:15 | ref arg buffer | taint.cpp:171:8:171:13 | buffer |  |
+| taint.cpp:170:10:170:15 | ref arg buffer | taint.cpp:172:10:172:15 | buffer |  |
+| taint.cpp:170:10:170:15 | ref arg buffer | taint.cpp:173:8:173:13 | buffer |  |
+| taint.cpp:171:8:171:13 | ref arg buffer | taint.cpp:171:8:171:13 | buffer |  |
 | taint.cpp:171:8:171:13 | ref arg buffer | taint.cpp:172:10:172:15 | buffer |  |
+| taint.cpp:171:8:171:13 | ref arg buffer | taint.cpp:173:8:173:13 | buffer |  |
 | taint.cpp:172:10:172:15 | buffer | taint.cpp:172:3:172:8 | call to strcat |  |
+| taint.cpp:172:10:172:15 | ref arg buffer | taint.cpp:172:10:172:15 | buffer |  |
 | taint.cpp:172:10:172:15 | ref arg buffer | taint.cpp:173:8:173:13 | buffer |  |
+| taint.cpp:173:8:173:13 | ref arg buffer | taint.cpp:173:8:173:13 | buffer |  |
 | taint.cpp:180:19:180:19 | p | taint.cpp:181:9:181:9 | p |  |
 | taint.cpp:181:9:181:9 | p | taint.cpp:181:8:181:9 | * ... | TAINT |
 | taint.cpp:185:11:185:16 | call to source | taint.cpp:186:11:186:11 | x |  |
+| taint.cpp:186:10:186:11 | ref arg & ... | taint.cpp:186:11:186:11 | x |  |
 | taint.cpp:186:11:186:11 | x | taint.cpp:186:10:186:11 | & ... | TAINT |