Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rust: Add {BreakExpr,ContinueExpr}.getTarget() #17644

Merged
merged 3 commits into from
Oct 3, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions rust/ql/.generated.list

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

2 changes: 0 additions & 2 deletions rust/ql/.gitattributes

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

4 changes: 3 additions & 1 deletion rust/ql/lib/codeql/rust/controlflow/ControlFlowGraph.qll
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,9 @@ final class BooleanSuccessor = BooleanSuccessorImpl;

final class MatchSuccessor = MatchSuccessorImpl;

final class LoopJumpSuccessor = LoopJumpSuccessorImpl;
final class BreakSuccessor = BreakSuccessorImpl;

final class ContinueSuccessor = ContinueSuccessorImpl;

final class ReturnSuccessor = ReturnSuccessorImpl;

Expand Down
52 changes: 14 additions & 38 deletions rust/ql/lib/codeql/rust/controlflow/internal/Completion.qll
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,8 @@ newtype TCompletion =
TSimpleCompletion() or
TBooleanCompletion(Boolean b) or
TMatchCompletion(Boolean isMatch) or
TLoopCompletion(TLoopJumpType kind, TLabelType label) {
label = TNoLabel()
or
kind = TBreakJump() and label = TLabel(any(BreakExpr b).getLifetime().getText())
or
kind = TContinueJump() and label = TLabel(any(ContinueExpr b).getLifetime().getText())
} or
TBreakCompletion() or
TContinueCompletion() or
TReturnCompletion()

/** A completion of a statement or an expression. */
Expand Down Expand Up @@ -148,42 +143,23 @@ class MatchCompletion extends TMatchCompletion, ConditionalCompletion {
}

/**
* A completion that represents a break or a continue.
* A completion that represents a `break`.
*/
class LoopJumpCompletion extends TLoopCompletion, Completion {
override LoopJumpSuccessor getAMatchingSuccessorType() {
result = TLoopSuccessor(this.getKind(), this.getLabelType())
}

final TLoopJumpType getKind() { this = TLoopCompletion(result, _) }

final TLabelType getLabelType() { this = TLoopCompletion(_, result) }
class BreakCompletion extends TBreakCompletion, Completion {
override BreakSuccessor getAMatchingSuccessorType() { any() }

final predicate hasLabel() { this.getLabelType() = TLabel(_) }
override predicate isValidForSpecific(AstNode e) { e instanceof BreakExpr }

final string getLabelName() { TLabel(result) = this.getLabelType() }

final predicate isContinue() { this.getKind() = TContinueJump() }
override string toString() { result = this.getAMatchingSuccessorType().toString() }
}

final predicate isBreak() { this.getKind() = TBreakJump() }
/**
* A completion that represents a `continue`.
*/
class ContinueCompletion extends TContinueCompletion, Completion {
override ContinueSuccessor getAMatchingSuccessorType() { any() }

override predicate isValidForSpecific(AstNode e) {
this.isBreak() and
e instanceof BreakExpr and
(
not e.(BreakExpr).hasLifetime() and not this.hasLabel()
or
e.(BreakExpr).getLifetime().getText() = this.getLabelName()
)
or
this.isContinue() and
e instanceof ContinueExpr and
(
not e.(ContinueExpr).hasLifetime() and not this.hasLabel()
or
e.(ContinueExpr).getLifetime().getText() = this.getLabelName()
)
}
override predicate isValidForSpecific(AstNode e) { e instanceof ContinueExpr }

override string toString() { result = this.getAMatchingSuccessorType().toString() }
}
Expand Down
100 changes: 32 additions & 68 deletions rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -145,44 +145,26 @@ class BlockExprTree extends StandardPostOrderTree, BlockExpr {
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)
}
override predicate propagatesAbnormal(AstNode child) { child = this.getChildNode(_) }
}

class BreakExprTree extends PostOrderTree instanceof BreakExpr {
override predicate propagatesAbnormal(AstNode child) { child = super.getExpr() }
class BreakExprTree extends PostOrderTree, BreakExpr {
override predicate propagatesAbnormal(AstNode child) { child = this.getExpr() }

override predicate first(AstNode node) {
first(super.getExpr(), node)
first(this.getExpr(), node)
or
not super.hasExpr() and node = this
not this.hasExpr() and node = this
}

override predicate last(AstNode last, Completion c) { none() }
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is having no last node valid?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, and we want it because the edge out of {Break,Continue}Expr is defined explicitly (as the jump target) in the succ relation.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, having a last node would cause an (incorrect) edge to be created from the break to the next statement sequentially in the program.


override predicate succ(AstNode pred, AstNode succ, Completion c) {
last(super.getExpr(), pred, c) and succ = this
or
pred = this and
c.isValidFor(pred) and
succ = this.getTarget()
}
}

Expand All @@ -200,7 +182,15 @@ class CastExprTree extends StandardPostOrderTree instanceof CastExpr {

class ClosureExprTree extends LeafTree instanceof ClosureExpr { }

class ContinueExprTree extends LeafTree instanceof ContinueExpr { }
class ContinueExprTree extends LeafTree, ContinueExpr {
override predicate last(AstNode last, Completion c) { none() }

override predicate succ(AstNode pred, AstNode succ, Completion c) {
pred = this and
c.isValidFor(pred) and
first(this.getTarget().(LoopingExprTree).getLoopContinue(), succ)
}
}

class ExprStmtTree extends StandardPreOrderTree instanceof ExprStmt {
override AstNode getChildNode(int i) { i = 0 and result = super.getExpr() }
Expand Down Expand Up @@ -310,57 +300,27 @@ class LetStmtTree extends PreOrderTree instanceof LetStmt {
class LiteralExprTree extends LeafTree instanceof LiteralExpr { }

abstract class LoopingExprTree extends PostOrderTree {
override predicate propagatesAbnormal(AstNode child) { none() }
override predicate propagatesAbnormal(AstNode child) { child = this.getLoopBody() }

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();

/** Holds if this loop captures the `c` completion. */
private predicate capturesLoopJumpCompletion(LoopJumpCompletion c) {
not c.hasLabel()
or
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(this.getLoopBody(), pred, c) and
(
completionIsNormal(c)
or
c.(LoopJumpCompletion).isContinue() and this.capturesLoopJumpCompletion(c)
) and
completionIsNormal(c) and
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(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) }
Expand All @@ -369,11 +329,13 @@ class LoopExprTree extends LoopingExprTree instanceof LoopExpr {
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 propagatesAbnormal(AstNode child) {
super.propagatesAbnormal(child)
or
child = super.getCondition()
}

override predicate first(AstNode node) { first(super.getCondition(), node) }

Expand All @@ -399,11 +361,13 @@ class WhileExprTree extends LoopingExprTree instanceof WhileExpr {
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 propagatesAbnormal(AstNode child) {
super.propagatesAbnormal(child)
or
child = super.getIterable()
}

override predicate first(AstNode node) { first(super.getIterable(), node) }

Expand Down
32 changes: 11 additions & 21 deletions rust/ql/lib/codeql/rust/controlflow/internal/SuccessorType.qll
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,8 @@ newtype TSuccessorType =
TSuccessorSuccessor() or
TBooleanSuccessor(Boolean b) or
TMatchSuccessor(Boolean b) or
TLoopSuccessor(TLoopJumpType kind, TLabelType label) { exists(TLoopCompletion(kind, label)) } or
TBreakSuccessor() or
TContinueSuccessor() or
TReturnSuccessor()

/** The type of a control flow successor. */
Expand Down Expand Up @@ -59,28 +60,17 @@ class MatchSuccessorImpl extends ConditionalSuccessorImpl, TMatchSuccessor {
}

/**
* A control flow successor of a loop control flow expression, `continue` or `break`.
* A control flow successor of a `break` expression.
*/
class LoopJumpSuccessorImpl extends SuccessorTypeImpl, TLoopSuccessor {
private TLoopJumpType getKind() { this = TLoopSuccessor(result, _) }

private TLabelType getLabelType() { this = TLoopSuccessor(_, result) }

predicate hasLabel() { this.getLabelType() = TLabel(_) }

string getLabelName() { this = TLoopSuccessor(_, TLabel(result)) }

predicate isContinue() { this.getKind() = TContinueJump() }

predicate isBreak() { this.getKind() = TBreakJump() }
class BreakSuccessorImpl extends SuccessorTypeImpl, TBreakSuccessor {
override string toString() { result = "break" }
}

override string toString() {
exists(string kind, string label |
(if this.isContinue() then kind = "continue" else kind = "break") and
(if this.hasLabel() then label = "(" + this.getLabelName() + ")" else label = "") and
result = kind + label
)
}
/**
* A control flow successor of a `continue` expression.
*/
class ContinueSuccessorImpl extends SuccessorTypeImpl, TContinueSuccessor {
override string toString() { result = "continue" }
}

/**
Expand Down
Loading
Loading