diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 780e2cfe73..abc287ab3c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/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('.'); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index db9a0a0a52..d6ada384ed 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/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"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/WMMSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/WMMSolver.java index 41441880e5..342495d024 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/WMMSolver.java +++ b/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 ============== diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventData.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventData.java index 368900784f..a1572a2f9f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventData.java +++ b/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); 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 614aaf999f..c3cb84f55a 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 @@ -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,6 +48,7 @@ public class ExecutionModel { private static final Logger logger = LogManager.getLogger(ExecutionModel.class); private final EncodingContext encodingContext; + private EncodingContext encodingContextForWitness; // ============= Model specific ============= private Model model; @@ -51,6 +56,10 @@ public class ExecutionModel { private boolean extractCoherences; private final EventMap eventMap; + private ExecutionModelManager manager; + private final Map relations; + private final Map definedRelations; + private final Map edges; // The event list is sorted lexicographically by (threadID, cID) private final ArrayList eventList; private final ArrayList 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 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 getMemoryLayoutMap() { return memoryLayoutMapView; } public Map> 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); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java new file mode 100644 index 0000000000..de29da8c30 --- /dev/null +++ b/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 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 relNames) { + rmManager.extractRelations(relNames); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModel.java new file mode 100644 index 0000000000..3951921691 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModel.java @@ -0,0 +1,108 @@ +package com.dat3m.dartagnan.verification.model.relation; + +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.verification.model.EventData; + +import java.util.Set; +import java.util.HashSet; + + +public class RelationModel { + private String name; + private final Relation relation; + private final Set edges = new HashSet<>(); + private final Set edgesToShow = new HashSet<>(); + + RelationModel(Relation r) { + relation = r; + } + + public Relation getRelation() { + return relation; + } + + public String getName() { + return name; + } + + public void setName(String name) { + this.name = name; + } + + public boolean isDefined() { + return name != null; + } + + public boolean containsEdge(EdgeModel edge) { + return edges.contains(edge); + } + + public void removeEdgeToShow(EdgeModel edge) { + edgesToShow.remove(edge); + } + + public Set getEdges() { + return Set.copyOf(edges); + } + + public Set getEdgesToShow() { + return Set.copyOf(edgesToShow); + } + + public void addEdge(EdgeModel edge) { + edges.add(edge); + edgesToShow.add(edge); + } + + public void addEdges(Set edgeModels) { + edges.addAll(edgeModels); + edgesToShow.addAll(edgeModels); + } + + public EdgeModel newEdge(EventData p, EventData s) { + EdgeModel edge = new EdgeModel(p, s); + addEdge(edge); + return edge; + } + + + public static class EdgeModel { + private final EventData predecessor; + private final EventData successor; + private final String identifier; + + EdgeModel(EventData p, EventData s) { + predecessor = p; + successor = s; + identifier = p.getId() + " -> " + s.getId(); + } + + public EventData getPredecessor() { + return predecessor; + } + + public EventData getSuccessor() { + return successor; + } + + public String getIdentifier() { + return identifier; + } + + @Override + public String toString() { return identifier; } + + @Override + public boolean equals(Object other) { + if (this == other) { + return true; + } + return identifier.equals(((EdgeModel) other).getIdentifier()); + } + + @Override + public int hashCode() { + return predecessor.getId() * 31 + successor.getId() * 23; + } + } +} 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 new file mode 100644 index 0000000000..6406f9d10c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModelManager.java @@ -0,0 +1,577 @@ +package com.dat3m.dartagnan.verification.model.relation; + +import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.verification.model.ExecutionModel; +import com.dat3m.dartagnan.verification.model.EventData; +import com.dat3m.dartagnan.verification.model.relation.RelationModel.EdgeModel; +import com.dat3m.dartagnan.wmm.Constraint.Visitor; +import com.dat3m.dartagnan.wmm.definition.*; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.utils.dependable.DependencyGraph; + +import com.google.common.collect.Sets; +import com.google.common.collect.Lists; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.apache.logging.log4j.Logger; +import org.apache.logging.log4j.LogManager; + +import java.math.BigInteger; +import java.util.*; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; +import static com.google.common.base.Preconditions.checkNotNull; + +public class RelationModelManager { + + private static final Logger logger = LogManager.getLogger(RelationModelManager.class); + + private final ExecutionModel executionModel; + private final RelationModelBuilder builder; + + private RelationModelManager(ExecutionModel m) { + executionModel = m; + builder = new RelationModelBuilder(); + } + + public static RelationModelManager newRMManager(ExecutionModel m) { + return new RelationModelManager(m); + } + + public void extractRelations(List relationNames) { + for (String name : relationNames) { + Relation r = executionModel.getMemoryModelForWitness().getRelation(name); + if (r == null) { + logger.warn("Relation with the name {} does not exist", name); + continue; + } + extractRelation(r, Optional.of(name)); + } + } + + private void extractRelation(Relation r, Optional name) { + if (executionModel.containsRelation(r)) { return; } + RelationModel rm; + // TODO: Treat DATA, ADDR, CTRL as derived. + if (name.isPresent() && name.get().equals(DATA)) { + rm = builder.buildDataDependency(r); + } else if (name.isPresent() && name.get().equals(ADDR)) { + rm = builder.buildAddressDependency(r); + } else if (name.isPresent() && name.get().equals(CTRL)) { + rm = builder.buildControlDependency(r); + } else { + List deps = r.getDependencies(); + for (Relation dep : deps) { + extractRelation(dep, dep.getName()); + } + rm = r.getDefinition().accept(builder); + if (name.isPresent()) { + rm.setName(name.get()); + } + } + executionModel.addRelation(r, rm); + } + + private RelationModel newModel(Relation r) { + return new RelationModel(r); + } + + private RelationModel newModel(Relation r, String relationName) { + RelationModel m = newModel(r); + m.setName(relationName); + return m; + } + + private void addEdgeToRelation(RelationModel r, EventData p, EventData s) { + // We do this check because we want only PO edges to connect Local or Assert events. + if (!r.isDefined() || (r.isDefined() && !r.getName().equals(PO))) { + if (!p.hasTag(Tag.VISIBLE) || !s.hasTag(Tag.VISIBLE)) { return; } + } + String identifier = p.getId() + " -> " + s.getId(); + EdgeModel edge = executionModel.getEdge(identifier); + if (edge == null) { + executionModel.addEdge(r.newEdge(p, s)); + } + else { + r.addEdge(edge); + } + } + + private RelationModel computeInverse(Relation r, RelationModel rm) { + RelationModel result = newModel(r); + for (EdgeModel edge : rm.getEdges()) { + addEdgeToRelation(result, edge.getSuccessor(), edge.getPredecessor()); + } + return result; + } + + private RelationModel computeComposition(Relation r, RelationModel first, RelationModel second) { + RelationModel result = newModel(r); + for (EdgeModel f : first.getEdges()) { + for (EdgeModel s : second.getEdges()) { + if (f.getSuccessor() == s.getPredecessor()) { + addEdgeToRelation(result, f.getPredecessor(), s.getSuccessor()); + } + } + } + return result; + } + + private RelationModel computeDifference(Relation r, RelationModel minuend, RelationModel subtrahend) { + RelationModel result = newModel(r); + for (EdgeModel m : minuend.getEdges()) { + boolean found = false; + for (EdgeModel s : subtrahend.getEdges()) { + if (m == s) { + found = true; + break; + } + } + if (!found) { + result.addEdge(m); + } + } + return result; + } + + private RelationModel computeUnion(Relation r, List relations) { + RelationModel result = newModel(r); + for (RelationModel rm : relations) { + result.addEdges(rm.getEdges()); + } + return result; + } + + private RelationModel computeIntersection(Relation r, List relations) { + RelationModel result = newModel(r); + if (relations.size() == 1) { + result.addEdges(relations.get(0).getEdges()); + } else { + if (relations.size() == 2) { + Set edges = Sets.intersection(relations.get(0).getEdges(), relations.get(1).getEdges()); + if (relations.size() > 2) { + for (int i = 2; i < relations.size(); i++) { + edges = Sets.intersection(edges, relations.get(i).getEdges()); + } + } + result.addEdges(edges); + } + } + return result; + } + + private RelationModel computeTransitiveClosure(Relation r, RelationModel rm) { + RelationModel result = newModel(r); + final Map> reachMap = new HashMap<>(); + for (EdgeModel edge : rm.getEdges()) { + reachMap.computeIfAbsent(edge.getPredecessor(), k -> new HashSet<>()).add(edge.getSuccessor()); + } + for (EventData p : reachMap.keySet()) { + final Set reachables = new HashSet<>(); + depthFirstSearch(p, reachMap, reachables); + for (EventData s : reachables) { + if (p != s) { addEdgeToRelation(result, p, s); } + } + } + return result; + } + + private void depthFirstSearch(EventData p, Map> reachMap, Set visited) { + if (visited.contains(p)) { return; } + visited.add(p); + if (reachMap.containsKey(p)) { + for (EventData s : reachMap.get(p)) { + depthFirstSearch(s, reachMap, visited); + } + } + } + + private RelationModel removeSelfLoopToShow(RelationModel rm) { + for (EdgeModel e : rm.getEdges()) { + if (e.getPredecessor() == e.getSuccessor()) { + rm.removeEdgeToShow(e); + } + } + return rm; + } + + // We do NOT show transitive edges in base relations. + private RelationModel removeTransitiveEdgesToShow(RelationModel rm) { + rm = removeSelfLoopToShow(rm); + for (EdgeModel e1 : rm.getEdges()) { + for (EdgeModel e2 : rm.getEdges()) { + if (e1.getSuccessor() == e2.getPredecessor()) { + rm.removeEdgeToShow(new EdgeModel(e1.getPredecessor(), e2.getSuccessor())); + } + } + } + return rm; + } + + + private final class RelationModelBuilder implements Visitor { + public RelationModelBuilder() {} + + @Override + public RelationModel visitInverse(Inverse invs) { + Relation inversed = invs.getDefinedRelation(); + RelationModel toInverse = executionModel.getRelationModel(invs.getOperand()); + return computeInverse(inversed, toInverse); + } + + @Override + public RelationModel visitComposition(Composition comp) { + Relation compR = comp.getDefinedRelation(); + RelationModel left = executionModel.getRelationModel(comp.getLeftOperand()); + RelationModel right = executionModel.getRelationModel(comp.getRightOperand()); + return computeComposition(compR, left, right); + } + + @Override + public RelationModel visitDifference(Difference diff) { + Relation diffR = diff.getDefinedRelation(); + RelationModel minuend = executionModel.getRelationModel(diff.getMinuend()); + RelationModel subtrahend = executionModel.getRelationModel(diff.getSubtrahend()); + return computeDifference(diffR, minuend, subtrahend); + } + + @Override + public RelationModel visitUnion(Union u) { + Relation uR = u.getDefinedRelation(); + List operandModels = u.getOperands().stream().map(r -> executionModel.getRelationModel(r)).collect(Collectors.toList()); + return computeUnion(uR, operandModels); + } + + @Override + public RelationModel visitIntersection(Intersection intsc) { + Relation intscR = intsc.getDefinedRelation(); + List operandModels = intsc.getOperands().stream().map(r -> executionModel.getRelationModel(r)).collect(Collectors.toList()); + return computeIntersection(intscR, operandModels); + } + + @Override + public RelationModel visitTransitiveClosure(TransitiveClosure tscl) { + Relation tsclR = tscl.getDefinedRelation(); + RelationModel operand = executionModel.getRelationModel(tscl.getOperand()); + return computeTransitiveClosure(tsclR, operand); + } + + @Override + public RelationModel visitProgramOrder(ProgramOrder po) { + Relation r = po.getDefinedRelation(); + RelationModel rm = newModel(r, PO); + for (Thread t : executionModel.getThreads()) { + List events = executionModel.getThreadEventsMap().get(t).stream() + .filter(e -> e.hasTag(Tag.VISIBLE) + || e.isLocal() + || e.isAssert()) + .toList(); + if (events.size() <= 1) { continue; } + for (int i = 1; i < events.size(); i++) { + EventData e1 = events.get(i - 1); + EventData e2 = events.get(i); + addEdgeToRelation(rm, e1, e2); + } + // Add PO edge also between visible events. + List visibles = getVisibleEvents(t); + for (int i = 1; i < visibles.size(); i++) { + EventData e1 = visibles.get(i - 1); + EventData e2 = visibles.get(i); + addEdgeToRelation(rm, e1, e2); + } + } + return removeTransitiveEdgesToShow(rm); + } + + @Override + public RelationModel visitReadFrom(ReadFrom rf) { + Relation r = rf.getDefinedRelation(); + RelationModel rm = newModel(r, RF); + EncodingContext.EdgeEncoder rfEncoder = executionModel.getContextForWitness().edge(r); + for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { + BigInteger address = reads.getKey(); + for (EventData read : reads.getValue()) { + for (EventData write : executionModel.getAddressWritesMap().get(address)) { + BooleanFormula rfExpr = rfEncoder.encode(write.getEvent(), read.getEvent()); + if (isTrue(rfExpr)) { + addEdgeToRelation(rm, write, read); + break; + } + } + } + } + return removeTransitiveEdgesToShow(rm); + } + + @Override + public RelationModel visitCoherence(Coherence co) { + Relation r = co.getDefinedRelation(); + RelationModel rm = newModel(r, CO); + EncodingContext.EdgeEncoder coEncoder = executionModel.getContextForWitness().edge(r); + for (Map.Entry> writes : executionModel.getAddressWritesMap().entrySet()) { + BigInteger address = writes.getKey(); + Set writeEvents = writes.getValue(); + List sortedWrites; + if (executionModel.getContext().usesSATEncoding()) { + Map> edges = new HashMap<>(); + for (EventData w1 : writeEvents) { + edges.put(w1, new ArrayList<>()); + for (EventData w2 : writeEvents) { + if (isTrue(coEncoder.encode(w1.getEvent(), w2.getEvent()))) { + edges.get(w1).add(w2); + } + } + } + DependencyGraph depGraph = DependencyGraph.from(writeEvents, edges); + sortedWrites = new ArrayList<>(Lists.reverse(depGraph.getNodeContents())); + } else { + Map writeClockMap = new HashMap<>(writeEvents.size() * 4 / 3, 0.75f); + for (EventData w : writeEvents) { + writeClockMap.put(w, executionModel.getModel().evaluate(executionModel.getContext().memoryOrderClock(w.getEvent()))); + } + sortedWrites = writeEvents.stream().sorted(Comparator.comparing(writeClockMap::get)).collect(Collectors.toList()); + } + + int index = 0; + for (EventData w : sortedWrites) { + w.setCoherenceIndex(index++); + } + for (int i = 2; i < sortedWrites.size(); i ++) { + EventData w1 = sortedWrites.get(i - 1); + EventData w2 = sortedWrites.get(i); + addEdgeToRelation(rm, w1, w2); + } + } + return removeTransitiveEdgesToShow(rm); + } + + @Override + public RelationModel visitSameLocation(SameLocation loc) { + Relation r = loc.getDefinedRelation(); + RelationModel rm = newModel(r, LOC); + EncodingContext.EdgeEncoder locEncoder = executionModel.getContextForWitness().edge(r); + Map> memoryAccesses = Stream.concat(executionModel.getAddressReadsMap().entrySet().stream(), + executionModel.getAddressWritesMap().entrySet().stream()) + .collect(Collectors.toMap( + Map.Entry::getKey, + Map.Entry::getValue, + (set1, set2) -> { + Set merged = new HashSet<>(set1); + merged.addAll(set2); + return merged; + } + )); + for (Map.Entry> sameLocAccesses : memoryAccesses.entrySet()) { + BigInteger addr = sameLocAccesses.getKey(); + List asList = new ArrayList<>(sameLocAccesses.getValue()); + for (int i = 0; i < asList.size(); i++) { + for (int j = i + 1; j < asList.size(); j++) { + EventData e1 = asList.get(i); + EventData e2 = asList.get(j); + BooleanFormula locExpr1 = locEncoder.encode(e1.getEvent(), e2.getEvent()); + if (isTrue(locExpr1)) { + addEdgeToRelation(rm, e1, e2); + } + BooleanFormula locExpr2 = locEncoder.encode(e2.getEvent(), e1.getEvent()); + if (isTrue(locExpr2)) { + addEdgeToRelation(rm, e2, e1); + } + } + } + } + return rm; + } + + @Override + public RelationModel visitInternal(Internal in) { + Relation r = in.getDefinedRelation(); + RelationModel rm = newModel(r, INT); + EncodingContext.EdgeEncoder intEncoder = executionModel.getContextForWitness().edge(r); + for (Thread t : executionModel.getThreads()) { + List events = getVisibleEvents(t); + if (events.size() <= 1) { continue; } + for (int i = 0; i < events.size(); i++) { + for (int j = i + 1; j < events.size(); j++) { + EventData e1 = events.get(i); + EventData e2 = events.get(j); + BooleanFormula intExpr1 = intEncoder.encode(e1.getEvent(), e2.getEvent()); + if (isTrue(intExpr1)) { + addEdgeToRelation(rm, e1, e2); + } + BooleanFormula intExpr2 = intEncoder.encode(e2.getEvent(), e1.getEvent()); + if (isTrue(intExpr2)) { + addEdgeToRelation(rm, e2, e1); + } + } + } + } + return rm; + } + + @Override + public RelationModel visitExternal(External ext) { + Relation r = ext.getDefinedRelation(); + RelationModel rm = newModel(r, EXT); + EncodingContext.EdgeEncoder extEncoder = executionModel.getContextForWitness().edge(r); + List threads = executionModel.getThreads(); + for (int i = 0; i < threads.size(); i++) { + List eventList1 = getVisibleEvents(threads.get(i)); + if (eventList1.size() <= 1) { continue; } + for (int j = i + 1; j < threads.size(); j++) { + List eventList2 = getVisibleEvents(threads.get(j)); + if (eventList2.size() <= 1) { continue; } + for (EventData e1 : eventList1) { + for (EventData e2 : eventList2) { + BooleanFormula extExpr1 = extEncoder.encode(e1.getEvent(), e2.getEvent()); + if (isTrue(extExpr1)) { + addEdgeToRelation(rm, e1, e2); + } + BooleanFormula extExpr2 = extEncoder.encode(e2.getEvent(), e1.getEvent()); + if (isTrue(extExpr2)) { + addEdgeToRelation(rm, e2, e1); + } + } + } + } + } + return rm; + } + + @Override + public RelationModel visitReadModifyWrites(ReadModifyWrites rmw) { + Relation r = rmw.getDefinedRelation(); + RelationModel rm = newModel(r, RMW); + EncodingContext.EdgeEncoder rmwEncoder = executionModel.getContextForWitness().edge(r); + for (Map.Entry> addressReads : executionModel.getAddressReadsMap().entrySet()) { + BigInteger addr = addressReads.getKey(); + for (EventData read : addressReads.getValue()) { + for (EventData write : executionModel.getAddressWritesMap().get(addr)) { + if (read.getThread() == write.getThread() + && read.isRMW() && write.isRMW()) { + BooleanFormula rmwExpr = rmwEncoder.encode(read.getEvent(), write.getEvent()); + if (isTrue(rmwExpr)) { + addEdgeToRelation(rm, read, write); + } + } + } + } + } + return removeTransitiveEdgesToShow(rm); + } + + @Override + public RelationModel visitProduct(CartesianProduct prod) { + Relation r = prod.getDefinedRelation(); + RelationModel rm = newModel(r); + List eList1 = executionModel.getEventList().stream() + .filter(e -> prod.getFirstFilter().apply(e.getEvent())) + .toList(); + List eList2 = executionModel.getEventList().stream() + .filter(e -> prod.getSecondFilter().apply(e.getEvent())) + .toList(); + for (EventData p : eList1) { + for (EventData s : eList2) { + if (p != s) { + addEdgeToRelation(rm, p, s); + } + } + } + return rm; + } + + @Override + public RelationModel visitSetIdentity(SetIdentity set) { + Relation r = set.getDefinedRelation(); + RelationModel rm = newModel(r); + List eList = executionModel.getEventList().stream() + .filter(e -> set.getFilter().apply(e.getEvent())) + .toList(); + eList.stream().forEach(e -> addEdgeToRelation(rm, e, e)); + return rm; + } + + @Override + public RelationModel visitRangeIdentity(RangeIdentity range) { + Relation r = range.getDefinedRelation(); + RelationModel rm = newModel(r); + Set successors = new HashSet<>(); + executionModel.getRelationModel(range.getOperand()).getEdges() + .stream().forEach(e -> successors.add(e.getSuccessor())); + successors.stream().forEach(s -> addEdgeToRelation(rm, s, s)); + return rm; + } + + @Override + public RelationModel visitDomainIdentity(DomainIdentity domain) { + Relation r = domain.getDefinedRelation(); + RelationModel rm = newModel(r); + Set predecessors = new HashSet<>(); + executionModel.getRelationModel(domain.getOperand()).getEdges() + .stream().forEach(e -> predecessors.add(e.getPredecessor())); + predecessors.stream().forEach(p -> addEdgeToRelation(rm, p, p)); + return rm; + } + + @Override + public RelationModel visitFree(Free f) { + Relation r = f.getDefinedRelation(); + RelationModel rm = newModel(r); + for (Thread t : executionModel.getThreads()) { + List events = getVisibleEvents(t); + if (events.size() <= 1) { continue; } + for (EventData e1 : events) { + for (EventData e2 : events) { + addEdgeToRelation(rm, e1, e2); + } + } + } + return rm; + } + + public RelationModel buildDataDependency(Relation dataDep) { + RelationModel rm = newModel(dataDep, DATA); + for (Map.Entry> deps : executionModel.getDataDepMap().entrySet()) { + EventData e = deps.getKey(); + for (EventData dep : deps.getValue()) { + addEdgeToRelation(rm, e, dep); + } + } + return rm; + } + + public RelationModel buildAddressDependency(Relation addrDep) { + RelationModel rm = newModel(addrDep, ADDR); + for (Map.Entry> deps : executionModel.getAddrDepMap().entrySet()) { + EventData e = deps.getKey(); + for (EventData dep : deps.getValue()) { + addEdgeToRelation(rm, e, dep); + } + } + return rm; + } + + public RelationModel buildControlDependency(Relation ctrlDep) { + RelationModel rm = newModel(ctrlDep, CTRL); + for (Map.Entry> deps : executionModel.getCtrlDepMap().entrySet()) { + EventData e = deps.getKey(); + for (EventData dep : deps.getValue()) { + addEdgeToRelation(rm, e, dep); + } + } + return rm; + } + + private boolean isTrue(BooleanFormula formula) { + return Boolean.TRUE.equals(executionModel.getModel().evaluate(formula)); + } + + private List getVisibleEvents(Thread t) { + return executionModel.getThreadEventsMap().get(t).stream() + .filter(e -> e.hasTag(Tag.VISIBLE)) + .toList(); + } + } +} 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 ae0e11f9fe..976b29ebe4 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; + protected EncodingContext contextForWitness; private String flaggedPairsOutput = ""; public final Result getResult() { @@ -43,6 +44,12 @@ public final Result getResult() { public EncodingContext getEncodingContext() { return context; } + public EncodingContext getEncodingContextForWitness() { + return contextForWitness; + } + protected void setEncodingContextForWitness(EncodingContext c) { + contextForWitness = c; + } public final String getFlaggedPairsOutput() { return 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 d89a872336..691396515d 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 @@ -205,6 +205,10 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati Context baselineContext = Context.createCopyFrom(analysisContext); performStaticWmmAnalyses(task, analysisContext, config); + // Encoding for witness generation only + EncodingContext contextForWitness = EncodingContext.of(task, analysisContext, ctx.getFormulaManager()); + setEncodingContextForWitness(contextForWitness); + // ------- Generate refinement model ------- final RefinementModel refinementModel = generateRefinementModel(memoryModel); final Wmm baselineModel = refinementModel.getBaseModel(); @@ -230,7 +234,7 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati final WmmEncoder baselineEncoder = WmmEncoder.withContext(context); final BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); - final WMMSolver solver = WMMSolver.withContext(refinementModel, context, analysisContext, config); + final WMMSolver solver = WMMSolver.withContext(refinementModel, context, contextForWitness, config); final Refiner refiner = new Refiner(refinementModel); final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java new file mode 100644 index 0000000000..49db3f50c1 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java @@ -0,0 +1,67 @@ +package com.dat3m.dartagnan.witness.graphviz; + +import java.awt.Color; +import java.util.Set; +import java.util.HashSet; +import java.util.Map; +import java.util.HashMap; + +import static com.dat3m.dartagnan.wmm.RelationNameRepository.PO; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; + + +class ColorMap { + private final Map fixedColorMap = new HashMap<>(); + private final Set usedColors = new HashSet<>(); + private int currentHue = 0; + private int step = 72; + private float saturation = 1.0f; + private float brightness = 1.0f; + + ColorMap() { + // Black for PO + fixedColorMap.put(PO, colorToHex(Color.getHSBColor(0.0f, 0.0f, 0.0f))); + // Green for RF + fixedColorMap.put(RF, colorToHex(Color.getHSBColor(0.33f, 1.0f, 1.0f))); + // Red for CO + fixedColorMap.put(CO, colorToHex(Color.getHSBColor(0.0f, 1.0f, 1.0f))); + // Orange for FR + fixedColorMap.put("fr", colorToHex(Color.getHSBColor(0.08f, 1.0f, 1.0f))); + + usedColors.addAll(fixedColorMap.values()); + } + + String getColor(String relName) { + if (fixedColorMap.containsKey(relName)) { + return fixedColorMap.get(relName); + } + return generateColor(); + } + + private String generateColor() { + updateHue(); + float hue = currentHue / 360.0f; + String c = colorToHex(Color.getHSBColor(hue, saturation, brightness)); + if (usedColors.contains(c)) { + c = generateColor(); + } + usedColors.add(c); + return c; + } + + private String colorToHex(Color c) { + return String.format("\"#%02x%02x%02x\"", c.getRed(), c.getGreen(), c.getBlue()); + } + + private void updateHue() { + currentHue += step; + if (currentHue >= 360) { + currentHue -= 360; + step /= 2; + if (currentHue == 0) { + updateHue(); + } + } + } +} \ 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 038e7310ea..893c9e23c2 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 @@ -7,6 +7,10 @@ import com.dat3m.dartagnan.verification.model.EventData; import com.dat3m.dartagnan.verification.model.ExecutionModel; import com.dat3m.dartagnan.verification.model.MemoryObjectModel; +import com.dat3m.dartagnan.verification.model.relation.RelationModel; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import com.google.common.collect.Lists; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -16,32 +20,40 @@ import java.io.IOException; import java.io.Writer; import java.math.BigInteger; -import java.util.ArrayList; -import java.util.Comparator; -import java.util.List; -import java.util.Map; +import java.util.*; import java.util.function.BiPredicate; import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; +import static com.dat3m.dartagnan.configuration.OptionNames.WITNESS_RELATIONS_TO_SHOW; /* This is some rudimentary class to create graphs of executions. Currently, it just creates very special graphs. */ +@Options public class ExecutionGraphVisualizer { private static final Logger logger = LogManager.getLogger(ExecutionGraphVisualizer.class); private final Graphviz graphviz; + private final ColorMap colorMap; private SyntacticContextAnalysis synContext = getEmptyInstance(); // By default, we do not filter anything private BiPredicate rfFilter = (x, y) -> true; private BiPredicate frFilter = (x, y) -> true; private BiPredicate coFilter = (x, y) -> true; private final List sortedMemoryObjects = new ArrayList<>(); + private Set relToShow; + + @Option(name=WITNESS_RELATIONS_TO_SHOW, + description="Names of relations to show in the witness graph.", + secure=true) + private String relToShowStr = "default"; public ExecutionGraphVisualizer() { this.graphviz = new Graphviz(); + this.colorMap = new ColorMap(); } @@ -70,13 +82,27 @@ public void generateGraphOfExecutionModel(Writer writer, String graphName, Execu graphviz.beginDigraph(graphName); graphviz.append(String.format("label=\"%s\" \n", graphName)); addAllThreadPos(model); - addReadFrom(model); - addFromRead(model); - addCoherence(model); + addRelations(model); graphviz.end(); graphviz.generateOutput(writer); } + private ExecutionGraphVisualizer setRelationsToShow(ExecutionModel model) + throws InvalidConfigurationException { + model.getContext().getTask().getConfig().inject(this); + if (relToShowStr.equals("default")) { + relToShow = new HashSet<>(Set.of(PO, RF, CO)); + } + else { + relToShow = new HashSet<>(Arrays.asList(relToShowStr.split(",\\s*"))); + } + return this; + } + + private BiPredicate getFilter(String relationName) { + return (x, y) -> true; + } + private void computeAddressMap(ExecutionModel model) { model.getMemoryLayoutMap().entrySet().stream() .sorted(Comparator.comparing(entry -> entry.getValue().address())) @@ -87,64 +113,37 @@ private boolean ignore(EventData e) { return false; // We ignore no events for now. } - 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"); + private ExecutionGraphVisualizer addRelations(ExecutionModel model) { + model.getManager().extractRelations(new ArrayList<>(relToShow)); + for (String relationName : relToShow) { + addRelation(model, relationName); } - 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)) { + private ExecutionGraphVisualizer addRelation(ExecutionModel model, String relationName) { + RelationModel rm = model.getRelationModel(relationName); + if (rm == null) { + logger.warn("Relation with the name {} does not exist", relationName); + return this; + } + graphviz.beginSubgraph(relationName); + String attributes = String.format("color=%s", colorMap.getColor(relationName)); + if (relationName.equals(PO)) { + attributes += ", weight=100"; + } + graphviz.setEdgeAttributes(attributes); + String label = String.format("label=\"%s\"", relationName); + BiPredicate filter = getFilter(relationName); + for (RelationModel.EdgeModel edge : rm.getEdgesToShow()) { + EventData predecessor = edge.getPredecessor(); + EventData successor = edge.getSuccessor(); + + if (ignore(predecessor) || ignore(successor) || !filter.test(predecessor, successor)) { 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"); - } + appendEdge(predecessor, successor, label); } graphviz.end(); return this; @@ -159,7 +158,7 @@ private ExecutionGraphVisualizer addAllThreadPos(ExecutionModel model) { private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model) { List threadEvents = model.getThreadEventsMap().get(thread) - .stream().filter(e -> e.hasTag(Tag.VISIBLE)).toList(); + .stream().filter(e -> e.hasTag(Tag.VISIBLE) || e.isLocal() || e.isAssert()).toList(); if (threadEvents.size() <= 1) { // This skips init threads. return this; @@ -167,17 +166,9 @@ private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model // --- 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 (EventData e : threadEvents) { + appendNode(e, (String[]) null); } // --- Subgraph end --- @@ -236,6 +227,10 @@ private void appendEdge(EventData a, EventData b, String... options) { graphviz.addEdge(eventToNode(a), eventToNode(b), options); } + private void appendNode(EventData e, String... attributes) { + graphviz.addNode(eventToNode(e), attributes); + } + public static File generateGraphvizFile(ExecutionModel model, int iterationCount, BiPredicate rfFilter, BiPredicate frFilter, BiPredicate coFilter, String directoryName, String fileNameBase, @@ -246,6 +241,7 @@ public static File generateGraphvizFile(ExecutionModel model, int iterationCount try (FileWriter writer = new FileWriter(fileVio)) { // Create .dot file new ExecutionGraphVisualizer() + .setRelationsToShow(model) .setSyntacticContext(synContext) .setReadFromFilter(rfFilter) .setFromReadFilter(frFilter) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java index bb95e22eb4..5926ea7253 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/Graphviz.java @@ -61,7 +61,11 @@ public Graphviz appendLine(String text) { } public Graphviz addNode(String name, String... attributes) { - text.append(String.format("%s [%s]\n", name, String.join(", ", attributes))); + if (attributes == null) { + text.append(String.format("%s\n", name)); + } else { + text.append(String.format("%s [%s]\n", name, String.join(", ", attributes))); + } return this; }