mirror of
https://github.com/github/codeql.git
synced 2026-04-24 16:25:15 +02:00
Java: Replace range analysis with shared version.
This commit is contained in:
Anders Schack-Mulligen
@@ -424,276 +424,13 @@ module Overflow implements OverflowSig<Sem, IntDelta> {
|
||||
module Range =
|
||||
RangeStage<Location, Sem, IntDelta, Bounds, Overflow, JavaLangImpl, SignInp, Modulus, Utils>;
|
||||
|
||||
cached
|
||||
private module RangeAnalysisCache {
|
||||
cached
|
||||
module RangeAnalysisPublic {
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `e`.
|
||||
* - `upper = true` : `e <= b + delta`
|
||||
* - `upper = false` : `e >= b + delta`
|
||||
*
|
||||
* The reason for the bound is given by `reason` and may be either a condition
|
||||
* or `NoReason` if the bound was proven directly without the use of a bounding
|
||||
* condition.
|
||||
*/
|
||||
cached
|
||||
predicate bounded(Expr e, Bound b, int delta, boolean upper, Reason reason) {
|
||||
bounded(e, b, delta, upper, _, _, reason) and
|
||||
bestBound(e, b, delta, upper)
|
||||
}
|
||||
}
|
||||
predicate bounded = Range::semBounded/5;
|
||||
|
||||
/**
|
||||
* Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
|
||||
*/
|
||||
cached
|
||||
predicate possibleReason(Guard guard) {
|
||||
guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)
|
||||
}
|
||||
}
|
||||
class Reason = Range::SemReason;
|
||||
|
||||
private import RangeAnalysisCache
|
||||
import RangeAnalysisPublic
|
||||
class NoReason = Range::SemNoReason;
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `e` and this is the best such delta.
|
||||
* - `upper = true` : `e <= b + delta`
|
||||
* - `upper = false` : `e >= b + delta`
|
||||
*/
|
||||
private predicate bestBound(Expr e, Bound b, int delta, boolean upper) {
|
||||
delta = min(int d | bounded(e, b, d, upper, _, _, _)) and upper = true
|
||||
or
|
||||
delta = max(int d | bounded(e, b, d, upper, _, _, _)) and upper = false
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `comp` corresponds to:
|
||||
* - `upper = true` : `v <= e + delta` or `v < e + delta`
|
||||
* - `upper = false` : `v >= e + delta` or `v > e + delta`
|
||||
*/
|
||||
private predicate boundCondition(
|
||||
ComparisonExpr comp, SsaVariable v, Expr e, int delta, boolean upper
|
||||
) {
|
||||
comp.getLesserOperand() = ssaRead(v, delta) and e = comp.getGreaterOperand() and upper = true
|
||||
or
|
||||
comp.getGreaterOperand() = ssaRead(v, delta) and e = comp.getLesserOperand() and upper = false
|
||||
or
|
||||
exists(SubExpr sub, ConstantIntegerExpr c, int d |
|
||||
// (v - d) - e < c
|
||||
comp.getLesserOperand() = sub and
|
||||
comp.getGreaterOperand() = c and
|
||||
sub.getLeftOperand() = ssaRead(v, d) and
|
||||
sub.getRightOperand() = e and
|
||||
upper = true and
|
||||
delta = d + c.getIntValue() and
|
||||
okInt(d.(float) + c.getIntValue().(float))
|
||||
or
|
||||
// (v - d) - e > c
|
||||
comp.getGreaterOperand() = sub and
|
||||
comp.getLesserOperand() = c and
|
||||
sub.getLeftOperand() = ssaRead(v, d) and
|
||||
sub.getRightOperand() = e and
|
||||
upper = false and
|
||||
delta = d + c.getIntValue() and
|
||||
okInt(d.(float) + c.getIntValue().(float))
|
||||
or
|
||||
// e - (v - d) < c
|
||||
comp.getLesserOperand() = sub and
|
||||
comp.getGreaterOperand() = c and
|
||||
sub.getLeftOperand() = e and
|
||||
sub.getRightOperand() = ssaRead(v, d) and
|
||||
upper = false and
|
||||
delta = d - c.getIntValue() and
|
||||
okInt(d.(float) - c.getIntValue().(float))
|
||||
or
|
||||
// e - (v - d) > c
|
||||
comp.getGreaterOperand() = sub and
|
||||
comp.getLesserOperand() = c and
|
||||
sub.getLeftOperand() = e and
|
||||
sub.getRightOperand() = ssaRead(v, d) and
|
||||
upper = true and
|
||||
delta = d - c.getIntValue() and
|
||||
okInt(d.(float) - c.getIntValue().(float))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `comp` is a comparison between `x` and `y` for which `y - x` has a
|
||||
* fixed value modulo some `mod > 1`, such that the comparison can be
|
||||
* strengthened by `strengthen` when evaluating to `testIsTrue`.
|
||||
*/
|
||||
private predicate modulusComparison(ComparisonExpr comp, boolean testIsTrue, int strengthen) {
|
||||
exists(
|
||||
Bound b, int v1, int v2, int mod1, int mod2, int mod, boolean resultIsStrict, int d, int k
|
||||
|
|
||||
// If `x <= y` and `x =(mod) b + v1` and `y =(mod) b + v2` then
|
||||
// `0 <= y - x =(mod) v2 - v1`. By choosing `k =(mod) v2 - v1` with
|
||||
// `0 <= k < mod` we get `k <= y - x`. If the resulting comparison is
|
||||
// strict then the strengthening amount is instead `k - 1` modulo `mod`:
|
||||
// `x < y` means `0 <= y - x - 1 =(mod) k - 1` so `k - 1 <= y - x - 1` and
|
||||
// thus `k - 1 < y - x` with `0 <= k - 1 < mod`.
|
||||
exprModulus(comp.getLesserOperand(), b, v1, mod1) and
|
||||
exprModulus(comp.getGreaterOperand(), b, v2, mod2) and
|
||||
mod = mod1.gcd(mod2) and
|
||||
mod != 1 and
|
||||
(testIsTrue = true or testIsTrue = false) and
|
||||
(
|
||||
if comp.isStrict()
|
||||
then resultIsStrict = testIsTrue
|
||||
else resultIsStrict = testIsTrue.booleanNot()
|
||||
) and
|
||||
(
|
||||
resultIsStrict = true and d = 1
|
||||
or
|
||||
resultIsStrict = false and d = 0
|
||||
) and
|
||||
(
|
||||
testIsTrue = true and k = v2 - v1
|
||||
or
|
||||
testIsTrue = false and k = v1 - v2
|
||||
) and
|
||||
strengthen = (((k - d) % mod) + mod) % mod
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a condition that tests whether `v` is bounded by `e + delta`.
|
||||
*
|
||||
* If the condition evaluates to `testIsTrue`:
|
||||
* - `upper = true` : `v <= e + delta`
|
||||
* - `upper = false` : `v >= e + delta`
|
||||
*/
|
||||
private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boolean testIsTrue) {
|
||||
exists(
|
||||
ComparisonExpr comp, int d1, int d2, int d3, int strengthen, boolean compIsUpper,
|
||||
boolean resultIsStrict
|
||||
|
|
||||
comp = result and
|
||||
boundCondition(comp, v, e, d1, compIsUpper) and
|
||||
(testIsTrue = true or testIsTrue = false) and
|
||||
upper = compIsUpper.booleanXor(testIsTrue.booleanNot()) and
|
||||
(
|
||||
if comp.isStrict()
|
||||
then resultIsStrict = testIsTrue
|
||||
else resultIsStrict = testIsTrue.booleanNot()
|
||||
) and
|
||||
(
|
||||
if v.getSourceVariable().getType() instanceof IntegralType
|
||||
then
|
||||
upper = true and strengthen = -1
|
||||
or
|
||||
upper = false and strengthen = 1
|
||||
else strengthen = 0
|
||||
) and
|
||||
(
|
||||
exists(int k | modulusComparison(comp, testIsTrue, k) and d2 = strengthen * k)
|
||||
or
|
||||
not modulusComparison(comp, testIsTrue, _) and d2 = 0
|
||||
) and
|
||||
// A strict inequality `x < y` can be strengthened to `x <= y - 1`.
|
||||
(
|
||||
resultIsStrict = true and d3 = strengthen
|
||||
or
|
||||
resultIsStrict = false and d3 = 0
|
||||
) and
|
||||
delta = d1 + d2 + d3 and
|
||||
okInt(d1.(float) + d2.(float) + d3.(float))
|
||||
)
|
||||
or
|
||||
exists(boolean testIsTrue0 |
|
||||
implies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0), testIsTrue0)
|
||||
)
|
||||
or
|
||||
result = eqFlowCond(v, e, delta, true, testIsTrue) and
|
||||
(upper = true or upper = false)
|
||||
or
|
||||
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
|
||||
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
|
||||
exists(SsaVariable v2, int d |
|
||||
// equality needs to control guard
|
||||
result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and
|
||||
result = boundFlowCond(v2, e, delta - d, upper, testIsTrue) and
|
||||
okInt((delta - d).(float) + d.(float))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a basic block in which `v1` equals `v2 + delta`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private BasicBlock eqSsaCondDirectlyControls(SsaVariable v1, SsaVariable v2, int delta) {
|
||||
exists(Guard guardEq, int d1, int d2, boolean eqIsTrue |
|
||||
guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
|
||||
delta = d2 - d1 and
|
||||
guardEq.directlyControls(result, eqIsTrue) and
|
||||
okInt(d2.(float) - d1.(float))
|
||||
)
|
||||
}
|
||||
|
||||
private newtype TReason =
|
||||
TNoReason() or
|
||||
TCondReason(Guard guard) { possibleReason(guard) }
|
||||
|
||||
/**
|
||||
* A reason for an inferred bound. This can either be `CondReason` if the bound
|
||||
* is due to a specific condition, or `NoReason` if the bound is inferred
|
||||
* without going through a bounding condition.
|
||||
*/
|
||||
abstract class Reason extends TReason {
|
||||
/** Gets a textual representation of this reason. */
|
||||
abstract string toString();
|
||||
}
|
||||
|
||||
/**
|
||||
* A reason for an inferred bound that indicates that the bound is inferred
|
||||
* without going through a bounding condition.
|
||||
*/
|
||||
class NoReason extends Reason, TNoReason {
|
||||
override string toString() { result = "NoReason" }
|
||||
}
|
||||
|
||||
/** A reason for an inferred bound pointing to a condition. */
|
||||
class CondReason extends Reason, TCondReason {
|
||||
/** Gets the condition that is the reason for the bound. */
|
||||
Guard getCond() { this = TCondReason(result) }
|
||||
|
||||
override string toString() { result = this.getCond().toString() }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e + delta` is a valid bound for `v` at `pos`.
|
||||
* - `upper = true` : `v <= e + delta`
|
||||
* - `upper = false` : `v >= e + delta`
|
||||
*/
|
||||
private predicate boundFlowStepSsa(
|
||||
SsaVariable v, SsaReadPosition pos, Expr e, int delta, boolean upper, Reason reason
|
||||
) {
|
||||
ssaUpdateStep(v, e, delta) and
|
||||
pos.hasReadOfVar(v) and
|
||||
(upper = true or upper = false) and
|
||||
reason = TNoReason()
|
||||
or
|
||||
exists(Guard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
|
||||
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TCondReason(guard)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
|
||||
private predicate unequalFlowStepIntegralSsa(
|
||||
SsaVariable v, SsaReadPosition pos, Expr e, int delta, Reason reason
|
||||
) {
|
||||
v.getSourceVariable().getType() instanceof IntegralType and
|
||||
exists(Guard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = eqFlowCond(v, e, delta, false, testIsTrue) and
|
||||
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TCondReason(guard)
|
||||
)
|
||||
}
|
||||
class CondReason = Range::SemCondReason;
|
||||
|
||||
/**
|
||||
* Holds if a cast from `fromtyp` to `totyp` can be ignored for the purpose of
|
||||
@@ -722,581 +459,3 @@ private predicate safeCast(Type fromtyp, Type totyp) {
|
||||
or
|
||||
safeCast(fromtyp, totyp.(BoxedType).getPrimitiveType())
|
||||
}
|
||||
|
||||
/**
|
||||
* A cast that can be ignored for the purpose of range analysis.
|
||||
*/
|
||||
private class RangeAnalysisSafeCastingExpr extends CastingExpr {
|
||||
RangeAnalysisSafeCastingExpr() {
|
||||
safeCast(this.getExpr().getType(), this.getType()) or
|
||||
this instanceof ImplicitCastExpr or
|
||||
this instanceof ImplicitNotNullExpr or
|
||||
this instanceof ImplicitCoercionToUnitExpr
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `typ` is a small integral type with the given lower and upper bounds.
|
||||
*/
|
||||
private predicate typeBound(Type typ, int lowerbound, int upperbound) {
|
||||
typ.(PrimitiveType).hasName("byte") and lowerbound = -128 and upperbound = 127
|
||||
or
|
||||
typ.(PrimitiveType).hasName("short") and lowerbound = -32768 and upperbound = 32767
|
||||
or
|
||||
typ.(PrimitiveType).hasName("char") and lowerbound = 0 and upperbound = 65535
|
||||
or
|
||||
typeBound(typ.(BoxedType).getPrimitiveType(), lowerbound, upperbound)
|
||||
}
|
||||
|
||||
/**
|
||||
* A cast to a small integral type that may overflow or underflow.
|
||||
*/
|
||||
private class NarrowingCastingExpr extends CastingExpr {
|
||||
NarrowingCastingExpr() {
|
||||
not this instanceof RangeAnalysisSafeCastingExpr and
|
||||
typeBound(this.getType(), _, _)
|
||||
}
|
||||
|
||||
/** Gets the lower bound of the resulting type. */
|
||||
int getLowerBound() { typeBound(this.getType(), result, _) }
|
||||
|
||||
/** Gets the upper bound of the resulting type. */
|
||||
int getUpperBound() { typeBound(this.getType(), _, result) }
|
||||
}
|
||||
|
||||
/** Holds if `e >= 1` as determined by sign analysis. */
|
||||
private predicate strictlyPositiveIntegralExpr(Expr e) {
|
||||
strictlyPositive(e) and e.getType() instanceof IntegralType
|
||||
}
|
||||
|
||||
/** Holds if `e <= -1` as determined by sign analysis. */
|
||||
private predicate strictlyNegativeIntegralExpr(Expr e) {
|
||||
strictlyNegative(e) and e.getType() instanceof IntegralType
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e1 + delta` is a valid bound for `e2`.
|
||||
* - `upper = true` : `e2 <= e1 + delta`
|
||||
* - `upper = false` : `e2 >= e1 + delta`
|
||||
*/
|
||||
private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
|
||||
valueFlowStep(e2, e1, delta) and
|
||||
(upper = true or upper = false)
|
||||
or
|
||||
e2.(RangeAnalysisSafeCastingExpr).getExpr() = e1 and
|
||||
delta = 0 and
|
||||
(upper = true or upper = false)
|
||||
or
|
||||
exists(Expr x |
|
||||
exists(SubExpr sub |
|
||||
e2 = sub and
|
||||
sub.getLeftOperand() = e1 and
|
||||
sub.getRightOperand() = x
|
||||
)
|
||||
or
|
||||
exists(AssignSubExpr sub |
|
||||
e2 = sub and
|
||||
sub.getDest() = e1 and
|
||||
sub.getRhs() = x
|
||||
)
|
||||
|
|
||||
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
|
||||
not x instanceof ConstantIntegerExpr and
|
||||
if strictlyPositiveIntegralExpr(x)
|
||||
then upper = true and delta = -1
|
||||
else
|
||||
if positive(x)
|
||||
then upper = true and delta = 0
|
||||
else
|
||||
if strictlyNegativeIntegralExpr(x)
|
||||
then upper = false and delta = 1
|
||||
else
|
||||
if negative(x)
|
||||
then upper = false and delta = 0
|
||||
else none()
|
||||
)
|
||||
or
|
||||
e2.(RemExpr).getRightOperand() = e1 and positive(e1) and delta = -1 and upper = true
|
||||
or
|
||||
e2.(RemExpr).getLeftOperand() = e1 and positive(e1) and delta = 0 and upper = true
|
||||
or
|
||||
e2.(AssignRemExpr).getRhs() = e1 and positive(e1) and delta = -1 and upper = true
|
||||
or
|
||||
e2.(AssignRemExpr).getDest() = e1 and positive(e1) and delta = 0 and upper = true
|
||||
or
|
||||
e2.(AndBitwiseExpr).getAnOperand() = e1 and positive(e1) and delta = 0 and upper = true
|
||||
or
|
||||
e2.(AssignAndExpr).getSource() = e1 and positive(e1) and delta = 0 and upper = true
|
||||
or
|
||||
e2.(OrBitwiseExpr).getAnOperand() = e1 and positive(e2) and delta = 0 and upper = false
|
||||
or
|
||||
e2.(AssignOrExpr).getSource() = e1 and positive(e2) and delta = 0 and upper = false
|
||||
or
|
||||
exists(RandomDataSource rds |
|
||||
e2 = rds.getOutput() and
|
||||
(
|
||||
e1 = rds.getUpperBoundExpr() and
|
||||
delta = -1 and
|
||||
upper = true
|
||||
or
|
||||
e1 = rds.getLowerBoundExpr() and
|
||||
delta = 0 and
|
||||
upper = false
|
||||
)
|
||||
)
|
||||
or
|
||||
exists(MethodCall ma, Method m |
|
||||
e2 = ma and
|
||||
ma.getMethod() = m and
|
||||
(
|
||||
m.hasName("max") and upper = false
|
||||
or
|
||||
m.hasName("min") and upper = true
|
||||
) and
|
||||
m.getDeclaringType().hasQualifiedName("java.lang", "Math") and
|
||||
e1 = ma.getAnArgument() and
|
||||
delta = 0
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
|
||||
private predicate boundFlowStepMul(Expr e2, Expr e1, int factor) {
|
||||
exists(ConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
|
||||
e2.(MulExpr).hasOperands(e1, c) and factor = k
|
||||
or
|
||||
exists(AssignMulExpr e | e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = k)
|
||||
or
|
||||
exists(AssignMulExpr e | e = e2 and e.getDest() = c and e.getRhs() = e1 and factor = k)
|
||||
or
|
||||
exists(LeftShiftExpr e |
|
||||
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
|
||||
)
|
||||
or
|
||||
exists(AssignLeftShiftExpr e |
|
||||
e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e2 = e1 / factor` and `factor > 0`.
|
||||
*
|
||||
* This conflates division, right shift, and unsigned right shift and is
|
||||
* therefore only valid for non-negative numbers.
|
||||
*/
|
||||
private predicate boundFlowStepDiv(Expr e2, Expr e1, int factor) {
|
||||
e2.getType() instanceof IntegralType and
|
||||
exists(ConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
|
||||
exists(DivExpr e |
|
||||
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = k
|
||||
)
|
||||
or
|
||||
exists(AssignDivExpr e | e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = k)
|
||||
or
|
||||
exists(RightShiftExpr e |
|
||||
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
|
||||
)
|
||||
or
|
||||
exists(AssignRightShiftExpr e |
|
||||
e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
|
||||
)
|
||||
or
|
||||
exists(UnsignedRightShiftExpr e |
|
||||
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
|
||||
)
|
||||
or
|
||||
exists(AssignUnsignedRightShiftExpr e |
|
||||
e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `v` at `pos`.
|
||||
* - `upper = true` : `v <= b + delta`
|
||||
* - `upper = false` : `v >= b + delta`
|
||||
*/
|
||||
private predicate boundedSsa(
|
||||
SsaVariable v, SsaReadPosition pos, Bound b, int delta, boolean upper, boolean fromBackEdge,
|
||||
int origdelta, Reason reason
|
||||
) {
|
||||
exists(Expr mid, int d1, int d2, Reason r1, Reason r2 |
|
||||
boundFlowStepSsa(v, pos, mid, d1, upper, r1) and
|
||||
bounded(mid, b, d2, upper, fromBackEdge, origdelta, r2) and
|
||||
// upper = true: v <= mid + d1 <= b + d1 + d2 = b + delta
|
||||
// upper = false: v >= mid + d1 >= b + d1 + d2 = b + delta
|
||||
delta = d1 + d2 and
|
||||
(if r1 instanceof NoReason then reason = r2 else reason = r1) and
|
||||
okInt(d1.(float) + d2.(float))
|
||||
)
|
||||
or
|
||||
exists(int d, Reason r1, Reason r2 |
|
||||
boundedSsa(v, pos, b, d, upper, fromBackEdge, origdelta, r2) or
|
||||
boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2)
|
||||
|
|
||||
unequalIntegralSsa(v, pos, b, d, r1) and
|
||||
(
|
||||
upper = true and delta = d - 1
|
||||
or
|
||||
upper = false and delta = d + 1
|
||||
) and
|
||||
(
|
||||
reason = r1
|
||||
or
|
||||
reason = r2 and not r2 instanceof NoReason
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `v != b + delta` at `pos` and `v` is of integral type.
|
||||
*/
|
||||
private predicate unequalIntegralSsa(
|
||||
SsaVariable v, SsaReadPosition pos, Bound b, int delta, Reason reason
|
||||
) {
|
||||
exists(Expr e, int d1, int d2 |
|
||||
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
|
||||
bounded(e, b, d2, true, _, _, _) and
|
||||
bounded(e, b, d2, false, _, _, _) and
|
||||
delta = d2 + d1
|
||||
)
|
||||
}
|
||||
|
||||
/** Weakens a delta to lie in the range `[-1..1]`. */
|
||||
bindingset[delta, upper]
|
||||
private int weakenDelta(boolean upper, int delta) {
|
||||
delta in [-1 .. 1] and result = delta
|
||||
or
|
||||
upper = true and result = -1 and delta < -1
|
||||
or
|
||||
upper = false and result = 1 and delta > 1
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `inp` when used as an input to
|
||||
* `phi` along `edge`.
|
||||
* - `upper = true` : `inp <= b + delta`
|
||||
* - `upper = false` : `inp >= b + delta`
|
||||
*/
|
||||
private predicate boundedPhiInp(
|
||||
SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, Bound b, int delta,
|
||||
boolean upper, boolean fromBackEdge, int origdelta, Reason reason
|
||||
) {
|
||||
edge.phiInput(phi, inp) and
|
||||
exists(int d, boolean fromBackEdge0 |
|
||||
boundedSsa(inp, edge, b, d, upper, fromBackEdge0, origdelta, reason)
|
||||
or
|
||||
boundedPhi(inp, b, d, upper, fromBackEdge0, origdelta, reason)
|
||||
or
|
||||
b.(SsaBound).getSsa() = inp and
|
||||
d = 0 and
|
||||
(upper = true or upper = false) and
|
||||
fromBackEdge0 = false and
|
||||
origdelta = 0 and
|
||||
reason = TNoReason()
|
||||
|
|
||||
if backEdge(phi, inp, edge)
|
||||
then
|
||||
fromBackEdge = true and
|
||||
(
|
||||
fromBackEdge0 = true and delta = weakenDelta(upper, d - origdelta) + origdelta
|
||||
or
|
||||
fromBackEdge0 = false and delta = d
|
||||
)
|
||||
else (
|
||||
delta = d and fromBackEdge = fromBackEdge0
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)`. */
|
||||
pragma[noinline]
|
||||
private predicate boundedPhiInp1(
|
||||
SsaPhiNode phi, Bound b, boolean upper, SsaVariable inp, SsaReadPositionPhiInputEdge edge,
|
||||
int delta
|
||||
) {
|
||||
boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `phi` is a valid bound for `inp` when used as an input to `phi`
|
||||
* along `edge`.
|
||||
* - `upper = true` : `inp <= phi`
|
||||
* - `upper = false` : `inp >= phi`
|
||||
*/
|
||||
private predicate selfBoundedPhiInp(
|
||||
SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, boolean upper
|
||||
) {
|
||||
exists(int d, SsaBound phibound |
|
||||
phibound.getSsa() = phi and
|
||||
boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _, _) and
|
||||
(
|
||||
upper = true and d <= 0
|
||||
or
|
||||
upper = false and d >= 0
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for some input, `inp`, to `phi`, and
|
||||
* thus a candidate bound for `phi`.
|
||||
* - `upper = true` : `inp <= b + delta`
|
||||
* - `upper = false` : `inp >= b + delta`
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate boundedPhiCand(
|
||||
SsaPhiNode phi, boolean upper, Bound b, int delta, boolean fromBackEdge, int origdelta,
|
||||
Reason reason
|
||||
) {
|
||||
boundedPhiInp(phi, _, _, b, delta, upper, fromBackEdge, origdelta, reason)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the candidate bound `b + delta` for `phi` is valid for the phi input
|
||||
* `inp` along `edge`.
|
||||
*/
|
||||
private predicate boundedPhiCandValidForEdge(
|
||||
SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
Reason reason, SsaVariable inp, SsaReadPositionPhiInputEdge edge
|
||||
) {
|
||||
boundedPhiCand(phi, upper, b, delta, fromBackEdge, origdelta, reason) and
|
||||
(
|
||||
exists(int d | boundedPhiInp1(phi, b, upper, inp, edge, d) | upper = true and d <= delta)
|
||||
or
|
||||
exists(int d | boundedPhiInp1(phi, b, upper, inp, edge, d) | upper = false and d >= delta)
|
||||
or
|
||||
selfBoundedPhiInp(phi, inp, edge, upper)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `phi`'s `rix`th input edge.
|
||||
* - `upper = true` : `phi <= b + delta`
|
||||
* - `upper = false` : `phi >= b + delta`
|
||||
*/
|
||||
private predicate boundedPhiStep(
|
||||
SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
Reason reason, int rix
|
||||
) {
|
||||
exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge |
|
||||
rankedPhiInput(phi, inp, edge, rix) and
|
||||
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) and
|
||||
(
|
||||
rix = 1
|
||||
or
|
||||
boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `phi`.
|
||||
* - `upper = true` : `phi <= b + delta`
|
||||
* - `upper = false` : `phi >= b + delta`
|
||||
*/
|
||||
private predicate boundedPhi(
|
||||
SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
Reason reason
|
||||
) {
|
||||
exists(int r |
|
||||
boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r) and
|
||||
maxPhiInputRank(phi, r)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e` has a lower bound of zero.
|
||||
*/
|
||||
private predicate lowerBoundZero(Expr e) {
|
||||
e.(MethodCall).getMethod() instanceof StringLengthMethod or
|
||||
e.(MethodCall).getMethod() instanceof CollectionSizeMethod or
|
||||
e.(MethodCall).getMethod() instanceof MapSizeMethod or
|
||||
e.(FieldRead).getField() instanceof ArrayLengthField or
|
||||
positive(e.(AndBitwiseExpr).getAnOperand())
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e` has an upper (for `upper = true`) or lower
|
||||
* (for `upper = false`) bound of `b`.
|
||||
*/
|
||||
private predicate baseBound(Expr e, int b, boolean upper) {
|
||||
lowerBoundZero(e) and b = 0 and upper = false
|
||||
or
|
||||
exists(Method read |
|
||||
e.(MethodCall).getMethod().overrides*(read) and
|
||||
read.getDeclaringType() instanceof TypeInputStream and
|
||||
read.hasName("read") and
|
||||
read.getNumberOfParameters() = 0
|
||||
|
|
||||
upper = true and b = 255
|
||||
or
|
||||
upper = false and b = -1
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the value being cast has an upper (for `upper = true`) or lower
|
||||
* (for `upper = false`) bound within the bounds of the resulting type.
|
||||
* For `upper = true` this means that the cast will not overflow and for
|
||||
* `upper = false` this means that the cast will not underflow.
|
||||
*/
|
||||
private predicate safeNarrowingCast(NarrowingCastingExpr cast, boolean upper) {
|
||||
exists(int bound | bounded(cast.getExpr(), any(ZeroBound zb), bound, upper, _, _, _) |
|
||||
upper = true and bound <= cast.getUpperBound()
|
||||
or
|
||||
upper = false and bound >= cast.getLowerBound()
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate boundedCastExpr(
|
||||
NarrowingCastingExpr cast, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
Reason reason
|
||||
) {
|
||||
bounded(cast.getExpr(), b, delta, upper, fromBackEdge, origdelta, reason)
|
||||
}
|
||||
|
||||
bindingset[f]
|
||||
private predicate okInt(float f) { -2.pow(31) <= f and f <= 2.pow(31) - 1 }
|
||||
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `e`.
|
||||
* - `upper = true` : `e <= b + delta`
|
||||
* - `upper = false` : `e >= b + delta`
|
||||
*/
|
||||
private predicate bounded(
|
||||
Expr e, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, Reason reason
|
||||
) {
|
||||
e = b.getExpr(delta) and
|
||||
(upper = true or upper = false) and
|
||||
fromBackEdge = false and
|
||||
origdelta = delta and
|
||||
reason = TNoReason()
|
||||
or
|
||||
baseBound(e, delta, upper) and
|
||||
b instanceof ZeroBound and
|
||||
fromBackEdge = false and
|
||||
origdelta = delta and
|
||||
reason = TNoReason()
|
||||
or
|
||||
exists(SsaVariable v, SsaReadPositionBlock bb |
|
||||
boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
|
||||
e = v.getAUse() and
|
||||
bb.getBlock() = e.getBasicBlock()
|
||||
)
|
||||
or
|
||||
exists(Expr mid, int d1, int d2 |
|
||||
boundFlowStep(e, mid, d1, upper) and
|
||||
// Constants have easy, base-case bounds, so let's not infer any recursive bounds.
|
||||
not e instanceof ConstantIntegerExpr and
|
||||
bounded(mid, b, d2, upper, fromBackEdge, origdelta, reason) and
|
||||
// upper = true: e <= mid + d1 <= b + d1 + d2 = b + delta
|
||||
// upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
|
||||
delta = d1 + d2 and
|
||||
okInt(d1.(float) + d2.(float))
|
||||
)
|
||||
or
|
||||
exists(SsaPhiNode phi |
|
||||
boundedPhi(phi, b, delta, upper, fromBackEdge, origdelta, reason) and
|
||||
e = phi.getAUse()
|
||||
)
|
||||
or
|
||||
exists(Expr mid, int factor, int d |
|
||||
boundFlowStepMul(e, mid, factor) and
|
||||
not e instanceof ConstantIntegerExpr and
|
||||
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
|
||||
b instanceof ZeroBound and
|
||||
delta = d * factor and
|
||||
okInt(d.(float) * factor.(float))
|
||||
)
|
||||
or
|
||||
exists(Expr mid, int factor, int d |
|
||||
boundFlowStepDiv(e, mid, factor) and
|
||||
not e instanceof ConstantIntegerExpr and
|
||||
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
|
||||
b instanceof ZeroBound and
|
||||
d >= 0 and
|
||||
delta = d / factor
|
||||
)
|
||||
or
|
||||
exists(NarrowingCastingExpr cast |
|
||||
cast = e and
|
||||
safeNarrowingCast(cast, upper.booleanNot()) and
|
||||
boundedCastExpr(cast, b, delta, upper, fromBackEdge, origdelta, reason)
|
||||
)
|
||||
or
|
||||
exists(
|
||||
ConditionalExpr cond, int d1, int d2, boolean fbe1, boolean fbe2, int od1, int od2, Reason r1,
|
||||
Reason r2
|
||||
|
|
||||
cond = e and
|
||||
boundedConditionalExpr(cond, b, upper, true, d1, fbe1, od1, r1) and
|
||||
boundedConditionalExpr(cond, b, upper, false, d2, fbe2, od2, r2) and
|
||||
(
|
||||
delta = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
|
||||
or
|
||||
delta = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
|
||||
)
|
||||
|
|
||||
upper = true and delta = d1.maximum(d2)
|
||||
or
|
||||
upper = false and delta = d1.minimum(d2)
|
||||
)
|
||||
or
|
||||
exists(
|
||||
Bound b1, Bound b2, int d1, int d2, boolean fbe1, boolean fbe2, int od1, int od2, Reason r1,
|
||||
Reason r2
|
||||
|
|
||||
boundedAddition(e, upper, b1, true, d1, fbe1, od1, r1) and
|
||||
boundedAddition(e, upper, b2, false, d2, fbe2, od2, r2) and
|
||||
delta = d1 + d2 and
|
||||
fromBackEdge = fbe1.booleanOr(fbe2) and
|
||||
okInt(d1.(float) + d2.(float))
|
||||
|
|
||||
b = b1 and origdelta = od1 and reason = r1 and b2 instanceof ZeroBound
|
||||
or
|
||||
b = b2 and origdelta = od2 and reason = r2 and b1 instanceof ZeroBound
|
||||
)
|
||||
}
|
||||
|
||||
private predicate boundedConditionalExpr(
|
||||
ConditionalExpr cond, Bound b, boolean upper, boolean branch, int delta, boolean fromBackEdge,
|
||||
int origdelta, Reason reason
|
||||
) {
|
||||
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
|
||||
}
|
||||
|
||||
private predicate nonConstAdd(Expr add, Expr operand, boolean isLeft) {
|
||||
exists(Expr other |
|
||||
add.(AddExpr).getLeftOperand() = operand and
|
||||
add.(AddExpr).getRightOperand() = other and
|
||||
isLeft = true
|
||||
or
|
||||
add.(AddExpr).getLeftOperand() = other and
|
||||
add.(AddExpr).getRightOperand() = operand and
|
||||
isLeft = false
|
||||
or
|
||||
add.(AssignAddExpr).getDest() = operand and
|
||||
add.(AssignAddExpr).getRhs() = other and
|
||||
isLeft = true
|
||||
or
|
||||
add.(AssignAddExpr).getDest() = other and
|
||||
add.(AssignAddExpr).getRhs() = operand and
|
||||
isLeft = false
|
||||
|
|
||||
// `ConstantIntegerExpr` is covered by valueFlowStep
|
||||
not other instanceof ConstantIntegerExpr and
|
||||
not operand instanceof ConstantIntegerExpr
|
||||
)
|
||||
}
|
||||
|
||||
private predicate boundedAddition(
|
||||
Expr add, boolean upper, Bound b, boolean isLeft, int delta, boolean fromBackEdge, int origdelta,
|
||||
Reason reason
|
||||
) {
|
||||
exists(Expr op |
|
||||
nonConstAdd(add, op, isLeft) and
|
||||
bounded(op, b, delta, upper, fromBackEdge, origdelta, reason)
|
||||
)
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user