Add pattern-case support and generally debug switch CFGs

These were reasonably broken beforehand, due to not taking switch rules into account in enough places, and confusing the expression/statement switch rule distinction with the distinction between switch statements and expressions.

(For example, `switch(x) { 1 -> System.out.println("Hello world") ... }` is a statement, but has a rule expression).
This commit is contained in:
Chris Smowton
2023-10-24 15:13:10 +01:00
parent f4b45fa511
commit 6c990c2cf6
7 changed files with 177 additions and 22 deletions

View File

@@ -435,7 +435,7 @@ private module ControlFlowGraphImpl {
}
/**
* Gets a SwitchCase's successor SwitchCase, if any.
* Holds if `succ` is `pred`'s successor `SwitchCase`.
*/
private predicate nextSwitchCase(SwitchCase pred, SwitchCase succ) {
exists(SwitchExpr se, int idx | se.getCase(idx) = pred and se.getCase(idx + 1) = succ)
@@ -723,7 +723,7 @@ private module ControlFlowGraphImpl {
*/
private predicate last(ControlFlowNode n, ControlFlowNode last, Completion completion) {
// Exceptions are propagated from any sub-expression.
// As are any break, continue, or return completions.
// As are any break, yield, continue, or return completions.
exists(Expr e | e.getParent() = n |
last(e, last, completion) and not completion instanceof NormalOrBooleanCompletion
)
@@ -859,7 +859,7 @@ private module ControlFlowGraphImpl {
// any other abnormal completion is propagated
last(switch.getAStmt(), last, completion) and
completion != anonymousBreakCompletion() and
completion != NormalCompletion()
not completion instanceof NormalOrBooleanCompletion
or
// if the last case completes normally, then so does the switch
last(switch.getStmt(strictcount(switch.getAStmt()) - 1), last, NormalCompletion()) and
@@ -879,32 +879,43 @@ private module ControlFlowGraphImpl {
// any other abnormal completion is propagated
last(switch.getAStmt(), last, completion) and
not completion instanceof YieldCompletion and
completion != NormalCompletion()
not completion instanceof NormalOrBooleanCompletion
)
or
// the last node in a case rule is the last node in the right-hand side
// if the rhs is a statement we wrap the completion as a break
exists(Completion caseCompletion |
last(n.(SwitchCase).getRuleStatement(), last, caseCompletion) and
// the last node in a case rule in statement context is the last node in the right-hand side.
// If the rhs is a statement, we wrap the completion as a break.
exists(Completion caseCompletion, SwitchStmt parent, SwitchCase case |
case = n and
case = parent.getACase() and
last(case.getRuleStatementOrExpressionStatement(), last, caseCompletion) and
if caseCompletion instanceof NormalOrBooleanCompletion
then completion = anonymousBreakCompletion()
else completion = caseCompletion
)
or
// ...and if the rhs is an expression we wrap the completion as a yield
exists(Completion caseCompletion |
last(n.(SwitchCase).getRuleExpression(), last, caseCompletion) and
if caseCompletion instanceof NormalOrBooleanCompletion
then completion = YieldCompletion(caseCompletion)
else completion = caseCompletion
// ...and when a switch occurs in expression context, we wrap the RHS in a yield statement.
// Note the wrapping can only occur in the expression case, because a statement would need
// to have explicit `yield` statements.
exists(SwitchExpr parent, SwitchCase case |
case = n and
case = parent.getACase() and
(
exists(Completion caseCompletion |
last(case.getRuleExpression(), last, caseCompletion) and
if caseCompletion instanceof NormalOrBooleanCompletion
then completion = YieldCompletion(caseCompletion)
else completion = caseCompletion
)
or
last(case.getRuleStatement(), last, completion)
)
)
or
// The last node in a case could always be a failing pattern check.
last = n.(PatternCase) and
completion = basicBooleanCompletion(false)
or
// The last node in a non-rule case is its variable declaration.
// The normal last node in a non-rule pattern case is its variable declaration.
// Note that either rule or non-rule pattern cases can end with pattern match failure, whereupon
// they branch to the next candidate pattern. This is accounted for in the `succ` relation.
last = n.(PatternCase).getDecl() and
not n.(PatternCase).isRule() and
completion = NormalCompletion()
or
// the last statement of a synchronized statement is the last statement of its body
@@ -1231,6 +1242,10 @@ private module ControlFlowGraphImpl {
)
or
// Statements within a switch body execute sequentially.
// Note this includes non-rule case statements and the successful pattern match successor
// of a non-rule pattern case statement. Rule case statements do not complete normally
// (they always break or yield), and the case of pattern matching failure branching to the
// next case is specially handled in the `PatternCase` logic below.
exists(int i |
last(switch.getStmt(i), n, completion) and result = first(switch.getStmt(i + 1))
)
@@ -1251,6 +1266,10 @@ private module ControlFlowGraphImpl {
)
or
// Statements within a switch body execute sequentially.
// Note this includes non-rule case statements and the successful pattern match successor
// of a non-rule pattern case statement. Rule case statements do not complete normally
// (they always break or yield), and the case of pattern matching failure branching to the
// next case is specially handled in the `PatternCase` logic below.
exists(int i |
last(switch.getStmt(i), n, completion) and result = first(switch.getStmt(i + 1))
)

View File

@@ -1514,7 +1514,7 @@ class SwitchExpr extends Expr, StmtParent, @switchexpr {
* which may be either a normal `case` or a `default`.
*/
SwitchCase getCase(int i) {
result = rank[i](SwitchCase case, int idx | case.isNthChildOf(this, idx) | case order by idx)
result = rank[i + 1](SwitchCase case, int idx | case.isNthChildOf(this, idx) | case order by idx)
}
/**

View File

@@ -387,7 +387,8 @@ class SwitchStmt extends Stmt, @switchstmt {
* which may be either a normal `case` or a `default`.
*/
SwitchCase getCase(int i) {
result = rank[i](SwitchCase case, int idx | case.isNthChildOf(this, idx) | case order by idx)
result =
rank[i + 1](SwitchCase case, int idx | case.isNthChildOf(this, idx) | case order by idx)
}
/**
@@ -469,7 +470,17 @@ class SwitchCase extends Stmt, @case {
* This predicate is mutually exclusive with `getRuleExpression`.
*/
Stmt getRuleStatement() {
result.getParent() = this and result.getIndex() = -1 and not result instanceof ExprStmt
result = this.getRuleStatementOrExpressionStatement() and not result instanceof ExprStmt
}
/**
* Gets the statement, including an expression statement, on the RHS of the arrow, if any.
*
* This means this could be an explicit `case e1 -> { s1; ... }` or an implicit
* `case e1 -> stmt;` rule.
*/
Stmt getRuleStatementOrExpressionStatement() {
result.getParent() = this and result.getIndex() = -1
}
}