hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-03-01 13:23:49 +01:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #4193 from tamasvajk/feature/sign-analysis

Browse Source 
C#: Sign analysis
This commit is contained in:
Tamás Vajk
2020-09-22 15:33:33 +02:00
committed by GitHub
parent 66e2ed9b65 06dbec78f7
commit 54c35748f0
33 changed files with 2670 additions and 696 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -6,6 +6,7 @@
import java
private import SSA
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
private import RangeUtils
private import semmle.code.java.controlflow.Guards
import Bound

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

@@ -66,6 +66,7 @@
import java
private import SSA
private import RangeUtils
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
private import semmle.code.java.controlflow.internal.GuardsLogic
private import SignAnalysis
private import ModulusAnalysis

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

@@ -5,6 +5,7 @@
import java
private import SSA
private import semmle.code.java.controlflow.internal.GuardsLogic
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
/**
* Holds if `v` is an input to `phi` that is not along a back edge, and the
@@ -127,63 +128,6 @@ Expr ssaRead(SsaVariable v, int delta) {
result.(AssignExpr).getSource() = ssaRead(v, delta)
}
private newtype TSsaReadPosition =
TSsaReadPositionBlock(BasicBlock bb) { exists(SsaVariable v | bb = v.getAUse().getBasicBlock()) } or
TSsaReadPositionPhiInputEdge(BasicBlock bbOrig, BasicBlock bbPhi) {
exists(SsaPhiNode phi | phi.hasInputFromBlock(_, bbOrig) and bbPhi = phi.getBasicBlock())
}
/**
* A position at which an SSA variable is read. This includes both ordinary
* reads occurring in basic blocks and input to phi nodes occurring along an
* edge between two basic blocks.
*/
class SsaReadPosition extends TSsaReadPosition {
/** Holds if `v` is read at this position. */
abstract predicate hasReadOfVar(SsaVariable v);
/** Gets a textual representation of this SSA read position. */
abstract string toString();
}
/** A basic block in which an SSA variable is read. */
class SsaReadPositionBlock extends SsaReadPosition, TSsaReadPositionBlock {
/** Gets the basic block corresponding to this position. */
BasicBlock getBlock() { this = TSsaReadPositionBlock(result) }
override predicate hasReadOfVar(SsaVariable v) { getBlock() = v.getAUse().getBasicBlock() }
override string toString() { result = "block" }
}
/**
* An edge between two basic blocks where the latter block has an SSA phi
* definition. The edge therefore has a read of an SSA variable serving as the
* input to the phi node.
*/
class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiInputEdge {
/** Gets the head of the edge. */
BasicBlock getOrigBlock() { this = TSsaReadPositionPhiInputEdge(result, _) }
/** Gets the tail of the edge. */
BasicBlock getPhiBlock() { this = TSsaReadPositionPhiInputEdge(_, result) }
override predicate hasReadOfVar(SsaVariable v) {
exists(SsaPhiNode phi |
phi.hasInputFromBlock(v, getOrigBlock()) and
getPhiBlock() = phi.getBasicBlock()
)
}
/** Holds if `inp` is an input to `phi` along this edge. */
predicate phiInput(SsaPhiNode phi, SsaVariable inp) {
phi.hasInputFromBlock(inp, getOrigBlock()) and
getPhiBlock() = phi.getBasicBlock()
}
override string toString() { result = "edge" }
}
/**
* Holds if `inp` is an input to `phi` along a back edge.
*/

594
java/ql/src/semmle/code/java/dataflow/SignAnalysis.qll
View File

@@ -6,596 +6,4 @@
* three-valued domain `{negative, zero, positive}`.
*/
import java
private import SSA
private import RangeUtils
private import semmle.code.java.controlflow.Guards
private import semmle.code.java.Reflection
private import semmle.code.java.Collections
private import semmle.code.java.Maps
private newtype TSign =
TNeg() or
TZero() or
TPos()
private class Sign extends TSign {
string toString() {
result = "-" and this = TNeg()
or
result = "0" and this = TZero()
or
result = "+" and this = TPos()
}
Sign inc() {
this = TNeg() and result = TNeg()
or
this = TNeg() and result = TZero()
or
this = TZero() and result = TPos()
or
this = TPos() and result = TPos()
}
Sign dec() { result.inc() = this }
Sign neg() {
this = TNeg() and result = TPos()
or
this = TZero() and result = TZero()
or
this = TPos() and result = TNeg()
}
Sign bitnot() {
this = TNeg() and result = TPos()
or
this = TNeg() and result = TZero()
or
this = TZero() and result = TNeg()
or
this = TPos() and result = TNeg()
}
Sign add(Sign s) {
this = TZero() and result = s
or
s = TZero() and result = this
or
this = s and this = result
or
this = TPos() and s = TNeg()
or
this = TNeg() and s = TPos()
}
Sign mul(Sign s) {
result = TZero() and this = TZero()
or
result = TZero() and s = TZero()
or
result = TNeg() and this = TPos() and s = TNeg()
or
result = TNeg() and this = TNeg() and s = TPos()
or
result = TPos() and this = TPos() and s = TPos()
or
result = TPos() and this = TNeg() and s = TNeg()
}
Sign div(Sign s) {
result = TZero() and s = TNeg()
or
result = TZero() and s = TPos()
or
result = TNeg() and this = TPos() and s = TNeg()
or
result = TNeg() and this = TNeg() and s = TPos()
or
result = TPos() and this = TPos() and s = TPos()
or
result = TPos() and this = TNeg() and s = TNeg()
}
Sign rem(Sign s) {
result = TZero() and s = TNeg()
or
result = TZero() and s = TPos()
or
result = this and s = TNeg()
or
result = this and s = TPos()
}
Sign bitand(Sign s) {
result = TZero() and this = TZero()
or
result = TZero() and s = TZero()
or
result = TZero() and this = TPos()
or
result = TZero() and s = TPos()
or
result = TNeg() and this = TNeg() and s = TNeg()
or
result = TPos() and this = TNeg() and s = TPos()
or
result = TPos() and this = TPos() and s = TNeg()
or
result = TPos() and this = TPos() and s = TPos()
}
Sign bitor(Sign s) {
result = TZero() and this = TZero() and s = TZero()
or
result = TNeg() and this = TNeg()
or
result = TNeg() and s = TNeg()
or
result = TPos() and this = TPos() and s = TZero()
or
result = TPos() and this = TZero() and s = TPos()
or
result = TPos() and this = TPos() and s = TPos()
}
Sign bitxor(Sign s) {
result = TZero() and this = s
or
result = this and s = TZero()
or
result = s and this = TZero()
or
result = TPos() and this = TPos() and s = TPos()
or
result = TNeg() and this = TNeg() and s = TPos()
or
result = TNeg() and this = TPos() and s = TNeg()
or
result = TPos() and this = TNeg() and s = TNeg()
}
Sign lshift(Sign s) {
result = TZero() and this = TZero()
or
result = this and s = TZero()
or
this != TZero() and s != TZero()
}
Sign rshift(Sign s) {
result = TZero() and this = TZero()
or
result = this and s = TZero()
or
result = TNeg() and this = TNeg()
or
result != TNeg() and this = TPos() and s != TZero()
}
Sign urshift(Sign s) {
result = TZero() and this = TZero()
or
result = this and s = TZero()
or
result != TZero() and this = TNeg() and s != TZero()
or
result != TNeg() and this = TPos() and s != TZero()
}
}
/** Gets the sign of `e` if this can be directly determined. */
private Sign certainExprSign(Expr e) {
exists(int i | e.(ConstantIntegerExpr).getIntValue() = i |
i < 0 and result = TNeg()
or
i = 0 and result = TZero()
or
i > 0 and result = TPos()
)
or
not exists(e.(ConstantIntegerExpr).getIntValue()) and
(
exists(float f |
f = e.(LongLiteral).getValue().toFloat() or
f = e.(FloatingPointLiteral).getValue().toFloat() or
f = e.(DoubleLiteral).getValue().toFloat()
|
f < 0 and result = TNeg()
or
f = 0 and result = TZero()
or
f > 0 and result = TPos()
)
or
exists(string charlit | charlit = e.(CharacterLiteral).getValue() |
if charlit = "\\0" or charlit = "\\u0000" then result = TZero() else result = TPos()
)
or
e.(MethodAccess).getMethod() instanceof StringLengthMethod and
(result = TPos() or result = TZero())
or
e.(MethodAccess).getMethod() instanceof CollectionSizeMethod and
(result = TPos() or result = TZero())
or
e.(MethodAccess).getMethod() instanceof MapSizeMethod and
(result = TPos() or result = TZero())
)
}
/** Holds if the sign of `e` is too complicated to determine. */
private predicate unknownSign(Expr e) {
not exists(e.(ConstantIntegerExpr).getIntValue()) and
(
exists(IntegerLiteral lit | lit = e and not exists(lit.getValue().toInt()))
or
exists(LongLiteral lit | lit = e and not exists(lit.getValue().toFloat()))
or
exists(CastExpr cast, Type fromtyp |
cast = e and
fromtyp = cast.getExpr().getType() and
not fromtyp instanceof NumericOrCharType
)
or
e instanceof ArrayAccess and e.getType() instanceof NumericOrCharType
or
e instanceof MethodAccess and e.getType() instanceof NumericOrCharType
or
e instanceof ClassInstanceExpr and e.getType() instanceof NumericOrCharType
)
}
/**
* Holds if `lowerbound` is a lower bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate lowerBound(Expr lowerbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) {
exists(boolean testIsTrue, ComparisonExpr comp |
pos.hasReadOfVar(v) and
guardControlsSsaRead(comp, pos, testIsTrue) and
not unknownSign(lowerbound)
|
testIsTrue = true and
comp.getLesserOperand() = lowerbound and
comp.getGreaterOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = true else isStrict = false)
or
testIsTrue = false and
comp.getGreaterOperand() = lowerbound and
comp.getLesserOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
/**
* Holds if `upperbound` is an upper bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate upperBound(Expr upperbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) {
exists(boolean testIsTrue, ComparisonExpr comp |
pos.hasReadOfVar(v) and
guardControlsSsaRead(comp, pos, testIsTrue) and
not unknownSign(upperbound)
|
testIsTrue = true and
comp.getGreaterOperand() = upperbound and
comp.getLesserOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = true else isStrict = false)
or
testIsTrue = false and
comp.getLesserOperand() = upperbound and
comp.getGreaterOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
/**
* Holds if `eqbound` is an equality/inequality for `v` at `pos`. This is
* restricted to only include bounds for which we might determine a sign. The
* boolean `isEq` gives the polarity:
* - `isEq = true` : `v = eqbound`
* - `isEq = false` : `v != eqbound`
*/
private predicate eqBound(Expr eqbound, SsaVariable v, SsaReadPosition pos, boolean isEq) {
exists(Guard guard, boolean testIsTrue, boolean polarity |
pos.hasReadOfVar(v) and
guardControlsSsaRead(guard, pos, testIsTrue) and
guard.isEquality(eqbound, ssaRead(v, 0), polarity) and
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
not unknownSign(eqbound)
)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
* order for `v` to be positive.
*/
private predicate posBound(Expr bound, SsaVariable v, SsaReadPosition pos) {
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
* order for `v` to be negative.
*/
private predicate negBound(Expr bound, SsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
* can be zero.
*/
private predicate zeroBound(Expr bound, SsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, _)
}
/** Holds if `bound` allows `v` to be positive at `pos`. */
private predicate posBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) {
posBound(bound, v, pos) and TPos() = exprSign(bound)
}
/** Holds if `bound` allows `v` to be negative at `pos`. */
private predicate negBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) {
negBound(bound, v, pos) and TNeg() = exprSign(bound)
}
/** Holds if `bound` allows `v` to be zero at `pos`. */
private predicate zeroBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) and TNeg() = exprSign(bound)
or
lowerBound(bound, v, pos, false) and TZero() = exprSign(bound)
or
upperBound(bound, v, pos, _) and TPos() = exprSign(bound)
or
upperBound(bound, v, pos, false) and TZero() = exprSign(bound)
or
eqBound(bound, v, pos, true) and TZero() = exprSign(bound)
or
eqBound(bound, v, pos, false) and TZero() != exprSign(bound)
}
/**
* Holds if there is a bound that might restrict whether `v` has the sign `s`
* at `pos`.
*/
private predicate hasGuard(SsaVariable v, SsaReadPosition pos, Sign s) {
s = TPos() and posBound(_, v, pos)
or
s = TNeg() and negBound(_, v, pos)
or
s = TZero() and zeroBound(_, v, pos)
}
pragma[noinline]
private Sign guardedSsaSign(SsaVariable v, SsaReadPosition pos) {
result = ssaDefSign(v) and
pos.hasReadOfVar(v) and
hasGuard(v, pos, result)
}
pragma[noinline]
private Sign unguardedSsaSign(SsaVariable v, SsaReadPosition pos) {
result = ssaDefSign(v) and
pos.hasReadOfVar(v) and
not hasGuard(v, pos, result)
}
private Sign guardedSsaSignOk(SsaVariable v, SsaReadPosition pos) {
result = TPos() and
forex(Expr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))
or
result = TNeg() and
forex(Expr bound | negBound(bound, v, pos) | negBoundOk(bound, v, pos))
or
result = TZero() and
forex(Expr bound | zeroBound(bound, v, pos) | zeroBoundOk(bound, v, pos))
}
/** Gets a possible sign for `v` at `pos`. */
private Sign ssaSign(SsaVariable v, SsaReadPosition pos) {
result = unguardedSsaSign(v, pos)
or
result = guardedSsaSign(v, pos) and
result = guardedSsaSignOk(v, pos)
}
/** Gets a possible sign for `v`. */
pragma[nomagic]
private Sign ssaDefSign(SsaVariable v) {
exists(VariableUpdate def | def = v.(SsaExplicitUpdate).getDefiningExpr() |
result = exprSign(def.(VariableAssign).getSource())
or
exists(EnhancedForStmt for | def = for.getVariable())
or
result = exprSign(def.(PostIncExpr).getExpr()).inc()
or
result = exprSign(def.(PreIncExpr).getExpr()).inc()
or
result = exprSign(def.(PostDecExpr).getExpr()).dec()
or
result = exprSign(def.(PreDecExpr).getExpr()).dec()
or
exists(AssignOp a | a = def and result = exprSign(a))
)
or
result = fieldSign(v.(SsaImplicitUpdate).getSourceVariable().getVariable())
or
result = fieldSign(v.(SsaImplicitInit).getSourceVariable().getVariable())
or
exists(Parameter p | v.(SsaImplicitInit).isParameterDefinition(p))
or
exists(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge |
v = phi and
edge.phiInput(phi, inp) and
result = ssaSign(inp, edge)
)
}
/** Gets a possible sign for `f`. */
private Sign fieldSign(Field f) {
result = exprSign(f.getAnAssignedValue())
or
exists(PostIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc())
or
exists(PreIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc())
or
exists(PostDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec())
or
exists(PreDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec())
or
exists(AssignOp a | a.getDest() = f.getAnAccess() | result = exprSign(a))
or
exists(ReflectiveFieldAccess rfa | rfa.inferAccessedField() = f)
or
if f.fromSource()
then not exists(f.getInitializer()) and result = TZero()
else
if f instanceof ArrayLengthField
then result != TNeg()
else
if f.hasName("MAX_VALUE")
then result = TPos()
else
if f.hasName("MIN_VALUE")
then result = TNeg()
else any()
}
/** Gets a possible sign for `e`. */
cached
private Sign exprSign(Expr e) {
result = certainExprSign(e)
or
not exists(certainExprSign(e)) and
(
unknownSign(e)
or
exists(SsaVariable v | v.getAUse() = e |
result = ssaSign(v, any(SsaReadPositionBlock bb | bb.getBlock() = e.getBasicBlock()))
or
not exists(e.getBasicBlock()) and result = ssaDefSign(v)
)
or
exists(FieldAccess fa | fa = e |
not exists(SsaVariable v | v.getAUse() = fa) and
result = fieldSign(fa.getField())
)
or
exists(VarAccess va | va = e |
not exists(SsaVariable v | v.getAUse() = va) and
not va instanceof FieldAccess
)
or
result = exprSign(e.(AssignExpr).getSource())
or
result = exprSign(e.(PlusExpr).getExpr())
or
result = exprSign(e.(PostIncExpr).getExpr())
or
result = exprSign(e.(PostDecExpr).getExpr())
or
result = exprSign(e.(PreIncExpr).getExpr()).inc()
or
result = exprSign(e.(PreDecExpr).getExpr()).dec()
or
result = exprSign(e.(MinusExpr).getExpr()).neg()
or
result = exprSign(e.(BitNotExpr).getExpr()).bitnot()
or
exists(DivExpr div |
div = e and
result = exprSign(div.getLeftOperand()) and
result != TZero()
|
div.getRightOperand().(FloatingPointLiteral).getValue().toFloat() = 0 or
div.getRightOperand().(DoubleLiteral).getValue().toFloat() = 0
)
or
exists(Sign s1, Sign s2 | binaryOpSigns(e, s1, s2) |
(e instanceof AssignAddExpr or e instanceof AddExpr) and
result = s1.add(s2)
or
(e instanceof AssignSubExpr or e instanceof SubExpr) and
result = s1.add(s2.neg())
or
(e instanceof AssignMulExpr or e instanceof MulExpr) and
result = s1.mul(s2)
or
(e instanceof AssignDivExpr or e instanceof DivExpr) and
result = s1.div(s2)
or
(e instanceof AssignRemExpr or e instanceof RemExpr) and
result = s1.rem(s2)
or
(e instanceof AssignAndExpr or e instanceof AndBitwiseExpr) and
result = s1.bitand(s2)
or
(e instanceof AssignOrExpr or e instanceof OrBitwiseExpr) and
result = s1.bitor(s2)
or
(e instanceof AssignXorExpr or e instanceof XorBitwiseExpr) and
result = s1.bitxor(s2)
or
(e instanceof AssignLShiftExpr or e instanceof LShiftExpr) and
result = s1.lshift(s2)
or
(e instanceof AssignRShiftExpr or e instanceof RShiftExpr) and
result = s1.rshift(s2)
or
(e instanceof AssignURShiftExpr or e instanceof URShiftExpr) and
result = s1.urshift(s2)
)
or
result = exprSign(e.(ChooseExpr).getAResultExpr())
or
result = exprSign(e.(CastExpr).getExpr())
)
}
private Sign binaryOpLhsSign(Expr e) {
result = exprSign(e.(BinaryExpr).getLeftOperand()) or
result = exprSign(e.(AssignOp).getDest())
}
private Sign binaryOpRhsSign(Expr e) {
result = exprSign(e.(BinaryExpr).getRightOperand()) or
result = exprSign(e.(AssignOp).getRhs())
}
pragma[noinline]
private predicate binaryOpSigns(Expr e, Sign lhs, Sign rhs) {
lhs = binaryOpLhsSign(e) and
rhs = binaryOpRhsSign(e)
}
/** Holds if `e` can be positive and cannot be negative. */
predicate positive(Expr e) {
exprSign(e) = TPos() and
not exprSign(e) = TNeg()
}
/** Holds if `e` can be negative and cannot be positive. */
predicate negative(Expr e) {
exprSign(e) = TNeg() and
not exprSign(e) = TPos()
}
/** Holds if `e` is strictly positive. */
predicate strictlyPositive(Expr e) {
exprSign(e) = TPos() and
not exprSign(e) = TNeg() and
not exprSign(e) = TZero()
}
/** Holds if `e` is strictly negative. */
predicate strictlyNegative(Expr e) {
exprSign(e) = TNeg() and
not exprSign(e) = TPos() and
not exprSign(e) = TZero()
}
import semmle.code.java.dataflow.internal.rangeanalysis.SignAnalysisCommon

219
java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/Sign.qll Normal file
View File

@@ -0,0 +1,219 @@
newtype TSign =
TNeg() or
TZero() or
TPos()
/** Class representing expression signs (+, -, 0). */
class Sign extends TSign {
/** Gets the string representation of this sign. */
string toString() {
result = "-" and this = TNeg()
or
result = "0" and this = TZero()
or
result = "+" and this = TPos()
}
/** Gets a possible sign after incrementing an expression that has this sign. */
Sign inc() {
this = TNeg() and result = TNeg()
or
this = TNeg() and result = TZero()
or
this = TZero() and result = TPos()
or
this = TPos() and result = TPos()
}
/** Gets a possible sign after decrementing an expression that has this sign. */
Sign dec() { result.inc() = this }
/** Gets a possible sign after negating an expression that has this sign. */
Sign neg() {
this = TNeg() and result = TPos()
or
this = TZero() and result = TZero()
or
this = TPos() and result = TNeg()
}
/**
* Gets a possible sign after bitwise complementing an expression that has this
* sign.
*/
Sign bitnot() {
this = TNeg() and result = TPos()
or
this = TNeg() and result = TZero()
or
this = TZero() and result = TNeg()
or
this = TPos() and result = TNeg()
}
/**
* Gets a possible sign after adding an expression with sign `s` to an expression
* that has this sign.
*/
Sign add(Sign s) {
this = TZero() and result = s
or
s = TZero() and result = this
or
this = s and this = result
or
this = TPos() and s = TNeg()
or
this = TNeg() and s = TPos()
}
/**
* Gets a possible sign after multiplying an expression with sign `s` to an expression
* that has this sign.
*/
Sign mul(Sign s) {
result = TZero() and this = TZero()
or
result = TZero() and s = TZero()
or
result = TNeg() and this = TPos() and s = TNeg()
or
result = TNeg() and this = TNeg() and s = TPos()
or
result = TPos() and this = TPos() and s = TPos()
or
result = TPos() and this = TNeg() and s = TNeg()
}
/**
* Gets a possible sign after integer dividing an expression that has this sign
* by an expression with sign `s`.
*/
Sign div(Sign s) {
result = TZero() and s = TNeg() // ex: 3 / -5 = 0
or
result = TZero() and s = TPos() // ex: 3 / 5 = 0
or
result = TNeg() and this = TPos() and s = TNeg()
or
result = TNeg() and this = TNeg() and s = TPos()
or
result = TPos() and this = TPos() and s = TPos()
or
result = TPos() and this = TNeg() and s = TNeg()
}
/**
* Gets a possible sign after modulo dividing an expression that has this sign
* by an expression with sign `s`.
*/
Sign rem(Sign s) {
result = TZero() and s = TNeg()
or
result = TZero() and s = TPos()
or
result = this and s = TNeg()
or
result = this and s = TPos()
}
/**
* Gets a possible sign after bitwise `and` of an expression that has this sign
* and an expression with sign `s`.
*/
Sign bitand(Sign s) {
result = TZero() and this = TZero()
or
result = TZero() and s = TZero()
or
result = TZero() and this = TPos()
or
result = TZero() and s = TPos()
or
result = TNeg() and this = TNeg() and s = TNeg()
or
result = TPos() and this = TNeg() and s = TPos()
or
result = TPos() and this = TPos() and s = TNeg()
or
result = TPos() and this = TPos() and s = TPos()
}
/**
* Gets a possible sign after bitwise `or` of an expression that has this sign
* and an expression with sign `s`.
*/
Sign bitor(Sign s) {
result = TZero() and this = TZero() and s = TZero()
or
result = TNeg() and this = TNeg()
or
result = TNeg() and s = TNeg()
or
result = TPos() and this = TPos() and s = TZero()
or
result = TPos() and this = TZero() and s = TPos()
or
result = TPos() and this = TPos() and s = TPos()
}
/**
* Gets a possible sign after bitwise `xor` of an expression that has this sign
* and an expression with sign `s`.
*/
Sign bitxor(Sign s) {
result = TZero() and this = s
or
result = this and s = TZero()
or
result = s and this = TZero()
or
result = TPos() and this = TPos() and s = TPos()
or
result = TNeg() and this = TNeg() and s = TPos()
or
result = TNeg() and this = TPos() and s = TNeg()
or
result = TPos() and this = TNeg() and s = TNeg()
}
/**
* Gets a possible sign after left shift of an expression that has this sign
* by an expression with sign `s`.
*/
Sign lshift(Sign s) {
result = TZero() and this = TZero()
or
result = this and s = TZero()
or
this != TZero() and s != TZero()
}
/**
* Gets a possible sign after right shift of an expression that has this sign
* by an expression with sign `s`.
*/
Sign rshift(Sign s) {
result = TZero() and this = TZero()
or
result = this and s = TZero()
or
result = TNeg() and this = TNeg()
or
result != TNeg() and this = TPos() and s != TZero()
}
/**
* Gets a possible sign after unsigned right shift of an expression that has
* this sign by an expression with sign `s`.
*/
Sign urshift(Sign s) {
result = TZero() and this = TZero()
or
result = this and s = TZero()
or
result != TZero() and this = TNeg() and s != TZero()
or
result != TNeg() and this = TPos() and s != TZero()
}
}

293
java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisCommon.qll Normal file
View File

@@ -0,0 +1,293 @@
/**
* Provides sign analysis to determine whether expression are always positive
* or negative.
*
* The analysis is implemented as an abstract interpretation over the
* three-valued domain `{negative, zero, positive}`.
*/
private import SignAnalysisSpecific::Private
private import SsaReadPositionCommon
private import Sign
/** Gets the sign of `e` if this can be directly determined. */
Sign certainExprSign(Expr e) {
exists(int i | e.(ConstantIntegerExpr).getIntValue() = i |
i < 0 and result = TNeg()
or
i = 0 and result = TZero()
or
i > 0 and result = TPos()
)
or
not exists(e.(ConstantIntegerExpr).getIntValue()) and
(
exists(float f | f = getNonIntegerValue(e) |
f < 0 and result = TNeg()
or
f = 0 and result = TZero()
or
f > 0 and result = TPos()
)
or
exists(string charlit | charlit = getCharValue(e) |
if charlit.regexpMatch("\\u0000") then result = TZero() else result = TPos()
)
or
containerSizeAccess(e) and
(result = TPos() or result = TZero())
or
positiveExpression(e) and result = TPos()
)
}
/** Holds if the sign of `e` is too complicated to determine. */
predicate unknownSign(Expr e) {
not exists(certainExprSign(e)) and
(
exists(IntegerLiteral lit | lit = e and not exists(lit.getValue().toInt()))
or
exists(LongLiteral lit | lit = e and not exists(lit.getValue().toFloat()))
or
exists(CastExpr cast, Type fromtyp |
cast = e and
fromtyp = cast.getExpr().getType() and
not fromtyp instanceof NumericOrCharType
)
or
unknownIntegerAccess(e)
)
}
/**
* Holds if `lowerbound` is a lower bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate lowerBound(Expr lowerbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) {
exists(boolean testIsTrue, ComparisonExpr comp |
pos.hasReadOfVar(v) and
guardControlsSsaRead(getComparisonGuard(comp), pos, testIsTrue) and
not unknownSign(lowerbound)
|
testIsTrue = true and
comp.getLesserOperand() = lowerbound and
comp.getGreaterOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = true else isStrict = false)
or
testIsTrue = false and
comp.getGreaterOperand() = lowerbound and
comp.getLesserOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
/**
* Holds if `upperbound` is an upper bound for `v` at `pos`. This is restricted
* to only include bounds for which we might determine a sign.
*/
private predicate upperBound(Expr upperbound, SsaVariable v, SsaReadPosition pos, boolean isStrict) {
exists(boolean testIsTrue, ComparisonExpr comp |
pos.hasReadOfVar(v) and
guardControlsSsaRead(getComparisonGuard(comp), pos, testIsTrue) and
not unknownSign(upperbound)
|
testIsTrue = true and
comp.getGreaterOperand() = upperbound and
comp.getLesserOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = true else isStrict = false)
or
testIsTrue = false and
comp.getLesserOperand() = upperbound and
comp.getGreaterOperand() = ssaRead(v, 0) and
(if comp.isStrict() then isStrict = false else isStrict = true)
)
}
/**
* Holds if `eqbound` is an equality/inequality for `v` at `pos`. This is
* restricted to only include bounds for which we might determine a sign. The
* boolean `isEq` gives the polarity:
* - `isEq = true` : `v = eqbound`
* - `isEq = false` : `v != eqbound`
*/
private predicate eqBound(Expr eqbound, SsaVariable v, SsaReadPosition pos, boolean isEq) {
exists(Guard guard, boolean testIsTrue, boolean polarity |
pos.hasReadOfVar(v) and
guardControlsSsaRead(guard, pos, testIsTrue) and
guard.isEquality(eqbound, ssaRead(v, 0), polarity) and
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
not unknownSign(eqbound)
)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
* order for `v` to be positive.
*/
private predicate posBound(Expr bound, SsaVariable v, SsaReadPosition pos) {
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
* order for `v` to be negative.
*/
private predicate negBound(Expr bound, SsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
eqBound(bound, v, pos, true)
}
/**
* Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
* can be zero.
*/
private predicate zeroBound(Expr bound, SsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) or
upperBound(bound, v, pos, _) or
eqBound(bound, v, pos, _)
}
/** Holds if `bound` allows `v` to be positive at `pos`. */
private predicate posBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) {
posBound(bound, v, pos) and TPos() = exprSign(bound)
}
/** Holds if `bound` allows `v` to be negative at `pos`. */
private predicate negBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) {
negBound(bound, v, pos) and TNeg() = exprSign(bound)
}
/** Holds if `bound` allows `v` to be zero at `pos`. */
private predicate zeroBoundOk(Expr bound, SsaVariable v, SsaReadPosition pos) {
lowerBound(bound, v, pos, _) and TNeg() = exprSign(bound)
or
lowerBound(bound, v, pos, false) and TZero() = exprSign(bound)
or
upperBound(bound, v, pos, _) and TPos() = exprSign(bound)
or
upperBound(bound, v, pos, false) and TZero() = exprSign(bound)
or
eqBound(bound, v, pos, true) and TZero() = exprSign(bound)
or
eqBound(bound, v, pos, false) and TZero() != exprSign(bound)
}
/**
* Holds if there is a bound that might restrict whether `v` has the sign `s`
* at `pos`.
*/
private predicate hasGuard(SsaVariable v, SsaReadPosition pos, Sign s) {
s = TPos() and posBound(_, v, pos)
or
s = TNeg() and negBound(_, v, pos)
or
s = TZero() and zeroBound(_, v, pos)
}
pragma[noinline]
private Sign guardedSsaSign(SsaVariable v, SsaReadPosition pos) {
// SSA variable can have sign `result`
result = ssaDefSign(v) and
pos.hasReadOfVar(v) and
// there are guards at this position on `v` that might restrict it to be sign `result`.
// (So we need to check if they are satisfied)
hasGuard(v, pos, result)
}
pragma[noinline]
private Sign unguardedSsaSign(SsaVariable v, SsaReadPosition pos) {
// SSA variable can have sign `result`
result = ssaDefSign(v) and
pos.hasReadOfVar(v) and
// there's no guard at this position on `v` that might restrict it to be sign `result`.
not hasGuard(v, pos, result)
}
/**
* Gets the sign of `v` at read position `pos`, when there's at least one guard
* on `v` at position `pos`. Each bound corresponding to a given sign must be met
* in order for `v` to be of that sign.
*/
private Sign guardedSsaSignOk(SsaVariable v, SsaReadPosition pos) {
result = TPos() and
forex(Expr bound | posBound(bound, v, pos) | posBoundOk(bound, v, pos))
or
result = TNeg() and
forex(Expr bound | negBound(bound, v, pos) | negBoundOk(bound, v, pos))
or
result = TZero() and
forex(Expr bound | zeroBound(bound, v, pos) | zeroBoundOk(bound, v, pos))
}
/** Gets a possible sign for `v` at `pos`. */
Sign ssaSign(SsaVariable v, SsaReadPosition pos) {
result = unguardedSsaSign(v, pos)
or
result = guardedSsaSign(v, pos) and
result = guardedSsaSignOk(v, pos)
}
/** Gets a possible sign for `v`. */
pragma[nomagic]
Sign ssaDefSign(SsaVariable v) {
result = explicitSsaDefSign(v)
or
result = implicitSsaDefSign(v)
or
exists(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge |
v = phi and
edge.phiInput(phi, inp) and
result = ssaSign(inp, edge)
)
}
/** Gets a possible sign for `e`. */
cached
Sign exprSign(Expr e) {
result = certainExprSign(e)
or
not exists(certainExprSign(e)) and
(
unknownSign(e)
or
exists(SsaVariable v | getARead(v) = e | result = ssaVariableSign(v, e))
or
e =
any(VarAccess access |
not exists(SsaVariable v | getARead(v) = access) and
(
result = fieldSign(getField(access.(FieldAccess))) or
not access instanceof FieldAccess
)
)
or
result = specificSubExprSign(e)
)
}
/** Holds if `e` can be positive and cannot be negative. */
predicate positive(Expr e) {
exprSign(e) = TPos() and
not exprSign(e) = TNeg()
}
/** Holds if `e` can be negative and cannot be positive. */
predicate negative(Expr e) {
exprSign(e) = TNeg() and
not exprSign(e) = TPos()
}
/** Holds if `e` is strictly positive. */
predicate strictlyPositive(Expr e) {
exprSign(e) = TPos() and
not exprSign(e) = TNeg() and
not exprSign(e) = TZero()
}
/** Holds if `e` is strictly negative. */
predicate strictlyNegative(Expr e) {
exprSign(e) = TNeg() and
not exprSign(e) = TPos() and
not exprSign(e) = TZero()
}

235
java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll Normal file
View File

@@ -0,0 +1,235 @@
/**
* Provides Java-specific definitions for use in sign analysis.
*/
module Private {
import semmle.code.java.dataflow.RangeUtils as RU
private import semmle.code.java.dataflow.SSA as Ssa
private import semmle.code.java.controlflow.Guards as G
private import java as J
import Impl
class ConstantIntegerExpr = RU::ConstantIntegerExpr;
class Guard = G::Guard;
class SsaVariable = Ssa::SsaVariable;
class SsaPhiNode = Ssa::SsaPhiNode;
class VarAccess = J::VarAccess;
class FieldAccess = J::FieldAccess;
class CharacterLiteral = J::CharacterLiteral;
class IntegerLiteral = J::IntegerLiteral;
class LongLiteral = J::LongLiteral;
class CastExpr = J::CastExpr;
class Type = J::Type;
class Expr = J::Expr;
class ComparisonExpr = J::ComparisonExpr;
class NumericOrCharType = J::NumericOrCharType;
predicate ssaRead = RU::ssaRead/2;
predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
}
private module Impl {
private import java
private import semmle.code.java.dataflow.RangeUtils
private import semmle.code.java.dataflow.SSA
private import semmle.code.java.controlflow.Guards
private import semmle.code.java.Reflection
private import semmle.code.java.Collections
private import semmle.code.java.Maps
private import Sign
private import SignAnalysisCommon
private import SsaReadPositionCommon
float getNonIntegerValue(Expr e) {
result = e.(LongLiteral).getValue().toFloat() or
result = e.(FloatingPointLiteral).getValue().toFloat() or
result = e.(DoubleLiteral).getValue().toFloat()
}
string getCharValue(Expr e) { result = e.(CharacterLiteral).getValue() }
predicate containerSizeAccess(Expr e) {
e.(MethodAccess).getMethod() instanceof StringLengthMethod
or
e.(MethodAccess).getMethod() instanceof CollectionSizeMethod
or
e.(MethodAccess).getMethod() instanceof MapSizeMethod
}
predicate positiveExpression(Expr e) { none() }
predicate unknownIntegerAccess(Expr e) {
e instanceof ArrayAccess and e.getType() instanceof NumericOrCharType
or
e instanceof MethodAccess and e.getType() instanceof NumericOrCharType
or
e instanceof ClassInstanceExpr and e.getType() instanceof NumericOrCharType
}
Sign explicitSsaDefSign(SsaVariable v) {
exists(VariableUpdate def | def = v.(SsaExplicitUpdate).getDefiningExpr() |
result = exprSign(def.(VariableAssign).getSource())
or
exists(EnhancedForStmt for | def = for.getVariable())
or
result = exprSign(def.(PostIncExpr).getExpr()).inc()
or
result = exprSign(def.(PreIncExpr).getExpr()).inc()
or
result = exprSign(def.(PostDecExpr).getExpr()).dec()
or
result = exprSign(def.(PreDecExpr).getExpr()).dec()
or
exists(AssignOp a | a = def and result = exprSign(a))
)
}
Sign implicitSsaDefSign(SsaVariable v) {
result = fieldSign(v.(SsaImplicitUpdate).getSourceVariable().getVariable())
or
result = fieldSign(v.(SsaImplicitInit).getSourceVariable().getVariable())
or
exists(Parameter p | v.(SsaImplicitInit).isParameterDefinition(p))
}
pragma[inline]
Sign ssaVariableSign(SsaVariable v, Expr e) {
result = ssaSign(v, any(SsaReadPositionBlock bb | getAnExpression(bb) = e))
or
not exists(SsaReadPositionBlock bb | getAnExpression(bb) = e) and
result = ssaDefSign(v)
}
/** Gets a possible sign for `f`. */
Sign fieldSign(Field f) {
result = exprSign(f.getAnAssignedValue())
or
exists(PostIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc())
or
exists(PreIncExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).inc())
or
exists(PostDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec())
or
exists(PreDecExpr inc | inc.getExpr() = f.getAnAccess() and result = fieldSign(f).dec())
or
exists(AssignOp a | a.getDest() = f.getAnAccess() | result = exprSign(a))
or
exists(ReflectiveFieldAccess rfa | rfa.inferAccessedField() = f)
or
if f.fromSource()
then not exists(f.getInitializer()) and result = TZero()
else
if f instanceof ArrayLengthField
then result != TNeg()
else
if f.hasName("MAX_VALUE")
then result = TPos()
else
if f.hasName("MIN_VALUE")
then result = TNeg()
else any()
}
Sign specificSubExprSign(Expr e) {
result = exprSign(e.(AssignExpr).getSource())
or
result = exprSign(e.(PlusExpr).getExpr())
or
result = exprSign(e.(PostIncExpr).getExpr())
or
result = exprSign(e.(PostDecExpr).getExpr())
or
result = exprSign(e.(PreIncExpr).getExpr()).inc()
or
result = exprSign(e.(PreDecExpr).getExpr()).dec()
or
result = exprSign(e.(MinusExpr).getExpr()).neg()
or
result = exprSign(e.(BitNotExpr).getExpr()).bitnot()
or
exists(DivExpr div |
div = e and
result = exprSign(div.getLeftOperand()) and
result != TZero()
|
div.getRightOperand().(FloatingPointLiteral).getValue().toFloat() = 0 or
div.getRightOperand().(DoubleLiteral).getValue().toFloat() = 0
)
or
exists(Sign s1, Sign s2 | binaryOpSigns(e, s1, s2) |
(e instanceof AssignAddExpr or e instanceof AddExpr) and
result = s1.add(s2)
or
(e instanceof AssignSubExpr or e instanceof SubExpr) and
result = s1.add(s2.neg())
or
(e instanceof AssignMulExpr or e instanceof MulExpr) and
result = s1.mul(s2)
or
(e instanceof AssignDivExpr or e instanceof DivExpr) and
result = s1.div(s2)
or
(e instanceof AssignRemExpr or e instanceof RemExpr) and
result = s1.rem(s2)
or
(e instanceof AssignAndExpr or e instanceof AndBitwiseExpr) and
result = s1.bitand(s2)
or
(e instanceof AssignOrExpr or e instanceof OrBitwiseExpr) and
result = s1.bitor(s2)
or
(e instanceof AssignXorExpr or e instanceof XorBitwiseExpr) and
result = s1.bitxor(s2)
or
(e instanceof AssignLShiftExpr or e instanceof LShiftExpr) and
result = s1.lshift(s2)
or
(e instanceof AssignRShiftExpr or e instanceof RShiftExpr) and
result = s1.rshift(s2)
or
(e instanceof AssignURShiftExpr or e instanceof URShiftExpr) and
result = s1.urshift(s2)
)
or
result = exprSign(e.(ChooseExpr).getAResultExpr())
or
result = exprSign(e.(CastExpr).getExpr())
}
private Sign binaryOpLhsSign(Expr e) {
result = exprSign(e.(BinaryExpr).getLeftOperand()) or
result = exprSign(e.(AssignOp).getDest())
}
private Sign binaryOpRhsSign(Expr e) {
result = exprSign(e.(BinaryExpr).getRightOperand()) or
result = exprSign(e.(AssignOp).getRhs())
}
pragma[noinline]
private predicate binaryOpSigns(Expr e, Sign lhs, Sign rhs) {
lhs = binaryOpLhsSign(e) and
rhs = binaryOpRhsSign(e)
}
Expr getARead(SsaVariable v) { result = v.getAUse() }
Field getField(FieldAccess fa) { result = fa.getField() }
Expr getAnExpression(SsaReadPositionBlock bb) { result = bb.getBlock().getANode() }
Guard getComparisonGuard(ComparisonExpr ce) { result = ce }
}

57
java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll Normal file
View File

@@ -0,0 +1,57 @@
/**
* Provides classes for representing a position at which an SSA variable is read.
*/
private import SsaReadPositionSpecific
private newtype TSsaReadPosition =
TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or
TSsaReadPositionPhiInputEdge(BasicBlock bbOrig, BasicBlock bbPhi) {
exists(SsaPhiNode phi | phi.hasInputFromBlock(_, bbOrig) and bbPhi = phi.getBasicBlock())
}
/**
* A position at which an SSA variable is read. This includes both ordinary
* reads occurring in basic blocks and input to phi nodes occurring along an
* edge between two basic blocks.
*/
class SsaReadPosition extends TSsaReadPosition {
/** Holds if `v` is read at this position. */
abstract predicate hasReadOfVar(SsaVariable v);
/** Gets a textual representation of this SSA read position. */
abstract string toString();
}
/** A basic block in which an SSA variable is read. */
class SsaReadPositionBlock extends SsaReadPosition, TSsaReadPositionBlock {
/** Gets the basic block corresponding to this position. */
BasicBlock getBlock() { this = TSsaReadPositionBlock(result) }
override predicate hasReadOfVar(SsaVariable v) { getBlock() = getAReadBasicBlock(v) }
override string toString() { result = "block" }
}
/**
* An edge between two basic blocks where the latter block has an SSA phi
* definition. The edge therefore has a read of an SSA variable serving as the
* input to the phi node.
*/
class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiInputEdge {
/** Gets the source of the edge. */
BasicBlock getOrigBlock() { this = TSsaReadPositionPhiInputEdge(result, _) }
/** Gets the target of the edge. */
BasicBlock getPhiBlock() { this = TSsaReadPositionPhiInputEdge(_, result) }
override predicate hasReadOfVar(SsaVariable v) { this.phiInput(_, v) }
/** Holds if `inp` is an input to `phi` along this edge. */
predicate phiInput(SsaPhiNode phi, SsaVariable inp) {
phi.hasInputFromBlock(inp, getOrigBlock()) and
getPhiBlock() = phi.getBasicBlock()
}
override string toString() { result = "edge" }
}

15
java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll Normal file
View File

@@ -0,0 +1,15 @@
/**
* Provides Java-specific definitions for use in the `SsaReadPosition`.
*/
private import semmle.code.java.dataflow.SSA as Ssa
private import semmle.code.java.controlflow.BasicBlocks as BB
class SsaVariable = Ssa::SsaVariable;
class SsaPhiNode = Ssa::SsaPhiNode;
class BasicBlock = BB::BasicBlock;
/** Gets a basic block in which SSA variable `v` is read. */
BasicBlock getAReadBasicBlock(SsaVariable v) { result = v.getAUse().getBasicBlock() }