Java/C++: Move range util backEdge predicate to shared pack.

This commit is contained in:
Anders Schack-Mulligen
2023-11-07 14:03:01 +01:00
parent 8d3ed68b68
commit f2ca52d951
8 changed files with 58 additions and 61 deletions

View File

@@ -142,7 +142,13 @@ signature module Semantic {
Expr getBranchExpr(boolean branch);
}
class BasicBlock;
class BasicBlock {
/** Holds if this block (transitively) dominates `otherblock`. */
predicate bbDominates(BasicBlock otherBlock);
}
/** Gets an immediate successor of basic block `bb`, if any. */
BasicBlock getABasicBlockSuccessor(BasicBlock bb);
class Guard {
string toString();
@@ -176,6 +182,8 @@ signature module Semantic {
class SsaVariable {
Expr getAUse();
BasicBlock getBasicBlock();
}
class SsaPhiNode extends SsaVariable;
@@ -189,6 +197,8 @@ signature module Semantic {
}
class SsaReadPositionPhiInputEdge extends SsaReadPosition {
BasicBlock getOrigBlock();
predicate phiInput(SsaPhiNode phi, SsaVariable inp);
}
@@ -196,8 +206,6 @@ signature module Semantic {
BasicBlock getBlock();
}
predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge);
predicate conversionCannotOverflow(Type fromType, Type toType);
}
@@ -928,7 +936,7 @@ module RangeStage<
origdelta = D::fromFloat(0) and
reason = TSemNoReason()
|
if Sem::backEdge(phi, inp, edge)
if backEdge(phi, inp, edge)
then
fromBackEdge = true and
(

View File

@@ -34,4 +34,37 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
or
result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
}
/**
* Holds if `inp` is an input to `phi` along a back edge.
*/
predicate backEdge(
Lang::SsaPhiNode phi, Lang::SsaVariable inp, Lang::SsaReadPositionPhiInputEdge edge
) {
edge.phiInput(phi, inp) and
(
phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
irreducibleSccEdge(edge.getOrigBlock(), phi.getBasicBlock())
)
}
/**
* Holds if the edge from b1 to b2 is part of a multiple-entry cycle in an irreducible control flow
* graph. Or if the edge is part of a cycle in unreachable code.
*
* An irreducible control flow graph is one where the usual dominance-based back edge detection does
* not work, because there is a cycle with multiple entry points, meaning there are
* mutually-reachable basic blocks where neither dominates the other. For such a graph, we first
* remove all detectable back-edges using the normal condition that the predecessor block is
* dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
* edges.
*/
private predicate irreducibleSccEdge(Lang::BasicBlock b1, Lang::BasicBlock b2) {
trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
}
private predicate trimmedEdge(Lang::BasicBlock pred, Lang::BasicBlock succ) {
Lang::getABasicBlockSuccessor(pred) = succ and
not succ.bbDominates(pred)
}
}