C#: Update dataflow consistency queries to cater for non unique post and pre unique update notes for conditional branches.

Author: michaelnebel

csharp/ql/consistency-queries/DataFlowConsistency.ql

@@ -35,13 +35,7 @@ private class MyConsistencyConfiguration extends ConsistencyConfiguration {
   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
-      )
+    not exists(getAPostUpdateNodeForArg(n.asExpr()))
     or
     n instanceof ImplicitCapturedArgumentNode
     or
@@ -50,5 +44,21 @@ private class MyConsistencyConfiguration extends ConsistencyConfiguration {
     n.asExpr() instanceof CIL::Expr
   }
 
+  override predicate postHasUniquePreExclude(PostUpdateNode n) {
+    exists(ControlFlow::Nodes::ExprNode e, ControlFlow::Nodes::ExprNode arg |
+      e = getAPostUpdateNodeForArg(arg.getExpr()) and
+      e != arg and
+      n = TExprPostUpdateNode(e)
+    )
+  }
+
+  override predicate uniquePostUpdateExclude(Node n) {
+    exists(ControlFlow::Nodes::ExprNode e, ControlFlow::Nodes::ExprNode arg |
+      e = getAPostUpdateNodeForArg(arg.getExpr()) and
+      e != arg and
+      n.asExpr() = arg.getExpr()
+    )
+  }
+
   override predicate reverseReadExclude(Node n) { n.asExpr() = any(AwaitExpr ae).getExpr() }
 }

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

@@ -197,7 +197,7 @@ private predicate relevantArgumentType(ControlFlow::Nodes::ExprNode cfn) {
 }
 
 /** Gets a node for which to construct a post-update node for argument `arg`. */
-private ControlFlow::Nodes::ExprNode getAPostUpdateNodeForArg(Argument arg) {
+ControlFlow::Nodes::ExprNode getAPostUpdateNodeForArg(Argument arg) {
   result = getALastEvalNode*(arg.getAControlFlowNode()) and
   relevantArgumentType(result) and
   not exists(getALastEvalNode(result))