Relation analysis with immutable and lazy data structures

hernanponcedeleon · Sep 27, 2024 · b632f5c · b632f5c
1 parent 73ba96c
commit b632f5c
Show file tree

Hide file tree

Showing 37 changed files with 5,251 additions and 2,829 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java
@@ -60,6 +60,9 @@ public static String getHomeDirectory() {
     }
 
     public static String getCatDirectory() {
+        if (USE_TEST_PATH) {
+            return "../cat";
+        }
         String env = System.getenv("DAT3M_HOME");
         env = env == null ? "" : env;
         return env + "/cat";

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/RelationAnalysisMethod.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/RelationAnalysisMethod.java
@@ -3,15 +3,15 @@
 import java.util.Arrays;
 
 public enum RelationAnalysisMethod implements OptionInterface {
-	NONE, NATIVE;
+	NONE, NATIVE, LAZY;
 
 	public static RelationAnalysisMethod getDefault() {
 		return NATIVE;
 	}
 
 	// Used to decide the order shown by the selector in the UI
 	public static RelationAnalysisMethod[] orderedValues() {
-		RelationAnalysisMethod[] order = { NONE, NATIVE };
+		RelationAnalysisMethod[] order = { NONE, NATIVE, LAZY };
 		// Be sure no element is missing
 		assert(Arrays.asList(order).containsAll(Arrays.asList(values())));
 		return order;

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java
@@ -7,7 +7,9 @@
 import com.dat3m.dartagnan.wmm.Relation;
 import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
 import com.dat3m.dartagnan.wmm.definition.*;
-import com.dat3m.dartagnan.wmm.utils.EventGraph;
+import com.dat3m.dartagnan.wmm.utils.graph.EventGraph;
+import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph;
+import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph;
 
 import java.util.HashMap;
 import java.util.Map;
@@ -61,8 +63,8 @@ public Map<Relation, EventGraph> visitComposition(Composition comp) {
 
         final Relation r1 = comp.getLeftOperand();
         final Relation r2 = comp.getRightOperand();
-        final EventGraph set1 = new EventGraph();
-        final EventGraph set2 = new EventGraph();
+        final MutableEventGraph set1 = new MapEventGraph();
+        final MutableEventGraph set2 = new MapEventGraph();
         final RelationAnalysis.Knowledge k1 = ra.getKnowledge(r1);
         final RelationAnalysis.Knowledge k2 = ra.getKnowledge(r2);
         Map<Event, Set<Event>> out = ra.getKnowledge(r1).getMaySet().getOutMap();
@@ -85,7 +87,7 @@ public Map<Relation, EventGraph> visitComposition(Composition comp) {
     public Map<Relation, EventGraph> visitDomainIdentity(DomainIdentity domId) {
         final RelationAnalysis.Knowledge k1 = ra.getKnowledge(domId.getOperand());
         Map<Event, Set<Event>> out = k1.getMaySet().getOutMap();
-        EventGraph result = new EventGraph();
+        MutableEventGraph result = new MapEventGraph();
         news.apply((e1, e2) ->
             out.getOrDefault(e1, Set.of()).forEach(e -> {
                 if (!k1.getMustSet().contains(e1, e)) {
@@ -100,7 +102,7 @@ public Map<Relation, EventGraph> visitDomainIdentity(DomainIdentity domId) {
     public Map<Relation, EventGraph> visitRangeIdentity(RangeIdentity rangeId) {
         final RelationAnalysis.Knowledge k1 = ra.getKnowledge(rangeId.getOperand());
         Map<Event, Set<Event>> in = k1.getMaySet().getInMap();
-        EventGraph result = new EventGraph();
+        MutableEventGraph result = new MapEventGraph();
         news.apply((e1, e2) ->
             in.getOrDefault(e2, Set.of()).forEach(e -> {
                 if (!k1.getMustSet().contains(e, e2)) {
@@ -122,7 +124,7 @@ public Map<Relation, EventGraph> visitInverse(Inverse inv) {
     public Map<Relation, EventGraph> visitTransitiveClosure(TransitiveClosure trans) {
         final Relation rel = trans.getDefinedRelation();
         final Relation r1 = trans.getOperand();
-        EventGraph factors = new EventGraph();
+        MutableEventGraph factors = new MapEventGraph();
         final RelationAnalysis.Knowledge k0 = ra.getKnowledge(rel);
         Map<Event, Set<Event>> out = k0.getMaySet().getOutMap();
         news.apply((e1, e2) -> {
@@ -142,7 +144,7 @@ public Map<Relation, EventGraph> visitTransitiveClosure(TransitiveClosure trans)
 
     @Override
     public Map<Relation, EventGraph> visitLinuxCriticalSections(LinuxCriticalSections rscs) {
-        EventGraph queue = new EventGraph();
+        MutableEventGraph queue = new MapEventGraph();
         final RelationAnalysis.Knowledge k0 = ra.getKnowledge(rscs.getDefinedRelation());
         Map<Event, Set<Event>> in = k0.getMaySet().getInMap();
         Map<Event, Set<Event>> out = k0.getMaySet().getOutMap();

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java
@@ -23,7 +23,7 @@
 import com.dat3m.dartagnan.wmm.Relation;
 import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis;
 import com.dat3m.dartagnan.wmm.axiom.Acyclicity;
-import com.dat3m.dartagnan.wmm.utils.EventGraph;
+import com.dat3m.dartagnan.wmm.utils.graph.EventGraph;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;