From 336e853197bc5a4f95be4fd9121d54facfc4a52a Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 21 Nov 2024 15:04:55 +0100 Subject: [PATCH] Replace CAATs RangeIdentityGraph by a general ProjectionIdentityGraph (can do Range and Domain) Remove default fallback to StaticDefaultWMMGraph for unknown relations in ExecutionGraph. This fallback was dangerous. Instead, the RefinementSolver shall cut unknown relations. --- .../predicates/misc/PredicateVisitor.java | 2 +- ...raph.java => ProjectionIdentityGraph.java} | 21 +++++++++++++++---- .../solver/caat/reasoning/Reasoner.java | 16 +++++++++----- .../solver/caat4wmm/ExecutionGraph.java | 17 +++++++++------ .../solving/RefinementSolver.java | 9 +++++--- 5 files changed, 46 insertions(+), 19 deletions(-) rename dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/{RangeIdentityGraph.java => ProjectionIdentityGraph.java} (72%) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java index 3c095ac7ba..c3b66c2b39 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java @@ -17,7 +17,7 @@ public interface PredicateVisitor { 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); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/RangeIdentityGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/ProjectionIdentityGraph.java similarity index 72% rename from dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/RangeIdentityGraph.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/ProjectionIdentityGraph.java index 055f668281..abc04b25c5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/RangeIdentityGraph.java +++ b/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 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 forwardPropagate(CAATPredicate changedSource, Collection @Override public TRet accept(PredicateVisitor visitor, TData data, TContext context) { - return visitor.visitRangeIdentity(this, data, context); + return visitor.visitProjectionIdentity(this, data, context); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java index 3af7850c73..50a3121fa0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java +++ b/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 visitSetIdentity(RelationGraph graph, Edge edge, } @Override - public Conjunction visitRangeIdentity(RelationGraph graph, Edge edge, Void unused) { + public Conjunction 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 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 reason = computeReason(inner, inEdge); + if (e.getDerivationLength() < edge.getDerivationLength()) { + Conjunction 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 diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index a6981cbb03..132abb092e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/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()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index d89a872336..b15c671c8f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/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) {