hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-29 18:55:14 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #334 from aschackmull/java/autoformat-rangeanalysis

Browse Source 
Approved by yh-semmle
This commit is contained in:
semmle-qlci
2018-10-18 15:38:33 +01:00
committed by GitHub
parent 3af91d5d0a 187918396c
commit 4dd868fb3d
5 changed files with 710 additions and 342 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
java/ql/src/semmle/code/java/dataflow/Bound.qll
View File

@@ -5,19 +5,23 @@ 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()) }
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)
}
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
}
@@ -29,6 +33,7 @@ abstract class Bound extends TBound {
*/
class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
}
@@ -38,8 +43,11 @@ class ZeroBound extends Bound, TBoundZero {
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)
}
@@ -51,7 +59,9 @@ class SsaBound extends Bound, TBoundSsa {
*/
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)
}

100
java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
View File

@@ -32,7 +32,8 @@ private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
exists(AddExpr a | a = add |
larg = a.getLeftOperand() and
rarg = a.getRightOperand()
) or
)
or
exists(AssignAddExpr a | a = add |
larg = a.getDest() and
rarg = a.getRhs()
@@ -51,7 +52,8 @@ private predicate nonConstSubtraction(Expr sub, Expr larg, Expr rarg) {
exists(SubExpr s | s = sub |
larg = s.getLeftOperand() and
rarg = s.getRightOperand()
) or
)
or
exists(AssignSubExpr s | s = sub |
larg = s.getDest() and
rarg = s.getRhs()
@@ -67,12 +69,14 @@ private Expr modExpr(Expr arg, int mod) {
arg = rem.getLeftOperand() and
rem.getRightOperand().(CompileTimeConstantExpr).getIntValue() = mod and
mod >= 2
) or
)
or
exists(CompileTimeConstantExpr c |
mod = 2.pow([1..30]) and
mod = 2.pow([1 .. 30]) and
c.getIntValue() = mod - 1 and
result.(AndBitwiseExpr).hasOperands(arg, c)
) or
)
or
result.(ParExpr).getExpr() = modExpr(arg, mod)
}
@@ -88,7 +92,9 @@ private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
(
testIsTrue = polarity and val = r
or
testIsTrue = polarity.booleanNot() and mod = 2 and val = 1 - r and
testIsTrue = polarity.booleanNot() and
mod = 2 and
val = 1 - r and
(r = 0 or r = 1)
)
)
@@ -109,17 +115,22 @@ private predicate moduloGuardedRead(SsaVariable v, SsaReadPosition pos, int val,
bindingset[mask]
private predicate andmaskFactor(int mask, int factor) {
mask % factor = 0 and
factor = 2.pow([1..30])
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.(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))
)
}
@@ -134,9 +145,17 @@ 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) {
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()))
edge = rank[r](SsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e
order by
getId(e.getOrigBlock())
)
}
/**
@@ -154,9 +173,11 @@ private int gcdLim() { result = 128 }
*/
private int gcd(int x, int y) {
result != 1 and
result = x.abs() and y = 0 and x in [-gcdLim()..gcdLim()]
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()]
result = gcd(y, x % y) and y != 0 and x in [-gcdLim() .. gcdLim()]
}
/**
@@ -167,14 +188,17 @@ private int gcd(int x, int y) {
*/
bindingset[val, mod]
private int remainder(int val, int mod) {
mod = 0 and result = val or
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) {
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
@@ -204,7 +228,7 @@ private predicate phiModulusRankStep(SsaPhiNode phi, Bound b, int val, int mod,
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
@@ -257,18 +281,22 @@ private predicate ssaModulus(SsaVariable v, SsaReadPosition pos, Bound b, int va
*/
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
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
)
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
)
or
exists(ConditionalExpr cond, int v1, int v2, int m1, int m2 |
cond = e and
condExprBranchModulus(cond, true, b, v1, m1) and
@@ -276,17 +304,20 @@ predicate exprModulus(Expr e, Bound b, int val, int mod) {
mod = gcd(gcd(m1, m2), v1 - v2) and
mod != 1 and
val = remainder(v1, mod)
) or
)
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 = b1 and b2 instanceof ZeroBound
or
b = b2 and b1 instanceof ZeroBound
) or
)
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
@@ -296,15 +327,16 @@ predicate exprModulus(Expr e, Bound b, int val, int mod) {
)
}
private predicate condExprBranchModulus(ConditionalExpr cond, boolean branch, Bound b, int val, int mod) {
exprModulus(cond.getTrueExpr(), b, val, mod) and branch = true or
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)
|
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
@@ -312,9 +344,7 @@ private predicate addModulus(Expr add, boolean isLeft, Bound b, int val, int mod
}
private predicate subModulus(Expr sub, boolean isLeft, Bound b, int val, int mod) {
exists(Expr larg, Expr rarg |
nonConstSubtraction(sub, larg, rarg)
|
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

305
java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll
View File

@@ -6,6 +6,7 @@
* The analysis is implemented as an abstract interpretation over the
* two-valued domain `{even, odd}`.
*/
import java
private import SSA
private import RangeUtils
@@ -14,38 +15,35 @@ private import SignAnalysis
private import semmle.code.java.Reflection
/** Gets an expression that is the remainder modulo 2 of `arg`. */
deprecated
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. */
deprecated
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`.
*/
deprecated
class Parity extends boolean {
deprecated class Parity extends boolean {
Parity() { this = true or this = false }
predicate isEven() { this = false }
predicate isOdd() { this = true }
}
@@ -53,8 +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`.
*/
deprecated
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
@@ -62,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()
)
)
@@ -71,26 +69,36 @@ private Guard parityCheck(SsaVariable v, Parity parity, boolean testIsTrue) {
/**
* Gets the parity of `e` if it can be directly determined.
*/
deprecated
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()
)
)
@@ -99,119 +107,211 @@ private Parity certainExprParity(Expr e) {
/**
* Gets the expression that defines the array length that equals `len`, if any.
*/
deprecated
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`. */
deprecated
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`. */
deprecated
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. */
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
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`. */
deprecated
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())
)
}
@@ -219,10 +319,7 @@ private Parity exprParity(Expr e) {
/**
* Gets the parity of `e` if it can be uniquely determined.
*/
deprecated
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.
@@ -230,8 +327,7 @@ Parity getExprParity(Expr e) {
* 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.
*/
deprecated
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
@@ -240,4 +336,3 @@ predicate parityComparison(ComparisonExpr comp, boolean eqparity) {
eqparity = lpar.booleanXor(rpar).booleanNot()
)
}

526
java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
View File

@@ -74,9 +74,10 @@ 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`
@@ -86,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)
}
}
@@ -94,8 +96,10 @@ 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
@@ -105,31 +109,45 @@ import RangeAnalysisPublic
* - `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()
)
}
@@ -137,7 +155,8 @@ private predicate gcdInput(int x, int y) {
exists(ComparisonExpr comp, Bound b |
exprModulus(comp.getLesserOperand(), b, _, x) and
exprModulus(comp.getGreaterOperand(), b, _, y)
) or
)
or
exists(int x0, int y0 |
gcdInput(x0, y0) and
x = y0 and
@@ -157,7 +176,9 @@ private int gcd(int x, int y) {
* 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 |
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
@@ -169,9 +190,21 @@ private predicate modulusComparison(ComparisonExpr comp, boolean testIsTrue, int
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
(
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
)
}
@@ -184,27 +217,47 @@ private predicate modulusComparison(ComparisonExpr comp, boolean testIsTrue, 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
(
exists(int k | modulusComparison(comp, testIsTrue, k) and d2 = strengthen * k) or
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 =
@@ -216,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() }
}
@@ -232,8 +284,13 @@ 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) {
ssaUpdateStep(v, e, delta) and pos.hasReadOfVar(v) and (upper = true or upper = false) and reason = TNoReason()
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
@@ -244,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
@@ -259,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())
}
@@ -276,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)
}
@@ -299,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) }
}
@@ -311,62 +382,84 @@ private class NarrowingCastExpr extends CastExpr {
* - `upper = false` : `e2 >= e1 + delta`
*/
private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
valueFlowStep(e2, e1, delta) and (upper = true or upper = false) or
e2.(SafeCastExpr).getExpr() = 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 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 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
@@ -375,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
@@ -389,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)
)
)
}
@@ -405,12 +511,27 @@ 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)
)
)
}
@@ -419,7 +540,10 @@ private predicate boundFlowStepDiv(Expr e2, Expr e1, int factor) {
* - `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
@@ -427,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
)
)
}
@@ -456,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
}
@@ -473,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, _, _, _)
}
@@ -503,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
)
)
}
@@ -518,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)
)
}
@@ -540,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)
)
@@ -562,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
)
}
@@ -581,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(), any(ZeroBound zb), 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)
}
@@ -599,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.
@@ -615,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
@@ -634,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)
}

103
java/ql/src/semmle/code/java/dataflow/RangeUtils.qll
View File

@@ -9,7 +9,8 @@ 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
@@ -26,37 +27,42 @@ private predicate constantIntegerExpr(Expr e, int 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)
}
@@ -121,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)
@@ -132,7 +139,8 @@ 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)
@@ -153,18 +161,25 @@ Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsT
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
)
or
exists(boolean testIsTrue0 | implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0))
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().(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
}
@@ -172,41 +187,53 @@ predicate ssaUpdateStep(SsaExplicitUpdate v, Expr e, int delta) {
* 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
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
)
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
) or
)
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
)
}