C#: Adopt shared SSA data-flow integration

Author: hvitved

csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll

@@ -29,7 +29,7 @@ module BaseSsa {
   ) {
     exists(ControlFlow::ControlFlow::BasicBlocks::EntryBlock entry |
       c = entry.getCallable() and
-      // In case `c` has multiple bodies, we want each body to gets its own implicit
+      // In case `c` has multiple bodies, we want each body to get its own implicit
       // entry definition. In case `c` doesn't have multiple bodies, the line below
       // is simply the same as `bb = entry`, because `entry.getFirstNode().getASuccessor()`
       // will be in the entry block.

csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll

@@ -256,8 +256,9 @@ module VariableCapture {
   private predicate closureFlowStep(ControlFlow::Nodes::ExprNode e1, ControlFlow::Nodes::ExprNode e2) {
     e1 = LocalFlow::getALastEvalNode(e2)
     or
-    exists(Ssa::Definition def |
-      LocalFlow::ssaDefAssigns(def.getAnUltimateDefinition(), e1) and
+    exists(Ssa::Definition def, AssignableDefinition adef |
+      LocalFlow::defAssigns(adef, _, e1) and
+      def.getAnUltimateDefinition().(Ssa::ExplicitDefinition).getADefinition() = adef and
       exists(def.getAReadAtNode(e2))
     )
   }
@@ -481,6 +482,30 @@ module VariableCapture {
   }
 }
 
+/** Provides logic related to SSA. */
+module SsaFlow {
+  private module Impl = SsaImpl::DataFlowIntegration;
+
+  Impl::Node asNode(Node n) {
+    n = TSsaNode(result)
+    or
+    result.(Impl::ExprNode).getExpr() = n.(ExprNode).getControlFlowNode()
+    or
+    result.(Impl::ExprPostUpdateNode).getExpr() =
+      n.(PostUpdateNode).getPreUpdateNode().(ExprNode).getControlFlowNode()
+    or
+    TExplicitParameterNode(result.(Impl::ParameterNode).getParameter()) = n
+  }
+
+  predicate localFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep) {
+    Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo), isUseStep)
+  }
+
+  predicate localMustFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
+    Impl::localMustFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
+  }
+}
+
 /** Provides predicates related to local data flow. */
 module LocalFlow {
   class LocalExprStepConfiguration extends ControlFlowReachabilityConfiguration {
@@ -606,105 +631,6 @@ module LocalFlow {
     any(LocalExprStepConfiguration x).hasDefPath(_, value, def, cfnDef)
   }
 
-  predicate ssaDefAssigns(Ssa::ExplicitDefinition ssaDef, ControlFlow::Nodes::ExprNode value) {
-    exists(AssignableDefinition def, ControlFlow::Node cfnDef |
-      any(LocalExprStepConfiguration conf).hasDefPath(_, value, def, cfnDef) and
-      ssaDef.getADefinition() = def and
-      ssaDef.getControlFlowNode() = cfnDef
-    )
-  }
-
-  /**
-   * An uncertain SSA definition. Either an uncertain explicit definition or an
-   * uncertain qualifier definition.
-   *
-   * Restricts `Ssa::UncertainDefinition` by excluding implicit call definitions,
-   * as we---conservatively---consider such definitions to be certain.
-   */
-  class UncertainExplicitSsaDefinition extends Ssa::UncertainDefinition {
-    UncertainExplicitSsaDefinition() {
-      this instanceof Ssa::ExplicitDefinition
-      or
-      this =
-        any(Ssa::ImplicitQualifierDefinition qdef |
-          qdef.getQualifierDefinition() instanceof UncertainExplicitSsaDefinition
-        )
-    }
-  }
-
-  /** An SSA definition into which another SSA definition may flow. */
-  private class SsaInputDefinitionExtNode extends SsaDefinitionExtNode {
-    SsaInputDefinitionExtNode() {
-      def instanceof Ssa::PhiNode
-      or
-      def instanceof SsaImpl::PhiReadNode
-      or
-      def instanceof LocalFlow::UncertainExplicitSsaDefinition
-    }
-  }
-
-  /**
-   * Holds if `nodeFrom` is a last node referencing SSA definition `def`, which
-   * can reach `next`.
-   */
-  private predicate localFlowSsaInputFromDef(
-    Node nodeFrom, SsaImpl::DefinitionExt def, SsaInputDefinitionExtNode next
-  ) {
-    exists(ControlFlow::BasicBlock bb, int i |
-      SsaImpl::lastRefBeforeRedefExt(def, bb, i, next.getDefinitionExt()) and
-      def.definesAt(_, bb, i, _) and
-      def = getSsaDefinitionExt(nodeFrom) and
-      nodeFrom != next
-    )
-  }
-
-  /**
-   * Holds if `read` is a last node reading SSA definition `def`, which
-   * can reach `next`.
-   */
-  predicate localFlowSsaInputFromRead(
-    Node read, SsaImpl::DefinitionExt def, SsaInputDefinitionExtNode next
-  ) {
-    exists(ControlFlow::BasicBlock bb, int i |
-      SsaImpl::lastRefBeforeRedefExt(def, bb, i, next.getDefinitionExt()) and
-      read.asExprAtNode(bb.getNode(i)) instanceof AssignableRead
-    )
-  }
-
-  private SsaImpl::DefinitionExt getSsaDefinitionExt(Node n) {
-    result = n.(SsaDefinitionExtNode).getDefinitionExt()
-    or
-    result = n.(ExplicitParameterNode).getSsaDefinition()
-  }
-
-  /**
-   * Holds if there is a local use-use flow step from `nodeFrom` to `nodeTo`
-   * involving SSA definition `def`.
-   */
-  predicate localSsaFlowStepUseUse(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
-    exists(ControlFlow::Node cfnFrom, ControlFlow::Node cfnTo |
-      SsaImpl::adjacentReadPairSameVarExt(def, cfnFrom, cfnTo) and
-      nodeTo = TExprNode(cfnTo) and
-      nodeFrom = TExprNode(cfnFrom)
-    )
-  }
-
-  /**
-   * Holds if there is a local flow step from `nodeFrom` to `nodeTo` involving
-   * SSA definition `def`.
-   */
-  predicate localSsaFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
-    // Flow from SSA definition/parameter to first read
-    def = getSsaDefinitionExt(nodeFrom) and
-    SsaImpl::firstReadSameVarExt(def, nodeTo.(ExprNode).getControlFlowNode())
-    or
-    // Flow from read to next read
-    localSsaFlowStepUseUse(def, nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
-    or
-    // Flow into phi (read)/uncertain SSA definition node from def
-    localFlowSsaInputFromDef(nodeFrom, def, nodeTo)
-  }
-
   /**
    * Holds if the source variable of SSA definition `def` is an instance field.
    */
@@ -788,10 +714,7 @@ module LocalFlow {
       node2.asExpr() instanceof AssignExpr
     )
     or
-    exists(SsaImpl::Definition def |
-      def = getSsaDefinitionExt(node1) and
-      exists(SsaImpl::getAReadAtNode(def, node2.(ExprNode).getControlFlowNode()))
-    )
+    SsaFlow::localMustFlowStep(_, node1, node2)
     or
     node2 = node1.(LocalFunctionCreationNode).getAnAccess(true)
     or
@@ -815,23 +738,14 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
   (
     LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
     or
-    exists(SsaImpl::DefinitionExt def |
+    exists(SsaImpl::DefinitionExt def, boolean isUseStep |
+      SsaFlow::localFlowStep(def, nodeFrom, nodeTo, isUseStep) and
       not LocalFlow::usesInstanceField(def) and
       not def instanceof VariableCapture::CapturedSsaDefinitionExt
     |
-      LocalFlow::localSsaFlowStep(def, nodeFrom, nodeTo)
-      or
-      LocalFlow::localSsaFlowStepUseUse(def, nodeFrom, nodeTo) and
-      not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _) and
-      nodeFrom != nodeTo
+      isUseStep = false
       or
-      // Flow into phi (read)/uncertain SSA definition node from read
-      exists(Node read | LocalFlow::localFlowSsaInputFromRead(read, def, nodeTo) |
-        nodeFrom = read and
-        not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _)
-        or
-        nodeFrom.(PostUpdateNode).getPreUpdateNode() = read
-      )
+      not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _)
     )
     or
     nodeTo.(ObjectCreationNode).getPreUpdateNode() = nodeFrom.(ObjectInitializerNode)
@@ -1097,10 +1011,7 @@ private module Cached {
   cached
   newtype TNode =
     TExprNode(ControlFlow::Nodes::ElementNode cfn) { cfn.getAstNode() instanceof Expr } or
-    TSsaDefinitionExtNode(SsaImpl::DefinitionExt def) {
-      // Handled by `TExplicitParameterNode` below
-      not def instanceof Ssa::ImplicitParameterDefinition
-    } or
+    TSsaNode(SsaImpl::DataFlowIntegration::SsaNode node) or
     TAssignableDefinitionNode(AssignableDefinition def, ControlFlow::Node cfn) {
       cfn = def.getExpr().getAControlFlowNode()
     } or
@@ -1165,17 +1076,7 @@ private module Cached {
   predicate localFlowStepImpl(Node nodeFrom, Node nodeTo) {
     LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
     or
-    LocalFlow::localSsaFlowStepUseUse(_, nodeFrom, nodeTo) and
-    nodeFrom != nodeTo
-    or
-    LocalFlow::localSsaFlowStep(_, nodeFrom, nodeTo)
-    or
-    // Flow into phi (read)/uncertain SSA definition node from read
-    exists(Node read | LocalFlow::localFlowSsaInputFromRead(read, _, nodeTo) |
-      nodeFrom = read
-      or
-      nodeFrom.(PostUpdateNode).getPreUpdateNode() = read
-    )
+    SsaFlow::localFlowStep(_, nodeFrom, nodeTo, _)
     or
     // Simple flow through library code is included in the exposed local
     // step relation, even though flow is technically inter-procedural
@@ -1233,13 +1134,18 @@ private module Cached {
   newtype TDataFlowType =
     TGvnDataFlowType(Gvn::GvnType t) or
     TDelegateDataFlowType(Callable lambda) { lambdaCreationExpr(_, lambda) }
+
+  cached
+  Node getABarrierNode(Guard guard, Ssa::Definition def, boolean branch) {
+    SsaFlow::asNode(result) = SsaImpl::DataFlowIntegration::getABarrierNode(guard, def, branch)
+  }
 }
 
 import Cached
 
 /** Holds if `n` should be hidden from path explanations. */
 predicate nodeIsHidden(Node n) {
-  n instanceof SsaDefinitionExtNode
+  n instanceof SsaNode
   or
   exists(Parameter p | p = n.(ParameterNode).getParameter() | not p.fromSource())
   or
@@ -1273,13 +1179,16 @@ predicate nodeIsHidden(Node n) {
   n instanceof CaptureNode
 }
 
-/** An SSA definition, viewed as a node in a data flow graph. */
-class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
+/** An SSA node. */
+abstract class SsaNode extends NodeImpl, TSsaNode {
+  SsaImpl::DataFlowIntegration::SsaNode node;
   SsaImpl::DefinitionExt def;
 
-  SsaDefinitionExtNode() { this = TSsaDefinitionExtNode(def) }
+  SsaNode() {
+    this = TSsaNode(node) and
+    def = node.getDefinitionExt()
+  }
 
-  /** Gets the underlying SSA definition. */
   SsaImpl::DefinitionExt getDefinitionExt() { result = def }
 
   override DataFlowCallable getEnclosingCallableImpl() {
@@ -1292,9 +1201,57 @@ class SsaDefinitionExtNode extends NodeImpl, TSsaDefinitionExtNode {
     result = def.(Ssa::Definition).getControlFlowNode()
   }
 
-  override Location getLocationImpl() { result = def.getLocation() }
+  override Location getLocationImpl() { result = node.getLocation() }
+
+  override string toStringImpl() { result = node.toString() }
+}
+
+/** An (extended) SSA definition, viewed as a node in a data flow graph. */
+class SsaDefinitionExtNode extends SsaNode {
+  override SsaImpl::DataFlowIntegration::SsaDefinitionExtNode node;
+}
 
-  override string toStringImpl() { result = def.toString() }
+/**
+ * A node that represents an input to an SSA phi (read) definition.
+ *
+ * This allows for barrier guards to filter input to phi nodes. For example, in
+ *
+ * ```csharp
+ * var x = taint;
+ * if (x != "safe")
+ * {
+ *     x = "safe";
+ * }
+ * sink(x);
+ * ```
+ *
+ * the `false` edge out of `x != "safe"` guards the input from `x = taint` into the
+ * `phi` node after the condition.
+ *
+ * It is also relevant to filter input into phi read nodes:
+ *
+ * ```csharp
+ * var x = taint;
+ * if (b)
+ * {
+ *     if (x != "safe1")
+ *     {
+ *         return;
+ *     }
+ * } else {
+ *     if (x != "safe2")
+ *     {
+ *         return;
+ *     }
+ * }
+ *
+ * sink(x);
+ * ```
+ *
+ * both inputs into the phi read node after the outer condition are guarded.
+ */
+class SsaInputNode extends SsaNode {
+  override SsaImpl::DataFlowIntegration::SsaInputNode node;
 }
 
 /** A definition, viewed as a node in a data flow graph. */
@@ -2844,7 +2801,7 @@ private predicate delegateCreationStep(Node nodeFrom, Node nodeTo) {
 /** Extra data-flow steps needed for lambda flow analysis. */
 predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) {
   exists(SsaImpl::DefinitionExt def |
-    LocalFlow::localSsaFlowStep(def, nodeFrom, nodeTo) and
+    SsaFlow::localFlowStep(def, nodeFrom, nodeTo, _) and
     preservesValue = true
   |
     LocalFlow::usesInstanceField(def)

csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPublic.qll

@@ -171,8 +171,22 @@ signature predicate guardChecksSig(Guard g, Expr e, AbstractValue v);
  * in data flow and taint tracking.
  */
 module BarrierGuard<guardChecksSig/3 guardChecks> {
+  pragma[nomagic]
+  private predicate guardChecksSsaDef(Guard g, Ssa::Definition def, boolean branch) {
+    exists(AbstractValues::BooleanValue v |
+      guardChecks(g, def.getARead(), v) and
+      branch = v.getValue()
+    )
+  }
+
   /** Gets a node that is safely guarded by the given guard check. */
-  ExprNode getABarrierNode() {
+  pragma[nomagic]
+  Node getABarrierNode() {
+    exists(Guard g, Ssa::Definition def, boolean branch |
+      result = getABarrierNode(g, def, branch) and
+      guardChecksSsaDef(g, def, branch)
+    )
+    or
     exists(Guard g, Expr e, AbstractValue v |
       guardChecks(g, e, v) and
       g.controlsNode(result.getControlFlowNode(), e, v)