diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index eaa18658a4..0eb11e8f48 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -20,9 +20,10 @@ import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.Utils; import com.dat3m.dartagnan.utils.options.BaseOptions; +import com.dat3m.dartagnan.verification.model.ExecutionModelManager; +import com.dat3m.dartagnan.verification.model.ExecutionModelNext; 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.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.DataRaceSolver; import com.dat3m.dartagnan.verification.solving.ModelChecker; @@ -230,8 +231,11 @@ 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 EncodingContext encodingContext = modelChecker instanceof RefinementSolver refinementSolver ? + refinementSolver.getContextWithFullWmm() : modelChecker.getEncodingContext(); + final ExecutionModelNext model = new ExecutionModelManager().buildExecutionModel( + encodingContext, prover.getModel() + ); final SyntacticContextAnalysis synContext = newInstance(task.getProgram()); final String progName = task.getProgram().getName(); final int fileSuffixIndex = progName.lastIndexOf('.'); @@ -239,11 +243,11 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir (fileSuffixIndex == - 1) ? progName : progName.substring(0, fileSuffixIndex); // RF edges give both ordering and data flow information, thus even when the pair is in PO // we get some data flow information by observing the edge - // FR edges only give ordering information which is known if the pair is also in PO // CO edges only give ordering information which is known if the pair is also in PO - return generateGraphvizFile(m, 1, (x, y) -> true, (x, y) -> !x.getThread().equals(y.getThread()), - (x, y) -> !x.getThread().equals(y.getThread()), getOrCreateOutputDirectory() + "/", name, - synContext, witnessType.convertToPng()); + return generateGraphvizFile(model, 1, (x, y) -> true, + (x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()), + getOrCreateOutputDirectory() + "/", name, + synContext, witnessType.convertToPng(), encodingContext.getTask().getConfig()); } private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, 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 3dde4d9401..4c5d64bf13 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -75,6 +75,7 @@ public class OptionNames { // Witness Options public static final String WITNESS_ORIGINAL_PROGRAM_PATH = "witness.originalProgramFilePath"; + public static final String WITNESS_SHOW = "witness.show"; // SVCOMP Options public static final String PROPERTYPATH = "svcomp.property"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java new file mode 100644 index 0000000000..40ee4beb56 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java @@ -0,0 +1,45 @@ +package com.dat3m.dartagnan.solver.caat4wmm; + +import com.dat3m.dartagnan.solver.caat.domain.Domain; +import com.dat3m.dartagnan.verification.model.event.EventModel; +import com.dat3m.dartagnan.verification.model.ExecutionModelNext; + +import java.util.Collection; +import java.util.List; + + +// TODO: this class is temporary and needs to be merged into EventDomain +// once there is one ExecutionModel for all use cases. +public class EventDomainNext implements Domain { + private final ExecutionModelNext executionModel; + private final List eventList; + + public EventDomainNext(ExecutionModelNext executionModel) { + this.executionModel = executionModel; + eventList = executionModel.getEventModels(); + } + + @Override + public int size() { + return eventList.size(); + } + + @Override + public Collection getElements() { + return eventList; + } + + @Override + public int getId(Object obj) { + if (obj instanceof EventModel em) { + return em.getId(); + } else { + throw new IllegalArgumentException(obj + " is not of type EventModel"); + } + } + + @Override + public EventModel getObjectById(int id) { + return eventList.get(id); + } +} \ No newline at end of file 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..50c0b61017 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 @@ -496,7 +496,7 @@ private void extractMemoryLayout() { for (MemoryObject obj : getProgram().getMemory().getObjects()) { final boolean isAllocated = obj.isStaticallyAllocated() || isTrue(encodingContext.execution(obj.getAllocationSite())); if (isAllocated) { - final BigInteger address = (BigInteger) model.evaluate(encodingContext.address(obj)); + final ValueModel address = new ValueModel(model.evaluate(encodingContext.address(obj))); final BigInteger size = (BigInteger) model.evaluate(encodingContext.size(obj)); memoryLayoutMap.put(obj, new MemoryObjectModel(obj, address, size)); } 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..c3a38569a1 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -0,0 +1,605 @@ +package com.dat3m.dartagnan.verification.model; + +import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.program.event.*; +import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.filter.Filter; +import com.dat3m.dartagnan.program.memory.MemoryObject; +import com.dat3m.dartagnan.program.Register; +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.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.caat4wmm.EventDomainNext; +import com.dat3m.dartagnan.utils.dependable.DependencyGraph; +import com.dat3m.dartagnan.verification.model.event.*; +import com.dat3m.dartagnan.verification.model.RelationModel.EdgeModel; +import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; +import com.dat3m.dartagnan.wmm.Constraint.Visitor; +import com.dat3m.dartagnan.wmm.definition.*; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.Wmm; +import com.google.common.collect.BiMap; +import com.google.common.collect.HashBiMap; +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.math.BigInteger; +import java.util.*; + +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; +import static com.google.common.base.Preconditions.checkNotNull; + + +public class ExecutionModelManager { + private final RelationGraphBuilder graphBuilder; + private final RelationGraphPopulator graphPopulator; + + private final Map relModelCache; + private final BiMap relGraphCache; + private final Map edgeModelCache; + + private ExecutionModelNext executionModel; + private EncodingContext context; + private Model model; + private Wmm wmm; + private EventDomainNext domain; + + public ExecutionModelManager(){ + graphBuilder = new RelationGraphBuilder(); + graphPopulator = new RelationGraphPopulator(); + relModelCache = new HashMap<>(); + relGraphCache = HashBiMap.create(); + edgeModelCache = new HashMap<>(); + } + + public ExecutionModelNext buildExecutionModel(EncodingContext context, Model model) { + executionModel = new ExecutionModelNext(); + + this.context = context; + this.model = model; + this.wmm = context.getTask().getMemoryModel(); + this.domain = new EventDomainNext(executionModel); + + extractEvents(); + extractMemoryLayout(); + + relModelCache.clear(); + relGraphCache.clear(); + edgeModelCache.clear(); + extractRelations(); + + this.context = null; + this.model = null; + this.wmm = null; + this.domain = null; + + return executionModel; + } + + private void extractEvents() { + int id = 0; + List threadList = new ArrayList<>(context.getTask().getProgram().getThreads()); + + for (Thread t : threadList) { + ThreadModel tm = new ThreadModel(t); + int eventNum = 0; + Event e = t.getEntry(); + + do { + if (!isTrue(context.execution(e))) { + e = e.getSuccessor(); + continue; + } + + if (toExtract(e)) { + extractEvent(e, tm, id++); + eventNum++; + } + + if (e instanceof CondJump jump + && isTrue(context.jumpCondition(jump))) { + e = jump.getLabel(); + } else { + e = e.getSuccessor(); + } + + } while (e != null); + + if (eventNum > 0) { executionModel.addThread(tm); } + } + } + + private void extractEvent(Event e, ThreadModel tm, int id) { + EventModel em; + if (e instanceof MemoryEvent memEvent) { + ValueModel address = new ValueModel(evaluateByModel(context.address(memEvent))); + ValueModel value = new ValueModel(evaluateByModel(context.value(memEvent))); + + if (memEvent instanceof Load load) { + em = new LoadModel(load, tm, id, address, value); + executionModel.addAddressRead(address, (LoadModel) em); + } else if (memEvent instanceof Store store) { + em = new StoreModel(store, tm, id, address, value); + executionModel.addAddressWrite(address, (StoreModel) em); + } else { + // Should never happen. + throw new IllegalArgumentException(String.format( + "Event %s is memory event but neither read nor write", memEvent + )); + } + + } else if (e instanceof GenericVisibleEvent visible) { + em = new GenericVisibleEventModel(visible, tm, id); + } else if (e instanceof Assert assrt) { + em = new AssertModel( + assrt, tm, id, isTrue(context.encodeExpressionAsBooleanAt(assrt.getExpression(), assrt)) + ); + } else if (e instanceof Local local) { + ValueModel value = new ValueModel(evaluateByModel(context.result(local))); + em = new LocalModel(local, tm, id, value); + } else if (e instanceof CondJump cj) { + em = new CondJumpModel(cj, tm, id); + } else { + // Should never happen. + throw new IllegalArgumentException(String.format("Event %s should not be extracted", e)); + } + + executionModel.addEvent(e, em); + } + + 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 e instanceof MemoryEvent + || e instanceof GenericVisibleEvent + || e instanceof Local + || e instanceof Assert + || e instanceof CondJump; + } + + private void extractMemoryLayout() { + for (MemoryObject obj : context.getTask().getProgram().getMemory().getObjects()) { + boolean isAllocated = obj.isStaticallyAllocated() + || isTrue(context.execution(obj.getAllocationSite())); + if (isAllocated) { + // Currently, addresses of memory objects are guaranteed to be integer and assigned. + ValueModel address = new ValueModel(evaluateByModel(context.address(obj))); + BigInteger size = (BigInteger) evaluateByModel(context.size(obj)); + executionModel.addMemoryObject(obj, new MemoryObjectModel(obj, address, size)); + } + } + } + + private void extractRelations() { + Set relsToExtract = new HashSet<>(wmm.getRelations()); + for (Relation r : relsToExtract) { createModel(r); } + + Set relGraphs = new HashSet<>(); + DependencyGraph dependencyGraph = DependencyGraph.from(relsToExtract); + + for (Set.Node> component : dependencyGraph.getSCCs()) { + for (DependencyGraph.Node node : component) { + Relation r = node.getContent(); + if (r.isRecursive()) { + RecursiveGraph recGraph = new RecursiveGraph(); + recGraph.setName(r.getNameOrTerm() + "_rec"); + relGraphs.add(recGraph); + relGraphCache.put(r, recGraph); + } + } + for (DependencyGraph.Node node : component) { + Relation r = node.getContent(); + RelationGraph rg = createGraph(r); + if (r.isRecursive()) { + RecursiveGraph recGraph = (RecursiveGraph) relGraphCache.get(r); + recGraph.setConcreteGraph(rg); + } else { + relGraphs.add(rg); + } + } + } + + Set predicates = new HashSet<>(relGraphs); + PredicateHierarchy hierarchy = new PredicateHierarchy(predicates); + hierarchy.initializeToDomain(domain); + + // Populate graphs of base relations. + for (CAATPredicate basePred : hierarchy.getBasePredicates()) { + Relation r = relGraphCache.inverse().get((RelationGraph) basePred); + try { + r.getDefinition().accept(graphPopulator); + } catch (UnsupportedOperationException e) { + // Populate graph of relations unsupported by the visitor using default relation analysis. + graphPopulator.populateDynamicDefaultGraph(r); + } + } + + // Do the computation. + hierarchy.populate(); + + for (CAATPredicate pred : hierarchy.getPredicateList()) { + Relation r = relGraphCache.inverse().get((RelationGraph) pred); + if (relModelCache.containsKey(r)) { + RelationModel rm = relModelCache.get(r); + ((RelationGraph) pred).edgeStream() + .forEach(e -> rm.addEdgeModel(getOrCreateEdgeModel(e))); + } + } + + for (Relation r : relsToExtract) { + executionModel.addRelation(r, relModelCache.get(r)); + } + } + + private void createModel(Relation r) { + if (relModelCache.containsKey(r)) { return; } + relModelCache.put(r, new RelationModel(r)); + } + + private RelationGraph createGraph(Relation r) { + RelationGraph rg = r.getDependencies().size() == 0 ? new SimpleGraph() : r.getDefinition().accept(graphBuilder); + rg.setName(r.getNameOrTerm()); + if (!r.isRecursive()) { + relGraphCache.put(r, rg); + } + return rg; + } + + private RelationGraph getOrCreateGraph(Relation r) { + if (relGraphCache.containsKey(r)) { + return relGraphCache.get(r); + } + return createGraph(r); + } + + private EdgeModel getOrCreateEdgeModel(Edge e) { + if (edgeModelCache.containsKey(e)) { + return edgeModelCache.get(e); + } + EdgeModel em = new EdgeModel(executionModel.getEventModelById(e.getFirst()), + executionModel.getEventModelById(e.getSecond())); + edgeModelCache.put(e, em); + return em; + } + + private boolean isTrue(BooleanFormula formula) { + return Boolean.TRUE.equals(model.evaluate(formula)); + } + + private Object evaluateByModel(Formula formula) { + return model.evaluate(formula); + } + + + // Usage: Populate graph of the base relations with instances of the Edge class + // based on the information from ExecutionModelNext. + private final class RelationGraphPopulator implements Visitor { + + @Override + public Void visitProgramOrder(ProgramOrder po) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(po.getDefinedRelation()); + for (ThreadModel tm : executionModel.getThreadModels()) { + List eventList = tm.getVisibleEventModels(); + if (eventList.size() <= 1) { continue; } + for (int i = 1; i < eventList.size(); i++) { + EventModel e1 = eventList.get(i); + for (int j = i + 1; j < eventList.size(); j++) { + EventModel e2 = eventList.get(j); + rg.add(new Edge(e1.getId(), e2.getId())); + } + } + } + return null; + } + + @Override + public Void visitReadFrom(ReadFrom readFrom) { + Relation relation = readFrom.getDefinedRelation(); + SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation); + EncodingContext.EdgeEncoder rf = context.edge(relation); + + for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { + ValueModel address = reads.getKey(); + if (!executionModel.getAddressWritesMap().containsKey(address)) { continue; } + for (LoadModel read : reads.getValue()) { + for (StoreModel write : executionModel.getAddressWritesMap().get(address)) { + if (isTrue(rf.encode(write.getEvent(), read.getEvent()))) { + rg.add(new Edge(write.getId(), read.getId())); + } + } + } + } + return null; + } + + @Override + public Void visitCoherence(Coherence coherence) { + Relation relation = coherence.getDefinedRelation(); + SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation); + EncodingContext.EdgeEncoder co = context.edge(relation); + + for (Set writes : executionModel.getAddressWritesMap().values()) { + for (StoreModel w1 : writes) { + for (StoreModel w2 : writes) { + if (isTrue(co.encode(w1.getEvent(), w2.getEvent()))) { + rg.add(new Edge(w1.getId(), w2.getId())); + } + } + } + } + return null; + } + + @Override + public Void visitReadModifyWrites(ReadModifyWrites rmw) { + Relation relation = rmw.getDefinedRelation(); + SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation); + EncodingContext.EdgeEncoder edge = context.edge(relation); + + for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { + ValueModel address = reads.getKey(); + if (!executionModel.getAddressWritesMap().containsKey(address)) { continue; } + for (LoadModel read : reads.getValue()) { + for (StoreModel write : executionModel.getAddressWritesMap().get(address)) { + if (isTrue(edge.encode(read.getEvent(), write.getEvent()))) { + rg.add(new Edge(read.getId(), write.getId())); + } + } + } + } + return null; + } + + @Override + public Void visitSameLocation(SameLocation loc) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(loc.getDefinedRelation()); + final Map> addressAccesses = new HashMap<>(); + + for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { + ValueModel address = reads.getKey(); + addressAccesses.putIfAbsent(address, new HashSet<>()); + for (LoadModel read : reads.getValue()) { + addressAccesses.get(address).add(read); + } + } + + for (Map.Entry> writes : executionModel.getAddressWritesMap().entrySet()) { + ValueModel address = writes.getKey(); + addressAccesses.putIfAbsent(address, new HashSet<>()); + for (StoreModel write : writes.getValue()) { + addressAccesses.get(address).add(write); + } + } + + for (Set sameLocAccesses : addressAccesses.values()) { + for (MemoryEventModel e1 : sameLocAccesses) { + for (MemoryEventModel e2 : sameLocAccesses) { + rg.add(new Edge(e1.getId(), e2.getId())); + } + } + } + return null; + } + + @Override + public Void visitInternal(Internal in) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(in.getDefinedRelation()); + for (ThreadModel tm : executionModel.getThreadModels()) { + List eventList = tm.getVisibleEventModels(); + for (EventModel e1 : eventList) { + for (EventModel e2 : eventList) { + rg.add(new Edge(e1.getId(), e2.getId())); + } + } + } + return null; + } + + @Override + public Void visitExternal(External ext) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(ext.getDefinedRelation()); + List threadList = executionModel.getThreadModels(); + for (int i = 0; i < threadList.size(); i ++) { + for (int j = i + 1; j < threadList.size(); j ++) { + for (EventModel e1 : threadList.get(i).getVisibleEventModels()) { + for (EventModel e2 : threadList.get(j).getVisibleEventModels()) { + rg.add(new Edge(e1.getId(), e2.getId())); + rg.add(new Edge(e2.getId(), e1.getId())); + } + } + } + } + return null; + } + + @Override + public Void visitSetIdentity(SetIdentity si) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(si.getDefinedRelation()); + executionModel.getEventModelsByFilter(si.getFilter()) + .stream().forEach(e -> rg.add(new Edge(e.getId(), e.getId()))); + return null; + } + + @Override + public Void visitProduct(CartesianProduct cp) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(cp.getDefinedRelation()); + List first = executionModel.getEventModelsByFilter(cp.getFirstFilter()); + List second = executionModel.getEventModelsByFilter(cp.getSecondFilter()); + for (EventModel e1 : first) { + for (EventModel e2 : second) { + rg.add(new Edge(e1.getId(), e2.getId())); + } + } + return null; + } + + @Override + public Void visitControlDependency(DirectControlDependency ctrlDirect) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(ctrlDirect.getDefinedRelation()); + for (ThreadModel tm : executionModel.getThreadModels()) { + for (EventModel em : tm.getEventModels()) { + if (em instanceof CondJumpModel cjm) { + for (EventModel dep : cjm.getDependentEvents(executionModel)) { + rg.add(new Edge(cjm.getId(), dep.getId())); + } + } + } + } + return null; + } + + @Override + public Void visitAddressDependency(DirectAddressDependency addrDirect) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(addrDirect.getDefinedRelation()); + for (ThreadModel tm : executionModel.getThreadModels()) { + Set writes = new HashSet<>(); + for (EventModel em : tm.getEventModels()) { + if (em instanceof RegWriterModel rwm) { + writes.add(rwm); + continue; + } + if (em instanceof RegReaderModel rrm) { + for (RegWriterModel write : writes) { + for (Register.Read read : rrm.getRegisterReads()) { + if (read.register() == write.getResultRegister() + && read.usageType() == Register.UsageType.ADDR) { + rg.add(new Edge(write.getId(), rrm.getId())); + } + } + } + } + } + } + return null; + } + + @Override + public Void visitInternalDataDependency(DirectDataDependency idd) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(idd.getDefinedRelation()); + for (ThreadModel tm : executionModel.getThreadModels()) { + Set writes = new HashSet<>(); + for (EventModel em : tm.getEventModels()) { + if (em instanceof RegWriterModel rwm) { + writes.add(rwm); + continue; + } + if (em instanceof RegReaderModel rrm) { + for (RegWriterModel write : writes) { + for (Register.Read read : rrm.getRegisterReads()) { + if (read.register() == write.getResultRegister() + && read.usageType() == Register.UsageType.DATA) { + rg.add(new Edge(write.getId(), rrm.getId())); + } + } + } + } + } + } + return null; + } + + @Override + public Void visitEmpty(Empty empty) { + return null; + } + + public void populateDynamicDefaultGraph(Relation r) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(r); + EncodingContext.EdgeEncoder edge = context.edge(r); + RelationAnalysis.Knowledge k = context.getAnalysisContext() + .get(RelationAnalysis.class) + .getKnowledge(r); + + if (k.getMaySet().size() < domain.size() * domain.size()) { + k.getMaySet().apply((e1, e2) -> { + EventModel em1 = executionModel.getEventModelByEvent(e1); + EventModel em2 = executionModel.getEventModelByEvent(e2); + if (em1 != null && em2 != null) { + if (isTrue(edge.encode(e1, e2))) { + rg.add(new Edge(em1.getId(), em2.getId())); + } + } + }); + } else { + for (EventModel em1 : executionModel.getEventModels()) { + for (EventModel em2 : executionModel.getEventModels()) { + if (isTrue(edge.encode(em1.getEvent(), em2.getEvent()))) { + rg.add(new Edge(em1.getId(), em2.getId())); + } + } + } + } + } + + } + + + // Create a the specific graph for derived relations, so that edges of them + // can be computed automatically by PredicateHierarchy. + private final class RelationGraphBuilder implements Visitor { + + @Override + public RelationGraph visitInverse(Inverse inv) { + return new InverseGraph(getOrCreateGraph(inv.getOperand())); + } + + @Override + public RelationGraph visitComposition(Composition comp) { + return new CompositionGraph(getOrCreateGraph(comp.getLeftOperand()), + getOrCreateGraph(comp.getRightOperand())); + } + + @Override + public RelationGraph visitDifference(Difference diff) { + return new DifferenceGraph(getOrCreateGraph(diff.getMinuend()), + getOrCreateGraph(diff.getSubtrahend())); + } + + @Override + public RelationGraph visitUnion(Union un) { + List ops = un.getOperands(); + RelationGraph[] rgs = new RelationGraph[ops.size()]; + for (int i = 0; i < rgs.length; i++) { + rgs[i] = getOrCreateGraph(ops.get(i)); + } + return new UnionGraph(rgs); + } + + @Override + public RelationGraph visitIntersection(Intersection inter) { + List ops = inter.getOperands(); + RelationGraph[] rgs = new RelationGraph[ops.size()]; + for (int i = 0; i < rgs.length; i++) { + rgs[i] = getOrCreateGraph(ops.get(i)); + } + return new IntersectionGraph(rgs); + } + + @Override + public RelationGraph visitTransitiveClosure(TransitiveClosure trans) { + return new TransitiveGraph(getOrCreateGraph(trans.getOperand())); + } + + @Override + public RelationGraph visitRangeIdentity(RangeIdentity ri) { + return new ProjectionIdentityGraph( + getOrCreateGraph(ri.getOperand()), + ProjectionIdentityGraph.Dimension.RANGE + ); + } + + @Override + public RelationGraph visitDomainIdentity(DomainIdentity di) { + return new ProjectionIdentityGraph( + getOrCreateGraph(di.getOperand()), + ProjectionIdentityGraph.Dimension.DOMAIN + ); + } + + } +} 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 new file mode 100644 index 0000000000..3bb6fceaa4 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java @@ -0,0 +1,104 @@ +package com.dat3m.dartagnan.verification.model; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.filter.Filter; +import com.dat3m.dartagnan.program.memory.MemoryObject; +import com.dat3m.dartagnan.verification.model.event.*; +import com.dat3m.dartagnan.verification.model.RelationModel; +import com.dat3m.dartagnan.wmm.Relation; + +import java.util.*; + + +// 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 is used only by ExecutionGraphVisualizer so far. +public class ExecutionModelNext { + private final List threadList; + private final List eventList; + private final Map eventMap; + private final Map relationMap; + private final Map memoryLayoutMap; + + private final Map> addressReadsMap; + private final Map> addressWritesMap; + + ExecutionModelNext() { + threadList = new ArrayList<>(); + eventList = new ArrayList<>(); + eventMap = new HashMap<>(); + relationMap = new HashMap<>(); + memoryLayoutMap= new HashMap<>(); + + addressReadsMap = new HashMap<>(); + addressWritesMap = new HashMap<>(); + } + + public void addThread(ThreadModel tModel) { + threadList.add(tModel); + } + + public void addEvent(Event e, EventModel eModel) { + eventList.add(eModel); + eventMap.put(e, eModel); + } + + public void addRelation(Relation r, RelationModel rModel) { + relationMap.put(r, rModel); + } + + public void addMemoryObject(MemoryObject m, MemoryObjectModel mModel) { + memoryLayoutMap.put(m, mModel); + } + + public void addAddressRead(ValueModel address, LoadModel read) { + addressReadsMap.computeIfAbsent(address, k -> new HashSet<>()).add(read); + } + + public void addAddressWrite(ValueModel address, StoreModel write) { + addressWritesMap.computeIfAbsent(address, k -> new HashSet<>()).add(write); + } + + public List getThreadModels() { + return Collections.unmodifiableList(threadList); + } + + public List getEventModels() { + return Collections.unmodifiableList(eventList); + } + + public List getVisibleEventModels() { + return eventList.stream() + .filter(e -> e instanceof MemoryEventModel || e instanceof GenericVisibleEventModel) + .toList(); + } + + public List getEventModelsByFilter(Filter filter) { + return eventList.stream().filter(e -> filter.apply(e.getEvent())).toList(); + } + + public EventModel getEventModelById(int id) { + return eventList.get(id); + } + + public EventModel getEventModelByEvent(Event event) { + return eventMap.get(event); + } + + public Set getRelationModels() { + return new HashSet<>(relationMap.values()); + } + + public Map getMemoryLayoutMap() { + return Collections.unmodifiableMap(memoryLayoutMap); + } + + public Map> getAddressReadsMap() { + return Collections.unmodifiableMap(addressReadsMap); + } + + public Map> getAddressWritesMap() { + return Collections.unmodifiableMap(addressWritesMap); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java index d5356d3d87..bad9a3cf69 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java @@ -4,5 +4,5 @@ import java.math.BigInteger; -public record MemoryObjectModel(MemoryObject object, BigInteger address, BigInteger size) { +public record MemoryObjectModel(MemoryObject object, ValueModel address, BigInteger size) { } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/RelationModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/RelationModel.java new file mode 100644 index 0000000000..2d58e2f207 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/RelationModel.java @@ -0,0 +1,68 @@ +package com.dat3m.dartagnan.verification.model; + +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.verification.model.event.EventModel; + +import java.util.Collections; +import java.util.Set; +import java.util.HashSet; + + +public class RelationModel { + private final Relation relation; + private final Set edgeModels; + + public RelationModel(Relation relation) { + this.relation = relation; + edgeModels = new HashSet<>(); + } + + public Relation getRelation() { + return relation; + } + + public Set getEdgeModels() { + return Collections.unmodifiableSet(edgeModels); + } + + public void addEdgeModel(EdgeModel edge) { + edgeModels.add(edge); + } + + + public static class EdgeModel { + private final EventModel from; + private final EventModel to; + + public EdgeModel(EventModel from, EventModel to) { + this.from = from; + this.to = to; + } + + public EventModel getFrom() { + return from; + } + + public EventModel getTo() { + return to; + } + + @Override + public String toString() { return from.getId() + " -> " + to.getId(); } + + @Override + public boolean equals(Object other) { + if (this == other) { + return true; + } + return from.getId() == ((EdgeModel) other).getFrom().getId() + && to.getId() == ((EdgeModel) other).getTo().getId(); + } + + @Override + public int hashCode() { + int a = from.getId(); + return a ^ (31 * to.getId() + 0x9e3779b9 + (a << 6) + (a >> 2)); + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java new file mode 100644 index 0000000000..e49a427bc8 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java @@ -0,0 +1,48 @@ +package com.dat3m.dartagnan.verification.model; + +import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.verification.model.event.EventModel; +import com.dat3m.dartagnan.verification.model.event.GenericVisibleEventModel; +import com.dat3m.dartagnan.verification.model.event.MemoryEventModel; + +import java.util.Collections; +import java.util.List; +import java.util.ArrayList; + + +public class ThreadModel { + private final Thread thread; + private final List eventList; + + public ThreadModel(Thread thread) { + this.thread = thread; + this.eventList = new ArrayList<>(); + } + + public void addEvent(EventModel event) { + eventList.add(event); + } + + public Thread getThread() { + return thread; + } + + public int getId() { + return thread.getId(); + } + + public String getName() { + return thread.getName(); + } + + public List getEventModels() { + return Collections.unmodifiableList(eventList); + } + + public List getVisibleEventModels() { + return eventList.stream() + .filter(e -> e instanceof MemoryEventModel || e instanceof GenericVisibleEventModel) + .toList(); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ValueModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ValueModel.java new file mode 100644 index 0000000000..efae322724 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ValueModel.java @@ -0,0 +1,50 @@ +package com.dat3m.dartagnan.verification.model; + +import java.math.BigInteger; + + +// This class currently only serves as a representation of values in ExecutionModelNext, +// in order to avoid the type conversion at value extraction. +public class ValueModel { + private final Object value; + + public ValueModel(Object literal) { + if (literal == null) { + value = null; + } else if (literal instanceof BigInteger || literal instanceof Boolean) { + value = literal; + } else { + throw new IllegalArgumentException("Unsupported value type: " + literal.getClass()); + } + } + + public Object getValue() { + return value; + } + + @Override + public boolean equals(Object other) { + if (this == other) { + return true; + } + + ValueModel vm = (ValueModel) other; + if (value == null) { + return vm.getValue() == null; + } + if (value.getClass() != vm.getValue().getClass()) { + return false; + } + return value.equals(vm.getValue()); + } + + @Override + public int hashCode() { + return value == null ? 0 : value.hashCode(); + } + + @Override + public String toString() { + return String.valueOf(value); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/AssertModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/AssertModel.java new file mode 100644 index 0000000000..7ca754aea0 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/AssertModel.java @@ -0,0 +1,18 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.core.Assert; +import com.dat3m.dartagnan.verification.model.ThreadModel; + + +public class AssertModel extends DefaultEventModel implements RegReaderModel { + private final boolean result; + + public AssertModel(Assert event, ThreadModel thread, int id, boolean result) { + super(event, thread, id); + this.result = result; + } + + public boolean getResult() { + return result; + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/CondJumpModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/CondJumpModel.java new file mode 100644 index 0000000000..cffd85a758 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/CondJumpModel.java @@ -0,0 +1,34 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.CondJump; +import com.dat3m.dartagnan.program.event.core.IfAsJump; +import com.dat3m.dartagnan.verification.model.ExecutionModelNext; +import com.dat3m.dartagnan.verification.model.ThreadModel; + +import java.util.List; + + +public class CondJumpModel extends DefaultEventModel implements RegReaderModel { + public CondJumpModel(CondJump event, ThreadModel thread, int id) { + super(event, thread, id); + } + + public List getDependentEvents(ExecutionModelNext executionModel) { + List dependents; + if (((CondJump) event).isGoto() || ((CondJump) event).isDead()) { + return List.of(); + } + + if (event instanceof IfAsJump jump) { + dependents = jump.getBranchesEvents(); + } else { + dependents = ((CondJump) event).getSuccessor().getSuccessors(); + } + + return dependents.stream() + .map(e -> executionModel.getEventModelByEvent(e)) + .filter(m -> m != null) + .toList(); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/DefaultEventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/DefaultEventModel.java new file mode 100644 index 0000000000..ffd8576c9d --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/DefaultEventModel.java @@ -0,0 +1,55 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.verification.model.ThreadModel; + + +public class DefaultEventModel implements EventModel { + protected final Event event; + protected final ThreadModel thread; + protected final int id; + + public DefaultEventModel(Event event, ThreadModel thread, int id) { + this.event = event; + this.thread = thread; + this.id = id; + + thread.addEvent(this); + } + + @Override + public Event getEvent() { + return event; + } + + @Override + public ThreadModel getThreadModel() { + return thread; + } + + @Override + public int getId() { + return id; + } + + @Override + public int hashCode() { + return id; + } + + @Override + public boolean equals(Object obj) { + // EventModel instances are unique per event. + return this == obj; + } + + @Override + public String toString() { + return String.format("T%d/E%d", thread.getId(), id); + } + + @Override + public int compareTo(EventModel e) { + return this.getId() - e.getId(); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModel.java new file mode 100644 index 0000000000..770f20be0d --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModel.java @@ -0,0 +1,13 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.verification.model.ThreadModel; + + +public interface EventModel extends Comparable { + Event getEvent(); + + ThreadModel getThreadModel(); + + int getId(); +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/GenericVisibleEventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/GenericVisibleEventModel.java new file mode 100644 index 0000000000..7746ecf5a2 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/GenericVisibleEventModel.java @@ -0,0 +1,11 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.core.GenericVisibleEvent; +import com.dat3m.dartagnan.verification.model.ThreadModel; + + +public class GenericVisibleEventModel extends DefaultEventModel { + public GenericVisibleEventModel(GenericVisibleEvent event, ThreadModel thread, int id) { + super(event, thread, id); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java new file mode 100644 index 0000000000..5efa9bb18c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java @@ -0,0 +1,12 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.verification.model.ThreadModel; +import com.dat3m.dartagnan.verification.model.ValueModel; + + +public class LoadModel extends MemoryEventModel implements RegWriterModel { + public LoadModel(Load load, ThreadModel thread, int id, ValueModel address, ValueModel value) { + super(load, thread, id, address, value); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LocalModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LocalModel.java new file mode 100644 index 0000000000..857fe4e837 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LocalModel.java @@ -0,0 +1,24 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.core.Local; +import com.dat3m.dartagnan.verification.model.ThreadModel; +import com.dat3m.dartagnan.verification.model.ValueModel; + + +public class LocalModel extends DefaultEventModel implements RegReaderModel, RegWriterModel { + private final ValueModel value; + + public LocalModel(Local event, ThreadModel thread, int id, ValueModel value) { + super(event, thread, id); + this.value = value; + } + + @Override + public Local getEvent() { + return (Local) event; + } + + public ValueModel getValue() { + return value; + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java new file mode 100644 index 0000000000..478fcc0696 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java @@ -0,0 +1,26 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.verification.model.ThreadModel; +import com.dat3m.dartagnan.verification.model.ValueModel; + + +public class MemoryEventModel extends DefaultEventModel implements RegReaderModel { + protected final ValueModel accessedAddress; + protected final ValueModel value; + + public MemoryEventModel( + MemoryEvent event, ThreadModel thread, int id, ValueModel address, ValueModel value) { + super(event, thread, id); + this.accessedAddress = address; + this.value = value; + } + + public ValueModel getAccessedAddress() { + return accessedAddress; + } + + public ValueModel getValue() { + return value; + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java new file mode 100644 index 0000000000..8daffd24fb --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java @@ -0,0 +1,13 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.Register.Read; + +import java.util.Set; + + +public interface RegReaderModel extends EventModel { + default Set getRegisterReads() { + return ((RegReader) this.getEvent()).getRegisterReads(); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegWriterModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegWriterModel.java new file mode 100644 index 0000000000..3b6ea9300f --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegWriterModel.java @@ -0,0 +1,11 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.program.Register; + + +public interface RegWriterModel extends EventModel { + default Register getResultRegister() { + return ((RegWriter) this.getEvent()).getResultRegister(); + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java new file mode 100644 index 0000000000..7c5dcf8d6d --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java @@ -0,0 +1,12 @@ +package com.dat3m.dartagnan.verification.model.event; + +import com.dat3m.dartagnan.program.event.core.Store; +import com.dat3m.dartagnan.verification.model.ThreadModel; +import com.dat3m.dartagnan.verification.model.ValueModel; + + +public class StoreModel extends MemoryEventModel { + public StoreModel(Store store, ThreadModel thread, int id, ValueModel address, ValueModel value) { + super(store, thread, id, address, value); + } +} \ No newline at end of file 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 b15c671c8f..c1686d1f84 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 @@ -29,6 +29,9 @@ import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.verification.model.EventData; import com.dat3m.dartagnan.verification.model.ExecutionModel; +import com.dat3m.dartagnan.verification.model.ExecutionModelManager; +import com.dat3m.dartagnan.verification.model.ExecutionModelNext; +import com.dat3m.dartagnan.verification.model.event.EventModel; import com.dat3m.dartagnan.wmm.Constraint; import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; @@ -86,6 +89,8 @@ public class RefinementSolver extends ModelChecker { private static final String FRE = "fre"; private static final String POLOC = "po-loc"; + private EncodingContext contextWithFullWmm; + // ================================================================================================================ // Configuration @@ -169,6 +174,10 @@ public RefinementTrace concat(RefinementTrace other) { private RefinementSolver() { } + public EncodingContext getContextWithFullWmm() { + return contextWithFullWmm; + } + //TODO: We do not yet use Witness information. The problem is that WitnessGraph.encode() generates // constraints on hb, which is not encoded in Refinement. //TODO (2): Add possibility for Refinement to handle CAT-properties (it ignores them for now). @@ -205,6 +214,9 @@ private void runInternal(SolverContext ctx, ProverWithTracker prover, Verificati Context baselineContext = Context.createCopyFrom(analysisContext); performStaticWmmAnalyses(task, analysisContext, config); + // Encoding context with the original Wmm and the analysis context for relation extraction. + contextWithFullWmm = EncodingContext.of(task, analysisContext, ctx.getFormulaManager()); + // ------- Generate refinement model ------- final RefinementModel refinementModel = generateRefinementModel(memoryModel); final Wmm baselineModel = refinementModel.getBaseModel(); @@ -388,7 +400,8 @@ private RefinementTrace runRefinement(VerificationTask task, ProverWithTracker p // ------------------------- Debugging/Logging ------------------------- if (generateGraphvizDebugFiles) { - generateGraphvizFiles(task, solver.getExecution(), trace.size(), iteration.inconsistencyReasons); + final ExecutionModelNext model = new ExecutionModelManager().buildExecutionModel(contextWithFullWmm, prover.getModel()); + generateGraphvizFiles(task, model, trace.size(), iteration.inconsistencyReasons); } if (logger.isDebugEnabled()) { // ---- Internal SMT stats after the first iteration ---- @@ -726,7 +739,7 @@ private void instrumentPolaritySeparation(Wmm wmm) { if (replacements.containsKey(b)) { bPrime = replacements.get(b); } else { - final String bPrimeName = b.getName().map(n -> n + "#POS").orElse("__POS" + counter++); + final String bPrimeName = b.getName().map(n -> n + "__POS").orElse("__POS" + counter++); bPrime = wmm.addDefinition(new Free(wmm.newRelation(bPrimeName))); replacements.put(b, bPrime); } @@ -862,16 +875,16 @@ private static CharSequence generateCoverageReport(Set coveredEvents, Pro // This code is pure debugging code that will generate graphical representations // of each refinement iteration. // Generate .dot files and .png files per iteration - private static void generateGraphvizFiles(VerificationTask task, ExecutionModel model, int iterationCount, - DNF reasons) { + private static void generateGraphvizFiles( + VerificationTask task, ExecutionModelNext model, int iterationCount, DNF reasons) { // =============== Visualization code ================== // The edgeFilter filters those co/rf that belong to some violation reason - BiPredicate edgeFilter = (e1, e2) -> { + BiPredicate edgeFilter = (e1, e2) -> { for (Conjunction cube : reasons.getCubes()) { for (CoreLiteral lit : cube.getLiterals()) { if (lit instanceof RelLiteral edgeLit) { - if (model.getData(edgeLit.getSource()).get() == e1 && - model.getData(edgeLit.getTarget()).get() == e2) { + if (model.getEventModelByEvent(edgeLit.getSource()) == e1 && + model.getEventModelByEvent(edgeLit.getTarget()) == e2) { return true; } } @@ -887,10 +900,10 @@ private static void generateGraphvizFiles(VerificationTask task, ExecutionModel String fileNameBase = String.format("%s-%d", programName, iterationCount); final SyntacticContextAnalysis emptySynContext = getEmptyInstance(); // File with reason edges only - generateGraphvizFile(model, iterationCount, edgeFilter, edgeFilter, edgeFilter, directoryName, fileNameBase, + generateGraphvizFile(model, iterationCount, edgeFilter, edgeFilter, directoryName, fileNameBase, emptySynContext); // File with all edges - generateGraphvizFile(model, iterationCount, (x, y) -> true, (x, y) -> true, (x, y) -> true, directoryName, + generateGraphvizFile(model, iterationCount, (x, y) -> true, (x, y) -> true, directoryName, fileNameBase + "-full", emptySynContext); } } \ No newline at end of file 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..4a42a24e6c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java @@ -0,0 +1,65 @@ +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))); + + 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..6a6edabec6 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 @@ -1,201 +1,282 @@ package com.dat3m.dartagnan.witness.graphviz; -import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; -import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.event.core.Init; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.verification.model.EventData; -import com.dat3m.dartagnan.verification.model.ExecutionModel; +import com.dat3m.dartagnan.utils.dependable.DependencyGraph; +import com.dat3m.dartagnan.verification.model.event.*; +import com.dat3m.dartagnan.verification.model.ExecutionModelNext; import com.dat3m.dartagnan.verification.model.MemoryObjectModel; +import com.dat3m.dartagnan.verification.model.RelationModel; +import com.dat3m.dartagnan.verification.model.RelationModel.EdgeModel; +import com.dat3m.dartagnan.verification.model.ThreadModel; +import com.dat3m.dartagnan.verification.model.ValueModel; +import com.dat3m.dartagnan.wmm.definition.Coherence; +import com.dat3m.dartagnan.wmm.definition.ProgramOrder; +import com.dat3m.dartagnan.wmm.definition.ReadFrom; +import com.dat3m.dartagnan.wmm.Relation; import com.google.common.collect.Lists; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; import java.io.File; import java.io.FileWriter; 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 java.util.stream.Collectors; +import static com.dat3m.dartagnan.configuration.OptionNames.WITNESS_SHOW; import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; -/* - 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 BiPredicate rfFilter = (x, y) -> true; + private BiPredicate coFilter = (x, y) -> true; private final List sortedMemoryObjects = new ArrayList<>(); + private List relsToShow; + + @Option(name=WITNESS_SHOW, + description="Names of relations to show in the witness graph.", + secure=true) + private String relsToShowStr = String.format("%s,%s,%s", PO, CO, RF); public ExecutionGraphVisualizer() { this.graphviz = new Graphviz(); + this.colorMap = new ColorMap(); } - public ExecutionGraphVisualizer setSyntacticContext(SyntacticContextAnalysis synContext) { this.synContext = synContext; return this; } - public ExecutionGraphVisualizer setReadFromFilter(BiPredicate filter) { + public ExecutionGraphVisualizer setReadFromFilter(BiPredicate filter) { this.rfFilter = filter; return this; } - public ExecutionGraphVisualizer setFromReadFilter(BiPredicate filter) { - this.frFilter = filter; - return this; - } - - public ExecutionGraphVisualizer setCoherenceFilter(BiPredicate filter) { + public ExecutionGraphVisualizer setCoherenceFilter(BiPredicate filter) { this.coFilter = filter; return this; } - public void generateGraphOfExecutionModel(Writer writer, String graphName, ExecutionModel model) throws IOException { + public void generateGraphOfExecutionModel(Writer writer, String graphName, ExecutionModelNext model) throws IOException { computeAddressMap(model); graphviz.beginDigraph(graphName); graphviz.append(String.format("label=\"%s\" \n", graphName)); - addAllThreadPos(model); - addReadFrom(model); - addFromRead(model); - addCoherence(model); + addEvents(model); + addRelations(model); graphviz.end(); graphviz.generateOutput(writer); } - private void computeAddressMap(ExecutionModel model) { + private void setRelationsToShow(Configuration config) throws InvalidConfigurationException { + config.inject(this); + relsToShow = Arrays.asList(relsToShowStr.split(",\\s*")); + } + + private BiPredicate getFilter(String relationName) { + return (x, y) -> true; + } + + private void computeAddressMap(ExecutionModelNext model) { model.getMemoryLayoutMap().entrySet().stream() - .sorted(Comparator.comparing(entry -> entry.getValue().address())) - .forEach(entry -> sortedMemoryObjects.add(entry.getValue())); + .sorted(Comparator.comparing(entry -> (BigInteger) entry.getValue().address().getValue())) + .forEach(entry -> sortedMemoryObjects.add(entry.getValue())); } - private boolean ignore(EventData e) { - return false; // We ignore no events for now. + private List getEventModelsToShow(ThreadModel tm) { + return tm.getEventModels() + .stream() + .filter(e -> e instanceof MemoryEventModel + || e instanceof GenericVisibleEventModel + || e instanceof LocalModel + || e instanceof AssertModel) + .toList(); } - private ExecutionGraphVisualizer addReadFrom(ExecutionModel model) { + private ExecutionGraphVisualizer addEvents(ExecutionModelNext model) { + for (ThreadModel tm : model.getThreadModels()) { + List threadEvents = getEventModelsToShow(tm); + if (threadEvents.size() <= 1) { + // This skips init threads. + return this; + } - graphviz.beginSubgraph("ReadFrom"); - graphviz.setEdgeAttributes("color=green"); - for (Map.Entry rw : model.getReadWriteMap().entrySet()) { - EventData r = rw.getKey(); - EventData w = rw.getValue(); + graphviz.beginSubgraph("T" + tm.getId()); - if (ignore(r) || ignore(w) || !rfFilter.test(w, r)) { - continue; + for (EventModel e : threadEvents) { + appendNode(e, (String[]) null); } - appendEdge(w, r, "label=rf"); + graphviz.end(); } - graphviz.end(); return this; } - private ExecutionGraphVisualizer addFromRead(ExecutionModel model) { + private Optional tryParseInt(String s) { + try { + int n = Integer.parseInt(s.substring(s.lastIndexOf("#") + 1)); + return Optional.of(n); + } catch (NumberFormatException e) { + return Optional.empty(); + } + } - graphviz.beginSubgraph("FromRead"); - graphviz.setEdgeAttributes("color=orange"); - for (Map.Entry rw : model.getReadWriteMap().entrySet()) { - EventData r = rw.getKey(); - EventData w = rw.getValue(); + private RelationModel getRelationModelByName(ExecutionModelNext model, String name) { + return model.getRelationModels().stream() + .filter(rm -> rm.getRelation().hasName(name)) + .findFirst().orElse(null); + } - if (ignore(r) || ignore(w)) { - continue; - } + // Getting the correct relation to show is tricky. + // In the case of redefinition, we care about the one defined last. + // If there is no redefinition, we simply return the original one. + private RelationModel getRelationModel(ExecutionModelNext model, String name) { + // First check if the original definition is asked. + if (name.endsWith("#0")) { + String originalName = name.substring(0, name.lastIndexOf("#")); + return getRelationModelByName(model, originalName); + } - 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"); + int maxId = -1; + for (RelationModel rm : model.getRelationModels()) { + int defIndex = -1; + for (String n : rm.getRelation().getNames()) { + if (n.startsWith(name + "#")) { + defIndex = tryParseInt(n).orElse(-1); + if (defIndex > -1) { break; } } } + maxId = Math.max(maxId, defIndex); + } + return maxId != -1 ? getRelationModelByName(model, name + "#" + maxId) + : getRelationModelByName(model, name); + } + + private ExecutionGraphVisualizer addRelations(ExecutionModelNext model) { + for (String name : relsToShow) { + RelationModel rm = getRelationModel(model, name); + if (rm == null) { + logger.warn("Relation with the name {} does not exist", name); + continue; + } + // For PO and CO we do not show the transitive edges in witness. + if (rm.getRelation().getDefinition().getClass() == ProgramOrder.class) { + addProgramOrder(model, name); + } else if (rm.getRelation().getDefinition().getClass() == Coherence.class) { + addCoherence(rm, model, name); + } else { + addRelation(rm, name); + } } - graphviz.end(); return this; } - private ExecutionGraphVisualizer addCoherence(ExecutionModel model) { + private ExecutionGraphVisualizer addRelation(RelationModel rm, String name) { + graphviz.beginSubgraph(name); + String attributes = String.format("color=%s", colorMap.getColor(name)); + graphviz.setEdgeAttributes(attributes); + String label = String.format("label=\"%s\"", name); + BiPredicate filter = rm.getRelation().getDefinition().getClass() == ReadFrom.class ? + rfFilter : getFilter(name); + for (EdgeModel edge : rm.getEdgeModels()) { + EventModel from = edge.getFrom(); + EventModel to = edge.getTo(); - graphviz.beginSubgraph("Coherence"); - graphviz.setEdgeAttributes("color=red"); + if (!filter.test(from, to)) { continue; } - 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(from, to, label); } graphviz.end(); return this; } - private ExecutionGraphVisualizer addAllThreadPos(ExecutionModel model) { - for (Thread thread : model.getThreads()) { - addThreadPo(thread, model); + private ExecutionGraphVisualizer addProgramOrder(ExecutionModelNext model, String name) { + graphviz.beginSubgraph(name); + String attributes = String.format("color=%s, weight=100", colorMap.getColor(PO)); + graphviz.setEdgeAttributes(attributes); + String label = String.format("label=\"%s\"", name); + BiPredicate filter = getFilter(PO); + for (ThreadModel tm : model.getThreadModels()) { + List eventsToShow = getEventModelsToShow(tm); + if (eventsToShow.size() <= 1) { continue; } + for (int i = 1; i < eventsToShow.size(); i++) { + EventModel from = eventsToShow.get(i - 1); + EventModel to = eventsToShow.get(i); + + if (!filter.test(from, to)) { continue; } + + appendEdge(from, to, label); + } } + graphviz.end(); return this; } - private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model) { - List threadEvents = model.getThreadEventsMap().get(thread) - .stream().filter(e -> e.hasTag(Tag.VISIBLE)).toList(); - if (threadEvents.size() <= 1) { - // This skips init threads. - return this; - } + private ExecutionGraphVisualizer addCoherence(RelationModel rm, ExecutionModelNext model, String name) { + graphviz.beginSubgraph(name); + String attributes = String.format("color=%s", colorMap.getColor(CO)); + graphviz.setEdgeAttributes(attributes); + String label = String.format("label=\"%s\"", name); + BiPredicate filter = getFilter(CO); + + Set coModels = rm.getEdgeModels(); + for (Set writes : model.getAddressWritesMap().values()) { + List coSortedWrites; + Map> coEdges = new HashMap<>(); + for (StoreModel w1 : writes) { + coEdges.put(w1, new ArrayList<>()); + for (StoreModel w2 : writes) { + if (coModels.contains(new EdgeModel(w1, w2))) { + coEdges.get(w1).add(w2); + } + } + } + DependencyGraph depGraph = DependencyGraph.from(writes, coEdges); + coSortedWrites = new ArrayList<>(Lists.reverse(depGraph.getNodeContents())); - // --- 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); + for (int i = 0; i < coSortedWrites.size(); i++) { + if (i >= 1) { + EventModel w1 = (EventModel) coSortedWrites.get(i - 1); + EventModel w2 = (EventModel) coSortedWrites.get(i); - if (ignore(e1) || ignore(e2)) { - continue; - } + if (!filter.test(w1, w2)) { continue; } - appendEdge(e1, e2, (String[]) null); + appendEdge(w1, w2, label); + } + } } - - // --- Subgraph end --- graphviz.end(); - return this; } - private String getAddressString(BigInteger address) { + private String getAddressString(ValueModel address) { + final BigInteger addrValue = (BigInteger) address.getValue(); final MemoryObjectModel accObj = Lists.reverse(sortedMemoryObjects).stream() - .filter(o -> o.address().compareTo(address) <= 0) + .filter(o -> ((BigInteger) o.address().getValue()).compareTo(addrValue) <= 0) .findFirst().orElse(null); if (accObj == null) { - return address + " [OOB]"; + return addrValue + " [OOB]"; } else { - final boolean isOOB = address.compareTo(accObj.address().add(accObj.size())) >= 0; - final BigInteger offset = address.subtract(accObj.address()); + final boolean isOOB = addrValue.compareTo(((BigInteger) accObj.address().getValue()).add(accObj.size())) >= 0; + final BigInteger offset = addrValue.subtract((BigInteger) accObj.address().getValue()); return String.format("%s[size=%s]%s%s", accObj.object(), accObj.size(), !offset.equals(BigInteger.ZERO) ? " + " + offset : "", isOOB ? " [OOB]" : "" @@ -203,26 +284,36 @@ private String getAddressString(BigInteger address) { } } - private String eventToNode(EventData e) { - if (e.isInit()) { - return String.format("\"I(%s, %d)\"", getAddressString(e.getAccessedAddress()), e.getValue()); + private String eventToNode(EventModel e) { + if (e instanceof StoreModel sm && e.getEvent() instanceof Init) { + return String.format("\"I(%s, %s)\"", getAddressString( + sm.getAccessedAddress()), sm.getValue() + ); } - // We have MemEvent + Fence + // We have MemEvent + Fence + Local + Assert String tag = e.getEvent().toString(); - if (e.isMemoryEvent()) { - String address = getAddressString(e.getAccessedAddress()); - BigInteger value = e.getValue(); - MemoryOrder mo = e.getEvent().getMetadata(MemoryOrder.class); + if (e instanceof MemoryEventModel mem) { + String address = getAddressString(mem.getAccessedAddress()); + ValueModel value = mem.getValue(); + MemoryOrder mo = mem.getEvent().getMetadata(MemoryOrder.class); String moString = mo == null ? "" : ", " + mo.value(); - tag = e.isWrite() ? - String.format("W(%s, %d%s)", address, value, moString) : + tag = mem instanceof StoreModel ? + String.format("W(%s, %s%s)", address, value, moString) : String.format("%s = R(%s%s)", value, address, moString); + } else if (e instanceof LocalModel lm) { + tag = String.format("%s(%s) <- %s", + lm.getEvent().getResultRegister(), + lm.getValue(), + lm.getEvent().getExpr() + ); + } else if (e instanceof AssertModel am) { + tag = String.format("Assertion(%s)", am.getResult()); } final String callStack = makeContextString( synContext.getContextInfo(e.getEvent()).getContextOfType(CallContext.class), " -> \\n"); final String nodeString = String.format("%s:T%s/E%s\\n%s%s\n%s", - e.getThread().getName(), - e.getThread().getId(), + e.getThreadModel().getName(), + e.getThreadModel().getId(), e.getEvent().getGlobalId(), callStack.isEmpty() ? callStack : callStack + " -> \\n", getSourceLocationString(e.getEvent()), @@ -232,25 +323,33 @@ private String eventToNode(EventData e) { return "\"" + nodeString + "\""; } - private void appendEdge(EventData a, EventData b, String... options) { + private void appendEdge(EventModel a, EventModel b, String... options) { graphviz.addEdge(eventToNode(a), eventToNode(b), options); } - public static File generateGraphvizFile(ExecutionModel model, int iterationCount, - BiPredicate rfFilter, BiPredicate frFilter, - BiPredicate coFilter, String directoryName, String fileNameBase, + private void appendNode(EventModel e, String... attributes) { + graphviz.addNode(eventToNode(e), attributes); + } + + public static File generateGraphvizFile(ExecutionModelNext model, + int iterationCount, + BiPredicate rfFilter, + BiPredicate coFilter, + String directoryName, + String fileNameBase, SyntacticContextAnalysis synContext, - boolean convert) { + boolean convert, + Configuration config) { File fileVio = new File(directoryName + fileNameBase + ".dot"); fileVio.getParentFile().mkdirs(); try (FileWriter writer = new FileWriter(fileVio)) { // Create .dot file - new ExecutionGraphVisualizer() - .setSyntacticContext(synContext) - .setReadFromFilter(rfFilter) - .setFromReadFilter(frFilter) - .setCoherenceFilter(coFilter) - .generateGraphOfExecutionModel(writer, "Iteration " + iterationCount, model); + ExecutionGraphVisualizer visualizer = new ExecutionGraphVisualizer(); + if (config != null) { visualizer.setRelationsToShow(config); } + visualizer.setSyntacticContext(synContext) + .setReadFromFilter(rfFilter) + .setCoherenceFilter(coFilter) + .generateGraphOfExecutionModel(writer, "Iteration " + iterationCount, model); writer.flush(); if (convert) { @@ -264,11 +363,21 @@ public static File generateGraphvizFile(ExecutionModel model, int iterationCount return null; } - public static void generateGraphvizFile(ExecutionModel model, int iterationCount, - BiPredicate rfFilter, BiPredicate frFilter, - BiPredicate coFilter, String directoryName, String fileNameBase, - SyntacticContextAnalysis synContext) { - generateGraphvizFile(model, iterationCount, rfFilter, frFilter, coFilter, directoryName, fileNameBase, - synContext, true); + public static void generateGraphvizFile(ExecutionModelNext model, + int iterationCount, + BiPredicate rfFilter, + BiPredicate coFilter, + String directoryName, + String fileNameBase, + SyntacticContextAnalysis synContext) { + generateGraphvizFile(model, + iterationCount, + rfFilter, + coFilter, + directoryName, + fileNameBase, + synContext, + true, + null); } } 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; }