[nils-loose]

What

A static, whole-program property pre-check for SV-COMP mode.

• de.uzl.its.swat.staticcheck.ExceptionFreedomCheck (executor jar, ASM). It analyses every class on the task classpath, entered at Main.main, and proves or fails to prove two facts:
  • exception_free: no RuntimeException can escape Main.main or a static initializer that may run. This is the no-runtime-exception property.
  • assertion_free: reachable code never creates an AssertionError, so no assert can fail. This is valid-assert.
• svcomp/PropertyPreCheck.py: the driver runs the check before round 0, as a subprocess with a 60 s timeout. A crash, a timeout or unparsable output proves nothing, and the run proceeds unchanged.
• If the property is proven:
  • Round 0 still runs, as a cross-check. If it finds a violation, the verdict is UNKNOWN and a precheck_contradiction execution error is recorded.
  • Otherwise the verdict is SAFE, without exploration.
  • The exploration's soundness downgrades (context loss, precision loss, uncaught exceptions, divergence, sa_desync) do not apply to this SAFE, because it does not rest on the exploration.
• If it is not proven: the behaviour is unchanged. The check adds about 0.2 s.
• stats.json gets a property_precheck block. --no-property-precheck disables the check.

Why

LIMITATIONS work item 2 (verdict-downgrade-too-coarse, no-exception-freedom-precheck, property-irrelevant-branches-explored, uncaught-exception-downgrade):

• Under no-runtime-exception, SAFE was downgraded for context or precision loss even when the program contains no instruction that can throw.
• SAFE needed an exhausted path space, which is impossible for unbounded loops (MinePump, float_unboundedloop, jayhorn-recursive).

A whole-program proof answers both questions at once, for every execution. That is simpler and safer than refining each downgrade by what is reachable after the context-loss point. The proof does not use the cfg-extraction SA graph: REVIEW-cfg lists ways in which that graph is unsound (B1-B3, S1-S6), and the graph is not in the competition package.

Soundness argument

The SAFE claim needs one thing: the proof holds for all executions of the original program. Exploration events then cannot matter, since they only describe what the exploration covered.

The proof is conservative everywhere. When something is unknown, the check fails.

1. Closed world. Every call from reachable code (call graph plus the static initializers that reachable code may trigger) must go to one of three places:

   • application code, with targets that over-approximate JVM selection: every non-private instance method of the superclass chain, every application default method, and the library implementation unless a public or protected application method overrides it. If a library default method might be selected, the targets are unknown and the check fails;
   • the modelled Verifier methods: nondet* except nondetObject, and assume. nondetString is non-null;
   • a short list of library methods in JdkModel that never throw a RuntimeException for the stated argument conditions, and never call back into application code.

   Anything else fails the check, even inside a catch: invokedynamic other than string concatenation, ldc of method handles, reflection, finalizers. Therefore application code only runs when application code calls it.

2. Instructions. Every instruction that JVMS lets throw a RuntimeException must be proven safe, or be covered by a handler for Throwable, Exception or RuntimeException (or ArithmeticException for division), whose code is checked in turn. Those instructions are: xaload/xastore, arraylength, (multi)newarray, get/putfield, invoke instructions, checkcast, idiv/irem/ldiv/lrem, athrow, monitors and invokedynamic. The values come from an abstract interpretation (ASM Analyzer) that tracks:

   • nullness;
   • int and long constants;
   • array lengths;
   • enum ordinals against values().length;
   • exact runtime types;
   • the receiver.

   A caught exception may be rethrown only if no instruction its handler covers can raise a RuntimeException. A thrown value must have an exact type that is not a RuntimeException.

3. Facts. The facts about fields, parameters and return values are least fixpoints of the joins of all stored, passed or returned values, over all application methods. Reference fields also hold their default null. The exception is a field that every constructor (or the static initializer) assigns in a straight-line, handler-free prefix, in which:

   • nothing that may execute (methods called transitively, static initializers triggered, superclass initializers) reads a field of that name;
   • the receiver does not escape (a may-alias flag that survives joins).

4. May-throw is a least fixpoint over the call graph. An exception must start at some instruction that is checked locally.

Assumptions:

• the classpath is the program. The check enforces this: it fails if any classpath class lies in a platform package (java/, javax/, jdk/, sun/, or the JDK 8 packages org/xml/, org/w3c/, org/omg/, org/ietf/, org/jcp/, com/sun/), in a package of the JDK's boot modules, or in the Verifier package other than Verifier/ObjectFactory. The JVM would refuse such a class, load the JDK's class instead, or run its static initializer without analysis;
• enums are compiled from Java source;
• the sv-benchmarks Verifier semantics hold;
• the whitelisted JDK methods behave as on JDK 8, 17 and 21. Methods that overflow on JDK 8 (concat, toLowerCase, new StringBuilder(String)) are excluded;
• Errors (StackOverflowError, OutOfMemoryError, linkage errors) are not RuntimeExceptions;
• an exception escaping a static initializer is counted, which is conservative.

Review. An independent adversarial review ran three rounds. It wrote programs that pass the check but throw, and confirmed each one by running it. It found 11 counterexamples:

• wrong selection of default, private and package-private methods;
• library default methods;
• a receiver escape hidden by a join;
• main(null);
• JDK 8 overflow in two whitelisted methods.

All of them are fixed and are now regression tests. Round 3 found none.

A second, independent review of this PR (results/review-pr73.md) found 6 more counterexamples. All of them come from one root cause: classpath classes that the JVM loads differently from the model.

• Static-field access to Verifier-package or javax/ helpers runs their static initializer without analysis.
• A java/ class makes the JVM throw a SecurityException.
• A program class shadows a JDK class (org.xml.sax), so the JVM loads the JDK's version.

These cases now fail the check, and all 6 are regression tests. The review found no task among the 998 that uses such packages. After the fix, the scan still proves the same 426 no-runtime-exception and 3 valid-assert tasks, so the measurement stands unchanged.

Measured

Configuration --sv-comp, 300 s CPU, --mem15g, no SA, compared against baseline-results.jsonl. 1286 runs:

set	runs	points
A: all runs where the check proves the property (426 no-runtime-exception, 3 valid-assert), final jar	434	+470
B: every run with expected verdict false, both properties	728	0
C: other KB runs with these causes, not proven	34	0
D: other runs (40 baseline-correct, 50 random)	90	0

Net +470, 235 flips (all UNKNOWN, timeout, stall or OOM to correct SAFE), 0 losses, 0 new wrong verdicts.

The static scan of all 998 tasks:

• proves 426 of the 699 no-runtime-exception tasks with expected true;
• proves none of the 36 with expected false;
• proves 3 valid-assert tasks, none of them among the 692 with expected false.

family	property	old outcome	runs	points
MinePump	NRE	timeout	64	+128
float-nonlinear-calculation	NRE	unknown / timeout / oom	79	+158
float_unboundedloop	NRE	timeout	29	+58
argv-tasks	NRE	timeout / unknown / ok	24	+48
jayhorn-recursive	NRE	stall / unknown / timeout / oom / ok	22	+44
jbmc-regression	NRE	unknown	5	+10
algorithms	NRE	oom / timeout	6	+12
java-ranger-regression, jdart-regression	NRE	timeout	4	+8
float-nonlinear-calculation (coral5, coral46)	valid-assert	unknown	2	+4

The median CPU time of a proven run is 2.2 s.

Tests

• ExceptionFreedomCheckSpec: 63 compiled programs. 50 may throw and must never be proven; these include every counterexample from both reviews. 13 are proven.
• tests/test_property_precheck.py: result parsing per property, the command line, disabling, failure and timeout, and the verdict with a proof, including the contradiction case.
• The executor's default test suite (8787 tests) and the explorer's unit tests pass.

Known limits

• valid-assert gains only on programs that create no AssertionError at all. The context-loss and uncaught-exception downgrades are unchanged for valid-assert, and so is the downgrade for programs that are not proven.
• No interval or path reasoning (assume, null checks), and no collections or most String methods. Most of securibench, objects (nondetObject), juliet and the algorithms array programs stay unproven.
• context-loss-swat-internal-helper is not touched, so the StringCompare05 caveat does not apply.

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.