java: inline range test

This commit is contained in:
Rasmus Lerchedahl Petersen
2024-11-14 23:49:52 +01:00
parent c8c15a0899
commit 15953bf569
3 changed files with 127 additions and 0 deletions

View File

@@ -0,0 +1,90 @@
public class B {
public int forloop() {
int result = 0;
for (int i = 0; i < 10; i++) {// $ bound="i in [0..10]" bound="i in [0..9]"
result = i; // $ bound="i in [0..9]"
}
return result; // $ bound="result in [0..9]"
}
public int forloopexit() {
int result = 0;
for (; result < 10;) { // $ bound="result in [0..10]"
result += 1; // $ bound="result in [0..9]"
}
return result; // $ bound="result = 10"
}
public int forloopexitstep() {
int result = 0;
for (; result < 10;) { // $ bound="result in [0..12]"
result += 3; // $ bound="result in [0..9]"
}
return result; // $ bound="result = 12"
}
public int forloopexitupd() {
int result = 0;
for (; result < 10; result++) { // $ bound="result in [0..9]" bound="result in [0..10]"
}
return result; // $ bound="result = 10"
}
public int forloopexitnested() {
int result = 0;
for (; result < 10;) {
int i = 0;
for (; i < 3;) { // $ bound="i in [0..3]"
i += 1; // $ bound="i in [0..2]"
}
result += i; // $ bound="result in [0..9]" bound="i = 3"
}
return result; // $ MISSING:bound="result = 12"
}
public int emptyforloop() {
int result = 0;
for (int i = 0; i < 0; i++) { // $ bound="i = 0" bound="i in [0..-1]"
result = i; // $ bound="i in [0..-1]"
}
return result; // $ bound="result = 0"
}
public int noloop() {
int result = 0;
result += 1; // $ bound="result = 0"
return result; // $ bound="result = 1"
}
public int foreachloop() {
int result = 0;
for (int i : new int[] {1, 2, 3, 4, 5}) {
result = i;
}
return result;
}
public int emptyforeachloop() {
int result = 0;
for (int i : new int[] {}) {
result = i;
}
return result;
}
public int whileloop() {
int result = 100;
while (result > 5) { // $ bound="result in [4..100]"
result = result - 2; // $ bound="result in [6..100]"
}
return result; // $ bound="result = 4"
}
public int oddwhileloop() {
int result = 101;
while (result > 5) { // $ bound="result in [5..101]"
result = result - 2; // $ bound="result in [7..101]"
}
return result; // $ bound="result = 5"
}
}

View File

@@ -0,0 +1,37 @@
/**
* Inline range analysis tests for Java.
* See `shared/util/codeql/dataflow/test/InlineFlowTest.qll`
*/
import java
import semmle.code.java.dataflow.RangeAnalysis
private import codeql.util.test.InlineExpectationsTest
private import TestUtilities.internal.InlineExpectationsTestImpl
private import Make<Impl> as IET
module RangeTest implements IET::TestSig {
string getARelevantTag() { result = "bound" }
predicate hasActualResult(Location location, string element, string tag, string value) {
tag = "bound" and
exists(Expr e, int lower, int upper |
constrained(e, lower, upper) and
e instanceof VarRead and
e.getCompilationUnit().fromSource()
|
location = e.getLocation() and
element = e.toString() and
if lower = upper
then value = "\"" + e.toString() + " = " + lower.toString() + "\""
else
value = "\"" + e.toString() + " in [" + lower.toString() + ".." + upper.toString() + "]\""
)
}
private predicate constrained(Expr e, int lower, int upper) {
lower = min(int delta | bounded(e, any(ZeroBound z), delta, false, _)) and
upper = min(int delta | bounded(e, any(ZeroBound z), delta, true, _))
}
}
import IET::MakeTest<RangeTest>