[nils-loose]

What / why

WitnessCreator 1.0 replaces the Java/Gradle tool by a standalone, stdlib-only Python package (witnesscreator, Python >= 3.10, tested on 3.10/3.13/3.14 — 3.14 is the SV-COMP 2027 image). It produces Java violation witnesses in the YAML format 2.3 (required for Java in SV-COMP 2027) and the legacy GraphML format, ports every behaviour of #1 (the Java YAML implementation) and fixes the review findings of that branch. It stays usable by tools other than SWAT: the library API and the event file carry plain data, nothing SWAT-specific.

Builds on #1 (branch feat/yaml-witness-2.3); the Java sources, Gradle files and StringTemplate templates are removed.

Library API

from witnesscreator import Task, Location, NondetReturn, Frame, Violation, write_witnesses

task = Task(input_files=["../common/", "Main.java"], property_file="valid-assert.prp",
            producer_name="SWAT", producer_version="svcomp27", base_dir=None)
values = [NondetReturn("nondetInt", "int", "42",
                       Location(class_name="pkg.Main", source_file="Main.java", line=12, call_index=0))]
violation = Violation("java.lang.AssertionError", [Frame("pkg.Main", "Main.java", 17)])
write_witnesses(task, values, violation, out_dir="output", formats=("yaml", "graphml"))
# -> {"yaml": Path("output/witness.yml"), "graphml": Path("output/witness.graphml")}

Never raises for bad data (logs on witnesscreator, each format written independently); render_yaml / render_graphml return strings; dump_events / read_events for the event file. Location additionally takes an optional method (the caller's descriptor, only used for the GraphML assumption.scope).

CLI

• witnesscreator events --events E.jsonl --property P.prp --input PATH... --out-dir D [--format yaml|graphml|both] [--producer-name N --producer-version V] — JSON-lines serialization of the objects above.
• witnesscreator legacy [<b64>] [--markers-file F] ... — SWAT's [WITNESS]/[WITNESS_TARGET] markers, 4- and 7-field payloads.
• witnesscreator <b64> <dir> [--input ..] [--property ..] [--out ..] [--producer-version ..] — the Java tool's command line, unchanged (drop-in: witnesscreator instead of java -jar WitnessCreator.jar).
• Exit 0 once something was written, 1 if nothing could be written, 2 for usage errors.
• Also shipped as a single-file witnesscreator.pyz (zipapp).

Fixes vs. the Java branch (#1)

• Escaping: Java literals escape every char >= 0x7f as \uXXXX (surrogate pairs beyond the BMP); YAML double-quoted scalars are plain ASCII (\uXXXX, \UXXXXXXXX); GraphML text (assumptions, scopes, paths, producer) is XML-escaped — the Java version wrote e.g. s1.equals("<bad/>") unescaped into the XML (7 securibench runs).
• Target frames: package must match (file path or package declaration); java., javax., jdk., sun., de.uzl.its.swat. frames skipped; name-only fallback only for value locations; exactly one final target segment when a target is known, warning otherwise (schema-valid file still written).
• Columns: computed on source with comments and string/char literals blanked out; nondet*( needs a word boundary; call_index-th call's closing ); target column = assert/throw keyword, else first token (skipping }/{/else).
• GraphML assumptions: \result = <value>; / \result.equals("…"); (what wit4java's parser extracts) instead of a variable name guessed from the source line (x = 3, or true when the line had no Verifier, which made wit4java parse true as an int).
• Literals as in Emit YAML violation witnesses (format 2.3) #1: L only outside int range, char literals, f suffix, Float.isNaN(\result), \result == Double.POSITIVE_INFINITY, -0.0 preserved, \result.equals("…").

Testing

• 101 pytest tests (unit: literals/escaping/markers/events/locations; golden e2e on copies of SV-COMP tasks incl. the GDart example task of sv-witnesses — our output equals the official ExDarko_false.witness-2.3.yml content —, jbmc-regression return2/StringValueOf08 (NumberFormatException thrown in the JDK)/exceptions16, jdart float (NaN/±Infinity/-0.0), MinePump (multi-file + package), a synthetic task (inner class, two calls on one line, unicode/control chars, packaged class); CLI incl. zipapp). All pass on 3.10, 3.13, 3.14. Every YAML is parsed with PyYAML, checked for exactly one final target segment and linted with WitnessLint 2.3 when available (CI installs it); GraphML parsed as XML.
• Java-vs-Python equivalence on the 35 marker sets of the 40-task runs-debug campaign (feat/yaml-witnesses worktree): 35/35 YAML identical (modulo uuid/creation_time); GraphML structurally identical on 28/35, the 7 differences are the fixes above (unescaped <bad/> in Java's XML; Basic4 true → \result = 3;). wit4java verdicts on the GraphML witnesses are identical for Java and Python on all 32 distinct tasks (19 correct, 2 spurious, 11 could-not-validate — same both sides); WitnessLint: 32/32 well-formed.

Breaking changes for Java users

• No jar, no witnesses/*.st, no Gradle. Replace java -jar build/libs/WitnessCreator.jar ARGS by witnesscreator ARGS (or python3 witnesscreator.pyz ARGS); arguments unchanged, no particular working directory needed.
• GraphML content: \result = …; assumptions, XML escaping, sourcecodelang/specification graph data. Stricter target resolution (package match). Non-ASCII escaped in Java literals.
• Log output goes to stderr.

Release steps

1. Merge; git tag v1.0.0 && git push origin v1.0.0.
2. CI builds wheel + sdist + witnesscreator.pyz + SHA256SUMS and attaches them to the GitHub release.
3. Install: pip install git+https://github.com/SWAT-project/WitnessCreator@v1.0.0 or the .pyz from the release.

🤖 Generated with Claude Code