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

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,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,8 +1735,9 @@
     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 }
@@ -1742,6 +1748,9 @@
           result = bb.getNode(i).getLocation()
         )
       }
+
+      /** Gets the variable accessed at this expression. */
+      SourceVariable getSourceVariable() { result = v_ }
     }
 
     final class ExprNodePreOrPost = ExprNodePreOrPostImpl;
@@ -1760,7 +1769,7 @@
       ExprPostUpdateNodeImpl() { isPost = true }
 
       /** Gets the pre-update expression node. */
-      ExprNode getPreUpdateNode() { result = TExprNode(e, false) }
+      ExprNode getPreUpdateNode() { result = TExprNode(e, _, false) }
 
       override string toString() { result = e.toString() + " [postupdate]" }
     }
@@ -1770,7 +1779,6 @@
     private class ReadNodeImpl extends ExprNodeImpl {
       private BasicBlock bb_;
       private int i_;
-      private SourceVariable v_;
 
       ReadNodeImpl() {
         variableRead(bb_, i_, v_, true) and
@@ -2144,6 +2152,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
+}