mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
Java/C++: Move SsaReadPosition to shared qlpack.
This commit is contained in:
Anders Schack-Mulligen
@@ -198,75 +198,15 @@ module SemanticExprConfig {
|
||||
result = v.asOperand().getUse().getBlock()
|
||||
}
|
||||
|
||||
private newtype TReadPosition =
|
||||
TReadPositionBlock(IR::IRBlock block) or
|
||||
TReadPositionPhiInputEdge(IR::IRBlock pred, IR::IRBlock succ) {
|
||||
exists(IR::PhiInputOperand input |
|
||||
pred = input.getPredecessorBlock() and
|
||||
succ = input.getUse().getBlock()
|
||||
)
|
||||
}
|
||||
|
||||
class SsaReadPosition extends TReadPosition {
|
||||
string toString() { none() }
|
||||
|
||||
Location getLocation() { none() }
|
||||
|
||||
predicate hasRead(SsaVariable v) { none() }
|
||||
}
|
||||
|
||||
private class SsaReadPositionBlock extends SsaReadPosition, TReadPositionBlock {
|
||||
IR::IRBlock block;
|
||||
|
||||
SsaReadPositionBlock() { this = TReadPositionBlock(block) }
|
||||
|
||||
final override string toString() { result = block.toString() }
|
||||
|
||||
final override Location getLocation() { result = block.getLocation() }
|
||||
|
||||
final override predicate hasRead(SsaVariable v) {
|
||||
exists(IR::Operand operand | operand.getDef() = v.asInstruction() |
|
||||
not operand instanceof IR::PhiInputOperand and
|
||||
operand.getUse().getBlock() = block
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private class SsaReadPositionPhiInputEdge extends SsaReadPosition, TReadPositionPhiInputEdge {
|
||||
IR::IRBlock pred;
|
||||
IR::IRBlock succ;
|
||||
|
||||
SsaReadPositionPhiInputEdge() { this = TReadPositionPhiInputEdge(pred, succ) }
|
||||
|
||||
final override string toString() { result = pred.toString() + "->" + succ.toString() }
|
||||
|
||||
final override Location getLocation() { result = succ.getLocation() }
|
||||
|
||||
final override predicate hasRead(SsaVariable v) {
|
||||
exists(IR::PhiInputOperand operand | operand.getDef() = v.asInstruction() |
|
||||
operand.getPredecessorBlock() = pred and
|
||||
operand.getUse().getBlock() = succ
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
predicate hasReadOfSsaVariable(SsaReadPosition pos, SsaVariable v) { pos.hasRead(v) }
|
||||
|
||||
predicate readBlock(SsaReadPosition pos, BasicBlock block) { pos = TReadPositionBlock(block) }
|
||||
|
||||
predicate phiInputEdge(SsaReadPosition pos, BasicBlock origBlock, BasicBlock phiBlock) {
|
||||
pos = TReadPositionPhiInputEdge(origBlock, phiBlock)
|
||||
}
|
||||
|
||||
predicate phiInput(SsaReadPosition pos, SsaVariable phi, SsaVariable input) {
|
||||
/** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
|
||||
predicate phiInputFromBlock(SsaVariable phi, SsaVariable inp, BasicBlock bb) {
|
||||
exists(IR::PhiInputOperand operand |
|
||||
pos = TReadPositionPhiInputEdge(operand.getPredecessorBlock(), operand.getUse().getBlock())
|
||||
|
|
||||
bb = operand.getPredecessorBlock() and
|
||||
phi.asInstruction() = operand.getUse() and
|
||||
(
|
||||
input.asInstruction() = operand.getDef()
|
||||
inp.asInstruction() = operand.getDef()
|
||||
or
|
||||
input.asOperand() = operand
|
||||
inp.asOperand() = operand
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -31,35 +31,8 @@ class SemSsaPhiNode extends SemSsaVariable {
|
||||
SemSsaPhiNode() { Specific::phi(this) }
|
||||
|
||||
final SemSsaVariable getAPhiInput() { result = Specific::getAPhiInput(this) }
|
||||
}
|
||||
|
||||
class SemSsaReadPosition instanceof Specific::SsaReadPosition {
|
||||
final string toString() { result = super.toString() }
|
||||
|
||||
final Specific::Location getLocation() { result = super.getLocation() }
|
||||
|
||||
final predicate hasReadOfVar(SemSsaVariable var) { Specific::hasReadOfSsaVariable(this, var) }
|
||||
}
|
||||
|
||||
class SemSsaReadPositionPhiInputEdge extends SemSsaReadPosition {
|
||||
SemBasicBlock origBlock;
|
||||
SemBasicBlock phiBlock;
|
||||
|
||||
SemSsaReadPositionPhiInputEdge() { Specific::phiInputEdge(this, origBlock, phiBlock) }
|
||||
|
||||
predicate phiInput(SemSsaPhiNode phi, SemSsaVariable inp) { Specific::phiInput(this, phi, inp) }
|
||||
|
||||
SemBasicBlock getOrigBlock() { result = origBlock }
|
||||
|
||||
SemBasicBlock getPhiBlock() { result = phiBlock }
|
||||
}
|
||||
|
||||
class SemSsaReadPositionBlock extends SemSsaReadPosition {
|
||||
SemBasicBlock block;
|
||||
|
||||
SemSsaReadPositionBlock() { Specific::readBlock(this, block) }
|
||||
|
||||
SemBasicBlock getBlock() { result = block }
|
||||
|
||||
SemExpr getAnExpr() { result = this.getBlock().getAnExpr() }
|
||||
|
||||
final predicate hasInputFromBlock(SemSsaVariable inp, SemBasicBlock bb) {
|
||||
Specific::phiInputFromBlock(this, inp, bb)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -74,6 +74,8 @@ module Sem implements Semantic {
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
int getBlockId1(BasicBlock bb) { result = bb.getUniqueId() }
|
||||
|
||||
class Guard = SemGuard;
|
||||
|
||||
predicate implies_v2 = semImplies_v2/4;
|
||||
@@ -92,12 +94,6 @@ module Sem implements Semantic {
|
||||
|
||||
class SsaExplicitUpdate = SemSsaExplicitUpdate;
|
||||
|
||||
class SsaReadPosition = SemSsaReadPosition;
|
||||
|
||||
class SsaReadPositionPhiInputEdge = SemSsaReadPositionPhiInputEdge;
|
||||
|
||||
class SsaReadPositionBlock = SemSsaReadPositionBlock;
|
||||
|
||||
predicate conversionCannotOverflow(Type fromType, Type toType) {
|
||||
SemanticType::conversionCannotOverflow(fromType, toType)
|
||||
}
|
||||
|
||||
@@ -133,33 +133,4 @@ module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
|
||||
or
|
||||
not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
|
||||
}
|
||||
|
||||
import Ranking
|
||||
}
|
||||
|
||||
import Ranking
|
||||
|
||||
module Ranking {
|
||||
/**
|
||||
* Holds if `rix` is the number of input edges to `phi`.
|
||||
*/
|
||||
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
|
||||
rix = max(int r | rankedPhiInput(phi, _, _, r))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
|
||||
* in an arbitrary 1-based numbering of the input edges to `phi`.
|
||||
*/
|
||||
predicate rankedPhiInput(
|
||||
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
|
||||
) {
|
||||
edge.phiInput(phi, inp) and
|
||||
edge =
|
||||
rank[r](SemSsaReadPositionPhiInputEdge e |
|
||||
e.phiInput(phi, _)
|
||||
|
|
||||
e order by e.getOrigBlock().getUniqueId()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
@@ -45,7 +45,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
/** An SSA Phi definition, whose sign is the union of the signs of its inputs. */
|
||||
private class PhiSignDef extends FlowSignDef instanceof SemSsaPhiNode {
|
||||
final override Sign getSign() {
|
||||
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
|
||||
exists(SemSsaVariable inp, SsaReadPositionPhiInputEdge edge |
|
||||
edge.phiInput(this, inp) and
|
||||
result = semSsaSign(inp, edge)
|
||||
)
|
||||
@@ -170,11 +170,11 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
override Sign getSignRestriction() {
|
||||
// Propagate via SSA
|
||||
// Propagate the sign from the def of `v`, incorporating any inference from guards.
|
||||
result = semSsaSign(v, any(SemSsaReadPositionBlock bb | bb.getAnExpr() = this))
|
||||
result = semSsaSign(v, any(SsaReadPositionBlock bb | bb.getBlock().getAnExpr() = this))
|
||||
or
|
||||
// No block for this read. Just use the sign of the def.
|
||||
// REVIEW: How can this happen?
|
||||
not exists(SemSsaReadPositionBlock bb | bb.getAnExpr() = this) and
|
||||
not exists(SsaReadPositionBlock bb | bb.getBlock().getAnExpr() = this) and
|
||||
result = semSsaDefSign(v)
|
||||
}
|
||||
}
|
||||
@@ -290,7 +290,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* to only include bounds for which we might determine a sign.
|
||||
*/
|
||||
private predicate lowerBound(
|
||||
SemExpr lowerbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
|
||||
SemExpr lowerbound, SemSsaVariable v, SsaReadPosition pos, boolean isStrict
|
||||
) {
|
||||
exists(boolean testIsTrue, SemRelationalExpr comp |
|
||||
pos.hasReadOfVar(v) and
|
||||
@@ -314,7 +314,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* to only include bounds for which we might determine a sign.
|
||||
*/
|
||||
private predicate upperBound(
|
||||
SemExpr upperbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isStrict
|
||||
SemExpr upperbound, SemSsaVariable v, SsaReadPosition pos, boolean isStrict
|
||||
) {
|
||||
exists(boolean testIsTrue, SemRelationalExpr comp |
|
||||
pos.hasReadOfVar(v) and
|
||||
@@ -340,7 +340,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* - `isEq = true` : `v = eqbound`
|
||||
* - `isEq = false` : `v != eqbound`
|
||||
*/
|
||||
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
|
||||
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SsaReadPosition pos, boolean isEq) {
|
||||
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
|
||||
pos.hasReadOfVar(pragma[only_bind_into](v)) and
|
||||
guardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
|
||||
@@ -355,7 +355,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
|
||||
* order for `v` to be positive.
|
||||
*/
|
||||
private predicate posBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private predicate posBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
|
||||
upperBound(bound, v, pos, _) or
|
||||
eqBound(bound, v, pos, true)
|
||||
}
|
||||
@@ -364,7 +364,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
|
||||
* order for `v` to be negative.
|
||||
*/
|
||||
private predicate negBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private predicate negBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
|
||||
lowerBound(bound, v, pos, _) or
|
||||
eqBound(bound, v, pos, true)
|
||||
}
|
||||
@@ -373,24 +373,24 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
|
||||
* can be zero.
|
||||
*/
|
||||
private predicate zeroBound(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private predicate zeroBound(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
|
||||
lowerBound(bound, v, pos, _) or
|
||||
upperBound(bound, v, pos, _) or
|
||||
eqBound(bound, v, pos, _)
|
||||
}
|
||||
|
||||
/** Holds if `bound` allows `v` to be positive at `pos`. */
|
||||
private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private predicate posBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
|
||||
posBound(bound, v, pos) and TPos() = semExprSign(bound)
|
||||
}
|
||||
|
||||
/** Holds if `bound` allows `v` to be negative at `pos`. */
|
||||
private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private predicate negBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
|
||||
negBound(bound, v, pos) and TNeg() = semExprSign(bound)
|
||||
}
|
||||
|
||||
/** Holds if `bound` allows `v` to be zero at `pos`. */
|
||||
private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private predicate zeroBoundOk(SemExpr bound, SemSsaVariable v, SsaReadPosition pos) {
|
||||
lowerBound(bound, v, pos, _) and TNeg() = semExprSign(bound)
|
||||
or
|
||||
lowerBound(bound, v, pos, false) and TZero() = semExprSign(bound)
|
||||
@@ -408,7 +408,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* Holds if there is a bound that might restrict whether `v` has the sign `s`
|
||||
* at `pos`.
|
||||
*/
|
||||
private predicate hasGuard(SemSsaVariable v, SemSsaReadPosition pos, Sign s) {
|
||||
private predicate hasGuard(SemSsaVariable v, SsaReadPosition pos, Sign s) {
|
||||
s = TPos() and posBound(_, v, pos)
|
||||
or
|
||||
s = TNeg() and negBound(_, v, pos)
|
||||
@@ -421,7 +421,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* might be ruled out by a guard.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private Sign guardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private Sign guardedSsaSign(SemSsaVariable v, SsaReadPosition pos) {
|
||||
result = semSsaDefSign(v) and
|
||||
pos.hasReadOfVar(v) and
|
||||
hasGuard(v, pos, result)
|
||||
@@ -432,7 +432,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* can rule it out.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private Sign unguardedSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private Sign unguardedSsaSign(SemSsaVariable v, SsaReadPosition pos) {
|
||||
result = semSsaDefSign(v) and
|
||||
pos.hasReadOfVar(v) and
|
||||
not hasGuard(v, pos, result)
|
||||
@@ -443,7 +443,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
* ruled out the sign but does not.
|
||||
* This does not check that the definition of `v` also allows the sign.
|
||||
*/
|
||||
private Sign guardedSsaSignOk(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private Sign guardedSsaSignOk(SemSsaVariable v, SsaReadPosition pos) {
|
||||
result = TPos() and
|
||||
forex(SemExpr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))
|
||||
or
|
||||
@@ -455,7 +455,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
}
|
||||
|
||||
/** Gets a possible sign for `v` at `pos`. */
|
||||
private Sign semSsaSign(SemSsaVariable v, SemSsaReadPosition pos) {
|
||||
private Sign semSsaSign(SemSsaVariable v, SsaReadPosition pos) {
|
||||
result = unguardedSsaSign(v, pos)
|
||||
or
|
||||
result = guardedSsaSign(v, pos) and
|
||||
|
||||
@@ -66,7 +66,6 @@
|
||||
import java
|
||||
private import SSA
|
||||
private import RangeUtils
|
||||
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
|
||||
private import semmle.code.java.controlflow.internal.GuardsLogic
|
||||
private import semmle.code.java.security.RandomDataSource
|
||||
private import SignAnalysis
|
||||
@@ -80,7 +79,6 @@ module Sem implements Semantic {
|
||||
private import java as J
|
||||
private import SSA as SSA
|
||||
private import RangeUtils as RU
|
||||
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
|
||||
private import semmle.code.java.controlflow.internal.GuardsLogic as GL
|
||||
|
||||
class Expr = J::Expr;
|
||||
@@ -213,6 +211,12 @@ module Sem implements Semantic {
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getABBSuccessor() }
|
||||
|
||||
private predicate id(BasicBlock x, BasicBlock y) { x = y }
|
||||
|
||||
private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
|
||||
|
||||
int getBlockId1(BasicBlock bb) { idOf(bb, result) }
|
||||
|
||||
final private class FinalGuard = GL::Guard;
|
||||
|
||||
class Guard extends FinalGuard {
|
||||
@@ -243,31 +247,14 @@ module Sem implements Semantic {
|
||||
Expr getAUse() { result = super.getAUse() }
|
||||
}
|
||||
|
||||
class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode { }
|
||||
class SsaPhiNode extends SsaVariable instanceof SSA::SsaPhiNode {
|
||||
predicate hasInputFromBlock(SsaVariable inp, BasicBlock bb) { super.hasInputFromBlock(inp, bb) }
|
||||
}
|
||||
|
||||
class SsaExplicitUpdate extends SsaVariable instanceof SSA::SsaExplicitUpdate {
|
||||
Expr getDefiningExpr() { result = super.getDefiningExpr() }
|
||||
}
|
||||
|
||||
final private class FinalSsaReadPosition = SsaReadPos::SsaReadPosition;
|
||||
|
||||
class SsaReadPosition extends FinalSsaReadPosition {
|
||||
predicate hasReadOfVar(SsaVariable v) { super.hasReadOfVar(v) }
|
||||
}
|
||||
|
||||
class SsaReadPositionPhiInputEdge extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionPhiInputEdge
|
||||
{
|
||||
BasicBlock getOrigBlock() { result = super.getOrigBlock() }
|
||||
|
||||
BasicBlock getPhiBlock() { result = super.getPhiBlock() }
|
||||
|
||||
predicate phiInput(SsaPhiNode phi, SsaVariable inp) { super.phiInput(phi, inp) }
|
||||
}
|
||||
|
||||
class SsaReadPositionBlock extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionBlock {
|
||||
BasicBlock getBlock() { result = super.getBlock() }
|
||||
}
|
||||
|
||||
predicate conversionCannotOverflow = safeCast/2;
|
||||
}
|
||||
|
||||
@@ -384,7 +371,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
|
||||
|
||||
module Utils implements UtilSig<Sem, IntDelta> {
|
||||
private import RangeUtils as RU
|
||||
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
|
||||
|
||||
Sem::Guard semEqFlowCond(
|
||||
Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
|
||||
@@ -403,14 +389,6 @@ module Utils implements UtilSig<Sem, IntDelta> {
|
||||
}
|
||||
|
||||
Sem::Type getTrackedType(Sem::Expr e) { result = e.getType() }
|
||||
|
||||
predicate rankedPhiInput(
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int r
|
||||
) {
|
||||
SsaReadPos::rankedPhiInput(phi, inp, edge, r)
|
||||
}
|
||||
|
||||
predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix) { SsaReadPos::maxPhiInputRank(phi, rix) }
|
||||
}
|
||||
|
||||
module Bounds implements BoundSig<Location, Sem, IntDelta> {
|
||||
|
||||
@@ -5,7 +5,6 @@
|
||||
import java
|
||||
private import SSA
|
||||
private import semmle.code.java.controlflow.internal.GuardsLogic
|
||||
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
|
||||
private import semmle.code.java.Constants
|
||||
private import semmle.code.java.dataflow.RangeAnalysis
|
||||
private import codeql.rangeanalysis.internal.RangeUtils
|
||||
|
||||
@@ -6,6 +6,8 @@ module Private {
|
||||
import semmle.code.java.dataflow.RangeUtils as RU
|
||||
private import semmle.code.java.dataflow.SSA as Ssa
|
||||
private import semmle.code.java.controlflow.Guards as G
|
||||
private import SsaReadPositionCommon
|
||||
private import semmle.code.java.controlflow.internal.GuardsLogic as GL
|
||||
private import Sign
|
||||
import Impl
|
||||
|
||||
@@ -168,7 +170,33 @@ module Private {
|
||||
|
||||
predicate ssaRead = RU::ssaRead/2;
|
||||
|
||||
predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
|
||||
/**
|
||||
* Holds if `guard` directly controls the position `controlled` with the
|
||||
* value `testIsTrue`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate guardDirectlyControlsSsaRead(
|
||||
Guard guard, SsaReadPosition controlled, boolean testIsTrue
|
||||
) {
|
||||
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
|
||||
or
|
||||
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
|
||||
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
|
||||
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
|
||||
*/
|
||||
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
|
||||
or
|
||||
exists(Guard guard0, boolean testIsTrue0 |
|
||||
GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
|
||||
guardControlsSsaRead(guard0, controlled, testIsTrue0)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private module Impl {
|
||||
|
||||
@@ -21,7 +21,7 @@ module ModulusAnalysis<
|
||||
|
||||
bindingset[pos, v]
|
||||
pragma[inline_late]
|
||||
private predicate hasReadOfVarInlineLate(Sem::SsaReadPosition pos, Sem::SsaVariable v) {
|
||||
private predicate hasReadOfVarInlineLate(SsaReadPosition pos, Sem::SsaVariable v) {
|
||||
pos.hasReadOfVar(v)
|
||||
}
|
||||
|
||||
@@ -29,9 +29,7 @@ module ModulusAnalysis<
|
||||
* Holds if `e + delta` equals `v` at `pos`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate valueFlowStepSsa(
|
||||
Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, int delta
|
||||
) {
|
||||
private predicate valueFlowStepSsa(Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, int delta) {
|
||||
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
|
||||
or
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
@@ -105,7 +103,7 @@ module ModulusAnalysis<
|
||||
/**
|
||||
* Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
|
||||
*/
|
||||
private predicate moduloGuardedRead(Sem::SsaVariable v, Sem::SsaReadPosition pos, int val, int mod) {
|
||||
private predicate moduloGuardedRead(Sem::SsaVariable v, SsaReadPosition pos, int val, int mod) {
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = moduloCheck(v, val, mod, testIsTrue) and
|
||||
@@ -148,7 +146,7 @@ module ModulusAnalysis<
|
||||
* Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
|
||||
*/
|
||||
private predicate phiSelfModulus(
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int mod
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, int mod
|
||||
) {
|
||||
exists(Bounds::SemSsaBound phibound, int v, int m |
|
||||
edge.phiInput(phi, inp) and
|
||||
@@ -163,7 +161,7 @@ module ModulusAnalysis<
|
||||
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
|
||||
*/
|
||||
private predicate phiModulusInit(Sem::SsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
|
||||
exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge |
|
||||
exists(Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge |
|
||||
edge.phiInput(phi, inp) and
|
||||
ssaModulus(inp, edge, b, val, mod)
|
||||
)
|
||||
@@ -181,7 +179,7 @@ module ModulusAnalysis<
|
||||
rix = 0 and
|
||||
phiModulusInit(phi, b, val, mod)
|
||||
or
|
||||
exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int v1, int m1 |
|
||||
exists(Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, int v1, int m1 |
|
||||
mod != 1 and
|
||||
val = remainder(v1, mod)
|
||||
|
|
||||
@@ -192,7 +190,7 @@ module ModulusAnalysis<
|
||||
// equals `v2` modulo `mod`. The largest value of `mod` that satisfies
|
||||
// this is the greatest common divisor of `m1`, `m2`, and `v1 - v2`.
|
||||
exists(int v2, int m2 |
|
||||
U::rankedPhiInput(phi, inp, edge, rix) and
|
||||
rankedPhiInput(phi, inp, edge, rix) and
|
||||
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
|
||||
ssaModulus(inp, edge, b, v2, m2) and
|
||||
mod = m1.gcd(m2).gcd(v1 - v2)
|
||||
@@ -202,7 +200,7 @@ module ModulusAnalysis<
|
||||
// preceding potential congruence class `b + v1` mod `m1`. The result will be
|
||||
// the congruence class modulo the greatest common divisor of `m1` and `m2`.
|
||||
exists(int m2 |
|
||||
U::rankedPhiInput(phi, inp, edge, rix) and
|
||||
rankedPhiInput(phi, inp, edge, rix) and
|
||||
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
|
||||
phiSelfModulus(phi, inp, edge, m2) and
|
||||
mod = m1.gcd(m2)
|
||||
@@ -215,7 +213,7 @@ module ModulusAnalysis<
|
||||
*/
|
||||
private predicate phiModulus(Sem::SsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
|
||||
exists(int r |
|
||||
U::maxPhiInputRank(phi, r) and
|
||||
maxPhiInputRank(phi, r) and
|
||||
phiModulusRankStep(phi, b, val, mod, r)
|
||||
)
|
||||
}
|
||||
@@ -224,7 +222,7 @@ module ModulusAnalysis<
|
||||
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
|
||||
*/
|
||||
private predicate ssaModulus(
|
||||
Sem::SsaVariable v, Sem::SsaReadPosition pos, Bounds::SemBound b, int val, int mod
|
||||
Sem::SsaVariable v, SsaReadPosition pos, Bounds::SemBound b, int val, int mod
|
||||
) {
|
||||
phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
|
||||
or
|
||||
@@ -254,7 +252,7 @@ module ModulusAnalysis<
|
||||
val = 0 and
|
||||
b instanceof Bounds::SemZeroBound
|
||||
or
|
||||
exists(Sem::SsaVariable v, Sem::SsaReadPositionBlock bb |
|
||||
exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
|
||||
ssaModulus(v, bb, b, val, mod) and
|
||||
e = v.getAUse() and
|
||||
bb.getBlock() = e.getBasicBlock()
|
||||
|
||||
@@ -150,6 +150,16 @@ signature module Semantic {
|
||||
/** Gets an immediate successor of basic block `bb`, if any. */
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb);
|
||||
|
||||
/**
|
||||
* Gets an ideally unique integer for `bb`. If it is undesirable to make this
|
||||
* unique, then `getBlock2` must provide a tiebreaker, such that the pair
|
||||
* `(getBlockId1(bb),getBlockId2(bb))` becomes unique.
|
||||
*/
|
||||
int getBlockId1(BasicBlock bb);
|
||||
|
||||
/** Gets a tiebreaker id in case `getBlockId1` is not unique. */
|
||||
default string getBlockId2(BasicBlock bb) { result = "" }
|
||||
|
||||
class Guard {
|
||||
string toString();
|
||||
|
||||
@@ -184,28 +194,15 @@ signature module Semantic {
|
||||
BasicBlock getBasicBlock();
|
||||
}
|
||||
|
||||
class SsaPhiNode extends SsaVariable;
|
||||
class SsaPhiNode extends SsaVariable {
|
||||
/** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
|
||||
predicate hasInputFromBlock(SsaVariable inp, BasicBlock bb);
|
||||
}
|
||||
|
||||
class SsaExplicitUpdate extends SsaVariable {
|
||||
Expr getDefiningExpr();
|
||||
}
|
||||
|
||||
class SsaReadPosition {
|
||||
predicate hasReadOfVar(SsaVariable v);
|
||||
}
|
||||
|
||||
class SsaReadPositionPhiInputEdge extends SsaReadPosition {
|
||||
BasicBlock getOrigBlock();
|
||||
|
||||
BasicBlock getPhiBlock();
|
||||
|
||||
predicate phiInput(SsaPhiNode phi, SsaVariable inp);
|
||||
}
|
||||
|
||||
class SsaReadPositionBlock extends SsaReadPosition {
|
||||
BasicBlock getBlock();
|
||||
}
|
||||
|
||||
predicate conversionCannotOverflow(Type fromType, Type toType);
|
||||
}
|
||||
|
||||
@@ -330,19 +327,6 @@ signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
|
||||
* primitive types as the underlying primitive type.
|
||||
*/
|
||||
Sem::Type getTrackedType(Sem::Expr e);
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
|
||||
* in an arbitrary 1-based numbering of the input edges to `phi`.
|
||||
*/
|
||||
predicate rankedPhiInput(
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int r
|
||||
);
|
||||
|
||||
/**
|
||||
* Holds if `rix` is the number of input edges to `phi`.
|
||||
*/
|
||||
predicate maxPhiInputRank(Sem::SsaPhiNode phi, int rix);
|
||||
}
|
||||
|
||||
signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
|
||||
@@ -688,7 +672,7 @@ module RangeStage<
|
||||
* - `upper = false` : `v >= e + delta`
|
||||
*/
|
||||
private predicate boundFlowStepSsa(
|
||||
Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, D::Delta delta, boolean upper,
|
||||
Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, D::Delta delta, boolean upper,
|
||||
SemReason reason
|
||||
) {
|
||||
semSsaUpdateStep(v, e, delta) and
|
||||
@@ -706,7 +690,7 @@ module RangeStage<
|
||||
|
||||
/** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
|
||||
private predicate unequalFlowStepIntegralSsa(
|
||||
Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, D::Delta delta, SemReason reason
|
||||
Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, D::Delta delta, SemReason reason
|
||||
) {
|
||||
getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
@@ -836,7 +820,7 @@ module RangeStage<
|
||||
* - `upper = false` : `v >= b + delta`
|
||||
*/
|
||||
private predicate boundedSsa(
|
||||
Sem::SsaVariable v, SemBound b, D::Delta delta, Sem::SsaReadPosition pos, boolean upper,
|
||||
Sem::SsaVariable v, SemBound b, D::Delta delta, SsaReadPosition pos, boolean upper,
|
||||
boolean fromBackEdge, D::Delta origdelta, SemReason reason
|
||||
) {
|
||||
exists(Sem::Expr mid, D::Delta d1, D::Delta d2, SemReason r1, SemReason r2 |
|
||||
@@ -873,7 +857,7 @@ module RangeStage<
|
||||
* Holds if `v != b + delta` at `pos` and `v` is of integral type.
|
||||
*/
|
||||
private predicate unequalIntegralSsa(
|
||||
Sem::SsaVariable v, SemBound b, D::Delta delta, Sem::SsaReadPosition pos, SemReason reason
|
||||
Sem::SsaVariable v, SemBound b, D::Delta delta, SsaReadPosition pos, SemReason reason
|
||||
) {
|
||||
exists(Sem::Expr e, D::Delta d1, D::Delta d2 |
|
||||
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
|
||||
@@ -920,7 +904,7 @@ module RangeStage<
|
||||
* - `upper = false` : `inp >= b + delta`
|
||||
*/
|
||||
private predicate boundedPhiInp(
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, SemBound b,
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, SemBound b,
|
||||
D::Delta delta, boolean upper, boolean fromBackEdge, D::Delta origdelta, SemReason reason
|
||||
) {
|
||||
edge.phiInput(phi, inp) and
|
||||
@@ -964,7 +948,7 @@ module RangeStage<
|
||||
pragma[noinline]
|
||||
private predicate boundedPhiInp1(
|
||||
Sem::SsaPhiNode phi, SemBound b, boolean upper, Sem::SsaVariable inp,
|
||||
Sem::SsaReadPositionPhiInputEdge edge, D::Delta delta
|
||||
SsaReadPositionPhiInputEdge edge, D::Delta delta
|
||||
) {
|
||||
boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)
|
||||
}
|
||||
@@ -976,7 +960,7 @@ module RangeStage<
|
||||
* - `upper = false` : `inp >= phi`
|
||||
*/
|
||||
private predicate selfBoundedPhiInp(
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, boolean upper
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge, boolean upper
|
||||
) {
|
||||
exists(D::Delta d, SemSsaBound phibound |
|
||||
phibound.getVariable() = phi and
|
||||
@@ -1009,8 +993,7 @@ module RangeStage<
|
||||
*/
|
||||
private predicate boundedPhiCandValidForEdge(
|
||||
Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
|
||||
D::Delta origdelta, SemReason reason, Sem::SsaVariable inp,
|
||||
Sem::SsaReadPositionPhiInputEdge edge
|
||||
D::Delta origdelta, SemReason reason, Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge
|
||||
) {
|
||||
boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and
|
||||
(
|
||||
@@ -1036,7 +1019,7 @@ module RangeStage<
|
||||
Sem::SsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,
|
||||
D::Delta origdelta, SemReason reason, int rix
|
||||
) {
|
||||
exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge |
|
||||
exists(Sem::SsaVariable inp, SsaReadPositionPhiInputEdge edge |
|
||||
rankedPhiInput(phi, inp, edge, rix) and
|
||||
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
|
||||
|
|
||||
@@ -1208,7 +1191,7 @@ module RangeStage<
|
||||
origdelta = delta and
|
||||
reason = TSemNoReason()
|
||||
or
|
||||
exists(Sem::SsaVariable v, Sem::SsaReadPositionBlock bb |
|
||||
exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
|
||||
boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and
|
||||
e = v.getAUse() and
|
||||
bb.getBlock() = e.getBasicBlock()
|
||||
|
||||
@@ -1,38 +1,99 @@
|
||||
private import codeql.rangeanalysis.RangeAnalysis
|
||||
|
||||
module MakeUtils<Semantic Lang, DeltaSig D> {
|
||||
private import Lang
|
||||
|
||||
/**
|
||||
* Gets an expression that equals `v - d`.
|
||||
*/
|
||||
Lang::Expr ssaRead(Lang::SsaVariable v, D::Delta delta) {
|
||||
Expr ssaRead(SsaVariable v, D::Delta delta) {
|
||||
result = v.getAUse() and delta = D::fromInt(0)
|
||||
or
|
||||
exists(D::Delta d1, Lang::ConstantIntegerExpr c |
|
||||
result.(Lang::AddExpr).hasOperands(ssaRead(v, d1), c) and
|
||||
exists(D::Delta d1, ConstantIntegerExpr c |
|
||||
result.(AddExpr).hasOperands(ssaRead(v, d1), c) and
|
||||
delta = D::fromFloat(D::toFloat(d1) - c.getIntValue()) and
|
||||
// In the scope of `x += ..`, which is SSA translated as `x2 = x1 + ..`,
|
||||
// the variable `x1` is shadowed by `x2`, so there's no need to view this
|
||||
// as a read of `x1`.
|
||||
not Lang::isAssignOp(result)
|
||||
not isAssignOp(result)
|
||||
)
|
||||
or
|
||||
exists(Lang::SubExpr sub, D::Delta d1, Lang::ConstantIntegerExpr c |
|
||||
exists(SubExpr sub, D::Delta d1, ConstantIntegerExpr c |
|
||||
result = sub and
|
||||
sub.getLeftOperand() = ssaRead(v, d1) and
|
||||
sub.getRightOperand() = c and
|
||||
delta = D::fromFloat(D::toFloat(d1) + c.getIntValue()) and
|
||||
not Lang::isAssignOp(result)
|
||||
not isAssignOp(result)
|
||||
)
|
||||
or
|
||||
result = v.(Lang::SsaExplicitUpdate).getDefiningExpr() and
|
||||
if result instanceof Lang::PostIncExpr
|
||||
result = v.(SsaExplicitUpdate).getDefiningExpr() and
|
||||
if result instanceof PostIncExpr
|
||||
then delta = D::fromFloat(1) // x++ === ++x - 1
|
||||
else
|
||||
if result instanceof Lang::PostDecExpr
|
||||
if result instanceof PostDecExpr
|
||||
then delta = D::fromFloat(-1) // x-- === --x + 1
|
||||
else delta = D::fromFloat(0)
|
||||
or
|
||||
result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
|
||||
result.(CopyValueExpr).getOperand() = ssaRead(v, delta)
|
||||
}
|
||||
|
||||
private newtype TSsaReadPosition =
|
||||
TSsaReadPositionBlock(BasicBlock bb) {
|
||||
exists(SsaVariable v | v.getAUse().getBasicBlock() = bb)
|
||||
} or
|
||||
TSsaReadPositionPhiInputEdge(BasicBlock bbOrig, BasicBlock bbPhi) {
|
||||
exists(SsaPhiNode phi | phi.hasInputFromBlock(_, bbOrig) and bbPhi = phi.getBasicBlock())
|
||||
}
|
||||
|
||||
/**
|
||||
* A position at which an SSA variable is read. This includes both ordinary
|
||||
* reads occurring in basic blocks and input to phi nodes occurring along an
|
||||
* edge between two basic blocks.
|
||||
*/
|
||||
class SsaReadPosition extends TSsaReadPosition {
|
||||
/** Holds if `v` is read at this position. */
|
||||
abstract predicate hasReadOfVar(SsaVariable v);
|
||||
|
||||
/** Gets a textual representation of this SSA read position. */
|
||||
abstract string toString();
|
||||
}
|
||||
|
||||
/** A basic block in which an SSA variable is read. */
|
||||
class SsaReadPositionBlock extends SsaReadPosition, TSsaReadPositionBlock {
|
||||
/** Gets the basic block corresponding to this position. */
|
||||
BasicBlock getBlock() { this = TSsaReadPositionBlock(result) }
|
||||
|
||||
override predicate hasReadOfVar(SsaVariable v) { exists(this.getAnSsaRead(v)) }
|
||||
|
||||
pragma[nomagic]
|
||||
Expr getAnSsaRead(SsaVariable v) {
|
||||
v.getAUse() = result and result.getBasicBlock() = this.getBlock()
|
||||
}
|
||||
|
||||
override string toString() { result = "block" }
|
||||
}
|
||||
|
||||
/**
|
||||
* An edge between two basic blocks where the latter block has an SSA phi
|
||||
* definition. The edge therefore has a read of an SSA variable serving as the
|
||||
* input to the phi node.
|
||||
*/
|
||||
class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiInputEdge {
|
||||
/** Gets the source of the edge. */
|
||||
BasicBlock getOrigBlock() { this = TSsaReadPositionPhiInputEdge(result, _) }
|
||||
|
||||
/** Gets the target of the edge. */
|
||||
BasicBlock getPhiBlock() { this = TSsaReadPositionPhiInputEdge(_, result) }
|
||||
|
||||
override predicate hasReadOfVar(SsaVariable v) { this.phiInput(_, v) }
|
||||
|
||||
/** Holds if `inp` is an input to `phi` along this edge. */
|
||||
predicate phiInput(SsaPhiNode phi, SsaVariable inp) {
|
||||
phi.hasInputFromBlock(inp, this.getOrigBlock()) and
|
||||
this.getPhiBlock() = phi.getBasicBlock()
|
||||
}
|
||||
|
||||
override string toString() { result = "edge" }
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -40,10 +101,10 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
|
||||
* value `testIsTrue`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate guardDirectlyControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guard.directlyControls(controlled.(Lang::SsaReadPositionBlock).getBlock(), testIsTrue)
|
||||
predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
|
||||
or
|
||||
exists(Lang::SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
|
||||
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
|
||||
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
|
||||
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
|
||||
)
|
||||
@@ -52,11 +113,11 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
|
||||
/**
|
||||
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
|
||||
*/
|
||||
predicate guardControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
|
||||
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
|
||||
or
|
||||
exists(Lang::Guard guard0, boolean testIsTrue0 |
|
||||
Lang::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
|
||||
exists(Guard guard0, boolean testIsTrue0 |
|
||||
implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
|
||||
guardControlsSsaRead(guard0, controlled, testIsTrue0)
|
||||
)
|
||||
}
|
||||
@@ -64,9 +125,7 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` along a back edge.
|
||||
*/
|
||||
predicate backEdge(
|
||||
Lang::SsaPhiNode phi, Lang::SsaVariable inp, Lang::SsaReadPositionPhiInputEdge edge
|
||||
) {
|
||||
predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
|
||||
edge.phiInput(phi, inp) and
|
||||
(
|
||||
phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
|
||||
@@ -85,12 +144,33 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
|
||||
* 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) {
|
||||
private predicate irreducibleSccEdge(BasicBlock b1, BasicBlock b2) {
|
||||
trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
|
||||
}
|
||||
|
||||
private predicate trimmedEdge(Lang::BasicBlock pred, Lang::BasicBlock succ) {
|
||||
Lang::getABasicBlockSuccessor(pred) = succ and
|
||||
private predicate trimmedEdge(BasicBlock pred, BasicBlock succ) {
|
||||
getABasicBlockSuccessor(pred) = succ and
|
||||
not succ.bbDominates(pred)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
|
||||
* in an arbitrary 1-based numbering of the input edges to `phi`.
|
||||
*/
|
||||
predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
|
||||
edge.phiInput(phi, inp) and
|
||||
edge =
|
||||
rank[r](SsaReadPositionPhiInputEdge e |
|
||||
e.phiInput(phi, _)
|
||||
|
|
||||
e order by getBlockId1(e.getOrigBlock()), getBlockId2(e.getOrigBlock())
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `rix` is the number of input edges to `phi`.
|
||||
*/
|
||||
predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
|
||||
rix = max(int r | rankedPhiInput(phi, _, _, r))
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user