C#: Rewrite predicates from using forall to using unique

This avoids generation of expensive anti-join predicates with Cartesian products.

Author: hvitved

csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll

@@ -1466,8 +1466,10 @@ module Internal {
         PreSsa::Definition def, AssignableRead read
       ) {
         read = def.getAFirstRead() and
-        not exists(AssignableRead other | PreSsa::adjacentReadPairSameVar(other, read) |
-          other != read
+        (
+          not PreSsa::adjacentReadPairSameVar(_, read)
+          or
+          read = unique(AssignableRead read0 | PreSsa::adjacentReadPairSameVar(read0, read))
         )
       }
 
@@ -1651,10 +1653,14 @@ module Internal {
         AssignableRead read1, AssignableRead read2
       ) {
         PreSsa::adjacentReadPairSameVar(read1, read2) and
-        not exists(AssignableRead other |
-          PreSsa::adjacentReadPairSameVar(other, read2) and
-          other != read1 and
-          other != read2
+        (
+          read1 = read2 and
+          read1 = unique(AssignableRead other | PreSsa::adjacentReadPairSameVar(other, read2))
+          or
+          read1 =
+            unique(AssignableRead other |
+              PreSsa::adjacentReadPairSameVar(other, read2) and other != read2
+            )
         )
       }
 
@@ -1887,10 +1893,14 @@ module Internal {
       Ssa::Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2
     ) {
       SsaImpl::adjacentReadPairSameVar(def, cfn1, cfn2) and
-      not exists(ControlFlow::Node other |
-        SsaImpl::adjacentReadPairSameVar(def, other, cfn2) and
-        other != cfn1 and
-        other != cfn2
+      (
+        cfn1 = cfn2 and
+        cfn1 = unique(ControlFlow::Node other | SsaImpl::adjacentReadPairSameVar(def, other, cfn2))
+        or
+        cfn1 =
+          unique(ControlFlow::Node other |
+            SsaImpl::adjacentReadPairSameVar(def, other, cfn2) and other != cfn2
+          )
       )
     }
 

csharp/ql/src/semmle/code/csharp/controlflow/internal/pressa/SsaImplSpecific.qll

@@ -15,13 +15,37 @@ class ExitBasicBlock extends BasicBlock {
   ExitBasicBlock() { scopeLast(_, this.getLastElement(), _) }
 }
 
-pragma[noinline]
+/** Holds if `a` is assigned in non-constructor callable `c`. */
+pragma[nomagic]
+private predicate assignableDefinition(Assignable a, Callable c) {
+  exists(AssignableDefinition def | def.getTarget() = a |
+    c = def.getEnclosingCallable() and
+    not c instanceof Constructor
+  )
+}
+
+/** Holds if `a` is accessed in callable `c`. */
+pragma[nomagic]
+private predicate assignableAccess(Assignable a, Callable c) {
+  exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable())
+}
+
+pragma[nomagic]
 private predicate assignableNoCapturing(Assignable a, Callable c) {
-  exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable()) and
-  forall(AssignableDefinition def | def.getTarget() = a |
-    c = def.getEnclosingCallable()
+  assignableAccess(a, c) and
+  /*
+   * The code below is equivalent to
+   * ```ql
+   * not exists(Callable other | assignableDefinition(a, other) | other != c)
+   * ```
+   * but it avoids a Cartesian product in the compiler generated antijoin
+   * predicate.
+   */
+
+  (
+    not assignableDefinition(a, _)
     or
-    def.getEnclosingCallable() instanceof Constructor
+    c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
   )
 }
 
@@ -41,7 +65,7 @@ class SourceVariable extends Assignable {
     (
       this instanceof LocalScopeVariable
       or
-      this instanceof Field
+      this = any(Field f | not f.isVolatile())
       or
       this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
     ) and