C++: Remove bbNotInLoop and its caller in FlowVar

This change is needed when enabling the QL CFG on certain snapshots such
as notaz/picodrive. It removes the `bbNotInLoop` predicate, which was
always a liability because it's inherently quadratic. The real slowdown
came in `skipLoop`, where all true-upon-entry loops were crossed with
all definitions of variables that should take their definition from the
loop body.
This commit is contained in:
Jonas Jensen
2019-10-01 14:20:28 +02:00
parent eed24f1933
commit 0990ceb09a

View File

@@ -513,9 +513,9 @@ module FlowVar_internal {
bbInLoopCondition(bb)
}
predicate bbNotInLoop(BasicBlock bb) {
not this.bbInLoop(bb) and
bb.getEnclosingFunction() = this.getEnclosingFunction()
/** Holds if `sbb` is inside this loop. */
predicate sbbInLoop(SubBasicBlock sbb) {
this.bbInLoop(sbb.getBasicBlock())
}
/**
@@ -537,22 +537,19 @@ module FlowVar_internal {
}
/**
* Holds if some loop always assigns to `v` before leaving through an edge
* from `bbInside` in its condition to `bbOutside` outside the loop, where
* (`sbbDef`, `v`) is a `BlockVar` defined outside the loop. Also, `v` must
* be used outside the loop.
* Holds if `loop` always assigns to `v` before leaving through an edge
* from `bbInside` in its condition to `bbOutside` outside the loop. Also,
* `v` must be used outside the loop.
*/
predicate skipLoop(
SubBasicBlock sbbInside, SubBasicBlock sbbOutside, SubBasicBlock sbbDef, Variable v
SubBasicBlock sbbInside, SubBasicBlock sbbOutside, Variable v, AlwaysTrueUponEntryLoop loop
) {
exists(AlwaysTrueUponEntryLoop loop, BasicBlock bbInside, BasicBlock bbOutside |
exists(BasicBlock bbInside, BasicBlock bbOutside |
loop.alwaysAssignsBeforeLeavingCondition(bbInside, bbOutside, v) and
bbInside = sbbInside.getBasicBlock() and
bbOutside = sbbOutside.getBasicBlock() and
sbbInside.lastInBB() and
sbbOutside.firstInBB() and
loop.bbNotInLoop(sbbDef.getBasicBlock()) and
exists(TBlockVar(sbbDef, v))
sbbOutside.firstInBB()
)
}
@@ -571,7 +568,9 @@ module FlowVar_internal {
start = TBlockVar(sbbDef, v) and
result = mid.getASuccessor() and
variableLiveInSBB(result, v) and
not skipLoop(mid, result, sbbDef, v) and
forall(AlwaysTrueUponEntryLoop loop | skipLoop(mid, result, v, loop) |
loop.sbbInLoop(sbbDef)
) and
not assignmentLikeOperation(result, v, _, _)
)
}