New Execution Model (#783)

Signed-off-by: Tianrui Zheng <[email protected]>
Co-authored-by: Tianrui Zheng <[email protected]>

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

@@ -20,9 +20,10 @@
 import com.dat3m.dartagnan.utils.Result;
 import com.dat3m.dartagnan.utils.Utils;
 import com.dat3m.dartagnan.utils.options.BaseOptions;
+import com.dat3m.dartagnan.verification.model.ExecutionModelManager;
+import com.dat3m.dartagnan.verification.model.ExecutionModelNext;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.verification.VerificationTask.VerificationTaskBuilder;
-import com.dat3m.dartagnan.verification.model.ExecutionModel;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
 import com.dat3m.dartagnan.verification.solving.DataRaceSolver;
 import com.dat3m.dartagnan.verification.solving.ModelChecker;
@@ -230,20 +231,23 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir
             throws InvalidConfigurationException, SolverException, IOException {
         Preconditions.checkArgument(modelChecker.hasModel(), "No execution graph to generate.");
 
-        final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext());
-        m.initialize(prover.getModel());
+        final EncodingContext encodingContext = modelChecker instanceof RefinementSolver refinementSolver ?
+            refinementSolver.getContextWithFullWmm() : modelChecker.getEncodingContext();
+        final ExecutionModelNext model = new ExecutionModelManager().buildExecutionModel(
+            encodingContext, prover.getModel()
+        );
         final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
         final String progName = task.getProgram().getName();
         final int fileSuffixIndex = progName.lastIndexOf('.');
         final String name = progName.isEmpty() ? "unnamed_program" :
                 (fileSuffixIndex == - 1) ? progName : progName.substring(0, fileSuffixIndex);
         // 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
-        // FR edges only give ordering information which is known if the pair is also in PO
         // CO edges only give ordering information which is known if the pair is also in PO
-        return generateGraphvizFile(m, 1, (x, y) -> true, (x, y) -> !x.getThread().equals(y.getThread()),
-                (x, y) -> !x.getThread().equals(y.getThread()), getOrCreateOutputDirectory() + "/", name,
-                synContext, witnessType.convertToPng());
+        return generateGraphvizFile(model, 1, (x, y) -> true,
+                (x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()),
+                getOrCreateOutputDirectory() + "/", name,
+                synContext, witnessType.convertToPng(), encodingContext.getTask().getConfig());
     }
 
     private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover,

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

@@ -75,6 +75,7 @@ public class OptionNames {
 
     // Witness Options
     public static final String WITNESS_ORIGINAL_PROGRAM_PATH = "witness.originalProgramFilePath";
+    public static final String WITNESS_SHOW = "witness.show";
 
     // SVCOMP Options
     public static final String PROPERTYPATH = "svcomp.property";

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java

@@ -0,0 +1,45 @@
+package com.dat3m.dartagnan.solver.caat4wmm;
+
+import com.dat3m.dartagnan.solver.caat.domain.Domain;
+import com.dat3m.dartagnan.verification.model.event.EventModel;
+import com.dat3m.dartagnan.verification.model.ExecutionModelNext;
+
+import java.util.Collection;
+import java.util.List;
+
+
+// TODO: this class is temporary and needs to be merged into EventDomain
+// once there is one ExecutionModel for all use cases.
+public class EventDomainNext implements Domain<EventModel> {
+    private final ExecutionModelNext executionModel;
+    private final List<EventModel> eventList;
+
+    public EventDomainNext(ExecutionModelNext executionModel) {
+        this.executionModel = executionModel;
+        eventList = executionModel.getEventModels();
+    }
+
+    @Override
+    public int size() {
+        return eventList.size();
+    }
+
+    @Override
+    public Collection<EventModel> getElements() {
+        return eventList;
+    }
+
+    @Override
+    public int getId(Object obj) {
+        if (obj instanceof EventModel em) {
+            return em.getId();
+        } else {
+            throw new IllegalArgumentException(obj + " is not of type EventModel");
+        }
+    }
+
+    @Override
+    public EventModel getObjectById(int id) {
+        return eventList.get(id);
+    }
+}

dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java

@@ -496,7 +496,7 @@ private void extractMemoryLayout() {
         for (MemoryObject obj : getProgram().getMemory().getObjects()) {
             final boolean isAllocated = obj.isStaticallyAllocated() || isTrue(encodingContext.execution(obj.getAllocationSite()));
             if (isAllocated) {
-                final BigInteger address = (BigInteger) model.evaluate(encodingContext.address(obj));
+                final ValueModel address = new ValueModel(model.evaluate(encodingContext.address(obj)));
                 final BigInteger size = (BigInteger) model.evaluate(encodingContext.size(obj));
                 memoryLayoutMap.put(obj, new MemoryObjectModel(obj, address, size));
             }