Add verification micro-benchmarks - #44
Open
tautschnig wants to merge 4 commits into
Open
Conversation
A benchmark/regression harness for the model library itself: probe programs whose method names encode the expected JBMC verdict (_t/_f), with a runner that checks verdicts and reports per-probe verification time. Intended for comparing model variants (correctness AND solver performance) and as a vacuity guard: every _f probe fails loudly if a model change prunes its counterexample path. The initial probe set covers HashMap (put/get/overwrite/null key/null value/remove/miss/entrySet iteration), ArrayList (add/get/set/contains/ indexOf/lastIndexOf/remove/capacity growth/iteration), and nondet (symbolic) map parameters -- including the boxed-primitive <clinit> path on which any autoboxing depends. This harness would have caught the getPrimitiveClass -> notModelled forName regression fixed in the sibling branch. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ration + duplicate-size vacuity guard) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
… iteration vacuity guard) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
Adds a lightweight JBMC-based verification micro-benchmark harness to exercise the model library and track both correctness (expected SUCCESS/FAIL verdicts) and per-probe verification time, helping detect regressions and vacuity.
Changes:
- Introduces probe programs for
HashMap,ArrayList,HashSet, and symbolic (nondet)HashMapparameters with_t/_fexpected-verdict encoding. - Adds a
run.shrunner to compile probes, run each method under JBMC, check verdicts, and report timings. - Documents the purpose and usage of the benchmark harness.
Reviewed changes
Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| verification-benchmarks/src/MapProbes.java | Adds HashMap behavior probes including iteration and negative (“_f”) cases. |
| verification-benchmarks/src/ListProbes.java | Adds ArrayList behavior probes including growth, iteration, and a negative (“_f”) case. |
| verification-benchmarks/src/SetProbes.java | Adds HashSet probes including null element and a negative (“_f”) case plus a small JVM sanity main. |
| verification-benchmarks/src/SymProbes.java | Adds probes intended to exercise symbolic HashMap parameters. |
| verification-benchmarks/run.sh | Adds the runner to compile probes, invoke JBMC per method, check verdicts, and time runs. |
| verification-benchmarks/README.md | Documents rationale and how to run the harness. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // 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; } |
| WORK=$(mktemp -d) | ||
| trap 'rm -rf "$WORK"' EXIT | ||
| cp "$DIR"/src/*.java "$WORK" | ||
| (cd "$WORK" && javac --release 11 *.java) |
…sertion, re-insert, access-order, entry views, removal vacuity guard) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A benchmark/regression harness for the model library itself: probe
programs whose method names encode the expected JBMC verdict (_t/_f),
with a runner that checks verdicts and reports per-probe verification
time. Intended for comparing model variants (correctness AND solver
performance) and as a vacuity guard: every _f probe fails loudly if a
model change prunes its counterexample path.
The initial probe set covers HashMap (put/get/overwrite/null key/null
value/remove/miss/entrySet iteration), ArrayList (add/get/set/contains/
indexOf/lastIndexOf/remove/capacity growth/iteration), and nondet
(symbolic) map parameters -- including the boxed-primitive
path on which any autoboxing depends. This harness would have caught
the getPrimitiveClass -> notModelled forName regression fixed in the
sibling branch.
Co-authored-by: Kiro kiro-agent@users.noreply.github.com