Rust: More CFG modelling #17633
Rust: More CFG modelling #17633
Conversation
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
hvitved
force-pushed
the
rust/cfg-fixes
branch
from
cf99de1 to
7eea229
Compare
rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
Outdated
Show resolved
Hide resolved
rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
Outdated
Show resolved
Hide resolved
| @@ -284,7 +284,9 @@ abstract class LoopingExprTree extends PostOrderTree { | |||
|
|
|||
| abstract Label getLabel(); | |||
|
|
|||
| /** Whether this loop captures the `c` completion. */ | |||
| abstract predicate entry(AstNode node); | |||
There was a problem hiding this comment.
A comment would be nice here.
There was a problem hiding this comment.
I still think a comment explaining the purpose of entry and how it differs from first would be nice.
| last(super.getPat(), pred, c) and | ||
| c.(MatchCompletion).failed() and | ||
| succ = this |
There was a problem hiding this comment.
This looks a little weird. The pattern in a for-loop can never fail, it is actually the implicit iter.next() call that may return None and exit the loop. Not sure if it matters much though. Perhaps we should have a special IteratorCompletion here?
There was a problem hiding this comment.
I think it would be even better if we could desugar for loops.
| @@ -86,7 +86,7 @@ class BooleanCompletion extends ConditionalCompletion, TBooleanCompletion { | |||
| or | |||
| e = any(WhileExpr c).getCondition() | |||
| or | |||
| any(MatchArm arm).getGuard() = e | |||
| any(MatchGuard guard).getCondition() = e | |||
There was a problem hiding this comment.
I guess we should drop /hideMatchGuard nodes from the AST at some point. They look like useless wrappers.
rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
Outdated
Show resolved
Hide resolved
rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
Outdated
Show resolved
Hide resolved
rust/ql/lib/codeql/rust/controlflow/internal/ControlFlowGraphImpl.qll
Outdated
Show resolved
Hide resolved
hvitved
force-pushed
the
rust/cfg-fixes
branch
from
7eea229 to
91aac76
Compare
hvitved
force-pushed
the
rust/cfg-fixes
branch
from
91aac76 to
8f0b7f0
Compare
| /** 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)) |
There was a problem hiding this comment.
This looks fine for now, we don't really have a way to identify "panic"-like statements. A real panic wouldn't complete normally, it would abort the program. When we extract types, we may refine this to hold if the type of the expression is !.
|
|
||
| /** Holds if this block captures the break completion `c`. */ | ||
| private predicate capturesBreakCompletion(LoopJumpCompletion c) { | ||
| c.isBreak() and |
There was a problem hiding this comment.
Do you also handle shadowing of labels? It's a silly thing to do, and the rust compiler will warn about it, but shadowed labels are allowed. For example:
'a: loop {
'a: loop {
'a: {
break 'a;
}
break 'a;
}
break 'a;
}You might want to add a test case, if you don't already have one;
There was a problem hiding this comment.
There was a problem hiding this comment.
Oh, wait, I we don't have one that shadows; I'll add.
There was a problem hiding this comment.
I have added one now, and the CFG is correct:
flowchart TD
1["enter test_loop_label_shadowing"]
10["b"]
11["ContinueExpr"]
12["ExprStmt"]
13["ContinueExpr"]
14["ExprStmt"]
2["1"]
3["ExprStmt"]
4["ExprStmt"]
5["IfExpr"]
6["b"]
7["ContinueExpr"]
8["ExprStmt"]
9["IfExpr"]
1 --> 3
2 --> 4
3 --> 2
4 --> 6
5 --> 14
6 -- false --> 10
6 -- true --> 8
7 -- continue --> 4
8 --> 7
9 --> 5
10 -- false --> 9
10 -- true --> 12
11 -- continue('loop) --> 4
12 --> 11
13 -- continue('loop) --> 4
14 --> 13
| @@ -284,7 +284,9 @@ abstract class LoopingExprTree extends PostOrderTree { | |||
|
|
|||
| abstract Label getLabel(); | |||
|
|
|||
| /** Whether this loop captures the `c` completion. */ | |||
| abstract predicate entry(AstNode node); | |||
There was a problem hiding this comment.
I still think a comment explaining the purpose of entry and how it differs from first would be nice.
This PR fixes all CFG inconsistencies in our test suite, by adding missing cases to
ControlFlowGraphImpl.qll.Commit-by-commit review is suggested.