Svcomp23 (#333)

* Added option to break symmetry on control-flow variables (by using special value "_cf")

* Added possibility to break symmetry on control flow by specifying "_cf" as breaking relation.

* Combined cf-based symmetry breaking with relation-based symmetry breaking by adding a dummy cf relation.

* Renamed symmetry breaking option + new description.
Minor refactoring.
Moved back the Configuration into the constructor of SymmetryEncoder to restore its functionality (since the constructor already relies on the config options)

* Small fixes for 2023 competition

* Set DAT3M_OUTPUT in svcomp script

* Working with CoVeriTeam

* MemEvent.canRace() should use mo.equals("") instead of mo == null

* Disable CP in svcomp script

* Update version to 3.1.1

* Throw exception if correctness witness is given

* Remove support for single threaded programs in svcomp script

Co-authored-by: Thomas Haas <[email protected]>

Dartagnan-SVCOMP.sh

@@ -1,6 +1,6 @@
 #!/bin/bash
 
-version=3.0.0
+version=3.1.1
 
 if [ $# -eq 0 ]; then
     echo "No input file supplied"
@@ -22,17 +22,11 @@ else
 
     cflags="-DSVCOMP -DCUSTOM_VERIFIER_ASSERT -fno-vectorize -fno-slp-vectorize"
     smackflags="-q -t --no-memory-splitting"
-
-    svcompflags="--method=assume"
-    if ! grep -q "pthread" $programpath; then
-        cflags+=" -O3"
-        smackflags+=" --integer-encoding bit-vector"
-        svcompflags+=" cat/sc.cat"
-    else
-        svcompflags+=" --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat"
-    fi
+    svcompflags="--method=assume --program.processing.constantPropagation=false --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat"
 
     export DAT3M_HOME=$(pwd)
+    export DAT3M_OUTPUT=$DAT3M_HOME/output
+    export PATH=$PATH:$DAT3M_HOME/smack/bin
     export CFLAGS=$cflags
     export SMACK_FLAGS=$smackflags
 

README.md

@@ -58,7 +58,7 @@ Usage
 Dartagnan comes with a user interface (not available from the docker container) where it is easy to import, export and modify both the program and the memory model and select the options for the verification engine (see below).
 You can start the user interface by running
 ```
-java -jar ui/target/ui-3.1.0.jar
+java -jar ui/target/ui-3.1.1.jar
 ```
 <p align="center"> 
 <img src="ui/src/main/resources/ui.jpg">
@@ -74,7 +74,7 @@ There are three possible results for the verification:
 You can also run Dartagnan from the console:
 
 ```
-java -jar dartagnan/target/dartagnan-3.1.0.jar <CAT file> [--target=<arch>] <program file> [options]
+java -jar dartagnan/target/dartagnan-3.1.1.jar <CAT file> [--target=<arch>] <program file> [options]
 ```
 For programs written in `.c` and `.bpl`, value `<arch>` specifies the programming language or architectures to which the program will be compiled. It must be one of the following: 
 - c11

dartagnan/pom.xml

@@ -6,7 +6,7 @@
   <parent>
     <groupId>com.dat3m</groupId>
     <artifactId>dat3m</artifactId>
-    <version>3.1.0</version>
+    <version>3.1.1</version>
   </parent>
 
   <groupId>com.dat3m.dartagnan</groupId>

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

@@ -23,7 +23,7 @@ public class OptionNames {
 	public static final String MERGE_CF_VARS = "encoding.mergeCFVars";
 	public static final String INITIALIZE_REGISTERS = "encoding.initializeRegisters";
 	public static final String PRECISION = "encoding.precision";
-	public static final String BREAK_SYMMETRY_ON_RELATION = "encoding.symmetry.breakOnRelation";
+	public static final String BREAK_SYMMETRY_ON = "encoding.symmetry.breakOn";
 	public static final String BREAK_SYMMETRY_BY_SYNC_DEGREE = "encoding.symmetry.orderBySyncDegree";
 	public static final String IDL_TO_SAT = "encoding.wmm.idl2sat";
 

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

@@ -1,6 +1,7 @@
 package com.dat3m.dartagnan.encoding;
 
 import com.dat3m.dartagnan.program.Thread;
+import com.dat3m.dartagnan.program.analysis.BranchEquivalence;
 import com.dat3m.dartagnan.program.analysis.ThreadSymmetry;
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.Event;
@@ -11,9 +12,11 @@
 import com.dat3m.dartagnan.wmm.axiom.Axiom;
 import com.dat3m.dartagnan.wmm.relation.Relation;
 import com.dat3m.dartagnan.wmm.utils.Tuple;
+import com.dat3m.dartagnan.wmm.utils.TupleSet;
 import com.google.common.base.Preconditions;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
+import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.common.configuration.Option;
 import org.sosy_lab.common.configuration.Options;
@@ -26,7 +29,7 @@
 import java.util.stream.Collectors;
 
 import static com.dat3m.dartagnan.configuration.OptionNames.BREAK_SYMMETRY_BY_SYNC_DEGREE;
-import static com.dat3m.dartagnan.configuration.OptionNames.BREAK_SYMMETRY_ON_RELATION;
+import static com.dat3m.dartagnan.configuration.OptionNames.BREAK_SYMMETRY_ON;
 
 @Options
 public class SymmetryEncoder implements Encoder {
@@ -38,102 +41,105 @@ public class SymmetryEncoder implements Encoder {
     private final ThreadSymmetry symm;
     private final Relation rel;
 
-    @Option(name = BREAK_SYMMETRY_ON_RELATION,
-            description = "The relation on which symmetry breaking should happen." +
-            "Empty, if symmetry shall not be encoded.",
+    @Option(name = BREAK_SYMMETRY_ON,
+            description = "The target to break symmetry on. Allowed options are:\n" +
+                    "- A relation name to break symmetry on.\n" +
+                    "- The special value \"_cf\" to break symmetry on the control flow.\n" +
+                    "- The empty string to disable symmetry breaking.",
             secure = true)
-    private String symmBreakRelName = "";
+    private String symmBreakTarget = "";
 
     @Option(name = BREAK_SYMMETRY_BY_SYNC_DEGREE,
-            description = "Orders the relation edges to break on based on their synchronization strength.",
+            description = "Orders the relation edges to break on based on their synchronization strength." +
+            "Only has impact if breaking symmetry on relations rather than control flow.",
             secure = true)
     private boolean breakBySyncDegree = true;
 
     // =====================================================================
 
-    private SymmetryEncoder(EncodingContext c, Wmm m, Context a) {
+    private SymmetryEncoder(EncodingContext c, Wmm m, Context a, Configuration config) throws InvalidConfigurationException {
         context = c;
         axioms = List.copyOf(m.getAxioms());
-        symm = c.getAnalysisContext().get(ThreadSymmetry.class);
+        symm = c.getAnalysisContext().requires(ThreadSymmetry.class);
         a.requires(RelationAnalysis.class);
-        if (symmBreakRelName.isEmpty()) {
+        config.inject(this);
+
+        if (symmBreakTarget.isEmpty()) {
             logger.info("Symmetry breaking disabled.");
             this.rel = null;
+        } else if (symmBreakTarget.equals("_cf")) {
+            logger.info("Breaking symmetry on control flow.");
+            a.requires(BranchEquivalence.class);
+            this.rel = new CfRelation();
+            this.breakBySyncDegree = false; // We cannot break by sync degree here
         } else {
-            this.rel = c.getTask().getMemoryModel().getRelation(symmBreakRelName);
+            this.rel = c.getTask().getMemoryModel().getRelation(symmBreakTarget);
             if (this.rel == null) {
                 logger.warn("The wmm has no relation named {} to break symmetry on." +
-                        " Symmetry breaking was disabled.", symmBreakRelName);
+                        " Symmetry breaking was disabled.", symmBreakTarget);
             } else {
-                logger.info("Breaking symmetry on relation: " + symmBreakRelName);
+                logger.info("Breaking symmetry on relation: " + symmBreakTarget);
                 logger.info("Breaking by sync degree: " + breakBySyncDegree);
             }
         }
     }
 
     public static SymmetryEncoder withContext(EncodingContext context, Wmm memoryModel, Context analysisContext) throws InvalidConfigurationException {
-        SymmetryEncoder encoder = new SymmetryEncoder(context, memoryModel, analysisContext);
-        context.getTask().getConfig().inject(encoder);
-        return encoder;
+        return new SymmetryEncoder(context, memoryModel, analysisContext, context.getTask().getConfig());
     }
 
     @Override
     public void initializeEncoding(SolverContext context) { }
 
-    public BooleanFormula encodeFullSymmetry() {
-        BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
-        BooleanFormula enc = bmgr.makeTrue();
-        if (rel == null) {
-            return enc;
+    public BooleanFormula encodeFullSymmetryBreaking() {
+        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
+        if (rel != null) {
+            return symm.getNonTrivialClasses().stream()
+                    .map(symmClass -> encodeSymmetryBreakingOnClass(rel, symmClass))
+                    .reduce(bmgr.makeTrue(), bmgr::and);
         }
-
-        for (EquivalenceClass<Thread> symmClass : symm.getNonTrivialClasses()) {
-            enc = bmgr.and(enc, encodeSymmetryClass(symmClass));
-        }
-        return enc;
+        return bmgr.makeTrue();
     }
 
-    public BooleanFormula encodeSymmetryClass(EquivalenceClass<Thread> symmClass) {
-        SolverContext ctx = context.getSolverContext();
-        BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager();
-        BooleanFormula enc = bmgr.makeTrue();
-        if (rel == null || symmClass.getEquivalence() != symm) {
-            return enc;
-        }
+    private BooleanFormula encodeSymmetryBreakingOnClass(Relation rel, EquivalenceClass<Thread> symmClass) {
+        Preconditions.checkArgument(symmClass.getEquivalence() == symm,
+                "Symmetry class belongs to unexpected symmetry relation.");
+        Preconditions.checkNotNull(rel);
 
-        Thread rep = symmClass.getRepresentative();
-        List<Thread> symmThreads = new ArrayList<>(symmClass);
+        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
+        final Thread rep = symmClass.getRepresentative();
+        final List<Thread> symmThreads = new ArrayList<>(symmClass);
         symmThreads.sort(Comparator.comparingInt(Thread::getId));
 
-
         // ===== Construct row =====
         //IMPORTANT: Each thread writes to its own special location for the purpose of starting/terminating threads
         // These need to get skipped.
         Thread t1 = symmThreads.get(0);
-        List<Tuple> r1Tuples = new ArrayList<>();
+        List<Tuple> t1Tuples = new ArrayList<>();
         for (Tuple t : rel.getMaxTupleSet()) {
             Event a = t.getFirst();
             Event b = t.getSecond();
             if (!a.is(Tag.C11.PTHREAD) && !b.is(Tag.C11.PTHREAD)
                     && a.getThread() == t1 && symmClass.contains(b.getThread())) {
-                r1Tuples.add(t);
+                t1Tuples.add(t);
             }
         }
-        sort(r1Tuples);
+        sort(t1Tuples);
 
         // Construct symmetric rows
+        BooleanFormula enc = bmgr.makeTrue();
         for (int i = 1; i < symmThreads.size(); i++) {
             Thread t2 = symmThreads.get(i);
             Function<Event, Event> p = symm.createTransposition(t1, t2);
-            List<Tuple> r2Tuples = r1Tuples.stream().map(t -> t.permute(p)).collect(Collectors.toList());
+            List<Tuple> t2Tuples = t1Tuples.stream().map(t -> t.permute(p)).collect(Collectors.toList());
 
-            List<BooleanFormula> r1 = r1Tuples.stream().map(t -> context.edge(rel, t)).collect(Collectors.toList());
-            List<BooleanFormula> r2 = r2Tuples.stream().map(t -> context.edge(rel, t)).collect(Collectors.toList());
+            List<BooleanFormula> r1 = t1Tuples.stream().map(t -> context.edge(rel, t)).collect(Collectors.toList());
+            List<BooleanFormula> r2 = t2Tuples.stream().map(t -> context.edge(rel, t)).collect(Collectors.toList());
             final String id = "_" + rep.getId() + "_" + i;
             enc = bmgr.and(enc, encodeLexLeader(id, r2, r1, context)); // r1 >= r2
 
             t1 = t2;
-            r1Tuples = r2Tuples;
+            t1Tuples = t2Tuples;
         }
 
         return enc;
@@ -149,16 +155,15 @@ private void sort(List<Tuple> row) {
         // ====== Sync-degree based order ======
 
         // Setup of data structures
-        Set<Event> inEvents = new HashSet<>();
-        Set<Event> outEvents = new HashSet<>();
+        final Set<Event> inEvents = new HashSet<>();
+        final Set<Event> outEvents = new HashSet<>();
         for (Tuple t : row) {
             inEvents.add(t.getFirst());
             outEvents.add(t.getSecond());
         }
 
-        Map<Event, Integer> combInDegree = new HashMap<>(inEvents.size());
-        Map<Event, Integer> combOutDegree = new HashMap<>(outEvents.size());
-
+        final Map<Event, Integer> combInDegree = new HashMap<>(inEvents.size());
+        final Map<Event, Integer> combOutDegree = new HashMap<>(outEvents.size());
         for (Event e : inEvents) {
             int syncDeg = axioms.stream()
                     .mapToInt(ax -> ax.getRelation().getMinTupleSet().getBySecond(e).size() + 1).max().orElse(0);
@@ -189,7 +194,7 @@ we will have r1(i) = FALSE and r2(i) = TRUE.
     */
     public static BooleanFormula encodeLexLeader(String uniqueIdent, List<BooleanFormula> r1, List<BooleanFormula> r2, EncodingContext context) {
         Preconditions.checkArgument(r1.size() == r2.size());
-        BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
+        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         // Return TRUE if there is nothing to encode
         if(r1.isEmpty()) {
         	return bmgr.makeTrue();
@@ -226,7 +231,27 @@ public static BooleanFormula encodeLexLeader(String uniqueIdent, List<BooleanFor
         BooleanFormula b = r2.get(size-1);
         enc = bmgr.and(enc, bmgr.or(bmgr.not(ylast), bmgr.not(a), b));
 
-
         return enc;
     }
+
+
+
+    // ========================================
+    // We use a dummy relation to break on control flow rather than a typical relation.
+    // This relation contains a self-loop for each event that represents a control-flow branch.
+    private class CfRelation extends Relation {
+
+        @Override
+        public TupleSet getMinTupleSet() { return getMaxTupleSet(); }
+
+        @Override
+        public TupleSet getMaxTupleSet() {
+            final BranchEquivalence branchEq = context.getAnalysisContext().requires(BranchEquivalence.class);
+            return branchEq.getAllEquivalenceClasses().stream()
+                    .filter(c -> c != branchEq.getInitialClass() && c != branchEq.getUnreachableClass())
+                    .map(EquivalenceClass::getRepresentative)
+                    .map(rep -> new Tuple(rep, rep))
+                    .collect(Collectors.toCollection(TupleSet::new));
+        }
+    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/witness/visitors/VisitorXML.java

@@ -42,6 +42,9 @@ public Object visitElement(XMLParser.ElementContext ctx) {
 					if(key.equals(UNROLLBOUND.toString())) {
 						graph.addAttribute(key, value);	
 					}
+					if(key.equals(WITNESSTYPE.toString()) && !value.equals("violation_witness")) {
+						throw new ParsingException("Dartagnan can only validate violation witnesses");	
+					}
 				}
 			}
 			if(ctx.Name(0).getText().equals("node")) {

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemEvent.java

@@ -55,7 +55,7 @@ public void setMo(String mo){
     }
 
     public boolean canRace() {
-    	return mo == null || mo.equals(C11.NONATOMIC);
+    	return mo.equals("") || mo.equals(C11.NONATOMIC);
     }
 
 	// Visitor

dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java

@@ -72,7 +72,7 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur
         // For validation this contains information.
         // For verification graph.encode() just returns ctx.mkTrue()
         prover.addConstraint(task.getWitness().encode(context));
-        prover.addConstraint(symmetryEncoder.encodeFullSymmetry());
+        prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking());
 
         BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager();
         BooleanFormula assumptionLiteral = bmgr.makeVariable("DAT3M_spec_assumption");

dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/IncrementalSolver.java

@@ -72,7 +72,7 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur
         // For validation this contains information.
         // For verification graph.encode() just returns ctx.mkTrue()
         prover.addConstraint(task.getWitness().encode(context));
-        prover.addConstraint(symmetryEncoder.encodeFullSymmetry());
+        prover.addConstraint(symmetryEncoder.encodeFullSymmetryBreaking());
         logger.info("Starting push()");
         prover.push();
         prover.addConstraint(propertyEncoding);

dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java

@@ -150,7 +150,7 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur
         logger.info("Starting encoding using " + ctx.getVersion());
         prover.addConstraint(programEncoder.encodeFullProgram());
         prover.addConstraint(baselineEncoder.encodeFullMemoryModel());
-        prover.addConstraint(symmEncoder.encodeFullSymmetry());
+        prover.addConstraint(symmEncoder.encodeFullSymmetryBreaking());
 
         prover.push();
         prover.addConstraint(propertyEncoding);

dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/TwoSolvers.java

@@ -82,7 +82,7 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur
 		prover1.addConstraint(encodeWitness);
         prover2.addConstraint(encodeWitness);
 
-        BooleanFormula encodeSymm = symmetryEncoder.encodeFullSymmetry();
+        BooleanFormula encodeSymm = symmetryEncoder.encodeFullSymmetryBreaking();
         prover1.addConstraint(encodeSymm);
         prover2.addConstraint(encodeSymm);
 

pom.xml

@@ -4,7 +4,7 @@
 
   <groupId>com.dat3m</groupId>
   <artifactId>dat3m</artifactId>
-  <version>3.1.0</version>
+  <version>3.1.1</version>
   <packaging>pom</packaging>
 
   <name>dat3m</name>

svcomp/pom.xml

@@ -6,7 +6,7 @@
   <parent>
     <artifactId>dat3m</artifactId>
     <groupId>com.dat3m</groupId>
-    <version>3.1.0</version>
+    <version>3.1.1</version>
   </parent>
 
   <groupId>com.dat3m.svcomp</groupId>
@@ -27,7 +27,7 @@
     <dependency>
       <groupId>com.dat3m.dartagnan</groupId>
       <artifactId>dartagnan</artifactId>
-      <version>3.1.0</version>
+      <version>3.1.1</version>
     </dependency>
     <dependency>
       <groupId>commons-cli</groupId>