Repository navigation
Emit YAML violation witnesses (format 2.3) - #54
Merged
Merged
Conversation
SV-COMP 2027 requires Java violation witnesses in the YAML format (version 2.3); WitnessCreator writes them from the executor's witness markers. This supplies what the markers were missing: - [WITNESS] markers now carry the index of the nondet call on its source line (per class, bytecode order = evaluation order), the JVM type descriptor of the value and the class' SourceFile attribute, so WitnessCreator can place the function_return waypoint at the closing parenthesis of the right call, render a typed Java literal and find the file of non-public or inner classes. - A new [WITNESS_TARGET] marker with the uncaught throwable and its stack trace is emitted by Witness.recordTarget, which the surrounding try/catch of main now calls instead of printStackTrace (the trace is still printed). WitnessCreator derives the target waypoint from the innermost frame inside the task sources. - Negative zero is recorded as -0.0 (BigDecimal has no sign for zero). - Harness (lib/witness.py) and competition wrapper (run_swat.py) pass both markers, the task's input paths and the property file to WitnessCreator (--input/--property/--out); sources are no longer copied around. Optional WitnessLint via SWAT_WITNESSLINT. - The package smoketest requires witness.yml with a target waypoint. Requires WitnessCreator >= the YAML-capable release (feat/yaml-witness-2.3); the CI pin WITNESS_CREATOR_VERSION/SHA256 must be bumped with it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.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.
Executor and harness changes for YAML violation witnesses (format 2.3). Closes #45 once the WitnessCreator release is pinned.
Draft until: SWAT-project/WitnessCreator#1 is merged and tagged (
v0.2.0); then bumpWITNESS_CREATOR_VERSION/WITNESS_CREATOR_SHA256in.github/workflows/gradle.yml. With v0.1.1 the new CLI is not understood: verdicts are unaffected, but no witness is written and the updatedsmoketest.shfails. Expect overlap with #52 (gradle.yml, package scripts).Changes
[WITNESS]markers carry the nondet call index on its source line (per class, bytecode order = evaluation order), the value's type descriptor and the class'SourceFileattribute[WITNESS_TARGET]marker:Witness.recordTargetreplacesprintStackTracein main's surrounding try/catch (trace still printed); covers AssertionError and RuntimeException-0.0recorded with its signlib/witness.pyandrun_swat.pypass markers, input paths and the property file to WitnessCreator (--input/--property/--out); sources are no longer copied. Optional lint viaSWAT_WITNESSLINTsmoketest.shrequireswitness.ymlwith a target waypointtargets/sv-comp/WitnessCreator/gitignored (runtime from the release)Testing
See SWAT-project/WitnessCreator#1: 40 tasks, WitnessLint 2.3 31/31, target on 27/27 violations, wit4java (GraphML) 23/27.
🤖 Generated with Claude Code