diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 53f0ab5b59..0e1fd85060 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -239,8 +239,6 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir manager.setContextWithFullWmm(contextWithFullWmm); } final ExecutionModelNext m = manager.initializeModel(prover.getModel()); - // final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext()); - // m.initialize(prover.getModel()); final SyntacticContextAnalysis synContext = newInstance(task.getProgram()); final String progName = task.getProgram().getName(); final int fileSuffixIndex = progName.lastIndexOf('.'); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java index d52a11ad7f..c9617bdba6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java @@ -273,6 +273,10 @@ private void extractEventsFromModel() { e = e.getSuccessor(); continue; } + // In the new model we extract visible events, Locals and Asserts to show them in the + // witness, and extract also CondJumps for tracking internal dependencies. For consistency + // of the view of events which infects the derived relation computation by CAAT, we need + // to extract the same events here in the old model. if (eventFilter.apply(e) || e instanceof Local || e instanceof Assert diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java index 03d0638dd9..5c59f0c6b7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java @@ -1,29 +1,35 @@ package com.dat3m.dartagnan.verification.model; import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.memory.MemoryObject; +import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.verification.model.event.*; import com.dat3m.dartagnan.verification.model.relation.RelationModel; -import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.Relation; -import org.sosy_lab.java_smt.api.Model; -import org.sosy_lab.java_smt.api.Formula; +import com.dat3m.dartagnan.wmm.Wmm; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.Model; -import java.util.*; import java.math.BigInteger; +import java.util.*; import static com.google.common.base.Preconditions.checkNotNull; +// This is a new implementation of ExecutionModel which serves as the data structure +// representing an execution in Dartagnan. It contains instances of EventModel for events +// and RelationModel for relations. It holds the information that has the same name and +// format as the old ExecutionModel so that it can replace the old one easily for CAAT also. +// It is used only by ExecutionGraphVisualizer so far. public class ExecutionModelNext { private final EncodingContext encodingContext; private Model model; - private EncodingContext contextWithFullWmm; // This context is needed for extraction of relations when RefinementSolver being used. + // This context is needed for extraction of relations when RefinementSolver being used. + private EncodingContext contextWithFullWmm; private ExecutionModelManager manager; private final List threadList; @@ -152,6 +158,7 @@ public void addEvent(Event e, EventModel eModel) { public void addRelation(Relation r, RelationModel rModel) { relationMap.put(r, rModel); + // We add an entry for each name of the relation. for (String name : rModel.getNames()) { relationNameMap.put(name, rModel); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModelManager.java index c24ab07ed9..aed2440f51 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModelManager.java @@ -12,8 +12,8 @@ import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; -import java.util.*; import java.math.BigInteger; +import java.util.*; public class EventModelManager { @@ -116,7 +116,11 @@ private EventModel getOrCreateModel(Event e, int id, int localId) { EventModel em = createAndInitializeModel(e); em.setId(id); em.setLocalId(localId); - em.setWasExecuted(true); + if (e instanceof CondJump) { + em.setWasExecuted( + executionModel.isTrue(getEncodingContext().jumpCondition((CondJump) e)) + ); + } else { em.setWasExecuted(true); } eventCache.put(e, em); return em; @@ -171,9 +175,6 @@ private EventModel createAndInitializeModel(Event e) { em = new LocalModel((Local) e); } else if (e instanceof CondJump) { em = new CondJumpModel((CondJump) e); - em.setWasExecuted( - executionModel.isTrue(getEncodingContext().jumpCondition((CondJump) e)) - ); } else { em = new DefaultEventModel(e); } @@ -182,6 +183,8 @@ private EventModel createAndInitializeModel(Event e) { } private boolean toExtract(Event e) { + // We extract visible events, Locals and Asserts to show them in the witness, + // and extract also CondJumps for tracking internal dependencies. return eventFilter.apply(e) || e instanceof Local || e instanceof Assert diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModelManager.java index d616843beb..cb5ee6204f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModelManager.java @@ -9,10 +9,10 @@ import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; import com.dat3m.dartagnan.solver.caat.predicates.PredicateHierarchy; -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.base.SimpleGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.*; +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.sets.SetPredicate; import com.dat3m.dartagnan.solver.caat4wmm.EventDomain; import com.dat3m.dartagnan.solver.caat4wmm.basePredicates.StaticDefaultWMMGraph; @@ -117,11 +117,11 @@ public void extractRelations(List relationNames) { } } - Set predicates = new HashSet<>(relGraphs); PredicateHierarchy hierarchy = new PredicateHierarchy(predicates); hierarchy.initializeToDomain(new EventDomain(oldModel)); + // Populate graphs of base relations. for (CAATPredicate basePred : hierarchy.getBasePredicates()) { if (basePred.getClass() == StaticWMMSet.class || basePred.getClass() == StaticDefaultWMMGraph.class @@ -130,6 +130,7 @@ public void extractRelations(List relationNames) { r.getDefinition().accept(graphPopulator); } + // Do the computation. hierarchy.populate(); for (CAATPredicate pred : hierarchy.getPredicateList()) { @@ -175,8 +176,7 @@ private RelationGraph getOrCreateGraph(Relation r) { if (relGraphCache.containsKey(r)) { return relGraphCache.get(r); } - RelationGraph rg = createGraph(r); - return rg; + return createGraph(r); } private SetPredicate getOrCreateSetFromFilter(Filter filter) { @@ -194,8 +194,8 @@ private EdgeModel getOrCreateEdgeModel(Edge e) { if (edgeModelCache.containsKey(identifier)) { return edgeModelCache.get(identifier); } - final List eventList = executionModel.getEventList(); - EdgeModel em = new EdgeModel(eventList.get(e.getFirst()), eventList.get(e.getSecond())); + EdgeModel em = new EdgeModel(executionModel.getEventModelById(e.getFirst()), + executionModel.getEventModelById(e.getSecond())); edgeModelCache.put(identifier, em); return em; } @@ -211,6 +211,8 @@ private List getVisibleEvents(Thread t) { } + // Usage: Populate graph of the base relations with instances of the Edge class + // based on the information from ExecutionModelNext. private final class BaseRelationGraphPopulator implements Visitor { @Override @@ -429,7 +431,7 @@ public Void visitAddressDependency(DirectAddressDependency addrDirect) { writes.add((RegWriterModel) em); continue; } - if (em.isWrite()) { + if (em.isRegReader()) { for (RegWriterModel write : writes) { for (Register.Read read : ((RegReaderModel) em).getRegisterReads()) { if (read.register() == write.getResultRegister() @@ -492,6 +494,9 @@ public Void visitEmpty(Empty empty) { } + // Create a SimpleGraph for base relations and the specific graph for derived ones, + // so that edges of base relations are set manually and edges of derived ones can be + // computed automatically by PredicateHierarchy. private final class RelationGraphBuilder implements Visitor { @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index 6e1551541c..d75baa1efd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -35,6 +35,7 @@ public abstract class ModelChecker { protected Result res = Result.UNKNOWN; protected EncodingContext context; + // This context is needed for extraction of relations when RefinementSolver being used. protected EncodingContext contextWithFullWmm; private String flaggedPairsOutput = ""; 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 3472cb9deb..6ae83643c8 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 @@ -891,9 +891,9 @@ private static void generateGraphvizFiles(VerificationTask task, ExecutionModelN final SyntacticContextAnalysis emptySynContext = getEmptyInstance(); // File with reason edges only generateGraphvizFile(model, iterationCount, edgeFilter, edgeFilter, edgeFilter, directoryName, fileNameBase, - emptySynContext); + emptySynContext, true); // File with all edges generateGraphvizFile(model, iterationCount, (x, y) -> true, (x, y) -> true, (x, y) -> true, directoryName, - fileNameBase + "-full", emptySynContext); + fileNameBase + "-full", emptySynContext, true); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java index d6a77e881e..636b3fe6b0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java @@ -83,9 +83,6 @@ public void generateGraphOfExecutionModel(Writer writer, String graphName, Execu graphviz.append(String.format("label=\"%s\" \n", graphName)); addAllThreadPos(model); addRelations(model); - // addReadFrom(model); - // addFromRead(model); - // addCoherence(model); graphviz.end(); graphviz.generateOutput(writer); } @@ -180,69 +177,6 @@ private ExecutionGraphVisualizer addProgramOrder(ExecutionModelNext model) { return this; } - // private ExecutionGraphVisualizer addReadFrom(ExecutionModel model) { - - // graphviz.beginSubgraph("ReadFrom"); - // graphviz.setEdgeAttributes("color=green"); - // for (Map.Entry rw : model.getReadWriteMap().entrySet()) { - // EventData r = rw.getKey(); - // EventData w = rw.getValue(); - - // if (ignore(r) || ignore(w) || !rfFilter.test(w, r)) { - // continue; - // } - - // appendEdge(w, r, "label=rf"); - // } - // graphviz.end(); - // return this; - // } - - // private ExecutionGraphVisualizer addFromRead(ExecutionModel model) { - - // graphviz.beginSubgraph("FromRead"); - // graphviz.setEdgeAttributes("color=orange"); - // for (Map.Entry rw : model.getReadWriteMap().entrySet()) { - // EventData r = rw.getKey(); - // EventData w = rw.getValue(); - - // if (ignore(r) || ignore(w)) { - // continue; - // } - - // List co = model.getCoherenceMap().get(w.getAccessedAddress()); - // // Check if exists w2 : co(w, w2) - // if (co.indexOf(w) + 1 < co.size()) { - // EventData w2 = co.get(co.indexOf(w) + 1); - // if (!ignore(w2) && frFilter.test(r, w2)) { - // appendEdge(r, w2, "label=fr"); - // } - // } - // } - // graphviz.end(); - // return this; - // } - - // private ExecutionGraphVisualizer addCoherence(ExecutionModel model) { - - // graphviz.beginSubgraph("Coherence"); - // graphviz.setEdgeAttributes("color=red"); - - // for (List co : model.getCoherenceMap().values()) { - // for (int i = 2; i < co.size(); i++) { - // // We skip the init writes - // EventData w1 = co.get(i - 1); - // EventData w2 = co.get(i); - // if (ignore(w1) || ignore(w2) || !coFilter.test(w1, w2)) { - // continue; - // } - // appendEdge(w1, w2, "label=co"); - // } - // } - // graphviz.end(); - // return this; - // } - private ExecutionGraphVisualizer addAllThreadPos(ExecutionModelNext model) { for (Thread thread : model.getThreads()) { addThreadPo(thread, model); @@ -259,18 +193,7 @@ private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModelNext m // --- Subgraph start --- graphviz.beginSubgraph("T" + thread.getId()); - // graphviz.setEdgeAttributes("weight=100"); - // // --- Node list --- - // for (int i = 1; i < threadEvents.size(); i++) { - // EventData e1 = threadEvents.get(i - 1); - // EventData e2 = threadEvents.get(i); - - // if (ignore(e1) || ignore(e2)) { - // continue; - // } - - // appendEdge(e1, e2, (String[]) null); - // } + for (EventModel e : threadEvents) { appendNode(e, (String[]) null); } @@ -303,7 +226,7 @@ private String eventToNode(EventModel e) { return String.format("\"I(%s, %d)\"", getAddressString( ((StoreModel) e).getAccessedAddress()), ((StoreModel) e).getValue()); } - // We have MemEvent + Fence + // We have MemEvent + Fence + Local + Assert String tag = e.getEvent().toString(); if (e.isMemoryEvent()) { String address = getAddressString(((MemoryEventModel) e).getAccessedAddress()); @@ -369,8 +292,8 @@ public static File generateGraphvizFile(ExecutionModelNext model, int iterationC public static void generateGraphvizFile(ExecutionModelNext model, int iterationCount, BiPredicate rfFilter, BiPredicate frFilter, BiPredicate coFilter, String directoryName, String fileNameBase, - SyntacticContextAnalysis synContext) { + SyntacticContextAnalysis synContext, boolean usedByRefinementSolver) { generateGraphvizFile(model, iterationCount, rfFilter, frFilter, coFilter, directoryName, fileNameBase, - synContext, true, true); + synContext, true, usedByRefinementSolver); } }