Improve complexity class of getASuccessorSwitchCase

This commit is contained in:
Chris Smowton
2023-11-22 19:37:34 +00:00
parent d99a005b42
commit 1047a89613
2 changed files with 24 additions and 6 deletions

View File

@@ -460,6 +460,15 @@ private module ControlFlowGraphImpl {
)
}
private int lastCaseIndex(StmtParent switch) {
result = max(int i | any(SwitchCase c).isNthCaseOf(switch, i))
}
// Join order engineering -- first determine the switch block and the case indices required, then retrieve them.
bindingset[switch, i]
pragma[inline_late]
private predicate isNthCaseOf(StmtParent switch, SwitchCase c, int i) { c.isNthCaseOf(switch, i) }
/**
* Gets a `SwitchCase` that may be `pred`'s direct successor.
*
@@ -469,14 +478,15 @@ private module ControlFlowGraphImpl {
* that any default case comes after the last pattern case.
*/
private SwitchCase getASuccessorSwitchCase(PatternCase pred) {
result.getParent() = pred.getParent() and
result.getIndex() > pred.getIndex() and
// Note we do include `case null, default` (as well as plain old `default`) here.
not result.(ConstCase).getValue(_) instanceof NullLiteral and
(
result.getIndex() <= getNextPatternCase(pred).getIndex()
or
not exists(getNextPatternCase(pred))
exists(int maxCaseIndex, StmtParent switch |
switch = pred.getParent() and
if exists(getNextPatternCase(pred))
then maxCaseIndex = getNextPatternCase(pred).getCaseIndex()
else maxCaseIndex = lastCaseIndex(switch)
|
isNthCaseOf(switch, result, [pred.getCaseIndex() + 1 .. maxCaseIndex])
)
}

View File

@@ -464,6 +464,14 @@ class SwitchCase extends Stmt, @case {
this = any(SwitchStmt ss).getCase(result) or this = any(SwitchExpr se).getCase(result)
}
/**
* Holds if this is the `n`th case of switch block `parent`.
*/
pragma[nomagic]
predicate isNthCaseOf(StmtParent parent, int n) {
this.getCaseIndex() = n and this.getParent() = parent
}
/**
* Holds if this `case` is a switch labeled rule of the form `... -> ...`.
*/