C#: Enable data-flow consistency queries

Author: hvitved

csharp/ql/consistency-queries/DataFlowConsistency.ql

@@ -0,0 +1,54 @@
+import csharp
+import cil
+import semmle.code.csharp.dataflow.internal.DataFlowPrivate
+import semmle.code.csharp.dataflow.internal.DataFlowPublic
+import semmle.code.csharp.dataflow.internal.DataFlowImplConsistency::Consistency
+
+private class MyConsistencyConfiguration extends ConsistencyConfiguration {
+  override predicate uniqueEnclosingCallableExclude(Node n) {
+    // TODO: Remove once static initializers are folded into the
+    // static constructors
+    exists(ControlFlow::Node cfn |
+      cfn.getElement() = any(FieldOrProperty f | f.isStatic()).getAChild+() and
+      cfn = n.getControlFlowNode()
+    )
+  }
+
+  override predicate uniqueNodeLocationExclude(Node n) {
+    // Methods with multiple implementations
+    n instanceof ParameterNode
+    or
+    this.missingLocationExclude(n)
+  }
+
+  override predicate missingLocationExclude(Node n) {
+    // Some CIL methods are missing locations
+    n.asParameter() instanceof CIL::Parameter
+  }
+
+  override predicate postWithInFlowExclude(Node n) {
+    n instanceof SummaryNode
+    or
+    n.asExpr().(ObjectCreation).hasInitializer()
+  }
+
+  override predicate argHasPostUpdateExclude(ArgumentNode n) {
+    n instanceof SummaryNode
+    or
+    n.asExpr().(Expr).stripCasts().getType() =
+      any(Type t |
+        not t instanceof RefType and
+        not t = any(TypeParameter tp | not tp.isValueType())
+        or
+        t instanceof NullType
+      )
+    or
+    n instanceof ImplicitCapturedArgumentNode
+    or
+    n instanceof ParamsArgumentNode
+    or
+    n.asExpr() instanceof CIL::Expr
+  }
+
+  override predicate reverseReadExclude(Node n) { n.asExpr() = any(AwaitExpr ae).getExpr() }
+}

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

@@ -15,11 +15,23 @@ module Consistency {
   class ConsistencyConfiguration extends TConsistencyConfiguration {
     string toString() { none() }
 
+    /** Holds if `n` should be excluded from the consistency test `uniqueEnclosingCallable`. */
+    predicate uniqueEnclosingCallableExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `uniqueNodeLocation`. */
+    predicate missingLocationExclude(Node n) { none() }
+
     /** Holds if `n` should be excluded from the consistency test `postWithInFlow`. */
     predicate postWithInFlowExclude(Node n) { none() }
 
     /** Holds if `n` should be excluded from the consistency test `argHasPostUpdate`. */
     predicate argHasPostUpdateExclude(ArgumentNode n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `reverseRead`. */
+    predicate reverseReadExclude(Node n) { none() }
   }
 
   private class RelevantNode extends Node {
@@ -46,6 +58,7 @@ module Consistency {
       n instanceof RelevantNode and
       c = count(nodeGetEnclosingCallable(n)) and
       c != 1 and
+      not any(ConsistencyConfiguration conf).uniqueEnclosingCallableExclude(n) and
       msg = "Node should have one enclosing callable but has " + c + "."
     )
   }
@@ -66,6 +79,7 @@ module Consistency {
           n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
         ) and
       c != 1 and
+      not any(ConsistencyConfiguration conf).uniqueNodeLocationExclude(n) and
       msg = "Node should have one location but has " + c + "."
     )
   }
@@ -76,7 +90,8 @@ module Consistency {
         strictcount(Node n |
           not exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
             n.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
-          )
+          ) and
+          not any(ConsistencyConfiguration conf).missingLocationExclude(n)
         ) and
       msg = "Nodes without location: " + c
     )
@@ -172,6 +187,7 @@ module Consistency {
 
   query predicate reverseRead(Node n, string msg) {
     exists(Node n2 | readStep(n, _, n2) and hasPost(n2) and not hasPost(n)) and
+    not any(ConsistencyConfiguration conf).reverseReadExclude(n) and
     msg = "Origin of readStep is missing a PostUpdateNode."
   }
 

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

@@ -1436,7 +1436,7 @@ private module OutNodes {
 import OutNodes
 
 /** A data-flow node used to model flow summaries. */
-private class SummaryNode extends NodeImpl, TSummaryNode {
+class SummaryNode extends NodeImpl, TSummaryNode {
   private FlowSummary::SummarizedCallable c;
   private FlowSummaryImpl::Private::SummaryNodeState state;
 
@@ -1485,6 +1485,13 @@ class FieldOrProperty extends Assignable, Modifiable {
     or
     result.(PropertyContent).getProperty() = this.getUnboundDeclaration()
   }
+
+  /** Gets the initializer of this field or property, if any. */
+  Expr getInitialier() {
+    result = this.(Field).getInitializer()
+    or
+    result = this.(Property).getInitializer()
+  }
 }
 
 private class InstanceFieldOrProperty extends FieldOrProperty {