mirror of
https://github.com/github/codeql.git
synced 2025-12-24 04:36:35 +01:00
Convert RangeAnalysis to trivial parameterized mod
This commit is contained in:
Robert Marsh
@@ -70,262 +70,6 @@ private import ModulusAnalysis
|
||||
private import experimental.semmle.code.cpp.semantic.Semantic
|
||||
private import ConstantAnalysis
|
||||
|
||||
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 semBounded(SemExpr e, SemBound b, int delta, boolean upper, SemReason reason) {
|
||||
bounded(e, b, delta, upper, _, _, reason) and
|
||||
bestBound(e, b, delta, upper)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
|
||||
*/
|
||||
cached
|
||||
predicate possibleReason(SemGuard guard) {
|
||||
guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _)
|
||||
}
|
||||
}
|
||||
|
||||
private import RangeAnalysisCache
|
||||
import RangeAnalysisPublic
|
||||
|
||||
/**
|
||||
* 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(SemExpr e, SemBound 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(
|
||||
SemRelationalExpr comp, SemSsaVariable v, SemExpr e, int delta, boolean upper
|
||||
) {
|
||||
comp.getLesserOperand() = semSsaRead(v, delta) and e = comp.getGreaterOperand() and upper = true
|
||||
or
|
||||
comp.getGreaterOperand() = semSsaRead(v, delta) and e = comp.getLesserOperand() and upper = false
|
||||
or
|
||||
exists(SemSubExpr sub, SemConstantIntegerExpr c, int d |
|
||||
// (v - d) - e < c
|
||||
comp.getLesserOperand() = sub and
|
||||
comp.getGreaterOperand() = c and
|
||||
sub.getLeftOperand() = semSsaRead(v, d) and
|
||||
sub.getRightOperand() = e and
|
||||
upper = true and
|
||||
delta = d + c.getIntValue()
|
||||
or
|
||||
// (v - d) - e > c
|
||||
comp.getGreaterOperand() = sub and
|
||||
comp.getLesserOperand() = c and
|
||||
sub.getLeftOperand() = semSsaRead(v, d) and
|
||||
sub.getRightOperand() = e and
|
||||
upper = false and
|
||||
delta = d + c.getIntValue()
|
||||
or
|
||||
// e - (v - d) < c
|
||||
comp.getLesserOperand() = sub and
|
||||
comp.getGreaterOperand() = c and
|
||||
sub.getLeftOperand() = e and
|
||||
sub.getRightOperand() = semSsaRead(v, d) and
|
||||
upper = false and
|
||||
delta = d - c.getIntValue()
|
||||
or
|
||||
// e - (v - d) > c
|
||||
comp.getGreaterOperand() = sub and
|
||||
comp.getLesserOperand() = c and
|
||||
sub.getLeftOperand() = e and
|
||||
sub.getRightOperand() = semSsaRead(v, d) and
|
||||
upper = true and
|
||||
delta = d - c.getIntValue()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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(SemRelationalExpr comp, boolean testIsTrue, int strengthen) {
|
||||
exists(
|
||||
SemBound 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`.
|
||||
semExprModulus(comp.getLesserOperand(), b, v1, mod1) and
|
||||
semExprModulus(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 SemGuard boundFlowCond(
|
||||
SemSsaVariable v, SemExpr e, int delta, boolean upper, boolean testIsTrue
|
||||
) {
|
||||
exists(
|
||||
SemRelationalExpr comp, int d1, int d2, int d3, int strengthen, boolean compIsUpper,
|
||||
boolean resultIsStrict
|
||||
|
|
||||
comp = result.asExpr() 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
|
||||
getTrackedTypeForSsaVariable(v) instanceof SemIntegerType or
|
||||
getTrackedTypeForSsaVariable(v) instanceof SemAddressType
|
||||
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
|
||||
)
|
||||
or
|
||||
exists(boolean testIsTrue0 |
|
||||
semImplies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0), testIsTrue0)
|
||||
)
|
||||
or
|
||||
result = semEqFlowCond(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(SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, int d1, int d2 |
|
||||
guardEq = semEqFlowCond(v, semSsaRead(v2, d1), d2, true, eqIsTrue) and
|
||||
result = boundFlowCond(v2, e, delta + d1 - d2, upper, testIsTrue) and
|
||||
// guardEq needs to control guard
|
||||
guardEq.directlyControls(result.getBasicBlock(), eqIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
private newtype TSemReason =
|
||||
TSemNoReason() or
|
||||
TSemCondReason(SemGuard 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 SemReason extends TSemReason {
|
||||
/** 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 SemNoReason extends SemReason, TSemNoReason {
|
||||
override string toString() { result = "NoReason" }
|
||||
}
|
||||
|
||||
/** A reason for an inferred bound pointing to a condition. */
|
||||
class SemCondReason extends SemReason, TSemCondReason {
|
||||
/** Gets the condition that is the reason for the bound. */
|
||||
SemGuard getCond() { this = TSemCondReason(result) }
|
||||
|
||||
override string toString() { result = 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(
|
||||
SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta, boolean upper, SemReason reason
|
||||
) {
|
||||
semSsaUpdateStep(v, e, delta) and
|
||||
pos.hasReadOfVar(v) and
|
||||
(upper = true or upper = false) and
|
||||
reason = TSemNoReason()
|
||||
or
|
||||
exists(SemGuard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
|
||||
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TSemCondReason(guard)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
|
||||
private predicate unequalFlowStepIntegralSsa(
|
||||
SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta, SemReason reason
|
||||
) {
|
||||
getTrackedTypeForSsaVariable(v) instanceof SemIntegerType and
|
||||
exists(SemGuard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
|
||||
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TSemCondReason(guard)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* An expression that does conversion, boxing, or unboxing
|
||||
@@ -385,22 +129,284 @@ private class NarrowingCastExpr extends ConvertOrBoxExpr {
|
||||
int getUpperBound() { typeBound(getTrackedType(this), _, result) }
|
||||
}
|
||||
|
||||
/** Holds if `e >= 1` as determined by sign analysis. */
|
||||
private predicate strictlyPositiveIntegralExpr(SemExpr e) {
|
||||
signature module RangeSig { }
|
||||
|
||||
module RangeStage<RangeSig RangeParam> {
|
||||
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 semBounded(SemExpr e, SemBound b, int delta, boolean upper, SemReason reason) {
|
||||
bounded(e, b, delta, upper, _, _, reason) and
|
||||
bestBound(e, b, delta, upper)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
|
||||
*/
|
||||
cached
|
||||
predicate possibleReason(SemGuard guard) {
|
||||
guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _)
|
||||
}
|
||||
}
|
||||
|
||||
private import RangeAnalysisCache
|
||||
import RangeAnalysisPublic
|
||||
|
||||
/**
|
||||
* 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(SemExpr e, SemBound 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(
|
||||
SemRelationalExpr comp, SemSsaVariable v, SemExpr e, int delta, boolean upper
|
||||
) {
|
||||
comp.getLesserOperand() = semSsaRead(v, delta) and e = comp.getGreaterOperand() and upper = true
|
||||
or
|
||||
comp.getGreaterOperand() = semSsaRead(v, delta) and
|
||||
e = comp.getLesserOperand() and
|
||||
upper = false
|
||||
or
|
||||
exists(SemSubExpr sub, SemConstantIntegerExpr c, int d |
|
||||
// (v - d) - e < c
|
||||
comp.getLesserOperand() = sub and
|
||||
comp.getGreaterOperand() = c and
|
||||
sub.getLeftOperand() = semSsaRead(v, d) and
|
||||
sub.getRightOperand() = e and
|
||||
upper = true and
|
||||
delta = d + c.getIntValue()
|
||||
or
|
||||
// (v - d) - e > c
|
||||
comp.getGreaterOperand() = sub and
|
||||
comp.getLesserOperand() = c and
|
||||
sub.getLeftOperand() = semSsaRead(v, d) and
|
||||
sub.getRightOperand() = e and
|
||||
upper = false and
|
||||
delta = d + c.getIntValue()
|
||||
or
|
||||
// e - (v - d) < c
|
||||
comp.getLesserOperand() = sub and
|
||||
comp.getGreaterOperand() = c and
|
||||
sub.getLeftOperand() = e and
|
||||
sub.getRightOperand() = semSsaRead(v, d) and
|
||||
upper = false and
|
||||
delta = d - c.getIntValue()
|
||||
or
|
||||
// e - (v - d) > c
|
||||
comp.getGreaterOperand() = sub and
|
||||
comp.getLesserOperand() = c and
|
||||
sub.getLeftOperand() = e and
|
||||
sub.getRightOperand() = semSsaRead(v, d) and
|
||||
upper = true and
|
||||
delta = d - c.getIntValue()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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(SemRelationalExpr comp, boolean testIsTrue, int strengthen) {
|
||||
exists(
|
||||
SemBound 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`.
|
||||
semExprModulus(comp.getLesserOperand(), b, v1, mod1) and
|
||||
semExprModulus(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 SemGuard boundFlowCond(
|
||||
SemSsaVariable v, SemExpr e, int delta, boolean upper, boolean testIsTrue
|
||||
) {
|
||||
exists(
|
||||
SemRelationalExpr comp, int d1, int d2, int d3, int strengthen, boolean compIsUpper,
|
||||
boolean resultIsStrict
|
||||
|
|
||||
comp = result.asExpr() 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
|
||||
getTrackedTypeForSsaVariable(v) instanceof SemIntegerType or
|
||||
getTrackedTypeForSsaVariable(v) instanceof SemAddressType
|
||||
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
|
||||
)
|
||||
or
|
||||
exists(boolean testIsTrue0 |
|
||||
semImplies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0), testIsTrue0)
|
||||
)
|
||||
or
|
||||
result = semEqFlowCond(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(SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, int d1, int d2 |
|
||||
guardEq = semEqFlowCond(v, semSsaRead(v2, d1), d2, true, eqIsTrue) and
|
||||
result = boundFlowCond(v2, e, delta + d1 - d2, upper, testIsTrue) and
|
||||
// guardEq needs to control guard
|
||||
guardEq.directlyControls(result.getBasicBlock(), eqIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
private newtype TSemReason =
|
||||
TSemNoReason() or
|
||||
TSemCondReason(SemGuard 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 SemReason extends TSemReason {
|
||||
/** 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 SemNoReason extends SemReason, TSemNoReason {
|
||||
override string toString() { result = "NoReason" }
|
||||
}
|
||||
|
||||
/** A reason for an inferred bound pointing to a condition. */
|
||||
class SemCondReason extends SemReason, TSemCondReason {
|
||||
/** Gets the condition that is the reason for the bound. */
|
||||
SemGuard getCond() { this = TSemCondReason(result) }
|
||||
|
||||
override string toString() { result = 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(
|
||||
SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta, boolean upper, SemReason reason
|
||||
) {
|
||||
semSsaUpdateStep(v, e, delta) and
|
||||
pos.hasReadOfVar(v) and
|
||||
(upper = true or upper = false) and
|
||||
reason = TSemNoReason()
|
||||
or
|
||||
exists(SemGuard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
|
||||
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TSemCondReason(guard)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `v != e + delta` at `pos` and `v` is of integral type. */
|
||||
private predicate unequalFlowStepIntegralSsa(
|
||||
SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta, SemReason reason
|
||||
) {
|
||||
getTrackedTypeForSsaVariable(v) instanceof SemIntegerType and
|
||||
exists(SemGuard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
|
||||
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TSemCondReason(guard)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `e >= 1` as determined by sign analysis. */
|
||||
private predicate strictlyPositiveIntegralExpr(SemExpr e) {
|
||||
semStrictlyPositive(e) and getTrackedType(e) instanceof SemIntegerType
|
||||
}
|
||||
}
|
||||
|
||||
/** Holds if `e <= -1` as determined by sign analysis. */
|
||||
private predicate strictlyNegativeIntegralExpr(SemExpr e) {
|
||||
/** Holds if `e <= -1` as determined by sign analysis. */
|
||||
private predicate strictlyNegativeIntegralExpr(SemExpr e) {
|
||||
semStrictlyNegative(e) and getTrackedType(e) instanceof SemIntegerType
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `e1 + delta` is a valid bound for `e2`.
|
||||
* - `upper = true` : `e2 <= e1 + delta`
|
||||
* - `upper = false` : `e2 >= e1 + delta`
|
||||
*/
|
||||
private predicate boundFlowStep(SemExpr e2, SemExpr e1, int delta, boolean upper) {
|
||||
private predicate boundFlowStep(SemExpr e2, SemExpr e1, int delta, boolean upper) {
|
||||
semValueFlowStep(e2, e1, delta) and
|
||||
(upper = true or upper = false)
|
||||
or
|
||||
@@ -465,10 +471,10 @@ private predicate boundFlowStep(SemExpr e2, SemExpr e1, int delta, boolean upper
|
||||
upper = false
|
||||
or
|
||||
Specific::hasBound(e2, e1, delta, upper)
|
||||
}
|
||||
}
|
||||
|
||||
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
|
||||
private predicate boundFlowStepMul(SemExpr e2, SemExpr e1, int factor) {
|
||||
/** Holds if `e2 = e1 * factor` and `factor > 0`. */
|
||||
private predicate boundFlowStepMul(SemExpr e2, SemExpr e1, int factor) {
|
||||
exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
|
||||
e2.(SemMulExpr).hasOperands(e1, c) and factor = k
|
||||
or
|
||||
@@ -476,15 +482,15 @@ private predicate boundFlowStepMul(SemExpr e2, SemExpr e1, int factor) {
|
||||
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = 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(SemExpr e2, SemExpr e1, int factor) {
|
||||
private predicate boundFlowStepDiv(SemExpr e2, SemExpr e1, int factor) {
|
||||
exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() and k > 0 |
|
||||
exists(SemDivExpr e |
|
||||
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = k
|
||||
@@ -498,17 +504,17 @@ private predicate boundFlowStepDiv(SemExpr e2, SemExpr e1, int factor) {
|
||||
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = 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(
|
||||
private predicate boundedSsa(
|
||||
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, int delta, boolean upper,
|
||||
boolean fromBackEdge, int origdelta, SemReason reason
|
||||
) {
|
||||
) {
|
||||
exists(SemExpr mid, int d1, int d2, SemReason r1, SemReason r2 |
|
||||
boundFlowStepSsa(v, pos, mid, d1, upper, r1) and
|
||||
bounded(mid, b, d2, upper, fromBackEdge, origdelta, r2) and
|
||||
@@ -534,62 +540,62 @@ private predicate boundedSsa(
|
||||
reason = r2 and not r2 instanceof SemNoReason
|
||||
)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `v != b + delta` at `pos` and `v` is of integral type.
|
||||
*/
|
||||
private predicate unequalIntegralSsa(
|
||||
private predicate unequalIntegralSsa(
|
||||
SemSsaVariable v, SemSsaReadPosition pos, SemBound b, int delta, SemReason reason
|
||||
) {
|
||||
) {
|
||||
exists(SemExpr e, int d1, int d2 |
|
||||
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
|
||||
boundedUpper(e, b, d1) and
|
||||
boundedLower(e, b, d2) and
|
||||
delta = d2 + d1
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `b + delta` is an upper bound for `e`.
|
||||
*
|
||||
* This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate boundedUpper(SemExpr e, SemBound b, int delta) {
|
||||
pragma[nomagic]
|
||||
private predicate boundedUpper(SemExpr e, SemBound b, int delta) {
|
||||
bounded(e, b, delta, true, _, _, _)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `b + delta` is a lower bound for `e`.
|
||||
*
|
||||
* This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate boundedLower(SemExpr e, SemBound b, int delta) {
|
||||
pragma[nomagic]
|
||||
private predicate boundedLower(SemExpr e, SemBound b, int delta) {
|
||||
bounded(e, b, delta, false, _, _, _)
|
||||
}
|
||||
}
|
||||
|
||||
/** Weakens a delta to lie in the range `[-1..1]`. */
|
||||
bindingset[delta, upper]
|
||||
private int weakenDelta(boolean upper, int delta) {
|
||||
/** 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(
|
||||
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, SemBound b, int delta,
|
||||
boolean upper, boolean fromBackEdge, int origdelta, SemReason reason
|
||||
) {
|
||||
private predicate boundedPhiInp(
|
||||
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, SemBound b,
|
||||
int delta, boolean upper, boolean fromBackEdge, int origdelta, SemReason reason
|
||||
) {
|
||||
edge.phiInput(phi, inp) and
|
||||
exists(int d, boolean fromBackEdge0 |
|
||||
boundedSsa(inp, edge, b, d, upper, fromBackEdge0, origdelta, reason)
|
||||
@@ -615,9 +621,9 @@ private predicate boundedPhiInp(
|
||||
delta = d and fromBackEdge = fromBackEdge0
|
||||
)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `inp` when used as an input to
|
||||
* `phi` along `edge`.
|
||||
* - `upper = true` : `inp <= b + delta`
|
||||
@@ -625,23 +631,23 @@ private predicate boundedPhiInp(
|
||||
*
|
||||
* Equivalent to `boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate boundedPhiInp1(
|
||||
pragma[noinline]
|
||||
private predicate boundedPhiInp1(
|
||||
SemSsaPhiNode phi, SemBound b, boolean upper, SemSsaVariable inp,
|
||||
SemSsaReadPositionPhiInputEdge 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(
|
||||
private predicate selfBoundedPhiInp(
|
||||
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, boolean upper
|
||||
) {
|
||||
) {
|
||||
exists(int d, SemSsaBound phibound |
|
||||
phibound.getAVariable() = phi and
|
||||
boundedPhiInp(phi, inp, edge, phibound, d, upper, _, _, _) and
|
||||
@@ -651,32 +657,32 @@ private predicate selfBoundedPhiInp(
|
||||
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(
|
||||
pragma[noinline]
|
||||
private predicate boundedPhiCand(
|
||||
SemSsaPhiNode phi, boolean upper, SemBound b, int delta, boolean fromBackEdge, int origdelta,
|
||||
SemReason reason
|
||||
) {
|
||||
) {
|
||||
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
|
||||
boundedPhiInp(phi, inp, edge, 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(
|
||||
private predicate boundedPhiCandValidForEdge(
|
||||
SemSsaPhiNode phi, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
SemReason reason, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge 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)
|
||||
@@ -685,27 +691,27 @@ private predicate boundedPhiCandValidForEdge(
|
||||
or
|
||||
selfBoundedPhiInp(phi, inp, edge, upper)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `phi`.
|
||||
* - `upper = true` : `phi <= b + delta`
|
||||
* - `upper = false` : `phi >= b + delta`
|
||||
*/
|
||||
private predicate boundedPhi(
|
||||
private predicate boundedPhi(
|
||||
SemSsaPhiNode phi, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
SemReason reason
|
||||
) {
|
||||
) {
|
||||
forex(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
|
||||
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `e` has an upper (for `upper = true`) or lower
|
||||
* (for `upper = false`) bound of `b`.
|
||||
*/
|
||||
private predicate baseBound(SemExpr e, int b, boolean upper) {
|
||||
private predicate baseBound(SemExpr e, int b, boolean upper) {
|
||||
Specific::hasConstantBound(e, b, upper)
|
||||
or
|
||||
upper = false and
|
||||
@@ -713,39 +719,39 @@ private predicate baseBound(SemExpr e, int b, boolean upper) {
|
||||
semPositive(e.(SemBitAndExpr).getAnOperand()) and
|
||||
// REVIEW: We let the language opt out here to preserve original results.
|
||||
not Specific::ignoreZeroLowerBound(e)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* 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(NarrowingCastExpr cast, boolean upper) {
|
||||
private predicate safeNarrowingCast(NarrowingCastExpr cast, boolean upper) {
|
||||
exists(int bound | bounded(cast.getOperand(), any(SemZeroBound zb), bound, upper, _, _, _) |
|
||||
upper = true and bound <= cast.getUpperBound()
|
||||
or
|
||||
upper = false and bound >= cast.getLowerBound()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate boundedCastExpr(
|
||||
NarrowingCastExpr cast, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
SemReason reason
|
||||
) {
|
||||
pragma[noinline]
|
||||
private predicate boundedCastExpr(
|
||||
NarrowingCastExpr cast, SemBound b, int delta, boolean upper, boolean fromBackEdge,
|
||||
int origdelta, SemReason reason
|
||||
) {
|
||||
bounded(cast.getOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
/**
|
||||
* Holds if `b + delta` is a valid bound for `e`.
|
||||
* - `upper = true` : `e <= b + delta`
|
||||
* - `upper = false` : `e >= b + delta`
|
||||
*/
|
||||
private predicate bounded(
|
||||
private predicate bounded(
|
||||
SemExpr e, SemBound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
|
||||
SemReason reason
|
||||
) {
|
||||
) {
|
||||
not Specific::ignoreExprBound(e) and
|
||||
(
|
||||
e = b.getExpr(delta) and
|
||||
@@ -822,11 +828,12 @@ private predicate bounded(
|
||||
upper = false and delta = d1.minimum(d2)
|
||||
)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private predicate boundedConditionalExpr(
|
||||
private predicate boundedConditionalExpr(
|
||||
SemConditionalExpr cond, SemBound b, boolean upper, boolean branch, int delta,
|
||||
boolean fromBackEdge, int origdelta, SemReason reason
|
||||
) {
|
||||
) {
|
||||
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user