C++: Speed up 'Buffer.qll'.

This commit is contained in:
Mathias Vorreiter Pedersen
2022-11-03 20:31:55 +00:00
parent f4915073c8
commit b42e81c32d
2 changed files with 35 additions and 13 deletions

View File

@@ -73,20 +73,13 @@ private int isSource(Expr bufferExpr, Element why) {
)
}
private predicate localFlowToExprStep(DataFlow::Node n1, DataFlow::Node n2) {
not exists(n2.asExpr()) and
DataFlow::localFlowStep(n1, n2)
}
/** Holds if `n2 + delta` may be equal to `n1`. */
/**
* Holds if data flow steps from `e1` to `e2` without stepping through any
* other intermediate expressions.
*/
private predicate localFlowStepToExpr(Expr e1, Expr e2) {
getBufferSizeCand0(e1) and
exists(DataFlow::Node n1, DataFlow::Node mid, DataFlow::Node n2 |
n1.asExpr() = e1 and
localFlowToExprStep*(n1, mid) and
DataFlow::localFlowStep(mid, n2) and
n2.asExpr() = e2
)
DataFlow::localExprFlowStep(e1, e2)
}
/**

View File

@@ -1320,7 +1320,36 @@ predicate localInstructionFlow(Instruction e1, Instruction e2) {
* local (intra-procedural) steps.
*/
pragma[inline]
predicate localExprFlow(Expr e1, Expr e2) { localFlow(exprNode(e1), exprNode(e2)) }
predicate localExprFlow(Expr e1, Expr e2) { localExprFlowStep*(e1, e2) }
/**
* Holds if `n1.asExpr()` doesn't have a result and `n1` flows to `n2` in a single
* dataflow step.
*/
private predicate localStepFromNonExpr(Node n1, Node n2) {
not exists(n1.asExpr()) and
localFlowStep(n1, n2)
}
/**
* Holds if `n1.asExpr()` doesn't have a result, `n2.asExpr() = e2` and
* `n2` is the first node reachable from `n2` such that `n2.asExpr()` exists.
*/
pragma[nomagic]
private predicate localStepsToExpr(Node n1, Node n2, Expr e2) {
localStepFromNonExpr*(n1, n2) and
e2 = n2.asExpr()
}
/** Holds if data can flow from `e1` to `e2` in one local (intra-procedural) step. */
cached
predicate localExprFlowStep(Expr e1, Expr e2) {
exists(Node mid, Node n1, Node n2 |
localFlowStep(n1, mid) and
localStepsToExpr(mid, n2, e2) and
e1 = n1.asExpr()
)
}
cached
private newtype TContent =