Merge pull request #20994 from hvitved/csharp/remove-pre-ssa

C#: Remove `PreSsa` library

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

@@ -842,6 +842,40 @@ module Internal {
     e3 = any(NullCoalescingExpr nce | e1 = nce.getLeftOperand() and e2 = nce.getRightOperand())
   }
 
+  predicate nullValueImplied(Expr e) {
+    nullValue(e)
+    or
+    exists(Expr e1 | nullValueImplied(e1) and nullValueImpliedUnary(e1, e))
+    or
+    exists(Expr e1, Expr e2 |
+      nullValueImplied(e1) and nullValueImplied(e2) and nullValueImpliedBinary(e1, e2, e)
+    )
+    or
+    e =
+      any(Ssa::Definition def |
+        forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nullDef(u))
+      ).getARead()
+  }
+
+  private predicate nullDef(Ssa::ExplicitDefinition def) {
+    nullValueImplied(def.getADefinition().getSource())
+  }
+
+  predicate nonNullValueImplied(Expr e) {
+    nonNullValue(e)
+    or
+    exists(Expr e1 | nonNullValueImplied(e1) and nonNullValueImpliedUnary(e1, e))
+    or
+    e =
+      any(Ssa::Definition def |
+        forex(Ssa::Definition u | u = def.getAnUltimateDefinition() | nonNullDef(u))
+      ).getARead()
+  }
+
+  private predicate nonNullDef(Ssa::ExplicitDefinition def) {
+    nonNullValueImplied(def.getADefinition().getSource())
+  }
+
   /** A callable that always returns a non-`null` value. */
   private class NonNullCallable extends Callable {
     NonNullCallable() { this = any(SystemObjectClass c).getGetTypeMethod() }
@@ -936,29 +970,6 @@ module Internal {
     e = any(BinaryArithmeticOperation bao | result = bao.getAnOperand())
   }
 
-  // The predicates in this module should be evaluated in the same stage as the CFG
-  // construction stage. This is to avoid recomputation of pre-basic-blocks and
-  // pre-SSA predicates
-  private module PreCfg {
-    private import semmle.code.csharp.controlflow.internal.PreBasicBlocks as PreBasicBlocks
-    private import semmle.code.csharp.controlflow.internal.PreSsa
-
-    private predicate nullDef(PreSsa::Definition def) {
-      nullValueImplied(def.getDefinition().getSource())
-    }
-
-    private predicate nonNullDef(PreSsa::Definition def) {
-      nonNullValueImplied(def.getDefinition().getSource())
-    }
-
-    private predicate emptyDef(PreSsa::Definition def) {
-      emptyValue(def.getDefinition().getSource())
-    }
-
-    private predicate nonEmptyDef(PreSsa::Definition def) {
-      nonEmptyValue(def.getDefinition().getSource())
-    }
-
   deprecated predicate isGuard(Expr e, GuardValue val) {
     (
       e.getType() instanceof BoolType and
@@ -974,116 +985,6 @@ module Internal {
     not e = any(LocalVariableDeclStmt s).getAVariableDeclExpr()
   }
 
-    cached
-    private module CachedWithCfg {
-      private import semmle.code.csharp.Caching
-
-      private predicate firstReadSameVarUniquePredecessor(
-        PreSsa::Definition def, AssignableRead read
-      ) {
-        read = def.getAFirstRead() and
-        (
-          not PreSsa::adjacentReadPairSameVar(_, read)
-          or
-          read = unique(AssignableRead read0 | PreSsa::adjacentReadPairSameVar(read0, read))
-        )
-      }
-
-      cached
-      predicate nullValueImplied(Expr e) {
-        nullValue(e)
-        or
-        exists(Expr e1 | nullValueImplied(e1) and nullValueImpliedUnary(e1, e))
-        or
-        exists(Expr e1, Expr e2 |
-          nullValueImplied(e1) and nullValueImplied(e2) and nullValueImpliedBinary(e1, e2, e)
-        )
-        or
-        e =
-          any(PreSsa::Definition def |
-            forex(PreSsa::Definition u | u = def.getAnUltimateDefinition() | nullDef(u))
-          ).getARead()
-      }
-
-      cached
-      predicate nonNullValueImplied(Expr e) {
-        nonNullValue(e)
-        or
-        exists(Expr e1 | nonNullValueImplied(e1) and nonNullValueImpliedUnary(e1, e))
-        or
-        e =
-          any(PreSsa::Definition def |
-            forex(PreSsa::Definition u | u = def.getAnUltimateDefinition() | nonNullDef(u))
-          ).getARead()
-      }
-
-      private predicate adjacentReadPairSameVarUniquePredecessor(
-        AssignableRead read1, AssignableRead read2
-      ) {
-        PreSsa::adjacentReadPairSameVar(read1, read2) and
-        (
-          read1 = read2 and
-          read1 = unique(AssignableRead other | PreSsa::adjacentReadPairSameVar(other, read2))
-          or
-          read1 =
-            unique(AssignableRead other |
-              PreSsa::adjacentReadPairSameVar(other, read2) and other != read2
-            )
-        )
-      }
-
-      cached
-      predicate emptyValue(Expr e) {
-        e.(ArrayCreation).getALengthArgument().getValue().toInt() = 0
-        or
-        e.(ArrayInitializer).hasNoElements()
-        or
-        exists(Expr mid | emptyValue(mid) |
-          mid = e.(AssignExpr).getRValue()
-          or
-          mid = e.(Cast).getExpr()
-        )
-        or
-        exists(PreSsa::Definition def | emptyDef(def) | firstReadSameVarUniquePredecessor(def, e))
-        or
-        exists(MethodCall mc |
-          mc.getTarget().getAnUltimateImplementee().getUnboundDeclaration() =
-            any(SystemCollectionsGenericICollectionInterface c).getClearMethod() and
-          adjacentReadPairSameVarUniquePredecessor(mc.getQualifier(), e)
-        )
-      }
-
-      cached
-      predicate nonEmptyValue(Expr e) {
-        forex(Expr length | length = e.(ArrayCreation).getALengthArgument() |
-          length.getValue().toInt() != 0
-        )
-        or
-        e.(ArrayInitializer).getNumberOfElements() > 0
-        or
-        exists(Expr mid | nonEmptyValue(mid) |
-          mid = e.(AssignExpr).getRValue()
-          or
-          mid = e.(Cast).getExpr()
-        )
-        or
-        exists(PreSsa::Definition def | nonEmptyDef(def) |
-          firstReadSameVarUniquePredecessor(def, e)
-        )
-        or
-        exists(MethodCall mc |
-          mc.getTarget().getAnUltimateImplementee().getUnboundDeclaration() =
-            any(SystemCollectionsGenericICollectionInterface c).getAddMethod() and
-          adjacentReadPairSameVarUniquePredecessor(mc.getQualifier(), e)
-        )
-      }
-    }
-
-    import CachedWithCfg
-  }
-
-  import PreCfg
-
   private predicate interestingDescendantCandidate(Expr e) {
     guardControls(e, _, _)
     or

csharp/ql/lib/semmle/code/csharp/controlflow/internal/PreSsa.qll

@@ -1,221 +0,0 @@
-import csharp
-
-/**
- * Provides an SSA implementation based on "pre-basic-blocks", restricted
- * to local scope variables and fields/properties that behave like local
- * scope variables.
- */
-module PreSsa {
-  private import AssignableDefinitions
-  private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
-  private import semmle.code.csharp.controlflow.internal.PreBasicBlocks as PreBasicBlocks
-  private import codeql.ssa.Ssa as SsaImplCommon
-
-  private predicate definitionAt(
-    AssignableDefinition def, PreBasicBlocks::PreBasicBlock bb, int i, SsaInput::SourceVariable v
-  ) {
-    bb.getNode(i) = def.getExpr() and
-    v = def.getTarget() and
-    // In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
-    not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = def |
-      second.getAssignment() = first.getAssignment() and
-      second.getEvaluationOrder() > first.getEvaluationOrder() and
-      second.getTarget() = v
-    )
-    or
-    def.(ImplicitParameterDefinition).getParameter() = v and
-    exists(Callable c | v = c.getAParameter() |
-      scopeFirst(c, bb) and
-      i = -1
-    )
-  }
-
-  predicate implicitEntryDef(
-    Callable c, PreBasicBlocks::PreBasicBlock bb, SsaInput::SourceVariable v
-  ) {
-    c = v.getACallable() and
-    scopeFirst(c, bb) and
-    (
-      not v instanceof LocalScopeVariable
-      or
-      v.(SimpleLocalScopeVariable).isReadonlyCapturedBy(c)
-    )
-  }
-
-  /** Holds if `a` is assigned in callable `c`. */
-  pragma[nomagic]
-  private predicate assignableDefinition(Assignable a, Callable c) {
-    exists(AssignableDefinition def |
-      def.getTarget() = a and
-      c = def.getEnclosingCallable()
-    |
-      not c instanceof Constructor or
-      a instanceof LocalScopeVariable
-    )
-  }
-
-  pragma[nomagic]
-  private predicate assignableUniqueWriter(Assignable a, Callable c) {
-    c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
-  }
-
-  /** 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())
-  }
-
-  /**
-   * A local scope variable that is amenable to SSA analysis.
-   *
-   * This is either a local variable that is not captured, or one
-   * where all writes happen in the defining callable.
-   */
-  class SimpleLocalScopeVariable extends LocalScopeVariable {
-    SimpleLocalScopeVariable() { assignableUniqueWriter(this, this.getCallable()) }
-
-    /** Holds if this local scope variable is read-only captured by `c`. */
-    predicate isReadonlyCapturedBy(Callable c) {
-      assignableAccess(this, c) and
-      c != this.getCallable()
-    }
-  }
-
-  module SsaInput implements SsaImplCommon::InputSig<Location, PreBasicBlocks::PreBasicBlock> {
-    private import semmle.code.csharp.Caching
-
-    private class ExitBasicBlock extends PreBasicBlocks::PreBasicBlock {
-      ExitBasicBlock() { scopeLast(_, this.getLastNode(), _) }
-    }
-
-    pragma[noinline]
-    private predicate assignableNoComplexQualifiers(Assignable a) {
-      forall(QualifiableExpr qe | qe.(AssignableAccess).getTarget() = a | qe.targetIsThisInstance())
-    }
-
-    /**
-     * A simple assignable. Either a local scope variable or a field/property
-     * that behaves like a local scope variable.
-     */
-    class SourceVariable extends Assignable {
-      private Callable c;
-
-      SourceVariable() {
-        assignableAccess(this, c) and
-        (
-          this instanceof SimpleLocalScopeVariable
-          or
-          (
-            this = any(Field f | not f.isVolatile())
-            or
-            this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
-          ) and
-          (
-            not assignableDefinition(this, _)
-            or
-            assignableUniqueWriter(this, c)
-          ) and
-          assignableNoComplexQualifiers(this)
-        )
-      }
-
-      /** Gets a callable in which this simple assignable can be analyzed. */
-      Callable getACallable() { result = c }
-    }
-
-    predicate variableWrite(
-      PreBasicBlocks::PreBasicBlock bb, int i, SourceVariable v, boolean certain
-    ) {
-      Stages::ControlFlowStage::forceCachingInSameStage() and
-      exists(AssignableDefinition def |
-        definitionAt(def, bb, i, v) and
-        if def.getTargetAccess().isRefArgument() then certain = false else certain = true
-      )
-      or
-      implicitEntryDef(_, bb, v) and
-      i = -1 and
-      certain = true
-    }
-
-    predicate variableRead(
-      PreBasicBlocks::PreBasicBlock bb, int i, SourceVariable v, boolean certain
-    ) {
-      exists(AssignableRead read |
-        read = bb.getNode(i) and
-        read.getTarget() = v and
-        certain = true
-      )
-      or
-      v =
-        any(LocalScopeVariable lsv |
-          lsv.getCallable() = bb.(ExitBasicBlock).getEnclosingCallable() and
-          i = bb.length() and
-          (lsv.isRef() or v.(Parameter).isOut()) and
-          certain = false
-        )
-    }
-  }
-
-  private module SsaImpl = SsaImplCommon::Make<Location, PreBasicBlocks::PreCfg, SsaInput>;
-
-  class Definition extends SsaImpl::Definition {
-    final AssignableRead getARead() {
-      exists(PreBasicBlocks::PreBasicBlock bb, int i |
-        SsaImpl::ssaDefReachesRead(_, this, bb, i) and
-        result = bb.getNode(i)
-      )
-    }
-
-    final AssignableDefinition getDefinition() {
-      exists(PreBasicBlocks::PreBasicBlock bb, int i, SsaInput::SourceVariable v |
-        this.definesAt(v, bb, i) and
-        definitionAt(result, bb, i, v)
-      )
-    }
-
-    final AssignableRead getAFirstRead() {
-      exists(PreBasicBlocks::PreBasicBlock bb, int i |
-        SsaImpl::firstUse(this, bb, i, true) and
-        result = bb.getNode(i)
-      )
-    }
-
-    private Definition getAPhiInputOrPriorDefinition() {
-      result = this.(PhiNode).getAnInput() or
-      SsaImpl::uncertainWriteDefinitionInput(this, result)
-    }
-
-    final Definition getAnUltimateDefinition() {
-      result = this.getAPhiInputOrPriorDefinition*() and
-      not result instanceof PhiNode
-    }
-
-    final predicate isLiveAtEndOfBlock(PreBasicBlocks::PreBasicBlock bb) {
-      SsaImpl::ssaDefReachesEndOfBlock(bb, this, _)
-    }
-
-    override Location getLocation() {
-      result = this.getDefinition().getLocation()
-      or
-      exists(Callable c, PreBasicBlocks::PreBasicBlock bb, SsaInput::SourceVariable v |
-        this.definesAt(v, bb, -1) and
-        implicitEntryDef(c, bb, v) and
-        result = c.getLocation()
-      )
-    }
-  }
-
-  class PhiNode extends SsaImpl::PhiNode, Definition {
-    final override Location getLocation() { result = this.getBasicBlock().getLocation() }
-
-    final Definition getAnInput() { SsaImpl::phiHasInputFromBlock(this, result, _) }
-  }
-
-  predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
-    exists(PreBasicBlocks::PreBasicBlock bb1, int i1, PreBasicBlocks::PreBasicBlock bb2, int i2 |
-      read1 = bb1.getNode(i1) and
-      SsaImpl::adjacentUseUse(bb1, i1, bb2, i2, _, true) and
-      read2 = bb2.getNode(i2)
-    )
-  }
-}

csharp/ql/lib/semmle/code/csharp/controlflow/internal/Splitting.qll

@@ -9,18 +9,11 @@ private import Completion as Comp
 private import Comp
 private import ControlFlowGraphImpl
 private import semmle.code.csharp.controlflow.ControlFlowGraph::ControlFlow as Cfg
-private import semmle.code.csharp.controlflow.internal.PreSsa
 
 cached
 private module Cached {
   private import semmle.code.csharp.Caching
 
-  cached
-  newtype TBooleanSplitSubKind =
-    TSsaBooleanSplitSubKind(PreSsa::Definition def) {
-      Stages::ControlFlowStage::forceCachingInSameStage()
-    }
-
   cached
   newtype TSplitKind = TConditionalCompletionSplitKind()
 

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

@@ -43,10 +43,47 @@ module BaseSsa {
     )
   }
 
-  private module SsaInput implements SsaImplCommon::InputSig<Location, ControlFlow::BasicBlock> {
-    private import semmle.code.csharp.controlflow.internal.PreSsa
+  /** Holds if `a` is assigned in callable `c`. */
+  pragma[nomagic]
+  private predicate assignableDefinition(Assignable a, Callable c) {
+    exists(AssignableDefinition def |
+      def.getTarget() = a and
+      c = def.getEnclosingCallable()
+    |
+      not c instanceof Constructor or
+      a instanceof LocalScopeVariable
+    )
+  }
 
-    class SourceVariable = PreSsa::SimpleLocalScopeVariable;
+  pragma[nomagic]
+  private predicate assignableUniqueWriter(Assignable a, Callable c) {
+    c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
+  }
+
+  /** 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())
+  }
+
+  /**
+   * A local scope variable that is amenable to SSA analysis.
+   *
+   * This is either a local variable that is not captured, or one
+   * where all writes happen in the defining callable.
+   */
+  class SimpleLocalScopeVariable extends LocalScopeVariable {
+    SimpleLocalScopeVariable() { assignableUniqueWriter(this, this.getCallable()) }
+
+    /** Holds if this local scope variable is read-only captured by `c`. */
+    predicate isReadonlyCapturedBy(Callable c) {
+      assignableAccess(this, c) and
+      c != this.getCallable()
+    }
+  }
+
+  private module SsaInput implements SsaImplCommon::InputSig<Location, ControlFlow::BasicBlock> {
+    class SourceVariable = SimpleLocalScopeVariable;
 
     predicate variableWrite(ControlFlow::BasicBlock bb, int i, SourceVariable v, boolean certain) {
       exists(AssignableDefinition def |

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

@@ -5,9 +5,9 @@
 import csharp
 private import codeql.ssa.Ssa as SsaImplCommon
 private import AssignableDefinitions
-private import semmle.code.csharp.controlflow.internal.PreSsa
 private import semmle.code.csharp.controlflow.BasicBlocks as BasicBlocks
 private import semmle.code.csharp.controlflow.Guards as Guards
+private import semmle.code.csharp.dataflow.internal.BaseSSA
 
 private module SsaInput implements SsaImplCommon::InputSig<Location, ControlFlow::BasicBlock> {
   class SourceVariable = Ssa::SourceVariable;
@@ -783,7 +783,7 @@ cached
 private module Cached {
   cached
   newtype TSourceVariable =
-    TLocalVar(Callable c, PreSsa::SimpleLocalScopeVariable v) {
+    TLocalVar(Callable c, BaseSsa::SimpleLocalScopeVariable v) {
       c = v.getCallable()
       or
       // Local scope variables can be captured

csharp/ql/test/library-tests/dataflow/defuse/defUseEquivalence.ql

@@ -1,9 +1,9 @@
 import csharp
-private import semmle.code.csharp.controlflow.internal.PreSsa
+private import semmle.code.csharp.dataflow.internal.BaseSSA
 
 /** "Naive" def-use implementation. */
 predicate defReaches(
-  AssignableDefinition def, PreSsa::SimpleLocalScopeVariable v, ControlFlow::Node cfn
+  AssignableDefinition def, BaseSsa::SimpleLocalScopeVariable v, ControlFlow::Node cfn
 ) {
   def.getTarget() = v and cfn = def.getExpr().getAControlFlowNode().getASuccessor()
   or

csharp/ql/test/library-tests/dataflow/defuse/parameterUseEquivalence.ql

@@ -1,10 +1,10 @@
 import csharp
-private import semmle.code.csharp.controlflow.internal.PreSsa
+private import semmle.code.csharp.dataflow.internal.BaseSSA
 
 /** "Naive" parameter-use implementation. */
 predicate parameterReaches(Parameter p, ControlFlow::Node cfn) {
   cfn = p.getCallable().getEntryPoint().getASuccessor() and
-  p instanceof PreSsa::SimpleLocalScopeVariable
+  p instanceof BaseSsa::SimpleLocalScopeVariable
   or
   exists(ControlFlow::Node mid | parameterReaches(p, mid) |
     not mid =

csharp/ql/test/library-tests/dataflow/defuse/useUseEquivalence.ql

@@ -1,9 +1,9 @@
 import csharp
-private import semmle.code.csharp.controlflow.internal.PreSsa
+private import semmle.code.csharp.dataflow.internal.BaseSSA
 
 /** "Naive" use-use implementation. */
 predicate useReaches(
-  LocalScopeVariableRead read, PreSsa::SimpleLocalScopeVariable v, ControlFlow::Node cfn
+  LocalScopeVariableRead read, BaseSsa::SimpleLocalScopeVariable v, ControlFlow::Node cfn
 ) {
   read.getTarget() = v and cfn = read.getAControlFlowNode().getASuccessor()
   or

csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.expected

@@ -1,3 +0,0 @@
-defReadInconsistency
-readReadInconsistency
-phiInconsistency

csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.ql

@@ -1,99 +0,0 @@
-import csharp
-import semmle.code.csharp.controlflow.internal.PreSsa
-import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
-import semmle.code.csharp.dataflow.internal.SsaImpl as SsaImpl
-
-class CallableWithSplitting extends Callable {
-  CallableWithSplitting() { this = any(SplitAstNode n).getEnclosingCallable() }
-}
-
-query predicate defReadInconsistency(
-  AssignableRead ar, Expr e, PreSsa::SsaInput::SourceVariable v, boolean b
-) {
-  // Exclude definitions in callables with CFG splitting, as SSA definitions may be
-  // very different from pre-SSA definitions
-  not ar.getEnclosingCallable() instanceof CallableWithSplitting and
-  exists(AssignableDefinition def | e = def.getExpr() |
-    b = true and
-    exists(PreSsa::Definition ssaDef | ssaDef.getSourceVariable() = v |
-      ar = ssaDef.getAFirstRead() and
-      ssaDef.getDefinition() = def and
-      not exists(Ssa::ExplicitDefinition edef |
-        edef.getADefinition() = def and
-        edef.getAFirstRead() = ar
-      )
-    )
-    or
-    b = false and
-    exists(Ssa::ExplicitDefinition edef |
-      edef.getADefinition() = def and
-      edef.getAFirstRead() = ar and
-      def.getTarget() = v and
-      not exists(PreSsa::Definition ssaDef |
-        ar = ssaDef.getAFirstRead() and
-        ssaDef.getDefinition() = def
-      )
-    )
-  )
-}
-
-query predicate readReadInconsistency(
-  LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SsaInput::SourceVariable v,
-  boolean b
-) {
-  // Exclude definitions in callables with CFG splitting, as SSA definitions may be
-  // very different from pre-SSA definitions
-  not read1.getEnclosingCallable() instanceof CallableWithSplitting and
-  (
-    b = true and
-    v = read1.getTarget() and
-    PreSsa::adjacentReadPairSameVar(read1, read2) and
-    not SsaImpl::adjacentReadPairSameVar(_, read1.getAControlFlowNode(), read2.getAControlFlowNode())
-    or
-    b = false and
-    v = read1.getTarget() and
-    SsaImpl::adjacentReadPairSameVar(_, read1.getAControlFlowNode(), read2.getAControlFlowNode()) and
-    read1.getTarget() instanceof PreSsa::SsaInput::SourceVariable and
-    not PreSsa::adjacentReadPairSameVar(read1, read2) and
-    // Exclude split CFG elements because SSA may be more precise than pre-SSA
-    // in those cases
-    not read1 instanceof SplitAstNode and
-    not read2 instanceof SplitAstNode
-  )
-}
-
-query predicate phiInconsistency(
-  ControlFlowElement cfe, Expr e, PreSsa::SsaInput::SourceVariable v, boolean b
-) {
-  // Exclude definitions in callables with CFG splitting, as SSA definitions may be
-  // very different from pre-SSA definitions
-  not cfe.getEnclosingCallable() instanceof CallableWithSplitting and
-  exists(AssignableDefinition adef | e = adef.getExpr() |
-    b = true and
-    exists(PreSsa::PhiNode prePhi | v = prePhi.getSourceVariable() |
-      adef = prePhi.getAnInput+().getDefinition() and
-      cfe = prePhi.getBasicBlock().getFirstElement() and
-      not exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
-        edef = phi.getAnUltimateDefinition()
-      |
-        edef.getADefinition() = adef and
-        phi.definesAt(_, bb, _) and
-        cfe = bb.getFirstNode().getAstNode()
-      )
-    )
-    or
-    b = false and
-    exists(Ssa::PhiNode phi, ControlFlow::BasicBlock bb, Ssa::ExplicitDefinition edef |
-      v = phi.getSourceVariable().getAssignable()
-    |
-      edef = phi.getAnUltimateDefinition() and
-      edef.getADefinition() = adef and
-      phi.definesAt(_, bb, _) and
-      cfe = bb.getFirstNode().getAstNode() and
-      not exists(PreSsa::PhiNode prePhi |
-        adef = prePhi.getAnInput+().getDefinition() and
-        cfe = prePhi.getBasicBlock().getFirstElement()
-      )
-    )
-  )
-}