Skip to content

Move the static property pre-check from the executor into the static pre-analysis #93

New issue
New issue
Open
Open
Move the static property pre-check from the executor into the static pre-analysis#93
Milestone
SV-COMP 2027

Description

@nils-loose
nils-loose
opened on Oct 20, 2026

@solid-eureka #92 added a static, whole-program property pre-check (originally #73). It runs inside the executor jar today, but it is static analysis, not symbolic execution, so it belongs in the static pre-analysis step. Can you take a look at whether and how it fits into your analysis?

What it does

  • The class: de.uzl.its.swat.staticcheck.ExceptionFreedomCheck (ASM, about 2k lines in symbolic-executor/.../staticcheck/). It analyses the task classpath, starting from Main.main, and proves or fails to prove two things:
    • exception_free: no RuntimeException escapes main or a static initializer that may run. This is the no-runtime-exception property.
    • assertion_free: no reachable code creates an AssertionError. This is valid-assert.
  • The driver: svcomp/PropertyPreCheck.py runs it before round 0, as a subprocess with a 60 s timeout. It reads one JSON line from stdout.
  • When the property is proven: the verdict is SAFE without exploration. SWAT still runs round 0 as a cross-check; a violation there gives UNKNOWN.
  • When it is not proven (including a crash or timeout): the run is unchanged.
  • Cost: about 0.2 s CPU and 60 MB per task.
  • Effect: +470 points on the 1713-run set, with 0 wrong verdicts. It proves 426 no-runtime-exception tasks and 3 valid-assert tasks. Most of them could never be closed by exploration: MinePump, float_unboundedloop and jayhorn-recursive run into timeouts.

How it proves it (conservative everywhere; unknown → not proven)

  • Closed world. Every call goes to application code, to a modelled Verifier method, or to a whitelisted JDK method (JdkModel). Method selection over-approximates the JVM's choice, including default, private and package-private methods. Reflection, invokedynamic (except string concatenation) and method handles fail the check.
  • Instructions. Every instruction that can throw a RuntimeException (array access, field access, invoke, checkcast, division, athrow, …) must be proven safe or be covered by a handler. The proof uses an abstract interpretation that tracks nullness, int and long constants, array lengths, enum ordinals and exact types.
  • Fixpoints. Field, parameter and return facts, and may-throw, are least fixpoints over all application methods.
  • Classpath guard. Classes in platform packages fail the check.
  • Review. Adversarial reviews found 17 counterexamples. All are fixed and kept as regression programs in ExceptionFreedomCheckSpec.groovy.

Moving it into the SA: what we found

  • Option (b), move the ASM pass as is into cfg-extraction, as its own entry point. It needs no SootUp view and does not use the CFG graph.

    • The unchanged sources compile against the extractor jar, which already bundles ASM, and give identical results on all 998 tasks.
    • Effort: about 1–2 days.
    • None of the extractor review items have to be fixed first.
    • It needs the extractor jar in the SV-COMP archive (it is not shipped today), a pinned version, and a choice of test framework for the regression programs: Spock or JUnit.

  • Option (a), a port onto SootUp. This is possible, but SootUp's building blocks are too loose for a SAFE proof:

    • dispatch picks a single target and gets private and package-private selection wrong;
    • ForwardFlowAnalysis does not carry state into exception handlers;
    • any TypeHierarchy query loads the whole JDK, about +4.5 s and +1.25 GB;
    • Jimple's local types are wrong after javac reuses a slot.

    At least 8 of the 17 known counterexamples would come back by default. Estimated effort: 2–3k lines plus new review rounds.

  • The interface should stay as it is: one JSON line on stdout, plus tool and version fields. On the SWAT side only PropertyPreCheck.command() changes. The result should not go into _metadata.json: the graph SA is now valid-assert only, while most proofs are for no-runtime-exception.

A broader idea

The pre-check is the extreme case of what the SA already does for asserts: it finds the property-relevant program sites, and proves there are none. Generalised:

  1. The SA computes the relevant sites per property.
    • Under valid-assert: the asserts.
    • Under no-runtime-exception: the instructions that may throw and that the value analysis cannot discharge.
  2. SWAT then:

Questions

  1. Is an ASM pass acceptable in cfg-extraction, as a separate entry point?
  2. Will the cfg-extraction jar ship in the SV-COMP archive, and how is its version pinned? Could the pre-check ship before the graph SA is ready?
  3. Who reviews the soundness of changes after the move? A false SAFE costs −32, and this proof skips all of SWAT's downgrades.
  4. Is the "relevant sites per property" interface something you want to build towards?

🤖 Generated with Claude Code

Activity

  1. nils-loose
    added this to the SV-COMP 2027 milestone on Oct 20, 2026

  2. solid-eureka commented on Oct 23, 2026

    @solid-eureka
    solid-eureka
    on Oct 23, 2026
    Contributor

    @nils-loose Thanks for the write-up. Short version: I agree with option (b), with rejecting (a), and with the broader idea. I'd add one concrete link between the two analyses, and one caution about the downgrade idea.

    Option (b): move the ASM pass as is into cfg-extraction

    Agreed.

    • Static analyses belong together, and identical results on all 998 tasks make the move low-risk.
    • There is a precedent: the extractor already reads class files with ASM (BranchKeys, which checks SootUp's ordinals against the bytecode).
    • It should stay a separate entry point that does not build a SootUp view. Otherwise it pays the extractor's start-up of about 5 s instead of its own 0.2 s.
    • The real cost is shipping, not code: the extractor jar in the SV-COMP archive, a pinned version, and a test framework for the regression programs. I'd keep Spock, since the specs exist.

    Option (a): a port onto SootUp

    Agreed that it should not be done. Our experience with the graph SA supports it; on top of your list:

    • getStmts() order is not bytecode order, not even within one source line (e.g. for a switch on a String, or javac's finally copies);
    • SootUp's line attribution is occasionally wrong;
    • exceptionalSuccessors() is unordered.

    The graph SA can live with that, because it marks what it cannot prove as unknown and checks itself against the trace. A proof that skips every downgrade cannot afford it.

    Interface

    Agreed: keep the one JSON line, and keep it out of _metadata.json.

    The broader idea: relevant sites per property

    Agreed. This is where the SA was meant to go. Two additions:

    1. Connect the two analyses, not only their location.
      • The problem: under no-runtime-exception, the graph today would mark almost every unguarded instruction as a possible exception (the pseudo exception types ?Exception). That leaves next to nothing to prune.
      • What the check offers: its value analysis is what could discharge most of them: non-null receivers, in-bounds constant indices, non-zero divisors, exact types for casts.
      • The missing piece is naming the same instruction on both sides. The branch-key scheme already does that between ASM and SootUp (owner.name(desc)|line|kind|ordinal, with ordinals checked against the bytecode). So the check could export its "cannot throw" facts by key, and the extractor could drop those exception edges.
      • Then: the relevant sites are the escapes that remain. An empty set gives SAFE, as the pre-check does today.
    2. Caution with "downgrade only when the loss is on a path to a relevant site".
      • Why: context and precision loss are data problems, not only control problems. A concrete value from a lossy library call, on a path that cannot reach any site, can still flow into a later branch that decides whether a site is reached.
      • So the condition must be data-based: "on a path to a relevant site" has to mean "may influence a branch on such a path", which needs data-flow information, roughly the check's facts extended to symbolic dependence.
      • The risk: decided by control flow alone, it reintroduces false SAFEs.
      • Before building it: I'd measure what it would gain (your estimate: the 55 float-nonlinear runs).

    Your questions

    1. An ASM pass in cfg-extraction as a separate entry point? Yes.
    2. Shipping and pinning.
      • The extractor jar has to ship anyway if the graph SA is ever used in the competition.
      • I'd pin it by tag: SWAT already depends on cfg-extraction's graph format and branch keys, so the two need a known-compatible pair anyway.
      • The pre-check can ship first, with the graph SA off in the archive. The two do not depend on each other.
    3. Soundness review after the move.
      • Keep the adversarial reviews and the regression programs.
      • Add a required gate before releases: a run of the check over the whole sv-benchmarks set, comparing every proof with the expected verdict (0 contradictions). That is the counterpart of the marking oracle we run over the graphs (tests/check_marking_on_graphs.py).
    4. Build towards the "relevant sites per property" interface? Yes, in steps:
      1. Move the check as in (b).
      2. Share instruction keys between the check and the graph.
      3. Only then prune under no-runtime-exception, re-adding the graph SA's guards for that property: entry points outside main's call tree, callbacks from library code, no pruning at unchecked pairings.

    🤖 Generated with Claude Code

  3. solid-eureka commented on Oct 24, 2026

    @solid-eureka
    solid-eureka
    on Oct 24, 2026
    Contributor

    Step 1 of the plan above (move the check as in (b)) is implemented. It is on its own branch in both repositories:

    • SWAT: issue-93-precheck-in-cfg-extraction, based on niklas/dev
      • 9f71629 Run the property pre-check from cfg-extraction
      • b8ff4ba Ship the property pre-check jar in the SV-COMP archive
    • cfg-extraction: issue-93-precheck-in-cfg-extraction, based on find-assertions
      • 825c43e Add the property pre-check from SWAT as its own entry point

    What changed

    • cfg-extraction
      • ExceptionFreedomCheck and its four helper classes moved unchanged, except for the package (de.uzl.its.cfg.staticcheck). It is a separate entry point and builds no SootUp view (about 0.13 s per task).
      • The JSON line is unchanged, plus tool and version fields (git describe at build time).
      • A new precheckJar task builds cfg-extractor-precheck.jar (260 KB) with only the check and ASM. That is what the archive ships, so no SootUp licenses have to be listed. The fat jar contains the check too; its resolved dependencies are unchanged.
      • The Spock spec moved too (63 cases, all pass).
      • scripts/precheck_gate.py is the release gate from point 3: it runs the check over sv-benchmarks and fails on any proof that contradicts an expected verdict.
    • SWAT
      • PropertyPreCheck runs cfg-extractor-precheck.jar: from --precheck-jar, else next to symbolic-explorer/ (archive layout), else ../cfg-extraction/build/libs/ (workspace). Without it the check is skipped as missing_jar (not proven). The cfg-extraction version is recorded in stats.json.
      • The check and its spec are removed from the executor.
      • Shipping: cfg-extraction.ref pins the cfg-extraction tag. CI checks cfg-extraction out at that tag and builds the jar. package-svcomp.sh requires it and ships it as cfg-extraction/cfg-extractor-precheck.jar; the license file lists its ASM. check-svcomp-package.sh also runs the pre-check in the competition image.

    Verification

    • Identical results: the old (executor) and the new (cfg-extraction) check give identical results on all 1342 tasks of sv-benchmarks and swat-benchmarks.
    • Gate: 998 tasks, 426 no-runtime-exception and 3 valid-assert proofs, 0 contradictions, 0 crashes. This matches the numbers in the issue.
    • Tests: the executor tests (11025 after the move) and the explorer tests pass.
    • End-to-end: AbstractChart_exceptionless is proven and answered SAFE, both in the workspace and from a locally built archive. The archive's smoke test passes.
    • Not run: check-svcomp-package.sh itself (no Docker on the machine I used).

    Three decisions left before this can be merged

    1. CI access to cfg-extraction. cfg-extraction is private, so SWAT's CI needs a secret CFG_EXTRACTION_TOKEN with read access to it. The alternative is to make cfg-extraction public. Without either, the build job fails at "Check out cfg-extraction" (run), and the test and package jobs, which depend on it, are skipped. Pull requests from forks do not get secrets, so their builds would fail the same way.
    2. The tag. cfg-extraction.ref names v0.1.0, which does not exist yet. It has to be created (on 825c43e, or wherever the cfg-extraction branch ends up after review) and pushed. Before every later move of the ref, precheck_gate.py has to pass.
    3. A license for cfg-extraction. The repository has no license file, but its code would now ship in the public SV-COMP archive. It needs one, presumably the same as SWAT's.

    Steps 2 and 3 of the plan (shared instruction keys between the check and the graph, then pruning under no-runtime-exception) build on this and are not started.

    🤖 Generated with Claude Code

  4. solid-eureka commented on Oct 24, 2026

    @solid-eureka
    solid-eureka
    on Oct 24, 2026
    Contributor

    Steps 2 and 3 are implemented too, plus fixes for two walk desyncs found along the way. Everything is in PR #108 (into dev, also merged into niklas/dev) and the cfg-extraction branch issue-93-precheck-in-cfg-extraction.

    Step 2: shared instruction facts

    • The check exports per-site facts (ExceptionFreedomCheck.siteFacts, --sites on the command line):
      • Guards (array access, division, array allocation) are named by their exact branch key.
      • Statement sites (field access, casts, throw, monitors, arraylength, calls) are grouped by method, line and kind. A group is safe only if every instruction in it is.
      • Under a closed world, the methods reachable from Main.main use the check's facts. Everything else only uses what each method shows itself, which holds in any world.
      • For a call, only the call itself counts (null receiver, library callee). An application callee's exceptions are in its own statements.
    • The extractor marks nodes cannotRaise (RaiseSites). A line is only used if its site kinds match the bytecode, which guards against SootUp's occasional wrong line numbers. Over 998 tasks: 99.95% of statement sites matched, 86% are safe, and 564 guards are safe. The graph structure is identical with and without facts.
    • SAGraph gives the exception side of a guard that cannot raise a dead node.

    Step 3: pruning under no-runtime-exception

    • Targets: the extractor emits runtimeExceptionPointIds: every site that may raise, plus uncaught[T] nodes of RuntimeException types. SWAT chooses the target list by property.
    • The existing guards still apply: a graph with code outside main's call tree is rejected, callbacks and <clinit> are masked, and unchecked pairings are never pruned.
      • A library call is a target unless the check rules out both an exception and a callback, so callbacks need no extra points.
      • An exception escaping a static initializer reaches main as an ExceptionInInitializerError, an Error, so it is not a violation.
    • Results (736 tasks, 300 s):
      • Sound: no false SAFE. 325 tasks have no target points, and all of them are expected true.
      • Queries on solved SAFE tasks drop by a third, but no new verdicts. The pre-check already proves 426 tasks, and the extractor costs 3 to 6 s per task.
      • So it is opt-in in the harness: svcomp test run --sa-no-runtime-exception.

    Walk desyncs (also under valid-assert)

    1. UtilInstrumented.refEquals changed in the dev merge, but the extractor still modelled the old two-branch helper. Its branch count depends on runtime types, so the executor now flags the helper's branches like callbacks, and the graph only has the comparison's own if.
    2. Verifier.nondetObject: the executor runs it as factory.createObject(). The extractor now expands and keys it that way.

    Valid-assert with SA (978 tasks): desyncs 73 → 0, correct verdicts 812 → 814. sa-soundness: 114 → 115.

    Still open

    The three decisions from my previous comment: the CFG_EXTRACTION_TOKEN secret (or making cfg-extraction public), the v0.1.0 tag, and a license for cfg-extraction. CI on the PR fails at the cfg-extraction checkout until they are settled.

    🤖 Generated with Claude Code

  5. solid-eureka
    added 6 commits that reference this issue on Oct 27, 2026

    Run the property pre-check from cfg-extraction (#93)

    28b8a38

    Ship the property pre-check jar in the SV-COMP archive (#93)

    0313fca

    Cut the exception side of guards that cannot raise (#93)

    90ca67a

    Prune by the graph under no-runtime-exception too (#93)

    d2e0aa0

    CI: check out cfg-extraction without a token (#93)

    0746098

    CI: check out cfg-extraction without a token (#93)

    af9fb0f

  6. solid-eureka commented on Oct 27, 2026

    @solid-eureka
    solid-eureka
    on Oct 27, 2026
    Contributor

    The three open decisions are settled:

    1. CI access: cfg-extraction is public now. The CFG_EXTRACTION_TOKEN line is removed from the workflow (af9fb0f on Move the property pre-check to cfg-extraction; prune under no-runtime-exception (#93) #108's branch, also in Relevance (slicing) and loop summaries; rebased onto svcomp27/overnight-solver-perf #109).
    2. Tag: v0.1.0 exists (cfg-extraction master: the pre-check plus the license). v0.2.0 adds the data-flow facts for the relevance analysis in Relevance (slicing) and loop summaries; rebased onto svcomp27/overnight-solver-perf #109, with an unchanged pre-check; Relevance (slicing) and loop summaries; rebased onto svcomp27/overnight-solver-perf #109 pins it. precheck_gate.py passed at both tags (998 tasks, 0 contradictions).
    3. License: cfg-extraction is MIT-licensed (LICENSE from GitHub's MIT template). Both jars carry it, so the SV-COMP archive ships it with the pre-check jar.

    cfg-extraction's issue-93-precheck-in-cfg-extraction is merged into its master. What's left is merging #108 (or #109, which contains it).

    🤖 Generated with Claude Code

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions