SSA: Tolerate multiple variables being read at the same CFG node

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll

@@ -1243,14 +1243,6 @@ private module IntWithParam<ParamSig P> {
 }
 
 module BarrierGuardWithIntParam<ParamSig P, IntWithParam<P>::guardChecksNodeSig/5 guardChecksNode> {
-  private predicate ssaDefReachesCertainUse(Definition def, UseImpl use) {
-    exists(SourceVariable v, IRBlock bb, int i |
-      use.hasIndexInBlock(bb, i, v) and
-      variableRead(bb, i, v, true) and
-      ssaDefReachesRead(v, def, bb, i)
-    )
-  }
-
   private predicate guardChecksInstr(
     IRGuards::Guards_v1::Guard g, IRGuards::GuardsInput::Expr instr, IRGuards::GuardValue gv,
     ParamIntPair<P>::TPair pair
@@ -1279,24 +1271,9 @@ module BarrierGuardWithIntParam<ParamSig P, IntWithParam<P>::guardChecksNodeSig/
   }
 
   Node getABarrierNode(int indirectionIndex, P p) {
-    // Only get the SynthNodes from the shared implementation, as the ExprNodes cannot
-    // be matched on SourceVariable.
-    result.(SsaSynthNode).getSynthNode() =
+    fromDfNode(result) =
       DataFlowIntegrationImpl::BarrierGuardDefWithState<ParamIntPair<P>::MkPair, guardChecksWithWrappers/4>::getABarrierNode(ParamIntPair<P>::MkPair(p,
           indirectionIndex))
-    or
-    // Calculate the guarded UseImpls corresponding to ExprNodes directly.
-    exists(
-      DataFlowIntegrationInput::Guard g, IRGuards::GuardValue branch, Definition def, IRBlock bb
-    |
-      exists(UseImpl use |
-        guardChecksWithWrappers(g, def, branch, ParamIntPair<P>::MkPair(p, indirectionIndex)) and
-        ssaDefReachesCertainUse(def, use) and
-        use.getBlock() = bb and
-        DataFlowIntegrationInput::guardControlsBlock(g, bb, branch) and
-        result = use.getNode()
-      )
-    )
   }
 }
 
@@ -1313,13 +1290,12 @@ module BarrierGuard<ParamSig P, WithParam<P>::guardChecksNodeSig/4 guardChecksNo
   }
 }
 
-bindingset[result, v]
-pragma[inline_late]
-private DataFlowIntegrationImpl::Node fromDfNode(Node n, SourceVariable v) {
+pragma[nomagic]
+private DataFlowIntegrationImpl::Node fromDfNode(Node n) {
   result = n.(SsaSynthNode).getSynthNode()
   or
-  exists(UseImpl use, IRBlock bb, int i |
-    result.(DataFlowIntegrationImpl::ExprNode).getExpr().hasCfgNode(bb, i) and
+  exists(UseImpl use, IRBlock bb, int i, SourceVariable v |
+    result.(DataFlowIntegrationImpl::ReadNode).readsAt(bb, i, v) and
     use.hasIndexInBlock(bb, i, v) and
     use.isCertain() and
     use.getNode() = n
@@ -1329,10 +1305,8 @@ private DataFlowIntegrationImpl::Node fromDfNode(Node n, SourceVariable v) {
 }
 
 private predicate ssaFlowImpl(Node nodeFrom, Node nodeTo) {
-  exists(SourceVariable v |
-    nodeFrom != nodeTo and
-    DataFlowIntegrationImpl::localFlowStep(v, fromDfNode(nodeFrom, v), fromDfNode(nodeTo, v), _)
-  )
+  nodeFrom != nodeTo and
+  DataFlowIntegrationImpl::localFlowStep(_, fromDfNode(nodeFrom), fromDfNode(nodeTo), _)
 }
 
 /** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */

csharp/ql/consistency-queries/SsaConsistency.ql

@@ -1,6 +1,7 @@
 import csharp
 import semmle.code.csharp.dataflow.internal.SsaImpl as Impl
 import Impl::Consistency
+import Impl::DataFlowIntegration::DfConsistency
 import Ssa
 
 query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {

java/ql/consistency-queries/SsaConsistency.ql

@@ -1,3 +1,4 @@
 import java
 import semmle.code.java.dataflow.internal.SsaImpl
 import Impl::Consistency
+import DataFlowIntegration::DfConsistency

javascript/ql/test/library-tests/FlowSummary/CaptureConsistency.expected

@@ -15,3 +15,4 @@ closureAliasMustBeInSameScope
 variableAccessAstNesting
 uniqueCallableLocation
 consistencyOverview
+ambiguousReadNode

python/ql/test/library-tests/dataflow/variable-capture/dataflow-capture-consistency.expected

@@ -15,3 +15,4 @@ closureAliasMustBeInSameScope
 variableAccessAstNesting
 uniqueCallableLocation
 consistencyOverview
+ambiguousReadNode

ruby/ql/consistency-queries/SsaConsistency.ql

@@ -1,3 +1,4 @@
 import codeql.ruby.dataflow.SSA
 import codeql.ruby.dataflow.internal.SsaImpl
 import Consistency
+import DataFlowIntegration::DfConsistency

rust/ql/consistency-queries/SsaConsistency.ql

@@ -8,3 +8,4 @@
 import codeql.rust.dataflow.Ssa
 import codeql.rust.dataflow.internal.SsaImpl
 import Consistency
+import DataFlowIntegration::DfConsistency

shared/dataflow/codeql/dataflow/VariableCapture.qll

@@ -389,6 +389,8 @@ module Flow<
       msg = "Callable has multiple locations" and 2 <= strictcount(c.getLocation())
     }
 
+    import SsaFlow::DfConsistency
+
     query predicate consistencyOverview(string msg, int n) {
       uniqueToString(msg, n) or
       n = strictcount(BasicBlock bb | uniqueEnclosingCallable(bb, msg)) or

shared/ssa/codeql/ssa/Ssa.qll

@@ -1680,7 +1680,16 @@
     cached
     private newtype TNode =
       TWriteDefSource(WriteDefinition def) { DfInput::ssaDefHasSource(def) } or
-      TExprNode(DfInput::Expr e, Boolean isPost) { e = DfInput::getARead(_) } or
+      TExprNode(DfInput::Expr e, SourceVariable v, Boolean isPost) {
+        exists(BasicBlock bb, int i |
+          e.hasCfgNode(bb, i) and
+          variableRead(bb, i, v, true) and
+          // Only materialise if 'expr' has a reaching definition.
+          // Note that the read may correspond to a different variable than 'v', but the C++
+          // instantiation currently expects this particular behaviour.
+          DfInput::getARead(_) = e
+        )
+      } or
       TSsaDefinitionNode(DefinitionExt def) {
         not phiHasUniqNextNode(def) and
         if DfInput::includeWriteDefsInFlowStep()
@@ -1730,18 +1739,25 @@
     abstract private class ExprNodePreOrPostImpl extends NodeImpl, TExprNode {
       DfInput::Expr e;
       boolean isPost;
+      SourceVariable v_;
 
-      ExprNodePreOrPostImpl() { this = TExprNode(e, isPost) }
+      ExprNodePreOrPostImpl() { this = TExprNode(e, v_, isPost) }
 
       /** Gets the underlying expression. */
       DfInput::Expr getExpr() { result = e }
 
+      /** Holds if this represents the access to `var` performed at `expr`. */
+      predicate isExprAndVariable(DfInput::Expr expr, SourceVariable var) { expr = e and var = v_ }
+
       override Location getLocation() {
         exists(BasicBlock bb, int i |
           e.hasCfgNode(bb, i) and
           result = bb.getNode(i).getLocation()
         )
       }
+
+      /** Gets the variable accessed at this expression. */
+      SourceVariable getSourceVariable() { result = v_ }
     }
 
     final class ExprNodePreOrPost = ExprNodePreOrPostImpl;
@@ -1760,32 +1776,34 @@
       ExprPostUpdateNodeImpl() { isPost = true }
 
       /** Gets the pre-update expression node. */
-      ExprNode getPreUpdateNode() { result = TExprNode(e, false) }
+      ExprNode getPreUpdateNode() { result = TExprNode(e, v_, false) }
 
       override string toString() { result = e.toString() + " [postupdate]" }
     }
 
     final class ExprPostUpdateNode = ExprPostUpdateNodeImpl;
 
-    private class ReadNodeImpl extends ExprNodeImpl {
-      private BasicBlock bb_;
-      private int i_;
-      private SourceVariable v_;
+    pragma[nomagic]
+    private predicate exprReadAt(
+      DfInput::Expr e, BasicBlock bb, int i, SourceVariable v, boolean isPost, TExprNode node
+    ) {
+      variableRead(bb, i, v, true) and
+      e.hasCfgNode(bb, i) and
+      node = TExprNode(e, v, isPost)
+    }
 
-      ReadNodeImpl() {
-        variableRead(bb_, i_, v_, true) and
-        this.getExpr().hasCfgNode(bb_, i_)
-      }
+    private class ReadNodeImpl extends ExprNodeImpl {
+      ReadNodeImpl() { exprReadAt(e, _, _, _, false, this) }
 
+      /** Holds if this node reads `v` at `bb,i` */
       pragma[nomagic]
       predicate readsAt(BasicBlock bb, int i, SourceVariable v) {
-        bb = bb_ and
-        i = i_ and
-        v = v_
+        exprReadAt(e, bb, i, v, false, this)
       }
     }
 
-    final private class ReadNode = ReadNodeImpl;
+    /** A node corresponding to a `(bb,i,v)` tuple from `variableRead(bb,i,v,true)` */
+    final class ReadNode = ReadNodeImpl;
 
     /** A synthesized SSA data flow node. */
     abstract private class SsaNodeImpl extends NodeImpl {
@@ -2017,13 +2035,13 @@
         v = def.getSourceVariable() and
         if DfInput::includeWriteDefsInFlowStep()
         then nodeTo.(SsaDefinitionNode).getDefinition() = def
-        else nodeTo.(ExprNode).getExpr() = DfInput::getARead(def)
+        else nodeTo.(ExprNode).isExprAndVariable(DfInput::getARead(def), v)
       )
       or
       // Flow from SSA definition to read
       exists(DefinitionExt def |
         nodeFrom.(SsaDefinitionExtNodeImpl).getDefExt() = def and
-        nodeTo.(ExprNode).getExpr() = DfInput::getARead(def) and
+        nodeTo.(ExprNode).isExprAndVariable(DfInput::getARead(def), v) and
         v = def.getSourceVariable()
       )
     }
@@ -2129,7 +2147,7 @@
             e = DfInput::getARead(def) and
             e.hasCfgNode(bb, _) and
             DfInput::guardControlsBlock(g, bb, val) and
-            result.(ExprNode).getExpr() = e
+            result.(ExprNode).isExprAndVariable(e, def.getSourceVariable())
           )
           or
           // guard controls input block to a phi node
@@ -2144,6 +2162,17 @@
         )
       }
     }
+
+    /** Provides consistency checks that depend on the DataFlowIntegration inputs. */
+    module DfConsistency {
+      /**
+       * The given `read` reads multiple variables at once. `var` is bound to one of them.
+       */
+      query predicate ambiguousReadNode(ReadNode read, SourceVariable var) {
+        strictcount(SourceVariable v | read.readsAt(_, _, v)) > 1 and
+        read.readsAt(_, _, var)
+      }
+    }
   }
 
   /**

unified/ql/consistency-queries/LocalSsaConsistency.ql

@@ -1,3 +1,4 @@
 private import unified
 private import codeql.unified.internal.dataflow.LocalSsa
 import LocalSsaOutput::Consistency
+import LocalSsaDataFlowOutput::DfConsistency

unified/ql/lib/codeql/unified/internal/dataflow/DataFlowPluginSwift.qll

@@ -25,5 +25,21 @@ private class SwiftDataFlowPlugin extends DataFlowPlugin {
       step.value() and
       node2.isResultValue(call)
     )
+    or
+    // Taint flow through unary "!" (TODO: model as a read of Optional.some, possibly with implicit taint read)
+    exists(UnaryExpr expr |
+      expr.getOperator().(PostfixOperator).getValue() = "!" and
+      node1.isResultValue(expr.getOperand()) and
+      step.taint() and
+      node2.isResultValue(expr)
+    )
+    or
+    // Taint flow through URL(string: x). TODO: Model with MaD and flow summaries
+    exists(CallExpr call |
+      call.getCallee().(Identifier).getValue() = ["URL", "NSURL"] and
+      node1.isResultValue(call.getNamedArgument("string")) and
+      step.taint() and
+      node2.isResultValue(call)
+    )
   }
 }

unified/ql/src/queries/security/CWE-022/PathInjection.ql

@@ -54,7 +54,7 @@ module PathInjectionConfig implements DataFlow::ConfigSig {
   }
 }
 
-module PathInjectionFlow = DataFlow::Global<PathInjectionConfig>;
+module PathInjectionFlow = TaintTracking::Global<PathInjectionConfig>;
 
 import PathInjectionFlow::PathGraph
 

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

@@ -178,6 +178,10 @@ edges
 | test.swift:175:25:175:39 | source(...) | test.swift:175:15:175:39 | ... + ... | provenance |  |
 | test.swift:175:42:175:66 | ... + ... | test.swift:175:14:175:67 | TupleExpr [1] | provenance |  |
 | test.swift:175:52:175:66 | source(...) | test.swift:175:42:175:66 | ... + ... | provenance |  |
+| test.swift:182:9:182:9 | x | test.swift:185:10:185:10 | x | provenance |  |
+| test.swift:182:13:182:27 | source(...) | test.swift:182:9:182:9 | x | provenance |  |
+| test.swift:183:9:183:9 | y | test.swift:186:10:186:10 | y | provenance |  |
+| test.swift:183:13:183:27 | source(...) | test.swift:183:9:183:9 | y | provenance |  |
 nodes
 | calls.swift:7:19:7:19 | x | semmle.label | x |
 | calls.swift:8:14:8:14 | x | semmle.label | x |
@@ -407,6 +411,12 @@ nodes
 | test.swift:175:52:175:66 | source(...) | semmle.label | source(...) |
 | test.swift:176:10:176:10 | a | semmle.label | a |
 | test.swift:177:10:177:10 | b | semmle.label | b |
+| test.swift:182:9:182:9 | x | semmle.label | x |
+| test.swift:182:13:182:27 | source(...) | semmle.label | source(...) |
+| test.swift:183:9:183:9 | y | semmle.label | y |
+| test.swift:183:13:183:27 | source(...) | semmle.label | source(...) |
+| test.swift:185:10:185:10 | x | semmle.label | x |
+| test.swift:186:10:186:10 | y | semmle.label | y |
 subpaths
 | calls.swift:31:17:31:30 | source(...) | calls.swift:28:19:28:19 | x | calls.swift:29:16:29:24 | ... + ... | calls.swift:31:10:31:31 | target(...) |
 | calls.swift:32:17:32:30 | source(...) | calls.swift:28:19:28:19 | x | calls.swift:29:16:29:24 | ... + ... | calls.swift:32:10:32:31 | target(...) |
@@ -476,3 +486,5 @@ testFailures
 | test.swift:168:10:168:12 | ... .0 | test.swift:167:29:167:43 | source(...) | test.swift:168:10:168:12 | ... .0 | $@ | test.swift:167:29:167:43 | source(...) | source(...) |
 | test.swift:176:10:176:10 | a | test.swift:175:25:175:39 | source(...) | test.swift:176:10:176:10 | a | $@ | test.swift:175:25:175:39 | source(...) | source(...) |
 | test.swift:177:10:177:10 | b | test.swift:175:52:175:66 | source(...) | test.swift:177:10:177:10 | b | $@ | test.swift:175:52:175:66 | source(...) | source(...) |
+| test.swift:185:10:185:10 | x | test.swift:182:13:182:27 | source(...) | test.swift:185:10:185:10 | x | $@ | test.swift:182:13:182:27 | source(...) | source(...) |
+| test.swift:186:10:186:10 | y | test.swift:183:13:183:27 | source(...) | test.swift:186:10:186:10 | y | $@ | test.swift:183:13:183:27 | source(...) | source(...) |

unified/ql/test/library-tests/dataflow/test.swift

@@ -176,3 +176,12 @@ func t19() {
     sink(a)  // $ hasTaintFlow=t19.1
     sink(b)  // $ hasTaintFlow=t19.2
 }
+
+func t20() {
+    func foo(x: String, y: String) -> String { return x }
+    var x = source("t20.1")
+    var y = source("t20.2")
+    foo(x: x, y: y)
+    sink(x)  // $ hasValueFlow=t20.1
+    sink(y)  // $ hasValueFlow=t20.2
+}