Swift: Fix CFG inconsistencies with StmtConditions.

Author: MathiasVP

swift/ql/lib/codeql/swift/controlflow/internal/Completion.qll

@@ -119,7 +119,7 @@ private predicate inBooleanContext(ControlFlowElement n) {
 }
 
 private predicate astInBooleanContext(AstNode n) {
-  n = any(ConditionElement condElem).getFullyUnresolved()
+  n = any(ConditionElement condElem).getBoolean().getFullyUnresolved()
   or
   n = any(StmtCondition stmtCond).getFullyUnresolved()
   or
@@ -160,9 +160,7 @@ private predicate astInBooleanContext(AstNode n) {
  * Holds if a normal completion of `ast` must be a matching completion. Thats is,
  * whether `ast` determines a match in a `switch` or `catch` statement.
  */
-private predicate mustHaveMatchingCompletion(AstNode ast) {
-  switchMatching(_, _, ast) or catchMatching(_, _, ast)
-}
+private predicate mustHaveMatchingCompletion(AstNode ast) { ast instanceof Pattern }
 
 /**
  * Holds if `ast` must have a matching completion, and `e` is the fully converted
@@ -180,30 +178,11 @@ private predicate mustHaveMatchingCompletion(Expr e, AstNode ast) {
  * case `c`, belonging to `switch` statement `switch`.
  */
 private predicate switchMatching(SwitchStmt switch, CaseStmt c, AstNode ast) {
-  switchMatchingCaseLabelItem(switch, c, ast)
-  or
-  switchMatchingPattern(switch, c, ast)
-}
-
-/**
- * Holds if `cli` a top-level pattern of case `c`, belonging
- * to `switch` statement `switch`.
- */
-private predicate switchMatchingCaseLabelItem(SwitchStmt switch, CaseStmt c, CaseLabelItem cli) {
   switch.getACase() = c and
-  c.getALabel() = cli
-}
-
-/**
- * Holds if `pattern` is a sub-pattern of the pattern in case
- * statement `c` of the `switch` statement `switch`.
- */
-private predicate switchMatchingPattern(SwitchStmt s, CaseStmt c, Pattern pattern) {
-  s.getACase() = c and
-  exists(CaseLabelItem cli | switchMatching(s, c, cli) |
-    cli.getPattern() = pattern
+  (
+    c.getALabel() = ast
     or
-    isSubPattern+(cli.getPattern(), pattern)
+    isSubPattern+(c.getALabel().getPattern(), ast)
   )
 }
 
@@ -455,6 +434,34 @@ class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
   override string toString() { if this.isMatch() then result = "match" else result = "no-match" }
 }
 
+class FalseOrNonMatchCompletion instanceof ConditionalCompletion {
+  FalseOrNonMatchCompletion() {
+    this instanceof FalseCompletion
+    or
+    this.(MatchingCompletion).isNonMatch()
+  }
+
+  string toString() {
+    result = this.(FalseCompletion).toString()
+    or
+    result = this.(MatchingCompletion).toString()
+  }
+}
+
+class TrueOrMatchCompletion instanceof ConditionalCompletion {
+  TrueOrMatchCompletion() {
+    this instanceof TrueCompletion
+    or
+    this.(MatchingCompletion).isMatch()
+  }
+
+  string toString() {
+    result = this.(TrueCompletion).toString()
+    or
+    result = this.(MatchingCompletion).toString()
+  }
+}
+
 class FallthroughCompletion extends Completion, TFallthroughCompletion {
   CaseStmt dest;
 

swift/ql/lib/codeql/swift/controlflow/internal/ControlFlowGraphImpl.qll

@@ -207,29 +207,70 @@ module Stmts {
     override FailStmt ast;
   }
 
-  private class StmtConditionTree extends AstPostOrderTree {
+  private class StmtConditionTree extends AstPreOrderTree {
     override StmtCondition ast;
 
     final override predicate propagatesAbnormal(ControlFlowElement child) {
-      child.asAstNode() = ast.getAnElement().getUnderlyingCondition()
+      child.asAstNode() = ast.getAnElement().getInitializer().getFullyConverted()
+      or
+      child.asAstNode() = ast.getAnElement().getPattern().getFullyUnresolved()
+      or
+      child.asAstNode() = ast.getAnElement().getBoolean().getFullyConverted()
     }
 
-    final override predicate first(ControlFlowElement first) {
-      astFirst(ast.getFirstElement().getUnderlyingCondition().getFullyUnresolved(), first)
+    predicate firstElement(int i, ControlFlowElement first) {
+      // If there is an initializer in the first element, evaluate that first
+      astFirst(ast.getElement(i).getInitializer().getFullyConverted(), first)
+      or
+      // Otherwise, the first element is a boolean condition.
+      not exists(ast.getElement(i).getInitializer()) and
+      astFirst(ast.getElement(i).getBoolean().getFullyConverted(), first)
     }
 
-    final override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
-      // Left-to-right evaluation of elements
-      exists(int i |
-        astLast(ast.getElement(i).getUnderlyingCondition().getFullyUnresolved(), pred, c) and
-        c instanceof NormalCompletion and
-        astFirst(ast.getElement(i + 1).getUnderlyingCondition().getFullyUnresolved(), succ)
-      )
+    predicate succElement(int i, ControlFlowElement pred, ControlFlowElement succ, Completion c) {
+      // Evaluate the pattern after the initializer
+      astLast(ast.getElement(i).getInitializer().getFullyConverted(), pred, c) and
+      c instanceof NormalCompletion and
+      astFirst(ast.getElement(i).getPattern().getFullyUnresolved(), succ)
       or
-      // Post-order: flow from thrown expression to the throw statement.
-      astLast(ast.getLastElement().getUnderlyingCondition().getFullyUnresolved(), pred, c) and
+      (
+        // After evaluating the pattern
+        astLast(ast.getElement(i).getPattern().getFullyUnresolved(), pred, c)
+        or
+        // ... or the boolean ...
+        astLast(ast.getElement(i).getBoolean().getFullyConverted(), pred, c)
+      ) and
+      // We evaluate the next element
       c instanceof NormalCompletion and
-      succ.asAstNode() = ast
+      this.firstElement(i + 1, succ)
+    }
+
+    final override predicate last(ControlFlowElement last, Completion c) {
+      // Stop if a boolean check failed
+      astLast(ast.getAnElement().getBoolean().getFullyConverted(), last, c) and
+      c instanceof FalseCompletion
+      or
+      // Stop is a pattern match failed
+      astLast(ast.getAnElement().getPattern().getFullyUnresolved(), last, c) and
+      not c.(MatchingCompletion).isMatch()
+      or
+      // Stop if we sucesfully evaluated all the conditionals
+      (
+        astLast(ast.getLastElement().getBoolean().getFullyConverted(), last, c)
+        or
+        astLast(ast.getLastElement().getPattern().getFullyUnresolved(), last, c)
+      ) and
+      c instanceof NormalCompletion
+    }
+
+    final override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
+      // Pre-order: Flow from this ast node to the first condition
+      pred.asAstNode() = ast and
+      c instanceof SimpleCompletion and
+      this.firstElement(0, succ)
+      or
+      // Left-to-right evaluation of elements
+      succElement(_, pred, succ, c)
     }
   }
 
@@ -245,7 +286,7 @@ module Stmts {
     final override predicate last(ControlFlowElement last, Completion c) {
       // Condition exits with a false completion and there is no `else` branch
       astLast(ast.getCondition().getFullyUnresolved(), last, c) and
-      c instanceof FalseCompletion and
+      c instanceof FalseOrNonMatchCompletion and
       not exists(ast.getElse())
       or
       // Then/Else branch exits with any completion
@@ -261,10 +302,12 @@ module Stmts {
       astLast(ast.getCondition().getFullyUnresolved(), pred, c) and
       (
         // Flow from last element of condition to first element of then branch
-        c instanceof TrueCompletion and astFirst(ast.getThen(), succ)
+        c instanceof TrueOrMatchCompletion and
+        astFirst(ast.getThen(), succ)
         or
         // Flow from last element of condition to first element of else branch
-        c instanceof FalseCompletion and astFirst(ast.getElse(), succ)
+        c instanceof FalseOrNonMatchCompletion and
+        astFirst(ast.getElse(), succ)
       )
     }
   }
@@ -284,7 +327,7 @@ module Stmts {
       or
       // Exit when a condition is true
       astLast(ast.getCondition().getFullyUnresolved(), last, c) and
-      c instanceof TrueCompletion
+      c instanceof TrueOrMatchCompletion
     }
 
     final override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
@@ -295,7 +338,7 @@ module Stmts {
       or
       // Flow to the body when the condition is false
       astLast(ast.getCondition().getFullyUnresolved(), pred, c) and
-      c instanceof FalseCompletion and
+      c instanceof FalseOrNonMatchCompletion and
       astFirst(ast.getBody(), succ)
     }
   }
@@ -322,7 +365,7 @@ module Stmts {
       final override predicate last(ControlFlowElement last, Completion c) {
         // Condition exits with a false completion
         last(this.getCondition(), last, c) and
-        c instanceof FalseCompletion
+        c instanceof FalseOrNonMatchCompletion
         or
         // Body exits with a break completion
         exists(BreakCompletion break |
@@ -339,7 +382,7 @@ module Stmts {
 
       override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
         last(this.getCondition(), pred, c) and
-        c instanceof TrueCompletion and
+        c instanceof TrueOrMatchCompletion and
         first(this.getBody(), succ)
         or
         last(this.getBody(), pred, c) and
@@ -484,9 +527,8 @@ module Stmts {
       astLast(ast.getExpr().getFullyConverted(), last, c) and
       c instanceof NormalCompletion
       or
-      // A statement exits (TODO: with a `break` completion?)
-      astLast(ast.getACase().getBody(), last, c) and
-      c instanceof NormalCompletion
+      // A statement exits
+      astLast(ast.getACase().getBody(), last, c)
       // Note: There's no need for an exit with a non-match as
       // Swift's switch statements are always exhaustive.
     }
@@ -849,7 +891,7 @@ module Patterns {
       or
       // Or we got to the some/none check and it failed
       n.asAstNode() = ast and
-      not c.(MatchingCompletion).isMatch()
+      c.(MatchingCompletion).isNonMatch()
     }
 
     override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {

swift/ql/lib/codeql/swift/controlflow/internal/Scope.qll

@@ -194,7 +194,16 @@ private module Cached {
       result = guard.getCondition()
     )
     or
-    result = ast.(StmtCondition).getElement(index).getUnderlyingCondition()
+    exists(StmtCondition stmtCond | stmtCond = ast |
+      index = 0 and
+      result = stmtCond.getElement(index).getPattern()
+      or
+      index = 1 and
+      result = stmtCond.getElement(index).getInitializer()
+      or
+      index = 2 and
+      result = stmtCond.getElement(index).getBoolean()
+    )
     or
     exists(IfStmt ifStmt | ifStmt = ast |
       index = 0 and

swift/ql/lib/codeql/swift/elements/stmt/ConditionElement.qll

@@ -2,13 +2,9 @@ private import codeql.swift.generated.stmt.ConditionElement
 private import codeql.swift.elements.AstNode
 
 class ConditionElement extends ConditionElementBase {
-  AstNode getUnderlyingCondition() {
-    result = this.getBoolean()
+  override string toString() {
+    result = this.getBoolean().toString()
     or
-    result = this.getInitializer()
-    or
-    result = this.getPattern()
+    result = this.getPattern().toString() + " = ... "
   }
-
-  override string toString() { result = this.getUnderlyingCondition().toString() }
 }

swift/ql/test/extractor-tests/statements/ConditionElements.expected

@@ -1,11 +1,7 @@
 | main.swift:3:8:3:13 | ... call to == ... | main.swift:3:8:3:13 | ... call to == ... |
 | main.swift:10:17:10:24 | ... call to < ... | main.swift:10:18:10:22 | ... call to < ... |
 | main.swift:39:9:39:14 | ... call to != ... | main.swift:39:9:39:14 | ... call to != ... |
-| main.swift:65:4:65:19 | let ... | main.swift:65:9:65:15 | let ... |
-| main.swift:65:4:65:19 | let ... | main.swift:65:19:65:19 | x |
-| main.swift:65:4:65:19 | x | main.swift:65:9:65:15 | let ... |
-| main.swift:65:4:65:19 | x | main.swift:65:19:65:19 | x |
-| main.swift:67:4:67:20 | .some(...) | main.swift:67:9:67:16 | .some(...) |
-| main.swift:67:4:67:20 | .some(...) | main.swift:67:20:67:20 | x |
-| main.swift:67:4:67:20 | x | main.swift:67:9:67:16 | .some(...) |
-| main.swift:67:4:67:20 | x | main.swift:67:20:67:20 | x |
+| main.swift:65:4:65:19 | let ... = ...  | main.swift:65:9:65:15 | let ... |
+| main.swift:65:4:65:19 | let ... = ...  | main.swift:65:19:65:19 | x |
+| main.swift:67:4:67:20 | .some(...) = ...  | main.swift:67:9:67:16 | .some(...) |
+| main.swift:67:4:67:20 | .some(...) = ...  | main.swift:67:20:67:20 | x |