PS: Add an emptiness successor to get rid of CFG inconsistencies.

Author: MathiasVP

powershell/ql/lib/semmle/code/powershell/controlflow/ControlFlowGraph.qll

@@ -108,6 +108,15 @@ module SuccessorTypes {
   class ExitSuccessor extends SuccessorType, CfgImpl::TExitSuccessor {
     final override string toString() { result = "exit" }
   }
+
+  class EmptinessSuccessor extends ConditionalSuccessor, CfgImpl::TEmptinessSuccessor {
+    EmptinessSuccessor() { this = CfgImpl::TEmptinessSuccessor(value) }
+
+    /** Holds if this is an empty successor. */
+    predicate isEmpty() { value = true }
+
+    override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }
+  }
 }
 
 class Split = Splitting::Split;

powershell/ql/lib/semmle/code/powershell/controlflow/internal/Completion.qll

@@ -19,7 +19,8 @@ private newtype TCompletion =
   TContinueCompletion() or
   TThrowCompletion() or
   TExitCompletion() or
-  TMatchingCompletion(Boolean b)
+  TMatchingCompletion(Boolean b) or
+  TEmptinessCompletion(Boolean isEmpty)
 
 private predicate commandThrows(Cmd c, boolean unconditional) {
   c.getNamedArgument("ErrorAction").(StringConstExpr).getValue().getValue() = "Stop" and
@@ -68,6 +69,9 @@ abstract class Completion extends TCompletion {
       not isMatchingConstant(n, _) and
       this = TMatchingCompletion(_)
     )
+    or
+    mustHaveEmptinessCompletion(n) and
+    this = TEmptinessCompletion(_)
   }
 
   private predicate isValidForSpecific(Ast n) { this.isValidForSpecific0(n) }
@@ -183,6 +187,12 @@ private predicate inMatchingContext(Ast n) {
   n = any(CatchClause cc).getACatchType()
 }
 
+/**
+ * Holds if a normal completion of `cfe` must be an emptiness completion. Thats is,
+ * whether `cfe` determines whether to execute the body of a `foreach` statement.
+ */
+private predicate mustHaveEmptinessCompletion(Ast n) { n instanceof ForEachStmt }
+
 /**
  * A completion that represents normal evaluation of a statement or an
  * expression.
@@ -296,3 +306,20 @@ class ExitCompletion extends Completion, TExitCompletion {
 
   override string toString() { result = "exit" }
 }
+
+/**
+ * A completion that represents evaluation of an emptiness test, for example
+ * a test in a `foreach` statement.
+ */
+class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
+  EmptinessCompletion() { this = TEmptinessCompletion(value) }
+
+  /** Holds if the emptiness test evaluates to `true`. */
+  predicate isEmpty() { value = true }
+
+  EmptinessCompletion getDual() { result = TEmptinessCompletion(value.booleanNot()) }
+
+  override EmptinessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
+
+  override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }
+}

powershell/ql/lib/semmle/code/powershell/controlflow/internal/ControlFlowGraphImpl.qll

@@ -404,7 +404,7 @@ module Trees {
     final override predicate last(AstNode last, Completion c) {
       // Emptiness test exits with no more elements
       last = this and
-      completionIsSimple(c)
+      c.(EmptinessCompletion).isEmpty()
       or
       super.last(last, c)
     }
@@ -418,7 +418,7 @@ module Trees {
       // Emptiness test to variable declaration
       pred = this and
       first(super.getVarAccess(), succ) and
-      completionIsSimple(c)
+      c = any(EmptinessCompletion ec | not ec.isEmpty())
       or
       // Variable declaration to body
       last(super.getVarAccess(), pred, c) and
@@ -779,7 +779,8 @@ private module Cached {
     TContinueSuccessor() or
     TThrowSuccessor() or
     TExitSuccessor() or
-    TMatchingSuccessor(Boolean b)
+    TMatchingSuccessor(Boolean b) or
+    TEmptinessSuccessor(Boolean b)
 }
 
 import Cached