diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java b/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java index 72f869b3c3..36f294b633 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java @@ -18,7 +18,6 @@ import com.dat3m.dartagnan.utils.ExitCode; import com.dat3m.dartagnan.verification.*; import com.dat3m.dartagnan.utils.Utils; -import com.dat3m.dartagnan.verification.model.ExecutionModelManager; import com.dat3m.dartagnan.verification.model.ExecutionModelNext; import com.dat3m.dartagnan.witness.WitnessType; import com.dat3m.dartagnan.wmm.Wmm; @@ -48,7 +47,11 @@ import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*; import static com.dat3m.dartagnan.utils.ExitCode.*; import static com.dat3m.dartagnan.verification.ResultStatus.*; +import static com.dat3m.dartagnan.verification.model.ExecutionModelManager.fromIREvaluator; import static com.dat3m.dartagnan.witness.graphviz.ExecutionGraphVisualizer.generateGraphvizFile; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.supportedPropertyNames; +import static com.dat3m.dartagnan.witness.svcomp.SvcompWitnessExtractor.forViolation; +import static com.dat3m.dartagnan.witness.svcomp.SvcompWitnessYamlWriter.write; @Options public class OutputGenerator { @@ -65,16 +68,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,11 +248,11 @@ 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()); - final ExecutionModelNext model = ExecutionModelManager.fromIREvaluator(result.getModel()); + final ExecutionModelNext model = fromIREvaluator(result.getModel()); // RF edges give both ordering and data flow information, thus even when the pair is in PO // we get some data flow information by observing the edge // CO edges only give ordering information which is known if the pair is also in PO @@ -259,6 +262,18 @@ private Path generateWitnessIfAble(VerificationResult result, String filename) t synContext, witnessType.convertToPng(), task.getConfig() ); } + case SV -> { + final ExecutionModelNext model = fromIREvaluator(result.getModel()); + final var witness = forViolation(model, task, result.getModel()); + if (witness.isEmpty()) { + logger.warn("SV-COMP violation witnesses are supported only for the following properties: {}.", + String.join(", ", supportedPropertyNames())); + return null; + } + final Path witnessFile = getOrCreateOutputDirectory().resolve(filename + ".yml"); + write(witness.get(), 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/SvcompProperty.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompProperty.java new file mode 100644 index 0000000000..64b8b9d82f --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompProperty.java @@ -0,0 +1,43 @@ +package com.dat3m.dartagnan.witness.svcomp; + +import java.util.List; + +import static java.util.Arrays.stream; + +/** Properties for which version 2.2 of the SV witness format defines a violation sequence. */ +public 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; + } + + public static List supportedPropertyNames() { + return stream(values()).map(SvcompProperty::propertyName).toList(); + } + + 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..d6d1519dc2 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessExtractor.java @@ -0,0 +1,360 @@ +package com.dat3m.dartagnan.witness.svcomp; + +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.metadata.SourceLocation.SourcePath; +import com.dat3m.dartagnan.program.Program; +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.utils.dependable.DependencyGraph; +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.RelationModel.EdgeModel; +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 com.google.common.base.Verify; +import com.google.common.base.VerifyException; + +import java.io.IOException; +import java.math.BigInteger; +import java.nio.file.Path; +import java.security.MessageDigest; +import java.security.NoSuchAlgorithmException; +import java.time.Instant; +import java.util.*; +import java.util.regex.Pattern; +import java.util.stream.Collectors; + +import static com.dat3m.dartagnan.configuration.Property.CAT_SPEC; +import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.DATA_RACE; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.UNREACH_CALL; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.fromAssertionError; +import static com.dat3m.dartagnan.witness.svcomp.SvcompWitness.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; +import static java.nio.file.Files.readAllBytes; + +/** Projects an {@link ExecutionModelNext} into an SV-COMP witness. */ +public final class SvcompWitnessExtractor { + + private static final String DATA_RACE_AXIOM = "data-race"; + private static final String HB = "hb-consistency"; + private static final Pattern C_IDENTIFIER = Pattern.compile("[A-Za-z_][A-Za-z0-9_]*"); + + private SvcompWitnessExtractor() { } + + public static Optional forViolation( + ExecutionModelNext model, VerificationTask task, IREvaluator evaluator) + throws IOException { + final Optional assertionViolation = findAssertionViolation(model, task, evaluator); + return assertionViolation.isPresent() + ? assertionViolation + : findDataRaceViolation(model, task, evaluator); + } + + private static Optional findAssertionViolation( + ExecutionModelNext model, VerificationTask task, IREvaluator evaluator) throws IOException { + if (!task.getProperties().contains(PROGRAM_SPEC) || !evaluator.propertyViolated(PROGRAM_SPEC)) { + return Optional.empty(); + } + 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( + fromAssertionError(assertion.getErrorMessage()), List.of(assertionViolation)); + return Optional.of(extract(model, task.getProgram(), violation)); + } + + private static Optional findDataRaceViolation( + ExecutionModelNext model, VerificationTask task, IREvaluator evaluator) throws IOException { + if (!task.getProperties().contains(CAT_SPEC)) { + return Optional.empty(); + } + final Optional dataRace = task.getMemoryModel().getAxioms().stream() + .filter(Axiom::isFlagged) + .filter(axiom -> DATA_RACE_AXIOM.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(); + if (dataRace.isEmpty()) { + return Optional.empty(); + } + final EdgeModel edge = dataRace.get(); + final EventModel first = edge.from(); + final EventModel second = edge.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(DATA_RACE, List.of(first, second)); + return Optional.of(extract(model, task.getProgram(), violation)); + } + + private static SvcompWitness extract(ExecutionModelNext model, Program program, SvcompViolation violation) + throws IOException { + if (!program.hasMetadata(SourcePath.class)) { + throw new IOException("Cannot generate an SV-COMP witness without program source metadata"); + } + final Path programFile = program.getMetadata(SourcePath.class).sourcePath(); + final SyntacticContextAnalysis context = SyntacticContextAnalysis.newInstance(program); + + final Map threadIds = new HashMap<>(); + final List segments = new ArrayList<>(); + final List linearized = linearize(model); + final Map assumptions = assumptionWaypoints(linearized, model, programFile); + final Set prefix = eventsBefore(violation.targets()); + for (EventModel event : linearized) { + if (!prefix.contains(event)) { + continue; + } + final ThreadModel thread = event.getThreadModel(); + registerThread(segments, thread, threadIds, model, programFile); + final String assumption = assumptions.get(event); + if (assumption != null) { + final Location location = inputLocation(event, programFile); + segments.add(new Segment(List.of(new Assumption( + threadIds.get(thread), 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(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 List linearize(ExecutionModelNext model) { + final RelationModel hb = model.getRelationModels().stream() + .filter(relation -> relation.getRelation().hasName(HB)) + .findFirst() + .orElseThrow(() -> new VerifyException( + "Execution model does not contain relation '%s'".formatted(HB))); + + final List events = model.getEventModels(); + final Map> predecessors = new HashMap<>(); + for (EdgeModel edge : hb.getEdgeModels()) { + Verify.verify(edge.from() != edge.to(), "svcomp.cat produced a non-SC execution"); + predecessors.computeIfAbsent(edge.to(), ignored -> new HashSet<>()).add(edge.from()); + } + + final DependencyGraph dependencyGraph = DependencyGraph.from(events, predecessors); + Verify.verify(dependencyGraph.getSCCs().size() == events.size(), + "svcomp.cat produced a non-SC execution"); + return dependencyGraph.getNodeContents(); + } + + private static Location targetLocation(EventModel target, SvcompProperty property, Path programFile, + SyntacticContextAnalysis context) { + if (property == 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 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(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..468a394ba7 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriter.java @@ -0,0 +1,105 @@ +package com.dat3m.dartagnan.witness.svcomp; + +import java.io.IOException; +import java.nio.file.Path; +import java.util.stream.Collectors; + +import static com.dat3m.dartagnan.witness.svcomp.SvcompWitness.*; +import static java.nio.charset.StandardCharsets.UTF_8; +import static java.nio.file.Files.createDirectories; +import static java.nio.file.Files.writeString; + +/** 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) { + createDirectories(parent); + } + writeString(file, render(witness), 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..c17fca0345 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompPropertyTest.java @@ -0,0 +1,47 @@ +package com.dat3m.dartagnan.witness.svcomp; + +import org.junit.Test; + +import java.util.List; + +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.DATA_RACE; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.NO_OVERFLOW; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.UNREACH_CALL; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.VALID_DEREF; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.VALID_FREE; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.fromAssertionError; +import static com.dat3m.dartagnan.witness.svcomp.SvcompProperty.supportedPropertyNames; +import static org.junit.Assert.assertEquals; + +public class SvcompPropertyTest { + + @Test + public void classifiesSupportedAssertionViolations() { + assertEquals(UNREACH_CALL, + fromAssertionError("user assertion")); + assertEquals(NO_OVERFLOW, + fromAssertionError("integer overflow")); + assertEquals(VALID_DEREF, + fromAssertionError("invalid dereference")); + assertEquals(VALID_FREE, + fromAssertionError("invalid free")); + } + + @Test + public void usesTheMatchingSvcompSpecification() { + assertEquals("CHECK( init(main()), LTL(G ! overflow) )", + NO_OVERFLOW.specification()); + assertEquals("CHECK( init(main()), LTL(G valid-deref) )", + VALID_DEREF.specification()); + assertEquals("CHECK( init(main()), LTL(G valid-free) )", + VALID_FREE.specification()); + assertEquals("CHECK( init(main()), LTL(G ! data-race) )", + DATA_RACE.specification()); + } + + @Test + public void listsSupportedPropertyNames() { + assertEquals(List.of("unreach-call", "no-overflow", "valid-deref", "valid-free", "no-data-race"), + 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..9bf75805a4 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/svcomp/SvcompWitnessYamlWriterTest.java @@ -0,0 +1,42 @@ +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 com.dat3m.dartagnan.witness.svcomp.SvcompWitnessYamlWriter.render; +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 = 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\"")); + assertTrue(yaml.contains(""" + - segment: + - waypoint: + type: function_enter + """)); + } +} 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