Java/C++: Share ssaUpdateStep.

This commit is contained in:
Anders Schack-Mulligen
2023-11-09 15:56:17 +01:00
parent daffae020b
commit b8e7e1d15e
6 changed files with 31 additions and 49 deletions

View File

@@ -9,30 +9,6 @@ private import RangeAnalysisImpl
private import ConstantAnalysis private import ConstantAnalysis
module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> { module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate semSsaUpdateStep(SemSsaExplicitUpdate v, SemExpr e, D::Delta delta) {
exists(SemExpr defExpr | defExpr = v.getSourceExpr() |
defExpr.(SemCopyValueExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(SemStoreExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(SemAddOneExpr).getOperand() = e and delta = D::fromFloat(1)
or
defExpr.(SemSubOneExpr).getOperand() = e and delta = D::fromFloat(-1)
or
e = defExpr and
not (
defExpr instanceof SemCopyValueExpr or
defExpr instanceof SemStoreExpr or
defExpr instanceof SemAddOneExpr or
defExpr instanceof SemSubOneExpr
) and
delta = D::fromFloat(0)
)
}
/** /**
* Holds if `e1 + delta` equals `e2`. * Holds if `e1 + delta` equals `e2`.
*/ */

View File

@@ -372,10 +372,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
module Utils implements UtilSig<Sem, IntDelta> { module Utils implements UtilSig<Sem, IntDelta> {
private import RangeUtils as RU private import RangeUtils as RU
predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, int delta) {
RU::ssaUpdateStep(v, e, delta)
}
predicate semValueFlowStep = RU::valueFlowStep/3; predicate semValueFlowStep = RU::valueFlowStep/3;
Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) { Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) {

View File

@@ -15,6 +15,8 @@ private predicate backEdge = U::backEdge/3;
predicate ssaRead = U::ssaRead/2; predicate ssaRead = U::ssaRead/2;
predicate ssaUpdateStep = U::ssaUpdateStep/3;
predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3; predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
predicate guardControlsSsaRead = U::guardControlsSsaRead/3; predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
@@ -158,23 +160,6 @@ class ConstantStringExpr extends Expr {
string getStringValue() { constantStringExpr(this, result) } string getStringValue() { constantStringExpr(this, result) }
} }
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate ssaUpdateStep(SsaExplicitUpdate v, Expr e, int delta) {
v.getDefiningExpr().(VariableAssign).getSource() = e and delta = 0
or
v.getDefiningExpr().(PostIncExpr).getExpr() = e and delta = 1
or
v.getDefiningExpr().(PreIncExpr).getExpr() = e and delta = 1
or
v.getDefiningExpr().(PostDecExpr).getExpr() = e and delta = -1
or
v.getDefiningExpr().(PreDecExpr).getExpr() = e and delta = -1
or
v.getDefiningExpr().(AssignOp) = e and delta = 0
}
/** /**
* Holds if `e1 + delta` equals `e2`. * Holds if `e1 + delta` equals `e2`.
*/ */

View File

@@ -30,7 +30,7 @@ module ModulusAnalysis<
*/ */
pragma[nomagic] pragma[nomagic]
private predicate valueFlowStepSsa(Sem::SsaVariable v, 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) ssaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
or or
exists(Sem::Guard guard, boolean testIsTrue | exists(Sem::Guard guard, boolean testIsTrue |
hasReadOfVarInlineLate(pos, v) and hasReadOfVarInlineLate(pos, v) and

View File

@@ -304,8 +304,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
} }
signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> { signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, DeltaParam::Delta delta);
predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta); predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta);
/** /**
@@ -671,7 +669,7 @@ module RangeStage<
Sem::SsaVariable v, 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 SemReason reason
) { ) {
semSsaUpdateStep(v, e, delta) and ssaUpdateStep(v, e, delta) and
pos.hasReadOfVar(v) and pos.hasReadOfVar(v) and
(upper = true or upper = false) and (upper = true or upper = false) and
reason = TSemNoReason() reason = TSemNoReason()

View File

@@ -57,6 +57,33 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
) )
} }
/**
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
*/
predicate ssaUpdateStep(SsaExplicitUpdate v, Expr e, D::Delta delta) {
exists(Expr defExpr | defExpr = v.getDefiningExpr() |
defExpr.(CopyValueExpr).getOperand() = e and delta = D::fromFloat(0)
or
defExpr.(PostIncExpr).getOperand() = e and delta = D::fromFloat(1)
or
defExpr.(PreIncExpr).getOperand() = e and delta = D::fromFloat(1)
or
defExpr.(PostDecExpr).getOperand() = e and delta = D::fromFloat(-1)
or
defExpr.(PreDecExpr).getOperand() = e and delta = D::fromFloat(-1)
or
e = defExpr and
not (
defExpr instanceof CopyValueExpr or
defExpr instanceof PostIncExpr or
defExpr instanceof PreIncExpr or
defExpr instanceof PostDecExpr or
defExpr instanceof PreDecExpr
) and
delta = D::fromFloat(0)
)
}
private newtype TSsaReadPosition = private newtype TSsaReadPosition =
TSsaReadPositionBlock(BasicBlock bb) { TSsaReadPositionBlock(BasicBlock bb) {
exists(SsaVariable v | v.getAUse().getBasicBlock() = bb) exists(SsaVariable v | v.getAUse().getBasicBlock() = bb)