From 05526a42e5e856f60a783591a29a1254bd0edc18 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 8 Sep 2026 11:32:25 +0200 Subject: [PATCH 1/2] Add support for sv-witness generation in 2.2. format --- .../com/dat3m/dartagnan/OutputGenerator.java | 22 +- .../dat3m/dartagnan/witness/WitnessType.java | 4 +- .../svcomp/SvcompExecutionLinearizer.java | 100 +++++ .../witness/svcomp/SvcompProperty.java | 35 ++ .../witness/svcomp/SvcompWitness.java | 86 +++++ .../svcomp/SvcompWitnessExtractor.java | 346 ++++++++++++++++++ .../svcomp/SvcompWitnessYamlWriter.java | 104 ++++++ .../witness/svcomp/SvcompPropertyTest.java | 40 ++ .../svcomp/SvcompWitnessYamlWriterTest.java | 36 ++ svcomp/svcomp.properties | 2 + 10 files changed, 769 insertions(+), 6 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompProperty.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitness.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriter.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompPropertyTest.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriterTest.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java b/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java index 72f869b3c3..131cac60a2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java +++ b/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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessType.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessType.java index 4253ab4a13..0b1517f758 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessType.java +++ b/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); } -} \ No newline at end of file +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java new file mode 100644 index 0000000000..1e5ee42597 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java @@ -0,0 +1,100 @@ +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.google.common.base.Verify; + +import java.util.*; + +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; + +/** + * Chooses a deterministic sequentially-consistent interleaving for an execution produced with {@code svcomp.cat}. + */ +final class SvcompExecutionLinearizer { + + private SvcompExecutionLinearizer() { } + + static List linearize(ExecutionModelNext model) { + final Set events = new HashSet<>(model.getEventModels()); + final Map> successors = new HashMap<>(); + events.forEach(event -> successors.put(event, new HashSet<>())); + + // Add program-order (po) edges between consecutive events of each thread. + for (var thread : model.getThreadModels()) { + final List threadEvents = thread.getEventModels(); + for (int i = 1; i < threadEvents.size(); i++) { + addEdge(successors, threadEvents.get(i - 1), threadEvents.get(i)); + } + } + + final Set 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()); + } + } + } + + // 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. + final Map inDegree = new HashMap<>(); + events.forEach(event -> inDegree.put(event, 0)); + for (Set targets : successors.values()) { + targets.forEach(target -> adjustInDegree(inDegree, target, 1)); + } + + // Events without remaining predecessors are ready. Ordering them by ID makes the result deterministic. + final Queue ready = new PriorityQueue<>(Comparator.comparingInt(EventModel::getId)); + inDegree.forEach((event, degree) -> { + if (degree == 0) { + ready.add(event); + } + }); + + final List result = new ArrayList<>(events.size()); + while (!ready.isEmpty()) { + final EventModel event = ready.remove(); + result.add(event); + // Conceptually remove the selected event's outgoing edges and enqueue newly ready successors. + for (EventModel successor : successors.get(event)) { + if (adjustInDegree(inDegree, successor, -1) == 0) { + ready.add(successor); + } + } + } + Verify.verify(result.size() == events.size(), "svcomp.cat produced a non-SC execution"); + return result; + } + + private static Set relationEdges(ExecutionModelNext model, String name) { + return model.getRelationModels().stream() + .filter(relation -> relation.getRelation().hasName(name)) + .findFirst() + .map(RelationModel::getEdgeModels) + .orElse(Set.of()); + } + + private static void addEdge(Map> successors, EventModel from, EventModel to) { + if (from != to) { + successors.get(from).add(to); + } + } + + private static int adjustInDegree(Map inDegree, EventModel event, int adjustment) { + final int degree = Verify.verifyNotNull( + inDegree.get(event), "Execution graph contains an edge to an unknown event: %s", event); + final int adjustedDegree = degree + adjustment; + inDegree.put(event, adjustedDegree); + return adjustedDegree; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompProperty.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompProperty.java new file mode 100644 index 0000000000..792c6157b4 --- /dev/null +++ b/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; + }; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitness.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitness.java new file mode 100644 index 0000000000..9e250e4f3b --- /dev/null +++ b/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 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 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"); + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java new file mode 100644 index 0000000000..1721b46a99 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java @@ -0,0 +1,346 @@ +package com.dat3m.dartagnan.witness.svcomp; + +import com.dat3m.dartagnan.configuration.Property; +import com.dat3m.dartagnan.encoding.IREvaluator; +import com.dat3m.dartagnan.expression.type.BooleanType; +import com.dat3m.dartagnan.expression.type.IntegerType; +import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.metadata.SourceLocation; +import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.Assert; +import com.dat3m.dartagnan.program.event.core.Init; +import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; +import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; +import com.dat3m.dartagnan.utils.EnvironmentInfo; +import com.dat3m.dartagnan.verification.VerificationTask; +import com.dat3m.dartagnan.verification.model.ExecutionModelNext; +import com.dat3m.dartagnan.verification.model.MemoryObjectModel; +import com.dat3m.dartagnan.verification.model.RelationModel; +import com.dat3m.dartagnan.verification.model.ThreadModel; +import com.dat3m.dartagnan.verification.model.event.AssertModel; +import com.dat3m.dartagnan.verification.model.event.EventModel; +import com.dat3m.dartagnan.verification.model.event.LoadModel; +import com.dat3m.dartagnan.verification.model.event.MemoryEventModel; +import com.dat3m.dartagnan.wmm.axiom.Axiom; + +import java.io.IOException; +import java.math.BigInteger; +import java.nio.file.Files; +import java.nio.file.Path; +import java.security.MessageDigest; +import java.security.NoSuchAlgorithmException; +import java.time.Instant; +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; +import java.util.regex.Pattern; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import static com.dat3m.dartagnan.witness.svcomp.SvcompWitness.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; + +/** Projects an {@link ExecutionModelNext} into an SV-COMP witness. */ +public final class SvcompWitnessExtractor { + + private static final Pattern C_IDENTIFIER = Pattern.compile("[A-Za-z_][A-Za-z0-9_]*"); + + private SvcompWitnessExtractor() { } + + public static List supportedPropertyNames() { + return Stream.of(SvcompProperty.values()).map(SvcompProperty::propertyName).toList(); + } + + public static Optional forViolation( + ExecutionModelNext model, VerificationTask task, IREvaluator evaluator) + throws IOException { + if (isProgramSpecViolation(task, evaluator)) { + return Optional.of(forAssertionViolation(model, task)); + } + if (task.getProperties().contains(Property.CAT_SPEC)) { + final Optional dataRace = findDataRace(model, task, evaluator); + if (dataRace.isPresent()) { + return Optional.of(forDataRaceViolation(model, task, dataRace.orElseThrow())); + } + } + return Optional.empty(); + } + + private static boolean isProgramSpecViolation(VerificationTask task, IREvaluator evaluator) { + return task.getProperties().contains(Property.PROGRAM_SPEC) + && evaluator.propertyViolated(Property.PROGRAM_SPEC); + } + + private static SvcompWitness forAssertionViolation(ExecutionModelNext model, VerificationTask task) + throws IOException { + final AssertModel assertionViolation = model.getEventModels().stream() + .filter(AssertModel.class::isInstance).map(AssertModel.class::cast) + .filter(assertion -> !assertion.getResult()).findFirst() + .orElseThrow(() -> new IllegalArgumentException("Execution model contains no violated assertion")); + final Assert assertion = (Assert) assertionViolation.getEvent(); + final SvcompViolation violation = new SvcompViolation( + SvcompProperty.fromAssertionError(assertion.getErrorMessage()), List.of(assertionViolation)); + return extract(model, task, violation); + } + + private static SvcompWitness forDataRaceViolation(ExecutionModelNext model, VerificationTask task, + RelationModel.EdgeModel dataRace) throws IOException { + final EventModel first = dataRace.from(); + final EventModel second = dataRace.to(); + if (!(first instanceof MemoryEventModel) || !(second instanceof MemoryEventModel)) { + throw new IllegalArgumentException("Data-race targets are not memory accesses"); + } + if (first.getThreadModel().equals(second.getThreadModel())) { + throw new IllegalArgumentException("Data-race targets belong to the same thread"); + } + final SvcompViolation violation = new SvcompViolation(SvcompProperty.DATA_RACE, List.of(first, second)); + return extract(model, task, violation); + } + + private static SvcompWitness extract(ExecutionModelNext model, VerificationTask task, SvcompViolation violation) + throws IOException { + if (!task.getProgram().hasMetadata(SourceLocation.SourcePath.class)) { + throw new IOException("Cannot generate an SV-COMP witness without program source metadata"); + } + final Path programFile = task.getProgram().getMetadata(SourceLocation.SourcePath.class).sourcePath(); + final SyntacticContextAnalysis context = SyntacticContextAnalysis.newInstance(task.getProgram()); + + final Map threadIds = new HashMap<>(); + final List segments = new ArrayList<>(); + final List linearized = SvcompExecutionLinearizer.linearize(model); + final Map assumptions = assumptionWaypoints(linearized, model, programFile); + final Set prefix = eventsBefore(violation.targets()); + for (EventModel event : linearized) { + if (!prefix.contains(event)) { + continue; + } + registerThread(segments, event.getThreadModel(), threadIds, model, programFile); + final Location location = inputLocation(event, programFile); + final String assumption = assumptions.get(event); + if (location != null && assumption != null) { + segments.add(new Segment(List.of(new Assumption( + threadIds.get(event.getThreadModel()), assumption, "c_expression", location)))); + } + } + for (EventModel target : violation.targets()) { + registerThread(segments, target.getThreadModel(), threadIds, model, programFile); + } + final List targetWaypoints = violation.targets().stream() + .map(target -> new Target(threadIds.get(target.getThreadModel()), + targetLocation(target, violation.property(), programFile, context))) + .toList(); + segments.add(new Segment(targetWaypoints)); + + return new SvcompWitness(new Metadata("2.2", UUID.randomUUID().toString(), Instant.now(), + new Producer("Dartagnan", EnvironmentInfo.getVersion()), + new Task(programFile, sha256(programFile), violation.property().specification(), "ILP32", "C")), segments); + } + + /* + * Version 2.2 has no direct representation of rf or co. Instead, a concurrent execution is described by an + * ordered sequence of thread-tagged waypoints. We only constrain reads that actually read from another thread. + * This keeps the witness coarse while recording the observable part of rf/co. + */ + private static Map assumptionWaypoints(List linearized, ExecutionModelNext model, + Path programFile) { + final Map sourcePoints = sourcePoints(model, programFile); + final Set crossThreadReads = relationEdges(model, RF).stream() + .filter(edge -> edge.to() instanceof LoadModel) + .filter(edge -> !(edge.from().getEvent() instanceof Init)) + .filter(edge -> !edge.from().getThreadModel().equals(edge.to().getThreadModel())) + .map(RelationModel.EdgeModel::to) + .collect(Collectors.toSet()); + + final Map representatives = new HashMap<>(); + final Map> constraints = new HashMap<>(); + for (EventModel event : linearized) { + final SourcePoint point = sourcePoints.get(event); + if (!(event instanceof LoadModel load) || !crossThreadReads.contains(event) + || point == null) { + continue; + } + final Optional constraint = readValueAssumption(load, model); + if (constraint.isPresent()) { + representatives.putIfAbsent(point, event); + constraints.computeIfAbsent(point, ignored -> new LinkedHashSet<>()).add(constraint.get()); + } + } + + final Map result = new HashMap<>(); + constraints.forEach((point, values) -> + result.put(representatives.get(point), String.join(" && ", values))); + return result; + } + + private static Map sourcePoints(ExecutionModelNext model, Path programFile) { + final Map result = new HashMap<>(); + for (ThreadModel thread : model.getThreadModels()) { + Location previous = null; + int occurrence = 0; + for (EventModel event : thread.getEventModels()) { + final Location location = inputLocation(event, programFile); + if (location == null) { + continue; + } + if (!location.equals(previous)) { + occurrence++; + previous = location; + } + result.put(event, new SourcePoint(thread, occurrence, location)); + } + } + return result; + } + + private static Optional readValueAssumption(LoadModel load, ExecutionModelNext model) { + final MemoryCoreEvent event = (MemoryCoreEvent) load.getEvent(); + if (!(event.getAccessType() instanceof IntegerType) && !(event.getAccessType() instanceof BooleanType)) { + return Optional.empty(); + } + final int accessSize = TypeFactory.getInstance().getMemorySizeInBytes(event.getAccessType()); + final Optional object = model.getMemoryLayoutMap().values().stream() + .filter(memory -> memory.object().isStaticallyAllocated() && memory.object().hasName()) + .filter(memory -> C_IDENTIFIER.matcher(memory.object().getName()).matches()) + .filter(memory -> memory.address().equals(load.getAccessedAddress())) + .filter(memory -> memory.size().equals(BigInteger.valueOf(accessSize))) + .findFirst(); + if (object.isEmpty()) { + return Optional.empty(); + } + final Object value = load.getValue().value(); + final String literal; + if (value instanceof Boolean booleanValue) { + literal = booleanValue ? "1" : "0"; + } else if (value instanceof Number) { + literal = value.toString(); + } else { + return Optional.empty(); + } + return Optional.of(String.format("(%s == %s)", object.get().object().getName(), literal)); + } + + private static Set relationEdges(ExecutionModelNext model, String name) { + return model.getRelationModels().stream() + .filter(relation -> relation.getRelation().hasName(name)) + .findFirst() + .map(RelationModel::getEdgeModels) + .orElse(Set.of()); + } + + private static Location targetLocation(EventModel target, SvcompProperty property, Path programFile, + SyntacticContextAnalysis context) { + if (property == SvcompProperty.UNREACH_CALL) { + final List calls = context.getContextInfo(target.getEvent()) + .getContextOfType(SyntacticContextAnalysis.CallContext.class); + for (int i = calls.size() - 1; i >= 0; i--) { + final SyntacticContextAnalysis.CallContext call = calls.get(i); + if ("reach_error".equals(call.funCallMarker().getFunctionName())) { + final Location location = inputLocation(call.funCallMarker(), programFile); + if (location != null) { + return location; + } + } + } + } + return requireInputLocation(target, programFile); + } + + private record SourcePoint(ThreadModel thread, int occurrence, Location location) { } + + private static void registerThread(List segments, ThreadModel thread, + Map threadIds, ExecutionModelNext model, Path programFile) { + if (threadIds.containsKey(thread)) { + return; + } + final ThreadStart start = thread.getThread().getEntry(); + if (!start.isSpawned()) { + threadIds.put(thread, 0); + return; + } + final Location location = inputLocation(start.getCreator(), programFile); + if (location == null) { + throw new IllegalArgumentException("Thread creation has no source location in the input program"); + } + final ThreadModel creator = threadOf(start.getCreator(), model); + registerThread(segments, creator, threadIds, model, programFile); + final int id = threadIds.size(); + segments.add(new Segment(List.of(new FunctionEnter(threadIds.get(creator), location)))); + threadIds.put(thread, id); + } + + private static ThreadModel threadOf(Event event, ExecutionModelNext model) { + return model.getThreadModels().stream().filter(thread -> thread.getThread().equals(event.getThread())) + .findFirst().orElseThrow(() -> new IllegalArgumentException("Thread creator is not part of the execution model")); + } + + private static Set eventsBefore(List targets) { + final Set result = new HashSet<>(); + for (EventModel target : targets) { + final List events = target.getThreadModel().getEventModels(); + final int index = events.indexOf(target); + if (index < 0) { + throw new IllegalArgumentException("Violation target is not part of the execution model"); + } + result.addAll(events.subList(0, index)); + } + return result; + } + + private static Optional findDataRace(ExecutionModelNext model, VerificationTask task, + IREvaluator evaluator) { + return task.getMemoryModel().getAxioms().stream() + .filter(Axiom::isFlagged) + .filter(axiom -> "data-race".equals(axiom.getName())) + .filter(evaluator::isFlaggedAxiomViolated) + .map(Axiom::getRelation) + .flatMap(relation -> model.getRelationModels().stream() + .filter(relationModel -> relationModel.getRelation().equals(relation)) + .flatMap(relationModel -> relationModel.getEdgeModels().stream())) + .findFirst(); + } + + private static Location requireInputLocation(EventModel event, Path programFile) { + final Location location = inputLocation(event, programFile); + if (location == null) { + throw new IllegalArgumentException("Violation target has no source location in the input program"); + } + return location; + } + + private static Location inputLocation(EventModel event, Path programFile) { + return inputLocation(event.getEvent(), programFile); + } + + private static Location inputLocation(Event event, Path programFile) { + final SourceLocation location = event.getMetadata(SourceLocation.class); + if (!(location instanceof SourceLocation.Generic generic) || generic.lineNumber() < 1 + || !generic.sourcePath().getFileName().equals(programFile.getFileName())) { + return null; + } + return new Location(programFile, generic.lineNumber()); + } + + // The targets identify the event(s) constituting the violation and become the final target waypoints. + private record SvcompViolation(SvcompProperty property, List targets) { + + private SvcompViolation { + targets = List.copyOf(targets); + } + } + + private static String sha256(Path file) throws IOException { + try { + return HexFormat.of().formatHex(MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(file))); + } catch (NoSuchAlgorithmException exception) { + throw new AssertionError("SHA-256 is unavailable", exception); + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriter.java new file mode 100644 index 0000000000..b6eae15f9c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriter.java @@ -0,0 +1,104 @@ +package com.dat3m.dartagnan.witness.svcomp; + +import java.io.IOException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.stream.Collectors; + +import static com.dat3m.dartagnan.witness.svcomp.SvcompWitness.*; + +/** Serializes {@link SvcompWitness} instances to SV-COMP's YAML representation. */ +public final class SvcompWitnessYamlWriter { + + private SvcompWitnessYamlWriter() { } + + public static void write(SvcompWitness witness, Path file) throws IOException { + final Path parent = file.getParent(); + if (parent != null) { + Files.createDirectories(parent); + } + Files.writeString(file, render(witness), StandardCharsets.UTF_8); + } + + static String render(SvcompWitness witness) { + final Metadata metadata = witness.metadata(); + final Producer producer = metadata.producer(); + final Task task = metadata.task(); + final String header = """ + - entry_type: violation_sequence + metadata: + format_version: \"%s\" + uuid: \"%s\" + creation_time: \"%s\" + producer: + name: %s + version: %s + task: + input_files: + - %s + input_file_hashes: + %s: \"%s\" + specification: %s + data_model: %s + language: %s + content: + """.formatted(metadata.formatVersion(), metadata.uuid(), metadata.creationTime(), yaml(producer.name()), + yaml(producer.version()), yaml(task.inputFile()), yaml(task.inputFile()), task.inputFileHash(), + yaml(task.specification()), task.dataModel(), task.language()); + return header + witness.segments().stream() + .map(SvcompWitnessYamlWriter::formatSegment) + .collect(Collectors.joining()); + } + + private static String formatSegment(Segment segment) { + return " - segment:\n" + segment.waypoints().stream() + .map(SvcompWitnessYamlWriter::formatWaypoint) + .collect(Collectors.joining()); + } + + private static String formatWaypoint(Waypoint waypoint) { + if (waypoint instanceof Assumption assumption) { + return """ + - waypoint: + type: assumption + action: follow + thread_id: %d + constraint: + value: %s + format: %s + location: + file_name: %s + line: %d + """.formatted(assumption.threadId(), yaml(assumption.value()), assumption.format(), + yaml(assumption.location().fileName()), assumption.location().line()); + } + + final String type; + if (waypoint instanceof FunctionEnter) { + type = "function_enter"; + } else if (waypoint instanceof Target) { + type = "target"; + } else { + throw new AssertionError("Unsupported waypoint: " + waypoint); + } + return """ + - waypoint: + type: %s + action: follow + thread_id: %d + location: + file_name: %s + line: %d + """.formatted(type, waypoint.threadId(), yaml(waypoint.location().fileName()), + waypoint.location().line()); + } + + private static String yaml(Path value) { + return yaml(value.toString()); + } + + private static String yaml(String value) { + return "\"" + value.replace("\\", "\\\\").replace("\"", "\\\"") + "\""; + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompPropertyTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompPropertyTest.java new file mode 100644 index 0000000000..99fcb7b3c5 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompPropertyTest.java @@ -0,0 +1,40 @@ +package com.dat3m.dartagnan.witness.svcomp; + +import org.junit.Test; + +import java.util.List; + +import static org.junit.Assert.assertEquals; + +public class SvcompPropertyTest { + + @Test + public void classifiesSupportedAssertionViolations() { + assertEquals(SvcompProperty.UNREACH_CALL, + SvcompProperty.fromAssertionError("user assertion")); + assertEquals(SvcompProperty.NO_OVERFLOW, + SvcompProperty.fromAssertionError("integer overflow")); + assertEquals(SvcompProperty.VALID_DEREF, + SvcompProperty.fromAssertionError("invalid dereference")); + assertEquals(SvcompProperty.VALID_FREE, + SvcompProperty.fromAssertionError("invalid free")); + } + + @Test + public void usesTheMatchingSvcompSpecification() { + assertEquals("CHECK( init(main()), LTL(G ! overflow) )", + SvcompProperty.NO_OVERFLOW.specification()); + assertEquals("CHECK( init(main()), LTL(G valid-deref) )", + SvcompProperty.VALID_DEREF.specification()); + assertEquals("CHECK( init(main()), LTL(G valid-free) )", + SvcompProperty.VALID_FREE.specification()); + assertEquals("CHECK( init(main()), LTL(G ! data-race) )", + SvcompProperty.DATA_RACE.specification()); + } + + @Test + public void listsSupportedPropertyNames() { + assertEquals(List.of("unreach-call", "no-overflow", "valid-deref", "valid-free", "no-data-race"), + SvcompWitnessExtractor.supportedPropertyNames()); + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriterTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriterTest.java new file mode 100644 index 0000000000..389a771847 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriterTest.java @@ -0,0 +1,36 @@ +package com.dat3m.dartagnan.witness.svcomp; + +import org.junit.Test; + +import java.nio.file.Path; +import java.time.Instant; +import java.util.List; + +import static com.dat3m.dartagnan.witness.svcomp.SvcompWitness.*; +import static org.junit.Assert.assertTrue; + +public class SvcompWitnessYamlWriterTest { + + @Test + public void serializesSemanticWitness() { + final Path inputFile = Path.of("example.c"); + final Location location = new Location(inputFile, 7); + final SvcompWitness witness = new SvcompWitness( + new Metadata("2.2", "test-uuid", Instant.parse("2026-01-01T00:00:00Z"), + new Producer("Dartagnan", "test-version"), + new Task(inputFile, "deadbeef", "CHECK( init(main()), LTL(G ! data-race) )", + "LP64", "C")), + List.of(new Segment(List.of(new FunctionEnter(0, location))), + new Segment(List.of(new Assumption(1, "1", "c_expression", location))), + new Segment(List.of(new Target(1, location))))); + + final String yaml = SvcompWitnessYamlWriter.render(witness); + + assertTrue(yaml.contains("entry_type: violation_sequence")); + assertTrue(yaml.contains("version: \"test-version\"")); + assertTrue(yaml.contains("type: function_enter")); + assertTrue(yaml.contains("type: assumption")); + assertTrue(yaml.contains("type: target")); + assertTrue(yaml.contains("file_name: \"example.c\"")); + } +} diff --git a/svcomp/svcomp.properties b/svcomp/svcomp.properties index 9c5df48b23..17e068169a 100644 --- a/svcomp/svcomp.properties +++ b/svcomp/svcomp.properties @@ -1,3 +1,5 @@ method=eager solver=yices2 encoding.wmm.idl2sat=true +witness=sv +witness.filename=witness From 99c4326c1b887ae5c688cec2996f9a461fd9fa96 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 19 Sep 2026 23:07:10 +0200 Subject: [PATCH 2/2] Feedback implemented --- .../svcomp/SvcompExecutionLinearizer.java | 98 ++++--------------- .../svcomp/SvcompWitnessExtractor.java | 11 +-- 2 files changed, 22 insertions(+), 87 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java index 1e5ee42597..3690960650 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompExecutionLinearizer.java @@ -3,98 +3,42 @@ 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.*; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; - /** - * Chooses a deterministic sequentially-consistent interleaving for an execution produced with {@code svcomp.cat}. + * 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 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 events = new HashSet<>(model.getEventModels()); - final Map> successors = new HashMap<>(); - events.forEach(event -> successors.put(event, new HashSet<>())); + 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"); - // Add program-order (po) edges between consecutive events of each thread. - for (var thread : model.getThreadModels()) { - final List threadEvents = thread.getEventModels(); - for (int i = 1; i < threadEvents.size(); i++) { - addEdge(successors, threadEvents.get(i - 1), threadEvents.get(i)); - } - } + final Map> predecessors = new HashMap<>(); + events.forEach(event -> predecessors.put(event, new HashSet<>())); - final Set 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()); - } - } + for (RelationModel.EdgeModel edge : hb.getEdgeModels()) { + predecessors.get(edge.to()).add(edge.from()); } - // 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. - final Map inDegree = new HashMap<>(); - events.forEach(event -> inDegree.put(event, 0)); - for (Set targets : successors.values()) { - targets.forEach(target -> adjustInDegree(inDegree, target, 1)); - } - - // Events without remaining predecessors are ready. Ordering them by ID makes the result deterministic. - final Queue ready = new PriorityQueue<>(Comparator.comparingInt(EventModel::getId)); - inDegree.forEach((event, degree) -> { - if (degree == 0) { - ready.add(event); - } - }); - - final List result = new ArrayList<>(events.size()); - while (!ready.isEmpty()) { - final EventModel event = ready.remove(); - result.add(event); - // Conceptually remove the selected event's outgoing edges and enqueue newly ready successors. - for (EventModel successor : successors.get(event)) { - if (adjustInDegree(inDegree, successor, -1) == 0) { - ready.add(successor); - } - } - } - Verify.verify(result.size() == events.size(), "svcomp.cat produced a non-SC execution"); - return result; - } - - private static Set relationEdges(ExecutionModelNext model, String name) { - return model.getRelationModels().stream() - .filter(relation -> relation.getRelation().hasName(name)) - .findFirst() - .map(RelationModel::getEdgeModels) - .orElse(Set.of()); - } - - private static void addEdge(Map> successors, EventModel from, EventModel to) { - if (from != to) { - successors.get(from).add(to); - } - } - - private static int adjustInDegree(Map inDegree, EventModel event, int adjustment) { - final int degree = Verify.verifyNotNull( - inDegree.get(event), "Execution graph contains an edge to an unknown event: %s", event); - final int adjustedDegree = degree + adjustment; - inDegree.put(event, adjustedDegree); - return adjustedDegree; + final DependencyGraph dependencyGraph = DependencyGraph.from(events, predecessors); + Verify.verify(dependencyGraph.getSCCs().size() == events.size(), + "svcomp.cat produced a non-SC execution"); + return dependencyGraph.getNodeContents(); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java index 1721b46a99..4e7a6542b2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java @@ -31,16 +31,7 @@ import java.security.MessageDigest; import java.security.NoSuchAlgorithmException; import java.time.Instant; -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; +import java.util.*; import java.util.regex.Pattern; import java.util.stream.Collectors; import java.util.stream.Stream;