Add domain identities to CAAT & remove dangerous fallback code in ExecutionGraph

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java

@@ -17,7 +17,7 @@ public interface PredicateVisitor<TRet, TData, TContext> {
     default TRet visitCartesian(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
     default TRet visitInverse(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
     default TRet visitSetIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
-    default TRet visitRangeIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
+    default TRet visitProjectionIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
     default TRet visitReflexiveClosure(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
     default TRet visitTransitiveClosure(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }
     default TRet visitRecursiveGraph(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); }

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/RangeIdentityGraph.java → dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/ProjectionIdentityGraph.java

@@ -12,21 +12,34 @@
 import java.util.List;
 import java.util.stream.Collectors;
 
-public class RangeIdentityGraph extends MaterializedGraph {
+public class ProjectionIdentityGraph extends MaterializedGraph {
+
+    public enum Dimension {
+        DOMAIN,
+        RANGE
+    }
 
     private final RelationGraph inner;
+    private final Dimension dimension;
 
     @Override
     public List<RelationGraph> getDependencies() {
         return List.of(inner);
     }
 
-    public RangeIdentityGraph(RelationGraph inner) {
+    public Dimension getProjectionDimension() { return dimension; }
+
+    public ProjectionIdentityGraph(RelationGraph inner, Dimension dimension) {
         this.inner = inner;
+        this.dimension = dimension;
     }
 
     private Edge derive(Edge e) {
-        return new Edge(e.getSecond(), e.getSecond(), e.getTime(), e.getDerivationLength() + 1);
+        int id = switch (this.dimension) {
+            case RANGE -> e.getSecond();
+            case DOMAIN -> e.getFirst();
+        };
+        return new Edge(id, id, e.getTime(), e.getDerivationLength() + 1);
     }
 
     @Override
@@ -50,7 +63,7 @@ public Collection<Edge> forwardPropagate(CAATPredicate changedSource, Collection
 
     @Override
     public <TRet, TData, TContext> TRet accept(PredicateVisitor<TRet, TData, TContext> visitor, TData data, TContext context) {
-        return visitor.visitRangeIdentity(this, data, context);
+        return visitor.visitProjectionIdentity(this, data, context);
     }
 
 }

dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java

@@ -8,6 +8,7 @@
 import com.dat3m.dartagnan.solver.caat.predicates.misc.PredicateVisitor;
 import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge;
 import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph;
+import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.ProjectionIdentityGraph;
 import com.dat3m.dartagnan.solver.caat.predicates.sets.Element;
 import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate;
 import com.dat3m.dartagnan.utils.logic.Conjunction;
@@ -220,19 +221,24 @@ public Conjunction<CAATLiteral> visitSetIdentity(RelationGraph graph, Edge edge,
         }
 
         @Override
-        public Conjunction<CAATLiteral> visitRangeIdentity(RelationGraph graph, Edge edge, Void unused) {
+        public Conjunction<CAATLiteral> visitProjectionIdentity(RelationGraph graph, Edge edge, Void unused) {
             assert edge.isLoop();
 
             RelationGraph inner = (RelationGraph) graph.getDependencies().get(0);
-            for (Edge inEdge : inner.inEdges(edge.getSecond())) {
+            ProjectionIdentityGraph.Dimension dim = ((ProjectionIdentityGraph)graph).getProjectionDimension();
+            Iterable<Edge> edges = switch (dim) {
+                case RANGE -> inner.inEdges(edge.getSecond());
+                case DOMAIN -> inner.outEdges(edge.getFirst());
+            };
+            for (Edge e : edges) {
                 // We use the first edge we find
-                if (inEdge.getDerivationLength() < edge.getDerivationLength()) {
-                    Conjunction<CAATLiteral> reason = computeReason(inner, inEdge);
+                if (e.getDerivationLength() < edge.getDerivationLength()) {
+                    Conjunction<CAATLiteral> reason = computeReason(inner, e);
                     assert !reason.isFalse();
                     return reason;
                 }
             }
-            throw new IllegalStateException("RangeIdentityGraph: No matching edge is found");
+            throw new IllegalStateException("ProjectionIdentityGraph: No matching edge is found");
         }
 
         @Override

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

@@ -230,11 +230,15 @@ private RelationGraph createGraphFromRelation(Relation rel) {
             graph = new ProgramOrderGraph();
         } else if (relClass == Coherence.class) {
             graph = new CoherenceGraph();
-        } else if (relClass == Inverse.class || relClass == TransitiveClosure.class || relClass == RangeIdentity.class) {
+        } else if (relClass == RangeIdentity.class || relClass == DomainIdentity.class) {
             RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0));
-            graph = relClass == Inverse.class ? new InverseGraph(g) :
-                    relClass == TransitiveClosure.class ? new TransitiveGraph(g) :
-                            new RangeIdentityGraph(g);
+            ProjectionIdentityGraph.Dimension dim = relClass == RangeIdentity.class ?
+                    ProjectionIdentityGraph.Dimension.RANGE :
+                    ProjectionIdentityGraph.Dimension.DOMAIN;
+            graph = new ProjectionIdentityGraph(g, dim);
+        } else if (relClass == Inverse.class || relClass == TransitiveClosure.class) {
+            RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0));
+            graph = relClass == Inverse.class ? new InverseGraph(g) : new TransitiveGraph(g);
         } else if (relClass == Union.class || relClass == Intersection.class) {
             RelationGraph[] graphs = new RelationGraph[dependencies.size()];
             for (int i = 0; i < graphs.length; i++) {
@@ -264,8 +268,9 @@ private RelationGraph createGraphFromRelation(Relation rel) {
         } else if (relClass == Empty.class) {
             graph = new EmptyGraph();
         } else {
-            // This is a fallback for all unimplemented static graphs
-            graph = new StaticDefaultWMMGraph(rel, ra);
+            final String error = String.format("Cannot handle relation %s with definition of type %s.",
+                    rel, relClass.getSimpleName());
+            throw new UnsupportedOperationException(error);
         }
 
         graph.setName(rel.getNameOrTerm());

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

@@ -11,11 +11,11 @@
 import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis;
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.MemoryEvent;
+import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
 import com.dat3m.dartagnan.program.event.metadata.OriginalId;
 import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
 import com.dat3m.dartagnan.program.filter.Filter;
-import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.solver.caat.CAATSolver;
 import com.dat3m.dartagnan.solver.caat4wmm.RefinementModel;
 import com.dat3m.dartagnan.solver.caat4wmm.Refiner;
@@ -234,7 +234,7 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati
         final Refiner refiner = new Refiner(refinementModel);
         final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task);
 
-        logger.info("Starting encoding using " + ctx.getVersion());
+        logger.info("Starting encoding using {}", ctx.getVersion());
         prover.writeComment("Program encoding");
         prover.addConstraint(programEncoder.encodeFullProgram());
         prover.writeComment("Memory model (baseline) encoding");
@@ -491,7 +491,10 @@ private static boolean isUnknownDefinitionForCAAT(Definition def) {
         // TODO: We should probably automatically cut all "unknown relation",
         //  i.e., use a white-list of known relations instead of a blacklist of unknown one's.
         return def instanceof LinuxCriticalSections // LKMM
-                || def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation; // GPUs
+                || def instanceof CASDependency // IMM
+                // GPUs
+                || def instanceof SameScope || def instanceof SyncWith
+                || def instanceof SyncFence || def instanceof SyncBar || def instanceof SameVirtualLocation;
     }
 
     private static RefinementModel generateRefinementModel(Wmm original) {