C#: Unmerge SSA and data flow stages

Author: hvitved

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

@@ -484,7 +484,7 @@ module VariableCapture {
 
 /** Provides logic related to SSA. */
 module SsaFlow {
-  module Impl = SsaImpl::DataFlowIntegration;
+  private module Impl = SsaImpl::DataFlowIntegration;
 
   Impl::Node asNode(Node n) {
     n = TSsaNode(result)
@@ -497,8 +497,8 @@ module SsaFlow {
     TExplicitParameterNode(result.(Impl::ParameterNode).getParameter()) = n
   }
 
-  predicate localFlowStep(SsaImpl::DefinitionExt def, Node nodeFrom, Node nodeTo) {
-    Impl::localFlowStep(def, asNode(nodeFrom), asNode(nodeTo))
+  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) {
@@ -738,10 +738,13 @@ predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo, string model) {
   (
     LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
     or
-    exists(SsaImpl::DefinitionExt def |
-      SsaFlow::localFlowStep(def, nodeFrom, nodeTo) and
+    exists(SsaImpl::DefinitionExt def, boolean isUseStep |
+      SsaFlow::localFlowStep(def, nodeFrom, nodeTo, isUseStep) and
       not LocalFlow::usesInstanceField(def) and
-      not def instanceof VariableCapture::CapturedSsaDefinitionExt and
+      not def instanceof VariableCapture::CapturedSsaDefinitionExt
+    |
+      isUseStep = false
+      or
       not FlowSummaryImpl::Private::Steps::prohibitsUseUseFlow(nodeFrom, _)
     )
     or
@@ -1008,7 +1011,7 @@ private module Cached {
   cached
   newtype TNode =
     TExprNode(ControlFlow::Nodes::ElementNode cfn) { cfn.getAstNode() instanceof Expr } or
-    TSsaNode(SsaFlow::Impl::SsaNode node) or
+    TSsaNode(SsaImpl::DataFlowIntegration::SsaNode node) or
     TAssignableDefinitionNode(AssignableDefinition def, ControlFlow::Node cfn) {
       cfn = def.getExpr().getAControlFlowNode()
     } or
@@ -1073,7 +1076,7 @@ private module Cached {
   predicate localFlowStepImpl(Node nodeFrom, Node nodeTo) {
     LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
     or
-    SsaFlow::localFlowStep(_, nodeFrom, nodeTo)
+    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
@@ -1178,7 +1181,7 @@ predicate nodeIsHidden(Node n) {
 
 /** An SSA node. */
 abstract class SsaNode extends NodeImpl, TSsaNode {
-  SsaFlow::Impl::SsaNode node;
+  SsaImpl::DataFlowIntegration::SsaNode node;
   SsaImpl::DefinitionExt def;
 
   SsaNode() {
@@ -1205,7 +1208,7 @@ abstract class SsaNode extends NodeImpl, TSsaNode {
 
 /** An (extended) SSA definition, viewed as a node in a data flow graph. */
 class SsaDefinitionExtNode extends SsaNode {
-  override SsaFlow::Impl::SsaDefinitionExtNode node;
+  override SsaImpl::DataFlowIntegration::SsaDefinitionExtNode node;
 }
 
 /**
@@ -1248,7 +1251,7 @@ class SsaDefinitionExtNode extends SsaNode {
  * both inputs into the phi read node after the outer condition are guarded.
  */
 class SsaInputNode extends SsaNode {
-  override SsaFlow::Impl::SsaInputNode node;
+  override SsaImpl::DataFlowIntegration::SsaInputNode node;
 }
 
 /** A definition, viewed as a node in a data flow graph. */
@@ -2798,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 |
-    SsaFlow::localFlowStep(def, nodeFrom, nodeTo) and
+    SsaFlow::localFlowStep(def, nodeFrom, nodeTo, _) and
     preservesValue = true
   |
     LocalFlow::usesInstanceField(def)

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

@@ -6,6 +6,7 @@ import csharp
 private import codeql.ssa.Ssa as SsaImplCommon
 private import AssignableDefinitions
 private import semmle.code.csharp.controlflow.internal.PreSsa
+private import semmle.code.csharp.controlflow.Guards as Guards
 
 private module SsaInput implements SsaImplCommon::InputSig<Location> {
   class BasicBlock = ControlFlow::BasicBlock;
@@ -978,13 +979,24 @@ private module Cached {
     )
   }
 
-  private import TaintTrackingPrivate as TaintTrackingPrivate
-
   cached
-  predicate forceCachingInSameStage() {
-    // needed in order to avoid recomputing SSA predicates in the `Integration` module
-    TaintTrackingPrivate::forceCachingInSameStage() and
-    DataFlowIntegration::localFlowStep(_, _, _)
+  module DataFlowIntegration {
+    import DataFlowIntegrationImpl
+
+    cached
+    predicate localFlowStep(DefinitionExt def, Node nodeFrom, Node nodeTo, boolean isUseStep) {
+      DataFlowIntegrationImpl::localFlowStep(def, nodeFrom, nodeTo, isUseStep)
+    }
+
+    cached
+    predicate localMustFlowStep(DefinitionExt def, Node nodeFrom, Node nodeTo) {
+      DataFlowIntegrationImpl::localMustFlowStep(def, nodeFrom, nodeTo)
+    }
+
+    cached
+    Node getABarrierNode(Guards::Guard guard, Ssa::Definition def, boolean branch) {
+      result = DataFlowIntegrationImpl::getABarrierNode(guard, def, branch)
+    }
   }
 }
 
@@ -1047,7 +1059,6 @@ class PhiReadNode extends DefinitionExt, Impl::PhiReadNode {
 private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInputSig {
   private import csharp as Cs
   private import semmle.code.csharp.controlflow.BasicBlocks
-  private import semmle.code.csharp.controlflow.Guards as Guards
 
   class Expr extends ControlFlow::Node {
     predicate hasCfgNode(ControlFlow::BasicBlock bb, int i) { this = bb.getNode(i) }
@@ -1104,4 +1115,4 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
   }
 }
 
-module DataFlowIntegration = Impl::DataFlowIntegration<DataFlowIntegrationInput>;
+private module DataFlowIntegrationImpl = Impl::DataFlowIntegration<DataFlowIntegrationInput>;