mirror of
https://github.com/github/codeql.git
synced 2025-12-26 05:36:32 +01:00
54aec7bb96
The changes to `ModificationOfParameterWithDefault.ql` and the use of
`ConditionBlock::controls` therein caused the `BasicBlock` argument to
get magicked in, resulting in the following antijoin for the `forall`:
```
[2021-10-04 12:07:46] (108s) Tuple counts for GuardedControlFlow::ConditionBlock::controls_dispred#fbf#antijoin_rhs/5@d84e94 after 1m44s:
201222345 ~7% {5} r1 = JOIN GuardedControlFlow::ConditionBlock::controls_dispred#fbf#shared#2 WITH Flow::BasicBlock::getASuccessor_dispred#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.0 'arg1', Rhs.1 'arg4', Lhs.1 'arg0', Lhs.2 'arg2', Lhs.3 'arg3'
200599933 ~4% {5} r2 = JOIN r1 WITH Flow::BasicBlock::dominates#ff ON FIRST 2 OUTPUT Lhs.2 'arg0', Lhs.0 'arg1', Lhs.3 'arg2', Lhs.4 'arg3', Lhs.1 'arg4'
0 ~0% {4} r3 = JOIN GuardedControlFlow::ConditionBlock::controls_dispred#fbf#shared#1 WITH GuardedControlFlow::ConditionBlock#class#f ON FIRST 1 OUTPUT Lhs.0 'arg3', Lhs.2 'arg1', Lhs.1 'arg0', false
0 ~0% {4} r4 = JOIN GuardedControlFlow::ConditionBlock::controls_dispred#fbf#shared WITH GuardedControlFlow::ConditionBlock#class#f ON FIRST 1 OUTPUT Lhs.0 'arg3', Lhs.2 'arg1', Lhs.1 'arg0', true
0 ~0% {4} r5 = r3 UNION r4
0 ~0% {5} r6 = JOIN r5 WITH Flow::BasicBlock::getASuccessor_dispred#ff ON FIRST 2 OUTPUT Lhs.2 'arg0', Lhs.1 'arg1', Lhs.3 'arg2', Lhs.0 'arg3', Rhs.0
200599933 ~4% {5} r7 = r2 UNION r6
return r7
```
(cancelled)
I observed that quick-eval'ing the `controls` predicate exhibit no such
bad join order (and terminated quickly) which lead me to conclude that
this was a case of bad magic.
Adding the `pragma[nomagic]` resulted in a return to the previous
performance.
70 lines
2.8 KiB
Plaintext
70 lines
2.8 KiB
Plaintext
import python
|
|
|
|
/** A basic block which terminates in a condition, splitting the subsequent control flow */
|
|
class ConditionBlock extends BasicBlock {
|
|
ConditionBlock() {
|
|
exists(ControlFlowNode succ |
|
|
succ = this.getATrueSuccessor() or succ = this.getAFalseSuccessor()
|
|
)
|
|
}
|
|
|
|
/** Basic blocks controlled by this condition, i.e. those BBs for which the condition is testIsTrue */
|
|
pragma[nomagic]
|
|
predicate controls(BasicBlock controlled, boolean testIsTrue) {
|
|
/*
|
|
* For this block to control the block 'controlled' with 'testIsTrue' the following must be true:
|
|
* Execution must have passed through the test i.e. 'this' must strictly dominate 'controlled'.
|
|
* Execution must have passed through the 'testIsTrue' edge leaving 'this'.
|
|
*
|
|
* Although "passed through the true edge" implies that this.getATrueSuccessor() dominates 'controlled',
|
|
* the reverse is not true, as flow may have passed through another edge to get to this.getATrueSuccessor()
|
|
* so we need to assert that this.getATrueSuccessor() dominates 'controlled' *and* that
|
|
* all predecessors of this.getATrueSuccessor() are either this or dominated by this.getATrueSuccessor().
|
|
*
|
|
* For example, in the following python snippet:
|
|
* <code>
|
|
* if x:
|
|
* controlled
|
|
* false_successor
|
|
* uncontrolled
|
|
* </code>
|
|
* false_successor dominates uncontrolled, but not all of its predecessors are this (if x)
|
|
* or dominated by itself. Whereas in the following code:
|
|
* <code>
|
|
* if x:
|
|
* while controlled:
|
|
* also_controlled
|
|
* false_successor
|
|
* uncontrolled
|
|
* </code>
|
|
* the block 'while controlled' is controlled because all of its predecessors are this (if x)
|
|
* or (in the case of 'also_controlled') dominated by itself.
|
|
*
|
|
* The additional constraint on the predecessors of the test successor implies
|
|
* that `this` strictly dominates `controlled` so that isn't necessary to check
|
|
* directly.
|
|
*/
|
|
|
|
exists(BasicBlock succ |
|
|
testIsTrue = true and succ = this.getATrueSuccessor()
|
|
or
|
|
testIsTrue = false and succ = this.getAFalseSuccessor()
|
|
|
|
|
succ.dominates(controlled) and
|
|
forall(BasicBlock pred | pred.getASuccessor() = succ | pred = this or succ.dominates(pred))
|
|
)
|
|
}
|
|
|
|
/** Holds if this condition controls the edge `pred->succ`, i.e. those edges for which the condition is `testIsTrue`. */
|
|
predicate controlsEdge(BasicBlock pred, BasicBlock succ, boolean testIsTrue) {
|
|
this.controls(pred, testIsTrue) and succ = pred.getASuccessor()
|
|
or
|
|
pred = this and
|
|
(
|
|
testIsTrue = true and succ = this.getATrueSuccessor()
|
|
or
|
|
testIsTrue = false and succ = this.getAFalseSuccessor()
|
|
)
|
|
}
|
|
}
|