Skip to content

Commit d0fa7c7

Browse files
aschackmullaschackmull
authored
Merge pull request github#12683 from aschackmull/java/rangeanalysis-add
Java: Support double-recursive range analysis bounds for addition.
2 parents 0acca2b + 7844384 commit d0fa7c7

File tree

3 files changed

+105
-40
lines changed

3 files changed

+105
-40
lines changed

‎java/ql/lib/change-notes/2023-03-29-rangeanalysis-add.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
---
2+
category: minorAnalysis
3+
---
4+
* 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`.

‎java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

Lines changed: 48 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -421,32 +421,6 @@ private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
421421
delta = 0 and
422422
(upper = true or upper = false)
423423
or
424-
exists(Expr x |
425-
e2.(AddExpr).hasOperands(e1, x)
426-
or
427-
exists(AssignAddExpr add | add = e2 |
428-
add.getDest() = e1 and add.getRhs() = x
429-
or
430-
add.getDest() = x and add.getRhs() = e1
431-
)
432-
|
433-
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
434-
not x instanceof ConstantIntegerExpr and
435-
not e1 instanceof ConstantIntegerExpr and
436-
if strictlyPositiveIntegralExpr(x)
437-
then upper = false and delta = 1
438-
else
439-
if positive(x)
440-
then upper = false and delta = 0
441-
else
442-
if strictlyNegativeIntegralExpr(x)
443-
then upper = true and delta = -1
444-
else
445-
if negative(x)
446-
then upper = true and delta = 0
447-
else none()
448-
)
449-
or
450424
exists(Expr x |
451425
exists(SubExpr sub |
452426
e2 = sub and
@@ -896,6 +870,20 @@ private predicate bounded(
896870
or
897871
upper = false and delta = d1.minimum(d2)
898872
)
873+
or
874+
exists(
875+
Bound b1, Bound b2, int d1, int d2, boolean fbe1, boolean fbe2, int od1, int od2, Reason r1,
876+
Reason r2
877+
|
878+
boundedAddition(e, upper, b1, true, d1, fbe1, od1, r1) and
879+
boundedAddition(e, upper, b2, false, d2, fbe2, od2, r2) and
880+
delta = d1 + d2 and
881+
fromBackEdge = fbe1.booleanOr(fbe2)
882+
|
883+
b = b1 and origdelta = od1 and reason = r1 and b2 instanceof ZeroBound
884+
or
885+
b = b2 and origdelta = od2 and reason = r2 and b1 instanceof ZeroBound
886+
)
899887
}
900888

901889
private predicate boundedConditionalExpr(
@@ -904,3 +892,37 @@ private predicate boundedConditionalExpr(
904892
) {
905893
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
906894
}
895+
896+
private predicate nonConstAdd(Expr add, Expr operand, boolean isLeft) {
897+
exists(Expr other |
898+
add.(AddExpr).getLeftOperand() = operand and
899+
add.(AddExpr).getRightOperand() = other and
900+
isLeft = true
901+
or
902+
add.(AddExpr).getLeftOperand() = other and
903+
add.(AddExpr).getRightOperand() = operand and
904+
isLeft = false
905+
or
906+
add.(AssignAddExpr).getDest() = operand and
907+
add.(AssignAddExpr).getRhs() = other and
908+
isLeft = true
909+
or
910+
add.(AssignAddExpr).getDest() = other and
911+
add.(AssignAddExpr).getRhs() = operand and
912+
isLeft = false
913+
|
914+
// `ConstantIntegerExpr` is covered by valueFlowStep
915+
not other instanceof ConstantIntegerExpr and
916+
not operand instanceof ConstantIntegerExpr
917+
)
918+
}
919+
920+
private predicate boundedAddition(
921+
Expr add, boolean upper, Bound b, boolean isLeft, int delta, boolean fromBackEdge, int origdelta,
922+
Reason reason
923+
) {
924+
exists(Expr op |
925+
nonConstAdd(add, op, isLeft) and
926+
bounded(op, b, delta, upper, fromBackEdge, origdelta, reason)
927+
)
928+
}

‎java/ql/test/library-tests/dataflow/range-analysis/RangeAnalysis.expected

Lines changed: 53 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -33,9 +33,17 @@
3333
| A.java:9:16:9:16 | x | SSA init(x) | 0 | upper | NoReason |
3434
| A.java:9:16:9:16 | x | SSA init(y) | -2 | lower | ... == ... |
3535
| A.java:9:16:9:16 | x | SSA init(y) | -2 | upper | ... == ... |
36-
| A.java:9:16:9:20 | ... + ... | 0 | 300 | lower | ... > ... |
37-
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 1 | lower | NoReason |
38-
| A.java:9:16:9:20 | ... + ... | SSA init(y) | -1 | lower | ... == ... |
36+
| A.java:9:16:9:20 | ... + ... | 0 | 600 | lower | ... > ... |
37+
| A.java:9:16:9:20 | ... + ... | 0 | 802 | upper | ... == ... |
38+
| A.java:9:16:9:20 | ... + ... | 0 | 802 | upper | ... > ... |
39+
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 301 | lower | ... == ... |
40+
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 301 | lower | NoReason |
41+
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 402 | upper | ... == ... |
42+
| A.java:9:16:9:20 | ... + ... | SSA init(x) | 402 | upper | NoReason |
43+
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 299 | lower | ... == ... |
44+
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 299 | lower | NoReason |
45+
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 400 | upper | ... == ... |
46+
| A.java:9:16:9:20 | ... + ... | SSA init(y) | 400 | upper | NoReason |
3947
| A.java:9:20:9:20 | y | 0 | 301 | lower | ... > ... |
4048
| A.java:9:20:9:20 | y | 0 | 402 | upper | ... == ... |
4149
| A.java:9:20:9:20 | y | SSA init(x) | 2 | lower | ... == ... |
@@ -54,6 +62,7 @@
5462
| A.java:13:19:13:19 | x | 0 | 400 | upper | ... > ... |
5563
| A.java:13:19:13:19 | x | SSA init(x) | 0 | lower | NoReason |
5664
| A.java:13:19:13:19 | x | SSA init(x) | 0 | upper | NoReason |
65+
| A.java:13:19:13:23 | ... + ... | SSA init(y) | 400 | upper | NoReason |
5766
| A.java:13:23:13:23 | y | SSA init(y) | 0 | lower | NoReason |
5867
| A.java:13:23:13:23 | y | SSA init(y) | 0 | upper | NoReason |
5968
| A.java:15:13:15:13 | y | 0 | 399 | upper | ... != ... |
@@ -69,9 +78,17 @@
6978
| A.java:16:21:16:21 | x | SSA init(x) | 0 | upper | NoReason |
7079
| A.java:16:21:16:21 | x | SSA init(y) | 1 | lower | ... != ... |
7180
| A.java:16:21:16:21 | x | SSA init(y) | 1 | upper | ... != ... |
72-
| A.java:16:21:16:25 | ... + ... | 0 | 303 | lower | ... > ... |
73-
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 1 | lower | NoReason |
74-
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 2 | lower | ... != ... |
81+
| A.java:16:21:16:25 | ... + ... | 0 | 603 | lower | ... > ... |
82+
| A.java:16:21:16:25 | ... + ... | 0 | 799 | upper | ... != ... |
83+
| A.java:16:21:16:25 | ... + ... | 0 | 799 | upper | ... > ... |
84+
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 301 | lower | ... != ... |
85+
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 301 | lower | NoReason |
86+
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 399 | upper | ... != ... |
87+
| A.java:16:21:16:25 | ... + ... | SSA init(x) | 399 | upper | NoReason |
88+
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 302 | lower | ... != ... |
89+
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 302 | lower | NoReason |
90+
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 400 | upper | ... != ... |
91+
| A.java:16:21:16:25 | ... + ... | SSA init(y) | 400 | upper | NoReason |
7592
| A.java:16:25:16:25 | y | 0 | 301 | lower | ... > ... |
7693
| A.java:16:25:16:25 | y | 0 | 399 | upper | ... != ... |
7794
| A.java:16:25:16:25 | y | SSA init(x) | -1 | lower | ... != ... |
@@ -153,14 +170,36 @@
153170
| A.java:35:16:35:16 | x | SSA init(y) | 1 | upper | ... == ... |
154171
| A.java:35:16:35:16 | x | SSA init(z) | -1 | lower | ... == ... |
155172
| A.java:35:16:35:16 | x | SSA init(z) | -1 | upper | ... == ... |
156-
| A.java:35:16:35:20 | ... + ... | 0 | 350 | lower | ... == ... |
157-
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 1 | lower | NoReason |
158-
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 2 | lower | ... == ... |
159-
| A.java:35:16:35:20 | ... + ... | SSA init(z) | 0 | lower | ... == ... |
160-
| A.java:35:16:35:24 | ... + ... | 0 | 351 | lower | ... == ... |
161-
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 2 | lower | NoReason |
162-
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 3 | lower | ... == ... |
163-
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 1 | lower | ... == ... |
173+
| A.java:35:16:35:20 | ... + ... | 0 | 697 | lower | ... == ... |
174+
| A.java:35:16:35:20 | ... + ... | 0 | 697 | upper | ... == ... |
175+
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | lower | ... == ... |
176+
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | lower | NoReason |
177+
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | upper | ... == ... |
178+
| A.java:35:16:35:20 | ... + ... | SSA init(x) | 348 | upper | NoReason |
179+
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | lower | ... == ... |
180+
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | lower | NoReason |
181+
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | upper | ... == ... |
182+
| A.java:35:16:35:20 | ... + ... | SSA init(y) | 349 | upper | NoReason |
183+
| A.java:35:16:35:20 | ... + ... | SSA init(z) | 347 | lower | ... == ... |
184+
| A.java:35:16:35:20 | ... + ... | SSA init(z) | 347 | upper | ... == ... |
185+
| A.java:35:16:35:24 | ... + ... | 0 | 1047 | lower | ... == ... |
186+
| A.java:35:16:35:24 | ... + ... | 0 | 1047 | upper | ... == ... |
187+
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | lower | ... == ... |
188+
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | lower | ... == ... |
189+
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | lower | NoReason |
190+
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | upper | ... == ... |
191+
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | upper | ... == ... |
192+
| A.java:35:16:35:24 | ... + ... | SSA init(x) | 698 | upper | NoReason |
193+
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | lower | ... == ... |
194+
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | lower | ... == ... |
195+
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | lower | NoReason |
196+
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | upper | ... == ... |
197+
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | upper | ... == ... |
198+
| A.java:35:16:35:24 | ... + ... | SSA init(y) | 699 | upper | NoReason |
199+
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | lower | ... == ... |
200+
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | lower | NoReason |
201+
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | upper | ... == ... |
202+
| A.java:35:16:35:24 | ... + ... | SSA init(z) | 697 | upper | NoReason |
164203
| A.java:35:20:35:20 | y | 0 | 348 | lower | ... == ... |
165204
| A.java:35:20:35:20 | y | 0 | 348 | upper | ... == ... |
166205
| A.java:35:20:35:20 | y | SSA init(x) | -1 | lower | ... == ... |

0 commit comments

Comments
 (0)