Python points-to: Make sure reachability can skip over if-statements.

This commit is contained in:
Mark Shannon
2019-05-14 11:50:21 +01:00
parent a5ff527ac2
commit 0afcb11a13
3 changed files with 22 additions and 1 deletions

View File

@@ -1077,6 +1077,22 @@ class BasicBlock extends @py_flow_node {
not result.(ConditionBlock).controls(this, _)
}
/** Holds if flow from this BasicBlock always reaches `succ`
*/
predicate alwaysReaches(BasicBlock succ) {
succ = this
or
strictcount(this.getASuccessor()) = 1
and succ = this.getASuccessor()
or
forex(BasicBlock immsucc |
immsucc = this.getASuccessor()
|
immsucc.alwaysReaches(succ)
)
}
}
private predicate start_bb_likely_reachable(BasicBlock b) {

View File

@@ -220,6 +220,11 @@ cached module PointsToInternal {
)
or
reachableEdge(_, b, context)
or
exists(BasicBlock pred |
reachableBlock(pred, context) and
pred.alwaysReaches(b)
)
}
private predicate reachableEdge(BasicBlock pred, BasicBlock succ, PointsToContext context) {

View File

@@ -1 +1 @@
| 1304 |
| 1284 |