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

Merge pull request #12683 from aschackmull/java/rangeanalysis-add

Browse Source 
Java: Support double-recursive range analysis bounds for addition.
This commit is contained in:
Anders Schack-Mulligen
2023-03-29 13:39:59 +02:00
committed by GitHub
parent 0acca2ba76 7844384768
commit d0fa7c7ff8
3 changed files with 105 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
java/ql/lib/change-notes/2023-03-29-rangeanalysis-add.md Normal file
View File

@@ -0,0 +1,4 @@
---
category: minorAnalysis
---
* Improved the handling of addition in the range analysis. This can cause in minor changes to the results produced by `java/index-out-of-bounds` and `java/constant-comparison`.

74
java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll
View File

@@ -421,32 +421,6 @@ private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
delta = 0 and
(upper = true or upper = false)
or
exists(Expr x |
e2.(AddExpr).hasOperands(e1, x)
or
exists(AssignAddExpr add | add = e2 |
add.getDest() = e1 and add.getRhs() = x
or
add.getDest() = x and add.getRhs() = e1
)
|
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
not x instanceof ConstantIntegerExpr and
not e1 instanceof ConstantIntegerExpr and
if strictlyPositiveIntegralExpr(x)
then upper = false and delta = 1
else
if positive(x)
then upper = false and delta = 0
else
if strictlyNegativeIntegralExpr(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
@@ -896,6 +870,20 @@ private predicate bounded(
or
upper = false and delta = d1.minimum(d2)
)
or
exists(
Bound b1, Bound b2, int d1, int d2, boolean fbe1, boolean fbe2, int od1, int od2, Reason r1,
Reason r2
|
boundedAddition(e, upper, b1, true, d1, fbe1, od1, r1) and
boundedAddition(e, upper, b2, false, d2, fbe2, od2, r2) and
delta = d1 + d2 and
fromBackEdge = fbe1.booleanOr(fbe2)
|
b = b1 and origdelta = od1 and reason = r1 and b2 instanceof ZeroBound
or
b = b2 and origdelta = od2 and reason = r2 and b1 instanceof ZeroBound
)
}
private predicate boundedConditionalExpr(
@@ -904,3 +892,37 @@ private predicate boundedConditionalExpr(
) {
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
}
private predicate nonConstAdd(Expr add, Expr operand, boolean isLeft) {
exists(Expr other |
add.(AddExpr).getLeftOperand() = operand and
add.(AddExpr).getRightOperand() = other and
isLeft = true
or
add.(AddExpr).getLeftOperand() = other and
add.(AddExpr).getRightOperand() = operand and
isLeft = false
or
add.(AssignAddExpr).getDest() = operand and
add.(AssignAddExpr).getRhs() = other and
isLeft = true
or
add.(AssignAddExpr).getDest() = other and
add.(AssignAddExpr).getRhs() = operand and
isLeft = false
|
// `ConstantIntegerExpr` is covered by valueFlowStep
not other instanceof ConstantIntegerExpr and
not operand instanceof ConstantIntegerExpr
)
}
private predicate boundedAddition(
Expr add, boolean upper, Bound b, boolean isLeft, int delta, boolean fromBackEdge, int origdelta,
Reason reason
) {
exists(Expr op |
nonConstAdd(add, op, isLeft) and
bounded(op, b, delta, upper, fromBackEdge, origdelta, reason)
)
}

67
java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected
View File

@@ -33,9 +33,17 @@
| A.java:9:16:9:16 | x | SSA init(x) | 0 | upper | NoReason |
| A.java:9:16:9:16 | x | SSA init(y) | -2 | lower | ... == ... |
| A.java:9:16:9:16 | x | SSA init(y) | -2 | upper | ... == ... |
| A.java:9:16:9:20 | ... + ... | 0 | 300 | lower | ... > ... |
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 1 | lower | NoReason |
| A.java:9:16:9:20 | ... + ... | SSA init(y) | -1 | lower | ... == ... |
| A.java:9:16:9:20 | ... + ... | 0 | 600 | lower | ... > ... |
| A.java:9:16:9:20 | ... + ... | 0 | 802 | upper | ... == ... |
| A.java:9:16:9:20 | ... + ... | 0 | 802 | upper | ... > ... |
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 301 | lower | ... == ... |
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 301 | lower | NoReason |
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 402 | upper | ... == ... |
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 402 | upper | NoReason |
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 299 | lower | ... == ... |
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 299 | lower | NoReason |
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 400 | upper | ... == ... |
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 400 | upper | NoReason |
| A.java:9:20:9:20 | y | 0 | 301 | lower | ... > ... |
| A.java:9:20:9:20 | y | 0 | 402 | upper | ... == ... |
| A.java:9:20:9:20 | y | SSA init(x) | 2 | lower | ... == ... |
@@ -54,6 +62,7 @@
| A.java:13:19:13:19 | x | 0 | 400 | upper | ... > ... |
| A.java:13:19:13:19 | x | SSA init(x) | 0 | lower | NoReason |
| A.java:13:19:13:19 | x | SSA init(x) | 0 | upper | NoReason |
| A.java:13:19:13:23 | ... + ... | SSA init(y) | 400 | upper | NoReason |
| A.java:13:23:13:23 | y | SSA init(y) | 0 | lower | NoReason |
| A.java:13:23:13:23 | y | SSA init(y) | 0 | upper | NoReason |
| A.java:15:13:15:13 | y | 0 | 399 | upper | ... != ... |
@@ -69,9 +78,17 @@
| A.java:16:21:16:21 | x | SSA init(x) | 0 | upper | NoReason |
| A.java:16:21:16:21 | x | SSA init(y) | 1 | lower | ... != ... |
| A.java:16:21:16:21 | x | SSA init(y) | 1 | upper | ... != ... |
| A.java:16:21:16:25 | ... + ... | 0 | 303 | lower | ... > ... |
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 1 | lower | NoReason |
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 2 | lower | ... != ... |
| A.java:16:21:16:25 | ... + ... | 0 | 603 | lower | ... > ... |
| A.java:16:21:16:25 | ... + ... | 0 | 799 | upper | ... != ... |
| A.java:16:21:16:25 | ... + ... | 0 | 799 | upper | ... > ... |
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 301 | lower | ... != ... |
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 301 | lower | NoReason |
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 399 | upper | ... != ... |
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 399 | upper | NoReason |
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 302 | lower | ... != ... |
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 302 | lower | NoReason |
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 400 | upper | ... != ... |
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 400 | upper | NoReason |
| A.java:16:25:16:25 | y | 0 | 301 | lower | ... > ... |
| A.java:16:25:16:25 | y | 0 | 399 | upper | ... != ... |
| A.java:16:25:16:25 | y | SSA init(x) | -1 | lower | ... != ... |
@@ -153,14 +170,36 @@
| A.java:35:16:35:16 | x | SSA init(y) | 1 | upper | ... == ... |
| A.java:35:16:35:16 | x | SSA init(z) | -1 | lower | ... == ... |
| A.java:35:16:35:16 | x | SSA init(z) | -1 | upper | ... == ... |
| A.java:35:16:35:20 | ... + ... | 0 | 350 | lower | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 1 | lower | NoReason |
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 2 | lower | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(z) | 0 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | 0 | 351 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 2 | lower | NoReason |
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 3 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 1 | lower | ... == ... |
| A.java:35:16:35:20 | ... + ... | 0 | 697 | lower | ... == ... |
| A.java:35:16:35:20 | ... + ... | 0 | 697 | upper | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | lower | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | lower | NoReason |
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | upper | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | upper | NoReason |
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | lower | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | lower | NoReason |
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | upper | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | upper | NoReason |
| A.java:35:16:35:20 | ... + ... | SSA init(z) | 347 | lower | ... == ... |
| A.java:35:16:35:20 | ... + ... | SSA init(z) | 347 | upper | ... == ... |
| A.java:35:16:35:24 | ... + ... | 0 | 1047 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | 0 | 1047 | upper | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | lower | NoReason |
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | upper | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | upper | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | upper | NoReason |
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | lower | NoReason |
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | upper | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | upper | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | upper | NoReason |
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | lower | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | lower | NoReason |
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | upper | ... == ... |
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | upper | NoReason |
| A.java:35:20:35:20 | y | 0 | 348 | lower | ... == ... |
| A.java:35:20:35:20 | y | 0 | 348 | upper | ... == ... |
| A.java:35:20:35:20 | y | SSA init(x) | -1 | lower | ... == ... |