Skip to content

Commit 6d6f269

Browse files
yoffyoff
authored
Merge pull request #17997 from yoff/java/inline-range-tests
2 parents 0c6b4cd + f508f8e commit 6d6f269

File tree

3 files changed

+229
-0
lines changed

3 files changed

+229
-0
lines changed

‎java/ql/test/library-tests/dataflow/range-analysis-inline/B.java‎

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
public class B {
2+
3+
// Use this method to mark non-integer bounds
4+
// that should also be annotated.
5+
static void bound(int b) { }
6+
7+
public int forLoop() {
8+
int result = 0;
9+
for (int i = 0;
10+
i < 10; // $ bound="i in [0..10]"
11+
i++) { // $ bound="i in [0..9]"
12+
result = i; // $ bound="i in [0..9]"
13+
}
14+
return result; // $ bound="result in [0..9]"
15+
}
16+
17+
public int forLoopExit() {
18+
int result = 0;
19+
for (; result < 10;) { // $ bound="result in [0..10]"
20+
result += 1; // $ bound="result in [0..9]"
21+
}
22+
return result; // $ bound="result = 10"
23+
}
24+
25+
public int forLoopExitStep() {
26+
int result = 0;
27+
for (; result < 10;) { // $ bound="result in [0..12]"
28+
result += 3; // $ bound="result in [0..9]"
29+
}
30+
return result; // $ bound="result = 12"
31+
}
32+
33+
public int forLoopExitUpd() {
34+
int result = 0;
35+
for (; result < 10; // $ bound="result in [0..10]"
36+
result++) { // $ bound="result in [0..9]"
37+
}
38+
return result; // $ bound="result = 10"
39+
}
40+
41+
public int forLoopExitNested() {
42+
int result = 0;
43+
for (; result < 10;) {
44+
int i = 0;
45+
for (; i < 3;) { // $ bound="i in [0..3]"
46+
i += 1; // $ bound="i in [0..2]"
47+
}
48+
result += i; // $ bound="result in [0..9]" bound="i = 3"
49+
}
50+
return result; // $ MISSING:bound="result = 12"
51+
}
52+
53+
public int emptyForLoop() {
54+
int result = 0;
55+
for (int i = 0; i < 0; // $ bound="i = 0"
56+
i++) { // $ bound="i in [0..-1]"
57+
result = i; // $ bound="i in [0..-1]"
58+
}
59+
return result; // $ bound="result = 0"
60+
}
61+
62+
public int noLoop() {
63+
int result = 0;
64+
result += 1; // $ bound="result = 0"
65+
return result; // $ bound="result = 1"
66+
}
67+
68+
public int foreachLoop() {
69+
int result = 0;
70+
for (int i : new int[] {1, 2, 3, 4, 5}) {
71+
result = i;
72+
}
73+
return result;
74+
}
75+
76+
public int emptyForeachLoop() {
77+
int result = 0;
78+
for (int i : new int[] {}) {
79+
result = i;
80+
}
81+
return result;
82+
}
83+
84+
public int whileLoop() {
85+
int result = 100;
86+
while (result > 5) { // $ bound="result in [4..100]"
87+
result = result - 2; // $ bound="result in [6..100]"
88+
}
89+
return result; // $ bound="result = 4"
90+
}
91+
92+
public int oddWhileLoop() {
93+
int result = 101;
94+
while (result > 5) { // $ bound="result in [5..101]"
95+
result = result - 2; // $ bound="result in [7..101]"
96+
}
97+
return result; // $ bound="result = 5"
98+
}
99+
100+
static void arrayLength(int[] arr) {
101+
bound(arr.length);
102+
for (int i = 0;
103+
i < arr.length;
104+
i++) { // $ bound="i <= arr.length - 1"
105+
arr[i]++; // $ bound="i <= arr.length - 1"
106+
}
107+
}
108+
109+
static int varBound(int b) {
110+
bound(b);
111+
int result = 0;
112+
for (int i = 0;
113+
i < b;
114+
i++) { // $ bound="i <= b - 1"
115+
result = i; // $ bound="i <= b - 1"
116+
}
117+
return result; // We cannot conclude anything here, since we do not know that b > 0
118+
}
119+
120+
static int varBoundPositiveGuard(int b) {
121+
bound(b);
122+
if (b > 0) {
123+
int result = 0;
124+
for (int i = 0;
125+
i < b;
126+
i++) { // $ bound="i <= b - 1"
127+
result = i; // $ bound="i <= b - 1"
128+
}
129+
return result; // $ MISSING: bound="result <= b - 1"
130+
} else {
131+
return 0;
132+
}
133+
}
134+
135+
static int varBoundPositiveGuardEarlyReturn(int b) {
136+
bound(b);
137+
if (b <= 0) return 0;
138+
int result = 0;
139+
for (int i = 0;
140+
i < b;
141+
i++) { // $ bound="i <= b - 1"
142+
result = i; // $ bound="i <= b - 1"
143+
}
144+
return result; // $ MISSING: bound="result <= b - 1"
145+
}
146+
147+
static int varBoundPositiveAssert(int b) {
148+
bound(b);
149+
assert b > 0;
150+
int result = 0;
151+
for (int i = 0;
152+
i < b;
153+
i++) { // $ bound="i <= b - 1"
154+
result = i; // $ bound="i <= b - 1"
155+
}
156+
return result; // $ MISSING: bound="result <= b - 1"
157+
}
158+
}

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

Whitespace-only changes.

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

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
/**
2+
* Inline range analysis tests for Java.
3+
* See `shared/util/codeql/dataflow/test/InlineFlowTest.qll`
4+
*/
5+
6+
import java
7+
import semmle.code.java.dataflow.RangeAnalysis
8+
private import TestUtilities.InlineExpectationsTest as IET
9+
10+
module RangeTest implements IET::TestSig {
11+
string getARelevantTag() { result = "bound" }
12+
13+
predicate hasActualResult(Location location, string element, string tag, string value) {
14+
tag = "bound" and
15+
(
16+
// simple integer bounds (`ZeroBound`s)
17+
exists(Expr e, int lower, int upper |
18+
constrained(e, lower, upper) and
19+
e instanceof VarRead and
20+
e.getCompilationUnit().fromSource()
21+
|
22+
location = e.getLocation() and
23+
element = e.toString() and
24+
if lower = upper
25+
then value = "\"" + e.toString() + " = " + lower.toString() + "\""
26+
else
27+
value = "\"" + e.toString() + " in [" + lower.toString() + ".." + upper.toString() + "]\""
28+
)
29+
or
30+
// advanced bounds
31+
exists(Expr e, int delta, string deltaStr, boolean upper, string cmp, Expr boundExpr |
32+
annotatedBound(e, _, boundExpr, delta, upper) and
33+
e instanceof VarRead and
34+
e.getCompilationUnit().fromSource() and
35+
(
36+
if delta = 0
37+
then deltaStr = ""
38+
else
39+
if delta > 0
40+
then deltaStr = " + " + delta.toString()
41+
else deltaStr = " - " + delta.abs().toString()
42+
) and
43+
if upper = true then cmp = "<=" else cmp = ">="
44+
|
45+
location = e.getLocation() and
46+
element = e.toString() and
47+
value = "\"" + e.toString() + " " + cmp + " " + boundExpr.toString() + deltaStr + "\""
48+
)
49+
)
50+
}
51+
52+
private predicate constrained(Expr e, int lower, int upper) {
53+
bounded(e, any(ZeroBound z), lower, false, _) and
54+
bounded(e, any(ZeroBound z), upper, true, _)
55+
}
56+
57+
private predicate annotatedBound(Expr e, Bound b, Expr boundExpr, int delta, boolean upper) {
58+
bounded(e, b, delta, upper, _) and
59+
// the expression for the bound is explicitly requested as being annotated
60+
// via a call such as
61+
// ```java
62+
// bound(expr);
63+
// ```
64+
boundExpr = b.getExpr() and
65+
exists(Call c | c.getCallee().getName() = "bound" and c.getArgument(0) = boundExpr) and
66+
// non-trivial bound
67+
not e = b.getExpr()
68+
}
69+
}
70+
71+
import IET::MakeTest<RangeTest>

0 commit comments

Comments
 (0)