Add packaging mechanism to automatically build SV-Comp `zip` by nils-loose · Pull Request #30 · SWAT-project/SWAT

nils-loose · 2026-06-24T12:57:21Z

No description provided.

nils-loose · 2026-06-29T14:12:11Z

+  SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content
+  SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6


@k0lja Can you propose a different mechanism, perhaps another repository here that publishes the required files, I dont want to reference zenodo here in the CI

In addition, the venv we are using is built on the specific ubuntu version required by sv-comp. updating the dependencies is a hassle atm. Can you check if it could be possible either here or in the supporting repo (for the above) you can actually build the venv based on the requirements (pip freeze the current venv) as part of the ci there? this would make updating the venv much easier

nils-loose · 2026-06-29T14:15:48Z

+    - name: Build WitnessCreator JAR
+      run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar


As discussed could you also move the full witness creator into its own repo that publishes an artifact we can use here?

nils-loose · 2026-06-29T14:17:07Z

@@ -18,8 +23,142 @@ jobs:
        distribution: 'temurin'
    - name: Setup Gradle
      uses: gradle/actions/setup-gradle@017a9effdb900e5b5b2fddfb590a105619dca3c3 # v4


While you are at it, could you also check why the setup-gradle v4 is referenced using this hash I assume? is that the proper way to do that? (I know this is older then your changes but I was wondering for some time)

nils-loose · 2026-06-29T14:17:49Z

This entire package of supporting file should then also move into the supporting repo I guess?

…peatable) id Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…y listed handler) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…it continues Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…n initializer, finally) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…modelled exceptions) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Two branches of one trace can share an iid (switch case index wraps at 16, loop counter at 64), and one got the other's constraint: false SAFE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…inside) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…omp27/integration

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…ounds - An if inside a diamond's side whose own sides are blocks again (and that only its own jumps enter) becomes a nested op: the simulation evaluates its condition and merges its sides by it. javac makes such an if-else meet at the outer if's end, so pending merges per join are a stack, applied innermost first. - IDIV/IREM by a nonzero constant are allowed in sides (they cannot throw). - Counting loops may run while i <= b (step +1) or i >= b (step -1). The closed forms count from b + step; they are wrong only for b at the type's limit, where the loop never ends and nothing after it runs, so they add no execution that exists. New loop-summary families count-even (nested, i % 2) and count-upto (<=). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Fixtures that build an SVCompDriver without __init__ lacked the attributes the relevance work added (sa.slicing, pending_projected, args). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

v0.2.0 adds the data-flow facts the relevance analysis and loop summaries need, and the extractor fixes for the HTTP driver; the property pre-check is unchanged from v0.1.0 (gate: 0 contradictions on 998 tasks). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

cfg-extraction is public now, and the tag cfg-extraction.ref names exists. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Otherwise the behaviour would change when running in debug mode, which is confusing.

…prefix - The explorer's console handler logs from INFO on (--console-log-level), the log files still from DEBUG on. The root logger starts at INFO instead of DEBUG, so the 'DEBUG:log:Setting up logger' lines are gone. - The harness relays a subprocess' output as it is, instead of logging each line again with its own timestamp and level. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

- The explorer logs relayed executor output (log.RELAYED) as it is, without its own timestamp, thread and level in front of the executor's. - The harness reads a task's output while it runs and, in single mode, prints each line when it arrives instead of all of them at the end. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

get_verdict_logger() returned the explorer logger, so verdict.log stayed empty. The verdict still goes to explorer.log too, and is printed once on the console. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ThreadHandler.init() created a Z3 SolverContext that nothing ever read, and never closed the previous one. Six test classes called it before every test case, so each case leaked a whole Z3 context (about 17 MB): the executor tests peaked above 22 GB, and GitHub's runner (16 GB) was shut down in the middle of :symbolic-executor:test. Without it the tests peak at 1.9 GB, and the executor no longer creates an unused Z3 context at the start of every run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ThreadHandler.init() created a Z3 SolverContext that nothing ever read, and never closed the previous one. Six test classes called it before every test case, so each case leaked a whole Z3 context (about 17 MB): the executor tests peaked above 22 GB, and GitHub's runner (16 GB) was shut down in the middle of :symbolic-executor:test. Without it the tests peak at 1.9 GB, and the executor no longer creates an unused Z3 context at the start of every run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit c17c0ef)

Since 373384d the marker is no tree level: Tree.structural keeps it as the unmodelled_exception flag on the node after it, and Tree.add is the only place that builds nodes. The walk's check for a marker node could only be reached by hand-built trees in test_sa_walk, which now set the flag instead. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

dfs (strategy/DFS.py) now reads as its three steps per branch: pair it with the graph (_pair), prune, slice (_classify). How a branch was paired is one of verified, resynced, unverified, lost or masked, and the walk counts those (Tree.walk) and logs one line per selection ("[DFS] Walk: ..."), also written to stats.json (static_analysis.last_walk). The walk state is a named tuple instead of an 8-tuple; dfs loses the parameters only it used itself (visited, clinit_depth, sa_stack, sa_index, trace_stack). Merged and sliced branches are one classification. SAGraph: target points are SANode.isTarget, reachesTargetSameLevel and targetDistance (no longer named after asserts). Dropped what nothing needs any more: graphs without return sites (and their context-insensitive marking), isPhantomGuard, the RETURN edge lists, the child accessors, and the call site's fall-through to its one callee. SANode.handler_for replaces three copies of the handler lookup. Relevance: the unused constructor parameter is gone, the closure of methods running a relevant branch is computed by one helper. Node and Leaf have class defaults for every per-node flag, so neither the walk nor tests need getattr fallbacks. Removed --sa-retry-without (explorer and harness): a guard against false SAFE from SA bugs from before keys checked the walk; desyncs now turn SAFE into UNKNOWN instead. The analysis results are unchanged: every node's summaries, relevance, regions and distances are the same as before on all 2201 graphs of sv-benchmarks and swat-benchmarks (valid-assert and no-runtime-exception). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…m too Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

StrategyService used a module logger, which reaches neither explorer.log nor the console: its walk summary (and, before, the relevance and loop-state lines) were never seen. It now uses the explorer's logger; is_symbolic_branch's two INFO lines per new candidate are one DEBUG line. The walk line uses the documented terms: [DFS] Walk: 34 branches (33 verified, 0 resynced, 0 unverified, 0 lost, 1 masked), 12 sides pruned; 32 sliced, 0 merged, 0 covered, 0 poisoned Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The SA modules (DFS, StrategyService, SAGraph, Relevance, the tree classes, StaticPreAnalysis) pass mypy with --check-untyped-defs --disallow-untyped-defs --disallow-any-generics. Named types instead of bare tuple/dict/set: - SAGraph: Location and Effect (the data-flow facts: dataflow is tuple[Effect, ...], control tuple[Location, ...]), CallFacts (a TypedDict for the `call` field), ExceptionChain, TraceFrames and TraceStack. LOST is an enum sentinel, so `is LOST` narrows. - Relevance: CfgNode (a graph node or a virtual EXIT/EXIT_EXC/END), Method (str | None: nodes without method metadata). - DFS: Pairing and Role are Literal types, OpenRegions names the region list; dfs's walk state is fully typed. - Node: Ident and BranchName (a candidate's identity); Branch: Position and PositionedState (loop-head states). - StrategyService.select_branch takes named parameters instead of **kwargs; `-> list()` return annotations (a call, not a type) are list[str]. Where a value is Optional in general but always set where it is read, there is now one accessor with an assertion instead of an unchecked read: SANode.sides() (a branch's two successors) and resume_site() (a call site's return site). dfs keeps the verified graph node in one variable (None unless the pairing was verified), which is what the pruning and slicing checks. Also: the Leaf docstring is its __doc__ again, Node caches its depth in a declared field (depth_cache) instead of a getattr'd _depth, and loop variables that were reused with another type in Relevance are renamed. Every node's analysis results are unchanged on the 2201 graphs from sv-benchmarks and swat-benchmarks; all explorer tests pass. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Relevance (slicing) and loop summaries; rebased onto svcomp27/overnight-solver-perf

Brings in the overnight solver performance work (#96, #98, #99), the property pre-check in cfg-extraction (#108), and relevance slicing and loop summaries (#109). The one conflict, in Transformer.java, comes from the #110 fix having been committed on both branches; resolved as on the overnight branch. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> # Conflicts: # symbolic-executor/src/main/java/de/uzl/its/swat/instrument/Transformer.java

Brings in the SA cleanup (one vocabulary for the walk, legacy graph format and --sa-retry-without removed, walk counts in the log and in stats.json), full type annotations of the SA code, and the console log changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Against dfs (300 s, with SA, 2026-11-03), coverage found 6 more violations on swat-benchmarks and 4 more on sv-benchmarks valid-assert that dfs did not find in five runs, lost only a flaky one, and left every SAFE verdict as it was. On no-runtime-exception it missed one real bug dfs finds (WeibullGenerator_exceptionless, whose label is wrong and is fixed locally in the sv-benchmarks checkout). The harness now always passes --search-order, so that an explicit --search-order dfs is not lost to the explorer's default. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…fault Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

The archive only shipped the property pre-check, and run_swat.py passed no --sa-path, so SA never ran there. Now: - CI builds cfg-extraction's fatJar next to precheckJar, and package-svcomp.sh ships it as cfg-extraction/cfg-extractor.jar. - The explorer takes the extractor jar itself with --sa-jar (--sa-path still takes a checkout). - run_swat.py passes --sa-jar under valid-assert only (as the harness does) and --target Main. Without --target the graph's entry was None and the extractor failed, silently leaving the run unpruned; StaticPreAnalysis now also defaults the entry to Main, the class the executor runs. - third_party_licenses.py lists the fat jar's components (needs its META-INF/swat-third-party.json from cfg-extraction's fatJarComponentList) and maps SootUp's and JGraphT's license names. - check-svcomp-package.sh fails unless the smoke test's static pre-analysis loaded its graph. Needs a cfg-extraction release with fatJarComponentList in cfg-extraction.ref (v0.2.0 has none). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

… static pre-analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

nils-loose commented Jun 29, 2026

View reviewed changes

solid-eureka and others added 29 commits October 16, 2026 10:16

Find the target of a divergence check by its position, not by its (re…

fc8e88e

…peatable) id Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

RESULTS.md: add the fixes of 2026-10-15/16 and the runs after them

71dc9cb

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SA graph: model exceptions of unknown type (pseudo types caught by an…

9ce3d15

…y listed handler) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Stop trusting the SA graph after an exception it does not model

552bcc0

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Close a static initializer left by an exception once the frame below …

86c0da2

…it continues Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

swat-benchmarks: add S2 reproducers (callee-decided NPE, Error from a…

f0ccb96

…n initializer, finally) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Document the S2 fix (unmodelled exceptions) in CLAUDE.md and RESULTS.md

fce1bec

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

swat-benchmarks: add exception-dispatch family (SA precision after un…

1e6cdea

…modelled exceptions) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Executor: record HANDLER_ENTRY events

6fb7464

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SA walk: resume at the handler after an unmodelled exception

50ce3ff

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: handler resumption tasks

7f6aa4c

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Docs: handler resumption results

b3a08e7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Executor: report branch keys and stack changes in the trace

1568fec

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SA walk: detect desyncs by key and resync after losing the graph

fc817ee

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Docs: branch keys, desync detection and resync

66a5d02

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Remove handler resumption (covered by resync)

8f5505e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Mask library callbacks in the SA walk

aa20dab

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: library callback tasks; docs

8dab346

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: library-callback-assert (known false SAFE with SA)

d8289a7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Flag to turn off callback targets (--sa-no-callback-targets)

6ced24e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Key the solver's constraint cache by tree node, not iid

f6197d3

Two branches of one trace can share an iid (switch case index wraps at 16, loop counter at 64), and one got the other's constraint: false SAFE. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

sa-soundness: exec-loop-iid-wrap

9046cd0

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Keep Z3's jar off the extractor's classpath

69c6b83

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

SA walk: call sites with several callees (union in summaries, resync …

98eb95d

…inside) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Docs: callback targets, multi-target calls, solver cache fix

65aab6e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Remove dead code left from the SA integration

604ba0a

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Remove generated timing plot, ignore it

8f0501b

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge remote-tracking branch 'origin/feat/witness-via-trace' into svc…

2f8e874

…omp27/integration

Merge #65 (static pre-analysis) into the integration branch

e65dbe2

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

solid-eureka and others added 30 commits October 27, 2026 14:46

prefer_small: tolerate solutions of any shape

895deaa

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Document the loop summary next steps, small models and deadlocks

cc607da

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Explorer tests: driver fixtures for slicing and projected divergence

b319354

Fixtures that build an SVCompDriver without __init__ lacked the attributes the relevance work added (sa.slicing, pending_projected, args). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

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

0746098

cfg-extraction is public now, and the tag cfg-extraction.ref names exists. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Bring swat-debug.cfg up-to-date with sv-comp.cfg

1ada655

Otherwise the behaviour would change when running in debug mode, which is confusing.

Log traces as DEBUG

d38fe31

Log possible branch IDs as DEBUG

27d7720

Write the verdict to verdict.log

18de9b1

get_verdict_logger() returned the explorer logger, so verdict.log stayed empty. The verdict still goes to explorer.log too, and is printed once on the console. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Add comments

6c4b590

dfs: one branch per role; test the walk counts; HTTP stats record the…

04a0ae5

…m too Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge pull request #109 from SWAT-project/niklas/relevance-slicing

66da216

Relevance (slicing) and loop summaries; rebased onto svcomp27/overnight-solver-perf

Merge niklas/coverage-default into dev: --search-order coverage by de…

8c8394a

…fault Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

cfg-extraction.ref: v0.2.1 (fat jar with component list, no GPL graph4j)

b24964c

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Merge niklas/svcomp-sa-package into dev: the SV-COMP archive runs the…

15759c0

… static pre-analysis Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Navigation Menu

Repository navigation

Add packaging mechanism to automatically build SV-Comp `zip` - #30

Add packaging mechanism to automatically build SV-Comp `zip`#30
nils-loose wants to merge 364 commits into
mainfrom
dev

nils-loose commented Jun 24, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

nils-loose Jun 29, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		SVCOMP_REFERENCE_URL: https://zenodo.org/api/records/17748741/files/swat-verify.zip/content
		SVCOMP_REFERENCE_MD5: 8c776d19ac33ecf5c1c7441d16cc18a6

		- name: Build WitnessCreator JAR
		run: ./gradlew --no-daemon :targets:sv-comp:WitnessCreator:shadowJar

Conversation

nils-loose commented Jun 24, 2026

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

nils-loose Jun 29, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants