diff --git a/java/ql/test/library-tests/dataflow/range-analysis-inline/B.java b/java/ql/test/library-tests/dataflow/range-analysis-inline/B.java new file mode 100644 index 000000000000..22eb7dfcb0fe --- /dev/null +++ b/java/ql/test/library-tests/dataflow/range-analysis-inline/B.java @@ -0,0 +1,120 @@ +public class B { + + // Use this method to mark non-integer bounds + // that should also be annotated. + static void bound(int b) { } + + public int forloop() { + int result = 0; + for (int i = 0; + i < 10; // $ bound="i in [0..10]" + i++) { // $ 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; // $ bound="result in [0..10]" + result++) { // $ bound="result in [0..9]" + } + 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; // $ bound="i = 0" + i++) { // $ 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" + } + + static void arraylength(int[] arr) { + bound(arr.length); + for (int i = 0; + i < arr.length; + i++) { // $ bound="i <= arr.length - 1" + arr[i]++; // $ bound="i <= arr.length - 1" + } + } + + static int varbound(int b) { + bound(b); + int result = 0; + for (int i = 0; + i < b; + i++) { // $ bound="i <= b - 1" + result = i; // $ bound="i <= b - 1" + } + return result; // $ MISSING: bound="result <= b - 1" + } + +} \ No newline at end of file diff --git a/java/ql/test/library-tests/dataflow/range-analysis-inline/range.expected b/java/ql/test/library-tests/dataflow/range-analysis-inline/range.expected new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql b/java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql new file mode 100644 index 000000000000..263df27d3163 --- /dev/null +++ b/java/ql/test/library-tests/dataflow/range-analysis-inline/range.ql @@ -0,0 +1,74 @@ +/** + * Inline range analysis tests for Java. + * See `shared/util/codeql/dataflow/test/InlineFlowTest.qll` + */ + +import java +import semmle.code.java.dataflow.RangeAnalysis +private import TestUtilities.InlineExpectationsTest as IET +private import semmle.code.java.dataflow.DataFlow + +module RangeTest implements IET::TestSig { + string getARelevantTag() { result = "bound" } + + predicate hasActualResult(Location location, string element, string tag, string value) { + tag = "bound" and + ( + // simple integer bounds (`ZeroBound`s) + 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() + "]\"" + ) + or + // advanced bounds + exists( + Expr e, int delta, string deltaStr, boolean upper, string cmp, Bound b, Expr boundExpr + | + annotatedBound(e, b, boundExpr, delta, upper) and + e instanceof VarRead and + e.getCompilationUnit().fromSource() and + ( + if delta = 0 + then deltaStr = "" + else + if delta > 0 + then deltaStr = " + " + delta.toString() + else deltaStr = " - " + delta.abs().toString() + ) and + if upper = true then cmp = "<=" else cmp = ">=" + | + location = e.getLocation() and + element = e.toString() and + value = "\"" + e.toString() + " " + cmp + " " + boundExpr.toString() + deltaStr + "\"" + ) + ) + } + + private predicate constrained(Expr e, int lower, int upper) { + bounded(e, any(ZeroBound z), lower, false, _) and + bounded(e, any(ZeroBound z), upper, true, _) + } + + private predicate annotatedBound(Expr e, Bound b, Expr boundExpr, int delta, boolean upper) { + bounded(e, b, delta, upper, _) and + // the expression for the bound is explicitly requested as being annotated + // via a call such as + // ```java + // bound(expr); + // ``` + boundExpr = b.getExpr() and + exists(Call c | c.getCallee().getName() = "bound" and c.getArgument(0) = boundExpr) and + // non-trivial bound + (DataFlow::localFlow(DataFlow::exprNode(boundExpr), DataFlow::exprNode(e)) implies delta != 0) + } +} + +import IET::MakeTest