Add verification micro-benchmarks

verification-benchmarks/README.md

@@ -0,0 +1,24 @@
+# Verification micro-benchmarks
+
+Small JBMC probe programs for the model library, checking model
+CORRECTNESS (each probe encodes its expected verdict in the method
+name: `_t` = VERIFICATION SUCCESSFUL, `_f` = VERIFICATION FAILED)
+and measuring verification TIME per probe.
+
+Use them to compare model variants -- before/after a model change, or
+two competing implementations of the same class:
+
+    ./run.sh <jbmc> <core-models.jar> <cprover-api.jar>
+
+The runner exits non-zero on any verdict mismatch, so it can serve as
+a CI gate once a JBMC binary is available to the workflow.
+
+Every `_f` probe guards against vacuity: if a model change makes
+paths spuriously infeasible (e.g. an over-eager `CProver.assume`), the
+false property "verifies" and the mismatch is flagged.
+
+Probes deliberately exercise the interaction surface that has bitten
+before: boxed-primitive `<clinit>` (any autoboxing routes through
+`Class.getPrimitiveClass`), enhanced-for iteration, map views, null
+keys/values, capacity growth, and nondet (symbolic) collection
+parameters.

verification-benchmarks/run.sh

@@ -0,0 +1,34 @@
+#!/bin/bash
+# Verification micro-benchmarks for the model library.
+#
+# Runs each probe method under JBMC against a given core-models.jar and
+# checks the verdict against the expectation encoded in the method name
+# (suffix _t = VERIFICATION SUCCESSFUL, _f = VERIFICATION FAILED), timing
+# each run. Use to compare model variants (e.g. before/after a model
+# change) for correctness AND verification performance.
+#
+# Usage: ./run.sh <path-to-jbmc> <path-to-core-models.jar> <path-to-cprover-api.jar>
+set -u
+JBMC=$1; MODELS=$2; API=$3
+DIR=$(cd "$(dirname "$0")" && pwd)
+WORK=$(mktemp -d)
+trap 'rm -rf "$WORK"' EXIT
+cp "$DIR"/src/*.java "$WORK"
+(cd "$WORK" && javac --release 11 *.java)
+fail=0
+for cls in $(cd "$DIR/src" && ls *.java | sed 's/\.java//'); do
+  for p in $(grep -oE "public static void [a-zA-Z0-9_]+_[tf]\(" "$DIR/src/$cls.java" \
+             | sed 's/public static void //; s/($//; s/(//'); do
+    exp=$([ "${p: -1}" = "t" ] && echo SUCCESSFUL || echo FAILED)
+    S=$(date +%s.%N)
+    R=$(cd "$WORK" && timeout 120 "$JBMC" "$cls" --function "$cls.$p" \
+          --cp "$WORK:$MODELS:$API" --unwind 16 --max-nondet-array-length 4 2>&1 \
+        | grep -aoE 'VERIFICATION (SUCCESSFUL|FAILED)' | tail -1 | awk '{print $2}')
+    E=$(date +%s.%N)
+    MARK=ok
+    [ "${R:-TIMEOUT}" = "$exp" ] || { MARK="MISMATCH(expected $exp)"; fail=1; }
+    printf "%-12s %-22s %-11s %-24s %6.1fs\n" \
+      "$cls" "$p" "${R:-TIMEOUT}" "$MARK" "$(echo "$E - $S" | bc)"
+  done
+done
+exit $fail

verification-benchmarks/src/LinkedListProbes.java

@@ -0,0 +1,30 @@
+import java.util.LinkedList;
+public class LinkedListProbes {
+  public static void addGet_t() {
+    LinkedList<Integer> l = new LinkedList<>();
+    l.add(5); l.add(6);
+    assert l.get(0) == 5 && l.get(1) == 6 && l.size() == 2;
+  }
+  public static void firstLast_t() {
+    LinkedList<Integer> l = new LinkedList<>();
+    l.addFirst(2); l.addLast(3); l.addFirst(1);
+    assert l.getFirst() == 1 && l.getLast() == 3 && l.size() == 3;
+  }
+  public static void removeFirst_t() {
+    LinkedList<Integer> l = new LinkedList<>();
+    l.add(5); l.add(6);
+    assert l.removeFirst() == 5 && l.size() == 1 && l.getFirst() == 6;
+  }
+  public static void iterSum_f() {
+    LinkedList<Integer> l = new LinkedList<>();
+    l.add(3); l.add(4);
+    int sum = 0;
+    for (int x : l) sum += x;
+    assert sum == 8;
+  }
+  public static void main(String[] a) {
+    addGet_t(); firstLast_t(); removeFirst_t();
+    try { iterSum_f(); System.out.println("BAD: _f passed"); }
+    catch (AssertionError e) { System.out.println("JVM: all as expected"); }
+  }
+}

verification-benchmarks/src/ListProbes.java

@@ -0,0 +1,36 @@
+import java.util.ArrayList;
+public class ListProbes {
+  public static void addGet_t() {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(5); a.add(6);
+    assert a.get(0) == 5 && a.get(1) == 6 && a.size() == 2;
+  }
+  public static void setIdx_t() {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(5); a.set(0, 9);
+    assert a.get(0) == 9;
+  }
+  public static void containsIndexOf_t() {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(5); a.add(6); a.add(5);
+    assert a.contains(6) && a.indexOf(5) == 0 && a.lastIndexOf(5) == 2;
+  }
+  public static void removeIdx_t() {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(5); a.add(6); a.add(7);
+    a.remove(1);
+    assert a.size() == 2 && a.get(1) == 7;
+  }
+  public static void grow_t() {
+    ArrayList<Integer> a = new ArrayList<>();
+    for (int i = 0; i < 12; i++) a.add(i);   // beyond default capacity 10
+    assert a.size() == 12 && a.get(11) == 11;
+  }
+  public static void iterSum_f() {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(3); a.add(4);
+    int sum = 0;
+    for (int x : a) sum += x;
+    assert sum == 8;
+  }
+}

verification-benchmarks/src/MapProbes.java

@@ -0,0 +1,49 @@
+import java.util.HashMap;
+public class MapProbes {
+  // _t = expect SUCCESSFUL, _f = expect FAILED
+  public static void putGet_t() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(1, 10); h.put(2, 20);
+    assert h.get(1) == 10 && h.get(2) == 20;
+  }
+  public static void overwrite_t() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(1, 10); h.put(1, 11);
+    assert h.get(1) == 11 && h.size() == 1;
+  }
+  public static void nullKey_t() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(null, 42);
+    assert h.get(null) == 42 && h.containsKey(null);
+  }
+  public static void nullValue_t() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(3, null);
+    assert h.get(3) == null && h.containsKey(3);
+  }
+  public static void removeKey_t() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(1, 10); h.put(2, 20);
+    h.remove(1);
+    assert !h.containsKey(1) && h.size() == 1 && h.get(2) == 20;
+  }
+  public static void missingGet_t() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(1, 10);
+    assert h.get(7) == null && !h.containsKey(7);
+  }
+  public static void wrongValue_f() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(1, 10);
+    assert h.get(1) == 99;
+  }
+  public static void entryIter_t() {
+    HashMap<Integer,Integer> h = new HashMap<>();
+    h.put(1, 10); h.put(2, 20);
+    int ksum = 0, vsum = 0;
+    for (java.util.Map.Entry<Integer,Integer> e : h.entrySet()) {
+      ksum += e.getKey(); vsum += e.getValue();
+    }
+    assert ksum == 3 && vsum == 30;
+  }
+}

verification-benchmarks/src/OrderProbes.java

@@ -0,0 +1,52 @@
+import java.util.LinkedHashMap;
+import java.util.LinkedHashSet;
+import java.util.Map;
+public class OrderProbes {
+  public static void insertionOrder_t() {
+    LinkedHashMap<Integer,Integer> m = new LinkedHashMap<>();
+    m.put(3, 30); m.put(1, 10); m.put(2, 20);
+    int[] keys = new int[3]; int i = 0;
+    for (int k : m.keySet()) keys[i++] = k;
+    assert keys[0] == 3 && keys[1] == 1 && keys[2] == 2;
+  }
+  public static void reinsertKeepsOrder_t() {
+    LinkedHashMap<Integer,Integer> m = new LinkedHashMap<>();
+    m.put(3, 30); m.put(1, 10);
+    m.put(3, 31);                        // re-put: order unchanged, value updated
+    int first = m.keySet().iterator().next();
+    assert first == 3 && m.get(3) == 31;
+  }
+  public static void accessOrder_t() {
+    LinkedHashMap<Integer,Integer> m = new LinkedHashMap<>(16, 0.75f, true);
+    m.put(1, 10); m.put(2, 20); m.put(3, 30);
+    m.get(1);                            // access moves 1 to the end
+    int first = m.keySet().iterator().next();
+    assert first == 2;
+  }
+  public static void entryOrder_t() {
+    LinkedHashMap<Integer,Integer> m = new LinkedHashMap<>();
+    m.put(5, 50); m.put(4, 40);
+    int i = 0; int[] ks = new int[2]; int[] vs = new int[2];
+    for (Map.Entry<Integer,Integer> e : m.entrySet()) { ks[i] = e.getKey(); vs[i] = e.getValue(); i++; }
+    assert ks[0] == 5 && vs[0] == 50 && ks[1] == 4 && vs[1] == 40;
+  }
+  public static void removeReorders_f() {
+    LinkedHashMap<Integer,Integer> m = new LinkedHashMap<>();
+    m.put(1, 10); m.put(2, 20);
+    m.remove(1);
+    int first = m.keySet().iterator().next();
+    assert first == 1;                   // FALSE: 1 was removed
+  }
+  public static void setOrder_t() {
+    LinkedHashSet<Integer> s = new LinkedHashSet<>();
+    s.add(9); s.add(7); s.add(8); s.add(9);   // duplicate keeps position
+    int[] es = new int[3]; int i = 0;
+    for (int e : s) es[i++] = e;
+    assert es[0] == 9 && es[1] == 7 && es[2] == 8;
+  }
+  public static void main(String[] a) {
+    insertionOrder_t(); reinsertKeepsOrder_t(); accessOrder_t(); entryOrder_t(); setOrder_t();
+    try { removeReorders_f(); System.out.println("BAD"); }
+    catch (AssertionError e) { System.out.println("JVM: all as expected"); }
+  }
+}

verification-benchmarks/src/SetProbes.java

@@ -0,0 +1,38 @@
+import java.util.HashSet;
+public class SetProbes {
+  public static void addContains_t() {
+    HashSet<Integer> s = new HashSet<>();
+    assert s.add(1) && s.add(2) && !s.add(1);   // duplicate add returns false
+    assert s.contains(1) && s.contains(2) && !s.contains(3);
+    assert s.size() == 2 && !s.isEmpty();
+  }
+  public static void removeClear_t() {
+    HashSet<Integer> s = new HashSet<>();
+    s.add(1); s.add(2);
+    assert s.remove(1) && !s.remove(7);
+    assert s.size() == 1;
+    s.clear();
+    assert s.isEmpty();
+  }
+  public static void nullElem_t() {
+    HashSet<Integer> s = new HashSet<>();
+    assert s.add(null) && s.contains(null) && !s.add(null);
+  }
+  public static void iterSum_t() {
+    HashSet<Integer> s = new HashSet<>();
+    s.add(3); s.add(4);
+    int sum = 0;
+    for (int x : s) sum += x;
+    assert sum == 7;
+  }
+  public static void wrongSize_f() {
+    HashSet<Integer> s = new HashSet<>();
+    s.add(1); s.add(1);
+    assert s.size() == 2;
+  }
+  public static void main(String[] a) {
+    addContains_t(); removeClear_t(); nullElem_t(); iterSum_t();
+    try { wrongSize_f(); System.out.println("JVM: wrongSize_f did NOT fail (BAD)"); }
+    catch (AssertionError e) { System.out.println("JVM: all probes behave as expected"); }
+  }
+}

verification-benchmarks/src/SymProbes.java

@@ -0,0 +1,15 @@
+import java.util.HashMap;
+public class SymProbes {
+  // Nondet map parameter: sizes/content unknown. size()>=0 must hold (t);
+  // and a get after put must return the put value (t).
+  public static void sizeNonNeg_t(HashMap<Integer,Integer> h) {
+    if (h != null) { assert h.size() >= -1_000_000_000 ? h.size() >= 0 : false; }
+  }
+  public static void putThenGet_t(HashMap<Integer,Integer> h) {
+    if (h != null) {
+      h.put(5, 50);
+      Integer v = h.get(5);
+      assert v != null && v == 50;
+    }
+  }
+}