Rangeanalysis: Switch to shared ssaRead predicate.

This commit is contained in:
Anders Schack-Mulligen
2023-10-31 15:23:05 +01:00
parent 19644a8f07
commit a39a94ca8e
4 changed files with 16 additions and 17 deletions

View File

@@ -12,7 +12,7 @@ module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
/** /**
* Gets an expression that equals `v - d`. * Gets an expression that equals `v - d`.
*/ */
SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) { private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
// There are various language-specific extension points that can be removed once we no longer // There are various language-specific extension points that can be removed once we no longer
// expect to match the original Java implementation's results exactly. // expect to match the original Java implementation's results exactly.
result = v.getAUse() and delta = D::fromInt(0) result = v.getAUse() and delta = D::fromInt(0)

View File

@@ -15,6 +15,8 @@ private import RangeUtils
private import Sign private import Sign
module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> { module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils<Sem, D>
/** /**
* An SSA definition for which the analysis can compute the sign. * An SSA definition for which the analysis can compute the sign.
* *
@@ -297,12 +299,12 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
| |
testIsTrue = true and testIsTrue = true and
comp.getLesserOperand() = lowerbound and comp.getLesserOperand() = lowerbound and
comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = true else isStrict = false) (if comp.isStrict() then isStrict = true else isStrict = false)
or or
testIsTrue = false and testIsTrue = false and
comp.getGreaterOperand() = lowerbound and comp.getGreaterOperand() = lowerbound and
comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = false else isStrict = true) (if comp.isStrict() then isStrict = false else isStrict = true)
) )
} }
@@ -321,12 +323,12 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
| |
testIsTrue = true and testIsTrue = true and
comp.getGreaterOperand() = upperbound and comp.getGreaterOperand() = upperbound and
comp.getLesserOperand() = Utils::semSsaRead(v, D::fromInt(0)) and comp.getLesserOperand() = ssaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = true else isStrict = false) (if comp.isStrict() then isStrict = true else isStrict = false)
or or
testIsTrue = false and testIsTrue = false and
comp.getLesserOperand() = upperbound and comp.getLesserOperand() = upperbound and
comp.getGreaterOperand() = Utils::semSsaRead(v, D::fromInt(0)) and comp.getGreaterOperand() = ssaRead(v, D::fromInt(0)) and
(if comp.isStrict() then isStrict = false else isStrict = true) (if comp.isStrict() then isStrict = false else isStrict = true)
) )
} }
@@ -342,7 +344,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e | exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
pos.hasReadOfVar(pragma[only_bind_into](v)) and pos.hasReadOfVar(pragma[only_bind_into](v)) and
semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
e = Utils::semSsaRead(pragma[only_bind_into](v), D::fromInt(0)) and e = ssaRead(pragma[only_bind_into](v), D::fromInt(0)) and
guard.isEquality(eqbound, e, polarity) and guard.isEquality(eqbound, e, polarity) and
isEq = polarity.booleanXor(testIsTrue).booleanNot() and isEq = polarity.booleanXor(testIsTrue).booleanNot() and
not unknownSign(eqbound) not unknownSign(eqbound)

View File

@@ -396,8 +396,6 @@ module Utils implements UtilSig<Sem, IntDelta> {
private import RangeUtils as RU private import RangeUtils as RU
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaReadPos
Sem::Expr semSsaRead(Sem::SsaVariable v, int delta) { result = RU::ssaRead(v, delta) }
Sem::Guard semEqFlowCond( Sem::Guard semEqFlowCond(
Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
) { ) {

View File

@@ -337,8 +337,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
} }
signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> { signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
Sem::Expr semSsaRead(Sem::SsaVariable v, DeltaParam::Delta delta);
Sem::Guard semEqFlowCond( Sem::Guard semEqFlowCond(
Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
); );
@@ -409,6 +407,7 @@ module RangeStage<
private import OverflowParam private import OverflowParam
private import SignAnalysis private import SignAnalysis
private import ModulusAnalysis private import ModulusAnalysis
private import internal.RangeUtils::MakeUtils<Sem, D>
/** /**
* An expression that does conversion, boxing, or unboxing * An expression that does conversion, boxing, or unboxing
@@ -522,11 +521,11 @@ module RangeStage<
private predicate boundCondition( private predicate boundCondition(
Sem::RelationalExpr comp, Sem::SsaVariable v, Sem::Expr e, D::Delta delta, boolean upper Sem::RelationalExpr comp, Sem::SsaVariable v, Sem::Expr e, D::Delta delta, boolean upper
) { ) {
comp.getLesserOperand() = semSsaRead(v, delta) and comp.getLesserOperand() = ssaRead(v, delta) and
e = comp.getGreaterOperand() and e = comp.getGreaterOperand() and
upper = true upper = true
or or
comp.getGreaterOperand() = semSsaRead(v, delta) and comp.getGreaterOperand() = ssaRead(v, delta) and
e = comp.getLesserOperand() and e = comp.getLesserOperand() and
upper = false upper = false
or or
@@ -534,7 +533,7 @@ module RangeStage<
// (v - d) - e < c // (v - d) - e < c
comp.getLesserOperand() = sub and comp.getLesserOperand() = sub and
comp.getGreaterOperand() = c and comp.getGreaterOperand() = c and
sub.getLeftOperand() = semSsaRead(v, d) and sub.getLeftOperand() = ssaRead(v, d) and
sub.getRightOperand() = e and sub.getRightOperand() = e and
upper = true and upper = true and
delta = D::fromFloat(D::toFloat(d) + c.getIntValue()) delta = D::fromFloat(D::toFloat(d) + c.getIntValue())
@@ -542,7 +541,7 @@ module RangeStage<
// (v - d) - e > c // (v - d) - e > c
comp.getGreaterOperand() = sub and comp.getGreaterOperand() = sub and
comp.getLesserOperand() = c and comp.getLesserOperand() = c and
sub.getLeftOperand() = semSsaRead(v, d) and sub.getLeftOperand() = ssaRead(v, d) and
sub.getRightOperand() = e and sub.getRightOperand() = e and
upper = false and upper = false and
delta = D::fromFloat(D::toFloat(d) + c.getIntValue()) delta = D::fromFloat(D::toFloat(d) + c.getIntValue())
@@ -551,7 +550,7 @@ module RangeStage<
comp.getLesserOperand() = sub and comp.getLesserOperand() = sub and
comp.getGreaterOperand() = c and comp.getGreaterOperand() = c and
sub.getLeftOperand() = e and sub.getLeftOperand() = e and
sub.getRightOperand() = semSsaRead(v, d) and sub.getRightOperand() = ssaRead(v, d) and
upper = false and upper = false and
delta = D::fromFloat(D::toFloat(d) - c.getIntValue()) delta = D::fromFloat(D::toFloat(d) - c.getIntValue())
or or
@@ -559,7 +558,7 @@ module RangeStage<
comp.getGreaterOperand() = sub and comp.getGreaterOperand() = sub and
comp.getLesserOperand() = c and comp.getLesserOperand() = c and
sub.getLeftOperand() = e and sub.getLeftOperand() = e and
sub.getRightOperand() = semSsaRead(v, d) and sub.getRightOperand() = ssaRead(v, d) and
upper = true and upper = true and
delta = D::fromFloat(D::toFloat(d) - c.getIntValue()) delta = D::fromFloat(D::toFloat(d) - c.getIntValue())
) )
@@ -677,7 +676,7 @@ module RangeStage<
Sem::SsaVariable v1, Sem::SsaVariable v2, float delta Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
) { ) {
exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue | exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
guardEq = semEqFlowCond(v1, semSsaRead(v2, d1), d2, true, eqIsTrue) and guardEq = semEqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
delta = D::toFloat(d2) - D::toFloat(d1) and delta = D::toFloat(d2) - D::toFloat(d1) and
guardEq.directlyControls(result, eqIsTrue) guardEq.directlyControls(result, eqIsTrue)
) )