@@ -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) {

@@ -1,3 +1,4 @@
 import java
 import semmle.code.java.dataflow.internal.SsaImpl
 import Impl::Consistency
+import DataFlowIntegration::DfConsistency
@@ -15,3 +15,4 @@ closureAliasMustBeInSameScope
 variableAccessAstNesting
 uniqueCallableLocation
 consistencyOverview
+ambiguousReadNode
@@ -15,3 +15,4 @@ closureAliasMustBeInSameScope
 variableAccessAstNesting
 uniqueCallableLocation
 consistencyOverview
+ambiguousReadNode
@@ -1,3 +1,4 @@
 import codeql.ruby.dataflow.SSA
 import codeql.ruby.dataflow.internal.SsaImpl
 import Consistency
+import DataFlowIntegration::DfConsistency
@@ -8,3 +8,4 @@
 import codeql.rust.dataflow.Ssa
 import codeql.rust.dataflow.internal.SsaImpl
 import Consistency
+import DataFlowIntegration::DfConsistency
@@ -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

@@ -1680,7 +1680,12 @@
     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(Definition def |
+          def.getSourceVariable() = v and
+          e = DfInput::getARead(def)
+        )
+      } or
       TSsaDefinitionNode(DefinitionExt def) {
         not phiHasUniqNextNode(def) and
         if DfInput::includeWriteDefsInFlowStep()
@@ -1730,18 +1735,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 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,28 +1772,28 @@
       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) }
 
       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)
       }
     }
 
@@ -2017,13 +2029,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 +2141,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 +2156,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)
+      }
+    }
   }
 
   /**

@@ -1,3 +1,4 @@
 private import unified
 private import codeql.unified.internal.dataflow.LocalSsa
 import LocalSsaOutput::Consistency
+import LocalSsaDataFlowOutput::DfConsistency
@@ -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)
+    )
   }
 }
@@ -54,7 +54,7 @@ module PathInjectionConfig implements DataFlow::ConfigSig {
   }
 }
 
-module PathInjectionFlow = DataFlow::Global<PathInjectionConfig>;
+module PathInjectionFlow = TaintTracking::Global<PathInjectionConfig>;
 
 import PathInjectionFlow::PathGraph
 

@@ -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(...) |
@@ -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
+}
-Original file line number
+Diff line change
@@ Expand Up / @@ -54,7 +54,7 @@ module PathInjectionConfig implements DataFlow::ConfigSig { @@
       }
     }
-    module PathInjectionFlow = DataFlow::Global<PathInjectionConfig>;
+    module PathInjectionFlow = TaintTracking::Global<PathInjectionConfig>;
     import PathInjectionFlow::PathGraph
@@ Expand Down @@