[RFC] Program extensions

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,

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;

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() {

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<Property> 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<BooleanFormula> 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<BooleanFormula> 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() {

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<String, MemoryObject> 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);
     }
 
     // ----------------------------------------------------------------------------------------------------------------

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<Expression> {

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<Expression> {
 
     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;
         }

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,13 +41,17 @@ public class ProgramBuilder {
     protected String entryPointId;
     protected Arch arch;
     protected Expression filterSpec;
+    protected Expression spec;
+    protected ProgramExtension.Litmus extension = ProgramExtension.Litmus.trivial();
     protected Set<String> nextOps;
 
     public ProgramBuilder(ThreadGrid grid) {
         this.grid = 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,19 +113,21 @@ 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) {
         if (this.filterSpec != null) {
             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) {

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);
     }