Merge master into next.

`master` up to and including cfe0b8803a.
This commit is contained in:
Aditya Sharad
2018-10-25 15:32:47 +01:00
122 changed files with 4155 additions and 1297 deletions

View File

@@ -167,6 +167,15 @@ predicate overFlowTest(ComparisonExpr comp) {
comp.getGreaterOperand().(IntegerLiteral).getIntValue() = 0
}
predicate concurrentModificationTest(BinaryExpr test) {
exists(IfStmt ifstmt, ThrowStmt throw, RefType exc |
ifstmt.getCondition() = test and
(ifstmt.getThen() = throw or ifstmt.getThen().(SingletonBlock).getStmt() = throw) and
throw.getExpr().(ClassInstanceExpr).getConstructedType() = exc and
exc.hasQualifiedName("java.util", "ConcurrentModificationException")
)
}
/**
* Holds if `test` and `guard` are equality tests of the same integral variable v with constants `c1` and `c2`.
*/
@@ -202,13 +211,13 @@ where
)
else
if constCondSimple(test, _)
then (
constCondSimple(test, testIsTrue) and reason = "" and reasonElem = test // dummy reason element
) else
then constCondSimple(test, testIsTrue) and reason = "" and reasonElem = test // dummy reason element
else
exists(CondReason r |
constCond(test, testIsTrue, r) and reason = ", because of $@" and reasonElem = r.getCond()
)
) and
not overFlowTest(test) and
not concurrentModificationTest(test) and
not exists(AssertStmt assert | assert.getExpr() = test.getParent*())
select test, "Test is always " + testIsTrue + reason + ".", reasonElem, "this condition"

View File

@@ -9,6 +9,7 @@
import java
import semmle.code.java.dataflow.Guards
import semmle.code.java.dataflow.ParityAnalysis
import semmle.code.java.security.DataFlow
from File f, string tag

View File

@@ -0,0 +1,68 @@
import java
private import SSA
private import RangeUtils
private newtype TBound =
TBoundZero() or
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
TBoundExpr(Expr e) {
e.(FieldRead).getField() instanceof ArrayLengthField and
not exists(SsaVariable v | e = v.getAUse())
}
/**
* A bound that may be inferred for an expression plus/minus an integer delta.
*/
abstract class Bound extends TBound {
abstract string toString();
/** Gets an expression that equals this bound plus `delta`. */
abstract Expr getExpr(int delta);
/** Gets an expression that equals this bound. */
Expr getExpr() { result = getExpr(0) }
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
}
}
/**
* The bound that corresponds to the integer 0. This is used to represent all
* integer bounds as bounds are always accompanied by an added integer delta.
*/
class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
}
/**
* A bound corresponding to the value of an SSA variable.
*/
class SsaBound extends Bound, TBoundSsa {
/** Gets the SSA variable that equals this bound. */
SsaVariable getSsa() { this = TBoundSsa(result) }
override string toString() { result = getSsa().toString() }
override Expr getExpr(int delta) { result = getSsa().getAUse() and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
}
/**
* A bound that corresponds to the value of a specific expression that might be
* interesting, but isn't otherwise represented by the value of an SSA variable.
*/
class ExprBound extends Bound, TBoundExpr {
override string toString() { result = getExpr().toString() }
override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
getExpr().hasLocationInfo(path, sl, sc, el, ec)
}
}

View File

@@ -0,0 +1,352 @@
/**
* Provides inferences of the form: `e` equals `b + v` modulo `m` where `e` is
* an expression, `b` is a `Bound` (typically zero or the value of an SSA
* variable), and `v` is an integer in the range `[0 .. m-1]`.
*/
import java
private import SSA
private import RangeUtils
private import semmle.code.java.controlflow.Guards
import Bound
/**
* Holds if `e + delta` equals `v` at `pos`.
*/
private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, int delta) {
ssaUpdateStep(v, e, delta) and pos.hasReadOfVar(v)
or
exists(Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = eqFlowCond(v, e, delta, true, testIsTrue) and
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
)
}
/**
* Holds if `add` is the addition of `larg` and `rarg`, neither of which are
* `ConstantIntegerExpr`s.
*/
private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
(
exists(AddExpr a | a = add |
larg = a.getLeftOperand() and
rarg = a.getRightOperand()
)
or
exists(AssignAddExpr a | a = add |
larg = a.getDest() and
rarg = a.getRhs()
)
) and
not larg instanceof ConstantIntegerExpr and
not rarg instanceof ConstantIntegerExpr
}
/**
* Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
* a `ConstantIntegerExpr`.
*/
private predicate nonConstSubtraction(Expr sub, Expr larg, Expr rarg) {
(
exists(SubExpr s | s = sub |
larg = s.getLeftOperand() and
rarg = s.getRightOperand()
)
or
exists(AssignSubExpr s | s = sub |
larg = s.getDest() and
rarg = s.getRhs()
)
) and
not rarg instanceof ConstantIntegerExpr
}
/** Gets an expression that is the remainder modulo `mod` of `arg`. */
private Expr modExpr(Expr arg, int mod) {
exists(RemExpr rem |
result = rem and
arg = rem.getLeftOperand() and
rem.getRightOperand().(CompileTimeConstantExpr).getIntValue() = mod and
mod >= 2
)
or
exists(CompileTimeConstantExpr c |
mod = 2.pow([1 .. 30]) and
c.getIntValue() = mod - 1 and
result.(AndBitwiseExpr).hasOperands(arg, c)
)
or
result.(ParExpr).getExpr() = modExpr(arg, mod)
}
/**
* Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
* its `testIsTrue` branch.
*/
private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
exists(Expr rem, CompileTimeConstantExpr c, int r, boolean polarity |
result.isEquality(rem, c, polarity) and
c.getIntValue() = r and
rem = modExpr(v.getAUse(), mod) and
(
testIsTrue = polarity and val = r
or
testIsTrue = polarity.booleanNot() and
mod = 2 and
val = 1 - r and
(r = 0 or r = 1)
)
)
}
/**
* Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
*/
private predicate moduloGuardedRead(SsaVariable v, SsaReadPosition pos, int val, int mod) {
exists(Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = moduloCheck(v, val, mod, testIsTrue) and
guardControlsSsaRead(guard, pos, testIsTrue)
)
}
/** Holds if `factor` is a power of 2 that divides `mask`. */
bindingset[mask]
private predicate andmaskFactor(int mask, int factor) {
mask % factor = 0 and
factor = 2.pow([1 .. 30])
}
/** Holds if `e` is evenly divisible by `factor`. */
private predicate evenlyDivisibleExpr(Expr e, int factor) {
exists(ConstantIntegerExpr c, int k | k = c.getIntValue() |
e.(MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
or
e.(AssignMulExpr).getSource() = c and factor = k.abs() and factor >= 2
or
e.(LShiftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
or
e.(AssignLShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
or
e.(AndBitwiseExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
or
e.(AssignAndExpr).getSource() = c and factor = max(int f | andmaskFactor(k, f))
)
}
private predicate id(BasicBlock x, BasicBlock y) { x = y }
private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
private int getId(BasicBlock bb) { idOf(bb, result) }
/**
* 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`.
*/
private 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
getId(e.getOrigBlock())
)
}
/**
* Holds if `rix` is the number of input edges to `phi`.
*/
private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}
private int gcdLim() { result = 128 }
/**
* Gets the greatest common divisor of `x` and `y`. This is restricted to small
* inputs and the case when `x` and `y` are not relatively prime.
*/
private int gcd(int x, int y) {
result != 1 and
result = x.abs() and
y = 0 and
x in [-gcdLim() .. gcdLim()]
or
result = gcd(y, x % y) and y != 0 and x in [-gcdLim() .. gcdLim()]
}
/**
* Gets the remainder of `val` modulo `mod`.
*
* For `mod = 0` the result equals `val` and for `mod > 1` the result is within
* the range `[0 .. mod-1]`.
*/
bindingset[val, mod]
private int remainder(int val, int mod) {
mod = 0 and result = val
or
mod > 1 and result = ((val % mod) + mod) % mod
}
/**
* Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
*/
private predicate phiSelfModulus(
SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int mod
) {
exists(SsaBound phibound, int v, int m |
edge.phiInput(phi, inp) and
phibound.getSsa() = phi and
ssaModulus(inp, edge, phibound, v, m) and
mod = gcd(m, v) and
mod != 1
)
}
/**
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
*/
private predicate phiModulusInit(SsaPhiNode phi, Bound b, int val, int mod) {
exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge |
edge.phiInput(phi, inp) and
ssaModulus(inp, edge, b, val, mod)
)
}
/**
* Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
*/
private predicate phiModulusRankStep(SsaPhiNode phi, Bound b, int val, int mod, int rix) {
rix = 0 and
phiModulusInit(phi, b, val, mod)
or
exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge, int v1, int m1 |
mod != 1 and
val = remainder(v1, mod)
|
exists(int v2, int m2 |
rankedPhiInput(phi, inp, edge, rix) and
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
ssaModulus(inp, edge, b, v2, m2) and
mod = gcd(gcd(m1, m2), v1 - v2)
)
or
exists(int m2 |
rankedPhiInput(phi, inp, edge, rix) and
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
phiSelfModulus(phi, inp, edge, m2) and
mod = gcd(m1, m2)
)
)
}
/**
* Holds if `phi` is equal to `b + val` modulo `mod`.
*/
private predicate phiModulus(SsaPhiNode phi, Bound b, int val, int mod) {
exists(int r |
maxPhiInputRank(phi, r) and
phiModulusRankStep(phi, b, val, mod, r)
)
}
/**
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
*/
private predicate ssaModulus(SsaVariable v, SsaReadPosition pos, Bound b, int val, int mod) {
phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
or
b.(SsaBound).getSsa() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
or
exists(Expr e, int val0, int delta |
exprModulus(e, b, val0, mod) and
valueFlowStepSsa(v, pos, e, delta) and
val = remainder(val0 + delta, mod)
)
or
moduloGuardedRead(v, pos, val, mod) and b instanceof ZeroBound
}
/**
* Holds if `e` is equal to `b + val` modulo `mod`.
*
* There are two cases for the modulus:
* - `mod = 0`: The equality `e = b + val` is an ordinary equality.
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
*/
cached
predicate exprModulus(Expr e, Bound b, int val, int mod) {
e = b.getExpr(val) and mod = 0
or
evenlyDivisibleExpr(e, mod) and val = 0 and b instanceof ZeroBound
or
exists(SsaVariable v, SsaReadPositionBlock bb |
ssaModulus(v, bb, b, val, mod) and
e = v.getAUse() and
bb.getBlock() = e.getBasicBlock()
)
or
exists(Expr mid, int val0, int delta |
exprModulus(mid, b, val0, mod) and
valueFlowStep(e, mid, delta) and
val = remainder(val0 + delta, mod)
)
or
exists(ConditionalExpr cond, int v1, int v2, int m1, int m2 |
cond = e and
condExprBranchModulus(cond, true, b, v1, m1) and
condExprBranchModulus(cond, false, b, v2, m2) and
mod = gcd(gcd(m1, m2), v1 - v2) and
mod != 1 and
val = remainder(v1, mod)
)
or
exists(Bound b1, Bound b2, int v1, int v2, int m1, int m2 |
addModulus(e, true, b1, v1, m1) and
addModulus(e, false, b2, v2, m2) and
mod = gcd(m1, m2) and
mod != 1 and
val = remainder(v1 + v2, mod)
|
b = b1 and b2 instanceof ZeroBound
or
b = b2 and b1 instanceof ZeroBound
)
or
exists(int v1, int v2, int m1, int m2 |
subModulus(e, true, b, v1, m1) and
subModulus(e, false, any(ZeroBound zb), v2, m2) and
mod = gcd(m1, m2) and
mod != 1 and
val = remainder(v1 - v2, mod)
)
}
private predicate condExprBranchModulus(
ConditionalExpr cond, boolean branch, Bound b, int val, int mod
) {
exprModulus(cond.getTrueExpr(), b, val, mod) and branch = true
or
exprModulus(cond.getFalseExpr(), b, val, mod) and branch = false
}
private predicate addModulus(Expr add, boolean isLeft, Bound b, int val, int mod) {
exists(Expr larg, Expr rarg | nonConstAddition(add, larg, rarg) |
exprModulus(larg, b, val, mod) and isLeft = true
or
exprModulus(rarg, b, val, mod) and isLeft = false
)
}
private predicate subModulus(Expr sub, boolean isLeft, Bound b, int val, int mod) {
exists(Expr larg, Expr rarg | nonConstSubtraction(sub, larg, rarg) |
exprModulus(larg, b, val, mod) and isLeft = true
or
exprModulus(rarg, b, val, mod) and isLeft = false
)
}

View File

@@ -1,9 +1,12 @@
/**
* DEPRECATED: Use semmle.code.java.dataflow.ModulusAnalysis instead.
*
* Parity Analysis.
*
* The analysis is implemented as an abstract interpretation over the
* two-valued domain `{even, odd}`.
*/
import java
private import SSA
private import RangeUtils
@@ -12,35 +15,35 @@ private import SignAnalysis
private import semmle.code.java.Reflection
/** Gets an expression that is the remainder modulo 2 of `arg`. */
private Expr mod2(Expr arg) {
deprecated private Expr mod2(Expr arg) {
exists(RemExpr rem |
result = rem and
arg = rem.getLeftOperand() and
rem.getRightOperand().(CompileTimeConstantExpr).getIntValue() = 2
) or
result.(AndBitwiseExpr).hasOperands(arg, any(CompileTimeConstantExpr c | c.getIntValue() = 1)) or
)
or
result.(AndBitwiseExpr).hasOperands(arg, any(CompileTimeConstantExpr c | c.getIntValue() = 1))
or
result.(ParExpr).getExpr() = mod2(arg)
}
/** An expression that calculates remainder modulo 2. */
private class Mod2 extends Expr {
Mod2() {
this = mod2(_)
}
deprecated private class Mod2 extends Expr {
Mod2() { this = mod2(_) }
/** Gets the argument of this remainder operation. */
Expr getArg() {
this = mod2(result)
}
Expr getArg() { this = mod2(result) }
}
/**
* Parity represented as booleans. Even corresponds to `false` and odd
* corresponds to `true`.
*/
class Parity extends boolean {
deprecated class Parity extends boolean {
Parity() { this = true or this = false }
predicate isEven() { this = false }
predicate isOdd() { this = true }
}
@@ -48,7 +51,7 @@ class Parity extends boolean {
* Gets a condition that performs a parity check on `v`, such that `v` has
* the given parity if the condition evaluates to `testIsTrue`.
*/
private Guard parityCheck(SsaVariable v, Parity parity, boolean testIsTrue) {
deprecated private Guard parityCheck(SsaVariable v, Parity parity, boolean testIsTrue) {
exists(Mod2 rem, CompileTimeConstantExpr c, int r, boolean polarity |
result.isEquality(rem, c, polarity) and
c.getIntValue() = r and
@@ -56,7 +59,8 @@ private Guard parityCheck(SsaVariable v, Parity parity, boolean testIsTrue) {
rem.getArg() = v.getAUse() and
(testIsTrue = true or testIsTrue = false) and
(
r = 0 and parity = testIsTrue.booleanXor(polarity) or
r = 0 and parity = testIsTrue.booleanXor(polarity)
or
r = 1 and parity = testIsTrue.booleanXor(polarity).booleanNot()
)
)
@@ -65,25 +69,36 @@ private Guard parityCheck(SsaVariable v, Parity parity, boolean testIsTrue) {
/**
* Gets the parity of `e` if it can be directly determined.
*/
private Parity certainExprParity(Expr e) {
deprecated private Parity certainExprParity(Expr e) {
exists(int i | e.(ConstantIntegerExpr).getIntValue() = i |
if i % 2 = 0 then result.isEven() else result.isOdd()
) or
e.(LongLiteral).getValue().regexpMatch(".*[02468]") and result.isEven() or
e.(LongLiteral).getValue().regexpMatch(".*[13579]") and result.isOdd() or
)
or
e.(LongLiteral).getValue().regexpMatch(".*[02468]") and result.isEven()
or
e.(LongLiteral).getValue().regexpMatch(".*[13579]") and result.isOdd()
or
not exists(e.(ConstantIntegerExpr).getIntValue()) and
(
result = certainExprParity(e.(ParExpr).getExpr()) or
result = certainExprParity(e.(ParExpr).getExpr())
or
exists(Guard guard, SsaVariable v, boolean testIsTrue |
guard = parityCheck(v, result, testIsTrue) and
e = v.getAUse() and
guardControls_v2(guard, e.getBasicBlock(), testIsTrue)
) or
)
or
exists(SsaVariable arr, int arrlen, FieldAccess len |
e = len and
len.getField() instanceof ArrayLengthField and
len.getQualifier() = arr.getAUse() and
arr.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getFirstDimensionSize() = arrlen and
arr
.(SsaExplicitUpdate)
.getDefiningExpr()
.(VariableAssign)
.getSource()
.(ArrayCreationExpr)
.getFirstDimensionSize() = arrlen and
if arrlen % 2 = 0 then result.isEven() else result.isOdd()
)
)
@@ -92,114 +107,211 @@ private Parity certainExprParity(Expr e) {
/**
* Gets the expression that defines the array length that equals `len`, if any.
*/
private Expr arrLenDef(FieldAccess len) {
deprecated private Expr arrLenDef(FieldAccess len) {
exists(SsaVariable arr |
len.getField() instanceof ArrayLengthField and
len.getQualifier() = arr.getAUse() and
arr.(SsaExplicitUpdate).getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getDimension(0) = result
arr
.(SsaExplicitUpdate)
.getDefiningExpr()
.(VariableAssign)
.getSource()
.(ArrayCreationExpr)
.getDimension(0) = result
)
}
/** Gets a possible parity for `v`. */
private Parity ssaParity(SsaVariable v) {
deprecated private Parity ssaParity(SsaVariable v) {
exists(VariableUpdate def | def = v.(SsaExplicitUpdate).getDefiningExpr() |
result = exprParity(def.(VariableAssign).getSource()) or
exists(EnhancedForStmt for | def = for.getVariable()) and (result = true or result = false) or
result = exprParity(def.(UnaryAssignExpr).getExpr()).booleanNot() or
result = exprParity(def.(VariableAssign).getSource())
or
exists(EnhancedForStmt for | def = for.getVariable()) and
(result = true or result = false)
or
result = exprParity(def.(UnaryAssignExpr).getExpr()).booleanNot()
or
exists(AssignOp a | a = def and result = exprParity(a))
) or
result = fieldParity(v.(SsaImplicitUpdate).getSourceVariable().getVariable()) or
result = fieldParity(v.(SsaImplicitInit).getSourceVariable().getVariable()) or
exists(Parameter p | v.(SsaImplicitInit).isParameterDefinition(p) and (result = true or result = false)) or
)
or
result = fieldParity(v.(SsaImplicitUpdate).getSourceVariable().getVariable())
or
result = fieldParity(v.(SsaImplicitInit).getSourceVariable().getVariable())
or
exists(Parameter p |
v.(SsaImplicitInit).isParameterDefinition(p) and
(result = true or result = false)
)
or
result = ssaParity(v.(SsaPhiNode).getAPhiInput())
}
/** Gets a possible parity for `f`. */
private Parity fieldParity(Field f) {
result = exprParity(f.getAnAssignedValue()) or
exists(UnaryAssignExpr u | u.getExpr() = f.getAnAccess() and (result = true or result = false)) or
exists(AssignOp a | a.getDest() = f.getAnAccess() | result = exprParity(a)) or
exists(ReflectiveFieldAccess rfa | rfa.inferAccessedField() = f and (result = true or result = false))
deprecated private Parity fieldParity(Field f) {
result = exprParity(f.getAnAssignedValue())
or
if f.fromSource() then
not exists(f.getInitializer()) and result.isEven()
else
exists(UnaryAssignExpr u |
u.getExpr() = f.getAnAccess() and
(result = true or result = false)
)
or
exists(AssignOp a | a.getDest() = f.getAnAccess() | result = exprParity(a))
or
exists(ReflectiveFieldAccess rfa |
rfa.inferAccessedField() = f and
(result = true or result = false)
)
or
if f.fromSource()
then not exists(f.getInitializer()) and result.isEven()
else (
result = true or result = false
)
}
/** Holds if the parity of `e` is too complicated to determine. */
private predicate unknownParity(Expr e) {
e instanceof AssignDivExpr or
e instanceof AssignRShiftExpr or
e instanceof AssignURShiftExpr or
e instanceof DivExpr or
e instanceof RShiftExpr or
e instanceof URShiftExpr or
exists(Type fromtyp | e.(CastExpr).getExpr().getType() = fromtyp and not fromtyp instanceof IntegralType) or
e instanceof ArrayAccess and e.getType() instanceof IntegralType or
e instanceof MethodAccess and e.getType() instanceof IntegralType or
e instanceof ClassInstanceExpr and e.getType() instanceof IntegralType or
e.getType() instanceof FloatingPointType or
deprecated private predicate unknownParity(Expr e) {
e instanceof AssignDivExpr
or
e instanceof AssignRShiftExpr
or
e instanceof AssignURShiftExpr
or
e instanceof DivExpr
or
e instanceof RShiftExpr
or
e instanceof URShiftExpr
or
exists(Type fromtyp |
e.(CastExpr).getExpr().getType() = fromtyp and not fromtyp instanceof IntegralType
)
or
e instanceof ArrayAccess and e.getType() instanceof IntegralType
or
e instanceof MethodAccess and e.getType() instanceof IntegralType
or
e instanceof ClassInstanceExpr and e.getType() instanceof IntegralType
or
e.getType() instanceof FloatingPointType
or
e.getType() instanceof CharacterType
}
/** Gets a possible parity for `e`. */
private Parity exprParity(Expr e) {
result = certainExprParity(e) or
deprecated private Parity exprParity(Expr e) {
result = certainExprParity(e)
or
not exists(certainExprParity(e)) and
(
result = exprParity(e.(ParExpr).getExpr()) or
result = exprParity(arrLenDef(e)) or
exists(SsaVariable v | v.getAUse() = e | result = ssaParity(v)) and not exists(arrLenDef(e)) or
result = exprParity(e.(ParExpr).getExpr())
or
result = exprParity(arrLenDef(e))
or
exists(SsaVariable v | v.getAUse() = e | result = ssaParity(v)) and
not exists(arrLenDef(e))
or
exists(FieldAccess fa | fa = e |
not exists(SsaVariable v | v.getAUse() = fa) and
not exists(arrLenDef(e)) and
result = fieldParity(fa.getField())
) or
)
or
exists(VarAccess va | va = e |
not exists(SsaVariable v | v.getAUse() = va) and
not va instanceof FieldAccess and
(result = true or result = false)
) or
result = exprParity(e.(AssignExpr).getSource()) or
result = exprParity(e.(PlusExpr).getExpr()) or
result = exprParity(e.(PostIncExpr).getExpr()) or
result = exprParity(e.(PostDecExpr).getExpr()) or
result = exprParity(e.(PreIncExpr).getExpr()).booleanNot() or
result = exprParity(e.(PreDecExpr).getExpr()).booleanNot() or
result = exprParity(e.(MinusExpr).getExpr()) or
result = exprParity(e.(BitNotExpr).getExpr()).booleanNot() or
unknownParity(e) and (result = true or result = false) or
)
or
result = exprParity(e.(AssignExpr).getSource())
or
result = exprParity(e.(PlusExpr).getExpr())
or
result = exprParity(e.(PostIncExpr).getExpr())
or
result = exprParity(e.(PostDecExpr).getExpr())
or
result = exprParity(e.(PreIncExpr).getExpr()).booleanNot()
or
result = exprParity(e.(PreDecExpr).getExpr()).booleanNot()
or
result = exprParity(e.(MinusExpr).getExpr())
or
result = exprParity(e.(BitNotExpr).getExpr()).booleanNot()
or
unknownParity(e) and
(result = true or result = false)
or
exists(Parity p1, Parity p2, AssignOp a |
a = e and
p1 = exprParity(a.getDest()) and
p2 = exprParity(a.getRhs())
|
a instanceof AssignAddExpr and result = p1.booleanXor(p2) or
a instanceof AssignSubExpr and result = p1.booleanXor(p2) or
a instanceof AssignMulExpr and result = p1.booleanAnd(p2) or
a instanceof AssignRemExpr and (p2.isEven() and result = p1 or p2.isOdd() and (result = true or result = false)) or
a instanceof AssignAndExpr and result = p1.booleanAnd(p2) or
a instanceof AssignOrExpr and result = p1.booleanOr(p2) or
a instanceof AssignXorExpr and result = p1.booleanXor(p2) or
a instanceof AssignLShiftExpr and (result.isEven() or result = p1 and not strictlyPositive(a.getRhs()))
) or
|
a instanceof AssignAddExpr and result = p1.booleanXor(p2)
or
a instanceof AssignSubExpr and result = p1.booleanXor(p2)
or
a instanceof AssignMulExpr and result = p1.booleanAnd(p2)
or
a instanceof AssignRemExpr and
(
p2.isEven() and result = p1
or
p2.isOdd() and
(result = true or result = false)
)
or
a instanceof AssignAndExpr and result = p1.booleanAnd(p2)
or
a instanceof AssignOrExpr and result = p1.booleanOr(p2)
or
a instanceof AssignXorExpr and result = p1.booleanXor(p2)
or
a instanceof AssignLShiftExpr and
(
result.isEven()
or
result = p1 and not strictlyPositive(a.getRhs())
)
)
or
exists(Parity p1, Parity p2, BinaryExpr bin |
bin = e and
p1 = exprParity(bin.getLeftOperand()) and
p2 = exprParity(bin.getRightOperand())
|
bin instanceof AddExpr and result = p1.booleanXor(p2) or
bin instanceof SubExpr and result = p1.booleanXor(p2) or
bin instanceof MulExpr and result = p1.booleanAnd(p2) or
bin instanceof RemExpr and (p2.isEven() and result = p1 or p2.isOdd() and (result = true or result = false)) or
bin instanceof AndBitwiseExpr and result = p1.booleanAnd(p2) or
bin instanceof OrBitwiseExpr and result = p1.booleanOr(p2) or
bin instanceof XorBitwiseExpr and result = p1.booleanXor(p2) or
bin instanceof LShiftExpr and (result.isEven() or result = p1 and not strictlyPositive(bin.getRightOperand()))
) or
result = exprParity(e.(ConditionalExpr).getTrueExpr()) or
result = exprParity(e.(ConditionalExpr).getFalseExpr()) or
|
bin instanceof AddExpr and result = p1.booleanXor(p2)
or
bin instanceof SubExpr and result = p1.booleanXor(p2)
or
bin instanceof MulExpr and result = p1.booleanAnd(p2)
or
bin instanceof RemExpr and
(
p2.isEven() and result = p1
or
p2.isOdd() and
(result = true or result = false)
)
or
bin instanceof AndBitwiseExpr and result = p1.booleanAnd(p2)
or
bin instanceof OrBitwiseExpr and result = p1.booleanOr(p2)
or
bin instanceof XorBitwiseExpr and result = p1.booleanXor(p2)
or
bin instanceof LShiftExpr and
(
result.isEven()
or
result = p1 and not strictlyPositive(bin.getRightOperand())
)
)
or
result = exprParity(e.(ConditionalExpr).getTrueExpr())
or
result = exprParity(e.(ConditionalExpr).getFalseExpr())
or
result = exprParity(e.(CastExpr).getExpr())
)
}
@@ -207,15 +319,15 @@ private Parity exprParity(Expr e) {
/**
* Gets the parity of `e` if it can be uniquely determined.
*/
Parity getExprParity(Expr e) {
result = exprParity(e) and 1 = count(exprParity(e))
}
deprecated Parity getExprParity(Expr e) { result = exprParity(e) and 1 = count(exprParity(e)) }
/**
* DEPRECATED: Use semmle.code.java.dataflow.ModulusAnalysis instead.
*
* Holds if the parity can be determined for both sides of `comp`. The boolean
* `eqparity` indicates whether the two sides have equal or opposite parity.
*/
predicate parityComparison(ComparisonExpr comp, boolean eqparity) {
deprecated predicate parityComparison(ComparisonExpr comp, boolean eqparity) {
exists(Expr left, Expr right, boolean lpar, boolean rpar |
comp.getLeftOperand() = left and
comp.getRightOperand() = right and
@@ -224,4 +336,3 @@ predicate parityComparison(ComparisonExpr comp, boolean eqparity) {
eqparity = lpar.booleanXor(rpar).booleanNot()
)
}

View File

@@ -68,14 +68,16 @@ private import SSA
private import RangeUtils
private import semmle.code.java.controlflow.internal.GuardsLogic
private import SignAnalysis
private import ParityAnalysis
private import ModulusAnalysis
private import semmle.code.java.Reflection
private import semmle.code.java.Collections
private import semmle.code.java.Maps
import Bound
cached private module RangeAnalysisCache {
cached module RangeAnalysisPublic {
cached
private module RangeAnalysisCache {
cached
module RangeAnalysisPublic {
/**
* Holds if `b + delta` is a valid bound for `e`.
* - `upper = true` : `e <= b + delta`
@@ -85,7 +87,8 @@ cached private module RangeAnalysisCache {
* 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) {
cached
predicate bounded(Expr e, Bound b, int delta, boolean upper, Reason reason) {
bounded(e, b, delta, upper, _, _, reason)
}
}
@@ -93,59 +96,116 @@ cached private module RangeAnalysisCache {
/**
* Holds if `guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)`.
*/
cached predicate possibleReason(Guard guard) { guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _) }
cached
predicate possibleReason(Guard guard) {
guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)
}
}
private import RangeAnalysisCache
import RangeAnalysisPublic
/**
* Gets a condition that tests whether `v` equals `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
private Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
exists(boolean eqpolarity |
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
(testIsTrue = true or testIsTrue = false) and
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 | implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0))
}
/**
* 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) {
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().getProperExpr() = sub and comp.getGreaterOperand() = c and
sub.getLeftOperand() = ssaRead(v, d) and sub.getRightOperand() = e and
upper = true and delta = d + c.getIntValue()
comp.getLesserOperand().getProperExpr() = sub and
comp.getGreaterOperand() = c and
sub.getLeftOperand() = ssaRead(v, d) and
sub.getRightOperand() = e and
upper = true and
delta = d + c.getIntValue()
or
// (v - d) - e > c
comp.getGreaterOperand().getProperExpr() = sub and comp.getLesserOperand() = c and
sub.getLeftOperand() = ssaRead(v, d) and sub.getRightOperand() = e and
upper = false and delta = d + c.getIntValue()
comp.getGreaterOperand().getProperExpr() = sub and
comp.getLesserOperand() = c and
sub.getLeftOperand() = ssaRead(v, d) and
sub.getRightOperand() = e and
upper = false and
delta = d + c.getIntValue()
or
// e - (v - d) < c
comp.getLesserOperand().getProperExpr() = sub and comp.getGreaterOperand() = c and
sub.getLeftOperand() = e and sub.getRightOperand() = ssaRead(v, d) and
upper = false and delta = d - c.getIntValue()
comp.getLesserOperand().getProperExpr() = sub and
comp.getGreaterOperand() = c and
sub.getLeftOperand() = e and
sub.getRightOperand() = ssaRead(v, d) and
upper = false and
delta = d - c.getIntValue()
or
// e - (v - d) > c
comp.getGreaterOperand().getProperExpr() = sub and comp.getLesserOperand() = c and
sub.getLeftOperand() = e and sub.getRightOperand() = ssaRead(v, d) and
upper = true and delta = d - c.getIntValue()
comp.getGreaterOperand().getProperExpr() = sub and
comp.getLesserOperand() = c and
sub.getLeftOperand() = e and
sub.getRightOperand() = ssaRead(v, d) and
upper = true and
delta = d - c.getIntValue()
)
}
private predicate gcdInput(int x, int y) {
exists(ComparisonExpr comp, Bound b |
exprModulus(comp.getLesserOperand(), b, _, x) and
exprModulus(comp.getGreaterOperand(), b, _, y)
)
or
exists(int x0, int y0 |
gcdInput(x0, y0) and
x = y0 and
y = x0 % y0
)
}
private int gcd(int x, int y) {
result = x.abs() and y = 0 and gcdInput(x, y)
or
result = gcd(y, x % y) and y != 0 and gcdInput(x, y)
}
/**
* 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 = gcd(mod1, 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
)
}
@@ -157,27 +217,47 @@ private predicate boundCondition(ComparisonExpr comp, SsaVariable v, Expr e, int
* - `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 |
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
// A non-strict inequality `x <= y` can be strengthened to `x <= y - 1` if
// `x` and `y` have opposite parities, and a strict inequality `x < y` can
// be similarly strengthened if `x` and `y` have equal parities.
(if parityComparison(comp, resultIsStrict) then d2 = strengthen else d2 = 0) 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
(
resultIsStrict = true and d3 = strengthen
or
resultIsStrict = false and d3 = 0
) and
delta = d1 + d2 + d3
) 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
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)
}
private newtype TReason =
@@ -189,14 +269,13 @@ private newtype TReason =
* is due to a specific condition, or `NoReason` if the bound is inferred
* without going through a bounding condition.
*/
abstract class Reason extends TReason {
abstract string toString();
}
class NoReason extends Reason, TNoReason {
override string toString() { result = "NoReason" }
}
abstract class Reason extends TReason { abstract string toString(); }
class NoReason extends Reason, TNoReason { override string toString() { result = "NoReason" } }
class CondReason extends Reason, TCondReason {
Guard getCond() { this = TCondReason(result) }
override string toString() { result = getCond().toString() }
}
@@ -205,15 +284,14 @@ class CondReason extends Reason, TCondReason {
* - `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) {
exists(SsaExplicitUpdate upd | v = upd and pos.hasReadOfVar(v) and reason = TNoReason() |
upd.getDefiningExpr().(VariableAssign).getSource() = e and delta = 0 and (upper = true or upper = false) or
upd.getDefiningExpr().(PostIncExpr).getExpr() = e and delta = 1 and (upper = true or upper = false) or
upd.getDefiningExpr().(PreIncExpr).getExpr() = e and delta = 1 and (upper = true or upper = false) or
upd.getDefiningExpr().(PostDecExpr).getExpr() = e and delta = -1 and (upper = true or upper = false) or
upd.getDefiningExpr().(PreDecExpr).getExpr() = e and delta = -1 and (upper = true or upper = false) or
upd.getDefiningExpr().(AssignOp) = e and delta = 0 and (upper = true or upper = false)
) or
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
@@ -223,7 +301,9 @@ private predicate boundFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
}
/** Holds if `v != e + delta` at `pos`. */
private predicate unequalFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, int delta, Reason reason) {
private predicate unequalFlowStepSsa(
SsaVariable v, SsaReadPosition pos, Expr e, int delta, Reason reason
) {
exists(Guard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = eqFlowCond(v, e, delta, false, testIsTrue) and
@@ -238,16 +318,25 @@ private predicate unequalFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e,
*/
private predicate safeCast(Type fromtyp, Type totyp) {
exists(PrimitiveType pfrom, PrimitiveType pto | pfrom = fromtyp and pto = totyp |
pfrom = pto or
pfrom.hasName("char") and pto.getName().regexpMatch("int|long|float|double") or
pfrom.hasName("byte") and pto.getName().regexpMatch("short|int|long|float|double") or
pfrom.hasName("short") and pto.getName().regexpMatch("int|long|float|double") or
pfrom.hasName("int") and pto.getName().regexpMatch("long|float|double") or
pfrom.hasName("long") and pto.getName().regexpMatch("float|double") or
pfrom.hasName("float") and pto.hasName("double") or
pfrom = pto
or
pfrom.hasName("char") and pto.getName().regexpMatch("int|long|float|double")
or
pfrom.hasName("byte") and pto.getName().regexpMatch("short|int|long|float|double")
or
pfrom.hasName("short") and pto.getName().regexpMatch("int|long|float|double")
or
pfrom.hasName("int") and pto.getName().regexpMatch("long|float|double")
or
pfrom.hasName("long") and pto.getName().regexpMatch("float|double")
or
pfrom.hasName("float") and pto.hasName("double")
or
pfrom.hasName("double") and pto.hasName("float")
) or
safeCast(fromtyp.(BoxedType).getPrimitiveType(), totyp) or
)
or
safeCast(fromtyp.(BoxedType).getPrimitiveType(), totyp)
or
safeCast(fromtyp, totyp.(BoxedType).getPrimitiveType())
}
@@ -255,18 +344,19 @@ private predicate safeCast(Type fromtyp, Type totyp) {
* A cast that can be ignored for the purpose of range analysis.
*/
private class SafeCastExpr extends CastExpr {
SafeCastExpr() {
safeCast(getExpr().getType(), getType())
}
SafeCastExpr() { safeCast(getExpr().getType(), getType()) }
}
/**
* 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
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)
}
@@ -278,8 +368,10 @@ private class NarrowingCastExpr extends CastExpr {
not this instanceof SafeCastExpr and
typeBound(getType(), _, _)
}
/** Gets the lower bound of the resulting type. */
int getLowerBound() { typeBound(getType(), result, _) }
/** Gets the upper bound of the resulting type. */
int getUpperBound() { typeBound(getType(), _, result) }
}
@@ -290,78 +382,84 @@ private class NarrowingCastExpr extends CastExpr {
* - `upper = false` : `e2 >= e1 + delta`
*/
private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
e2.(ParExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
e2.(AssignExpr).getSource() = e1 and delta = 0 and (upper = true or upper = false) or
e2.(PlusExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
e2.(PostIncExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
e2.(PostDecExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
e2.(PreIncExpr).getExpr() = e1 and delta = 1 and (upper = true or upper = false) or
e2.(PreDecExpr).getExpr() = e1 and delta = -1 and (upper = true or upper = false) or
e2.(SafeCastExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
exists(SsaExplicitUpdate v, FieldRead arrlen |
e2 = arrlen and
arrlen.getField() instanceof ArrayLengthField and
arrlen.getQualifier() = v.getAUse() and
v.getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getDimension(0) = e1 and
delta = 0 and
(upper = true or upper = false)
) or
valueFlowStep(e2, e1, delta) and
(upper = true or upper = false)
or
e2.(SafeCastExpr).getExpr() = e1 and
delta = 0 and
(upper = true or upper = false)
or
exists(Expr x |
e2.(AddExpr).hasOperands(e1, x) or
e2.(AddExpr).hasOperands(e1, x)
or
exists(AssignAddExpr add | add = e2 |
add.getDest() = e1 and add.getRhs() = x or
add.getDest() = e1 and add.getRhs() = x
or
add.getDest() = x and add.getRhs() = e1
)
|
x.(ConstantIntegerExpr).getIntValue() = delta and (upper = true or upper = false)
or
|
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
not x instanceof ConstantIntegerExpr and
not e1 instanceof ConstantIntegerExpr and
if strictlyPositive(x) then
(upper = false and delta = 1)
else if positive(x) then
(upper = false and delta = 0)
else if strictlyNegative(x) then
(upper = true and delta = -1)
else if negative(x) then
(upper = true and delta = 0)
else
none()
) or
if strictlyPositive(x)
then (
upper = false and delta = 1
) else
if positive(x)
then (
upper = false and delta = 0
) else
if strictlyNegative(x)
then (
upper = true and delta = -1
) else if negative(x) then (upper = true and delta = 0) else none()
)
or
exists(Expr x |
exists(SubExpr sub |
e2 = sub and
sub.getLeftOperand() = e1 and
sub.getRightOperand() = x
) or
)
or
exists(AssignSubExpr sub |
e2 = sub and
sub.getDest() = e1 and
sub.getRhs() = x
)
|
x.(ConstantIntegerExpr).getIntValue() = -delta and (upper = true or upper = false)
or
|
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
not x instanceof ConstantIntegerExpr and
if strictlyPositive(x) then
(upper = true and delta = -1)
else if positive(x) then
(upper = true and delta = 0)
else if strictlyNegative(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
if strictlyPositive(x)
then (
upper = true and delta = -1
) else
if positive(x)
then (
upper = true and delta = 0
) else
if strictlyNegative(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(MethodAccess ma, Method m |
e2 = ma and
ma.getMethod() = m and
@@ -370,11 +468,16 @@ private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
e1 = ma.getAnArgument() and
delta = -1 and
upper = true
) or
)
or
exists(MethodAccess 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.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
@@ -384,11 +487,19 @@ private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
/** 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(LShiftExpr e | e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)) or
exists(AssignLShiftExpr e | e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k))
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(LShiftExpr e |
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
)
or
exists(AssignLShiftExpr e |
e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
)
)
}
@@ -400,76 +511,39 @@ private predicate boundFlowStepMul(Expr e2, Expr e1, int factor) {
*/
private predicate boundFlowStepDiv(Expr e2, Expr e1, int factor) {
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(RShiftExpr e | e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)) or
exists(AssignRShiftExpr e | e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)) or
exists(URShiftExpr e | e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)) or
exists(AssignURShiftExpr e | e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k))
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(RShiftExpr e |
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
)
or
exists(AssignRShiftExpr e |
e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
)
or
exists(URShiftExpr e |
e = e2 and e.getLeftOperand() = e1 and e.getRightOperand() = c and factor = 2.pow(k)
)
or
exists(AssignURShiftExpr e |
e = e2 and e.getDest() = e1 and e.getRhs() = c and factor = 2.pow(k)
)
)
}
private newtype TBound =
TBoundZero() or
TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
TBoundExpr(Expr e) { e.(FieldRead).getField() instanceof ArrayLengthField and not exists(SsaVariable v | e = v.getAUse()) }
/**
* A bound that may be inferred for an expression plus/minus an integer delta.
*/
abstract class Bound extends TBound {
abstract string toString();
/** Gets an expression that equals this bound plus `delta`. */
abstract Expr getExpr(int delta);
/** Gets an expression that equals this bound. */
Expr getExpr() {
result = getExpr(0)
}
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
}
}
/**
* The bound that corresponds to the integer 0. This is used to represent all
* integer bounds as bounds are always accompanied by an added integer delta.
*/
class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
}
/**
* A bound corresponding to the value of an SSA variable.
*/
class SsaBound extends Bound, TBoundSsa {
/** Gets the SSA variable that equals this bound. */
SsaVariable getSsa() { this = TBoundSsa(result) }
override string toString() { result = getSsa().toString() }
override Expr getExpr(int delta) { result = getSsa().getAUse() and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
}
/**
* A bound that corresponds to the value of a specific expression that might be
* interesting, but isn't otherwise represented by the value of an SSA variable.
*/
class ExprBound extends Bound, TBoundExpr {
override string toString() { result = getExpr().toString() }
override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
getExpr().hasLocationInfo(path, sl, sc, el, ec)
}
}
/**
* 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) {
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
@@ -477,14 +551,23 @@ private predicate boundedSsa(SsaVariable v, SsaReadPosition pos, Bound b, int de
// upper = false: v >= mid + d1 >= b + d1 + d2 = b + delta
delta = d1 + d2 and
(if r1 instanceof NoReason then reason = r2 else reason = r1)
) or
)
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)
|
|
unequalSsa(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)
(
upper = true and delta = d - 1
or
upper = false and delta = d + 1
) and
(
reason = r1
or
reason = r2 and not r2 instanceof NoReason
)
)
}
@@ -506,14 +589,19 @@ private predicate unequalSsa(SsaVariable v, SsaReadPosition pos, Bound b, int de
private predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
edge.phiInput(phi, inp) and
// Conservatively assume that every edge is a back edge if we don't have dominance information.
(phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or not hasDominanceInformation(edge.getOrigBlock()))
(
phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
not hasDominanceInformation(edge.getOrigBlock())
)
}
/** 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
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
}
@@ -523,27 +611,43 @@ private int weakenDelta(boolean upper, int delta) {
* - `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) {
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
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 = true and delta = weakenDelta(upper, d - origdelta) + origdelta
or
fromBackEdge0 = false and delta = d
)
else
(delta = d and fromBackEdge = fromBackEdge0)
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) {
private predicate boundedPhiInp1(
SsaPhiNode phi, Bound b, boolean upper, SsaVariable inp, SsaReadPositionPhiInputEdge edge,
int delta
) {
boundedPhiInp(phi, inp, edge, b, delta, upper, _, _, _)
}
@@ -553,11 +657,17 @@ private predicate boundedPhiInp1(SsaPhiNode phi, Bound b, boolean upper, SsaVari
* - `upper = true` : `inp <= phi`
* - `upper = false` : `inp >= phi`
*/
private predicate selfBoundedPhiInp(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, boolean upper) {
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)
(
upper = true and d <= 0
or
upper = false and d >= 0
)
)
}
@@ -568,19 +678,29 @@ private predicate selfBoundedPhiInp(SsaPhiNode phi, SsaVariable inp, SsaReadPosi
* - `upper = false` : `inp >= b + delta`
*/
pragma[noinline]
private predicate boundedPhiCand(SsaPhiNode phi, boolean upper, Bound b, int delta, boolean fromBackEdge, int origdelta, Reason reason) {
exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge | boundedPhiInp(phi, inp, edge, b, delta, upper, fromBackEdge, origdelta, reason))
private predicate boundedPhiCand(
SsaPhiNode phi, boolean upper, Bound b, int delta, boolean fromBackEdge, int origdelta,
Reason reason
) {
exists(SsaVariable inp, SsaReadPositionPhiInputEdge 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(SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, Reason reason, SsaVariable inp, SsaReadPositionPhiInputEdge 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
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)
)
}
@@ -590,7 +710,10 @@ private predicate boundedPhiCandValidForEdge(SsaPhiNode phi, Bound b, int delta,
* - `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) {
private predicate boundedPhi(
SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
Reason reason
) {
forex(SsaVariable inp, SsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
)
@@ -612,14 +735,16 @@ private predicate lowerBoundZero(Expr e) {
* (for `upper = false`) bound of `b`.
*/
private predicate baseBound(Expr e, int b, boolean upper) {
lowerBoundZero(e) and b = 0 and upper = false or
lowerBoundZero(e) and b = 0 and upper = false
or
exists(Method read |
e.(MethodAccess).getMethod().overrides*(read) and
read.getDeclaringType().hasQualifiedName("java.io", "InputStream") and
read.hasName("read") and
read.getNumberOfParameters() = 0
|
upper = true and b = 255 or
|
upper = true and b = 255
or
upper = false and b = -1
)
}
@@ -631,16 +756,18 @@ private predicate baseBound(Expr e, int b, boolean upper) {
* `upper = false` this means that the cast will not underflow.
*/
private predicate safeNarrowingCast(NarrowingCastExpr cast, boolean upper) {
exists(int bound |
bounded(cast.getExpr(), TBoundZero(), bound, upper, _, _, _)
|
upper = true and bound <= cast.getUpperBound() or
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(NarrowingCastExpr cast, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta, Reason reason) {
private predicate boundedCastExpr(
NarrowingCastExpr cast, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
Reason reason
) {
bounded(cast.getExpr(), b, delta, upper, fromBackEdge, origdelta, reason)
}
@@ -649,14 +776,27 @@ private predicate boundedCastExpr(NarrowingCastExpr cast, Bound b, int delta, bo
* - `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
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
)
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.
@@ -665,18 +805,21 @@ private predicate bounded(Expr e, Bound b, int delta, boolean upper, boolean fro
// upper = true: e <= mid + d1 <= b + d1 + d2 = b + delta
// upper = false: e >= mid + d1 >= b + d1 + d2 = b + delta
delta = d1 + d2
) or
)
or
exists(SsaPhiNode phi |
boundedPhi(phi, b, delta, upper, fromBackEdge, origdelta, reason) and
e = phi.getAUse()
) or
)
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
) or
)
or
exists(Expr mid, int factor, int d |
boundFlowStepDiv(e, mid, factor) and
not e instanceof ConstantIntegerExpr and
@@ -684,25 +827,38 @@ private predicate bounded(Expr e, Bound b, int delta, boolean upper, boolean fro
b instanceof ZeroBound and
d >= 0 and
delta = d / factor
) or
)
or
exists(NarrowingCastExpr 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 |
)
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
(
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)
)
}
private predicate boundedConditionalExpr(ConditionalExpr cond, Bound b, boolean upper, boolean branch, int delta, boolean fromBackEdge, int origdelta, Reason reason) {
branch = true and bounded(cond.getTrueExpr(), b, delta, upper, fromBackEdge, origdelta, reason) or
private predicate boundedConditionalExpr(
ConditionalExpr cond, Bound b, boolean upper, boolean branch, int delta, boolean fromBackEdge,
int origdelta, Reason reason
) {
branch = true and bounded(cond.getTrueExpr(), b, delta, upper, fromBackEdge, origdelta, reason)
or
branch = false and bounded(cond.getFalseExpr(), b, delta, upper, fromBackEdge, origdelta, reason)
}

View File

@@ -9,47 +9,60 @@ private import semmle.code.java.controlflow.internal.GuardsLogic
/** An expression that always has the same integer value. */
pragma[nomagic]
private predicate constantIntegerExpr(Expr e, int val) {
e.(CompileTimeConstantExpr).getIntValue() = val or
e.(CompileTimeConstantExpr).getIntValue() = val
or
exists(SsaExplicitUpdate v, Expr src |
e = v.getAUse() and
src = v.getDefiningExpr().(VariableAssign).getSource() and
constantIntegerExpr(src, val)
)
or
exists(SsaExplicitUpdate v, FieldRead arrlen |
e = arrlen and
arrlen.getField() instanceof ArrayLengthField and
arrlen.getQualifier() = v.getAUse() and
v.getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getFirstDimensionSize() = val
)
}
/** An expression that always has the same integer value. */
class ConstantIntegerExpr extends Expr {
ConstantIntegerExpr() {
constantIntegerExpr(this, _)
}
ConstantIntegerExpr() { constantIntegerExpr(this, _) }
/** Gets the integer value of this expression. */
int getIntValue() {
constantIntegerExpr(this, result)
}
int getIntValue() { constantIntegerExpr(this, result) }
}
/**
* Gets an expression that equals `v - d`.
*/
Expr ssaRead(SsaVariable v, int delta) {
result = v.getAUse() and delta = 0 or
result.(ParExpr).getExpr() = ssaRead(v, delta) or
result = v.getAUse() and delta = 0
or
result.(ParExpr).getExpr() = ssaRead(v, delta)
or
exists(int d1, ConstantIntegerExpr c |
result.(AddExpr).hasOperands(ssaRead(v, d1), c) and
delta = d1 - c.getIntValue()
) or
)
or
exists(SubExpr sub, int d1, ConstantIntegerExpr c |
result = sub and
sub.getLeftOperand() = ssaRead(v, d1) and
sub.getRightOperand() = c and
delta = d1 + c.getIntValue()
) or
v.(SsaExplicitUpdate).getDefiningExpr().(PreIncExpr) = result and delta = 0 or
v.(SsaExplicitUpdate).getDefiningExpr().(PreDecExpr) = result and delta = 0 or
v.(SsaExplicitUpdate).getDefiningExpr().(PostIncExpr) = result and delta = 1 or // x++ === ++x - 1
v.(SsaExplicitUpdate).getDefiningExpr().(PostDecExpr) = result and delta = -1 or // x-- === --x + 1
v.(SsaExplicitUpdate).getDefiningExpr().(Assignment) = result and delta = 0 or
)
or
v.(SsaExplicitUpdate).getDefiningExpr().(PreIncExpr) = result and delta = 0
or
v.(SsaExplicitUpdate).getDefiningExpr().(PreDecExpr) = result and delta = 0
or
v.(SsaExplicitUpdate).getDefiningExpr().(PostIncExpr) = result and delta = 1 // x++ === ++x - 1
or
v.(SsaExplicitUpdate).getDefiningExpr().(PostDecExpr) = result and delta = -1 // x-- === --x + 1
or
v.(SsaExplicitUpdate).getDefiningExpr().(Assignment) = result and delta = 0
or
result.(AssignExpr).getSource() = ssaRead(v, delta)
}
@@ -114,7 +127,8 @@ class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiIn
* value `testIsTrue`.
*/
predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue) or
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)
@@ -125,9 +139,101 @@ predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled,
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
*/
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue) or
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
or
exists(Guard guard0, boolean testIsTrue0 |
implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
guardControlsSsaRead(guard0, controlled, testIsTrue0)
)
}
/**
* Gets a condition that tests whether `v` equals `e + delta`.
*
* If the condition evaluates to `testIsTrue`:
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
exists(boolean eqpolarity |
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
(testIsTrue = true or testIsTrue = false) and
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 |
implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
)
}
/**
* 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`.
*/
predicate valueFlowStep(Expr e2, Expr e1, int delta) {
e2.(ParExpr).getExpr() = e1 and delta = 0
or
e2.(AssignExpr).getSource() = e1 and delta = 0
or
e2.(PlusExpr).getExpr() = e1 and delta = 0
or
e2.(PostIncExpr).getExpr() = e1 and delta = 0
or
e2.(PostDecExpr).getExpr() = e1 and delta = 0
or
e2.(PreIncExpr).getExpr() = e1 and delta = 1
or
e2.(PreDecExpr).getExpr() = e1 and delta = -1
or
exists(SsaExplicitUpdate v, FieldRead arrlen |
e2 = arrlen and
arrlen.getField() instanceof ArrayLengthField and
arrlen.getQualifier() = v.getAUse() and
v.getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getDimension(0) = e1 and
delta = 0
)
or
exists(Expr x |
e2.(AddExpr).hasOperands(e1, x)
or
exists(AssignAddExpr add | add = e2 |
add.getDest() = e1 and add.getRhs() = x
or
add.getDest() = x and add.getRhs() = e1
)
|
x.(ConstantIntegerExpr).getIntValue() = delta
)
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.(ConstantIntegerExpr).getIntValue() = -delta
)
}

View File

@@ -724,76 +724,27 @@ private predicate localFlowBigStep(
localFlowExit(node2, config)
}
/**
* Holds if `f` may contain an object of the same type, `t`, as the one
* that contains `f`, and if this fact should be used to compress
* access paths.
*
* Examples include the tail pointer in a linked list or the left and right
* pointers in a binary tree.
*/
private predicate selfRef(Content f, RefType t) {
t = f.getDeclaringType() and
f.isSelfRef()
}
private newtype TFlowContainer =
TRegularContent(Content f) { not selfRef(f, _) } or
TSelfRefContent(RefType t) { selfRef(_, t) }
/**
* A `Content` or a `Content` abstracted as its declaring type.
*
* Sequences of one or more `Content`s in the same declaring type for which
* `isSelfRef()` holds are represented as a single `FlowContainer` in an
* `AccessPath`.
*/
private class FlowContainer extends TFlowContainer {
string toString() {
exists(Content f | this = TRegularContent(f) and result = f.toString())
or
exists(RefType t | this = TSelfRefContent(t) and result = t.toString())
}
predicate usesContent(Content f) {
this = TRegularContent(f)
or
exists(RefType t | this = TSelfRefContent(t) and selfRef(f, t))
}
RefType getContainerType() {
exists(Content f | this = TRegularContent(f) and result = f.getDeclaringType())
or
this = TSelfRefContent(result)
}
}
private newtype TAccessPathFront =
TFrontNil(Type t) or
TFrontHead(FlowContainer f)
TFrontHead(Content f)
/**
* The front of an `AccessPath`. This is either a head or a nil.
*/
private class AccessPathFront extends TAccessPathFront {
string toString() {
exists(Type t | this = TFrontNil(t) | result = t.toString())
exists(Type t | this = TFrontNil(t) | result = ppReprType(t))
or
exists(FlowContainer f | this = TFrontHead(f) | result = f.toString())
exists(Content f | this = TFrontHead(f) | result = f.toString())
}
Type getType() {
this = TFrontNil(result)
or
exists(FlowContainer head | this = TFrontHead(head) | result = head.getContainerType())
exists(Content head | this = TFrontHead(head) | result = head.getContainerType())
}
predicate headUsesContent(Content f) {
exists(FlowContainer fc |
fc.usesContent(f) and
this = TFrontHead(fc)
)
}
predicate headUsesContent(Content f) { this = TFrontHead(f) }
}
private class AccessPathFrontNil extends AccessPathFront, TFrontNil { }
@@ -1004,7 +955,7 @@ private predicate consCand(Content f, AccessPathFront apf, Configuration config)
private newtype TAccessPath =
TNil(Type t) or
TCons(FlowContainer f, int len) { len in [1 .. 5] }
TCons(Content f, int len) { len in [1 .. 5] }
/**
* Conceptually a list of `Content`s followed by a `Type`, but only the first
@@ -1016,7 +967,7 @@ private newtype TAccessPath =
private class AccessPath extends TAccessPath {
abstract string toString();
FlowContainer getHead() { this = TCons(result, _) }
Content getHead() { this = TCons(result, _) }
int len() {
this = TNil(_) and result = 0
@@ -1027,27 +978,27 @@ private class AccessPath extends TAccessPath {
Type getType() {
this = TNil(result)
or
exists(FlowContainer head | this = TCons(head, _) | result = head.getContainerType())
exists(Content head | this = TCons(head, _) | result = head.getContainerType())
}
abstract AccessPathFront getFront();
}
private class AccessPathNil extends AccessPath, TNil {
override string toString() { exists(Type t | this = TNil(t) | result = t.toString()) }
override string toString() { exists(Type t | this = TNil(t) | result = ppReprType(t)) }
override AccessPathFront getFront() { exists(Type t | this = TNil(t) | result = TFrontNil(t)) }
}
private class AccessPathCons extends AccessPath, TCons {
override string toString() {
exists(FlowContainer f, int len | this = TCons(f, len) |
exists(Content f, int len | this = TCons(f, len) |
result = f.toString() + ", ... (" + len.toString() + ")"
)
}
override AccessPathFront getFront() {
exists(FlowContainer f | this = TCons(f, _) | result = TFrontHead(f))
exists(Content f | this = TCons(f, _) | result = TFrontHead(f))
}
}

View File

@@ -724,76 +724,27 @@ private predicate localFlowBigStep(
localFlowExit(node2, config)
}
/**
* Holds if `f` may contain an object of the same type, `t`, as the one
* that contains `f`, and if this fact should be used to compress
* access paths.
*
* Examples include the tail pointer in a linked list or the left and right
* pointers in a binary tree.
*/
private predicate selfRef(Content f, RefType t) {
t = f.getDeclaringType() and
f.isSelfRef()
}
private newtype TFlowContainer =
TRegularContent(Content f) { not selfRef(f, _) } or
TSelfRefContent(RefType t) { selfRef(_, t) }
/**
* A `Content` or a `Content` abstracted as its declaring type.
*
* Sequences of one or more `Content`s in the same declaring type for which
* `isSelfRef()` holds are represented as a single `FlowContainer` in an
* `AccessPath`.
*/
private class FlowContainer extends TFlowContainer {
string toString() {
exists(Content f | this = TRegularContent(f) and result = f.toString())
or
exists(RefType t | this = TSelfRefContent(t) and result = t.toString())
}
predicate usesContent(Content f) {
this = TRegularContent(f)
or
exists(RefType t | this = TSelfRefContent(t) and selfRef(f, t))
}
RefType getContainerType() {
exists(Content f | this = TRegularContent(f) and result = f.getDeclaringType())
or
this = TSelfRefContent(result)
}
}
private newtype TAccessPathFront =
TFrontNil(Type t) or
TFrontHead(FlowContainer f)
TFrontHead(Content f)
/**
* The front of an `AccessPath`. This is either a head or a nil.
*/
private class AccessPathFront extends TAccessPathFront {
string toString() {
exists(Type t | this = TFrontNil(t) | result = t.toString())
exists(Type t | this = TFrontNil(t) | result = ppReprType(t))
or
exists(FlowContainer f | this = TFrontHead(f) | result = f.toString())
exists(Content f | this = TFrontHead(f) | result = f.toString())
}
Type getType() {
this = TFrontNil(result)
or
exists(FlowContainer head | this = TFrontHead(head) | result = head.getContainerType())
exists(Content head | this = TFrontHead(head) | result = head.getContainerType())
}
predicate headUsesContent(Content f) {
exists(FlowContainer fc |
fc.usesContent(f) and
this = TFrontHead(fc)
)
}
predicate headUsesContent(Content f) { this = TFrontHead(f) }
}
private class AccessPathFrontNil extends AccessPathFront, TFrontNil { }
@@ -1004,7 +955,7 @@ private predicate consCand(Content f, AccessPathFront apf, Configuration config)
private newtype TAccessPath =
TNil(Type t) or
TCons(FlowContainer f, int len) { len in [1 .. 5] }
TCons(Content f, int len) { len in [1 .. 5] }
/**
* Conceptually a list of `Content`s followed by a `Type`, but only the first
@@ -1016,7 +967,7 @@ private newtype TAccessPath =
private class AccessPath extends TAccessPath {
abstract string toString();
FlowContainer getHead() { this = TCons(result, _) }
Content getHead() { this = TCons(result, _) }
int len() {
this = TNil(_) and result = 0
@@ -1027,27 +978,27 @@ private class AccessPath extends TAccessPath {
Type getType() {
this = TNil(result)
or
exists(FlowContainer head | this = TCons(head, _) | result = head.getContainerType())
exists(Content head | this = TCons(head, _) | result = head.getContainerType())
}
abstract AccessPathFront getFront();
}
private class AccessPathNil extends AccessPath, TNil {
override string toString() { exists(Type t | this = TNil(t) | result = t.toString()) }
override string toString() { exists(Type t | this = TNil(t) | result = ppReprType(t)) }
override AccessPathFront getFront() { exists(Type t | this = TNil(t) | result = TFrontNil(t)) }
}
private class AccessPathCons extends AccessPath, TCons {
override string toString() {
exists(FlowContainer f, int len | this = TCons(f, len) |
exists(Content f, int len | this = TCons(f, len) |
result = f.toString() + ", ... (" + len.toString() + ")"
)
}
override AccessPathFront getFront() {
exists(FlowContainer f | this = TCons(f, _) | result = TFrontHead(f))
exists(Content f | this = TCons(f, _) | result = TFrontHead(f))
}
}

View File

@@ -724,76 +724,27 @@ private predicate localFlowBigStep(
localFlowExit(node2, config)
}
/**
* Holds if `f` may contain an object of the same type, `t`, as the one
* that contains `f`, and if this fact should be used to compress
* access paths.
*
* Examples include the tail pointer in a linked list or the left and right
* pointers in a binary tree.
*/
private predicate selfRef(Content f, RefType t) {
t = f.getDeclaringType() and
f.isSelfRef()
}
private newtype TFlowContainer =
TRegularContent(Content f) { not selfRef(f, _) } or
TSelfRefContent(RefType t) { selfRef(_, t) }
/**
* A `Content` or a `Content` abstracted as its declaring type.
*
* Sequences of one or more `Content`s in the same declaring type for which
* `isSelfRef()` holds are represented as a single `FlowContainer` in an
* `AccessPath`.
*/
private class FlowContainer extends TFlowContainer {
string toString() {
exists(Content f | this = TRegularContent(f) and result = f.toString())
or
exists(RefType t | this = TSelfRefContent(t) and result = t.toString())
}
predicate usesContent(Content f) {
this = TRegularContent(f)
or
exists(RefType t | this = TSelfRefContent(t) and selfRef(f, t))
}
RefType getContainerType() {
exists(Content f | this = TRegularContent(f) and result = f.getDeclaringType())
or
this = TSelfRefContent(result)
}
}
private newtype TAccessPathFront =
TFrontNil(Type t) or
TFrontHead(FlowContainer f)
TFrontHead(Content f)
/**
* The front of an `AccessPath`. This is either a head or a nil.
*/
private class AccessPathFront extends TAccessPathFront {
string toString() {
exists(Type t | this = TFrontNil(t) | result = t.toString())
exists(Type t | this = TFrontNil(t) | result = ppReprType(t))
or
exists(FlowContainer f | this = TFrontHead(f) | result = f.toString())
exists(Content f | this = TFrontHead(f) | result = f.toString())
}
Type getType() {
this = TFrontNil(result)
or
exists(FlowContainer head | this = TFrontHead(head) | result = head.getContainerType())
exists(Content head | this = TFrontHead(head) | result = head.getContainerType())
}
predicate headUsesContent(Content f) {
exists(FlowContainer fc |
fc.usesContent(f) and
this = TFrontHead(fc)
)
}
predicate headUsesContent(Content f) { this = TFrontHead(f) }
}
private class AccessPathFrontNil extends AccessPathFront, TFrontNil { }
@@ -1004,7 +955,7 @@ private predicate consCand(Content f, AccessPathFront apf, Configuration config)
private newtype TAccessPath =
TNil(Type t) or
TCons(FlowContainer f, int len) { len in [1 .. 5] }
TCons(Content f, int len) { len in [1 .. 5] }
/**
* Conceptually a list of `Content`s followed by a `Type`, but only the first
@@ -1016,7 +967,7 @@ private newtype TAccessPath =
private class AccessPath extends TAccessPath {
abstract string toString();
FlowContainer getHead() { this = TCons(result, _) }
Content getHead() { this = TCons(result, _) }
int len() {
this = TNil(_) and result = 0
@@ -1027,27 +978,27 @@ private class AccessPath extends TAccessPath {
Type getType() {
this = TNil(result)
or
exists(FlowContainer head | this = TCons(head, _) | result = head.getContainerType())
exists(Content head | this = TCons(head, _) | result = head.getContainerType())
}
abstract AccessPathFront getFront();
}
private class AccessPathNil extends AccessPath, TNil {
override string toString() { exists(Type t | this = TNil(t) | result = t.toString()) }
override string toString() { exists(Type t | this = TNil(t) | result = ppReprType(t)) }
override AccessPathFront getFront() { exists(Type t | this = TNil(t) | result = TFrontNil(t)) }
}
private class AccessPathCons extends AccessPath, TCons {
override string toString() {
exists(FlowContainer f, int len | this = TCons(f, len) |
exists(Content f, int len | this = TCons(f, len) |
result = f.toString() + ", ... (" + len.toString() + ")"
)
}
override AccessPathFront getFront() {
exists(FlowContainer f | this = TCons(f, _) | result = TFrontHead(f))
exists(Content f | this = TCons(f, _) | result = TFrontHead(f))
}
}

View File

@@ -724,76 +724,27 @@ private predicate localFlowBigStep(
localFlowExit(node2, config)
}
/**
* Holds if `f` may contain an object of the same type, `t`, as the one
* that contains `f`, and if this fact should be used to compress
* access paths.
*
* Examples include the tail pointer in a linked list or the left and right
* pointers in a binary tree.
*/
private predicate selfRef(Content f, RefType t) {
t = f.getDeclaringType() and
f.isSelfRef()
}
private newtype TFlowContainer =
TRegularContent(Content f) { not selfRef(f, _) } or
TSelfRefContent(RefType t) { selfRef(_, t) }
/**
* A `Content` or a `Content` abstracted as its declaring type.
*
* Sequences of one or more `Content`s in the same declaring type for which
* `isSelfRef()` holds are represented as a single `FlowContainer` in an
* `AccessPath`.
*/
private class FlowContainer extends TFlowContainer {
string toString() {
exists(Content f | this = TRegularContent(f) and result = f.toString())
or
exists(RefType t | this = TSelfRefContent(t) and result = t.toString())
}
predicate usesContent(Content f) {
this = TRegularContent(f)
or
exists(RefType t | this = TSelfRefContent(t) and selfRef(f, t))
}
RefType getContainerType() {
exists(Content f | this = TRegularContent(f) and result = f.getDeclaringType())
or
this = TSelfRefContent(result)
}
}
private newtype TAccessPathFront =
TFrontNil(Type t) or
TFrontHead(FlowContainer f)
TFrontHead(Content f)
/**
* The front of an `AccessPath`. This is either a head or a nil.
*/
private class AccessPathFront extends TAccessPathFront {
string toString() {
exists(Type t | this = TFrontNil(t) | result = t.toString())
exists(Type t | this = TFrontNil(t) | result = ppReprType(t))
or
exists(FlowContainer f | this = TFrontHead(f) | result = f.toString())
exists(Content f | this = TFrontHead(f) | result = f.toString())
}
Type getType() {
this = TFrontNil(result)
or
exists(FlowContainer head | this = TFrontHead(head) | result = head.getContainerType())
exists(Content head | this = TFrontHead(head) | result = head.getContainerType())
}
predicate headUsesContent(Content f) {
exists(FlowContainer fc |
fc.usesContent(f) and
this = TFrontHead(fc)
)
}
predicate headUsesContent(Content f) { this = TFrontHead(f) }
}
private class AccessPathFrontNil extends AccessPathFront, TFrontNil { }
@@ -1004,7 +955,7 @@ private predicate consCand(Content f, AccessPathFront apf, Configuration config)
private newtype TAccessPath =
TNil(Type t) or
TCons(FlowContainer f, int len) { len in [1 .. 5] }
TCons(Content f, int len) { len in [1 .. 5] }
/**
* Conceptually a list of `Content`s followed by a `Type`, but only the first
@@ -1016,7 +967,7 @@ private newtype TAccessPath =
private class AccessPath extends TAccessPath {
abstract string toString();
FlowContainer getHead() { this = TCons(result, _) }
Content getHead() { this = TCons(result, _) }
int len() {
this = TNil(_) and result = 0
@@ -1027,27 +978,27 @@ private class AccessPath extends TAccessPath {
Type getType() {
this = TNil(result)
or
exists(FlowContainer head | this = TCons(head, _) | result = head.getContainerType())
exists(Content head | this = TCons(head, _) | result = head.getContainerType())
}
abstract AccessPathFront getFront();
}
private class AccessPathNil extends AccessPath, TNil {
override string toString() { exists(Type t | this = TNil(t) | result = t.toString()) }
override string toString() { exists(Type t | this = TNil(t) | result = ppReprType(t)) }
override AccessPathFront getFront() { exists(Type t | this = TNil(t) | result = TFrontNil(t)) }
}
private class AccessPathCons extends AccessPath, TCons {
override string toString() {
exists(FlowContainer f, int len | this = TCons(f, len) |
exists(Content f, int len | this = TCons(f, len) |
result = f.toString() + ", ... (" + len.toString() + ")"
)
}
override AccessPathFront getFront() {
exists(FlowContainer f | this = TCons(f, _) | result = TFrontHead(f))
exists(Content f | this = TCons(f, _) | result = TFrontHead(f))
}
}

View File

@@ -724,76 +724,27 @@ private predicate localFlowBigStep(
localFlowExit(node2, config)
}
/**
* Holds if `f` may contain an object of the same type, `t`, as the one
* that contains `f`, and if this fact should be used to compress
* access paths.
*
* Examples include the tail pointer in a linked list or the left and right
* pointers in a binary tree.
*/
private predicate selfRef(Content f, RefType t) {
t = f.getDeclaringType() and
f.isSelfRef()
}
private newtype TFlowContainer =
TRegularContent(Content f) { not selfRef(f, _) } or
TSelfRefContent(RefType t) { selfRef(_, t) }
/**
* A `Content` or a `Content` abstracted as its declaring type.
*
* Sequences of one or more `Content`s in the same declaring type for which
* `isSelfRef()` holds are represented as a single `FlowContainer` in an
* `AccessPath`.
*/
private class FlowContainer extends TFlowContainer {
string toString() {
exists(Content f | this = TRegularContent(f) and result = f.toString())
or
exists(RefType t | this = TSelfRefContent(t) and result = t.toString())
}
predicate usesContent(Content f) {
this = TRegularContent(f)
or
exists(RefType t | this = TSelfRefContent(t) and selfRef(f, t))
}
RefType getContainerType() {
exists(Content f | this = TRegularContent(f) and result = f.getDeclaringType())
or
this = TSelfRefContent(result)
}
}
private newtype TAccessPathFront =
TFrontNil(Type t) or
TFrontHead(FlowContainer f)
TFrontHead(Content f)
/**
* The front of an `AccessPath`. This is either a head or a nil.
*/
private class AccessPathFront extends TAccessPathFront {
string toString() {
exists(Type t | this = TFrontNil(t) | result = t.toString())
exists(Type t | this = TFrontNil(t) | result = ppReprType(t))
or
exists(FlowContainer f | this = TFrontHead(f) | result = f.toString())
exists(Content f | this = TFrontHead(f) | result = f.toString())
}
Type getType() {
this = TFrontNil(result)
or
exists(FlowContainer head | this = TFrontHead(head) | result = head.getContainerType())
exists(Content head | this = TFrontHead(head) | result = head.getContainerType())
}
predicate headUsesContent(Content f) {
exists(FlowContainer fc |
fc.usesContent(f) and
this = TFrontHead(fc)
)
}
predicate headUsesContent(Content f) { this = TFrontHead(f) }
}
private class AccessPathFrontNil extends AccessPathFront, TFrontNil { }
@@ -1004,7 +955,7 @@ private predicate consCand(Content f, AccessPathFront apf, Configuration config)
private newtype TAccessPath =
TNil(Type t) or
TCons(FlowContainer f, int len) { len in [1 .. 5] }
TCons(Content f, int len) { len in [1 .. 5] }
/**
* Conceptually a list of `Content`s followed by a `Type`, but only the first
@@ -1016,7 +967,7 @@ private newtype TAccessPath =
private class AccessPath extends TAccessPath {
abstract string toString();
FlowContainer getHead() { this = TCons(result, _) }
Content getHead() { this = TCons(result, _) }
int len() {
this = TNil(_) and result = 0
@@ -1027,27 +978,27 @@ private class AccessPath extends TAccessPath {
Type getType() {
this = TNil(result)
or
exists(FlowContainer head | this = TCons(head, _) | result = head.getContainerType())
exists(Content head | this = TCons(head, _) | result = head.getContainerType())
}
abstract AccessPathFront getFront();
}
private class AccessPathNil extends AccessPath, TNil {
override string toString() { exists(Type t | this = TNil(t) | result = t.toString()) }
override string toString() { exists(Type t | this = TNil(t) | result = ppReprType(t)) }
override AccessPathFront getFront() { exists(Type t | this = TNil(t) | result = TFrontNil(t)) }
}
private class AccessPathCons extends AccessPath, TCons {
override string toString() {
exists(FlowContainer f, int len | this = TCons(f, len) |
exists(Content f, int len | this = TCons(f, len) |
result = f.toString() + ", ... (" + len.toString() + ")"
)
}
override AccessPathFront getFront() {
exists(FlowContainer f | this = TCons(f, _) | result = TFrontHead(f))
exists(Content f | this = TCons(f, _) | result = TFrontHead(f))
}
}

View File

@@ -118,7 +118,7 @@ private module ImplCommon {
node1.(ArgumentNode).argumentOf(call, i1) and
node2.getPreUpdateNode().(ArgumentNode).argumentOf(call, i2) and
compatibleTypes(node1.getTypeBound(), f.getType()) and
compatibleTypes(node2.getTypeBound(), f.getDeclaringType())
compatibleTypes(node2.getTypeBound(), f.getContainerType())
)
}
@@ -149,7 +149,7 @@ private module ImplCommon {
setterReturn(p, f) and
arg.argumentOf(node2.asExpr(), _) and
compatibleTypes(node1.getTypeBound(), f.getType()) and
compatibleTypes(node2.getTypeBound(), f.getDeclaringType())
compatibleTypes(node2.getTypeBound(), f.getContainerType())
)
}
@@ -174,7 +174,7 @@ private module ImplCommon {
viableParamArg(p, arg) and
getter(p, f) and
arg.argumentOf(node2.asExpr(), _) and
compatibleTypes(node1.getTypeBound(), f.getDeclaringType()) and
compatibleTypes(node1.getTypeBound(), f.getContainerType()) and
compatibleTypes(node2.getTypeBound(), f.getType())
)
}

View File

@@ -724,76 +724,27 @@ private predicate localFlowBigStep(
localFlowExit(node2, config)
}
/**
* Holds if `f` may contain an object of the same type, `t`, as the one
* that contains `f`, and if this fact should be used to compress
* access paths.
*
* Examples include the tail pointer in a linked list or the left and right
* pointers in a binary tree.
*/
private predicate selfRef(Content f, RefType t) {
t = f.getDeclaringType() and
f.isSelfRef()
}
private newtype TFlowContainer =
TRegularContent(Content f) { not selfRef(f, _) } or
TSelfRefContent(RefType t) { selfRef(_, t) }
/**
* A `Content` or a `Content` abstracted as its declaring type.
*
* Sequences of one or more `Content`s in the same declaring type for which
* `isSelfRef()` holds are represented as a single `FlowContainer` in an
* `AccessPath`.
*/
private class FlowContainer extends TFlowContainer {
string toString() {
exists(Content f | this = TRegularContent(f) and result = f.toString())
or
exists(RefType t | this = TSelfRefContent(t) and result = t.toString())
}
predicate usesContent(Content f) {
this = TRegularContent(f)
or
exists(RefType t | this = TSelfRefContent(t) and selfRef(f, t))
}
RefType getContainerType() {
exists(Content f | this = TRegularContent(f) and result = f.getDeclaringType())
or
this = TSelfRefContent(result)
}
}
private newtype TAccessPathFront =
TFrontNil(Type t) or
TFrontHead(FlowContainer f)
TFrontHead(Content f)
/**
* The front of an `AccessPath`. This is either a head or a nil.
*/
private class AccessPathFront extends TAccessPathFront {
string toString() {
exists(Type t | this = TFrontNil(t) | result = t.toString())
exists(Type t | this = TFrontNil(t) | result = ppReprType(t))
or
exists(FlowContainer f | this = TFrontHead(f) | result = f.toString())
exists(Content f | this = TFrontHead(f) | result = f.toString())
}
Type getType() {
this = TFrontNil(result)
or
exists(FlowContainer head | this = TFrontHead(head) | result = head.getContainerType())
exists(Content head | this = TFrontHead(head) | result = head.getContainerType())
}
predicate headUsesContent(Content f) {
exists(FlowContainer fc |
fc.usesContent(f) and
this = TFrontHead(fc)
)
}
predicate headUsesContent(Content f) { this = TFrontHead(f) }
}
private class AccessPathFrontNil extends AccessPathFront, TFrontNil { }
@@ -1004,7 +955,7 @@ private predicate consCand(Content f, AccessPathFront apf, Configuration config)
private newtype TAccessPath =
TNil(Type t) or
TCons(FlowContainer f, int len) { len in [1 .. 5] }
TCons(Content f, int len) { len in [1 .. 5] }
/**
* Conceptually a list of `Content`s followed by a `Type`, but only the first
@@ -1016,7 +967,7 @@ private newtype TAccessPath =
private class AccessPath extends TAccessPath {
abstract string toString();
FlowContainer getHead() { this = TCons(result, _) }
Content getHead() { this = TCons(result, _) }
int len() {
this = TNil(_) and result = 0
@@ -1027,27 +978,27 @@ private class AccessPath extends TAccessPath {
Type getType() {
this = TNil(result)
or
exists(FlowContainer head | this = TCons(head, _) | result = head.getContainerType())
exists(Content head | this = TCons(head, _) | result = head.getContainerType())
}
abstract AccessPathFront getFront();
}
private class AccessPathNil extends AccessPath, TNil {
override string toString() { exists(Type t | this = TNil(t) | result = t.toString()) }
override string toString() { exists(Type t | this = TNil(t) | result = ppReprType(t)) }
override AccessPathFront getFront() { exists(Type t | this = TNil(t) | result = TFrontNil(t)) }
}
private class AccessPathCons extends AccessPath, TCons {
override string toString() {
exists(FlowContainer f, int len | this = TCons(f, len) |
exists(Content f, int len | this = TCons(f, len) |
result = f.toString() + ", ... (" + len.toString() + ")"
)
}
override AccessPathFront getFront() {
exists(FlowContainer f | this = TCons(f, _) | result = TFrontHead(f))
exists(Content f | this = TCons(f, _) | result = TFrontHead(f))
}
}

View File

@@ -118,20 +118,10 @@ class Content extends TContent {
}
/** Gets the type of the object containing this content. */
abstract RefType getDeclaringType();
abstract RefType getContainerType();
/** Gets the type of this content. */
abstract Type getType();
/**
* Holds if this content may contain an object of the same type as the one
* that contains this content, and if this fact should be used to compress
* access paths.
*
* Examples include the tail pointer in a linked list or the left and right
* pointers in a binary tree.
*/
predicate isSelfRef() { none() }
}
private class FieldContent extends Content, TFieldContent {
@@ -147,17 +137,15 @@ private class FieldContent extends Content, TFieldContent {
f.getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
override RefType getDeclaringType() { result = f.getDeclaringType() }
override RefType getContainerType() { result = f.getDeclaringType() }
override Type getType() { result = getFieldTypeBound(f) }
override predicate isSelfRef() { compatibleTypes(getDeclaringType(), getType()) }
}
private class CollectionContent extends Content, TCollectionContent {
override string toString() { result = "collection" }
override RefType getDeclaringType() { none() }
override RefType getContainerType() { none() }
override Type getType() { none() }
}
@@ -165,7 +153,7 @@ private class CollectionContent extends Content, TCollectionContent {
private class ArrayContent extends Content, TArrayContent {
override string toString() { result = "array" }
override RefType getDeclaringType() { none() }
override RefType getContainerType() { none() }
override Type getType() { none() }
}
@@ -212,6 +200,13 @@ RefType getErasedRepr(Type t) {
)
}
/** Gets a string representation of a type returned by `getErasedRepr`. */
string ppReprType(Type t) {
if t.(BoxedType).getPrimitiveType().getName() = "double"
then result = "Number"
else result = t.toString()
}
private predicate canContainBool(Type t) {
t instanceof BooleanType or
any(BooleanType b).(RefType).getASourceSupertype+() = t
@@ -227,12 +222,9 @@ predicate compatibleTypes(Type t1, Type t2) {
e1 = getErasedRepr(t1) and
e2 = getErasedRepr(t2)
|
/*
* Because of `getErasedRepr`, `erasedHaveIntersection` is a sufficient
* compatibility check, but `conContainBool` is kept as a dummy disjunct
* to get the proper join-order.
*/
// Because of `getErasedRepr`, `erasedHaveIntersection` is a sufficient
// compatibility check, but `conContainBool` is kept as a dummy disjunct
// to get the proper join-order.
erasedHaveIntersection(e1, e2)
or
canContainBool(e1) and canContainBool(e2)

View File

@@ -0,0 +1,165 @@
public class A {
private static final int[] arr1 = new int[] { 1, 2, 3, 4, 5, 6, 7, 8 };
private final int[] arr2;
private final int[] arr3;
public A(int[] arr2, int n) {
if (arr2.length % 2 != 0)
throw new Exception();
this.arr2 = arr2;
this.arr3 = new int[n << 1];
}
void m1(int[] a) {
int sum = 0;
for (int i = 0; i <= a.length; i++) {
sum += a[i]; // Out of bounds
}
}
void m2(int[] a) {
int sum = 0;
for (int i = 0; i < a.length; i += 2) {
sum += a[i] + a[i + 1]; // Out of bounds (unless len%2==0)
}
}
void m3(int[] a) {
if (a.length % 2 != 0)
return;
int sum = 0;
for (int i = 0; i < a.length; ) {
sum += a[i++]; // OK
sum += a[i++]; // OK
}
for (int i = 0; i < arr1.length; ) {
sum += arr1[i++]; // OK
sum += arr1[i++]; // OK - FP
i += 2;
}
for (int i = 0; i < arr2.length; ) {
sum += arr2[i++]; // OK
sum += arr2[i++]; // OK - FP
}
for (int i = 0; i < arr3.length; ) {
sum += arr3[i++]; // OK
sum += arr3[i++]; // OK - FP
}
int[] b;
if (sum > 3)
b = a;
else
b = arr1;
for (int i = 0; i < b.length; i++) {
sum += b[i]; // OK
sum += b[++i]; // OK - FP
}
}
void m4(int[] a, int[] b) {
assert a.length % 2 == 0;
int sum = 0;
for (int i = 0; i < a.length; ) {
sum += a[i++]; // OK
sum += a[i++]; // OK - FP
}
int len = b.length;
if ((len & 1) != 0)
return;
for (int i = 0; i < len; ) {
sum += b[i++]; // OK
sum += b[i++]; // OK
}
}
void m5(int n) {
int[] a = new int[3 * n];
int sum = 0;
for (int i = 0; i < a.length; i += 3) {
sum += a[i] + a[i + 1] + a[i + 2]; // OK
}
}
int m6(int[] a, int ix) {
if (ix < 0 || ix > a.length)
return 0;
return a[ix]; // Out of bounds
}
void m7() {
int[] xs = new int[11];
int sum = 0;
for (int i = 0; i < 11; i++) {
for (int j = 0; j < 11; j++) {
sum += xs[i]; // OK
sum += xs[j]; // OK
if (i < j)
sum += xs[i + 11 - j]; // OK - FP
else
sum += xs[i - j]; // OK
}
}
}
void m8(int[] a) {
if ((a.length - 4) % 3 != 0)
return;
int sum = 0;
for (int i = 4; i < a.length; i += 3) {
sum += a[i]; // OK
sum += a[i + 1]; // OK - FP
sum += a[i + 2]; // OK - FP
}
}
void m9() {
int[] a = new int[] { 1, 2, 3, 4, 5 };
int sum = 0;
for (int i = 0; i < 10; i++) {
if (i < 5)
sum += a[i]; // OK
else
sum += a[9 - i]; // OK - FP
}
}
void m10(int n, int m) {
int len = Math.min(n, m);
int[] a = new int[n];
int sum = 0;
for (int i = n - 1; i >= 0; i--) {
sum += a[i]; // OK
for (int j = i + 1; j < len; j++) {
sum += a[j]; // OK
sum += a[i + 1]; // OK - FP
}
}
}
void m11(int n) {
int len = n*2;
int[] a = new int[len];
int sum = 0;
for (int i = 0; i < len; i = i + 2) {
sum += a[i+1]; // OK
for (int j = i; j < len - 2; j = j + 2) {
sum += a[j]; // OK
sum += a[j+1]; // OK
sum += a[j+2]; // OK
sum += a[j+3]; // OK
}
}
}
void m12() {
int[] a = new int[] { 1, 2, 3, 4, 5, 6 };
int sum = 0;
for (int i = 0; i < a.length; i += 2) {
sum += a[i] + a[i + 1]; // OK
}
int[] b = new int[8];
for (int i = 2; i < 8; i += 2) {
sum += b[i] + b[i + 1]; // OK
}
}
}

View File

@@ -0,0 +1,13 @@
| A.java:16:14:16:17 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:23:21:23:28 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:37:14:37:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:42:14:42:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:46:14:46:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:55:14:55:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:64:14:64:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:86:12:86:16 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:97:18:97:31 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 8. |
| A.java:110:14:110:21 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
| A.java:111:14:111:21 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 1. |
| A.java:122:16:122:23 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 3. |
| A.java:134:16:134:23 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |

View File

@@ -0,0 +1 @@
Likely Bugs/Collections/ArrayIndexOutOfBounds.ql

View File

@@ -0,0 +1,22 @@
import java.util.*;
import java.util.function.*;
public class B {
int modcount = 0;
int[] arr;
public void modify(IntUnaryOperator func) {
int mc = modcount;
for (int i = 0; i < arr.length; i++) {
arr[i] = func.applyAsInt(arr[i]);
}
// Always false unless there is a call path from func.applyAsInt(..) to
// this method, but should not be reported, as checks guarding
// ConcurrentModificationExceptions are expected to always be false in the
// absence of API misuse.
if (mc != modcount)
throw new ConcurrentModificationException();
modcount++;
}
}