Skip to content

Commit

Permalink
Rust: Include patterns in the CFG
Browse files Browse the repository at this point in the history
  • Loading branch information
hvitved committed Oct 9, 2024
1 parent e33cbec commit 105d3d6
Show file tree
Hide file tree
Showing 9 changed files with 498 additions and 177 deletions.
1 change: 0 additions & 1 deletion rust/ql/.generated.list

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 0 additions & 1 deletion rust/ql/.gitattributes

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

52 changes: 50 additions & 2 deletions rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ abstract class ConditionalCompletion extends NormalCompletion {
abstract ConditionalCompletion getDual();
}

/** Holds if node `le` has the Boolean constant value `value`. */
/** Holds if node `le` has the constant Boolean value `value`. */
private predicate isBooleanConstant(LiteralExpr le, Boolean value) {
le.getTextValue() = value.toString()
}
Expand Down Expand Up @@ -117,13 +117,61 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion {
override string toString() { result = "boolean(" + value + ")" }
}

/** Holds if node `pat` has the constant match value `value`. */
pragma[nomagic]
private predicate isMatchConstant(Pat pat, boolean value) {
value = true and
(
pat instanceof WildcardPat
or
pat = any(IdentPat ip | not ip.hasPat())
or
pat instanceof RestPat
or
// `let` statements without an `else` branch must be exhaustive
pat = any(LetStmt let | not let.hasLetElse()).getPat()
or
// `match` expressions must be exhaustive, so last arm cannot fail
pat = any(MatchExpr me).getLastArm().getPat()
or
// parameter patterns must be exhaustive
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) |
pat = parent.(BoxPat).getPat()
or
pat = parent.(IdentPat).getPat()
or
pat = parent.(ParenPat).getPat()
or
pat = parent.(RecordPat).getRecordPatFieldList().getField(_).getPat()
or
pat = parent.(RefPat).getPat()
or
pat = parent.(TuplePat).getAField()
or
pat = parent.(TupleStructPat).getAField()
or
pat = parent.(OrPat).getLastPat()
)
}

/**
* A completion that represents the result of a pattern match.
*/
class MatchCompletion extends TMatchCompletion, ConditionalCompletion {
MatchCompletion() { this = TMatchCompletion(value) }

override predicate isValidForSpecific(AstNode e) { e instanceof Pat }
override predicate isValidForSpecific(AstNode e) {
e instanceof Pat and
(
isMatchConstant(e, value)
or
not isMatchConstant(e, _)
)
}

override MatchSuccessor getAMatchingSuccessorType() { result.getValue() = value }

Expand Down
Loading

0 comments on commit 105d3d6

Please sign in to comment.