java: inline range test

Author: yoff

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

@@ -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"
+    }
+}

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

@@ -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>