Merge pull request #64 from github/hvitved/cfg/rescue

Implement CFG logic for `rescue-ensure`
2026-02-20 08:53:49 +01:00 · 2020-12-15 11:43:14 +01:00
parent b76f97d337 a76e6848c7
commit 5108b369e1
10 changed files with 4474 additions and 1562 deletions
--- a/ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll
+++ b/ql/src/codeql_ruby/controlflow/ControlFlowGraph.qll
@@ -186,12 +186,17 @@ module SuccessorTypes {

  /**
   * A conditional control flow successor. Either a Boolean successor (`BooleanSuccessor`),
-   * or an emptiness successor (`EmptinessSuccessor`).
+   * an emptiness successor (`EmptinessSuccessor`), or a matching successor
+   * (`MatchingSuccessor`)
   */
  class ConditionalSuccessor extends SuccessorType {
    boolean value;

-    ConditionalSuccessor() { this = TBooleanSuccessor(value) or this = TEmptinessSuccessor(value) }
+    ConditionalSuccessor() {
+      this = TBooleanSuccessor(value) or
+      this = TEmptinessSuccessor(value) or
+      this = TMatchingSuccessor(value)
+    }

    /** Gets the Boolean value of this successor. */
    final boolean getValue() { result = value }
@@ -248,12 +253,38 @@ module SuccessorTypes {
   * ```
   */
  class EmptinessSuccessor extends ConditionalSuccessor, TEmptinessSuccessor {
-    /** Holds if this is an empty successor. */
-    predicate isEmpty() { value = true }
+    override string toString() { if value = true then result = "empty" else result = "non-empty" }
+  }

-    final override string toString() {
-      if this.isEmpty() then result = "empty" else result = "non-empty"
-    }
+  /**
+   * A matching control flow successor.
+   *
+   * For example, this program fragment:
+   *
+   * ```rb
+   * case x
+   *   when 1 then puts "one"
+   *   else puts "not one"
+   * end
+   * ```
+   *
+   * has a control flow graph containing matching successors:
+   *
+   * ```
+   *            x
+   *            |
+   *            1
+   *           / \
+   *          /   \
+   *         /     \
+   *        /       \
+   *     match    non-match
+   *       |          |
+   *  puts "one"  puts "not one"
+   * ```
+   */
+  class MatchingSuccessor extends ConditionalSuccessor, TMatchingSuccessor {
+    override string toString() { if value = true then result = "match" else result = "no-match" }
  }

  /**
--- a/ql/src/codeql_ruby/controlflow/internal/Cfg.ql
+++ b/ql/src/codeql_ruby/controlflow/internal/Cfg.ql
@@ -1,3 +1,7 @@
+/**
+ * @kind graph
+ */
+
 import codeql_ruby.controlflow.ControlFlowGraph

 query predicate nodes(CfgNode n) { any() }
@@ -5,6 +9,6 @@ query predicate nodes(CfgNode n) { any() }
 query predicate edges(CfgNode pred, CfgNode succ, string attr, string val) {
  exists(SuccessorType t | succ = pred.getASuccessor(t) |
    attr = "semmle.label" and
-    val = t.toString()
+    if t instanceof SuccessorTypes::NormalSuccessor then val = "" else val = t.toString()
  )
 }
--- a/ql/src/codeql_ruby/controlflow/internal/Completion.qll
+++ b/ql/src/codeql_ruby/controlflow/internal/Completion.qll
@@ -7,13 +7,15 @@
 private import codeql_ruby.ast.internal.TreeSitter::Generated
 private import codeql_ruby.controlflow.ControlFlowGraph
 private import AstNodes
+private import ControlFlowGraphImpl
 private import NonReturning
 private import SuccessorTypes

 private newtype TCompletion =
  TSimpleCompletion() or
-  TBooleanCompletion(boolean b) { b = true or b = false } or
-  TEmptinessCompletion(boolean isEmpty) { isEmpty = true or isEmpty = false } or
+  TBooleanCompletion(boolean b) { b in [false, true] } or
+  TEmptinessCompletion(boolean isEmpty) { isEmpty in [false, true] } or
+  TMatchingCompletion(boolean isMatch) { isMatch in [false, true] } or
  TReturnCompletion() or
  TBreakCompletion() or
  TNextCompletion() or
@@ -21,11 +23,35 @@ private newtype TCompletion =
  TRetryCompletion() or
  TRaiseCompletion() or // TODO: Add exception type?
  TExitCompletion() or
-  TNestedCompletion(Completion inner, Completion outer) {
-    outer = TSimpleCompletion() and
-    inner = TBreakCompletion()
+  TNestedCompletion(Completion inner, Completion outer, int nestLevel) {
+    inner = TBreakCompletion() and
+    outer instanceof NonNestedNormalCompletion and
+    nestLevel = 0
+    or
+    inner instanceof NormalCompletion and
+    nestedEnsureCompletion(outer, nestLevel)
  }

+pragma[noinline]
+private predicate nestedEnsureCompletion(Completion outer, int nestLevel) {
+  (
+    outer = TReturnCompletion()
+    or
+    outer = TBreakCompletion()
+    or
+    outer = TNextCompletion()
+    or
+    outer = TRedoCompletion()
+    or
+    outer = TRetryCompletion()
+    or
+    outer = TRaiseCompletion()
+    or
+    outer = TExitCompletion()
+  ) and
+  nestLevel = any(Trees::RescueEnsureBlockTree t).nestLevel()
+}
+
 pragma[noinline]
 private predicate completionIsValidForStmt(AstNode n, Completion c) {
  n instanceof Break and
@@ -57,11 +83,15 @@ abstract class Completion extends TCompletion {
      this = TBooleanCompletion(_)
    )
    or
+    mustHaveMatchingCompletion(n) and
+    this = TMatchingCompletion(_)
+    or
    n = any(RescueModifier parent).getBody() and this = TRaiseCompletion()
    or
    not n instanceof NonReturningCall and
    not completionIsValidForStmt(n, _) and
    not mustHaveBooleanCompletion(n) and
+    not mustHaveMatchingCompletion(n) and
    this = TSimpleCompletion()
  }

@@ -140,7 +170,35 @@ private predicate inBooleanContext(AstNode n) {
  or
  n = any(ParenthesizedStatement parent | inBooleanContext(parent)).getChild()
  or
-  n instanceof Pattern
+  exists(Case c, When w |
+    not exists(c.getValue()) and
+    c.getChild(_) = w and
+    w.getPattern(_).getChild() = n
+  )
+}
+
+/**
+ * Holds if a normal completion of `n` must be a matching completion.
+ */
+private predicate mustHaveMatchingCompletion(AstNode n) {
+  inMatchingContext(n) and
+  not n instanceof NonReturningCall
+}
+
+/**
+ * Holds if `n` is used in a matching context. That is, whether or
+ * not the value of `n` matches, determines the successor.
+ */
+private predicate inMatchingContext(AstNode n) {
+  n = any(Rescue r).getExceptions().getChild(_)
+  or
+  exists(Case c, When w |
+    exists(c.getValue()) and
+    c.getChild(_) = w and
+    w.getPattern(_).getChild() = n
+  )
+  or
+  n.(Trees::DefaultValueParameterTree).hasDefaultValue()
 }

 /**
@@ -149,8 +207,10 @@ private predicate inBooleanContext(AstNode n) {
 */
 abstract class NormalCompletion extends Completion { }

+abstract private class NonNestedNormalCompletion extends NormalCompletion { }
+
 /** A simple (normal) completion. */
-class SimpleCompletion extends NormalCompletion, TSimpleCompletion {
+class SimpleCompletion extends NonNestedNormalCompletion, TSimpleCompletion {
  override NormalSuccessor getAMatchingSuccessorType() { any() }

  override string toString() { result = "simple" }
@@ -158,23 +218,26 @@ class SimpleCompletion extends NormalCompletion, TSimpleCompletion {

 /**
 * A completion that represents evaluation of an expression, whose value determines
- * the successor. Either a Boolean completion (`BooleanCompletion`)
- * or an emptiness completion (`EmptinessCompletion`).
+ * the successor. Either a Boolean completion (`BooleanCompletion`), an emptiness
+ * completion (`EmptinessCompletion`), or a matching completion (`MatchingCompletion`).
 */
-abstract class ConditionalCompletion extends NormalCompletion { }
+abstract class ConditionalCompletion extends NonNestedNormalCompletion {
+  boolean value;
+
+  bindingset[value]
+  ConditionalCompletion() { any() }
+
+  /** Gets the Boolean value of this conditional completion. */
+  final boolean getValue() { result = value }
+}

 /**
 * A completion that represents evaluation of an expression
 * with a Boolean value.
 */
 class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
-  private boolean value;
-
  BooleanCompletion() { this = TBooleanCompletion(value) }

-  /** Gets the Boolean value of this completion. */
-  boolean getValue() { result = value }
-
  /** Gets the dual Boolean completion. */
  BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }

@@ -198,84 +261,149 @@ class FalseCompletion extends BooleanCompletion {
 * a test in a `for in` statement.
 */
 class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
-  /** Holds if the emptiness test evaluates to `true`. */
-  predicate isEmpty() { this = TEmptinessCompletion(true) }
+  EmptinessCompletion() { this = TEmptinessCompletion(value) }

-  override EmptinessSuccessor getAMatchingSuccessorType() {
-    if isEmpty() then result.getValue() = true else result.getValue() = false
-  }
+  override EmptinessSuccessor getAMatchingSuccessorType() { result.getValue() = value }

-  override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }
+  override string toString() { if value = true then result = "empty" else result = "non-empty" }
+}
+
+/**
+ * A completion that represents evaluation of a matching test, for example
+ * a test in a `rescue` statement.
+ */
+class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
+  MatchingCompletion() { this = TMatchingCompletion(value) }
+
+  override MatchingSuccessor getAMatchingSuccessorType() { result.getValue() = value }
+
+  override string toString() { if value = true then result = "match" else result = "no-match" }
 }

 /**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a return.
 */
-class ReturnCompletion extends Completion, TReturnCompletion {
+class ReturnCompletion extends Completion {
+  ReturnCompletion() {
+    this = TReturnCompletion() or
+    this = TNestedCompletion(_, TReturnCompletion(), _)
+  }
+
  override ReturnSuccessor getAMatchingSuccessorType() { any() }

-  override string toString() { result = "return" }
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TReturnCompletion() and result = "return"
+  }
 }

 /**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a break from a loop.
 */
-class BreakCompletion extends Completion, TBreakCompletion {
+class BreakCompletion extends Completion {
+  BreakCompletion() {
+    this = TBreakCompletion() or
+    this = TNestedCompletion(_, TBreakCompletion(), _)
+  }
+
  override BreakSuccessor getAMatchingSuccessorType() { any() }

-  override string toString() { result = "break" }
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TBreakCompletion() and result = "break"
+  }
 }

 /**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a continuation of a loop.
 */
-class NextCompletion extends Completion, TNextCompletion {
+class NextCompletion extends Completion {
+  NextCompletion() {
+    this = TNextCompletion() or
+    this = TNestedCompletion(_, TNextCompletion(), _)
+  }
+
  override NextSuccessor getAMatchingSuccessorType() { any() }

-  override string toString() { result = "next" }
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TNextCompletion() and result = "next"
+  }
 }

 /**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a redo of a loop iteration.
 */
-class RedoCompletion extends Completion, TRedoCompletion {
+class RedoCompletion extends Completion {
+  RedoCompletion() {
+    this = TRedoCompletion() or
+    this = TNestedCompletion(_, TRedoCompletion(), _)
+  }
+
  override RedoSuccessor getAMatchingSuccessorType() { any() }

-  override string toString() { result = "redo" }
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TRedoCompletion() and result = "redo"
+  }
 }

 /**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a retry.
 */
-class RetryCompletion extends Completion, TRetryCompletion {
+class RetryCompletion extends Completion {
+  RetryCompletion() {
+    this = TRetryCompletion() or
+    this = TNestedCompletion(_, TRetryCompletion(), _)
+  }
+
  override RetrySuccessor getAMatchingSuccessorType() { any() }

-  override string toString() { result = "retry" }
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TRetryCompletion() and result = "retry"
+  }
 }

 /**
 * A completion that represents evaluation of a statement or an
 * expression resulting in a thrown exception.
 */
-class RaiseCompletion extends Completion, TRaiseCompletion {
+class RaiseCompletion extends Completion {
+  RaiseCompletion() {
+    this = TRaiseCompletion() or
+    this = TNestedCompletion(_, TRaiseCompletion(), _)
+  }
+
  override RaiseSuccessor getAMatchingSuccessorType() { any() }

-  override string toString() { result = "raise" }
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TRaiseCompletion() and result = "raise"
+  }
 }

 /**
 * A completion that represents evaluation of a statement or an
 * expression resulting in an abort/exit.
 */
-class ExitCompletion extends Completion, TExitCompletion {
+class ExitCompletion extends Completion {
+  ExitCompletion() {
+    this = TExitCompletion() or
+    this = TNestedCompletion(_, TExitCompletion(), _)
+  }
+
  override ExitSuccessor getAMatchingSuccessorType() { any() }

-  override string toString() { result = "exit" }
+  override string toString() {
+    // `NestedCompletion` defines `toString()` for the other case
+    this = TExitCompletion() and result = "exit"
+  }
 }

 /**
@@ -296,25 +424,60 @@ class ExitCompletion extends Completion, TExitCompletion {
 * the `while` loop can have a nested completion where the inner completion
 * is a `break` and the outer completion is a simple successor.
 */
-class NestedCompletion extends Completion, TNestedCompletion {
+abstract class NestedCompletion extends Completion, TNestedCompletion {
  Completion inner;
  Completion outer;
+  int nestLevel;

-  NestedCompletion() { this = TNestedCompletion(inner, outer) }
+  NestedCompletion() { this = TNestedCompletion(inner, outer, nestLevel) }

-  override Completion getInnerCompletion() { result = inner }
+  /** Gets a completion that is compatible with the inner completion. */
+  abstract Completion getAnInnerCompatibleCompletion();
+
+  /** Gets the level of this nested completion. */
+  final int getNestLevel() { result = nestLevel }
+
+  override string toString() { result = outer + " [" + inner + "] (" + nestLevel + ")" }
+}
+
+class NestedBreakCompletion extends NormalCompletion, NestedCompletion {
+  NestedBreakCompletion() {
+    inner = TBreakCompletion() and
+    outer instanceof NonNestedNormalCompletion
+  }
+
+  override BreakCompletion getInnerCompletion() { result = inner }
+
+  override NonNestedNormalCompletion getOuterCompletion() { result = outer }
+
+  override Completion getAnInnerCompatibleCompletion() {
+    result = inner and
+    outer = TSimpleCompletion()
+    or
+    result = TNestedCompletion(outer, inner, _)
+  }
+
+  override SuccessorType getAMatchingSuccessorType() {
+    outer instanceof SimpleCompletion and
+    result instanceof BreakSuccessor
+    or
+    result = outer.(ConditionalCompletion).getAMatchingSuccessorType()
+  }
+}
+
+class NestedEnsureCompletion extends NestedCompletion {
+  NestedEnsureCompletion() {
+    inner instanceof NormalCompletion and
+    nestedEnsureCompletion(outer, nestLevel)
+  }
+
+  override NormalCompletion getInnerCompletion() { result = inner }

  override Completion getOuterCompletion() { result = outer }

-  override SuccessorType getAMatchingSuccessorType() {
-    inner = TBreakCompletion() and
-    outer = TSimpleCompletion() and
-    result instanceof BreakSuccessor
+  override Completion getAnInnerCompatibleCompletion() {
+    result.getOuterCompletion() = this.getInnerCompletion()
  }

-  override string toString() { result = outer + " [" + inner + "]" }
-}
-
-private class NestedNormalCompletion extends NormalCompletion, NestedCompletion {
-  NestedNormalCompletion() { outer instanceof NormalCompletion }
+  override SuccessorType getAMatchingSuccessorType() { none() }
 }
--- a/ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll
+++ b/ql/src/codeql_ruby/controlflow/internal/ControlFlowGraphImpl.qll
@@ -38,6 +38,14 @@ private import Completion
 private import SuccessorTypes
 private import Splitting

+private AstNode parent(AstNode n) {
+  result.getAFieldOrChild() = n and
+  not n instanceof CfgScope
+}
+
+/** Gets the CFG scope of node `n`. */
+CfgScope getScope(AstNode n) { result = parent+(n) }
+
 abstract private class ControlFlowTree extends AstNode {
  /**
   * Holds if `first` is the first element executed within this AST node.
@@ -227,7 +235,7 @@ abstract private class LeafTree extends PreOrderTree, PostOrderTree {
 }

 /** Defines the CFG by dispatch on the various AST types. */
-private module Trees {
+module Trees {
  private class AliasTree extends StandardPreOrderTree, Alias {
    final override AstNode getChildNode(int i) {
      i = 0 and result = this.getName()
@@ -262,12 +270,9 @@ private module Trees {
    final override Interpolation getChildNode(int i) { result = this.getChild(i) }
  }

-  private class BeginTree extends StandardPreOrderTree, Begin {
-    final override AstNode getChildNode(int i) {
-      result = this.getChild(i) and
-      not result instanceof Rescue and
-      not result instanceof Else and
-      not result instanceof Ensure
+  private class BeginTree extends RescueEnsureBlockTree, Begin {
+    final override AstNode getChildNode(int i, boolean rescuable) {
+      result = this.getChild(i) and rescuable = true
    }

    override predicate isHidden() { any() }
@@ -357,7 +362,7 @@ private module Trees {
      exists(int i, WhenTree branch | branch = this.getChild(i) |
        last(branch.getLastPattern(), pred, c) and
        first(this.getChild(i + 1), succ) and
-        c instanceof FalseCompletion
+        c.(ConditionalCompletion).getValue() = false
      )
    }
  }
@@ -370,11 +375,11 @@ private module Trees {

  private class CharacterTree extends LeafTree, Character { }

-  private class ClassTree extends StandardPreOrderTree, Class {
-    final override AstNode getChildNode(int i) {
-      result = this.getName() and i = 0
+  private class ClassTree extends RescueEnsureBlockTree, Class {
+    final override AstNode getChildNode(int i, boolean rescuable) {
+      result = this.getName() and i = 0 and rescuable = false
      or
-      result = this.getChild(i - 1)
+      result = this.getChild(i - 1) and rescuable = true
    }
  }

@@ -384,6 +389,33 @@ private module Trees {

  private class ConstantTree extends LeafTree, Constant { }

+  /** A parameter that may have a default value. */
+  abstract class DefaultValueParameterTree extends PreOrderTree {
+    abstract AstNode getDefaultValue();
+
+    predicate hasDefaultValue() { exists(this.getDefaultValue()) }
+
+    final override predicate propagatesAbnormal(AstNode child) { child = this.getDefaultValue() }
+
+    final override predicate last(AstNode last, Completion c) {
+      last = this and
+      exists(this.getDefaultValue()) and
+      c.(MatchingCompletion).getValue() = true
+      or
+      last(this.getDefaultValue(), last, c)
+      or
+      last = this and
+      not exists(this.getDefaultValue()) and
+      c instanceof SimpleCompletion
+    }
+
+    final override predicate succ(AstNode pred, AstNode succ, Completion c) {
+      pred = this and
+      first(this.getDefaultValue(), succ) and
+      c.(MatchingCompletion).getValue() = false
+    }
+  }
+
  private class DestructuredLeftAssignmentTree extends StandardPostOrderTree,
    DestructuredLeftAssignment {
    final override AstNode getChildNode(int i) { result = this.getChild(i) }
@@ -399,11 +431,11 @@ private module Trees {
    override predicate isHidden() { any() }
  }

-  private class DoBlockTree extends StandardPreOrderTree, DoBlock {
-    final override AstNode getChildNode(int i) {
-      result = this.getParameters() and i = 0
+  private class DoBlockTree extends RescueEnsureBlockTree, DoBlock {
+    final override AstNode getChildNode(int i, boolean rescuable) {
+      result = this.getParameters() and i = 0 and rescuable = false
      or
-      result = this.getChild(i - 1)
+      result = this.getChild(i - 1) and rescuable = true
    }

    override predicate isHidden() { any() }
@@ -431,8 +463,6 @@ private module Trees {

  private class EnsureTree extends StandardPreOrderTree, Ensure {
    final override AstNode getChildNode(int i) { result = this.getChild(i) }
-
-    override predicate isHidden() { any() }
  }

  private class EscapeSequenceTree extends LeafTree, EscapeSequence { }
@@ -443,8 +473,30 @@ private module Trees {
    override predicate isHidden() { any() }
  }

-  private class ExceptionsTree extends StandardPostOrderTree, Exceptions {
-    final override AstNode getChildNode(int i) { result = this.getChild(i) }
+  private class ExceptionsTree extends PreOrderTree, Exceptions {
+    final override predicate propagatesAbnormal(AstNode child) { none() }
+
+    final override predicate last(AstNode last, Completion c) {
+      last(this.getChild(_), last, c) and
+      c.(MatchingCompletion).getValue() = true
+      or
+      exists(int lst |
+        last(this.getChild(lst), last, c) and
+        not exists(this.getChild(lst + 1))
+      )
+    }
+
+    final override predicate succ(AstNode pred, AstNode succ, Completion c) {
+      pred = this and
+      first(this.getChild(0), succ) and
+      c instanceof SimpleCompletion
+      or
+      exists(int i |
+        last(this.getChild(i), pred, c) and
+        c.(MatchingCompletion).getValue() = false and
+        first(this.getChild(i + 1), succ)
+      )
+    }

    override predicate isHidden() { any() }
  }
@@ -493,18 +545,14 @@ private module Trees {

    final override predicate last(AstNode last, Completion c) {
      last = this and
-      c.(EmptinessCompletion).isEmpty()
+      c.(EmptinessCompletion).getValue() = true
      or
      last(this.getBody(), last, c) and
      not c.continuesLoop() and
      not c instanceof BreakCompletion and
      not c instanceof RedoCompletion
      or
-      c =
-        any(NestedCompletion nc |
-          last(this.getBody(), last, nc.getInnerCompletion().(BreakCompletion)) and
-          nc.getOuterCompletion() instanceof SimpleCompletion
-        )
+      last(this.getBody(), last, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion())
    }

    /**
@@ -521,8 +569,7 @@ private module Trees {
      or
      pred = this and
      first(this.getPattern(0), succ) and
-      c instanceof EmptinessCompletion and
-      not c.(EmptinessCompletion).isEmpty()
+      c.(EmptinessCompletion).getValue() = false
      or
      exists(int i, ControlFlowTree next |
        last(this.getPattern(i), pred, c) and
@@ -637,8 +684,8 @@ private module Trees {
    final override AstNode getChildNode(int i) { result = this.getChild() and i = 0 }
  }

-  private class KeywordParameterTree extends StandardPostOrderTree, KeywordParameter {
-    final override AstNode getChildNode(int i) { result = this.getValue() and i = 0 }
+  private class KeywordParameterTree extends DefaultValueParameterTree, KeywordParameter {
+    final override AstNode getDefaultValue() { result = this.getValue() }
  }

  private class LambdaTree extends StandardPreOrderTree, Lambda {
@@ -719,11 +766,11 @@ private module Trees {
    }
  }

-  private class MethodTree extends StandardPreOrderTree, Method {
-    final override AstNode getChildNode(int i) {
-      result = this.getParameters() and i = 0
+  private class MethodTree extends RescueEnsureBlockTree, Method {
+    final override AstNode getChildNode(int i, boolean rescuable) {
+      result = this.getParameters() and i = 0 and rescuable = false
      or
-      result = this.getChild(i - 1)
+      result = this.getChild(i - 1) and rescuable = true
    }

    override predicate isHidden() { any() }
@@ -744,11 +791,11 @@ private module Trees {
    override predicate isHidden() { any() }
  }

-  private class ModuleTree extends StandardPreOrderTree, Module {
-    final override AstNode getChildNode(int i) {
-      result = this.getName() and i = 0
+  private class ModuleTree extends RescueEnsureBlockTree, Module {
+    final override AstNode getChildNode(int i, boolean rescuable) {
+      result = this.getName() and i = 0 and rescuable = false
      or
-      result = this.getChild(i - 1)
+      result = this.getChild(i - 1) and rescuable = true
    }
  }

@@ -766,8 +813,8 @@ private module Trees {
    }
  }

-  private class OptionalParameterTree extends StandardPostOrderTree, OptionalParameter {
-    final override AstNode getChildNode(int i) { result = this.getValue() and i = 0 }
+  private class OptionalParameterTree extends DefaultValueParameterTree, OptionalParameter {
+    final override AstNode getDefaultValue() { result = this.getValue() }
  }

  private class PairTree extends StandardPostOrderTree, Pair {
@@ -782,8 +829,10 @@ private module Trees {
    final override AstNode getChildNode(int i) { result = this.getChild(i) }
  }

-  private class PatternTree extends StandardPostOrderTree, Pattern {
+  private class PatternTree extends StandardPreOrderTree, Pattern {
    final override AstNode getChildNode(int i) { result = this.getChild() and i = 0 }
+
+    final override predicate isHidden() { any() }
  }

  private class ProgramTree extends StandardPreOrderTree, Program {
@@ -809,13 +858,282 @@ private module Trees {
    final override Interpolation getChildNode(int i) { result = this.getChild(i) }
  }

-  private class RescueTree extends StandardPreOrderTree, Rescue {
-    final override AstNode getChildNode(int i) {
-      result = this.getExceptions() and i = 0
+  private class RescueTree extends PreOrderTree, Rescue {
+    final override predicate propagatesAbnormal(AstNode child) { child = this.getExceptions() }
+
+    predicate lastMatch(AstNode last, Completion c) {
+      last(this.getBody(), last, c)
      or
-      result = this.getVariable() and i = 1
+      not exists(this.getBody()) and
+      (
+        last(this.getVariable(), last, c)
+        or
+        not exists(this.getVariable()) and
+        (
+          last(this.getExceptions(), last, c) and
+          c.(MatchingCompletion).getValue() = true
+          or
+          not exists(this.getExceptions()) and
+          last = this and
+          c.isValidFor(this)
+        )
+      )
+    }
+
+    predicate lastNoMatch(AstNode last, Completion c) {
+      last(this.getExceptions(), last, c) and
+      c.(MatchingCompletion).getValue() = false
+    }
+
+    final override predicate last(AstNode last, Completion c) {
+      this.lastNoMatch(last, c)
      or
-      result = this.getBody() and i = 2
+      this.lastMatch(last, c)
+    }
+
+    final override predicate succ(AstNode pred, AstNode succ, Completion c) {
+      exists(AstNode next |
+        pred = this and
+        first(next, succ) and
+        c instanceof SimpleCompletion
+      |
+        next = this.getExceptions()
+        or
+        not exists(this.getExceptions()) and
+        (
+          next = this.getVariable()
+          or
+          not exists(this.getVariable()) and
+          next = this.getBody()
+        )
+      )
+      or
+      exists(AstNode next |
+        last(this.getExceptions(), pred, c) and
+        first(next, succ) and
+        c.(MatchingCompletion).getValue() = true
+      |
+        next = this.getVariable()
+        or
+        not exists(this.getVariable()) and
+        next = this.getBody()
+      )
+      or
+      last(this.getVariable(), pred, c) and
+      first(this.getBody(), succ) and
+      c instanceof NormalCompletion
+    }
+  }
+
+  /** Gets a child of `n` that is in CFG scope `scope`. */
+  pragma[noinline]
+  private AstNode getAChildInScope(AstNode n, CfgScope scope) {
+    result.getParent() = n and
+    scope = getScope(result)
+  }
+
+  /** A block that may contain `rescue`/`ensure`. */
+  abstract class RescueEnsureBlockTree extends PreOrderTree {
+    /**
+     * Gets the `i`th child of this block. `rescuable` indicates whether exceptional
+     * execution of the child can be caught by `rescue`/`ensure`.
+     */
+    abstract AstNode getChildNode(int i, boolean rescuable);
+
+    /** Gets the `i`th child in the body of this block. */
+    final private AstNode getBodyChild(int i, boolean rescuable) {
+      result = this.getChildNode(_, rescuable) and
+      result =
+        rank[i + 1](AstNode child, int j |
+          child = this.getChildNode(j, _) and
+          not result instanceof Rescue and
+          not result instanceof Ensure and
+          not result instanceof Else and
+          not child instanceof CfgScope
+        |
+          child order by j
+        )
+    }
+
+    /** Gets the `i`th `rescue` block in this block. */
+    final Rescue getRescue(int i) {
+      result = rank[i + 1](Rescue s | s = this.getAFieldOrChild() | s order by s.getParentIndex())
+    }
+
+    /** Gets the `else` block in this block, if any. */
+    final private Else getElse() { result = unique(Else s | s = this.getAFieldOrChild()) }
+
+    /** Gets the `ensure` block in this block, if any. */
+    final Ensure getEnsure() { result = unique(Ensure s | s = this.getAFieldOrChild()) }
+
+    final private predicate hasEnsure() { exists(this.getEnsure()) }
+
+    final override predicate propagatesAbnormal(AstNode child) {
+      child = this.getEnsure()
+      or
+      child = this.getBodyChild(_, false)
+    }
+
+    /**
+     * Gets a descendant that belongs to the `ensure` block of this block, if any.
+     * Nested `ensure` blocks are not included.
+     */
+    AstNode getAnEnsureDescendant() {
+      result = this.getEnsure()
+      or
+      exists(AstNode mid |
+        mid = this.getAnEnsureDescendant() and
+        result = getAChildInScope(mid, getScope(mid)) and
+        not exists(RescueEnsureBlockTree nestedBlock |
+          result = nestedBlock.getEnsure() and
+          nestedBlock != this
+        )
+      )
+    }
+
+    /**
+     * Holds if `innerBlock` has an `ensure` block and is immediately nested inside the
+     * `ensure` block of this block.
+     */
+    private predicate nestedEnsure(RescueEnsureBlockTree innerBlock) {
+      exists(Ensure innerEnsure |
+        innerEnsure = getAChildInScope(this.getAnEnsureDescendant(), getScope(this)) and
+        innerEnsure = innerBlock.getEnsure()
+      )
+    }
+
+    /**
+     * Gets the `ensure`-nesting level of this block. That is, the number of `ensure`
+     * blocks that this block is nested under.
+     */
+    int nestLevel() { result = count(RescueEnsureBlockTree outer | outer.nestedEnsure+(this)) }
+
+    /**
+     * Holds if `last` is a last element in the body of this block. `ensurable`
+     * indicates whether `last` may be a predecessor of an `ensure` block.
+     */
+    pragma[nomagic]
+    private predicate lastBody(AstNode last, Completion c, boolean ensurable) {
+      exists(boolean rescuable |
+        if c instanceof RaiseCompletion then ensurable = rescuable else ensurable = true
+      |
+        last(this.getBodyChild(_, rescuable), last, c) and
+        not c instanceof NormalCompletion
+        or
+        exists(int lst |
+          last(this.getBodyChild(lst, rescuable), last, c) and
+          not exists(this.getBodyChild(lst + 1, _))
+        )
+      )
+    }
+
+    /**
+     * Gets a last element from this block that may finish with completion `c`, such
+     * that control may be transferred to the `ensure` block (if it exists), but only
+     * if `ensurable = true`.
+     */
+    pragma[nomagic]
+    private AstNode getAnEnsurePredecessor(Completion c, boolean ensurable) {
+      this.lastBody(result, c, ensurable) and
+      (
+        // Any non-throw completion will always continue directly to the `ensure` block,
+        // unless there is an `else` block
+        not c instanceof RaiseCompletion and
+        not exists(this.getElse())
+        or
+        // Any completion will continue to the `ensure` block when there are no `rescue`
+        // blocks
+        not exists(this.getRescue(_))
+      )
+      or
+      // Last element from any matching `rescue` block continues to the `ensure` block
+      this.getRescue(_).(RescueTree).lastMatch(result, c) and
+      ensurable = true
+      or
+      // If the last `rescue` block does not match, continue to the `ensure` block
+      exists(int lst, MatchingCompletion mc |
+        this.getRescue(lst).(RescueTree).lastNoMatch(result, mc) and
+        mc.getValue() = false and
+        not exists(this.getRescue(lst + 1)) and
+        c =
+          any(NestedEnsureCompletion nec |
+            nec.getOuterCompletion() instanceof RaiseCompletion and
+            nec.getInnerCompletion() = mc and
+            nec.getNestLevel() = 0
+          ) and
+        ensurable = true
+      )
+      or
+      // Last element of `else` block continues to the `ensure` block
+      last(this.getElse(), result, c) and
+      ensurable = true
+    }
+
+    pragma[nomagic]
+    private predicate lastEnsure0(AstNode last, Completion c) { last(this.getEnsure(), last, c) }
+
+    pragma[nomagic]
+    private predicate lastEnsure(
+      AstNode last, NormalCompletion ensure, Completion outer, int nestLevel
+    ) {
+      this.lastEnsure0(last, ensure) and
+      exists(
+        this.getAnEnsurePredecessor(any(Completion c0 | outer = c0.getOuterCompletion()), true)
+      ) and
+      nestLevel = this.nestLevel()
+    }
+
+    override predicate last(AstNode last, Completion c) {
+      exists(boolean ensurable | last = this.getAnEnsurePredecessor(c, ensurable) |
+        not this.hasEnsure()
+        or
+        ensurable = false
+      )
+      or
+      // If the body completes normally, take the completion from the `ensure` block
+      this.lastEnsure(last, c, any(NormalCompletion nc), _)
+      or
+      // If the `ensure` block completes normally, it inherits any non-normal
+      // completion from the body
+      c =
+        any(NestedEnsureCompletion nec |
+          this
+              .lastEnsure(last, nec.getAnInnerCompatibleCompletion(), nec.getOuterCompletion(),
+                nec.getNestLevel())
+        )
+    }
+
+    final override predicate succ(AstNode pred, AstNode succ, Completion c) {
+      pred = this and
+      first(this.getBodyChild(0, _), succ) and
+      c instanceof SimpleCompletion
+      or
+      // Normal left-to-right evaluation in the body
+      exists(int i |
+        last(this.getBodyChild(i, _), pred, c) and
+        first(this.getBodyChild(i + 1, _), succ) and
+        c instanceof NormalCompletion
+      )
+      or
+      // Exceptional flow from body to first `rescue`
+      this.lastBody(pred, c, true) and
+      first(this.getRescue(0), succ) and
+      c instanceof RaiseCompletion
+      or
+      // Flow from one `rescue` clause to the next when there is no match
+      exists(RescueTree rescue, int i | rescue = this.getRescue(i) |
+        rescue.lastNoMatch(pred, c) and
+        first(this.getRescue(i + 1), succ)
+      )
+      or
+      // Flow from body to `else` block when no exception
+      this.lastBody(pred, c, _) and
+      first(this.getElse(), succ) and
+      c instanceof NormalCompletion
+      or
+      // Flow into `ensure` block
+      pred = getAnEnsurePredecessor(c, true) and
+      first(this.getEnsure(), succ)
    }
  }

@@ -870,23 +1188,31 @@ private module Trees {

  private class SetterTree extends LeafTree, Setter { }

-  private class SingletonClassTree extends StandardPreOrderTree, SingletonClass {
-    final override AstNode getChildNode(int i) {
-      result = this.getValue() and i = 0
-      or
-      result = this.getChild(i - 1)
+  private class SingletonClassTree extends RescueEnsureBlockTree, SingletonClass {
+    final override AstNode getChildNode(int i, boolean rescuable) {
+      rescuable = true and
+      (
+        result = this.getValue() and i = 0
+        or
+        result = this.getChild(i - 1)
+      )
    }

    override predicate isHidden() { any() }
  }

-  private class SingletonMethodTree extends StandardPreOrderTree, SingletonMethod {
-    final override AstNode getChildNode(int i) {
-      result = this.getObject() and i = 0
+  private class SingletonMethodTree extends RescueEnsureBlockTree, SingletonMethod {
+    final override AstNode getChildNode(int i, boolean rescuable) {
+      result = this.getObject() and
+      i = 0 and
+      rescuable = false
      or
-      result = this.getParameters() and i = 1
+      result = this.getParameters() and
+      i = 1 and
+      rescuable = false
      or
-      result = this.getChild(i - 2)
+      result = this.getChild(i - 2) and
+      rescuable = true
    }

    override predicate isHidden() { any() }
@@ -956,7 +1282,7 @@ private module Trees {

    final override predicate last(AstNode last, Completion c) {
      last(this.getLastPattern(), last, c) and
-      c instanceof FalseCompletion
+      c.(ConditionalCompletion).getValue() = false
      or
      last(this.getBody(), last, c)
    }
@@ -966,13 +1292,15 @@ private module Trees {
      first(this.getPattern(0), succ) and
      c instanceof SimpleCompletion
      or
-      exists(int i, Pattern p |
+      exists(int i, Pattern p, boolean b |
        p = this.getPattern(i) and
-        last(p, pred, c)
+        last(p, pred, c) and
+        b = c.(ConditionalCompletion).getValue()
      |
-        c instanceof TrueCompletion and first(this.getBody(), succ)
+        b = true and
+        first(this.getBody(), succ)
        or
-        c instanceof FalseCompletion and
+        b = false and
        first(this.getPattern(i + 1), succ)
      )
    }
@@ -990,11 +1318,7 @@ private module Trees {
      not c instanceof BreakCompletion and
      not c instanceof RedoCompletion
      or
-      c =
-        any(NestedCompletion nc |
-          last(this.getBodyNode(), last, nc.getInnerCompletion().(BreakCompletion)) and
-          nc.getOuterCompletion() instanceof SimpleCompletion
-        )
+      last(this.getBodyNode(), last, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion())
    }

    final override predicate succ(AstNode pred, AstNode succ, Completion c) {
@@ -1010,9 +1334,9 @@ private module Trees {
      first(this.getConditionNode(), succ) and
      c.continuesLoop()
      or
-      last(this.getBodyNode(), pred, any(RedoCompletion rc)) and
+      last(this.getBodyNode(), pred, c) and
      first(this.getBodyNode(), succ) and
-      c instanceof SimpleCompletion
+      c instanceof RedoCompletion
    }
  }
 }
@@ -1048,8 +1372,9 @@ private module Cached {
  cached
  newtype TSuccessorType =
    TSuccessorSuccessor() or
-    TBooleanSuccessor(boolean b) { b = true or b = false } or
-    TEmptinessSuccessor(boolean isEmpty) { isEmpty = true or isEmpty = false } or
+    TBooleanSuccessor(boolean b) { b in [false, true] } or
+    TEmptinessSuccessor(boolean isEmpty) { isEmpty in [false, true] } or
+    TMatchingSuccessor(boolean isMatch) { isMatch in [false, true] } or
    TReturnSuccessor() or
    TBreakSuccessor() or
    TNextSuccessor() or
--- a/ql/src/codeql_ruby/controlflow/internal/NonReturning.qll
+++ b/ql/src/codeql_ruby/controlflow/internal/NonReturning.qll
@@ -12,11 +12,11 @@ abstract class NonReturningCall extends AstNode {
 private class RaiseCall extends NonReturningCall, MethodCall {
  RaiseCall() { this.getMethod().toString() = "raise" }

-  override RaiseCompletion getACompletion() { any() }
+  override RaiseCompletion getACompletion() { not result instanceof NestedCompletion }
 }

 private class ExitCall extends NonReturningCall, MethodCall {
  ExitCall() { this.getMethod().toString() in ["abort", "exit"] }

-  override ExitCompletion getACompletion() { any() }
+  override ExitCompletion getACompletion() { not result instanceof NestedCompletion }
 }
--- a/ql/src/codeql_ruby/controlflow/internal/Splitting.qll
+++ b/ql/src/codeql_ruby/controlflow/internal/Splitting.qll
@@ -15,10 +15,16 @@ private int maxSplits() { result = 5 }
 cached
 private module Cached {
  cached
-  newtype TSplitKind = TConditionalCompletionSplitKind()
+  newtype TSplitKind =
+    TConditionalCompletionSplitKind() or
+    TEnsureSplitKind(int nestLevel) { nestLevel = any(Trees::RescueEnsureBlockTree t).nestLevel() }

  cached
-  newtype TSplit = TConditionalCompletionSplit(BooleanCompletion c)
+  newtype TSplit =
+    TConditionalCompletionSplit(ConditionalCompletion c) or
+    TEnsureSplit(EnsureSplitting::EnsureSplitType type, int nestLevel) {
+      nestLevel = any(Trees::RescueEnsureBlockTree t).nestLevel()
+    }

  cached
  newtype TSplits =
@@ -60,13 +66,6 @@ class Split extends TSplit {
  string toString() { none() }
 }

-private AstNode parent(AstNode n) {
-  result.getAFieldOrChild() = n and
-  not n instanceof CfgScope
-}
-
-private CfgScope getScope(AstNode n) { result = parent+(n) }
-
 /**
 * Holds if split kinds `sk1` and `sk2` may overlap. That is, they may apply
 * to at least one common AST node inside `scope`.
@@ -195,7 +194,7 @@ private module ConditionalCompletionSplitting {
   * restrict the edges out of `x < 2 and x > 0` accordingly.
   */
  class ConditionalCompletionSplit extends Split, TConditionalCompletionSplit {
-    BooleanCompletion completion;
+    ConditionalCompletion completion;

    ConditionalCompletionSplit() { this = TConditionalCompletionSplit(completion) }

@@ -238,19 +237,258 @@ private module ConditionalCompletionSplitting {
    override predicate hasExit(AstNode pred, AstNode succ, Completion c) {
      this.appliesTo(pred) and
      succ(pred, succ, c) and
-      if c instanceof BooleanCompletion then completion = c else any()
+      if c instanceof ConditionalCompletion then completion = c else any()
    }

    override predicate hasExitScope(AstNode last, CfgScope scope, Completion c) {
      this.appliesTo(last) and
      succExit(last, scope, c) and
-      if c instanceof BooleanCompletion then completion = c else any()
+      if c instanceof ConditionalCompletion then completion = c else any()
    }

    override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) { none() }
  }
 }

+module EnsureSplitting {
+  /**
+   * The type of a split `ensure` node.
+   *
+   * The type represents one of the possible ways of entering an `ensure`
+   * block. For example, if a block ends with a `return` statement, then
+   * the `ensure` block must end with a `return` as well (provided that
+   * the `ensure` block executes normally).
+   */
+  class EnsureSplitType extends SuccessorType {
+    EnsureSplitType() { not this instanceof ConditionalSuccessor }
+
+    /** Holds if this split type matches entry into an `ensure` block with completion `c`. */
+    predicate isSplitForEntryCompletion(Completion c) {
+      if c instanceof NormalCompletion
+      then
+        // If the entry into the `ensure` block completes with any normal completion,
+        // it simply means normal execution after the `ensure` block
+        this instanceof NormalSuccessor
+      else this = c.getAMatchingSuccessorType()
+    }
+  }
+
+  /** A node that belongs to an `ensure` block. */
+  private class EnsureNode extends AstNode {
+    private Trees::RescueEnsureBlockTree block;
+
+    EnsureNode() { this = block.getAnEnsureDescendant() }
+
+    /** Gets the immediate block that this node belongs to. */
+    Trees::RescueEnsureBlockTree getBlock() { result = block }
+
+    /** Holds if this node is the entry node in the `ensure` block it belongs to. */
+    predicate isEntryNode() { first(block.getEnsure(), this) }
+  }
+
+  /** A node that does not belong to an `ensure` block. */
+  private class NonEnsureNode extends EnsureNode {
+    NonEnsureNode() { not this = any(Trees::RescueEnsureBlockTree t).getAnEnsureDescendant() }
+  }
+
+  /**
+   * A split for nodes belonging to an `ensure` block, which determines how to
+   * continue execution after leaving the `ensure` block. For example, in
+   *
+   * ```rb
+   * begin
+   *   if x
+   *     raise "Exception"
+   *   end
+   * ensure
+   *   puts "Ensure"
+   * end
+   * ```
+   *
+   * all control flow nodes in the `ensure` block have two splits: one representing
+   * normal execution of the body (when `x` evaluates to `true`), and one representing
+   * exceptional execution of the body (when `x` evaluates to `false`).
+   */
+  class EnsureSplit extends Split, TEnsureSplit {
+    private EnsureSplitType type;
+    private int nestLevel;
+
+    EnsureSplit() { this = TEnsureSplit(type, nestLevel) }
+
+    /**
+     * Gets the type of this `ensure` split, that is, how to continue execution after the
+     * `ensure` block.
+     */
+    EnsureSplitType getType() { result = type }
+
+    /** Gets the nesting level. */
+    int getNestLevel() { result = nestLevel }
+
+    override string toString() {
+      if type instanceof NormalSuccessor
+      then result = ""
+      else
+        if nestLevel > 0
+        then result = "ensure(" + nestLevel + "): " + type.toString()
+        else result = "ensure: " + type.toString()
+    }
+  }
+
+  private int getListOrder(EnsureSplitKind kind) {
+    result = ConditionalCompletionSplitting::getNextListOrder() + kind.getNestLevel()
+  }
+
+  int getNextListOrder() {
+    result = max([getListOrder(_) + 1, ConditionalCompletionSplitting::getNextListOrder()])
+  }
+
+  private class EnsureSplitKind extends SplitKind, TEnsureSplitKind {
+    private int nestLevel;
+
+    EnsureSplitKind() { this = TEnsureSplitKind(nestLevel) }
+
+    /** Gets the nesting level. */
+    int getNestLevel() { result = nestLevel }
+
+    override int getListOrder() { result = getListOrder(this) }
+
+    override string toString() { result = "ensure (" + nestLevel + ")" }
+  }
+
+  pragma[noinline]
+  private predicate hasEntry0(AstNode pred, EnsureNode succ, int nestLevel, Completion c) {
+    succ.isEntryNode() and
+    nestLevel = succ.getBlock().nestLevel() and
+    succ(pred, succ, c)
+  }
+
+  private class EnsureSplitImpl extends SplitImpl, EnsureSplit {
+    override EnsureSplitKind getKind() { result.getNestLevel() = this.getNestLevel() }
+
+    override predicate hasEntry(AstNode pred, AstNode succ, Completion c) {
+      hasEntry0(pred, succ, this.getNestLevel(), c) and
+      this.getType().isSplitForEntryCompletion(c)
+    }
+
+    override predicate hasEntryScope(CfgScope scope, AstNode first) { none() }
+
+    /**
+     * Holds if this split applies to `pred`, where `pred` is a valid predecessor.
+     */
+    private predicate appliesToPredecessor(AstNode pred) {
+      this.appliesTo(pred) and
+      (succ(pred, _, _) or succExit(pred, _, _))
+    }
+
+    pragma[noinline]
+    private predicate exit0(
+      AstNode pred, Trees::RescueEnsureBlockTree block, int nestLevel, Completion c
+    ) {
+      this.appliesToPredecessor(pred) and
+      nestLevel = block.nestLevel() and
+      last(block, pred, c)
+    }
+
+    /**
+     * Holds if `pred` may exit this split with completion `c`. The Boolean
+     * `inherited` indicates whether `c` is an inherited completion from the
+     * body.
+     */
+    private predicate exit(
+      Trees::RescueEnsureBlockTree block, AstNode pred, Completion c, boolean inherited
+    ) {
+      exists(EnsureSplitType type |
+        exit0(pred, block, this.getNestLevel(), c) and
+        type = this.getType()
+      |
+        if last(block.getEnsure(), pred, c)
+        then
+          // `ensure` block can itself exit with completion `c`: either `c` must
+          // match this split, `c` must be an abnormal completion, or this split
+          // does not require another completion to be recovered
+          inherited = false and
+          (
+            type = c.getAMatchingSuccessorType()
+            or
+            not c instanceof NormalCompletion
+            or
+            type instanceof NormalSuccessor
+          )
+        else (
+          // `ensure` block can exit with inherited completion `c`, which must
+          // match this split
+          inherited = true and
+          type = c.getAMatchingSuccessorType() and
+          not type instanceof NormalSuccessor
+        )
+      )
+      or
+      // If this split is normal, and an outer split can exit based on an inherited
+      // completion, we need to exit this split as well. For example, in
+      //
+      // ```rb
+      // def m(b1, b2)
+      //   if b1
+      //     return
+      //   end
+      // ensure
+      //   begin
+      //     if b2
+      //       raise "Exception"
+      //     end
+      //   ensure
+      //     puts "inner ensure"
+      //   end
+      // end
+      // ```
+      //
+      // if the outer split for `puts "inner ensure"` is `return` and the inner split
+      // is "normal" (corresponding to `b1 = true` and `b2 = false`), then the inner
+      // split must be able to exit with a `return` completion.
+      this.appliesToPredecessor(pred) and
+      exists(EnsureSplitImpl outer |
+        outer.getNestLevel() = this.getNestLevel() - 1 and
+        outer.exit(_, pred, c, inherited) and
+        this.getType() instanceof NormalSuccessor and
+        inherited = true
+      )
+    }
+
+    override predicate hasExit(AstNode pred, AstNode succ, Completion c) {
+      succ(pred, succ, c) and
+      (
+        exit(_, pred, c, _)
+        or
+        exit(_, pred, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion(), _)
+      )
+    }
+
+    override predicate hasExitScope(AstNode last, CfgScope scope, Completion c) {
+      succExit(last, scope, c) and
+      (
+        exit(_, last, c, _)
+        or
+        exit(_, last, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion(), _)
+      )
+    }
+
+    override predicate hasSuccessor(AstNode pred, AstNode succ, Completion c) {
+      this.appliesToPredecessor(pred) and
+      succ(pred, succ, c) and
+      succ =
+        any(EnsureNode en |
+          if en.isEntryNode()
+          then
+            // entering a nested `ensure` block
+            en.getBlock().nestLevel() > this.getNestLevel()
+          else
+            // staying in the same (possibly nested) `ensure` block as `pred`
+            en.getBlock().nestLevel() >= this.getNestLevel()
+        )
+    }
+  }
+}
+
 /**
 * A set of control flow node splits. The set is represented by a list of splits,
 * ordered by ascending rank.