Abstract Interpretation Framework

.gitignore

@@ -59,3 +59,4 @@ visualizer/C1Visualizer/*/target/
 *.interp
 *.tokens
 /vm/tests/gh_workflows/CDTInspectorTest/target/
+/abstint-tests/out

absint-tests/src/bounds/inter/BoundsAllContextSafe.java

@@ -0,0 +1,14 @@
+public class BoundsAllContextSafe {
+    static final int[] arr = new int[100];
+
+    static void safeStore(int idx, int value) {
+        arr[idx] = value;
+    }
+
+    public static void main(String[] args) {
+        for (int i = 0; i < 100; i++) {
+            safeStore(i, i * 2);
+        }
+        System.out.println(arr[0]);
+    }
+}

absint-tests/src/bounds/inter/BoundsCalleeAlwaysSafe.java

@@ -0,0 +1,21 @@
+public class BoundsCalleeAlwaysSafe {
+    static int safeGet(int[] a, int i) {
+        if (a == null) return -1;
+        if (i >= 0 && i < a.length) {
+            return a[i];
+        }
+        return -1;
+    }
+
+    public static void main(String[] args) {
+        int[] a = new int[4];
+        for (int i = 0; i < a.length; i++) a[i] = i + 1;
+
+        int v1 = safeGet(a, 2);
+        int v2 = safeGet(a, -1);
+        int v3 = safeGet(a, 99);
+
+        if (v1 + v2 + v3 == 123456) System.out.println("unlikely");
+    }
+}
+

absint-tests/src/bounds/inter/BoundsCalleeGuarded.java

@@ -0,0 +1,18 @@
+public class BoundsCalleeGuarded {
+    static int getOrDefault(int[] a, int i) {
+        if (a == null) return -1;
+        if (i >= 0 && i < a.length) {
+            return a[i];
+        }
+        return -1;
+    }
+
+    public static void main(String[] args) {
+        int[] a = new int[4];
+        for (int i = 0; i < a.length; i++) a[i] = i + 1;
+        int v1 = getOrDefault(a, 2);
+        int v2 = getOrDefault(a, -1);
+        int v3 = getOrDefault(a, 99);
+        if (v1 + v2 + v3 == 123456) System.out.println("unlikely");
+    }
+}

absint-tests/src/bounds/inter/BoundsCalleeUnsafeCallerSafe.java

@@ -0,0 +1,27 @@
+public class BoundsCalleeUnsafeCallerSafe {
+  static int uncheckedGet(int[] a, int i) {
+    // No internal guard: safety fully depends on caller.
+    return a[i];
+  }
+
+  public static void main(String[] args) {
+    int[] a = new int[5];
+    for (int i = 0; i < a.length; i++) a[i] = i;
+
+    int sum = 0;
+
+    // Safe usage: caller guards i before calling.
+    for (int i = -2; i < a.length + 2; i++) {
+      if (i >= 0 && i < a.length) {
+        // On this path, i is definitely in [0, a.length-1], so the call is safe.
+        sum += uncheckedGet(a, i);
+      }
+    }
+
+    // Unsafe usage: caller does not guard the index.
+    int bad = uncheckedGet(a, a.length); // always out-of-bounds
+
+    if (sum + bad == 123456) System.out.println("unlikely");
+  }
+}
+

absint-tests/src/bounds/inter/BoundsCallerGuards.java

@@ -0,0 +1,15 @@
+public class BoundsCallerGuards {
+    static int uncheckedAt(int[] a, int i) {
+        return a[i];
+    }
+
+    public static void main(String[] args) {
+        int[] a = new int[6];
+        for (int i = 0; i < a.length; i++) a[i] = i * 2;
+        int sum = 0;
+        for (int i = 0; i < a.length; i++) {
+            sum += uncheckedAt(a, i);
+        }
+        if (sum == -1) System.out.println("impossible");
+    }
+}

absint-tests/src/bounds/inter/BoundsClampIndex.java

@@ -0,0 +1,17 @@
+public class BoundsClampIndex {
+    static int clamp(int i, int len) {
+        if (i < 0) return 0;
+        if (i >= len) return len - 1;
+        return i;
+    }
+
+    public static void main(String[] args) {
+        int[] a = new int[5];
+        for (int i = 0; i < a.length; i++) a[i] = i + 10;
+        int idx = clamp(100, a.length);
+        int v1 = a[idx];
+        idx = clamp(-7, a.length);
+        int v2 = a[idx];
+        if (v1 + v2 == -1) System.out.println("impossible");
+    }
+}

absint-tests/src/bounds/inter/BoundsLengthPropagationInterproc.java

@@ -0,0 +1,22 @@
+public class BoundsLengthPropagationInterproc {
+  static int mid(int[] a) {
+    if (a == null || a.length == 0) return -1;
+    return a.length / 2;
+  }
+
+  public static void main(String[] args) {
+    int[] a = new int[args.length + 1];
+
+    int m = mid(a);
+    if (m >= 0) {
+      a[m] = 42;
+
+      if (m >= a.length) {
+        System.out.println("unreachable");
+      }
+    }
+
+    if (a[m] == 123456) System.out.println("unlikely");
+  }
+}
+

absint-tests/src/bounds/inter/BoundsProducerConsumer.java

@@ -0,0 +1,19 @@
+public class BoundsProducerConsumer {
+  static int consumeLast(int[] a) {
+    if (a.length == 0) return 0;
+    int i = a.length - 1;
+    return a[i];
+  }
+
+  static int[] produce(int n) {
+    int[] a = new int[n];
+    for (int i = 0; i < a.length; i++) a[i] = i + 1;
+    return a;
+  }
+
+  public static void main(String[] args) {
+    int[] a = produce(4);
+    int v = consumeLast(a); // safe access
+    if (v == -1) System.out.println("impossible");
+  }
+}

absint-tests/src/bounds/intra/ArrayIndexing.java

@@ -0,0 +1,21 @@
+public class ArrayIndexing {
+  private static int val;
+  private static int computed;
+  public static void main(String[] args) {
+    int[] a = new int[5];
+    for (int i = 0; i < a.length; i++) {
+      a[i] = i * 2; 
+    }
+
+    int idx = 2;
+    val = a[idx];
+
+    if (val > 3) {
+      idx = 4;
+    } else {
+      idx = 0;
+    }
+
+    computed = (a[1] / 2) + 1;
+  }
+}

absint-tests/src/bounds/intra/Bounds2D.java

@@ -0,0 +1,16 @@
+// Intra-procedural: 2D array with per-row lengths, classic nested loops
+public class Bounds2D {
+  public static void main(String[] args) {
+    int rows = 3;
+    int cols = 4;
+    int[][] m = new int[rows][cols];
+    int sum = 0;
+    for (int i = 0; i < m.length; i++) {
+      for (int j = 0; j < m[i].length; j++) {
+        m[i][j] = i + j;
+        sum += m[i][j];
+      }
+    }
+    if (sum == -1) System.out.println("impossible");
+  }
+}

absint-tests/src/bounds/intra/BoundsAlwaysOffByOne.java

@@ -0,0 +1,13 @@
+public class BoundsAlwaysOffByOne {
+    public static void main(String[] args) {
+        int[] a = new int[5];
+
+        for (int i = 0; i <= a.length; i++) {
+            if (i < a.length) {
+                a[i] = i;
+            } else {
+            }
+        }
+    }
+}
+

absint-tests/src/bounds/intra/BoundsAlwaysSafeSimple.java

@@ -0,0 +1,26 @@
+public class BoundsAlwaysSafeSimple {
+  public static void main(String[] args) {
+    int[] a = new int[4];
+    for (int i = 0; i < a.length; i++) {
+      // At this point, an interval analysis should infer i in [0, a.length-1]
+      // so the following access is always in-bounds.
+      a[i] = i;
+      if (!(0 <= i && i < a.length)) {
+        // This branch should be unreachable (condition always false).
+        System.out.println("unreachable");
+      }
+      if (i >= a.length) {
+        // Also unreachable: i >= a.length is always false in the loop body.
+        System.out.println("also unreachable");
+      }
+    }
+
+    int sum = 0;
+    for (int i = 0; i < a.length; i++) {
+      // Again, always in-bounds.
+      sum += a[i];
+    }
+    if (sum == 123456) System.out.println("unlikely");
+  }
+}
+

absint-tests/src/bounds/intra/BoundsConstantIndex.java

@@ -0,0 +1,10 @@
+public class BoundsConstantIndex {
+  private static int v;
+  public static void main(String[] args) {
+    int[] a = new int[6];
+    a[2] = 7;
+    a[4] = 9;
+    v = a[2] + a[4];
+    if (v == 0) System.out.println("impossible");
+  }
+}

absint-tests/src/bounds/intra/BoundsConstantOOB.java

@@ -0,0 +1,31 @@
+public class BoundsConstantOOB {
+  public static void main(String[] args) {
+    int[] a = new int[5];
+
+    int in = 3; // always in-bounds
+    int outNeg = -1; // always out-of-bounds (negative)
+    int outHigh = 5; // always out-of-bounds (== length)
+
+    // Definitely safe
+    a[in] = 1;
+
+    // The following two uses are definitely out-of-bounds.
+    // An interval analysis should classify these as always unsafe.
+    // (They may still run and throw at runtime if executed.)
+    if (outNeg >= 0 && outNeg < a.length) {
+      // Guard is always false; body is unreachable.
+      a[outNeg] = 2;
+    }
+
+    if (outHigh >= 0 && outHigh < a.length) {
+      // Guard is always false; body is unreachable.
+      a[outHigh] = 3;
+    }
+
+    // Unguarded OOB access for analysis to detect.
+    // a[outHigh] = 4; // uncomment to create a concrete runtime error
+
+    if (a[in] == 123456) System.out.println("unlikely");
+  }
+}
+

absint-tests/src/bounds/intra/BoundsGuardedIndex.java

@@ -0,0 +1,18 @@
+// Intra-procedural: access guarded by explicit 0 <= idx < length checks
+public class BoundsGuardedIndex {
+  private static int unknown() { return (int)(System.currentTimeMillis() & 7); }
+
+  public static void main(String[] args) {
+    int[] a = new int[8];
+    for (int i = 0; i < a.length; i++) a[i] = i * 3;
+
+    int idx = unknown(); // some unknown in [0,7]
+    int v;
+    if (idx >= 0 && idx < a.length) {
+      v = a[idx]; // should be recognized as safe after guard
+    } else {
+      v = -1;
+    }
+    if (v == 123456) System.out.println("unlikely");
+  }
+}

absint-tests/src/bounds/intra/BoundsMinCopy.java

@@ -0,0 +1,15 @@
+public class BoundsMinCopy {
+
+  public static void main(String[] args) {
+    int[] src = new int[7];
+    int[] dst = new int[5];
+    for (int i = 0; i < src.length; i++) {
+        src[i] = i * 2;
+    }
+
+    int n = Math.min(src.length, dst.length);
+    for (int i = 0; i < n; i++) {
+      dst[i] = src[i]; 
+    }
+  }
+}

absint-tests/src/bounds/intra/BoundsOffByOne.java

@@ -0,0 +1,11 @@
+public class BoundsOffByOne {
+  public static void main(String[] args) {
+    int[] a = new int[5];
+    for (int i = 0; i < a.length; i++) a[i] = i;
+
+    int last = 0;
+    if (a.length > 0) {
+      last = a[a.length - 1]; 
+    }
+  }
+}

absint-tests/src/bounds/intra/BoundsPathSensitiveIfElse.java

@@ -0,0 +1,25 @@
+public class BoundsPathSensitiveIfElse {
+  public static void main(String[] args) {
+    int[] a = new int[8];
+    int i = args.length - 1; // abstractly, could be negative or up to some small number
+
+    if (i >= 0 && i < a.length) {
+      // On this path, index is definitely within [0, a.length-1].
+      a[i] = 1; // always safe on the then-branch.
+    } else {
+      // Here, we only know that !(0 <= i < a.length), so i < 0 or i >= a.length.
+      // This access is potentially unsafe and should be flagged.
+      // Depending on analysis precision, it might be classified as definitely out-of-bounds
+      // or at least unknown.
+       a[i] = 2;
+    }
+
+    if (i >= 0 && i < a.length) {
+      // This condition is not always true at this point (because we have both branches),
+      // but it is exactly the same as the guard above.
+      // Interval analysis may classify this as unknown in general.
+      System.out.println("maybe");
+    }
+  }
+}
+

absint-tests/src/bounds/intra/BoundsSafeLoop.java

@@ -0,0 +1,14 @@
+public class BoundsSafeLoop {
+    public static void main(String[] args) {
+        int n = 10;
+        int[] a = new int[n];
+        int sum = 0;
+        for (int i = 0; i < a.length; i++) {
+            a[i] = i;
+        }
+        for (int i = 0; i < a.length; i++) {
+            sum += a[i];
+        }
+        if (sum == -1) System.out.println("impossible");
+    }
+}

absint-tests/src/bounds/intra/BoundsUnsafeAccess.java

@@ -0,0 +1,10 @@
+public class BoundsUnsafeAccess {
+  public static void main(String[] args) {
+    int[] a = new int[5];
+    int x = 0;
+    int i = 5; 
+    if (args.length == 42) {
+      x = a[i];
+    }
+  }
+}

absint-tests/src/bounds/intra/UnknownCycleLength.java

@@ -0,0 +1,8 @@
+public class UnknownCycleLength {
+    private static int res = 0;
+    public static void main(String[] args) {
+        for (String arg : args) {
+            res += arg.length();
+        }
+    }
+}