Rust: More CFG modelling

rust/ql/consistency-queries/CfgConsistency.ql

@@ -11,6 +11,7 @@ import codeql.rust.controlflow.internal.Completion
 query predicate nonPostOrderExpr(Expr e, string cls) {
   cls = e.getPrimaryQlClasses() and
   not e instanceof LetExpr and
+  not e instanceof ParenExpr and
   not e instanceof LogicalAndExpr and // todo
   not e instanceof LogicalOrExpr and
   exists(AstNode last, Completion c |
@@ -25,3 +26,14 @@ query predicate scopeNoFirst(CfgScope scope) {
   not scope = any(Function f | not exists(f.getBody())) and
   not scope = any(ClosureExpr c | not exists(c.getBody()))
 }
+
+/** Holds if  `be` is the `else` branch of a `let` statement that results in a panic. */
+private predicate letElsePanic(BlockExpr be) {
+  be = any(LetStmt let).getLetElse().getBlockExpr() and
+  exists(Completion c | CfgImpl::last(be, _, c) | completionIsNormal(c))
+}
+
+query predicate deadEnd(CfgImpl::Node node) {
+  Consistency::deadEnd(node) and
+  not letElsePanic(node.getAstNode())
+}

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

@@ -84,14 +84,18 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
   private predicate isValidForSpecific0(AstNode e) {
     e = any(IfExpr c).getCondition()
     or
-    any(MatchArm arm).getGuard() = e
+    e = any(WhileExpr c).getCondition()
+    or
+    any(MatchGuard guard).getCondition() = e
     or
     exists(BinaryExpr expr |
       expr.getOperatorName() = ["&&", "||"] and
       e = expr.getLhs()
     )
     or
     exists(Expr parent | this.isValidForSpecific0(parent) |
+      e = parent.(ParenExpr).getExpr()
+      or
       parent =
         any(PrefixExpr expr |
           expr.getOperatorName() = "!" and

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

@@ -61,6 +61,10 @@ import CfgImpl
 /** Holds if `p` is a trivial pattern that is always guaranteed to match. */
 predicate trivialPat(Pat p) { p instanceof WildcardPat or p instanceof IdentPat }
 
+class ArrayExprTree extends StandardPostOrderTree, ArrayExpr {
+  override AstNode getChildNode(int i) { result = this.getExpr(i) }
+}
+
 class AsmExprTree extends LeafTree instanceof AsmExpr { }
 
 class AwaitExprTree extends StandardPostOrderTree instanceof AwaitExpr {
@@ -132,14 +136,40 @@ class LogicalAndBinaryOpExprTree extends PreOrderTree, LogicalAndExpr {
   }
 }
 
-class BlockExprBaseTree extends StandardPostOrderTree instanceof BlockExpr {
+class BlockExprTree extends StandardPostOrderTree, BlockExpr {
   override AstNode getChildNode(int i) {
     result = super.getStmtList().getStatement(i)
     or
     not exists(super.getStmtList().getStatement(i)) and
     (exists(super.getStmtList().getStatement(i - 1)) or i = 0) and
     result = super.getStmtList().getTailExpr()
   }
+
+  override predicate propagatesAbnormal(AstNode child) { none() }
+
+  /** Holds if this block captures the break completion `c`. */
+  private predicate capturesBreakCompletion(LoopJumpCompletion c) {
+    c.isBreak() and
+    c.getLabelName() = this.getLabel().getLifetime().getText()
+  }
+
+  override predicate succ(AstNode pred, AstNode succ, Completion c) {
+    super.succ(pred, succ, c)
+    or
+    // Edge for exiting the block with a break expressions
+    last(this.getChildNode(_), pred, c) and
+    this.capturesBreakCompletion(c) and
+    succ = this
+  }
+
+  override predicate last(AstNode last, Completion c) {
+    super.last(last, c)
+    or
+    // Any abnormal completions that this block does not capture should propagate
+    last(this.getChildNode(_), last, c) and
+    not completionIsNormal(c) and
+    not this.capturesBreakCompletion(c)
+  }
 }
 
 class BreakExprTree extends PostOrderTree instanceof BreakExpr {
@@ -189,7 +219,7 @@ class IfExprTree extends PostOrderTree instanceof IfExpr {
     child = [super.getCondition(), super.getThen(), super.getElse()]
   }
 
-  ConditionalCompletion conditionCompletion(Completion c) {
+  private ConditionalCompletion conditionCompletion(Completion c) {
     if super.getCondition() instanceof LetExpr
     then result = c.(MatchCompletion)
     else result = c.(BooleanCompletion)
@@ -226,6 +256,8 @@ class IndexExprTree extends StandardPostOrderTree instanceof IndexExpr {
   }
 }
 
+class ItemTree extends LeafTree, Item { }
+
 // `LetExpr` is a pre-order tree such that the pattern itself ends up
 // dominating successors in the graph in the same way that patterns do in
 // `match` expressions.
@@ -277,45 +309,124 @@ class LetStmtTree extends PreOrderTree instanceof LetStmt {
 
 class LiteralExprTree extends LeafTree instanceof LiteralExpr { }
 
-class LoopExprTree extends PostOrderTree instanceof LoopExpr {
+abstract class LoopingExprTree extends PostOrderTree {
   override predicate propagatesAbnormal(AstNode child) { none() }
 
-  override predicate first(AstNode node) { first(super.getLoopBody(), node) }
+  abstract BlockExpr getLoopBody();
+
+  abstract Label getLabel();
+
+  /**
+   * Gets the node to execute when continuing the loop; either after
+   * executing the last node in the body or after an explicit `continue`.
+   */
+  abstract AstNode getLoopContinue();
 
-  /** Whether this `LoopExpr` captures the `c` completion. */
+  /** Holds if this loop captures the `c` completion. */
   private predicate capturesLoopJumpCompletion(LoopJumpCompletion c) {
     not c.hasLabel()
     or
-    c.getLabelName() = super.getLabel().getLifetime().getText()
+    c.getLabelName() = this.getLabel().getLifetime().getText()
   }
 
   override predicate succ(AstNode pred, AstNode succ, Completion c) {
+    // Edge for exiting the loop with a break expressions
+    last(this.getLoopBody(), pred, c) and
+    c.(LoopJumpCompletion).isBreak() and
+    this.capturesLoopJumpCompletion(c) and
+    succ = this
+    or
     // Edge back to the start for final expression and continue expressions
-    last(super.getLoopBody(), pred, c) and
+    last(this.getLoopBody(), pred, c) and
     (
       completionIsNormal(c)
       or
       c.(LoopJumpCompletion).isContinue() and this.capturesLoopJumpCompletion(c)
     ) and
-    this.first(succ)
-    or
-    // Edge for exiting the loop with a break expressions
-    last(super.getLoopBody(), pred, c) and
-    c.(LoopJumpCompletion).isBreak() and
-    this.capturesLoopJumpCompletion(c) and
-    succ = this
+    first(this.getLoopContinue(), succ)
   }
 
   override predicate last(AstNode last, Completion c) {
     super.last(last, c)
     or
     // Any abnormal completions that this loop does not capture should propagate
-    last(super.getLoopBody(), last, c) and
+    last(this.getLoopBody(), last, c) and
     not completionIsNormal(c) and
     not this.capturesLoopJumpCompletion(c)
   }
 }
 
+class LoopExprTree extends LoopingExprTree instanceof LoopExpr {
+  override BlockExpr getLoopBody() { result = LoopExpr.super.getLoopBody() }
+
+  override Label getLabel() { result = LoopExpr.super.getLabel() }
+
+  override AstNode getLoopContinue() { result = this.getLoopBody() }
+
+  override predicate first(AstNode node) { first(this.getLoopBody(), node) }
+}
+
+class WhileExprTree extends LoopingExprTree instanceof WhileExpr {
+  override BlockExpr getLoopBody() { result = WhileExpr.super.getLoopBody() }
+
+  override Label getLabel() { result = WhileExpr.super.getLabel() }
+
+  override AstNode getLoopContinue() { result = super.getCondition() }
+
+  override predicate propagatesAbnormal(AstNode child) { child = super.getCondition() }
+
+  override predicate first(AstNode node) { first(super.getCondition(), node) }
+
+  private ConditionalCompletion conditionCompletion(Completion c) {
+    if super.getCondition() instanceof LetExpr
+    then result = c.(MatchCompletion)
+    else result = c.(BooleanCompletion)
+  }
+
+  override predicate succ(AstNode pred, AstNode succ, Completion c) {
+    super.succ(pred, succ, c)
+    or
+    last(super.getCondition(), pred, c) and
+    this.conditionCompletion(c).succeeded() and
+    first(this.getLoopBody(), succ)
+    or
+    last(super.getCondition(), pred, c) and
+    this.conditionCompletion(c).failed() and
+    succ = this
+  }
+}
+
+class ForExprTree extends LoopingExprTree instanceof ForExpr {
+  override BlockExpr getLoopBody() { result = ForExpr.super.getLoopBody() }
+
+  override Label getLabel() { result = ForExpr.super.getLabel() }
+
+  override AstNode getLoopContinue() { result = super.getPat() }
+
+  override predicate propagatesAbnormal(AstNode child) { child = super.getIterable() }
+
+  override predicate first(AstNode node) { first(super.getIterable(), node) }
+
+  override predicate succ(AstNode pred, AstNode succ, Completion c) {
+    super.succ(pred, succ, c)
+    or
+    last(super.getIterable(), pred, c) and
+    first(super.getPat(), succ) and
+    completionIsNormal(c)
+    or
+    last(super.getPat(), pred, c) and
+    c.(MatchCompletion).succeeded() and
+    first(this.getLoopBody(), succ)
+    or
+    last(super.getPat(), pred, c) and
+    c.(MatchCompletion).failed() and
+    succ = this
+  }
+}
+
+// TODO: replace with expanded macro once the extractor supports it
+class MacroExprTree extends LeafTree, MacroExpr { }
+
 class MatchArmTree extends ControlFlowTree instanceof MatchArm {
   override predicate propagatesAbnormal(AstNode child) { child = super.getExpr() }
 
@@ -376,10 +487,24 @@ class MethodCallExprTree extends StandardPostOrderTree instanceof MethodCallExpr
   }
 }
 
+class NameTree extends LeafTree, Name { }
+
+class NameRefTree extends LeafTree, NameRef { }
+
 class OffsetOfExprTree extends LeafTree instanceof OffsetOfExpr { }
 
-class ParenExprTree extends StandardPostOrderTree, ParenExpr {
-  override AstNode getChildNode(int i) { i = 0 and result = super.getExpr() }
+class ParenExprTree extends ControlFlowTree, ParenExpr {
+  private ControlFlowTree expr;
+
+  ParenExprTree() { expr = super.getExpr() }
+
+  override predicate propagatesAbnormal(AstNode child) { expr.propagatesAbnormal(child) }
+
+  override predicate first(AstNode first) { expr.first(first) }
+
+  override predicate last(AstNode last, Completion c) { expr.last(last, c) }
+
+  override predicate succ(AstNode pred, AstNode succ, Completion c) { none() }
 }
 
 // This covers all patterns as they all extend `Pat`