[SVCOMP] Add support for sv-witness generation in 2.2. format - #1102
Open
hernanponcedeleon wants to merge 1 commit into
Open
hernanponcedeleon wants to merge 1 commit into
hernanponcedeleon wants to merge 1 commit into
Conversation
hernanponcedeleon
changed the title
Performance comparisonLinux x64Benchmark detailsMemory model: vmm
Memory model: aarch64
Memory model: power
Total
4 benchmark(s) omitted because both averages were below 5 seconds. macOS ARM64Benchmark detailsMemory model: vmm
Memory model: aarch64
Memory model: power
Total
|
ThomasHaas
reviewed
Sep 14, 2026
Comment on lines
+25
to
+45
| // Add program-order (po) edges between consecutive events of each thread. | ||
| for (var thread : model.getThreadModels()) { | ||
| final List<EventModel> threadEvents = thread.getEventModels(); | ||
| for (int i = 1; i < threadEvents.size(); i++) { | ||
| addEdge(successors, threadEvents.get(i - 1), threadEvents.get(i)); | ||
| } | ||
| } | ||
|
|
||
| final Set<RelationModel.EdgeModel> coherence = relationEdges(model, CO); | ||
| for (RelationModel.EdgeModel edge : coherence) { | ||
| addEdge(successors, edge.from(), edge.to()); | ||
| } | ||
| for (RelationModel.EdgeModel readFrom : relationEdges(model, RF)) { | ||
| addEdge(successors, readFrom.from(), readFrom.to()); | ||
| for (RelationModel.EdgeModel co : coherence) { | ||
| if (co.from().equals(readFrom.from())) { | ||
| // fr = rf^-1 ; co | ||
| addEdge(successors, readFrom.to(), co.to()); | ||
| } | ||
| } | ||
| } |
Collaborator
There was a problem hiding this comment.
Doesn't the ExecutionModelNext already contain usable hb relation? Is the recomputation here necessary?
Comment on lines
+47
to
+49
| // TODO: Extract this deterministic, cycle-rejecting topological sort into a general utility. | ||
| // Use Kahn's algorithm to construct a topological ordering. The in-degree records how many | ||
| // predecessors of each event still need to be added to the result. |
Collaborator
There was a problem hiding this comment.
Well, DependencyGraph.from(events, successors) already computes this. No TODO needed :).
This subsumes essentially all of the following code.
Comment on lines
+34
to
+43
| import java.util.ArrayList; | ||
| import java.util.HashMap; | ||
| import java.util.HashSet; | ||
| import java.util.HexFormat; | ||
| import java.util.LinkedHashSet; | ||
| import java.util.List; | ||
| import java.util.Map; | ||
| import java.util.Optional; | ||
| import java.util.Set; | ||
| import java.util.UUID; |
Comment on lines
+62
to
+64
| public static Optional<SvcompWitness> forViolation( | ||
| ExecutionModelNext model, VerificationTask task, IREvaluator evaluator) | ||
| throws IOException { |
Collaborator
There was a problem hiding this comment.
Here you can see how our current model sucks. Despite having the model, you still need an IREvaluator because the model has not enough information :(.
Comment on lines
+125
to
128
| public Output getOutputFromSolver(TaskSolver solver, Path programPath) { | ||
| if (solver instanceof VerificationTaskSolver verificationTaskSolver) { | ||
| return getOutputFromSolver(verificationTaskSolver, programPath); | ||
| } |
Collaborator
There was a problem hiding this comment.
With program.getInputPath() as metadata, I think the second parameter can be fully removed from all methods with the exception of getOutputFromException.
I always disliked that parameter and it was only there due to lack of source metadata in Program.
I think you can (and should) cleanly split the PR into two:
(1) Add source metadata to Program, update ProgramParser to add the metadata when parsing, update OutputLogger to use that data and get rid of the programPath parameter.
You can also put all other minor changes in this PR (e.g. EnvironmentInfo.getVersion().
(2) Add SVCOMP witnesses.
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
2 participants
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.
Summary
This PR adds support for generating violation witnesses in the SV-Witness 2.2 YAML format. It supports reachability, data-race, overflow, and memory-safety violations.
The generated witnesses describe a coarse concurrent execution containing the relevant thread ordering, assumptions, and violation targets.
Validation
The 30 fastest successful SV-COMP 2026
false(unreach-call)benchmarks were tested (using the only two available validators for the new format) with a 30-second limit per tool.Most unsuccessful validations resulted from timeouts or unsupported features in the validators.