Merge pull request #4780 from hvitved/csharp/cfg/nested-finally

C#: Add missing CFG edges for nested `finally` blocks

Author: hvitved

csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll

@@ -23,11 +23,11 @@ import csharp
 private import semmle.code.csharp.commons.Assertions
 private import semmle.code.csharp.commons.Constants
 private import semmle.code.csharp.frameworks.System
+private import ControlFlowGraphImpl
 private import NonReturning
 private import SuccessorType
 private import SuccessorTypes
 
-// Internal representation of completions
 private newtype TCompletion =
   TSimpleCompletion() or
   TBooleanCompletion(boolean b) { b = true or b = false } or
@@ -40,26 +40,33 @@ private newtype TCompletion =
   TGotoCompletion(string label) { label = any(GotoStmt gs).getLabel() } or
   TThrowCompletion(ExceptionClass ec) or
   TExitCompletion() or
-  TNestedCompletion(Completion inner, Completion outer) {
-    inner instanceof NormalCompletion and
-    (
-      outer = TReturnCompletion()
-      or
-      outer = TBreakCompletion()
-      or
-      outer = TContinueCompletion()
-      or
-      outer = TGotoCompletion(_)
-      or
-      outer = TThrowCompletion(_)
-      or
-      outer = TExitCompletion()
-    )
-    or
+  TNestedCompletion(Completion inner, Completion outer, int nestLevel) {
     inner = TBreakCompletion() and
-    outer instanceof NonNestedNormalCompletion
+    outer instanceof NonNestedNormalCompletion and
+    nestLevel = 0
+    or
+    inner instanceof NormalCompletion and
+    nestedFinallyCompletion(outer, nestLevel)
   }
 
+pragma[noinline]
+private predicate nestedFinallyCompletion(Completion outer, int nestLevel) {
+  (
+    outer = TReturnCompletion()
+    or
+    outer = TBreakCompletion()
+    or
+    outer = TContinueCompletion()
+    or
+    outer = TGotoCompletion(_)
+    or
+    outer = TThrowCompletion(_)
+    or
+    outer = TExitCompletion()
+  ) and
+  nestLevel = any(Statements::TryStmtTree t).nestLevel()
+}
+
 pragma[noinline]
 private predicate completionIsValidForStmt(Stmt s, Completion c) {
   s instanceof BreakStmt and
@@ -674,21 +681,25 @@ class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
 class NestedCompletion extends Completion, TNestedCompletion {
   Completion inner;
   Completion outer;
+  int nestLevel;
 
-  NestedCompletion() { this = TNestedCompletion(inner, outer) }
+  NestedCompletion() { this = TNestedCompletion(inner, outer, nestLevel) }
 
   /** Gets a completion that is compatible with the inner completion. */
   Completion getAnInnerCompatibleCompletion() {
     result.getOuterCompletion() = this.getInnerCompletion()
   }
 
+  /** Gets the level of this nested completion. */
+  int getNestLevel() { result = nestLevel }
+
   override Completion getInnerCompletion() { result = inner }
 
   override Completion getOuterCompletion() { result = outer }
 
   override SuccessorType getAMatchingSuccessorType() { none() }
 
-  override string toString() { result = outer + " [" + inner + "]" }
+  override string toString() { result = outer + " [" + inner + "] (" + nestLevel + ")" }
 }
 
 /**
@@ -725,13 +736,13 @@ class NestedBreakCompletion extends NormalCompletion, NestedCompletion {
 
   override BreakCompletion getInnerCompletion() { result = inner }
 
-  override SimpleCompletion getOuterCompletion() { result = outer }
+  override NonNestedNormalCompletion getOuterCompletion() { result = outer }
 
   override Completion getAnInnerCompatibleCompletion() {
     result = inner and
     outer = TSimpleCompletion()
     or
-    result = TNestedCompletion(outer, inner)
+    result = TNestedCompletion(outer, inner, _)
   }
 
   override SuccessorType getAMatchingSuccessorType() {
@@ -749,7 +760,7 @@ class NestedBreakCompletion extends NormalCompletion, NestedCompletion {
 class ReturnCompletion extends Completion {
   ReturnCompletion() {
     this = TReturnCompletion() or
-    this = TNestedCompletion(_, TReturnCompletion())
+    this = TNestedCompletion(_, TReturnCompletion(), _)
   }
 
   override ReturnSuccessor getAMatchingSuccessorType() { any() }
@@ -768,7 +779,7 @@ class ReturnCompletion extends Completion {
 class BreakCompletion extends Completion {
   BreakCompletion() {
     this = TBreakCompletion() or
-    this = TNestedCompletion(_, TBreakCompletion())
+    this = TNestedCompletion(_, TBreakCompletion(), _)
   }
 
   override BreakSuccessor getAMatchingSuccessorType() { any() }
@@ -787,7 +798,7 @@ class BreakCompletion extends Completion {
 class ContinueCompletion extends Completion {
   ContinueCompletion() {
     this = TContinueCompletion() or
-    this = TNestedCompletion(_, TContinueCompletion())
+    this = TNestedCompletion(_, TContinueCompletion(), _)
   }
 
   override ContinueSuccessor getAMatchingSuccessorType() { any() }
@@ -807,7 +818,7 @@ class GotoCompletion extends Completion {
 
   GotoCompletion() {
     this = TGotoCompletion(label) or
-    this = TNestedCompletion(_, TGotoCompletion(label))
+    this = TNestedCompletion(_, TGotoCompletion(label), _)
   }
 
   /** Gets the label of the `goto` completion. */
@@ -830,7 +841,7 @@ class ThrowCompletion extends Completion {
 
   ThrowCompletion() {
     this = TThrowCompletion(ec) or
-    this = TNestedCompletion(_, TThrowCompletion(ec))
+    this = TNestedCompletion(_, TThrowCompletion(ec), _)
   }
 
   /** Gets the type of the exception being thrown. */
@@ -856,7 +867,7 @@ class ThrowCompletion extends Completion {
 class ExitCompletion extends Completion {
   ExitCompletion() {
     this = TExitCompletion() or
-    this = TNestedCompletion(_, TExitCompletion())
+    this = TNestedCompletion(_, TExitCompletion(), _)
   }
 
   override ExitSuccessor getAMatchingSuccessorType() { any() }

csharp/ql/src/semmle/code/csharp/controlflow/internal/ControlFlowGraphImpl.qll

@@ -858,6 +858,7 @@ module Expressions {
         (cc.(MatchingCompletion).isNonMatch() or cc instanceof FalseCompletion) and
         c =
           any(NestedCompletion nc |
+            nc.getNestLevel() = 0 and
             nc.getInnerCompletion() = cc and
             nc.getOuterCompletion()
                 .(ThrowCompletion)
@@ -1300,13 +1301,53 @@ module Statements {
     last(cc.getBlock(), result, c)
   }
 
+  /** Gets a child of `cfe` that is in CFG scope `scope`. */
+  pragma[noinline]
+  private ControlFlowElement getAChildInScope(ControlFlowElement cfe, Callable scope) {
+    result = cfe.getAChild() and
+    scope = result.getEnclosingCallable()
+  }
+
   class TryStmtTree extends PreOrderTree, TryStmt {
     ControlFlowTree body;
 
     final override predicate propagatesAbnormal(ControlFlowElement child) {
       child = this.getFinally()
     }
 
+    /**
+     * Gets a descendant that belongs to the `finally` block of this try statement.
+     */
+    ControlFlowElement getAFinallyDescendant() {
+      result = this.getFinally()
+      or
+      exists(ControlFlowElement mid |
+        mid = this.getAFinallyDescendant() and
+        result = getAChildInScope(mid, mid.getEnclosingCallable()) and
+        not exists(TryStmtTree nestedTry |
+          result = nestedTry.getFinally() and
+          nestedTry != this
+        )
+      )
+    }
+
+    /**
+     * Holds if `innerTry` has a `finally` block and is immediately nested inside the
+     * `finally` block of this `try` statement.
+     */
+    private predicate nestedFinally(TryStmtTree innerTry) {
+      exists(ControlFlowElement innerFinally |
+        innerFinally = getAChildInScope(this.getAFinallyDescendant(), this.getEnclosingCallable()) and
+        innerFinally = innerTry.getFinally()
+      )
+    }
+
+    /**
+     * Gets the `finally`-nesting level of this `try` statement. That is, the number of
+     * `finally` blocks that this `try` statement is nested under.
+     */
+    int nestLevel() { result = count(TryStmtTree outer | outer.nestedFinally+(this)) }
+
     /** Holds if `last` is a last element of the block of this `try` statement. */
     pragma[nomagic]
     predicate lastBlock(ControlFlowElement last, Completion c) { last(this.getBlock(), last, c) }
@@ -1343,10 +1384,11 @@ module Statements {
 
     pragma[nomagic]
     private predicate lastFinally(
-      ControlFlowElement last, NormalCompletion finally, Completion outer
+      ControlFlowElement last, NormalCompletion finally, Completion outer, int nestLevel
     ) {
       this.lastFinally0(last, finally) and
-      exists(this.getBlockOrCatchFinallyPred(any(Completion c0 | outer = c0.getOuterCompletion())))
+      exists(this.getBlockOrCatchFinallyPred(any(Completion c0 | outer = c0.getOuterCompletion()))) and
+      nestLevel = this.nestLevel()
     }
 
     final override predicate last(ControlFlowElement last, Completion c) {
@@ -1360,13 +1402,14 @@ module Statements {
         c instanceof ExitCompletion
       )
       or
-      this.lastFinally(last, c, any(NormalCompletion nc))
+      this.lastFinally(last, c, any(NormalCompletion nc), _)
       or
       // If the `finally` block completes normally, it inherits any non-normal
       // completion that was current before the `finally` block was entered
       c =
         any(NestedCompletion nc |
-          this.lastFinally(last, nc.getAnInnerCompatibleCompletion(), nc.getOuterCompletion())
+          this.lastFinally(last, nc.getAnInnerCompatibleCompletion(), nc.getOuterCompletion(),
+            nc.getNestLevel())
         )
     }
 
@@ -1481,6 +1524,7 @@ module Statements {
       this.isLast() and
       c =
         any(NestedCompletion nc |
+          nc.getNestLevel() = 0 and
           this.throwMayBeUncaught(nc.getOuterCompletion().(ThrowCompletion)) and
           (
             // Incompatible exception type: clause itself