From 3939eff26067cd429c9429406026fa24248a61c3 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 15:00:05 +0100
Subject: [PATCH 01/12] TypeFlow: Rename step to uniqStep.

---
 .../semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll  |  4 ++--
 java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll     |  4 ++--
 shared/typeflow/codeql/typeflow/TypeFlow.qll           |  2 +-
 .../typeflow/codeql/typeflow/internal/TypeFlowImpl.qll | 10 +++++-----
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll
index 69f94dad91b6..55d1a0d2c7e9 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll
@@ -199,7 +199,7 @@ private module Input implements TypeFlowInput<Location> {
     i2.(PointerArithmeticInstruction).getLeft() = i1
   }
 
-  predicate step(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) {
     instructionStep(n1.asInstruction(), n2.asInstruction())
   }
 
@@ -246,7 +246,7 @@ private module Input implements TypeFlowInput<Location> {
   pragma[nomagic]
   private predicate upcastCand(TypeFlowNode n, Type t1, Type t2) {
     exists(TypeFlowNode next |
-      step(n, next)
+      uniqStep(n, next)
       or
       joinStep(n, next)
     |
diff --git a/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll b/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
index 0c37215de78d..da17d5ff5b7b 100644
--- a/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
@@ -118,7 +118,7 @@ private module Input implements TypeFlowInput<Location> {
    * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
    * functionally determined by `n2`.
    */
-  predicate step(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) {
     n2.asExpr() = n1.asField().getAnAccess()
     or
     n2.asExpr() = n1.asSsa().getAUse()
@@ -169,7 +169,7 @@ private module Input implements TypeFlowInput<Location> {
    */
   pragma[nomagic]
   private predicate upcastCand(TypeFlowNode n, RefType t1, RefType t1e, RefType t2, RefType t2e) {
-    exists(TypeFlowNode next | step(n, next) or joinStep(n, next) |
+    exists(TypeFlowNode next | uniqStep(n, next) or joinStep(n, next) |
       n.getType() = t1 and
       next.getType() = t2 and
       t1.getErasure() = t1e and
diff --git a/shared/typeflow/codeql/typeflow/TypeFlow.qll b/shared/typeflow/codeql/typeflow/TypeFlow.qll
index 7518805ac56f..a447bc7fb8f9 100644
--- a/shared/typeflow/codeql/typeflow/TypeFlow.qll
+++ b/shared/typeflow/codeql/typeflow/TypeFlow.qll
@@ -37,7 +37,7 @@ signature module TypeFlowInput<LocationSig Location> {
    * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
    * functionally determined by `n2`.
    */
-  predicate step(TypeFlowNode n1, TypeFlowNode n2);
+  predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2);
 
   /** Holds if `n` represents a `null` value. */
   predicate isNullValue(TypeFlowNode n);
diff --git a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
index ac7de53f85aa..15084402990b 100644
--- a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
+++ b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
@@ -9,7 +9,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   predicate isNull(TypeFlowNode n) {
     isNullValue(n)
     or
-    exists(TypeFlowNode mid | isNull(mid) and step(mid, n))
+    exists(TypeFlowNode mid | isNull(mid) and uniqStep(mid, n))
     or
     forex(TypeFlowNode mid | joinStep(mid, n) | isNull(mid)) and
     not isExcludedFromNullAnalysis(n)
@@ -24,7 +24,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   }
 
   private predicate anyStep(TypeFlowNode n1, TypeFlowNode n2) {
-    joinStepNotNull(n1, n2) or step(n1, n2)
+    joinStepNotNull(n1, n2) or uniqStep(n1, n2)
   }
 
   private predicate sccEdge(TypeFlowNode n1, TypeFlowNode n2) {
@@ -171,7 +171,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private predicate exactType(TypeFlowNode n, Type t) {
     exactTypeBase(n, t)
     or
-    exists(TypeFlowNode mid | exactType(mid, t) and step(mid, n))
+    exists(TypeFlowNode mid | exactType(mid, t) and uniqStep(mid, n))
     or
     // The following is an optimized version of
     // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | exactType(mid, t))`
@@ -234,7 +234,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private predicate typeFlow(TypeFlowNode n, Type t) {
     typeFlowBase(n, t)
     or
-    exists(TypeFlowNode mid | typeFlow(mid, t) and step(mid, n))
+    exists(TypeFlowNode mid | typeFlow(mid, t) and uniqStep(mid, n))
     or
     ForAll<TypeFlowNode, RankedJoinStep, TypeFlowPropagation>::flowJoin(n, t)
     or
@@ -366,7 +366,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
         ForAll<TypeFlowScc, RankedSccJoinStep, HasUnionTypePropagation>::flowJoin(scc, _)
       )
       or
-      exists(TypeFlowNode mid | step(mid, n) and hasUnionTypeFlow(mid))
+      exists(TypeFlowNode mid | uniqStep(mid, n) and hasUnionTypeFlow(mid))
       or
       instanceofDisjunctionGuarded(n, _)
     )

From fba4d09e65400ed588ea3cd2e233bb3d0a8c09b8 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 15:09:09 +0100
Subject: [PATCH 02/12] TypeFlow: Simplify interface.

---
 .../code/cpp/ir/dataflow/internal/TypeFlow.qll  | 14 ++++----------
 .../lib/semmle/code/java/dataflow/TypeFlow.qll  | 17 ++++++-----------
 shared/typeflow/codeql/typeflow/TypeFlow.qll    | 13 ++++---------
 .../codeql/typeflow/internal/TypeFlowImpl.qll   | 14 +++++++++++++-
 4 files changed, 27 insertions(+), 31 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll
index 55d1a0d2c7e9..41e30e2902b1 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll
@@ -159,7 +159,7 @@ private module Input implements TypeFlowInput<Location> {
     )
   }
 
-  predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate step(TypeFlowNode n1, TypeFlowNode n2) {
     // instruction -> phi
     getAnUltimateLocalDefinition(n2.asInstruction()) = n1.asInstruction()
     or
@@ -179,6 +179,8 @@ private module Input implements TypeFlowInput<Location> {
       n1.asInstruction() = arg and
       n2.asInstruction() = p
     )
+    or
+    instructionStep(n1.asInstruction(), n2.asInstruction())
   }
 
   /**
@@ -199,10 +201,6 @@ private module Input implements TypeFlowInput<Location> {
     i2.(PointerArithmeticInstruction).getLeft() = i1
   }
 
-  predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) {
-    instructionStep(n1.asInstruction(), n2.asInstruction())
-  }
-
   predicate isNullValue(TypeFlowNode n) { n.isNullValue() }
 
   private newtype TType =
@@ -245,11 +243,7 @@ private module Input implements TypeFlowInput<Location> {
 
   pragma[nomagic]
   private predicate upcastCand(TypeFlowNode n, Type t1, Type t2) {
-    exists(TypeFlowNode next |
-      uniqStep(n, next)
-      or
-      joinStep(n, next)
-    |
+    exists(TypeFlowNode next | step(n, next) |
       n.getType() = t1 and
       next.getType() = t2 and
       t1 != t2
diff --git a/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll b/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
index da17d5ff5b7b..7b6e4e725af3 100644
--- a/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
@@ -84,10 +84,11 @@ private module Input implements TypeFlowInput<Location> {
   }
 
   /**
-   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
-   * necessarily functionally determined by `n2`.
+   * Holds if data can flow from `n1` to `n2` in one step.
+   *
+   * For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
    */
-  predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate step(TypeFlowNode n1, TypeFlowNode n2) {
     n2.asExpr().(ChooseExpr).getAResultExpr() = n1.asExpr()
     or
     exists(Field f, Expr e |
@@ -112,13 +113,7 @@ private module Input implements TypeFlowInput<Location> {
       // skip trivial recursion
       not arg = n2.asSsa().getAUse()
     )
-  }
-
-  /**
-   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
-   * functionally determined by `n2`.
-   */
-  predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) {
+    or
     n2.asExpr() = n1.asField().getAnAccess()
     or
     n2.asExpr() = n1.asSsa().getAUse()
@@ -169,7 +164,7 @@ private module Input implements TypeFlowInput<Location> {
    */
   pragma[nomagic]
   private predicate upcastCand(TypeFlowNode n, RefType t1, RefType t1e, RefType t2, RefType t2e) {
-    exists(TypeFlowNode next | uniqStep(n, next) or joinStep(n, next) |
+    exists(TypeFlowNode next | step(n, next) |
       n.getType() = t1 and
       next.getType() = t2 and
       t1.getErasure() = t1e and
diff --git a/shared/typeflow/codeql/typeflow/TypeFlow.qll b/shared/typeflow/codeql/typeflow/TypeFlow.qll
index a447bc7fb8f9..a2ae213ecb7f 100644
--- a/shared/typeflow/codeql/typeflow/TypeFlow.qll
+++ b/shared/typeflow/codeql/typeflow/TypeFlow.qll
@@ -28,16 +28,11 @@ signature module TypeFlowInput<LocationSig Location> {
   }
 
   /**
-   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
-   * necessarily functionally determined by `n2`.
-   */
-  predicate joinStep(TypeFlowNode n1, TypeFlowNode n2);
-
-  /**
-   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
-   * functionally determined by `n2`.
+   * Holds if data can flow from `n1` to `n2` in one step.
+   *
+   * For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
    */
-  predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2);
+  predicate step(TypeFlowNode n1, TypeFlowNode n2);
 
   /** Holds if `n` represents a `null` value. */
   predicate isNullValue(TypeFlowNode n);
diff --git a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
index 15084402990b..5913e9d6ffe7 100644
--- a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
+++ b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
@@ -5,8 +5,20 @@ private import codeql.util.Unit
 module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private import I
 
+  /**
+   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
+   * functionally determined by `n2`.
+   */
+  private predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) { n1 = unique(TypeFlowNode n | step(n, n2)) }
+
+  /**
+   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
+   * functionally determined by `n2`.
+   */
+  private predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) { step(n1, n2) and not uniqStep(n1, n2) }
+
   /** Holds if `null` is the only value that flows to `n`. */
-  predicate isNull(TypeFlowNode n) {
+  private predicate isNull(TypeFlowNode n) {
     isNullValue(n)
     or
     exists(TypeFlowNode mid | isNull(mid) and uniqStep(mid, n))

From ea458c09a0341e7d08122b1f4d9d0165dba24b5e Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 15:48:29 +0100
Subject: [PATCH 03/12] TypeFlow: Extract a universal flow library abstraction
 from TypeFlow.

---
 .../codeql/typeflow/internal/TypeFlowImpl.qll | 226 ++++++++++++------
 1 file changed, 154 insertions(+), 72 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
index 5913e9d6ffe7..1a29581ea0d8 100644
--- a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
+++ b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
@@ -2,7 +2,37 @@ private import codeql.typeflow.TypeFlow
 private import codeql.util.Location
 private import codeql.util.Unit
 
-module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
+signature module UniversalFlowInput<LocationSig Location> {
+  /**
+   * A node for which certain data flow properties may be proved. For example,
+   * expressions and method declarations.
+   */
+  class TypeFlowNode {
+    /** Gets a textual representation of this node. */
+    string toString();
+
+    /** Gets the location of this node. */
+    Location getLocation();
+  }
+
+  /**
+   * Holds if data can flow from `n1` to `n2` in one step.
+   *
+   * For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
+   */
+  predicate step(TypeFlowNode n1, TypeFlowNode n2);
+
+  /** Holds if `n` represents a `null` value. */
+  predicate isNullValue(TypeFlowNode n);
+
+  /**
+   * Holds if `n` should be excluded from the set of null values even if
+   * the null analysis determines that `n` is always null.
+   */
+  default predicate isExcludedFromNullAnalysis(TypeFlowNode n) { none() }
+}
+
+module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   private import I
 
   /**
@@ -31,11 +61,11 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
    * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
    * functionally determined by `n2`, and `n1` might take a non-null value.
    */
-  private predicate joinStepNotNull(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate joinStepNotNull(TypeFlowNode n1, TypeFlowNode n2) {
     joinStep(n1, n2) and not isNull(n1)
   }
 
-  private predicate anyStep(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate anyStep(TypeFlowNode n1, TypeFlowNode n2) {
     joinStepNotNull(n1, n2) or uniqStep(n1, n2)
   }
 
@@ -168,34 +198,117 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
 
   private module RankedSccJoinStep = RankEdge<SccJoinStep>;
 
-  private module ExactTypePropagation implements TypePropagation {
-    class Typ = Type;
+  signature module NullaryPropertySig {
+    predicate hasPropertyBase(TypeFlowNode n);
+
+    default predicate barrier(TypeFlowNode n) { none() }
+  }
+
+  module FlowNullary<NullaryPropertySig P> {
+    private module Propagation implements TypePropagation {
+      class Typ = Unit;
 
-    predicate candType = exactType/2;
+      predicate candType(TypeFlowNode n, Unit u) { hasProperty(n) and exists(u) }
 
-    predicate supportsType = exactType/2;
+      predicate supportsType = candType/2;
+    }
+
+    predicate hasProperty(TypeFlowNode n) {
+      P::hasPropertyBase(n)
+      or
+      not P::barrier(n) and
+      (
+        exists(TypeFlowNode mid | hasProperty(mid) and uniqStep(mid, n))
+        or
+        // The following is an optimized version of
+        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
+        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, _)
+        or
+        exists(TypeFlowScc scc |
+          sccRepr(n, scc) and
+          // Optimized version of
+          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
+          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, _)
+        )
+      )
+    }
+  }
+
+  signature module PropertySig {
+    class Prop;
+
+    bindingset[t1, t2]
+    default predicate propImplies(Prop t1, Prop t2) { t1 = t2 }
+
+    predicate hasPropertyBase(TypeFlowNode n, Prop t);
+
+    default predicate barrier(TypeFlowNode n) { none() }
+  }
+
+  module Flow<PropertySig P> {
+    private module Propagation implements TypePropagation {
+      class Typ = P::Prop;
+
+      predicate candType = hasProperty/2;
+
+      bindingset[t]
+      predicate supportsType(TypeFlowNode n, Typ t) {
+        exists(Typ t0 | hasProperty(n, t0) and P::propImplies(t0, t))
+      }
+    }
+
+    /**
+     * Holds if the runtime type of `n` is exactly `t` and if this bound is a
+     * non-trivial lower bound, that is, `t` has a subtype.
+     */
+    predicate hasProperty(TypeFlowNode n, P::Prop t) {
+      P::hasPropertyBase(n, t)
+      or
+      not P::barrier(n) and
+      (
+        exists(TypeFlowNode mid | hasProperty(mid, t) and uniqStep(mid, n))
+        or
+        // The following is an optimized version of
+        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
+        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, t)
+        or
+        exists(TypeFlowScc scc |
+          sccRepr(n, scc) and
+          // Optimized version of
+          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
+          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, t)
+        )
+      )
+    }
+  }
+}
+
+module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
+  private import I
+
+  private module UfInput implements UniversalFlowInput<Location> {
+    class TypeFlowNode = I::TypeFlowNode;
+
+    predicate step = I::step/2;
+
+    predicate isNullValue = I::isNullValue/1;
+
+    predicate isExcludedFromNullAnalysis = I::isExcludedFromNullAnalysis/1;
+  }
+
+  private module UnivFlow = UfMake<Location, UfInput>;
+
+  private module ExactTypeProperty implements UnivFlow::PropertySig {
+    class Prop = Type;
+
+    predicate hasPropertyBase = exactTypeBase/2;
   }
 
   /**
    * Holds if the runtime type of `n` is exactly `t` and if this bound is a
    * non-trivial lower bound, that is, `t` has a subtype.
    */
-  private predicate exactType(TypeFlowNode n, Type t) {
-    exactTypeBase(n, t)
-    or
-    exists(TypeFlowNode mid | exactType(mid, t) and uniqStep(mid, n))
-    or
-    // The following is an optimized version of
-    // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | exactType(mid, t))`
-    ForAll<TypeFlowNode, RankedJoinStep, ExactTypePropagation>::flowJoin(n, t)
-    or
-    exists(TypeFlowScc scc |
-      sccRepr(n, scc) and
-      // Optimized version of
-      // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | exactType(mid, t))`
-      ForAll<TypeFlowScc, RankedSccJoinStep, ExactTypePropagation>::flowJoin(scc, t)
-    )
-  }
+  private predicate exactType = UnivFlow::Flow<ExactTypeProperty>::hasProperty/2;
 
   /**
    * Gets the source declaration of a direct supertype of this type, excluding itself.
@@ -226,17 +339,13 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
     )
   }
 
-  private module TypeFlowPropagation implements TypePropagation {
-    class Typ = Type;
+  private module TypeFlowProperty implements UnivFlow::PropertySig {
+    class Prop = Type;
 
-    predicate candType = typeFlow/2;
+    bindingset[t1, t2]
+    predicate propImplies(Type t1, Type t2) { getAnAncestor(pragma[only_bind_out](t1)) = t2 }
 
-    bindingset[t]
-    predicate supportsType(TypeFlowNode mid, Type t) {
-      exists(Type midtyp | exactType(mid, midtyp) or typeFlow(mid, midtyp) |
-        getAnAncestor(pragma[only_bind_out](midtyp)) = t
-      )
-    }
+    predicate hasPropertyBase(TypeFlowNode n, Prop t) { typeFlowBase(n, t) or exactType(n, t) }
   }
 
   /**
@@ -244,16 +353,8 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
    * likely to be better than the static type of `n`.
    */
   private predicate typeFlow(TypeFlowNode n, Type t) {
-    typeFlowBase(n, t)
-    or
-    exists(TypeFlowNode mid | typeFlow(mid, t) and uniqStep(mid, n))
-    or
-    ForAll<TypeFlowNode, RankedJoinStep, TypeFlowPropagation>::flowJoin(n, t)
-    or
-    exists(TypeFlowScc scc |
-      sccRepr(n, scc) and
-      ForAll<TypeFlowScc, RankedSccJoinStep, TypeFlowPropagation>::flowJoin(scc, t)
-    )
+    UnivFlow::Flow<TypeFlowProperty>::hasProperty(n, t) and
+    not exactType(n, t)
   }
 
   pragma[nomagic]
@@ -341,22 +442,20 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
    */
   private predicate unionTypeFlowBaseCand(TypeFlowNode n, Type t, boolean exact) {
     exists(TypeFlowNode next |
-      joinStepNotNull(n, next) and
+      UnivFlow::joinStepNotNull(n, next) and
       bestTypeFlowOrTypeFlowBase(n, t, exact) and
       not bestTypeFlowOrTypeFlowBase(next, t, exact) and
       not exactType(next, _)
     )
   }
 
-  private module HasUnionTypePropagation implements TypePropagation {
-    class Typ = Unit;
-
-    predicate candType(TypeFlowNode mid, Unit unit) {
-      exists(unit) and
-      (unionTypeFlowBaseCand(mid, _, _) or hasUnionTypeFlow(mid))
+  module UnionTypeFlowProperty implements UnivFlow::NullaryPropertySig {
+    predicate hasPropertyBase(TypeFlowNode n) {
+      unionTypeFlowBaseCand(n, _, _) or
+      instanceofDisjunctionGuarded(n, _)
     }
 
-    predicate supportsType = candType/2;
+    predicate barrier(TypeFlowNode n) { exactType(n, _) }
   }
 
   /**
@@ -364,25 +463,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
    * `unionTypeFlowBaseCand`, such that we can compute a union type bound for `n`.
    * Disregards nodes for which we have an exact bound.
    */
-  private predicate hasUnionTypeFlow(TypeFlowNode n) {
-    not exactType(n, _) and
-    (
-      // Optimized version of
-      // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | unionTypeFlowBaseCand(mid, _, _) or hasUnionTypeFlow(mid))`
-      ForAll<TypeFlowNode, RankedJoinStep, HasUnionTypePropagation>::flowJoin(n, _)
-      or
-      exists(TypeFlowScc scc |
-        sccRepr(n, scc) and
-        // Optimized version of
-        // `forex(TypeFlowNode mid | sccJoinStep(mid, scc) | unionTypeFlowBaseCand(mid, _, _) or hasUnionTypeFlow(mid))`
-        ForAll<TypeFlowScc, RankedSccJoinStep, HasUnionTypePropagation>::flowJoin(scc, _)
-      )
-      or
-      exists(TypeFlowNode mid | uniqStep(mid, n) and hasUnionTypeFlow(mid))
-      or
-      instanceofDisjunctionGuarded(n, _)
-    )
-  }
+  private predicate hasUnionTypeFlow = UnivFlow::FlowNullary<UnionTypeFlowProperty>::hasProperty/1;
 
   pragma[nomagic]
   private Type getTypeBound(TypeFlowNode n) {
@@ -395,9 +476,9 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private predicate unionTypeFlow0(TypeFlowNode n, Type t, boolean exact) {
     hasUnionTypeFlow(n) and
     (
-      exists(TypeFlowNode mid | anyStep(mid, n) |
-        unionTypeFlowBaseCand(mid, t, exact) or unionTypeFlow(mid, t, exact)
-      )
+      exists(TypeFlowNode mid | UnivFlow::anyStep(mid, n) | unionTypeFlow(mid, t, exact))
+      or
+      unionTypeFlowBaseCand(n, t, exact)
       or
       instanceofDisjunctionGuarded(n, t) and exact = false
     )
@@ -482,6 +563,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
    */
   predicate bestUnionType(TypeFlowNode n, Type t, boolean exact) {
     unionTypeFlow(n, t, exact) and
+    not exactType(n, _) and
     not irrelevantUnionType(n) and
     not irrelevantUnionTypePart(n, t, exact)
   }

From 1aecdb44dc66a2fcc4ad749fd111f261ac4e95fb Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 16:20:16 +0100
Subject: [PATCH 04/12] UniversalFlow: Move Universal Flow library to its own
 file.

---
 .../codeql/typeflow/UniversalFlow.qll         | 284 ++++++++++++++++++
 .../codeql/typeflow/internal/TypeFlowImpl.qll | 282 +----------------
 2 files changed, 285 insertions(+), 281 deletions(-)
 create mode 100644 shared/typeflow/codeql/typeflow/UniversalFlow.qll

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
new file mode 100644
index 000000000000..7aa07e0a59c7
--- /dev/null
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -0,0 +1,284 @@
+private import codeql.util.Location
+private import codeql.util.Unit
+
+/** Provides the input specification. */
+signature module UniversalFlowInput<LocationSig Location> {
+  /**
+   * A node for which certain data flow properties may be proved. For example,
+   * expressions and method declarations.
+   */
+  class TypeFlowNode {
+    /** Gets a textual representation of this node. */
+    string toString();
+
+    /** Gets the location of this node. */
+    Location getLocation();
+  }
+
+  /**
+   * Holds if data can flow from `n1` to `n2` in one step.
+   *
+   * For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
+   */
+  predicate step(TypeFlowNode n1, TypeFlowNode n2);
+
+  /** Holds if `n` represents a `null` value. */
+  predicate isNullValue(TypeFlowNode n);
+
+  /**
+   * Holds if `n` should be excluded from the set of null values even if
+   * the null analysis determines that `n` is always null.
+   */
+  default predicate isExcludedFromNullAnalysis(TypeFlowNode n) { none() }
+}
+
+module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
+  private import I
+
+  /**
+   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
+   * functionally determined by `n2`.
+   */
+  private predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) { n1 = unique(TypeFlowNode n | step(n, n2)) }
+
+  /**
+   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
+   * functionally determined by `n2`.
+   */
+  private predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) { step(n1, n2) and not uniqStep(n1, n2) }
+
+  /** Holds if `null` is the only value that flows to `n`. */
+  private predicate isNull(TypeFlowNode n) {
+    isNullValue(n)
+    or
+    exists(TypeFlowNode mid | isNull(mid) and uniqStep(mid, n))
+    or
+    forex(TypeFlowNode mid | joinStep(mid, n) | isNull(mid)) and
+    not isExcludedFromNullAnalysis(n)
+  }
+
+  /**
+   * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
+   * functionally determined by `n2`, and `n1` might take a non-null value.
+   */
+  predicate joinStepNotNull(TypeFlowNode n1, TypeFlowNode n2) {
+    joinStep(n1, n2) and not isNull(n1)
+  }
+
+  predicate anyStep(TypeFlowNode n1, TypeFlowNode n2) {
+    joinStepNotNull(n1, n2) or uniqStep(n1, n2)
+  }
+
+  private predicate sccEdge(TypeFlowNode n1, TypeFlowNode n2) {
+    anyStep(n1, n2) and anyStep+(n2, n1)
+  }
+
+  private module Scc = QlBuiltins::EquivalenceRelation<TypeFlowNode, sccEdge/2>;
+
+  private class TypeFlowScc = Scc::EquivalenceClass;
+
+  /** Holds if `n` is part of an SCC of size 2 or more represented by `scc`. */
+  private predicate sccRepr(TypeFlowNode n, TypeFlowScc scc) { scc = Scc::getEquivalenceClass(n) }
+
+  private predicate sccJoinStepNotNull(TypeFlowNode n, TypeFlowScc scc) {
+    exists(TypeFlowNode mid |
+      joinStepNotNull(n, mid) and
+      sccRepr(mid, scc) and
+      not sccRepr(n, scc)
+    )
+  }
+
+  private signature class NodeSig;
+
+  private signature module Edge {
+    class Node;
+
+    predicate edge(TypeFlowNode n1, Node n2);
+  }
+
+  private signature module RankedEdge<NodeSig Node> {
+    predicate edgeRank(int r, TypeFlowNode n1, Node n2);
+
+    int lastRank(Node n);
+  }
+
+  private module RankEdge<Edge E> implements RankedEdge<E::Node> {
+    private import E
+
+    /**
+     * Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. The used
+     * ordering is not necessarily total, so the ranking may have gaps.
+     */
+    private predicate edgeRank1(int r, TypeFlowNode n1, Node n2) {
+      n1 =
+        rank[r](TypeFlowNode n, int startline, int startcolumn |
+          edge(n, n2) and
+          n.getLocation().hasLocationInfo(_, startline, startcolumn, _, _)
+        |
+          n order by startline, startcolumn
+        )
+    }
+
+    /**
+     * Holds if `r2` is a ranking of the ranks from `edgeRank1`. This removes the
+     * gaps from the ranking.
+     */
+    private predicate edgeRank2(int r2, int r1, Node n) {
+      r1 = rank[r2](int r | edgeRank1(r, _, n) | r)
+    }
+
+    /** Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. */
+    predicate edgeRank(int r, TypeFlowNode n1, Node n2) {
+      exists(int r1 |
+        edgeRank1(r1, n1, n2) and
+        edgeRank2(r, r1, n2)
+      )
+    }
+
+    int lastRank(Node n) { result = max(int r | edgeRank(r, _, n)) }
+  }
+
+  private signature module TypePropagation {
+    class Typ;
+
+    predicate candType(TypeFlowNode n, Typ t);
+
+    bindingset[t]
+    predicate supportsType(TypeFlowNode n, Typ t);
+  }
+
+  /** Implements recursion through `forall` by way of edge ranking. */
+  private module ForAll<NodeSig Node, RankedEdge<Node> E, TypePropagation T> {
+    /**
+     * Holds if `t` is a bound that holds on one of the incoming edges to `n` and
+     * thus is a candidate bound for `n`.
+     */
+    pragma[nomagic]
+    private predicate candJoinType(Node n, T::Typ t) {
+      exists(TypeFlowNode mid |
+        T::candType(mid, t) and
+        E::edgeRank(_, mid, n)
+      )
+    }
+
+    /**
+     * Holds if `t` is a candidate bound for `n` that is also valid for data coming
+     * through the edges into `n` ranked from `1` to `r`.
+     */
+    private predicate flowJoin(int r, Node n, T::Typ t) {
+      (
+        r = 1 and candJoinType(n, t)
+        or
+        flowJoin(r - 1, n, t) and E::edgeRank(r, _, n)
+      ) and
+      forall(TypeFlowNode mid | E::edgeRank(r, mid, n) | T::supportsType(mid, t))
+    }
+
+    /**
+     * Holds if `t` is a candidate bound for `n` that is also valid for data
+     * coming through all the incoming edges, and therefore is a valid bound for
+     * `n`.
+     */
+    predicate flowJoin(Node n, T::Typ t) { flowJoin(E::lastRank(n), n, t) }
+  }
+
+  private module JoinStep implements Edge {
+    class Node = TypeFlowNode;
+
+    predicate edge = joinStepNotNull/2;
+  }
+
+  private module SccJoinStep implements Edge {
+    class Node = TypeFlowScc;
+
+    predicate edge = sccJoinStepNotNull/2;
+  }
+
+  private module RankedJoinStep = RankEdge<JoinStep>;
+
+  private module RankedSccJoinStep = RankEdge<SccJoinStep>;
+
+  signature module NullaryPropertySig {
+    predicate hasPropertyBase(TypeFlowNode n);
+
+    default predicate barrier(TypeFlowNode n) { none() }
+  }
+
+  module FlowNullary<NullaryPropertySig P> {
+    private module Propagation implements TypePropagation {
+      class Typ = Unit;
+
+      predicate candType(TypeFlowNode n, Unit u) { hasProperty(n) and exists(u) }
+
+      predicate supportsType = candType/2;
+    }
+
+    predicate hasProperty(TypeFlowNode n) {
+      P::hasPropertyBase(n)
+      or
+      not P::barrier(n) and
+      (
+        exists(TypeFlowNode mid | hasProperty(mid) and uniqStep(mid, n))
+        or
+        // The following is an optimized version of
+        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
+        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, _)
+        or
+        exists(TypeFlowScc scc |
+          sccRepr(n, scc) and
+          // Optimized version of
+          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
+          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, _)
+        )
+      )
+    }
+  }
+
+  signature module PropertySig {
+    class Prop;
+
+    bindingset[t1, t2]
+    default predicate propImplies(Prop t1, Prop t2) { t1 = t2 }
+
+    predicate hasPropertyBase(TypeFlowNode n, Prop t);
+
+    default predicate barrier(TypeFlowNode n) { none() }
+  }
+
+  module Flow<PropertySig P> {
+    private module Propagation implements TypePropagation {
+      class Typ = P::Prop;
+
+      predicate candType = hasProperty/2;
+
+      bindingset[t]
+      predicate supportsType(TypeFlowNode n, Typ t) {
+        exists(Typ t0 | hasProperty(n, t0) and P::propImplies(t0, t))
+      }
+    }
+
+    /**
+     * Holds if the runtime type of `n` is exactly `t` and if this bound is a
+     * non-trivial lower bound, that is, `t` has a subtype.
+     */
+    predicate hasProperty(TypeFlowNode n, P::Prop t) {
+      P::hasPropertyBase(n, t)
+      or
+      not P::barrier(n) and
+      (
+        exists(TypeFlowNode mid | hasProperty(mid, t) and uniqStep(mid, n))
+        or
+        // The following is an optimized version of
+        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
+        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, t)
+        or
+        exists(TypeFlowScc scc |
+          sccRepr(n, scc) and
+          // Optimized version of
+          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
+          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, t)
+        )
+      )
+    }
+  }
+}
\ No newline at end of file
diff --git a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
index 1a29581ea0d8..eb4a30ef305f 100644
--- a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
+++ b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
@@ -1,288 +1,8 @@
 private import codeql.typeflow.TypeFlow
+private import codeql.typeflow.UniversalFlow
 private import codeql.util.Location
 private import codeql.util.Unit
 
-signature module UniversalFlowInput<LocationSig Location> {
-  /**
-   * A node for which certain data flow properties may be proved. For example,
-   * expressions and method declarations.
-   */
-  class TypeFlowNode {
-    /** Gets a textual representation of this node. */
-    string toString();
-
-    /** Gets the location of this node. */
-    Location getLocation();
-  }
-
-  /**
-   * Holds if data can flow from `n1` to `n2` in one step.
-   *
-   * For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
-   */
-  predicate step(TypeFlowNode n1, TypeFlowNode n2);
-
-  /** Holds if `n` represents a `null` value. */
-  predicate isNullValue(TypeFlowNode n);
-
-  /**
-   * Holds if `n` should be excluded from the set of null values even if
-   * the null analysis determines that `n` is always null.
-   */
-  default predicate isExcludedFromNullAnalysis(TypeFlowNode n) { none() }
-}
-
-module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
-  private import I
-
-  /**
-   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
-   * functionally determined by `n2`.
-   */
-  private predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) { n1 = unique(TypeFlowNode n | step(n, n2)) }
-
-  /**
-   * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
-   * functionally determined by `n2`.
-   */
-  private predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) { step(n1, n2) and not uniqStep(n1, n2) }
-
-  /** Holds if `null` is the only value that flows to `n`. */
-  private predicate isNull(TypeFlowNode n) {
-    isNullValue(n)
-    or
-    exists(TypeFlowNode mid | isNull(mid) and uniqStep(mid, n))
-    or
-    forex(TypeFlowNode mid | joinStep(mid, n) | isNull(mid)) and
-    not isExcludedFromNullAnalysis(n)
-  }
-
-  /**
-   * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
-   * functionally determined by `n2`, and `n1` might take a non-null value.
-   */
-  predicate joinStepNotNull(TypeFlowNode n1, TypeFlowNode n2) {
-    joinStep(n1, n2) and not isNull(n1)
-  }
-
-  predicate anyStep(TypeFlowNode n1, TypeFlowNode n2) {
-    joinStepNotNull(n1, n2) or uniqStep(n1, n2)
-  }
-
-  private predicate sccEdge(TypeFlowNode n1, TypeFlowNode n2) {
-    anyStep(n1, n2) and anyStep+(n2, n1)
-  }
-
-  private module Scc = QlBuiltins::EquivalenceRelation<TypeFlowNode, sccEdge/2>;
-
-  private class TypeFlowScc = Scc::EquivalenceClass;
-
-  /** Holds if `n` is part of an SCC of size 2 or more represented by `scc`. */
-  private predicate sccRepr(TypeFlowNode n, TypeFlowScc scc) { scc = Scc::getEquivalenceClass(n) }
-
-  private predicate sccJoinStepNotNull(TypeFlowNode n, TypeFlowScc scc) {
-    exists(TypeFlowNode mid |
-      joinStepNotNull(n, mid) and
-      sccRepr(mid, scc) and
-      not sccRepr(n, scc)
-    )
-  }
-
-  private signature class NodeSig;
-
-  private signature module Edge {
-    class Node;
-
-    predicate edge(TypeFlowNode n1, Node n2);
-  }
-
-  private signature module RankedEdge<NodeSig Node> {
-    predicate edgeRank(int r, TypeFlowNode n1, Node n2);
-
-    int lastRank(Node n);
-  }
-
-  private module RankEdge<Edge E> implements RankedEdge<E::Node> {
-    private import E
-
-    /**
-     * Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. The used
-     * ordering is not necessarily total, so the ranking may have gaps.
-     */
-    private predicate edgeRank1(int r, TypeFlowNode n1, Node n2) {
-      n1 =
-        rank[r](TypeFlowNode n, int startline, int startcolumn |
-          edge(n, n2) and
-          n.getLocation().hasLocationInfo(_, startline, startcolumn, _, _)
-        |
-          n order by startline, startcolumn
-        )
-    }
-
-    /**
-     * Holds if `r2` is a ranking of the ranks from `edgeRank1`. This removes the
-     * gaps from the ranking.
-     */
-    private predicate edgeRank2(int r2, int r1, Node n) {
-      r1 = rank[r2](int r | edgeRank1(r, _, n) | r)
-    }
-
-    /** Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. */
-    predicate edgeRank(int r, TypeFlowNode n1, Node n2) {
-      exists(int r1 |
-        edgeRank1(r1, n1, n2) and
-        edgeRank2(r, r1, n2)
-      )
-    }
-
-    int lastRank(Node n) { result = max(int r | edgeRank(r, _, n)) }
-  }
-
-  private signature module TypePropagation {
-    class Typ;
-
-    predicate candType(TypeFlowNode n, Typ t);
-
-    bindingset[t]
-    predicate supportsType(TypeFlowNode n, Typ t);
-  }
-
-  /** Implements recursion through `forall` by way of edge ranking. */
-  private module ForAll<NodeSig Node, RankedEdge<Node> E, TypePropagation T> {
-    /**
-     * Holds if `t` is a bound that holds on one of the incoming edges to `n` and
-     * thus is a candidate bound for `n`.
-     */
-    pragma[nomagic]
-    private predicate candJoinType(Node n, T::Typ t) {
-      exists(TypeFlowNode mid |
-        T::candType(mid, t) and
-        E::edgeRank(_, mid, n)
-      )
-    }
-
-    /**
-     * Holds if `t` is a candidate bound for `n` that is also valid for data coming
-     * through the edges into `n` ranked from `1` to `r`.
-     */
-    private predicate flowJoin(int r, Node n, T::Typ t) {
-      (
-        r = 1 and candJoinType(n, t)
-        or
-        flowJoin(r - 1, n, t) and E::edgeRank(r, _, n)
-      ) and
-      forall(TypeFlowNode mid | E::edgeRank(r, mid, n) | T::supportsType(mid, t))
-    }
-
-    /**
-     * Holds if `t` is a candidate bound for `n` that is also valid for data
-     * coming through all the incoming edges, and therefore is a valid bound for
-     * `n`.
-     */
-    predicate flowJoin(Node n, T::Typ t) { flowJoin(E::lastRank(n), n, t) }
-  }
-
-  private module JoinStep implements Edge {
-    class Node = TypeFlowNode;
-
-    predicate edge = joinStepNotNull/2;
-  }
-
-  private module SccJoinStep implements Edge {
-    class Node = TypeFlowScc;
-
-    predicate edge = sccJoinStepNotNull/2;
-  }
-
-  private module RankedJoinStep = RankEdge<JoinStep>;
-
-  private module RankedSccJoinStep = RankEdge<SccJoinStep>;
-
-  signature module NullaryPropertySig {
-    predicate hasPropertyBase(TypeFlowNode n);
-
-    default predicate barrier(TypeFlowNode n) { none() }
-  }
-
-  module FlowNullary<NullaryPropertySig P> {
-    private module Propagation implements TypePropagation {
-      class Typ = Unit;
-
-      predicate candType(TypeFlowNode n, Unit u) { hasProperty(n) and exists(u) }
-
-      predicate supportsType = candType/2;
-    }
-
-    predicate hasProperty(TypeFlowNode n) {
-      P::hasPropertyBase(n)
-      or
-      not P::barrier(n) and
-      (
-        exists(TypeFlowNode mid | hasProperty(mid) and uniqStep(mid, n))
-        or
-        // The following is an optimized version of
-        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
-        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, _)
-        or
-        exists(TypeFlowScc scc |
-          sccRepr(n, scc) and
-          // Optimized version of
-          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
-          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, _)
-        )
-      )
-    }
-  }
-
-  signature module PropertySig {
-    class Prop;
-
-    bindingset[t1, t2]
-    default predicate propImplies(Prop t1, Prop t2) { t1 = t2 }
-
-    predicate hasPropertyBase(TypeFlowNode n, Prop t);
-
-    default predicate barrier(TypeFlowNode n) { none() }
-  }
-
-  module Flow<PropertySig P> {
-    private module Propagation implements TypePropagation {
-      class Typ = P::Prop;
-
-      predicate candType = hasProperty/2;
-
-      bindingset[t]
-      predicate supportsType(TypeFlowNode n, Typ t) {
-        exists(Typ t0 | hasProperty(n, t0) and P::propImplies(t0, t))
-      }
-    }
-
-    /**
-     * Holds if the runtime type of `n` is exactly `t` and if this bound is a
-     * non-trivial lower bound, that is, `t` has a subtype.
-     */
-    predicate hasProperty(TypeFlowNode n, P::Prop t) {
-      P::hasPropertyBase(n, t)
-      or
-      not P::barrier(n) and
-      (
-        exists(TypeFlowNode mid | hasProperty(mid, t) and uniqStep(mid, n))
-        or
-        // The following is an optimized version of
-        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
-        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, t)
-        or
-        exists(TypeFlowScc scc |
-          sccRepr(n, scc) and
-          // Optimized version of
-          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
-          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, t)
-        )
-      )
-    }
-  }
-}
-
 module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private import I
 

From d6e420bd0e1d7abf5ca839b5c0022560ac7e1e01 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 16:23:44 +0100
Subject: [PATCH 05/12] UniversalFlow: Rename node type.

---
 .../codeql/typeflow/UniversalFlow.qll         | 84 +++++++++----------
 .../codeql/typeflow/internal/TypeFlowImpl.qll |  2 +-
 2 files changed, 43 insertions(+), 43 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
index 7aa07e0a59c7..23778397df90 100644
--- a/shared/typeflow/codeql/typeflow/UniversalFlow.qll
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -7,7 +7,7 @@ signature module UniversalFlowInput<LocationSig Location> {
    * A node for which certain data flow properties may be proved. For example,
    * expressions and method declarations.
    */
-  class TypeFlowNode {
+  class FlowNode {
     /** Gets a textual representation of this node. */
     string toString();
 
@@ -20,16 +20,16 @@ signature module UniversalFlowInput<LocationSig Location> {
    *
    * For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
    */
-  predicate step(TypeFlowNode n1, TypeFlowNode n2);
+  predicate step(FlowNode n1, FlowNode n2);
 
   /** Holds if `n` represents a `null` value. */
-  predicate isNullValue(TypeFlowNode n);
+  predicate isNullValue(FlowNode n);
 
   /**
    * Holds if `n` should be excluded from the set of null values even if
    * the null analysis determines that `n` is always null.
    */
-  default predicate isExcludedFromNullAnalysis(TypeFlowNode n) { none() }
+  default predicate isExcludedFromNullAnalysis(FlowNode n) { none() }
 }
 
 module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
@@ -39,21 +39,21 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
    * Holds if data can flow from `n1` to `n2` in one step, and `n1` is
    * functionally determined by `n2`.
    */
-  private predicate uniqStep(TypeFlowNode n1, TypeFlowNode n2) { n1 = unique(TypeFlowNode n | step(n, n2)) }
+  private predicate uniqStep(FlowNode n1, FlowNode n2) { n1 = unique(FlowNode n | step(n, n2)) }
 
   /**
    * Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
    * functionally determined by `n2`.
    */
-  private predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) { step(n1, n2) and not uniqStep(n1, n2) }
+  private predicate joinStep(FlowNode n1, FlowNode n2) { step(n1, n2) and not uniqStep(n1, n2) }
 
   /** Holds if `null` is the only value that flows to `n`. */
-  private predicate isNull(TypeFlowNode n) {
+  private predicate isNull(FlowNode n) {
     isNullValue(n)
     or
-    exists(TypeFlowNode mid | isNull(mid) and uniqStep(mid, n))
+    exists(FlowNode mid | isNull(mid) and uniqStep(mid, n))
     or
-    forex(TypeFlowNode mid | joinStep(mid, n) | isNull(mid)) and
+    forex(FlowNode mid | joinStep(mid, n) | isNull(mid)) and
     not isExcludedFromNullAnalysis(n)
   }
 
@@ -61,27 +61,27 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
    * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
    * functionally determined by `n2`, and `n1` might take a non-null value.
    */
-  predicate joinStepNotNull(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate joinStepNotNull(FlowNode n1, FlowNode n2) {
     joinStep(n1, n2) and not isNull(n1)
   }
 
-  predicate anyStep(TypeFlowNode n1, TypeFlowNode n2) {
+  predicate anyStep(FlowNode n1, FlowNode n2) {
     joinStepNotNull(n1, n2) or uniqStep(n1, n2)
   }
 
-  private predicate sccEdge(TypeFlowNode n1, TypeFlowNode n2) {
+  private predicate sccEdge(FlowNode n1, FlowNode n2) {
     anyStep(n1, n2) and anyStep+(n2, n1)
   }
 
-  private module Scc = QlBuiltins::EquivalenceRelation<TypeFlowNode, sccEdge/2>;
+  private module Scc = QlBuiltins::EquivalenceRelation<FlowNode, sccEdge/2>;
 
   private class TypeFlowScc = Scc::EquivalenceClass;
 
   /** Holds if `n` is part of an SCC of size 2 or more represented by `scc`. */
-  private predicate sccRepr(TypeFlowNode n, TypeFlowScc scc) { scc = Scc::getEquivalenceClass(n) }
+  private predicate sccRepr(FlowNode n, TypeFlowScc scc) { scc = Scc::getEquivalenceClass(n) }
 
-  private predicate sccJoinStepNotNull(TypeFlowNode n, TypeFlowScc scc) {
-    exists(TypeFlowNode mid |
+  private predicate sccJoinStepNotNull(FlowNode n, TypeFlowScc scc) {
+    exists(FlowNode mid |
       joinStepNotNull(n, mid) and
       sccRepr(mid, scc) and
       not sccRepr(n, scc)
@@ -93,11 +93,11 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   private signature module Edge {
     class Node;
 
-    predicate edge(TypeFlowNode n1, Node n2);
+    predicate edge(FlowNode n1, Node n2);
   }
 
   private signature module RankedEdge<NodeSig Node> {
-    predicate edgeRank(int r, TypeFlowNode n1, Node n2);
+    predicate edgeRank(int r, FlowNode n1, Node n2);
 
     int lastRank(Node n);
   }
@@ -109,9 +109,9 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
      * Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. The used
      * ordering is not necessarily total, so the ranking may have gaps.
      */
-    private predicate edgeRank1(int r, TypeFlowNode n1, Node n2) {
+    private predicate edgeRank1(int r, FlowNode n1, Node n2) {
       n1 =
-        rank[r](TypeFlowNode n, int startline, int startcolumn |
+        rank[r](FlowNode n, int startline, int startcolumn |
           edge(n, n2) and
           n.getLocation().hasLocationInfo(_, startline, startcolumn, _, _)
         |
@@ -128,7 +128,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
     }
 
     /** Holds if `r` is a ranking of the incoming edges `(n1,n2)` to `n2`. */
-    predicate edgeRank(int r, TypeFlowNode n1, Node n2) {
+    predicate edgeRank(int r, FlowNode n1, Node n2) {
       exists(int r1 |
         edgeRank1(r1, n1, n2) and
         edgeRank2(r, r1, n2)
@@ -141,10 +141,10 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   private signature module TypePropagation {
     class Typ;
 
-    predicate candType(TypeFlowNode n, Typ t);
+    predicate candType(FlowNode n, Typ t);
 
     bindingset[t]
-    predicate supportsType(TypeFlowNode n, Typ t);
+    predicate supportsType(FlowNode n, Typ t);
   }
 
   /** Implements recursion through `forall` by way of edge ranking. */
@@ -155,7 +155,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
      */
     pragma[nomagic]
     private predicate candJoinType(Node n, T::Typ t) {
-      exists(TypeFlowNode mid |
+      exists(FlowNode mid |
         T::candType(mid, t) and
         E::edgeRank(_, mid, n)
       )
@@ -171,7 +171,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
         or
         flowJoin(r - 1, n, t) and E::edgeRank(r, _, n)
       ) and
-      forall(TypeFlowNode mid | E::edgeRank(r, mid, n) | T::supportsType(mid, t))
+      forall(FlowNode mid | E::edgeRank(r, mid, n) | T::supportsType(mid, t))
     }
 
     /**
@@ -183,7 +183,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   }
 
   private module JoinStep implements Edge {
-    class Node = TypeFlowNode;
+    class Node = FlowNode;
 
     predicate edge = joinStepNotNull/2;
   }
@@ -199,35 +199,35 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   private module RankedSccJoinStep = RankEdge<SccJoinStep>;
 
   signature module NullaryPropertySig {
-    predicate hasPropertyBase(TypeFlowNode n);
+    predicate hasPropertyBase(FlowNode n);
 
-    default predicate barrier(TypeFlowNode n) { none() }
+    default predicate barrier(FlowNode n) { none() }
   }
 
   module FlowNullary<NullaryPropertySig P> {
     private module Propagation implements TypePropagation {
       class Typ = Unit;
 
-      predicate candType(TypeFlowNode n, Unit u) { hasProperty(n) and exists(u) }
+      predicate candType(FlowNode n, Unit u) { hasProperty(n) and exists(u) }
 
       predicate supportsType = candType/2;
     }
 
-    predicate hasProperty(TypeFlowNode n) {
+    predicate hasProperty(FlowNode n) {
       P::hasPropertyBase(n)
       or
       not P::barrier(n) and
       (
-        exists(TypeFlowNode mid | hasProperty(mid) and uniqStep(mid, n))
+        exists(FlowNode mid | hasProperty(mid) and uniqStep(mid, n))
         or
         // The following is an optimized version of
-        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
-        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, _)
+        // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
+        ForAll<FlowNode, RankedJoinStep, Propagation>::flowJoin(n, _)
         or
         exists(TypeFlowScc scc |
           sccRepr(n, scc) and
           // Optimized version of
-          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
+          // `forex(FlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
           ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, _)
         )
       )
@@ -240,9 +240,9 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
     bindingset[t1, t2]
     default predicate propImplies(Prop t1, Prop t2) { t1 = t2 }
 
-    predicate hasPropertyBase(TypeFlowNode n, Prop t);
+    predicate hasPropertyBase(FlowNode n, Prop t);
 
-    default predicate barrier(TypeFlowNode n) { none() }
+    default predicate barrier(FlowNode n) { none() }
   }
 
   module Flow<PropertySig P> {
@@ -252,7 +252,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
       predicate candType = hasProperty/2;
 
       bindingset[t]
-      predicate supportsType(TypeFlowNode n, Typ t) {
+      predicate supportsType(FlowNode n, Typ t) {
         exists(Typ t0 | hasProperty(n, t0) and P::propImplies(t0, t))
       }
     }
@@ -261,21 +261,21 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
      * Holds if the runtime type of `n` is exactly `t` and if this bound is a
      * non-trivial lower bound, that is, `t` has a subtype.
      */
-    predicate hasProperty(TypeFlowNode n, P::Prop t) {
+    predicate hasProperty(FlowNode n, P::Prop t) {
       P::hasPropertyBase(n, t)
       or
       not P::barrier(n) and
       (
-        exists(TypeFlowNode mid | hasProperty(mid, t) and uniqStep(mid, n))
+        exists(FlowNode mid | hasProperty(mid, t) and uniqStep(mid, n))
         or
         // The following is an optimized version of
-        // `forex(TypeFlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
-        ForAll<TypeFlowNode, RankedJoinStep, Propagation>::flowJoin(n, t)
+        // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
+        ForAll<FlowNode, RankedJoinStep, Propagation>::flowJoin(n, t)
         or
         exists(TypeFlowScc scc |
           sccRepr(n, scc) and
           // Optimized version of
-          // `forex(TypeFlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
+          // `forex(FlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
           ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, t)
         )
       )
diff --git a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
index eb4a30ef305f..42b615cc3fa9 100644
--- a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
+++ b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
@@ -7,7 +7,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private import I
 
   private module UfInput implements UniversalFlowInput<Location> {
-    class TypeFlowNode = I::TypeFlowNode;
+    class FlowNode = TypeFlowNode;
 
     predicate step = I::step/2;
 

From 6680537e930718ff0490e2e0f44973529a6ce72f Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 16:25:30 +0100
Subject: [PATCH 06/12] UniversalFlow: Minor tweak to isNull and autoformat.

---
 .../codeql/typeflow/UniversalFlow.qll         | 24 ++++++++-----------
 1 file changed, 10 insertions(+), 14 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
index 23778397df90..3929a35d06e3 100644
--- a/shared/typeflow/codeql/typeflow/UniversalFlow.qll
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -51,27 +51,23 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   private predicate isNull(FlowNode n) {
     isNullValue(n)
     or
-    exists(FlowNode mid | isNull(mid) and uniqStep(mid, n))
-    or
-    forex(FlowNode mid | joinStep(mid, n) | isNull(mid)) and
-    not isExcludedFromNullAnalysis(n)
+    not isExcludedFromNullAnalysis(n) and
+    (
+      exists(FlowNode mid | isNull(mid) and uniqStep(mid, n))
+      or
+      forex(FlowNode mid | joinStep(mid, n) | isNull(mid))
+    )
   }
 
   /**
    * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
    * functionally determined by `n2`, and `n1` might take a non-null value.
    */
-  predicate joinStepNotNull(FlowNode n1, FlowNode n2) {
-    joinStep(n1, n2) and not isNull(n1)
-  }
+  predicate joinStepNotNull(FlowNode n1, FlowNode n2) { joinStep(n1, n2) and not isNull(n1) }
 
-  predicate anyStep(FlowNode n1, FlowNode n2) {
-    joinStepNotNull(n1, n2) or uniqStep(n1, n2)
-  }
+  predicate anyStep(FlowNode n1, FlowNode n2) { joinStepNotNull(n1, n2) or uniqStep(n1, n2) }
 
-  private predicate sccEdge(FlowNode n1, FlowNode n2) {
-    anyStep(n1, n2) and anyStep+(n2, n1)
-  }
+  private predicate sccEdge(FlowNode n1, FlowNode n2) { anyStep(n1, n2) and anyStep+(n2, n1) }
 
   private module Scc = QlBuiltins::EquivalenceRelation<FlowNode, sccEdge/2>;
 
@@ -281,4 +277,4 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
       )
     }
   }
-}
\ No newline at end of file
+}

From d41b86a87d9646225167288b5815d3bdda070ab0 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 16:27:27 +0100
Subject: [PATCH 07/12] UniversalFlow: Tweak visibility and add qldoc.

---
 .../codeql/typeflow/UniversalFlow.qll         | 48 ++++++++++++++++---
 .../codeql/typeflow/internal/TypeFlowImpl.qll |  4 +-
 2 files changed, 44 insertions(+), 8 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
index 3929a35d06e3..8cc05eff5ee6 100644
--- a/shared/typeflow/codeql/typeflow/UniversalFlow.qll
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -1,3 +1,31 @@
+/**
+ * Provides predicates for proving data flow properties that hold for all
+ * paths, that is, reachability is computed using universal quantification over
+ * the step relation.
+ *
+ * Regular data flow search for the existence of a path, that is, reachability
+ * using existential quantification over the step relation. Hence, this library
+ * computes the dual reachability predicate that states that a certain property
+ * always holds for a given node regardless of the path taken.
+ *
+ * As a simple comparison, the computed predicate is essentially equivalent to
+ * the folllowing:
+ * ```ql
+ *   predicate hasProperty(FlowNode n, Prop t) {
+ *     basecase(n, t)
+ *     or
+ *     forex(FlowNode mid | step(mid, n) | hasProperty(mid, t))
+ *   }
+ * ```
+ * More complex property propagation is supported, and strongly connected
+ * components in the flow graph are handled.
+ *
+ * As an initial such property calculation, the library computes the set of
+ * nodes that are always null. These are then subtracted from the graph such
+ * that subsequently calculated properties hold under the assumption that the
+ * value is not null.
+ */
+
 private import codeql.util.Location
 private import codeql.util.Unit
 
@@ -59,13 +87,21 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
     )
   }
 
-  /**
-   * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
-   * functionally determined by `n2`, and `n1` might take a non-null value.
-   */
-  predicate joinStepNotNull(FlowNode n1, FlowNode n2) { joinStep(n1, n2) and not isNull(n1) }
+  private import Internal
 
-  predicate anyStep(FlowNode n1, FlowNode n2) { joinStepNotNull(n1, n2) or uniqStep(n1, n2) }
+  module Internal {
+    /**
+     * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
+     * functionally determined by `n2`, and `n1` might take a non-null value.
+     */
+    predicate joinStepNotNull(FlowNode n1, FlowNode n2) { joinStep(n1, n2) and not isNull(n1) }
+
+    /**
+     * Holds if data can flow from `n1` to `n2` in one step, excluding join
+     * steps from nodes that are always null.
+     */
+    predicate anyStep(FlowNode n1, FlowNode n2) { joinStepNotNull(n1, n2) or uniqStep(n1, n2) }
+  }
 
   private predicate sccEdge(FlowNode n1, FlowNode n2) { anyStep(n1, n2) and anyStep+(n2, n1) }
 
diff --git a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
index 42b615cc3fa9..a994118e852a 100644
--- a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
+++ b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
@@ -162,7 +162,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
    */
   private predicate unionTypeFlowBaseCand(TypeFlowNode n, Type t, boolean exact) {
     exists(TypeFlowNode next |
-      UnivFlow::joinStepNotNull(n, next) and
+      UnivFlow::Internal::joinStepNotNull(n, next) and
       bestTypeFlowOrTypeFlowBase(n, t, exact) and
       not bestTypeFlowOrTypeFlowBase(next, t, exact) and
       not exactType(next, _)
@@ -196,7 +196,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private predicate unionTypeFlow0(TypeFlowNode n, Type t, boolean exact) {
     hasUnionTypeFlow(n) and
     (
-      exists(TypeFlowNode mid | UnivFlow::anyStep(mid, n) | unionTypeFlow(mid, t, exact))
+      exists(TypeFlowNode mid | UnivFlow::Internal::anyStep(mid, n) | unionTypeFlow(mid, t, exact))
       or
       unionTypeFlowBaseCand(n, t, exact)
       or

From 7d98d391b704ad291ff3065eed2af7f6b56cc64c Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 16:28:28 +0100
Subject: [PATCH 08/12] UniversalFlow: Rename FlowScc.

---
 .../typeflow/codeql/typeflow/UniversalFlow.qll   | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
index 8cc05eff5ee6..0ae4bbaed480 100644
--- a/shared/typeflow/codeql/typeflow/UniversalFlow.qll
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -107,12 +107,12 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
 
   private module Scc = QlBuiltins::EquivalenceRelation<FlowNode, sccEdge/2>;
 
-  private class TypeFlowScc = Scc::EquivalenceClass;
+  private class FlowScc = Scc::EquivalenceClass;
 
   /** Holds if `n` is part of an SCC of size 2 or more represented by `scc`. */
-  private predicate sccRepr(FlowNode n, TypeFlowScc scc) { scc = Scc::getEquivalenceClass(n) }
+  private predicate sccRepr(FlowNode n, FlowScc scc) { scc = Scc::getEquivalenceClass(n) }
 
-  private predicate sccJoinStepNotNull(FlowNode n, TypeFlowScc scc) {
+  private predicate sccJoinStepNotNull(FlowNode n, FlowScc scc) {
     exists(FlowNode mid |
       joinStepNotNull(n, mid) and
       sccRepr(mid, scc) and
@@ -221,7 +221,7 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   }
 
   private module SccJoinStep implements Edge {
-    class Node = TypeFlowScc;
+    class Node = FlowScc;
 
     predicate edge = sccJoinStepNotNull/2;
   }
@@ -256,11 +256,11 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
         // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
         ForAll<FlowNode, RankedJoinStep, Propagation>::flowJoin(n, _)
         or
-        exists(TypeFlowScc scc |
+        exists(FlowScc scc |
           sccRepr(n, scc) and
           // Optimized version of
           // `forex(FlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid))`
-          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, _)
+          ForAll<FlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, _)
         )
       )
     }
@@ -304,11 +304,11 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
         // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
         ForAll<FlowNode, RankedJoinStep, Propagation>::flowJoin(n, t)
         or
-        exists(TypeFlowScc scc |
+        exists(FlowScc scc |
           sccRepr(n, scc) and
           // Optimized version of
           // `forex(FlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
-          ForAll<TypeFlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, t)
+          ForAll<FlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, t)
         )
       )
     }

From 1d3bad1358840afc8dfe8af3ae4559e5c3f37f39 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Mon, 28 Oct 2024 16:31:23 +0100
Subject: [PATCH 09/12] UniversalFlow: More renaming.

---
 .../codeql/typeflow/UniversalFlow.qll         | 52 +++++++++----------
 .../codeql/typeflow/internal/TypeFlowImpl.qll |  6 +--
 2 files changed, 29 insertions(+), 29 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
index 0ae4bbaed480..8ef73133e054 100644
--- a/shared/typeflow/codeql/typeflow/UniversalFlow.qll
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -60,7 +60,7 @@ signature module UniversalFlowInput<LocationSig Location> {
   default predicate isExcludedFromNullAnalysis(FlowNode n) { none() }
 }
 
-module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
+module Make<LocationSig Location, UniversalFlowInput<Location> I> {
   private import I
 
   /**
@@ -170,48 +170,48 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
     int lastRank(Node n) { result = max(int r | edgeRank(r, _, n)) }
   }
 
-  private signature module TypePropagation {
-    class Typ;
+  private signature module PropPropagation {
+    class Prop;
 
-    predicate candType(FlowNode n, Typ t);
+    predicate candProp(FlowNode n, Prop t);
 
     bindingset[t]
-    predicate supportsType(FlowNode n, Typ t);
+    predicate supportsProp(FlowNode n, Prop t);
   }
 
   /** Implements recursion through `forall` by way of edge ranking. */
-  private module ForAll<NodeSig Node, RankedEdge<Node> E, TypePropagation T> {
+  private module ForAll<NodeSig Node, RankedEdge<Node> E, PropPropagation T> {
     /**
-     * Holds if `t` is a bound that holds on one of the incoming edges to `n` and
-     * thus is a candidate bound for `n`.
+     * Holds if `t` is a property that holds on one of the incoming edges to `n` and
+     * thus is a candidate property for `n`.
      */
     pragma[nomagic]
-    private predicate candJoinType(Node n, T::Typ t) {
+    private predicate candJoinProp(Node n, T::Prop t) {
       exists(FlowNode mid |
-        T::candType(mid, t) and
+        T::candProp(mid, t) and
         E::edgeRank(_, mid, n)
       )
     }
 
     /**
-     * Holds if `t` is a candidate bound for `n` that is also valid for data coming
+     * Holds if `t` is a candidate property for `n` that is also valid for data coming
      * through the edges into `n` ranked from `1` to `r`.
      */
-    private predicate flowJoin(int r, Node n, T::Typ t) {
+    private predicate flowJoin(int r, Node n, T::Prop t) {
       (
-        r = 1 and candJoinType(n, t)
+        r = 1 and candJoinProp(n, t)
         or
         flowJoin(r - 1, n, t) and E::edgeRank(r, _, n)
       ) and
-      forall(FlowNode mid | E::edgeRank(r, mid, n) | T::supportsType(mid, t))
+      forall(FlowNode mid | E::edgeRank(r, mid, n) | T::supportsProp(mid, t))
     }
 
     /**
-     * Holds if `t` is a candidate bound for `n` that is also valid for data
-     * coming through all the incoming edges, and therefore is a valid bound for
+     * Holds if `t` is a candidate property for `n` that is also valid for data
+     * coming through all the incoming edges, and therefore is a valid property for
      * `n`.
      */
-    predicate flowJoin(Node n, T::Typ t) { flowJoin(E::lastRank(n), n, t) }
+    predicate flowJoin(Node n, T::Prop t) { flowJoin(E::lastRank(n), n, t) }
   }
 
   private module JoinStep implements Edge {
@@ -237,12 +237,12 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   }
 
   module FlowNullary<NullaryPropertySig P> {
-    private module Propagation implements TypePropagation {
-      class Typ = Unit;
+    private module Propagation implements PropPropagation {
+      class Prop = Unit;
 
-      predicate candType(FlowNode n, Unit u) { hasProperty(n) and exists(u) }
+      predicate candProp(FlowNode n, Unit u) { hasProperty(n) and exists(u) }
 
-      predicate supportsType = candType/2;
+      predicate supportsProp = candProp/2;
     }
 
     predicate hasProperty(FlowNode n) {
@@ -278,14 +278,14 @@ module UfMake<LocationSig Location, UniversalFlowInput<Location> I> {
   }
 
   module Flow<PropertySig P> {
-    private module Propagation implements TypePropagation {
-      class Typ = P::Prop;
+    private module Propagation implements PropPropagation {
+      class Prop = P::Prop;
 
-      predicate candType = hasProperty/2;
+      predicate candProp = hasProperty/2;
 
       bindingset[t]
-      predicate supportsType(FlowNode n, Typ t) {
-        exists(Typ t0 | hasProperty(n, t0) and P::propImplies(t0, t))
+      predicate supportsProp(FlowNode n, Prop t) {
+        exists(Prop t0 | hasProperty(n, t0) and P::propImplies(t0, t))
       }
     }
 
diff --git a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
index a994118e852a..f578b61b77bb 100644
--- a/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
+++ b/shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
@@ -1,12 +1,12 @@
 private import codeql.typeflow.TypeFlow
-private import codeql.typeflow.UniversalFlow
+private import codeql.typeflow.UniversalFlow as UniversalFlow
 private import codeql.util.Location
 private import codeql.util.Unit
 
 module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
   private import I
 
-  private module UfInput implements UniversalFlowInput<Location> {
+  private module UfInput implements UniversalFlow::UniversalFlowInput<Location> {
     class FlowNode = TypeFlowNode;
 
     predicate step = I::step/2;
@@ -16,7 +16,7 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
     predicate isExcludedFromNullAnalysis = I::isExcludedFromNullAnalysis/1;
   }
 
-  private module UnivFlow = UfMake<Location, UfInput>;
+  private module UnivFlow = UniversalFlow::Make<Location, UfInput>;
 
   private module ExactTypeProperty implements UnivFlow::PropertySig {
     class Prop = Type;

From b00597331788f04136f2ab11d5d6a7354edea8ff Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 30 Oct 2024 14:08:38 +0100
Subject: [PATCH 10/12] UniversalFlow: Skip property propagation to null nodes.

---
 shared/typeflow/codeql/typeflow/UniversalFlow.qll | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
index 8ef73133e054..fd413ffc5a6e 100644
--- a/shared/typeflow/codeql/typeflow/UniversalFlow.qll
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -87,6 +87,10 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
     )
   }
 
+  private predicate uniqStepNotNull(FlowNode n1, FlowNode n2) {
+    uniqStep(n1, n2) and not isNull(n1)
+  }
+
   private import Internal
 
   module Internal {
@@ -100,7 +104,9 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
      * Holds if data can flow from `n1` to `n2` in one step, excluding join
      * steps from nodes that are always null.
      */
-    predicate anyStep(FlowNode n1, FlowNode n2) { joinStepNotNull(n1, n2) or uniqStep(n1, n2) }
+    predicate anyStep(FlowNode n1, FlowNode n2) {
+      joinStepNotNull(n1, n2) or uniqStepNotNull(n1, n2)
+    }
   }
 
   private predicate sccEdge(FlowNode n1, FlowNode n2) { anyStep(n1, n2) and anyStep+(n2, n1) }
@@ -250,7 +256,7 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
       or
       not P::barrier(n) and
       (
-        exists(FlowNode mid | hasProperty(mid) and uniqStep(mid, n))
+        exists(FlowNode mid | hasProperty(mid) and uniqStepNotNull(mid, n))
         or
         // The following is an optimized version of
         // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
@@ -298,7 +304,7 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
       or
       not P::barrier(n) and
       (
-        exists(FlowNode mid | hasProperty(mid, t) and uniqStep(mid, n))
+        exists(FlowNode mid | hasProperty(mid, t) and uniqStepNotNull(mid, n))
         or
         // The following is an optimized version of
         // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`

From 9b493c1e1bfd7ddb72b4d0d8af4869e26a668cdb Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Wed, 30 Oct 2024 15:05:36 +0100
Subject: [PATCH 11/12] Java: Fix bug related to null inference for pattern
 initializer.

---
 java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll b/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
index 7b6e4e725af3..f71c99321638 100644
--- a/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
@@ -138,7 +138,7 @@ private module Input implements TypeFlowInput<Location> {
     exists(LocalVariableDeclExpr decl |
       n.asSsa().(BaseSsaUpdate).getDefiningExpr() = decl and
       not decl.hasImplicitInit() and
-      not exists(decl.getInit())
+      not exists(decl.getInitOrPatternSource())
     )
   }
 

From bae61875cd531f132a7df1aaba5b1136dd2aebcd Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Fri, 1 Nov 2024 14:04:27 +0100
Subject: [PATCH 12/12] UniversalFlow: Fixup some qldoc.

---
 .../codeql/typeflow/UniversalFlow.qll         | 37 +++++++++++++++++--
 1 file changed, 33 insertions(+), 4 deletions(-)

diff --git a/shared/typeflow/codeql/typeflow/UniversalFlow.qll b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
index fd413ffc5a6e..75b210f8cebb 100644
--- a/shared/typeflow/codeql/typeflow/UniversalFlow.qll
+++ b/shared/typeflow/codeql/typeflow/UniversalFlow.qll
@@ -60,6 +60,9 @@ signature module UniversalFlowInput<LocationSig Location> {
   default predicate isExcludedFromNullAnalysis(FlowNode n) { none() }
 }
 
+/**
+ * Provides an implementation of universal flow using input `I`.
+ */
 module Make<LocationSig Location, UniversalFlowInput<Location> I> {
   private import I
 
@@ -93,6 +96,7 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
 
   private import Internal
 
+  /** Provides access to internal step relations. */
   module Internal {
     /**
      * Holds if data can flow from `n1` to `n2` in one step, `n1` is not necessarily
@@ -242,6 +246,10 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
     default predicate barrier(FlowNode n) { none() }
   }
 
+  /**
+   * Calculates a (nullary) property using universal flow given a base case
+   * relation.
+   */
   module FlowNullary<NullaryPropertySig P> {
     private module Propagation implements PropPropagation {
       class Prop = Unit;
@@ -251,6 +259,10 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
       predicate supportsProp = candProp/2;
     }
 
+    /**
+     * Holds if all flow reaching `n` originates from nodes in
+     * `hasPropertyBase`.
+     */
     predicate hasProperty(FlowNode n) {
       P::hasPropertyBase(n)
       or
@@ -283,6 +295,10 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
     default predicate barrier(FlowNode n) { none() }
   }
 
+  /**
+   * Calculates a unary property using universal flow given a base case
+   * relation.
+   */
   module Flow<PropertySig P> {
     private module Propagation implements PropPropagation {
       class Prop = P::Prop;
@@ -296,8 +312,9 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
     }
 
     /**
-     * Holds if the runtime type of `n` is exactly `t` and if this bound is a
-     * non-trivial lower bound, that is, `t` has a subtype.
+     * Holds if all flow reaching `n` originates from nodes in
+     * `hasPropertyBase`. The property `t` is taken from one of those origins
+     * such that all other origins imply `t`.
      */
     predicate hasProperty(FlowNode n, P::Prop t) {
       P::hasPropertyBase(n, t)
@@ -307,13 +324,25 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
         exists(FlowNode mid | hasProperty(mid, t) and uniqStepNotNull(mid, n))
         or
         // The following is an optimized version of
-        // `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t))`
+        // ```
+        // exists(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, t)) and
+        // forall(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid, _)) and
+        // forall(FlowNode mid, P::Prop t0 | joinStepNotNull(mid, n) and hasPropery(mid, t0) |
+        //   P::propImplies(t0, t)
+        // )
+        // ```
         ForAll<FlowNode, RankedJoinStep, Propagation>::flowJoin(n, t)
         or
         exists(FlowScc scc |
           sccRepr(n, scc) and
           // Optimized version of
-          // `forex(FlowNode mid | sccJoinStepNotNull(mid, scc) | hasPropery(mid, t))`
+          // ```
+          // exists(FlowNode mid | sccJoinStepNotNull(mid, n) | hasPropery(mid, t)) and
+          // forall(FlowNode mid | sccJoinStepNotNull(mid, n) | hasPropery(mid, _)) and
+          // forall(FlowNode mid, P::Prop t0 | sccJoinStepNotNull(mid, n) and hasPropery(mid, t0) |
+          //   P::propImplies(t0, t)
+          // )
+          // ```
           ForAll<FlowScc, RankedSccJoinStep, Propagation>::flowJoin(scc, t)
         )
       )