From ffd6b9864c3b7108f20d192031202ebed3d37cbc Mon Sep 17 00:00:00 2001
From: Tom Hvitved <hvitved@github.com>
Date: Fri, 11 Oct 2024 14:27:42 +0200
Subject: [PATCH] Address review comments

---
 .../rust/controlflow/internal/Completion.qll  | 19 +++++--------
 .../internal/ControlFlowGraphImpl.qll         | 28 ++++++-------------
 2 files changed, 16 insertions(+), 31 deletions(-)

diff --git a/rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll b/rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll
index fc67c32045b7..256b058f823e 100644
--- a/rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll
+++ b/rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll
@@ -117,10 +117,9 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
   override string toString() { result = "boolean(" + value + ")" }
 }
 
-/** Holds if node `pat` has the constant match value `value`. */
+/** Holds if `pat` is guaranteed to match. */
 pragma[nomagic]
-private predicate isMatchConstant(Pat pat, boolean value) {
-  value = true and
+private predicate isIrrefutablePattern(Pat pat) {
   (
     pat instanceof WildcardPat
     or
@@ -128,18 +127,18 @@ private predicate isMatchConstant(Pat pat, boolean value) {
     or
     pat instanceof RestPat
     or
-    // `let` statements without an `else` branch must be exhaustive
+    // `let` statements without an `else` branch must be irrefutible
     pat = any(LetStmt let | not let.hasLetElse()).getPat()
     or
-    // `match` expressions must be exhaustive, so last arm cannot fail
+    // `match` expressions must be irrefutible, so last arm cannot fail
     pat = any(MatchExpr me).getLastArm().getPat()
     or
-    // parameter patterns must be exhaustive
+    // parameter patterns must be irrefutible
     pat = any(Param p).getPat()
   ) and
   not pat = any(ForExpr for).getPat() // workaround until `for` loops are desugared
   or
-  exists(Pat parent | isMatchConstant(parent, value) |
+  exists(Pat parent | isIrrefutablePattern(parent) |
     pat = parent.(BoxPat).getPat()
     or
     pat = parent.(IdentPat).getPat()
@@ -166,11 +165,7 @@ class MatchCompletion extends TMatchCompletion, ConditionalCompletion {
 
   override predicate isValidForSpecific(AstNode e) {
     e instanceof Pat and
-    (
-      isMatchConstant(e, value)
-      or
-      not isMatchConstant(e, _)
-    )
+    if isIrrefutablePattern(e) then value = true else any()
   }
 
   override MatchSuccessor getAMatchingSuccessorType() { result.getValue() = value }
diff --git a/rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll b/rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
index 6c0c257767a7..cc797dcb3de9 100644
--- a/rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
+++ b/rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
@@ -179,12 +179,14 @@ class CastExprTree extends StandardPostOrderTree instanceof CastExpr {
   override AstNode getChildNode(int i) { i = 0 and result = super.getExpr() }
 }
 
-// Closures have their own CFG scope, so we need to make sure that their
-// CFG is not mixed with the surrounding CFG. This is done by retrofitting
-// `first`, `propagatesAbnormal`, and `succ` below.
-class ClosureExprTree extends StandardPostOrderTree, ClosureExpr {
+class ClosureExprTree extends StandardTree, ClosureExpr {
   override predicate first(AstNode first) { first = this }
 
+  override predicate last(AstNode last, Completion c) {
+    last = this and
+    completionIsValidFor(c, this)
+  }
+
   override predicate propagatesAbnormal(AstNode child) { none() }
 
   override AstNode getChildNode(int i) {
@@ -193,11 +195,6 @@ class ClosureExprTree extends StandardPostOrderTree, ClosureExpr {
     i = this.getParamList().getNumberOfParams() and
     result = this.getBody()
   }
-
-  override predicate succ(AstNode pred, AstNode succ, Completion c) {
-    super.succ(pred, succ, c) and
-    not succ = this
-  }
 }
 
 class ContinueExprTree extends LeafTree, ContinueExpr {
@@ -218,11 +215,9 @@ class FieldExprTree extends StandardPostOrderTree instanceof FieldExpr {
   override AstNode getChildNode(int i) { i = 0 and result = super.getExpr() }
 }
 
-// Functions have their own CFG scope, so we need to make sure that their
-// CFG is not mixed with the surrounding CFG in case of nested functions.
-// This is done by retrofitting `last`, `propagatesAbnormal`, and `succ`
-// below.
-class FunctionTree extends StandardPreOrderTree, Function {
+class FunctionTree extends StandardTree, Function {
+  override predicate first(AstNode first) { first = this }
+
   override predicate last(AstNode last, Completion c) {
     last = this and
     completionIsValidFor(c, this)
@@ -236,11 +231,6 @@ class FunctionTree extends StandardPreOrderTree, Function {
     i = this.getParamList().getNumberOfParams() and
     result = this.getBody()
   }
-
-  override predicate succ(AstNode pred, AstNode succ, Completion c) {
-    super.succ(pred, succ, c) and
-    not pred = this
-  }
 }
 
 class ParamTree extends StandardPostOrderTree, Param {