Merge pull request #116 from microsoft/powershell-add-empty-completion

PS: Add `Emptiness` completion 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

powershell/ql/test/library-tests/controlflow/graph/Cfg.expected

@@ -276,8 +276,8 @@
 | functions.ps1:28:5:28:13 | ...=... | functions.ps1:28:5:28:9 | sum |  |
 | functions.ps1:28:12:28:13 | 0 | functions.ps1:28:12:28:13 | 0 |  |
 | functions.ps1:28:12:28:13 | 0 | functions.ps1:29:25:29:33 | numbers |  |
-| functions.ps1:29:5:32:6 | forach(... in ...) | functions.ps1:29:14:29:21 | number |  |
-| functions.ps1:29:5:32:6 | forach(... in ...) | functions.ps1:33:5:33:9 | sum |  |
+| functions.ps1:29:5:32:6 | forach(... in ...) | functions.ps1:29:14:29:21 | number | non-empty |
+| functions.ps1:29:5:32:6 | forach(... in ...) | functions.ps1:33:5:33:9 | sum | empty |
 | functions.ps1:29:14:29:21 | number | functions.ps1:29:35:32:6 | {...} |  |
 | functions.ps1:29:25:29:33 | numbers | functions.ps1:29:5:32:6 | forach(... in ...) |  |
 | functions.ps1:29:25:29:33 | numbers | functions.ps1:29:25:29:33 | numbers |  |
@@ -480,8 +480,8 @@
 | loops.ps1:51:5:51:11 | ...=... | loops.ps1:51:5:51:7 | a |  |
 | loops.ps1:51:10:51:11 | 0 | loops.ps1:51:10:51:11 | 0 |  |
 | loops.ps1:51:10:51:11 | 0 | loops.ps1:52:25:52:37 | letterArray |  |
-| loops.ps1:52:5:55:6 | forach(... in ...) | loops.ps1:49:23:56:2 | exit {...} (normal) |  |
-| loops.ps1:52:5:55:6 | forach(... in ...) | loops.ps1:52:14:52:21 | letter |  |
+| loops.ps1:52:5:55:6 | forach(... in ...) | loops.ps1:49:23:56:2 | exit {...} (normal) | empty |
+| loops.ps1:52:5:55:6 | forach(... in ...) | loops.ps1:52:14:52:21 | letter | non-empty |
 | loops.ps1:52:14:52:21 | letter | loops.ps1:53:5:55:6 | {...} |  |
 | loops.ps1:52:25:52:37 | letterArray | loops.ps1:52:5:55:6 | forach(... in ...) |  |
 | loops.ps1:52:25:52:37 | letterArray | loops.ps1:52:25:52:37 | letterArray |  |