C#: Delete splitting-aware controls implementation.

This commit is contained in:
Anders Schack-Mulligen
2025-10-29 16:02:55 +01:00
parent ab2c2ef6ae
commit f6dfcf1ca4
2 changed files with 0 additions and 134 deletions

View File

@@ -33,8 +33,6 @@ module Stages {
cached
private predicate forceCachingInSameStageRev() {
any(ControlFlowElement cfe).controlsBlock(_, _, _)
or
exists(GuardedExpr ge)
or
forceCachingInSameStageRev()

View File

@@ -87,148 +87,16 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
result.getAControlFlowNode()
}
pragma[noinline]
private predicate immediatelyControlsBlockSplit0(
ConditionBlock cb, BasicBlock succ, ConditionalSuccessor s
) {
// Only calculate dominance by explicit recursion for split nodes;
// all other nodes can use regular CFG dominance
this instanceof Impl::SplitAstNode and
cb.getLastNode() = this.getAControlFlowNode() and
succ = cb.getASuccessor(s)
}
pragma[noinline]
private predicate immediatelyControlsBlockSplit1(
ConditionBlock cb, BasicBlock succ, ConditionalSuccessor s, BasicBlock pred, SuccessorType t
) {
this.immediatelyControlsBlockSplit0(cb, succ, s) and
pred = succ.getAPredecessorByType(t) and
pred != cb
}
pragma[noinline]
private predicate immediatelyControlsBlockSplit2(
ConditionBlock cb, BasicBlock succ, ConditionalSuccessor s, BasicBlock pred, SuccessorType t
) {
this.immediatelyControlsBlockSplit1(cb, succ, s, pred, t) and
(
succ.dominates(pred)
or
// `pred` might be another split of this element
pred.getLastNode().getAstNode() = this and
t = s
)
}
/**
* Holds if basic block `succ` is immediately controlled by this control flow
* element with conditional value `s`. That is, `succ` can only be reached from
* the callable entry point by going via the `s` edge out of *some* basic block
* `pred` ending with this element, and `pred` is an immediate predecessor
* of `succ`.
*
* Moreover, this control flow element corresponds to multiple control flow nodes,
* which is why
*
* ```ql
* exists(ConditionBlock cb |
* cb.getLastNode() = this.getAControlFlowNode() |
* cb.immediatelyControls(succ, s)
* )
* ```
*
* does not work.
*
* `cb` records all of the possible condition blocks for this control flow element
* that a path from the callable entry point to `succ` may go through.
*/
pragma[nomagic]
private predicate immediatelyControlsBlockSplit(
BasicBlock succ, ConditionalSuccessor s, ConditionBlock cb
) {
this.immediatelyControlsBlockSplit0(cb, succ, s) and
forall(BasicBlock pred, SuccessorType t |
this.immediatelyControlsBlockSplit1(cb, succ, s, pred, t)
|
this.immediatelyControlsBlockSplit2(cb, succ, s, pred, t)
)
}
pragma[noinline]
private predicate controlsJoinBlockPredecessor(
JoinBlock controlled, ConditionalSuccessor s, int i, ConditionBlock cb
) {
this.controlsBlockSplit(controlled.getJoinBlockPredecessor(i), s, cb)
}
private predicate controlsJoinBlockSplit(JoinBlock controlled, ConditionalSuccessor s, int i) {
i = -1 and
this.controlsJoinBlockPredecessor(controlled, s, _, _)
or
this.controlsJoinBlockSplit(controlled, s, i - 1) and
(
this.controlsJoinBlockPredecessor(controlled, s, i, _)
or
controlled.dominates(controlled.getJoinBlockPredecessor(i))
)
}
cached
private predicate controlsBlockSplit(
BasicBlock controlled, ConditionalSuccessor s, ConditionBlock cb
) {
Stages::GuardsStage::forceCachingInSameStage() and
this.immediatelyControlsBlockSplit(controlled, s, cb)
or
// Equivalent with
//
// ```ql
// exists(JoinBlockPredecessor pred | pred = controlled.getAPredecessor() |
// this.controlsBlockSplit(pred, s)
// ) and
// forall(JoinBlockPredecessor pred | pred = controlled.getAPredecessor() |
// this.controlsBlockSplit(pred, s)
// or
// controlled.dominates(pred)
// )
// ```
//
// but uses no universal recursion for better performance.
exists(int last |
last = max(int i | exists(controlled.(JoinBlock).getJoinBlockPredecessor(i)))
|
this.controlsJoinBlockSplit(controlled, s, last)
) and
this.controlsJoinBlockPredecessor(controlled, s, _, cb)
or
not controlled instanceof JoinBlock and
this.controlsBlockSplit(controlled.getAPredecessor(), s, cb)
}
/**
* Holds if basic block `controlled` is controlled by this control flow element
* with conditional value `s`. That is, `controlled` can only be reached from
* the callable entry point by going via the `s` edge out of *some* basic block
* ending with this element.
*
* This predicate is different from
*
* ```ql
* exists(ConditionBlock cb |
* cb.getLastNode() = this.getAControlFlowNode() |
* cb.controls(controlled, s)
* )
* ```
*
* as control flow splitting is taken into account.
*
* `cb` records all of the possible condition blocks for this control flow element
* that a path from the callable entry point to `controlled` may go through.
*/
predicate controlsBlock(BasicBlock controlled, ConditionalSuccessor s, ConditionBlock cb) {
this.controlsBlockSplit(controlled, s, cb)
or
cb.getLastNode() = this.getAControlFlowNode() and
cb.edgeDominates(controlled, s)
}