C#: Data-flow pruning based on call contexts

Author: hvitved

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

@@ -3,10 +3,12 @@ private import cil
 private import dotnet
 private import DataFlowPublic
 private import DataFlowDispatch
+private import DataFlowImplCommon::Public
 private import ControlFlowReachability
 private import DelegateDataFlow
 private import semmle.code.csharp.Caching
 private import semmle.code.csharp.ExprOrStmtParent
+private import semmle.code.csharp.controlflow.Guards
 private import semmle.code.csharp.dataflow.LibraryTypeDataFlow
 private import semmle.code.csharp.dispatch.Dispatch
 private import semmle.code.csharp.frameworks.EntityFramework
@@ -439,6 +441,22 @@ private module Cached {
       c.(FieldLikeContent).getField() = node2.asExpr().(FieldLikeRead).getTarget()
     )
   }
+
+  /**
+   * Holds if the node `n` is unreachable when the call context is `call`.
+   */
+  cached
+  predicate isUnreachableInCall(Node n, DataFlowCall call) {
+    exists(
+      SsaDefinitionNode paramNode, Ssa::ExplicitDefinition param, Guard guard,
+      ControlFlow::SuccessorTypes::BooleanSuccessor bs
+    |
+      viableConstantBooleanParamArg(paramNode, bs.getValue().booleanNot(), call) and
+      paramNode.getDefinition() = param and
+      param.getARead() = guard and
+      guard.controlsBlock(n.getControlFlowNode().getBasicBlock(), bs)
+    )
+  }
 }
 
 import Cached
@@ -1358,4 +1376,31 @@ class DataFlowType = DotNet::Type;
 
 class DataFlowLocation = Location;
 
-predicate isUnreachableInCall(Node n, DataFlowCall call) { none() } // stub implementation
+/** Holds if `e` is an expression that always has the same Boolean value `val`. */
+private predicate constantBooleanExpr(Expr e, boolean val) {
+  e = any(AbstractValues::BooleanValue bv | val = bv.getValue()).getAnExpr()
+  or
+  exists(Ssa::ExplicitDefinition def, Expr src |
+    e = def.getARead() and
+    src = def.getADefinition().getSource() and
+    constantBooleanExpr(src, val)
+  )
+}
+
+/** An argument that always has the same Boolean value. */
+private class ConstantBooleanArgumentNode extends ExprNode {
+  ConstantBooleanArgumentNode() { constantBooleanExpr(this.(ArgumentNode).asExpr(), _) }
+
+  /** Gets the Boolean value of this expression. */
+  boolean getBooleanValue() { constantBooleanExpr(this.getExpr(), result) }
+}
+
+pragma[noinline]
+private predicate viableConstantBooleanParamArg(
+  SsaDefinitionNode paramNode, boolean b, DataFlowCall call
+) {
+  exists(ConstantBooleanArgumentNode arg |
+    viableParamArg(call, paramNode, arg) and
+    b = arg.getBooleanValue()
+  )
+}