diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java b/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java index e5b5097171..f518842c84 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/OutputGenerator.java @@ -12,6 +12,7 @@ import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Assert; import com.dat3m.dartagnan.program.event.core.CondJump; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.processing.LoopUnrolling; import com.dat3m.dartagnan.utils.ExitCode; @@ -355,12 +356,13 @@ private static String getSpecificationString(Program program) { return ""; } - final StringBuilder sb = new StringBuilder(); - sb.append(program.getSpecificationType().toString().toLowerCase()).append(" "); - // TODO: Can the spec really be null here? - if (program.getSpecification() != null) { - sb.append(new ExpressionPrinter(true).visit(program.getSpecification())); + if (!(program.getExtension() instanceof ProgramExtension.Litmus litmusExtension)) { + return ""; } + + final StringBuilder sb = new StringBuilder(); + sb.append(litmusExtension.specType().toString().toLowerCase()).append(" "); + sb.append(new ExpressionPrinter(true).visit(litmusExtension.spec())); sb.append("\n"); return sb.toString(); } @@ -369,9 +371,13 @@ private static String getFilterString(Task task) { if ("true".equals(task.getConfig().getProperty(IGNORE_FILTER_SPECIFICATION))) return ""; - final Expression filter = task.getProgram().getFilterSpecification(); - final boolean isTrivialFilter = filter instanceof BoolLiteral bLit && bLit.getValue(); - return isTrivialFilter ? "" : filter.toString(); + if (task.getProgram().getExtension() instanceof ProgramExtension.Litmus litmusExtension) { + final Expression filter = litmusExtension.filter(); + final boolean isTrivialFilter = filter instanceof BoolLiteral bLit && bLit.getValue(); + return isTrivialFilter ? "" : filter.toString(); + } + + return ""; } private static String toSummary(String test, String filter, ResultStatus status, String condition, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Property.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Property.java index bfc62481d2..adfc062258 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Property.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Property.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.configuration; import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.verification.Task; import com.dat3m.dartagnan.wmm.axiom.Axiom; import com.google.common.base.Preconditions; @@ -40,7 +41,9 @@ public String asStringOption() { } public Type getType(Task context) { - if (this == PROGRAM_SPEC && context.getProgram().hasReachabilitySpecification()) { + if (this == PROGRAM_SPEC + && context.getProgram().getExtension() instanceof ProgramExtension.Litmus litmusExtension + && ProgramExtension.Litmus.SpecificationType.EXISTS == litmusExtension.specType()) { return Type.REACHABILITY; } else { return Type.SAFETY; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index 610bba4c67..8f1b8cf329 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -16,6 +16,7 @@ import com.dat3m.dartagnan.program.event.*; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.core.threading.*; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.verification.Context; @@ -494,8 +495,11 @@ public BooleanFormula encodeDependencies() { } public BooleanFormula encodeFilter() { - final Expression filterSpec = context.getTask().getProgram().getFilterSpecification(); - return ignoreFilterSpec ? bmgr.makeTrue() : exprEnc.encodeBooleanFinal(filterSpec).formula(); + final Program program = context.getTask().getProgram(); + if (!ignoreFilterSpec && program.getExtension() instanceof ProgramExtension.Litmus litmusExtension) { + return exprEnc.encodeBooleanFinal(litmusExtension.filter()).formula(); + } + return bmgr.makeTrue(); } public BooleanFormula encodeFinalRegisterValues() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index b9eaa7891f..951811de6b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -12,6 +12,7 @@ import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; @@ -31,7 +32,6 @@ import static com.dat3m.dartagnan.configuration.Property.*; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM; -import static com.dat3m.dartagnan.program.Program.SpecificationType.ASSERT; import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder { @@ -156,7 +156,7 @@ private BooleanFormula encodePropertyWitnesses(EnumSet properties) { // Litmus (program spec). We cannot check this together with safety specs, so we make sure // that we do not mix them up. Preconditions.checkArgument(properties.contains(PROGRAM_SPEC)); - Preconditions.checkArgument(program.hasReachabilitySpecification()); + //Preconditions.checkArgument(program.hasReachabilitySpecification()); final TrackableFormula progSpec = encodeProgramSpecification(); // NOTE: We have a single property to check, so the tracking becomes trivial. @@ -174,28 +174,28 @@ private TrackableFormula encodeProgramSpecification() { final ExpressionEncoder exprEnc = context.getExpressionEncoder(); // We can only perform existential queries to the SMT-engine, so for // safety specs we need to query for a violation (= negation of the spec) - BooleanFormula encoding = switch (program.getSpecificationType()) { - case EXISTS, NOT_EXISTS -> exprEnc.encodeBooleanFinal(program.getSpecification()).formula(); - case FORALL -> bmgr.not(exprEnc.encodeBooleanFinal(program.getSpecification()).formula()); - case ASSERT -> { - // User-placed assertions inside C code. - List assertionsHold = new ArrayList<>(); - for (Assert assertion : program.getThreadEvents(Assert.class)) { - assertionsHold.add(bmgr.implication(context.execution(assertion), - exprEnc.encodeBooleanAt(assertion.getExpression(), assertion).formula() - )); - } - yield bmgr.not(bmgr.and(assertionsHold)); - } - }; - BooleanFormula trackingLiteral = switch (program.getSpecificationType()) { - case FORALL, NOT_EXISTS, ASSERT -> bmgr.not(PROGRAM_SPEC.getSMTVariable(context)); - case EXISTS -> PROGRAM_SPEC.getSMTVariable(context); - }; - if (!ASSERT.equals(program.getSpecificationType())) { + if (program.getExtension() instanceof ProgramExtension.Litmus litmusExtension) { + BooleanFormula encoding = switch (litmusExtension.specType()) { + case EXISTS, NOT_EXISTS -> exprEnc.encodeBooleanFinal(litmusExtension.spec()).formula(); + case FORALL -> bmgr.not(exprEnc.encodeBooleanFinal(litmusExtension.spec()).formula()); + }; + BooleanFormula trackingLiteral = switch (litmusExtension.specType()) { + case FORALL, NOT_EXISTS -> bmgr.not(PROGRAM_SPEC.getSMTVariable(context)); + case EXISTS -> PROGRAM_SPEC.getSMTVariable(context); + }; encoding = bmgr.and(encoding, encodeProgramTermination()); + return new TrackableFormula(trackingLiteral, encoding); + } else { + List assertionsHold = new ArrayList<>(); + for (Assert assertion : program.getThreadEvents(Assert.class)) { + assertionsHold.add(bmgr.implication(context.execution(assertion), + exprEnc.encodeBooleanAt(assertion.getExpression(), assertion).formula() + )); + } + BooleanFormula encoding = bmgr.not(bmgr.and(assertionsHold)); + BooleanFormula trackingLiteral = bmgr.not(PROGRAM_SPEC.getSMTVariable(context)); + return new TrackableFormula(trackingLiteral, encoding); } - return new TrackableFormula(trackingLiteral, encoding); } private BooleanFormula encodeProgramTermination() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java index 388877b0c8..9191fe0748 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java @@ -18,6 +18,7 @@ import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; import com.dat3m.dartagnan.program.event.metadata.OriginalId; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.memory.VirtualMemoryObject; @@ -49,12 +50,15 @@ public class ProgramBuilder { private final Map locations = new HashMap<>(); private final Program program; + private final ProgramExtension.Litmus litmusExtension; // ---------------------------------------------------------------------------------------------------------------- // Construction private ProgramBuilder(SourceLanguage format) { Preconditions.checkArgument(format == SourceLanguage.LITMUS); this.program = new Program(new Memory(), format); + this.litmusExtension = ProgramExtension.Litmus.trivial(); + this.program.setExtension(litmusExtension); } public static ProgramBuilder forArch(SourceLanguage format, Arch arch) { @@ -128,12 +132,12 @@ public ExpressionFactory getExpressionFactory() { return expressions; } - public void setAssert(Program.SpecificationType type, Expression ass) { - program.setSpecification(type, ass); + public void setAssert(ProgramExtension.Litmus.SpecificationType type, Expression ass) { + litmusExtension.setSpec(type, ass); } public void setAssertFilter(Expression ass) { - program.setFilterSpecification(ass); + litmusExtension.setFilter(ass); } // ---------------------------------------------------------------------------------------------------------------- diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java index 6edb76b566..a318fec076 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAssertions.java @@ -20,7 +20,7 @@ import java.math.BigInteger; -import static com.dat3m.dartagnan.program.Program.SpecificationType.*; +import static com.dat3m.dartagnan.program.extensions.ProgramExtension.Litmus.SpecificationType.*; import static com.google.common.base.Preconditions.checkState; class VisitorLitmusAssertions extends LitmusAssertionsBaseVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java index 5bb7a79130..e047432b91 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorSpirvOutput.java @@ -12,22 +12,22 @@ import com.dat3m.dartagnan.parsers.program.visitors.spirv.builders.ProgramBuilder; import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperInputs; import com.dat3m.dartagnan.parsers.program.visitors.spirv.helpers.HelperTypes; -import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.ScopedPointerVariable; import java.util.List; import static com.dat3m.dartagnan.expression.integers.IntCmpOp.*; -import static com.dat3m.dartagnan.program.Program.SpecificationType.*; +import static com.dat3m.dartagnan.program.extensions.ProgramExtension.Litmus.SpecificationType.*; public class VisitorSpirvOutput extends SpirvBaseVisitor { private static final TypeFactory types = TypeFactory.getInstance(); private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); private final ProgramBuilder builder; - private Program.SpecificationType type; + private ProgramExtension.Litmus.SpecificationType type; private Expression condition; private Expression filter; @@ -66,7 +66,7 @@ public Expression visitFilterHeader(SpirvParser.FilterHeaderContext ctx) { @Override public Expression visitAssertionList(SpirvParser.AssertionListContext ctx) { - Program.SpecificationType parsedType = parseType(ctx); + ProgramExtension.Litmus.SpecificationType parsedType = parseType(ctx); Expression parsedAssertion = ctx.assertion().accept(this); if (condition == null) { type = parsedType; @@ -155,7 +155,7 @@ private Expression normalize(Expression target, Expression other) { target.getClass().getSimpleName(), other.getClass().getSimpleName()); } - private Program.SpecificationType parseType(SpirvParser.AssertionListContext ctx) { + private ProgramExtension.Litmus.SpecificationType parseType(SpirvParser.AssertionListContext ctx) { if (ctx.ModeHeader_AssertionNot() != null) { return NOT_EXISTS; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java index 10f4db6083..851a6e7902 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/builders/ProgramBuilder.java @@ -14,6 +14,7 @@ import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.functions.FunctionCall; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.memory.ScopedPointerVariable; @@ -40,6 +41,8 @@ public class ProgramBuilder { protected String entryPointId; protected Arch arch; protected Expression filterSpec; + protected Expression spec; + protected ProgramExtension.Litmus extension = ProgramExtension.Litmus.trivial(); protected Set nextOps; public ProgramBuilder(ThreadGrid grid) { @@ -47,6 +50,8 @@ public ProgramBuilder(ThreadGrid grid) { this.program = new Program(new Memory(), Program.SourceLanguage.SPV); this.controlFlowBuilder = new ControlFlowBuilder(expressions); this.decorationsBuilder = new DecorationsBuilder(grid); + + program.setExtension(extension); } public Program build() { @@ -108,11 +113,13 @@ public void setArch(Arch arch) { this.arch = arch; } - public void setSpecification(Program.SpecificationType type, Expression condition) { - if (program.getSpecification() != null) { + public void setSpecification(ProgramExtension.Litmus.SpecificationType type, Expression condition) { + if (this.spec != null) { throw new ParsingException("Attempt to override program specification"); } - program.setSpecification(type, condition); + + this.spec = condition; + this.extension.setSpec(type, condition); } public void setFilterSpecification(Expression condition) { @@ -120,7 +127,7 @@ public void setFilterSpecification(Expression condition) { throw new ParsingException("Attempt to override program filter specification"); } this.filterSpec = condition; - program.setFilterSpecification(this.filterSpec); + this.extension.setFilter(condition); } public boolean hasInput(String id) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java index e38597d690..232c59d276 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java @@ -8,6 +8,7 @@ import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; @@ -32,8 +33,6 @@ public class Program { public enum SourceLanguage { LITMUS, LLVM, SPV } - public enum SpecificationType { EXISTS, FORALL, NOT_EXISTS, ASSERT } - @Options public static class SemanticConfig { @Option(name = ROUNDING_MODE_FLOATS, @@ -54,10 +53,8 @@ public static class SemanticConfig { private final Memory memory; private Entrypoint entrypoint = new Entrypoint.None(); - // Spec - private SpecificationType specificationType = SpecificationType.ASSERT; - private Expression spec; - private Expression filterSpec; // Acts like "assume" statements, filtering out executions + // Extension + private ProgramExtension extension = new ProgramExtension.None(); // Semantic options private final SemanticConfig semanticConfig = new SemanticConfig(); @@ -82,8 +79,6 @@ public Program(String name, Memory memory, SourceLanguage format) { this.name = name; this.memory = memory; this.format = format; - - this.filterSpec = ExpressionFactory.getInstance().makeTrue(); } public SourceLanguage getFormat() { @@ -130,32 +125,6 @@ public Entrypoint getEntrypoint() { return entrypoint; } - public SpecificationType getSpecificationType() { - return specificationType; - } - - public boolean hasReachabilitySpecification() { - return SpecificationType.EXISTS.equals(specificationType); - } - - public Expression getSpecification() { - return spec; - } - - public void setSpecification(SpecificationType type, Expression spec) { - this.specificationType = type; - this.spec = spec; - } - - public Expression getFilterSpecification() { - return filterSpec; - } - - public void setFilterSpecification(Expression spec) { - Preconditions.checkArgument(spec.getType() instanceof BooleanType); - this.filterSpec = spec; - } - public FloatingPointRoundingMode getFloatRoundingMode() { return semanticConfig.floatRoundingMode; } @@ -168,6 +137,10 @@ public void setFloatRoundingMode(FloatingPointRoundingMode roundingMode) { this.semanticConfig.floatRoundingMode = roundingMode; } + public void setExtension(ProgramExtension extension) { this.extension = extension; } + + public ProgramExtension getExtension() { return extension; } + public void injectConfig(Configuration configuration) throws InvalidConfigurationException { configuration.inject(semanticConfig); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java index 5587cfef95..02b1eee5c8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -8,6 +8,7 @@ import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.core.Label; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.verification.Context; import com.google.common.base.Preconditions; import com.google.common.base.Verify; @@ -111,13 +112,13 @@ public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, C } private static Set finalRegisters(Program program) { - final Set finalRegisters = new LinkedHashSet<>(); - if (program.getSpecification() != null) { - finalRegisters.addAll(program.getSpecification().getRegs()); - } - if (program.getFilterSpecification() != null) { - finalRegisters.addAll(program.getFilterSpecification().getRegs()); + if (!(program.getExtension() instanceof ProgramExtension.Litmus litmusExtension)) { + return ImmutableSet.of(); } + + final Set finalRegisters = new LinkedHashSet<>(); + finalRegisters.addAll(litmusExtension.spec().getRegs()); + finalRegisters.addAll(litmusExtension.filter().getRegs()); return finalRegisters; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/extensions/ProgramExtension.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/extensions/ProgramExtension.java new file mode 100644 index 0000000000..d20e044dc4 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/extensions/ProgramExtension.java @@ -0,0 +1,82 @@ +package com.dat3m.dartagnan.program.extensions; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionFactory; +import com.dat3m.dartagnan.expression.ExpressionPrinter; +import com.dat3m.dartagnan.expression.booleans.BoolLiteral; + +import java.util.Objects; + +public sealed interface ProgramExtension { + + record None() implements ProgramExtension { } + + final class Litmus implements ProgramExtension { + public enum SpecificationType { EXISTS, FORALL, NOT_EXISTS } + + private SpecificationType specType; + private Expression spec; + private Expression filter; + // private final List locations; // TODO + + public Litmus(SpecificationType specType, Expression spec, Expression filter) { + this.specType = specType; + this.spec = spec; + this.filter = filter; + } + + public static Litmus trivial() { + final ExpressionFactory exprs = ExpressionFactory.getInstance(); + return new Litmus(SpecificationType.FORALL, exprs.makeTrue(), exprs.makeTrue()); + } + + public void setSpec(SpecificationType specType, Expression spec) { + this.specType = specType; + this.spec = spec; + } + + public void setFilter(Expression filter) { + this.filter = filter; + } + + public SpecificationType specType() { + return specType; + } + + public Expression spec() { + return spec; + } + + public Expression filter() { + return filter; + } + + + @Override + public boolean equals(Object obj) { + if (obj == this) return true; + if (obj == null || obj.getClass() != this.getClass()) return false; + var that = (Litmus) obj; + return Objects.equals(this.specType, that.specType) && + Objects.equals(this.spec, that.spec) && + Objects.equals(this.filter, that.filter); + } + + @Override + public int hashCode() { + return Objects.hash(specType, spec, filter); + } + + @Override + public String toString() { + final ExpressionPrinter printer = new ExpressionPrinter(true); + final StringBuilder sb = new StringBuilder(); + if (!(filter instanceof BoolLiteral lit && lit.getValue())) { + sb.append("filter ").append(filter.accept(printer)).append("\n"); + } + sb.append(specType.toString().toLowerCase()).append(" ").append(spec.accept(printer)); + + return sb.toString(); + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java index e1d50e9589..6d21d57883 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java @@ -8,6 +8,7 @@ import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.Alloc; import com.dat3m.dartagnan.program.event.core.Local; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.google.common.collect.Lists; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -40,12 +41,10 @@ public void run(Function function) { private void eliminateDeadAssignments(Function function) { final Program program = function.getProgram(); Set usedRegs = new HashSet<>(); - if(program.getSpecification() != null) { - usedRegs.addAll(program.getSpecification().getRegs()); - // for litmus tests - if (program.getFilterSpecification() != null) { - usedRegs.addAll(program.getFilterSpecification().getRegs()); - } + + if (program.getExtension() instanceof ProgramExtension.Litmus litmusExtension) { + usedRegs.addAll(litmusExtension.spec().getRegs()); + usedRegs.addAll(litmusExtension.filter().getRegs()); } // Compute events to be removed (removal is delayed) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java index 0aeea91d3d..4bb114f267 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java @@ -4,6 +4,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; @@ -33,8 +34,8 @@ public void run(Program program) { .forEach(f -> collector.memoryObjects.addAll(o.getInitialValue(f).getMemoryObjects()))); // Assertions - if (program.getSpecification() != null) { - collector.memoryObjects.addAll(program.getSpecification().getMemoryObjects()); + if (program.getExtension() instanceof ProgramExtension.Litmus litmusExtension) { + collector.memoryObjects.addAll(litmusExtension.spec().getMemoryObjects()); } // Remove unused objects diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java index f842b69605..e61a4445a1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Tearing.java @@ -23,6 +23,7 @@ import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.FinalMemoryValue; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.verification.Context; @@ -165,17 +166,16 @@ private int tearInits(Program program, AliasAnalysis alias, boolean bigEndian) { private void tearExpressions(Program program) { //TODO currently, FinalMemoryValue only occurs in the program's final state expressions. - final Expression specification = program.getSpecification(); - final Expression filter = program.getFilterSpecification(); final var substitution = new FinalValueTearSubstitution(); for (Init init : program.getThreadEvents(Init.class)) { substitution.typesByObject.computeIfAbsent(init.getBase(), k -> new HashMap<>()) .put(init.getOffset(), init.getAccessType()); } - final Expression updatedSpecification = specification == null ? null : specification.accept(substitution); - final Expression updatedFilter = filter.accept(substitution); - program.setSpecification(program.getSpecificationType(), updatedSpecification); - program.setFilterSpecification(updatedFilter); + + if (program.getExtension() instanceof ProgramExtension.Litmus litmusExtension) { + litmusExtension.setSpec(litmusExtension.specType(), litmusExtension.spec().accept(substitution)); + litmusExtension.setFilter(litmusExtension.filter().accept(substitution)); + } } private List createTransaction(Load load, List offsets) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java index d653108b46..457eed09e2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java @@ -2,12 +2,12 @@ import com.dat3m.dartagnan.configuration.OptionNames; import com.dat3m.dartagnan.expression.ExpressionPrinter; -import com.dat3m.dartagnan.expression.booleans.BoolLiteral; import com.dat3m.dartagnan.program.*; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; @@ -244,18 +244,14 @@ private boolean showEvent(Event event) { // Specification private static void appendSpecification(Program program, StringBuilder result) { - final ExpressionPrinter expressionPrinter = new ExpressionPrinter(true); - - if (program.getSpecification() != null) { + if (program.getExtension() instanceof ProgramExtension.Litmus litmusExtension) { + final ExpressionPrinter expressionPrinter = new ExpressionPrinter(true); result.append("\nSpecification:\n") - .append(program.getSpecificationType()).append(" ") - .append(program.getSpecification().accept(expressionPrinter)) + .append(litmusExtension.specType()).append(" ") + .append(litmusExtension.spec().accept(expressionPrinter)) .append("\n"); - } - - if (!(program.getFilterSpecification() instanceof BoolLiteral c && c.getValue())) { result.append("\nFilter specification:\n") - .append(program.getFilterSpecification().accept(expressionPrinter)); + .append(litmusExtension.filter().accept(expressionPrinter)); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/PrinterTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/PrinterTest.java index 2b05a469ed..a8cc860bd5 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/PrinterTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/others/miscellaneous/PrinterTest.java @@ -31,42 +31,36 @@ public void Printll() throws Exception { public void PrintX86() throws Exception { Program p = new ProgramParser().parse(getTestResourcePath("litmus/MP+mfence-rmw+rmw-mfence.litmus")); assertNotNull(Printer.newInstance().print(p)); - assertNotNull(p.getSpecification().toString()); } @Test() public void PrintPPC() throws Exception { Program p = new ProgramParser().parse(getTestResourcePath("litmus/MP+lwsync+data-wsi-rfi-ctrlisync.litmus")); assertNotNull(Printer.newInstance().print(p)); - assertNotNull(p.getSpecification().toString()); } @Test() public void PrintAARCH64() throws Exception { Program p = new ProgramParser().parse(getTestResourcePath("litmus/MP+popl+poap.litmus")); assertNotNull(Printer.newInstance().print(p)); - assertNotNull(p.getSpecification().toString()); } @Test() public void PrintLinux() throws Exception { Program p = new ProgramParser().parse(getTestResourcePath("litmus/C-rcu-link-after.litmus")); assertNotNull(Printer.newInstance().print(p)); - assertNotNull(p.getSpecification().toString()); } @Test() public void PrintLinux2() throws Exception { Program p = new ProgramParser().parse(getRootPath("litmus/LKMM/dart/C-atomic-fetch-simple-01.litmus")); assertNotNull(Printer.newInstance().print(p)); - assertNotNull(p.getSpecification().toString()); } @Test() public void PrintLinux3() throws Exception { Program p = new ProgramParser().parse(getRootPath("litmus/LKMM/manual/atomic/C-atomic-01.litmus")); assertNotNull(Printer.newInstance().print(p)); - assertNotNull(p.getSpecification().toString()); } @Test() diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/AssertTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/AssertTest.java index 53158761a9..a79a845492 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/AssertTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/AssertTest.java @@ -1,13 +1,14 @@ package com.dat3m.dartagnan.spirv.header; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; import java.util.Arrays; -import static com.dat3m.dartagnan.program.Program.SpecificationType.*; +import static com.dat3m.dartagnan.program.extensions.ProgramExtension.Litmus.SpecificationType.*; import static org.junit.Assert.assertEquals; @RunWith(Parameterized.class) @@ -15,9 +16,9 @@ public class AssertTest extends AbstractTest { private final String input; private final String expValue; - private final Program.SpecificationType expType; + private final ProgramExtension.Litmus.SpecificationType expType; - public AssertTest(String input, String expValue, Program.SpecificationType expType) { + public AssertTest(String input, String expValue, ProgramExtension.Litmus.SpecificationType expType) { this.input = input; this.expValue = expValue; this.expType = expType; @@ -96,7 +97,8 @@ public void testAssertions() { Program program = parse(input); // then - assertEquals(expValue, program.getSpecification().toString()); - assertEquals(expType, program.getSpecificationType()); + final ProgramExtension.Litmus litmusExtension = (ProgramExtension.Litmus) program.getExtension(); + assertEquals(expValue, litmusExtension.spec().toString()); + assertEquals(expType, litmusExtension.specType()); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/FilterTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/FilterTest.java index d485393a96..2285ae8cab 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/FilterTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/header/FilterTest.java @@ -1,6 +1,8 @@ package com.dat3m.dartagnan.spirv.header; + import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.extensions.ProgramExtension; import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; @@ -36,6 +38,6 @@ public void testAssertions() { Program program = parse(input); // then - assertEquals(expValue, program.getFilterSpecification().toString()); + assertEquals(expValue, ((ProgramExtension.Litmus)program.getExtension()).filter().toString()); } }