[WIP][SVCOMP] Add support for sv-witness generation in 2.2. format

dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java

@@ -21,6 +21,8 @@
 import com.dat3m.dartagnan.verification.model.ExecutionModelManager;
 import com.dat3m.dartagnan.verification.model.ExecutionModelNext;
 import com.dat3m.dartagnan.witness.WitnessType;
+import com.dat3m.dartagnan.witness.svcomp.SvcompWitnessExtractor;
+import com.dat3m.dartagnan.witness.svcomp.SvcompWitnessYamlWriter;
 import com.dat3m.dartagnan.wmm.Wmm;
 import com.dat3m.dartagnan.wmm.axiom.Axiom;
 import com.google.common.base.Charsets;
@@ -65,16 +67,16 @@ public class OutputGenerator {
 
     @Option(
             name = WITNESS,
-            description = "Type of the violation graph to generate in the output directory.")
+            description = "Type of violation witness to generate in the output directory.")
     private WitnessType witnessType = WitnessType.getDefault();
 
     @Option(name=WITNESS_FILENAME,
-            description="Name for the witness graph file.",
+            description="Name for the witness file.",
             secure=true)
     private String witnessFilename = "";
 
     @Option(name=WITNESS_UNKNOWN,
-            description="Generate witness graph even if result is UNKNOWN.",
+            description="Generate a witness even if result is UNKNOWN.",
             secure=true)
     private boolean generateWitnessForUnknown = false;
 
@@ -245,7 +247,7 @@ private Path generateWitnessIfAble(VerificationResult result, String filename) t
             return null;
         }
 
-        final Task task = result.getTask();
+        final VerificationTask task = result.getTask();
         switch (witnessType) {
             case DOT, PNG -> {
                 final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
@@ -259,6 +261,18 @@ private Path generateWitnessIfAble(VerificationResult result, String filename) t
                         synContext, witnessType.convertToPng(), task.getConfig()
                 );
             }
+            case SV -> {
+                final ExecutionModelNext model = ExecutionModelManager.fromIREvaluator(result.getModel());
+                final var witness = SvcompWitnessExtractor.forViolation(model, task, result.getModel());
+                if (witness.isEmpty()) {
+                    logger.warn("SV-COMP violation witnesses are supported only for the following properties: {}.",
+                            String.join(", ", SvcompWitnessExtractor.supportedPropertyNames()));
+                    return null;
+                }
+                final Path witnessFile = getOrCreateOutputDirectory().resolve(filename + ".yml");
+                SvcompWitnessYamlWriter.write(witness.orElseThrow(), witnessFile);
+                return witnessFile;
+            }
         }
 
         return null;

dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessType.java

@@ -3,7 +3,7 @@
 import com.dat3m.dartagnan.configuration.OptionInterface;
 
 public enum WitnessType implements OptionInterface {
-    NONE, DOT, PNG;
+    NONE, DOT, PNG, SV;
 
     public static WitnessType getDefault() {
         return NONE;
@@ -13,4 +13,4 @@ public boolean convertToPng() {
         return this.equals(PNG);
     }
 
-}
+}

dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java

@@ -0,0 +1,44 @@
+package com.dat3m.dartagnan.witness.svcomp;
+
+import com.dat3m.dartagnan.verification.model.ExecutionModelNext;
+import com.dat3m.dartagnan.verification.model.RelationModel;
+import com.dat3m.dartagnan.verification.model.event.EventModel;
+import com.dat3m.dartagnan.utils.dependable.DependencyGraph;
+import com.google.common.base.Verify;
+
+import java.util.*;
+
+/**
+ * Chooses a sequentially-consistent interleaving for an execution produced with {@code svcomp.cat}.
+ */
+final class SvcompExecutionLinearizer {
+
+    private static final String HB = "hb-consistency";
+
+    private SvcompExecutionLinearizer() { }
+
+    static List<EventModel> linearize(ExecutionModelNext model) {
+        final RelationModel hb = Verify.verifyNotNull(model.getRelationModels().stream()
+                .filter(relation -> relation.getRelation().hasName(HB))
+                .findFirst()
+                .orElse(null), "Execution model does not contain relation '%s'", HB);
+        final Set<EventModel> events = new HashSet<>(model.getEventModels());
+        Verify.verify(hb.getEdgeModels().stream().allMatch(edge ->
+                        events.contains(edge.from()) && events.contains(edge.to())),
+                "Execution graph contains an edge with an unknown event");
+        Verify.verify(hb.getEdgeModels().stream().noneMatch(edge -> edge.from() == edge.to()),
+                "svcomp.cat produced a non-SC execution");
+
+        final Map<EventModel, Set<EventModel>> predecessors = new HashMap<>();
+        events.forEach(event -> predecessors.put(event, new HashSet<>()));
+
+        for (RelationModel.EdgeModel edge : hb.getEdgeModels()) {
+            predecessors.get(edge.to()).add(edge.from());
+        }
+
+        final DependencyGraph<EventModel> dependencyGraph = DependencyGraph.from(events, predecessors);
+        Verify.verify(dependencyGraph.getSCCs().size() == events.size(),
+                "svcomp.cat produced a non-SC execution");
+        return dependencyGraph.getNodeContents();
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompProperty.java

@@ -0,0 +1,35 @@
+package com.dat3m.dartagnan.witness.svcomp;
+
+/** Properties for which version 2.2 of the SV witness format defines a violation sequence. */
+enum SvcompProperty {
+    UNREACH_CALL("unreach-call", "CHECK( init(main()), LTL(G ! call(reach_error())) )"),
+    NO_OVERFLOW("no-overflow", "CHECK( init(main()), LTL(G ! overflow) )"),
+    VALID_DEREF("valid-deref", "CHECK( init(main()), LTL(G valid-deref) )"),
+    VALID_FREE("valid-free", "CHECK( init(main()), LTL(G valid-free) )"),
+    DATA_RACE("no-data-race", "CHECK( init(main()), LTL(G ! data-race) )");
+
+    private final String propertyName;
+    private final String specification;
+
+    SvcompProperty(String propertyName, String specification) {
+        this.propertyName = propertyName;
+        this.specification = specification;
+    }
+
+    String propertyName() {
+        return propertyName;
+    }
+
+    String specification() {
+        return specification;
+    }
+
+    static SvcompProperty fromAssertionError(String errorMessage) {
+        return switch (errorMessage) {
+            case "integer overflow" -> NO_OVERFLOW;
+            case "invalid dereference" -> VALID_DEREF;
+            case "invalid free" -> VALID_FREE;
+            default -> UNREACH_CALL;
+        };
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitness.java

@@ -0,0 +1,86 @@
+package com.dat3m.dartagnan.witness.svcomp;
+
+import java.nio.file.Path;
+import java.time.Instant;
+import java.util.List;
+import java.util.Objects;
+
+import static com.google.common.base.Preconditions.checkArgument;
+
+/** Data model for an SV-COMP 2.2 violation witness, independent of its YAML serialization. */
+public record SvcompWitness(Metadata metadata, List<Segment> segments) {
+
+    public SvcompWitness {
+        metadata = Objects.requireNonNull(metadata);
+        segments = List.copyOf(segments);
+    }
+
+    public record Metadata(String formatVersion, String uuid, Instant creationTime, Producer producer, Task task) {
+        public Metadata {
+            formatVersion = Objects.requireNonNull(formatVersion);
+            uuid = Objects.requireNonNull(uuid);
+            creationTime = Objects.requireNonNull(creationTime);
+            producer = Objects.requireNonNull(producer);
+            task = Objects.requireNonNull(task);
+        }
+    }
+
+    public record Producer(String name, String version) {
+        public Producer {
+            name = Objects.requireNonNull(name);
+            version = Objects.requireNonNull(version);
+        }
+    }
+
+    public record Task(Path inputFile, String inputFileHash, String specification, String dataModel, String language) {
+        public Task {
+            inputFile = Objects.requireNonNull(inputFile);
+            inputFileHash = Objects.requireNonNull(inputFileHash);
+            specification = Objects.requireNonNull(specification);
+            dataModel = Objects.requireNonNull(dataModel);
+            language = Objects.requireNonNull(language);
+        }
+    }
+
+    public record Segment(List<Waypoint> waypoints) {
+        public Segment {
+            waypoints = List.copyOf(waypoints);
+        }
+    }
+
+    public sealed interface Waypoint permits FunctionEnter, Assumption, Target {
+        int threadId();
+
+        Location location();
+    }
+
+    public record FunctionEnter(int threadId, Location location) implements Waypoint {
+        public FunctionEnter {
+            checkArgument(threadId >= 0, "Witness thread identifier must be non-negative");
+            location = Objects.requireNonNull(location);
+        }
+    }
+
+    public record Assumption(int threadId, String value, String format, Location location) implements Waypoint {
+        public Assumption {
+            checkArgument(threadId >= 0, "Witness thread identifier must be non-negative");
+            value = Objects.requireNonNull(value);
+            format = Objects.requireNonNull(format);
+            location = Objects.requireNonNull(location);
+        }
+    }
+
+    public record Target(int threadId, Location location) implements Waypoint {
+        public Target {
+            checkArgument(threadId >= 0, "Witness thread identifier must be non-negative");
+            location = Objects.requireNonNull(location);
+        }
+    }
+
+    public record Location(Path fileName, int line) {
+        public Location {
+            fileName = Objects.requireNonNull(fileName);
+            checkArgument(line > 0, "Source location line must be positive");
+        }
+    }
+}