Add predicate for cast test passing edge in switch statement

This commit is contained in:
Owen Mansel-Chan
2021-02-02 11:07:44 +00:00
parent dd079d4e51
commit c4eaf791e6
2 changed files with 32 additions and 2 deletions

View File

@@ -274,6 +274,17 @@ module ControlFlow {
* cannot return normally, but never fails to hold of a function that can return normally.
*/
predicate mayReturnNormally(FuncDecl f) { CFG::mayReturnNormally(f.getBody()) }
/**
* Holds if `pred` is the node for the case `testExpr` in an expression
* switch statement which is switching on `switchExpr`, and `succ` is the
* node to be executed next if the case test succeeds.
*/
predicate isSwitchCaseTestPassingEdge(
ControlFlow::Node pred, ControlFlow::Node succ, Expr switchExpr, Expr testExpr
) {
CFG::isSwitchCaseTestPassingEdge(pred, succ, switchExpr, testExpr)
}
}
class Write = ControlFlow::WriteNode;

View File

@@ -1046,11 +1046,16 @@ module CFG {
pred = getExprEnd(i, false) and
succ = getExprStart(i + 1)
or
pred = getExprEnd(i, true) and
succ = getBodyStart()
isPassingEdge(i, pred, succ, _)
)
}
predicate isPassingEdge(int i, ControlFlow::Node pred, ControlFlow::Node succ, Expr testExpr) {
pred = getExprEnd(i, true) and
succ = getBodyStart() and
testExpr = getExpr(i)
}
override ControlFlowTree getChildTree(int i) { result = getStmt(i) }
}
@@ -1959,6 +1964,20 @@ module CFG {
exists(ControlFlow::Node last, Completion cmpl | lastNode(root, last, cmpl) and cmpl != Panic())
}
/**
* Holds if `pred` is the node for the case `testExpr` in an expression
* switch statement which is switching on `switchExpr`, and `succ` is the
* node to be executed next if the case test succeeds.
*/
cached
predicate isSwitchCaseTestPassingEdge(
ControlFlow::Node pred, ControlFlow::Node succ, Expr switchExpr, Expr testExpr
) {
exists(ExpressionSwitchStmt ess | ess.getExpr() = switchExpr |
ess.getACase().(CaseClauseTree).isPassingEdge(_, pred, succ, testExpr)
)
}
/** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
cached
ControlFlow::Node succ(ControlFlow::Node nd) { any(ControlFlowTree tree).succ(nd, result) }