Rust: Loops propagate CFG return completions but captures continue and break

This commit is contained in:
Simon Friis Vindum
2024-09-13 11:50:57 +02:00
parent b979df61ea
commit 1a85dfd9ce
2 changed files with 15 additions and 1 deletions

View File

@@ -119,3 +119,9 @@ predicate completionIsSimple(Completion c) { c instanceof SimpleCompletion }
/** Holds if `c` is a valid completion for `n`. */
predicate completionIsValidFor(Completion c, AstNode n) { c.isValidFor(n) }
/** Holds if `c` is a completion that interacts with a loop such as `loop`, `for`, `while`. */
predicate isLoopCompletion(Completion c) {
c instanceof BreakCompletion or
c instanceof ContinueCompletion
}

View File

@@ -174,7 +174,7 @@ class LetStmtTree extends StandardPostOrderTree instanceof LetStmt {
}
class LoopExprTree extends PostOrderTree instanceof LoopExpr {
override predicate propagatesAbnormal(AstNode child) { child = super.getBody() }
override predicate propagatesAbnormal(AstNode child) { none() }
override predicate first(AstNode node) { first(super.getBody(), node) }
@@ -189,6 +189,14 @@ class LoopExprTree extends PostOrderTree instanceof LoopExpr {
c instanceof BreakCompletion and
succ = this
}
override predicate last(AstNode last, Completion c) {
super.last(last, c)
or
last(super.getBody(), last, c) and
not completionIsNormal(c) and
not isLoopCompletion(c)
}
}
class ReturnExprTree extends PostOrderTree instanceof ReturnExpr {