Skip to content

Commit 915fcf9

Browse files
committed
Shared/Java: Improve range analysis for phi exits out of loops and accept test changes.
1 parent 582d21d commit 915fcf9

File tree

2 files changed

+29
-0
lines changed

2 files changed

+29
-0
lines changed

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,7 @@
236236
| A.java:44:13:44:13 | 0 | 0 | 0 | upper | NoReason |
237237
| A.java:45:12:45:12 | i | 0 | 0 | lower | NoReason |
238238
| A.java:45:12:45:12 | i | SSA def(i) | 0 | lower | NoReason |
239+
| A.java:45:12:45:12 | i | SSA param(size) | 0 | upper | ... < ... |
239240
| A.java:45:12:45:12 | i | SSA phi(i) | 0 | lower | NoReason |
240241
| A.java:45:12:45:12 | i | SSA phi(i) | 0 | upper | NoReason |
241242
| A.java:45:16:45:19 | size | SSA param(size) | 0 | lower | NoReason |
@@ -253,6 +254,7 @@
253254
| A.java:48:12:48:12 | i | 0 | 0 | lower | NoReason |
254255
| A.java:48:12:48:12 | i | SSA def(i) | 0 | lower | NoReason |
255256
| A.java:48:12:48:12 | i | SSA param(size) | 0 | lower | ... < ... |
257+
| A.java:48:12:48:12 | i | SSA param(size) | 0 | upper | ... < ... |
256258
| A.java:48:12:48:12 | i | SSA phi(i) | 0 | lower | NoReason |
257259
| A.java:48:12:48:12 | i | SSA phi(i) | 0 | upper | NoReason |
258260
| A.java:52:9:52:13 | i | 0 | 0 | lower | NoReason |

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1011,6 +1011,27 @@ module RangeStage<
10111011
boundedPhiInp(phi, _, b, delta, upper, fromBackEdge, origdelta, reason)
10121012
}
10131013

1014+
/**
1015+
* Holds if `inp <= delta` where `inp` is the input to `phi` along the edge
1016+
* with rank `rix`.
1017+
*
1018+
* Equivalent to `boundedPhiInp(phi, rix, any(SemZeroBound zb), delta, true, _, _, _)`.
1019+
*/
1020+
private predicate zeroUpperBoundedPhiInp1(Sem::SsaPhiNode phi, int rix, D::Delta delta) {
1021+
boundedPhiInp1(phi, any(SemZeroBound zb), true, rix, delta)
1022+
}
1023+
1024+
/**
1025+
* Holds if `inp <= b + delta` for some input, `inp`, to `phi` and `b >= 0`.
1026+
*/
1027+
private predicate upperBoundedPhiCand(
1028+
Sem::SsaPhiNode phi, SemSsaBound b, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
1029+
SemReason reason
1030+
) {
1031+
boundedPhiCand(phi, true, b, delta, fromBackEdge, origdelta, reason) and
1032+
typeBound(Sem::getSsaType(b.getVariable()), any(float f | f >= 0), _)
1033+
}
1034+
10141035
/**
10151036
* Holds if the candidate bound `b + delta` for `phi` is valid for the phi input
10161037
* along the edge with rank `rix`.
@@ -1031,6 +1052,12 @@ module RangeStage<
10311052
or
10321053
selfBoundedPhiInp(phi, rix, upper)
10331054
)
1055+
or
1056+
upperBoundedPhiCand(phi, b, delta, fromBackEdge, origdelta, reason) and
1057+
exists(D::Delta d1 | zeroUpperBoundedPhiInp1(phi, rix, d1) |
1058+
upper = true and
1059+
D::toFloat(d1) <= D::toFloat(delta)
1060+
)
10341061
}
10351062

10361063
/**

0 commit comments

Comments
 (0)