Relation Model Implementation

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

@@ -22,6 +22,7 @@
 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.model.ExecutionModelManager;
 import com.dat3m.dartagnan.verification.solving.AssumeSolver;
 import com.dat3m.dartagnan.verification.solving.DataRaceSolver;
 import com.dat3m.dartagnan.verification.solving.ModelChecker;
@@ -225,8 +226,9 @@ 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 ExecutionModel m = ExecutionModelManager.newManager(modelChecker.getEncodingContext())
+                                                      .setEncodingContextForWitness(modelChecker.getEncodingContextForWitness())
+                                                      .initializeModel(prover.getModel());
         final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
         final String progName = task.getProgram().getName();
         final int fileSuffixIndex = progName.lastIndexOf('.');

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

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

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

@@ -9,6 +9,7 @@
 import com.dat3m.dartagnan.utils.logic.DNF;
 import com.dat3m.dartagnan.verification.Context;
 import com.dat3m.dartagnan.verification.model.ExecutionModel;
+import com.dat3m.dartagnan.verification.model.ExecutionModelManager;
 import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
@@ -22,27 +23,29 @@
 public class WMMSolver {
 
     private final ExecutionGraph executionGraph;
-    private final ExecutionModel executionModel;
+    private final ExecutionModelManager executionModelManager;
     private final CAATSolver solver;
     private final CoreReasoner reasoner;
 
-    private WMMSolver(RefinementModel refinementModel, Context analysisContext, ExecutionModel m) {
+    private WMMSolver(RefinementModel refinementModel, Context analysisContext, ExecutionModelManager manager) {
         final RelationAnalysis ra = analysisContext.requires(RelationAnalysis.class);
         this.executionGraph = new ExecutionGraph(refinementModel, ra);
-        this.executionModel = m;
+        this.executionModelManager = manager;
         this.reasoner = new CoreReasoner(analysisContext, executionGraph);
         this.solver = CAATSolver.create();
     }
 
     public static WMMSolver withContext(RefinementModel refinementModel, EncodingContext context,
-            Context analysisContext, Configuration config) throws InvalidConfigurationException {
-        final var solver = new WMMSolver(refinementModel, analysisContext, ExecutionModel.withContext(context));
+            EncodingContext contextForWitness, Configuration config) throws InvalidConfigurationException {
+        ExecutionModelManager manager = ExecutionModelManager.newManager(context)
+                                                             .setEncodingContextForWitness(contextForWitness);
+        final var solver = new WMMSolver(refinementModel, contextForWitness.getAnalysisContext(), manager);
         config.inject(solver.reasoner);
         return solver;
     }
 
     public ExecutionModel getExecution() {
-        return executionModel;
+        return executionModelManager.getExecutionModel();
     }
 
     public ExecutionGraph getExecutionGraph() {
@@ -52,8 +55,7 @@ public ExecutionGraph getExecutionGraph() {
     public Result check(Model model) {
         // ============ Extract ExecutionModel ==============
         long curTime = System.currentTimeMillis();
-        executionModel.initialize(model);
-        executionGraph.initializeFromModel(executionModel);
+        executionGraph.initializeFromModel(executionModelManager.initializeModel(model));
         long extractTime = System.currentTimeMillis() - curTime;
 
         // ============== Run the CAATSolver ==============

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

@@ -3,6 +3,8 @@
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.core.CondJump;
+import com.dat3m.dartagnan.program.event.core.Local;
+import com.dat3m.dartagnan.program.event.core.Assert;
 
 import java.math.BigInteger;
 
@@ -74,7 +76,7 @@ void setWasExecuted(boolean flag) {
     }
 
     public int getCoherenceIndex() { return coIndex; }
-    void setCoherenceIndex(int index) { coIndex = index; }
+    public void setCoherenceIndex(int index) { coIndex = index; }
 
     public boolean isMemoryEvent() { return event.hasTag(MEMORY); }
     public boolean isInit() {
@@ -92,6 +94,12 @@ public boolean isExclusive() {
     public boolean isRMW() {
     	return event.hasTag(RMW);
     }
+    public boolean isLocal() {
+        return event instanceof Local;
+    }
+    public boolean isAssert() {
+        return event instanceof Assert;
+    }
 
     public boolean hasTag(String tag) {
     	return event.hasTag(tag);

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

@@ -5,6 +5,7 @@
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.*;
+import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument;
 import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic;
@@ -14,6 +15,9 @@
 import com.dat3m.dartagnan.utils.dependable.DependencyGraph;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.wmm.Wmm;
+import com.dat3m.dartagnan.wmm.Relation;
+import com.dat3m.dartagnan.verification.model.relation.RelationModel;
+import com.dat3m.dartagnan.verification.model.relation.RelationModel.EdgeModel;
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Lists;
@@ -28,9 +32,9 @@
 import java.math.BigInteger;
 import java.util.*;
 import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
-import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO;
-import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF;
+import static com.dat3m.dartagnan.wmm.RelationNameRepository.*;
 import static com.google.common.base.Preconditions.checkNotNull;
 
 /*
@@ -44,13 +48,18 @@ public class ExecutionModel {
     private static final Logger logger = LogManager.getLogger(ExecutionModel.class);
 
     private final EncodingContext encodingContext;
+    private EncodingContext encodingContextForWitness;
 
     // ============= Model specific  =============
     private Model model;
     private Filter eventFilter;
     private boolean extractCoherences;
 
     private final EventMap eventMap;
+    private ExecutionModelManager manager;
+    private final Map<Relation, RelationModel> relations;
+    private final Map<String, RelationModel> definedRelations;
+    private final Map<String, EdgeModel> edges;
     // The event list is sorted lexicographically by (threadID, cID)
     private final ArrayList<EventData> eventList;
     private final ArrayList<Thread> threadList;
@@ -109,6 +118,9 @@ private ExecutionModel(EncodingContext c) {
         addrDepMap = new HashMap<>();
         ctrlDepMap = new HashMap<>();
         coherenceMap = new HashMap<>();
+        relations = new HashMap<>();
+        definedRelations = new HashMap<>();
+        edges = new HashMap<>();
 
         createViews();
     }
@@ -141,11 +153,15 @@ private void createViews() {
     public VerificationTask getTask() {
         return encodingContext.getTask();
     }
-    
+
     public Wmm getMemoryModel() {
         return encodingContext.getTask().getMemoryModel();
     }
 
+    public Wmm getMemoryModelForWitness() {
+        return getContextForWitness().getTask().getMemoryModel();
+    }
+
     public Program getProgram() {
         return encodingContext.getTask().getProgram();
     }
@@ -157,6 +173,15 @@ public Model getModel() {
     public EncodingContext getContext() {
         return encodingContext;
     }
+    public EncodingContext getContextForWitness() {
+        if (encodingContextForWitness != null) {
+            return encodingContextForWitness;
+        }
+        return encodingContext;
+    }
+    void setEncodingContextForWitness(EncodingContext c) {
+        encodingContextForWitness = c;
+    }
     public Filter getEventFilter() {
         return eventFilter;
     }
@@ -172,6 +197,37 @@ public List<Thread> getThreads() {
         return threadListView;
     }
 
+    public ExecutionModelManager getManager() {
+        return manager;
+    }
+
+    public boolean containsRelation(Relation r) {
+        return relations.containsKey(r);
+    }
+
+    public void addRelation(Relation r, RelationModel rm) {
+        relations.put(r, rm);
+        if (rm.isDefined()) {
+            definedRelations.put(rm.getName(), rm);
+        }
+    }
+
+    public RelationModel getRelationModel(String name) {
+        return definedRelations.get(name);
+    }
+
+    public RelationModel getRelationModel(Relation r) {
+        return relations.get(r);
+    }
+
+    public EdgeModel getEdge(String identifier) {
+        return edges.get(identifier);
+    }
+
+    public void addEdge(EdgeModel edge) {
+        edges.put(edge.getIdentifier(), edge);
+    }
+
     public Map<MemoryObject, MemoryObjectModel> getMemoryLayoutMap() { return memoryLayoutMapView; }
     public Map<Thread, List<EventData>> getThreadEventsMap() {
         return threadEventsMapView;
@@ -238,6 +294,11 @@ public void initialize(Model model, Filter eventFilter, boolean extractCoherence
         }
     }
 
+    public void initialize(Model model, ExecutionModelManager manager) {
+        this.manager = manager;
+        initialize(model, true);
+    }
+
     //========================== Internal methods  =========================
 
     private void extractEventsFromModel() {
@@ -273,7 +334,7 @@ private void extractEventsFromModel() {
                     e = e.getSuccessor();
                     continue;
                 }
-                if (eventFilter.apply(e)) {
+                if (eventFilter.apply(e) || e instanceof Local || e instanceof Assert) {
                     addEvent(e, id++, localId++);
                 }
                 trackDependencies(e);

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

@@ -0,0 +1,48 @@
+package com.dat3m.dartagnan.verification.model;
+
+import com.dat3m.dartagnan.encoding.EncodingContext;
+import com.dat3m.dartagnan.verification.model.ExecutionModel;
+import com.dat3m.dartagnan.verification.model.relation.RelationModelManager;
+
+import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+
+import java.util.*;
+
+import static com.dat3m.dartagnan.wmm.RelationNameRepository.*;
+
+
+public class ExecutionModelManager {
+    private final ExecutionModel model;
+    private final RelationModelManager rmManager;
+    private final Set<String> necessaryRelations;
+
+    private ExecutionModelManager(ExecutionModel model) {
+        this.model = model;
+        rmManager = RelationModelManager.newRMManager(model);
+        necessaryRelations = new HashSet<>(Set.of(PO, RF, CO));
+    }
+
+    public static ExecutionModelManager newManager(EncodingContext context)
+            throws InvalidConfigurationException{
+        ExecutionModel m = ExecutionModel.withContext(context);
+        return new ExecutionModelManager(m);
+    }
+
+    public ExecutionModel getExecutionModel() { return model; }
+
+    public ExecutionModelManager setEncodingContextForWitness(EncodingContext c) {
+        model.setEncodingContextForWitness(c);
+        return this;
+    }
+
+    public ExecutionModel initializeModel(Model m) {
+        model.initialize(m, this);
+        extractRelations(new ArrayList<>(necessaryRelations));
+        return model;
+    }
+
+    public void extractRelations(List<String> relNames) {
+        rmManager.extractRelations(relNames);
+    }
+}