Merge pull request #7231 from hvitved/csharp/dataflow/consistency-queries

C#: Enable data-flow consistency queries

cpp/ql/lib/semmle/code/cpp/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 `uniqueNodeLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    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."
   }
 

cpp/ql/lib/semmle/code/cpp/ir/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 `uniqueNodeLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    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/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/cil/Method.qll

@@ -89,7 +89,7 @@ class Method extends DotNet::Callable, Element, Member, TypeContainer, DataFlowN
 
   override Location getLocation() { result = Element.super.getLocation() }
 
-  override Location getALocation() { cil_method_location(this.getUnboundDeclaration(), result) }
+  override Location getALocation() { cil_method_location(this.getUnboundMethod+(), result) }
 
   override MethodParameter getParameter(int n) {
     if this.isStatic()

csharp/ql/lib/semmle/code/csharp/Unification.qll

@@ -80,7 +80,8 @@ module Gvn {
     LeafType() {
       not this instanceof GenericType and
       not this instanceof TypeParameter and
-      not this instanceof DynamicType
+      not this instanceof DynamicType and
+      not this instanceof TupleType
     }
   }
 
@@ -478,6 +479,8 @@ module Gvn {
     GvnType getGlobalValueNumber(Type t) {
       result = TLeafGvnType(t)
       or
+      result = TLeafGvnType(t.(TupleType).getUnderlyingType())
+      or
       t instanceof DynamicType and
       result = TLeafGvnType(any(ObjectType ot))
       or

csharp/ql/lib/semmle/code/csharp/dataflow/LibraryTypeDataFlow.qll

@@ -585,7 +585,7 @@ class IEnumerableFlow extends LibraryTypeDataFlow, RefType {
           sink = getDelegateFlowSinkArg(m, 1, 1) and
           sinkAp = AccessPath::empty()
           or
-          source = TCallableFlowSourceDelegateArg(1) and
+          source = getDelegateFlowSourceArg(m, 1) and
           sourceAp = AccessPath::empty() and
           sink = TCallableFlowSinkReturn() and
           sinkAp = AccessPath::empty()
@@ -603,7 +603,7 @@ class IEnumerableFlow extends LibraryTypeDataFlow, RefType {
           sink = getDelegateFlowSinkArg(m, 2, 0) and
           sinkAp = AccessPath::empty()
           or
-          source = TCallableFlowSourceDelegateArg(2) and
+          source = getDelegateFlowSourceArg(m, 2) and
           sourceAp = AccessPath::empty() and
           sink = TCallableFlowSinkReturn() and
           sinkAp = AccessPath::empty()
@@ -621,12 +621,12 @@ class IEnumerableFlow extends LibraryTypeDataFlow, RefType {
           sink = getDelegateFlowSinkArg(m, 2, 0) and
           sinkAp = AccessPath::empty()
           or
-          source = TCallableFlowSourceDelegateArg(2) and
+          source = getDelegateFlowSourceArg(m, 2) and
           sourceAp = AccessPath::empty() and
           sink = getDelegateFlowSinkArg(m, 3, 0) and
           sinkAp = AccessPath::empty()
           or
-          source = TCallableFlowSourceDelegateArg(3) and
+          source = getDelegateFlowSourceArg(m, 3) and
           sourceAp = AccessPath::empty() and
           sink = TCallableFlowSinkReturn() and
           sinkAp = AccessPath::empty()
@@ -841,7 +841,7 @@ class IEnumerableFlow extends LibraryTypeDataFlow, RefType {
           sink = getDelegateFlowSinkArg(m, 4, 1) and
           sinkAp = AccessPath::empty()
           or
-          source = TCallableFlowSourceDelegateArg(4) and
+          source = getDelegateFlowSourceArg(m, 4) and
           sourceAp = AccessPath::empty() and
           sink = TCallableFlowSinkReturn() and
           sinkAp = AccessPath::element()
@@ -924,7 +924,7 @@ class IEnumerableFlow extends LibraryTypeDataFlow, RefType {
         sink = getDelegateFlowSinkArg(m, 1, 0) and
         sinkAp = AccessPath::empty()
         or
-        source = TCallableFlowSourceDelegateArg(1) and
+        source = getDelegateFlowSourceArg(m, 1) and
         sourceAp = AccessPath::empty() and
         sink = TCallableFlowSinkReturn() and
         sinkAp = AccessPath::element()
@@ -943,12 +943,12 @@ class IEnumerableFlow extends LibraryTypeDataFlow, RefType {
         sink = getDelegateFlowSinkArg(m, 2, 0) and
         sinkAp = AccessPath::empty()
         or
-        source = TCallableFlowSourceDelegateArg(1) and
+        source = getDelegateFlowSourceArg(m, 1) and
         sourceAp = AccessPath::element() and
         sink = getDelegateFlowSinkArg(m, 2, 1) and
         sinkAp = AccessPath::empty()
         or
-        source = TCallableFlowSourceDelegateArg(2) and
+        source = getDelegateFlowSourceArg(m, 2) and
         sourceAp = AccessPath::empty() and
         sink = TCallableFlowSinkReturn() and
         sinkAp = AccessPath::element()

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 `uniqueNodeLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    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

@@ -65,7 +65,9 @@ abstract class NodeImpl extends Node {
 
 private class ExprNodeImpl extends ExprNode, NodeImpl {
   override DataFlowCallable getEnclosingCallableImpl() {
-    result = this.getExpr().getEnclosingCallable()
+    result = this.getExpr().(CIL::Expr).getEnclosingCallable()
+    or
+    result = this.getControlFlowNodeImpl().getEnclosingCallable()
   }
 
   override DotNet::Type getTypeImpl() {
@@ -618,6 +620,7 @@ private predicate arrayRead(Expr e1, ArrayRead e2) { e1 = e2.getQualifier() }
 private Type getCSharpType(DotNet::Type t) {
   result = t
   or
+  not t instanceof Type and
   result.matchesHandle(t)
 }
 
@@ -688,7 +691,7 @@ private module Cached {
       not def.(Ssa::ExplicitDefinition).getADefinition() instanceof
         AssignableDefinitions::ImplicitParameterDefinition
     } or
-    TExplicitParameterNode(DotNet::Parameter p) { p.isUnboundDeclaration() } or
+    TExplicitParameterNode(DotNet::Parameter p) { p = any(DataFlowCallable c).getAParameter() } or
     TInstanceParameterNode(Callable c) {
       c.isUnboundDeclaration() and not c.(Modifiable).isStatic()
     } or
@@ -707,25 +710,28 @@ private module Cached {
     TObjectInitializerNode(ControlFlow::Nodes::ElementNode cfn) {
       cfn.getElement().(ObjectCreation).hasInitializer()
     } or
-    TExprPostUpdateNode(ControlFlow::Nodes::ElementNode cfn) {
-      exists(Argument a, Type t |
-        a = cfn.getElement() and
-        t = a.stripCasts().getType()
-      |
-        t instanceof RefType and
-        not t instanceof NullType
+    TExprPostUpdateNode(ControlFlow::Nodes::ExprNode cfn) {
+      exists(Expr e | e = cfn.getExpr() |
+        exists(Type t | t = e.(Argument).stripCasts().getType() |
+          t instanceof RefType and
+          not t instanceof NullType
+          or
+          t = any(TypeParameter tp | not tp.isValueType())
+        )
         or
-        t = any(TypeParameter tp | not tp.isValueType())
-      )
-      or
-      fieldOrPropertyStore(_, _, _, cfn.getElement(), true)
-      or
-      arrayStore(_, _, cfn.getElement(), true)
-      or
-      exists(TExprPostUpdateNode upd, FieldOrPropertyAccess fla |
-        upd = TExprPostUpdateNode(fla.getAControlFlowNode())
-      |
-        cfn.getElement() = fla.getQualifier()
+        fieldOrPropertyStore(_, _, _, e, true)
+        or
+        arrayStore(_, _, e, true)
+        or
+        // needed for reverse stores; e.g. `x.f1.f2 = y` induces
+        // a store step of `f1` into `x`
+        exists(TExprPostUpdateNode upd, Expr read |
+          upd = TExprPostUpdateNode(read.getAControlFlowNode())
+        |
+          fieldOrPropertyRead(e, _, read)
+          or
+          arrayRead(e, read)
+        )
       )
     } or
     TSummaryNode(FlowSummary::SummarizedCallable c, FlowSummaryImpl::Private::SummaryNodeState state) {
@@ -1436,7 +1442,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;
 

csharp/ql/lib/semmle/code/dotnet/Variable.qll

@@ -20,7 +20,7 @@ class Parameter extends Variable, @dotnet_parameter {
   /** Gets the position of this parameter, excluding the `this` parameter. */
   int getPosition() { this = this.getDeclaringElement().getParameter(result) }
 
-  /** Gets the callable defining this parameter. */
+  /** Gets the callable defining this parameter, if any. */
   Callable getCallable() { result = this.getDeclaringElement() }
 
   /** Gets the declaring `Parameterizable`. */

java/ql/lib/semmle/code/java/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 `uniqueNodeLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    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."
   }
 

python/ql/lib/semmle/python/dataflow/new/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 `uniqueNodeLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    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."
   }
 

ruby/ql/lib/codeql/ruby/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 `uniqueNodeLocation`. */
+    predicate uniqueNodeLocationExclude(Node n) { none() }
+
+    /** Holds if `n` should be excluded from the consistency test `missingLocation`. */
+    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."
   }