Skip to content

Commit

Permalink
Address review comments
Browse files Browse the repository at this point in the history
  • Loading branch information
hvitved committed Oct 11, 2024
1 parent 756affa commit ffd6b98
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 31 deletions.
19 changes: 7 additions & 12 deletions rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll
Original file line number Diff line number Diff line change
Expand Up @@ -117,29 +117,28 @@ 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
pat = any(IdentPat ip | not ip.hasPat() and ip = any(Variable v).getPat())
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()
Expand All @@ -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 }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand All @@ -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 {
Expand All @@ -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)
Expand All @@ -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 {
Expand Down

0 comments on commit ffd6b98

Please sign in to comment.