Assertion expressions

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

@@ -3,6 +3,7 @@
 import com.dat3m.dartagnan.configuration.OptionNames;
 import com.dat3m.dartagnan.configuration.Property;
 import com.dat3m.dartagnan.encoding.EncodingContext;
+import com.dat3m.dartagnan.expression.ExpressionPrinter;
 import com.dat3m.dartagnan.parsers.cat.ParserCat;
 import com.dat3m.dartagnan.parsers.program.ProgramParser;
 import com.dat3m.dartagnan.parsers.witness.ParserWitness;
@@ -335,7 +336,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
         } else {
             // Litmus-specific output format that matches with Herd7 (as good as it can)
             if (p.getFilterSpecification() != null) {
-                summary.append("Filter ").append(p.getFilterSpecification().toStringWithType()).append("\n");
+                summary.append("Filter ").append(p.getFilterSpecification()).append("\n");
             }
 
             // NOTE: We cannot produce an output that matches herd7 when checking for both program spec and cat properties.
@@ -349,12 +350,12 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
                 // We have a positive witness or no violations, then the program must be ok.
                 // NOTE: We also treat the UNKNOWN case as positive, assuming that
                 // looping litmus tests are unusual.
-                summary.append("Condition ").append(p.getSpecification().toStringWithType()).append("\n");
+                printSpecification(summary, p);
                 summary.append("Ok").append("\n");
             } else if (hasViolations) {
                 if (props.contains(PROGRAM_SPEC) && FALSE.equals(model.evaluate(PROGRAM_SPEC.getSMTVariable(encCtx)))) {
                     // Program spec violated
-                    summary.append("Condition ").append(p.getSpecification().toStringWithType()).append("\n");
+                    printSpecification(summary, p);
                     summary.append("No").append("\n");
                 } else {
                     final List<Axiom> violatedCATSpecs = task.getMemoryModel().getAxioms().stream()
@@ -376,7 +377,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
                     summary.append(result).append("\n");
                 } else if (task.getProperty().contains(PROGRAM_SPEC)) {
                     // ... which can be good or bad (no witness = bad, not violation = good)
-                    summary.append("Condition ").append(p.getSpecification().toStringWithType()).append("\n");
+                    printSpecification(summary, p);
                     summary.append(result == PASS ? "Ok" : "No").append("\n");
                 }
             }
@@ -397,4 +398,18 @@ private static void printWarningIfThreadStartFailed(Program p, EncodingContext e
             }
         }
     }
+
+    private static void printSpecification(StringBuilder sb, Program program) {
+        sb.append("Condition ").append(program.getSpecificationType().toString().toLowerCase()).append(" ");
+        boolean init = false;
+        if (program.getSpecification() != null) {
+            sb.append(new ExpressionPrinter(true).visit(program.getSpecification()));
+            init = true;
+        }
+        for (Assert assertion : program.getThreadEvents(Assert.class)) {
+            sb.append(init ? " && " : "").append(assertion.getExpression()).append("%").append(assertion.getGlobalId());
+            init = true;
+        }
+        sb.append("\n");
+    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Property.java

@@ -46,7 +46,7 @@ public String asStringOption() {
     }
 
     public Type getType(VerificationTask context) {
-        if (this == PROGRAM_SPEC && !context.getProgram().getSpecification().isSafetySpec()) {
+        if (this == PROGRAM_SPEC && context.getProgram().hasReachabilitySpecification()) {
             return Type.REACHABILITY;
         } else {
             return Type.SAFETY;

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java

@@ -128,6 +128,10 @@ public Formula encodeFinalExpression(Expression expression) {
         return new ExpressionEncoder(this, null).encode(expression);
     }
 
+    public BooleanFormula encodeFinalExpressionAsBoolean(Expression expression) {
+        return new ExpressionEncoder(this, null).encodeAsBoolean(expression);
+    }
+
     public BooleanFormula encodeExpressionAsBooleanAt(Expression expression, Event event) {
         return new ExpressionEncoder(this, event).encodeAsBoolean(expression);
     }

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java

@@ -248,7 +248,7 @@ public BooleanFormula encodeDependencies() {
 
     public BooleanFormula encodeFilter() {
         return context.getTask().getProgram().getFilterSpecification() != null ?
-                context.getTask().getProgram().getFilterSpecification().encode(context) :
+                context.encodeFinalExpressionAsBoolean(context.getTask().getProgram().getFilterSpecification()) :
                 context.getBooleanFormulaManager().makeTrue();
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java

@@ -12,7 +12,6 @@
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.metadata.MemoryOrder;
-import com.dat3m.dartagnan.program.specification.AbstractAssert;
 import com.dat3m.dartagnan.wmm.Relation;
 import com.dat3m.dartagnan.wmm.RelationNameRepository;
 import com.dat3m.dartagnan.wmm.Wmm;
@@ -154,7 +153,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.getSpecification().isSafetySpec());
+        Preconditions.checkArgument(program.hasReachabilitySpecification());
 
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         final TrackableFormula progSpec = encodeProgramSpecification();
@@ -250,28 +249,26 @@ private BooleanFormula lastCoVar(Event write) {
 
     private TrackableFormula encodeProgramSpecification() {
         logger.info("Encoding program specification");
-        final AbstractAssert spec = program.getSpecification();
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         // 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)
-        final BooleanFormula encoding;
-        final BooleanFormula trackingLiteral;
-        switch (spec.getType()) {
-            case AbstractAssert.ASSERT_TYPE_FORALL:
-                encoding = bmgr.not(spec.encode(context));
-                trackingLiteral = bmgr.not(PROGRAM_SPEC.getSMTVariable(context));
-                break;
-            case AbstractAssert.ASSERT_TYPE_NOT_EXISTS:
-                encoding = spec.encode(context);
-                trackingLiteral = bmgr.not(PROGRAM_SPEC.getSMTVariable(context));
-                break;
-            case AbstractAssert.ASSERT_TYPE_EXISTS:
-                encoding = spec.encode(context);
-                trackingLiteral = PROGRAM_SPEC.getSMTVariable(context);
-                break;
-            default:
-                throw new IllegalStateException("Unrecognized program specification: " + spec.toStringWithType());
-        }
+        BooleanFormula encoding = switch (program.getSpecificationType()) {
+            case EXISTS, NOT_EXISTS -> context.encodeFinalExpressionAsBoolean(program.getSpecification());
+            case FORALL -> bmgr.not(context.encodeFinalExpressionAsBoolean(program.getSpecification()));
+            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),
+                            context.encodeExpressionAsBooleanAt(assertion.getExpression(), assertion)));
+                }
+                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);
+        };
         return new TrackableFormula(trackingLiteral, encoding);
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionPrinter.java

@@ -0,0 +1,98 @@
+package com.dat3m.dartagnan.expression;
+
+import com.dat3m.dartagnan.expression.floats.FloatSizeCast;
+import com.dat3m.dartagnan.expression.floats.IntToFloatCast;
+import com.dat3m.dartagnan.expression.integers.FloatToIntCast;
+import com.dat3m.dartagnan.expression.integers.IntSizeCast;
+import com.dat3m.dartagnan.expression.misc.ConstructExpr;
+import com.dat3m.dartagnan.expression.misc.ExtractExpr;
+import com.dat3m.dartagnan.expression.misc.GEPExpr;
+import com.dat3m.dartagnan.expression.misc.ITEExpr;
+import com.dat3m.dartagnan.program.Register;
+
+import java.util.stream.Collectors;
+
+public final class ExpressionPrinter implements ExpressionVisitor<String> {
+
+    private final boolean qualified;
+
+    private ExpressionKind kind;
+
+    public ExpressionPrinter(boolean qualified) {
+        this.qualified = qualified;
+    }
+
+    public String visit(Expression expr) {
+        final ExpressionKind kind = this.kind;
+        this.kind = expr.getKind();
+        final String inner = expr.accept(this);
+        final boolean direct = kind == null || kind == this.kind || expr.getOperands().isEmpty();
+        final String result = direct ? inner : "(" + inner + ")";
+        this.kind = kind;
+        return result;
+    }
+
+    @Override
+    public String visitExpression(Expression expr) {
+        return expr.toString();
+    }
+
+    @Override
+    public String visitBinaryExpression(BinaryExpression expr) {
+        return visit(expr.getLeft()) + " " + expr.getKind() + " " + visit(expr.getRight());
+    }
+
+    @Override
+    public String visitUnaryExpression(UnaryExpression expr) {
+        return expr.getKind() + visit(expr.getOperand());
+    }
+
+    @Override
+    public String visitIntSizeCastExpression(IntSizeCast expr) {
+        final String opName = expr.isTruncation() ? "trunc" : (expr.preservesSign() ? "sext" : "zext");
+        return String.format("%s %s to %s", opName, visit(expr.getOperand()), expr.getTargetType());
+    }
+
+    @Override
+    public String visitFloatToIntCastExpression(FloatToIntCast expr) {
+        final String opName = expr.isSigned() ? "fptosi" : "fptoui";
+        return String.format("%s %s to %s", opName, expr.getOperand().toString(), expr.getTargetType());
+    }
+
+    @Override
+    public String visitFloatSizeCastExpression(FloatSizeCast expr) {
+        final String opName = expr.isTruncation() ? "trunc" : "ext";
+        return String.format("%s %s to %s", visit(expr.getOperand()), opName, expr.getTargetType());
+    }
+
+    @Override
+    public String visitIntToFloatCastExpression(IntToFloatCast expr) {
+        final String opName = expr.isSigned() ? "sitofp" : "uitofp";
+        return String.format("%s %s to %s", opName, visit(expr.getOperand()), expr.getTargetType());
+    }
+
+    @Override
+    public String visitExtractExpression(ExtractExpr extract) {
+        return visit(extract.getOperand()) + "[" + extract.getFieldIndex() + "]";
+    }
+
+    @Override
+    public String visitConstructExpression(ConstructExpr expr) {
+        return expr.getOperands().stream().map(this::visit).collect(Collectors.joining(", ", "{ ", " }"));
+    }
+
+    @Override
+    public String visitGEPExpression(GEPExpr expr) {
+        return expr.getOperands().stream().map(this::visit).collect(Collectors.joining(", ", "GEP(", ")"));
+    }
+
+    @Override
+    public String visitITEExpression(ITEExpr expr) {
+        return visit(expr.getCondition()) + " ? " + visit(expr.getTrueCase()) + " : " + visit(expr.getFalseCase());
+    }
+
+    @Override
+    public String visitRegister(Register reg) {
+        return qualified ? reg.getFunction().getId() + ":" + reg.getName() : reg.toString();
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/expression/base/BinaryExpressionBase.java

@@ -33,11 +33,6 @@ protected BinaryExpressionBase(TType type, TKind kind, Expression left, Expressi
     @Override
     public TKind getKind() { return kind; }
 
-    @Override
-    public String toString() {
-        return "(" + left + " " + kind + " " + right + ")";
-    }
-
     @Override
     public int hashCode() {
         return Objects.hash(type, kind, left, right);

dartagnan/src/main/java/com/dat3m/dartagnan/expression/base/CastExpressionBase.java

@@ -10,21 +10,18 @@
 import java.util.Objects;
 
 @NoInterface
-public abstract class CastExpressionBase<TTargetType extends Type, TSourceType extends Type> implements CastExpression {
+public abstract class CastExpressionBase<TTargetType extends Type, TSourceType extends Type> extends ExpressionBase<TTargetType>
+        implements CastExpression {
 
-    protected final TTargetType targetType;
     protected final Expression operand;
 
     protected CastExpressionBase(TTargetType targetType, Expression operand) {
-        this.targetType = targetType;
+        super(targetType);
         this.operand = operand;
     }
 
     @Override
-    public TTargetType getTargetType() { return targetType; }
-
-    @Override
-    public TTargetType getType() { return getTargetType(); }
+    public TTargetType getTargetType() { return getType(); }
 
     @Override @SuppressWarnings("unchecked")
     public TSourceType getSourceType() {
@@ -40,14 +37,9 @@ public TSourceType getSourceType() {
     @Override
     public ExpressionKind.Other getKind() { return ExpressionKind.Other.CAST; }
 
-    @Override
-    public String toString() {
-        return String.format("cast %s to %s", operand, targetType);
-    }
-
     @Override
     public int hashCode() {
-        return Objects.hash(targetType, operand);
+        return Objects.hash(type, operand);
     }
 
     @Override
@@ -59,7 +51,7 @@ public boolean equals(Object obj) {
         }
 
         final CastExpression expr = (CastExpression) obj;
-        return this.targetType.equals(expr.getTargetType())
+        return this.type.equals(expr.getTargetType())
                 && this.operand.equals(expr.getOperand());
     }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/expression/base/ExpressionBase.java

@@ -1,6 +1,7 @@
 package com.dat3m.dartagnan.expression.base;
 
 import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.ExpressionPrinter;
 import com.dat3m.dartagnan.expression.Type;
 import com.dat3m.dartagnan.program.event.common.NoInterface;
 
@@ -18,6 +19,11 @@ protected ExpressionBase(TType type) {
     @Override
     public TType getType() { return this.type; }
 
+    @Override
+    public String toString() {
+        return new ExpressionPrinter(false).visit(this);
+    }
+
     @Override
     public int hashCode() {
         return Objects.hash(type, getKind(), getOperands());

dartagnan/src/main/java/com/dat3m/dartagnan/expression/base/UnaryExpressionBase.java

@@ -30,11 +30,6 @@ protected UnaryExpressionBase(TType type, TKind kind, Expression operand) {
     @Override
     public TKind getKind() { return kind; }
 
-    @Override
-    public String toString() {
-        return "(" + kind + operand + ")";
-    }
-
     @Override
     public int hashCode() {
         return Objects.hash(type, kind, operand);

dartagnan/src/main/java/com/dat3m/dartagnan/expression/floats/FloatSizeCast.java

@@ -29,12 +29,6 @@ private static boolean isExtension(FloatType sourceType, FloatType targetType) {
         return sourceType.getBitWidth() < targetType.getBitWidth();
     }
 
-    @Override
-    public String toString() {
-        final String opName = isTruncation() ? "trunc" : "ext";
-        return String.format("%s %s to %s", operand, opName, targetType);
-    }
-
     @Override
     public <T> T accept(ExpressionVisitor<T> visitor) {
         return visitor.visitFloatSizeCastExpression(this);

dartagnan/src/main/java/com/dat3m/dartagnan/expression/floats/IntToFloatCast.java

@@ -19,12 +19,6 @@ public IntToFloatCast(FloatType targetType, Expression operand, boolean isSigned
 
     public boolean isSigned() { return isSigned; }
 
-    @Override
-    public String toString() {
-        final String opName = isSigned ? "sitofp" : "uitofp";
-        return String.format("%s %s to %s", opName, operand, targetType);
-    }
-
     @Override
     public <T> T accept(ExpressionVisitor<T> visitor) {
         return visitor.visitIntToFloatCastExpression(this);

dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/FloatToIntCast.java

@@ -19,12 +19,6 @@ public FloatToIntCast(IntegerType targetType, Expression operand, boolean isSign
 
     public boolean isSigned() { return isSigned; }
 
-    @Override
-    public String toString() {
-        final String opName = isSigned ? "fptosi" : "fptoui";
-        return String.format("%s %s to %s", opName, operand, targetType);
-    }
-
     @Override
     public <T> T accept(ExpressionVisitor<T> visitor) {
         return visitor.visitFloatToIntCastExpression(this);

dartagnan/src/main/java/com/dat3m/dartagnan/expression/integers/IntSizeCast.java

@@ -36,12 +36,6 @@ private static boolean isExtension(IntegerType sourceType, IntegerType targetTyp
         return sourceType.getBitWidth() < targetType.getBitWidth();
     }
 
-    @Override
-    public String toString() {
-        final String opName = isTruncation() ? "trunc" : (preserveSign ? "sext" : "zext");
-        return String.format("%s %s to %s", opName, operand, targetType);
-    }
-
     @Override
     public <T> T accept(ExpressionVisitor<T> visitor) {
         return visitor.visitIntSizeCastExpression(this);