From b632f5ca1fed66903b734b3046abdc6ed4ec167a Mon Sep 17 00:00:00 2001 From: Natalia Gavrilenko Date: Wed, 25 Sep 2024 10:24:36 +0200 Subject: [PATCH] Relation analysis with immutable and lazy data structures --- .../com/dat3m/dartagnan/GlobalSettings.java | 3 + .../configuration/RelationAnalysisMethod.java | 4 +- .../dat3m/dartagnan/encoding/EncodeSets.java | 16 +- .../dartagnan/encoding/EncodingContext.java | 2 +- .../dartagnan/encoding/LazyEncodeSets.java | 359 ++++ .../dartagnan/encoding/PropertyEncoder.java | 2 +- .../dartagnan/encoding/SymmetryEncoder.java | 6 +- .../dat3m/dartagnan/encoding/WmmEncoder.java | 161 +- .../analysis/alias/EqualityAliasAnalysis.java | 7 +- .../witness/graphml/WitnessGraph.java | 8 +- .../com/dat3m/dartagnan/wmm/Assumption.java | 4 +- .../com/dat3m/dartagnan/wmm/Constraint.java | 2 +- .../wmm/analysis/CoarseRelationAnalysis.java | 13 +- .../wmm/analysis/LazyRelationAnalysis.java | 651 ++++++ .../wmm/analysis/NativeRelationAnalysis.java | 410 ++-- .../wmm/analysis/RelationAnalysis.java | 75 +- .../dat3m/dartagnan/wmm/axiom/Acyclicity.java | 19 +- .../com/dat3m/dartagnan/wmm/axiom/Axiom.java | 2 +- .../dat3m/dartagnan/wmm/axiom/Emptiness.java | 6 +- .../dartagnan/wmm/axiom/ForceEncodeAxiom.java | 2 +- .../dartagnan/wmm/axiom/Irreflexivity.java | 6 +- .../dartagnan/wmm/utils/EmptyEventGraph.java | 51 - .../dat3m/dartagnan/wmm/utils/EventGraph.java | 234 --- .../dartagnan/wmm/utils/graph/EventGraph.java | 82 + .../graph/immutable/ImmutableEventGraph.java | 56 + .../immutable/ImmutableMapEventGraph.java | 225 ++ .../utils/graph/immutable/LazyEventGraph.java | 259 +++ .../utils/graph/mutable/MapEventGraph.java | 303 +++ .../graph/mutable/MutableEventGraph.java | 46 + .../encoding/RelationAnalysisTest.java | 185 ++ .../wmm/utils/EmptyEventGraphTest.java | 359 ---- .../dartagnan/wmm/utils/EventGraphTest.java | 1842 ----------------- .../wmm/utils/graph/EventGraphStaticTest.java | 785 +++++++ .../wmm/utils/graph/EventGraphTest.java | 594 ++++++ .../immutable/EmptyEventGraphStaticTest.java | 359 ++++ .../graph/immutable/EmptyEventGraphTest.java | 187 ++ .../graph/mutable/MutableEventGraphTest.java | 755 +++++++ 37 files changed, 5251 insertions(+), 2829 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java delete mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java delete mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraph.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableEventGraph.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableMapEventGraph.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/LazyEventGraph.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MapEventGraph.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraph.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java delete mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java delete mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphStaticTest.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphTest.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphStaticTest.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphTest.java create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraphTest.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java index 6e36bebf24..8d2ddee97f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java @@ -60,6 +60,9 @@ public static String getHomeDirectory() { } public static String getCatDirectory() { + if (USE_TEST_PATH) { + return "../cat"; + } String env = System.getenv("DAT3M_HOME"); env = env == null ? "" : env; return env + "/cat"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/RelationAnalysisMethod.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/RelationAnalysisMethod.java index c0f57dae6d..fe564d787a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/RelationAnalysisMethod.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/RelationAnalysisMethod.java @@ -3,7 +3,7 @@ import java.util.Arrays; public enum RelationAnalysisMethod implements OptionInterface { - NONE, NATIVE; + NONE, NATIVE, LAZY; public static RelationAnalysisMethod getDefault() { return NATIVE; @@ -11,7 +11,7 @@ public static RelationAnalysisMethod getDefault() { // Used to decide the order shown by the selector in the UI public static RelationAnalysisMethod[] orderedValues() { - RelationAnalysisMethod[] order = { NONE, NATIVE }; + RelationAnalysisMethod[] order = { NONE, NATIVE, LAZY }; // Be sure no element is missing assert(Arrays.asList(order).containsAll(Arrays.asList(values()))); return order; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java index 4a757351ee..d2f239da5d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java @@ -7,7 +7,9 @@ import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.definition.*; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import java.util.HashMap; import java.util.Map; @@ -61,8 +63,8 @@ public Map visitComposition(Composition comp) { final Relation r1 = comp.getLeftOperand(); final Relation r2 = comp.getRightOperand(); - final EventGraph set1 = new EventGraph(); - final EventGraph set2 = new EventGraph(); + final MutableEventGraph set1 = new MapEventGraph(); + final MutableEventGraph set2 = new MapEventGraph(); final RelationAnalysis.Knowledge k1 = ra.getKnowledge(r1); final RelationAnalysis.Knowledge k2 = ra.getKnowledge(r2); Map> out = ra.getKnowledge(r1).getMaySet().getOutMap(); @@ -85,7 +87,7 @@ public Map visitComposition(Composition comp) { public Map visitDomainIdentity(DomainIdentity domId) { final RelationAnalysis.Knowledge k1 = ra.getKnowledge(domId.getOperand()); Map> out = k1.getMaySet().getOutMap(); - EventGraph result = new EventGraph(); + MutableEventGraph result = new MapEventGraph(); news.apply((e1, e2) -> out.getOrDefault(e1, Set.of()).forEach(e -> { if (!k1.getMustSet().contains(e1, e)) { @@ -100,7 +102,7 @@ public Map visitDomainIdentity(DomainIdentity domId) { public Map visitRangeIdentity(RangeIdentity rangeId) { final RelationAnalysis.Knowledge k1 = ra.getKnowledge(rangeId.getOperand()); Map> in = k1.getMaySet().getInMap(); - EventGraph result = new EventGraph(); + MutableEventGraph result = new MapEventGraph(); news.apply((e1, e2) -> in.getOrDefault(e2, Set.of()).forEach(e -> { if (!k1.getMustSet().contains(e, e2)) { @@ -122,7 +124,7 @@ public Map visitInverse(Inverse inv) { public Map visitTransitiveClosure(TransitiveClosure trans) { final Relation rel = trans.getDefinedRelation(); final Relation r1 = trans.getOperand(); - EventGraph factors = new EventGraph(); + MutableEventGraph factors = new MapEventGraph(); final RelationAnalysis.Knowledge k0 = ra.getKnowledge(rel); Map> out = k0.getMaySet().getOutMap(); news.apply((e1, e2) -> { @@ -142,7 +144,7 @@ public Map visitTransitiveClosure(TransitiveClosure trans) @Override public Map visitLinuxCriticalSections(LinuxCriticalSections rscs) { - EventGraph queue = new EventGraph(); + MutableEventGraph queue = new MapEventGraph(); final RelationAnalysis.Knowledge k0 = ra.getKnowledge(rscs.getDefinedRelation()); Map> in = k0.getMaySet().getInMap(); Map> out = k0.getMaySet().getOutMap(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java index 0630de7760..d4e369c89d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java @@ -23,7 +23,7 @@ import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Acyclicity; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.InvalidConfigurationException; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java new file mode 100644 index 0000000000..454b1947b7 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java @@ -0,0 +1,359 @@ +package com.dat3m.dartagnan.encoding; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.wmm.Constraint; +import com.dat3m.dartagnan.wmm.Definition; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; +import com.dat3m.dartagnan.wmm.definition.*; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; +import com.google.common.collect.Sets; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; + +import java.util.*; +import java.util.stream.Collectors; + +public class LazyEncodeSets implements Constraint.Visitor { + + private static final Logger logger = LogManager.getLogger(LazyEncodeSets.class); + + private final RelationAnalysis ra; + private final Map data; + private MutableEventGraph update; + + public LazyEncodeSets(RelationAnalysis ra, Map data) { + this.ra = ra; + this.data = data; + } + + public void add(Relation relation, MutableEventGraph eventGraph) { + setUpdate(eventGraph); + relation.getDefinition().accept(this); + } + + @Override + public Boolean visitDefinition(Definition definition) { + throw new UnsupportedOperationException("Unsupported definition " + + definition.getDefinedRelation().getNameOrTerm() + " " + definition.getClass().getSimpleName()); + } + + @Override + public Boolean visitFree(Free definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitProduct(CartesianProduct definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitSetIdentity(SetIdentity definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitExternal(External definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitInternal(Internal definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitProgramOrder(ProgramOrder definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitControlDependency(DirectControlDependency definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitAddressDependency(DirectAddressDependency definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitInternalDataDependency(DirectDataDependency definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitCASDependency(CASDependency definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitLinuxCriticalSections(LinuxCriticalSections definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitReadModifyWrites(ReadModifyWrites definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitCoherence(Coherence definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitReadFrom(ReadFrom definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitSameLocation(SameLocation definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitSameScope(SameScope definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitSyncBarrier(SyncBar definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitSyncFence(SyncFence definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitSameVirtualLocation(SameVirtualLocation definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitSyncWith(SyncWith definition) { + return doUpdateSelf(definition); + } + + @Override + public Boolean visitDomainIdentity(DomainIdentity definition) { + if (doUpdateSelf(definition)) { + long start = System.currentTimeMillis(); + MutableEventGraph operandUpdate = new MapEventGraph(); + Map> outMap = ra.getKnowledge(definition.getOperand()).getMaySet().getOutMap(); + update.getDomain().forEach(e1 -> operandUpdate.addRange(e1, outMap.get(e1))); + setUpdate(operandUpdate); + operandTime(definition, start, System.currentTimeMillis()); + definition.getOperand().getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitRangeIdentity(RangeIdentity definition) { + if (doUpdateSelf(definition)) { + long start = System.currentTimeMillis(); + MutableEventGraph operandUpdate = new MapEventGraph(); + Map> inMap = ra.getKnowledge(definition.getOperand()).getMaySet().getInMap(); + update.getDomain().forEach(e2 -> inMap.get(e2).forEach(e1 -> operandUpdate.add(e1, e2))); + setUpdate(operandUpdate); + operandTime(definition, start, System.currentTimeMillis()); + definition.getOperand().getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitInverse(Inverse definition) { + if (doUpdateSelf(definition)) { + long start = System.currentTimeMillis(); + setUpdate(update.inverse()); + operandTime(definition, start, System.currentTimeMillis()); + definition.getOperand().getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitTransitiveClosure(TransitiveClosure definition) { + if (doUpdateSelf(definition)) { + long start = System.currentTimeMillis(); + MutableEventGraph operandUpdate = new MapEventGraph(); + RelationAnalysis.Knowledge knowledge = ra.getKnowledge(definition.getDefinedRelation()); + EventGraph may = ImmutableMapEventGraph.from(knowledge.getMaySet()); + EventGraph must = ImmutableMapEventGraph.from(knowledge.getMustSet()); + EventGraph mayInv = may.inverse(); + while (!update.isEmpty()) { + Map> next = new HashMap<>(); + Map> nextInverse = new HashMap<>(); + EventGraph updateInverse = update.inverse(); + update.getDomain().forEach(e1 -> { + Set range = update.getRange(e1); + next.put(e1, may.getRange(e1).stream() + .filter(e -> may.getRange(e).stream().anyMatch(range::contains)) + .collect(Collectors.toSet())); + }); + updateInverse.getDomain().forEach(e2 -> { + Set range = updateInverse.getRange(e2); + nextInverse.put(e2, mayInv.getRange(e2).stream() + .filter(e -> mayInv.getRange(e).stream().anyMatch(range::contains)) + .collect(Collectors.toSet())); + }); + nextInverse.forEach((e2, range) -> range.forEach(e1 -> next.computeIfAbsent(e1, x -> new HashSet<>()).add(e2))); + operandUpdate.addAll(update); + update = new MapEventGraph(next); + update.removeAll(operandUpdate); + update.removeAll(must); + } + getEncodeKnowledge(definition.getDefinedRelation()).addAll(operandUpdate); + operandUpdate.retainAll(ra.getKnowledge(definition.getOperand().getDefinition().getDefinedRelation()).getMaySet()); + setUpdate(operandUpdate); + operandTime(definition, start, System.currentTimeMillis()); + definition.getOperand().getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitUnion(Union definition) { + if (doUpdateSelf(definition)) { + long totalTime = 0; + List operands = definition.getOperands(); + MutableEventGraph origUpdate = update; + for (int i = 0; i < operands.size() - 1; i++) { + long start = System.currentTimeMillis(); + Relation operand = operands.get(i); + MutableEventGraph newUpdate = MapEventGraph.from(origUpdate); + newUpdate.retainAll(ra.getKnowledge(operand.getDefinition().getDefinedRelation()).getMaySet()); + setUpdate(newUpdate); + totalTime += System.currentTimeMillis() - start; + operand.getDefinition().accept(this); + } + long start = System.currentTimeMillis(); + Relation operand = operands.get(operands.size() - 1); + origUpdate.retainAll(ra.getKnowledge(operand.getDefinition().getDefinedRelation()).getMaySet()); + setUpdate(origUpdate); + operandTime(definition, start, totalTime + System.currentTimeMillis()); + operand.getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitIntersection(Intersection definition) { + if (doUpdateSelf(definition)) { + long totalTime = 0; + List operands = definition.getOperands(); + MutableEventGraph origUpdate = update; + for (int i = 0; i < operands.size() - 1; i++) { + long start = System.currentTimeMillis(); + Relation operand = operands.get(i); + MutableEventGraph newUpdate = MapEventGraph.from(origUpdate); + setUpdate(newUpdate); + totalTime += System.currentTimeMillis() - start; + operand.getDefinition().accept(this); + } + long start = System.currentTimeMillis(); + Relation operand = operands.get(operands.size() - 1); + setUpdate(origUpdate); + operandTime(definition, start, totalTime + System.currentTimeMillis()); + operand.getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitDifference(Difference definition) { + if (doUpdateSelf(definition)) { + long totalTime = 0; + long start = System.currentTimeMillis(); + MutableEventGraph origUpdate = update; + MutableEventGraph newUpdate = MapEventGraph.from(origUpdate); + setUpdate(newUpdate); + totalTime += System.currentTimeMillis() - start; + definition.getMinuend().getDefinition().accept(this); + start = System.currentTimeMillis(); + Relation subtrahend = definition.getSubtrahend().getDefinition().getDefinedRelation(); + origUpdate.retainAll(ra.getKnowledge(subtrahend).getMaySet()); + setUpdate(origUpdate); + operandTime(definition, start, totalTime + System.currentTimeMillis()); + definition.getSubtrahend().getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitComposition(Composition definition) { + if (doUpdateSelf(definition)) { + long start = System.currentTimeMillis(); + MapEventGraph leftUpdate = new MapEventGraph(); + MapEventGraph rightUpdate = new MapEventGraph(); + RelationAnalysis.Knowledge leftKnowledge = ra.getKnowledge(definition.getLeftOperand()); + RelationAnalysis.Knowledge rightKnowledge = ra.getKnowledge(definition.getRightOperand()); + EventGraph mayLeft = ImmutableMapEventGraph.from(leftKnowledge.getMaySet()); + EventGraph mayRightInverse = ImmutableMapEventGraph.from(rightKnowledge.getMaySet()).inverse(); + for (Event e1 : update.getDomain()) { + for (Event e2 : update.getRange(e1)) { + Set intermediate = Sets.intersection(mayLeft.getRange(e1), mayRightInverse.getRange(e2)); + for (Event e : intermediate) { + leftUpdate.add(e1, e); + rightUpdate.add(e, e2); + } + } + } + operandTime(definition, start, System.currentTimeMillis()); + setUpdate(leftUpdate); + definition.getLeftOperand().getDefinition().accept(this); + setUpdate(rightUpdate); + definition.getRightOperand().getDefinition().accept(this); + return true; + } + return false; + } + + private boolean doUpdateSelf(Definition definition) { + long start = System.currentTimeMillis(); + Relation relation = definition.getDefinedRelation(); + MutableEventGraph encode = getEncodeKnowledge(relation); + update.removeAll(ra.getKnowledge(relation).getMustSet()); + update.removeAll(encode); + boolean result = encode.addAll(update); + time(definition, start, System.currentTimeMillis(), update.size()); + return result; + } + + private MutableEventGraph getEncodeKnowledge(Relation relation) { + return data.computeIfAbsent(relation, x -> new MapEventGraph()); + } + + private void setUpdate(MutableEventGraph update) { + this.update = update; + } + + private void time(Definition definition, long start, long end, int size) { + if (logger.isDebugEnabled()) { + logger.debug(String.format("%6s ms : %6s edges : %s", end - start, size, + definition.getDefinedRelation().getNameOrTerm())); + } + } + + private void operandTime(Definition definition, long start, long end) { + if (logger.isDebugEnabled()) { + logger.debug(String.format("%6s ms : %s", end - start, + definition.getDefinedRelation().getNameOrTerm())); + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index 994f9da6bd..9b1d1e1ee9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -18,7 +18,7 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Axiom; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import com.google.common.base.Preconditions; import com.google.common.collect.Lists; import org.apache.logging.log4j.LogManager; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java index 8e0bda0348..a8320c36bf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java @@ -9,8 +9,10 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Axiom; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; import com.dat3m.dartagnan.wmm.utils.Tuple; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import com.google.common.base.Preconditions; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -246,7 +248,7 @@ public static BooleanFormula encodeLexLeader(String uniqueIdent, List { if (c != branchEq.getInitialClass() && c != branchEq.getUnreachableClass()) { Event rep = c.getRepresentative(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index b85578e9b2..2ba019cb76 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -5,27 +5,26 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; -import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.event.MemoryEvent; -import com.dat3m.dartagnan.program.event.RegReader; -import com.dat3m.dartagnan.program.event.RegWriter; -import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.event.*; import com.dat3m.dartagnan.program.event.core.ControlBarrier; import com.dat3m.dartagnan.program.event.core.Load; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.core.RMWStoreExclusive; -import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.utils.Utils; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; import com.dat3m.dartagnan.wmm.Constraint; import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.Wmm; +import com.dat3m.dartagnan.wmm.analysis.LazyRelationAnalysis; +import com.dat3m.dartagnan.wmm.analysis.NativeRelationAnalysis; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Axiom; import com.dat3m.dartagnan.wmm.definition.*; -import com.dat3m.dartagnan.wmm.utils.EventGraph; import com.dat3m.dartagnan.wmm.utils.Flag; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import com.google.common.collect.Iterables; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -35,12 +34,12 @@ import org.sosy_lab.java_smt.api.*; import java.util.*; +import java.util.stream.Collectors; import static com.dat3m.dartagnan.configuration.OptionNames.ENABLE_ACTIVE_SETS; import static com.dat3m.dartagnan.configuration.OptionNames.MEMORY_IS_ZEROED; import static com.dat3m.dartagnan.program.event.Tag.*; import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; -import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; import static com.google.common.base.Verify.verify; import static java.lang.Boolean.TRUE; @@ -48,7 +47,7 @@ public class WmmEncoder implements Encoder { private static final Logger logger = LogManager.getLogger(WmmEncoder.class); - final Map encodeSets = new HashMap<>(); + final Map encodeSets; private final EncodingContext context; // ===================================================================== @@ -69,30 +68,30 @@ public class WmmEncoder implements Encoder { private WmmEncoder(EncodingContext c) { context = c; c.getAnalysisContext().requires(RelationAnalysis.class); + encodeSets = initializeEncodeSets(); } public static WmmEncoder withContext(EncodingContext context) throws InvalidConfigurationException { + long t0 = System.currentTimeMillis(); WmmEncoder encoder = new WmmEncoder(context); context.getTask().getConfig().inject(encoder); - logger.info("{}: {}", ENABLE_ACTIVE_SETS, encoder.enableActiveSets); - logger.info("{}: {}", MEMORY_IS_ZEROED, encoder.memoryIsZeroed); - long t0 = System.currentTimeMillis(); - if (encoder.enableActiveSets) { - encoder.initializeEncodeSets(); - } else { - encoder.initializeAlternative(); + if (logger.isInfoEnabled()) { + logger.info("{}: {}", ENABLE_ACTIVE_SETS, encoder.enableActiveSets); + logger.info("{}: {}", MEMORY_IS_ZEROED, encoder.memoryIsZeroed); + logger.info("Finished active sets in {}", Utils.toTimeString(System.currentTimeMillis() - t0)); } - logger.info("Finished active sets in {}", Utils.toTimeString(System.currentTimeMillis() - t0)); RelationAnalysis ra = context.getAnalysisContext().get(RelationAnalysis.class); - logger.info("Number of unknown edges: {}", context.getTask().getMemoryModel().getRelations().stream() - .filter(r -> !r.isInternal()) - .map(ra::getKnowledge) - .mapToLong(k -> difference(k.getMaySet(), k.getMustSet()).size()) - .sum()); - logger.info("Number of encoded edges: {}", encoder.encodeSets.entrySet().stream() - .filter(e -> !e.getKey().isInternal()) - .mapToLong(e -> e.getValue().size()) - .sum()); + if (logger.isInfoEnabled()) { + logger.info("Number of unknown edges: {}", context.getTask().getMemoryModel().getRelations().stream() + .filter(r -> !r.isInternal()) + .map(ra::getKnowledge) + .mapToLong(k -> EventGraph.difference(k.getMaySet(), k.getMustSet()).size()) + .sum()); + logger.info("Number of encoded edges: {}", encoder.encodeSets.entrySet().stream() + .filter(e -> !e.getKey().isInternal()) + .mapToLong(e -> e.getValue().size()) + .sum()); + } return encoder; } @@ -143,12 +142,77 @@ public BooleanFormula encodeConsistency() { public EventGraph getEventGraph(Relation relation, Model model) { EncodingContext.EdgeEncoder edge = context.edge(relation); - EventGraph encodeSet = encodeSets.getOrDefault(relation, EventGraph.empty()) + EventGraph encodeSet = encodeSets.getOrDefault(relation, new MapEventGraph()) .filter((e1, e2) -> TRUE.equals(model.evaluate(edge.encode(e1, e2)))); EventGraph mustEncodeSet = context.getAnalysisContext().get(RelationAnalysis.class).getKnowledge(relation).getMustSet() .filter((e1, e2) -> TRUE.equals(model.evaluate(context.execution(e1, e2)))); - encodeSet.addAll(mustEncodeSet); - return encodeSet; + return EventGraph.union(encodeSet, mustEncodeSet); + } + + private Map initializeEncodeSets() { + RelationAnalysis ra = context.getAnalysisContext().get(RelationAnalysis.class); + if (enableActiveSets) { + if (ra instanceof LazyRelationAnalysis lra) { + return initializeLazyEncodeSets(lra); + } else if (ra instanceof NativeRelationAnalysis nra) { + return initializeNativeEncodeSets(nra); + } else { + throw new UnsupportedOperationException("Encode set computation is not supported by " + + ra.getClass().getSimpleName()); + } + } + return context.getTask().getMemoryModel().getRelations().stream() + .collect(Collectors.toMap(r -> r, r -> ra.getKnowledge(r).getMaySet())); + } + + private Map initializeNativeEncodeSets(NativeRelationAnalysis nra) { + logger.trace("Start"); + Set relations = context.getTask().getMemoryModel().getRelations(); + List axioms = context.getTask().getMemoryModel().getAxioms(); + Map mutableSets = new HashMap<>(); + EncodeSets visitor = new EncodeSets(context.getAnalysisContext()); + Map> queue = new HashMap<>(); + relations.forEach(r -> mutableSets.put(r, new MapEventGraph())); + axioms.forEach(a -> a.getEncodeGraph(context.getTask(), context.getAnalysisContext()) + .forEach((relation, encodeSet) -> { + if (!(encodeSet instanceof MutableEventGraph mutable)) { + throw new IllegalArgumentException("Unexpected immutable event graph in " + nra.getClass().getSimpleName()); + } + queue.computeIfAbsent(relation, k -> new ArrayList<>()).add(mutable); + })); + nra.populateQueue(queue, relations); + while (!queue.isEmpty()) { + Relation r = queue.keySet().iterator().next(); + logger.trace("Update encode set of '{}'", r); + MutableEventGraph s = mutableSets.get(r); + MutableEventGraph c = new MapEventGraph(); + queue.remove(r).forEach(news -> news.filter(s::add).apply(c::add)); + if (!c.isEmpty()) { + visitor.news = c; + r.getDefinition().accept(visitor) + .forEach((key, value) -> queue.computeIfAbsent(key, k -> new ArrayList<>()).add(value)); + } + } + logger.trace("End"); + return relations.stream().collect(Collectors.toMap(r -> r, mutableSets::get)); + } + + private Map initializeLazyEncodeSets(LazyRelationAnalysis lra) { + Set relations = context.getTask().getMemoryModel().getRelations(); + List axioms = context.getTask().getMemoryModel().getAxioms(); + Map mutableSets = new HashMap<>(); + LazyEncodeSets visitor = new LazyEncodeSets(lra, mutableSets); + axioms.forEach(a -> a.getEncodeGraph(context.getTask(), context.getAnalysisContext()) + .forEach((r, eg) -> { + MutableEventGraph copy = new MapEventGraph(eg.getOutMap()); + copy.retainAll(lra.getKnowledge(r).getMaySet()); + visitor.add(r, copy); + // Force adding must edges to match the result of native analysis + // TODO: Is it really necessary? Method getEventGraph appends them anyway + mutableSets.get(r).addAll(eg); + })); + return relations.stream().collect(Collectors.toMap(r -> r, r -> mutableSets.containsKey(r) + ? mutableSets.get(r) : EventGraph.empty())); } private final class RelationEncoder implements Constraint.Visitor { @@ -684,43 +748,4 @@ private BooleanFormula execution(Event e1, Event e2) { return context.execution(e1, e2); } } - - private void initializeAlternative() { - RelationAnalysis ra = context.getAnalysisContext().get(RelationAnalysis.class); - for (Relation r : context.getTask().getMemoryModel().getRelations()) { - encodeSets.put(r, ra.getKnowledge(r).getMaySet()); - } - } - - private void initializeEncodeSets() { - logger.trace("Start"); - for (Relation r : context.getTask().getMemoryModel().getRelations()) { - encodeSets.put(r, new EventGraph()); - } - EncodeSets v = new EncodeSets(context.getAnalysisContext()); - Map> queue = new HashMap<>(); - for (Axiom a : context.getTask().getMemoryModel().getAxioms()) { - for (Map.Entry e : a.getEncodeGraph(context.getTask(), context.getAnalysisContext()).entrySet()) { - queue.computeIfAbsent(e.getKey(), k -> new ArrayList<>()).add(e.getValue()); - } - } - RelationAnalysis ra = context.getAnalysisContext().get(RelationAnalysis.class); - ra.populateQueue(queue, context.getTask().getMemoryModel().getRelations()); - while (!queue.isEmpty()) { - Relation r = queue.keySet().iterator().next(); - logger.trace("Update encode set of '{}'", r); - EventGraph s = encodeSets.get(r); - EventGraph c = new EventGraph(); - for (EventGraph news : queue.remove(r)) { - news.filter(s::add).apply(c::add); - } - if (!c.isEmpty()) { - v.news = c; - for (Map.Entry e : r.getDefinition().accept(v).entrySet()) { - queue.computeIfAbsent(e.getKey(), k -> new ArrayList<>()).add(e.getValue()); - } - } - } - logger.trace("End"); - } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java index 98a4611144..9d5a923e78 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java @@ -5,7 +5,8 @@ import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -20,8 +21,8 @@ */ public class EqualityAliasAnalysis implements AliasAnalysis { - private final EventGraph trueSet = new EventGraph(); - private final EventGraph falseSet = new EventGraph(); + private final MutableEventGraph trueSet = new MapEventGraph(); + private final MutableEventGraph falseSet = new MapEventGraph(); public static EqualityAliasAnalysis fromConfig(Program program, Configuration config) throws InvalidConfigurationException { return new EqualityAliasAnalysis(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessGraph.java index 8e854aeb66..a19784f487 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessGraph.java @@ -7,7 +7,9 @@ import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import com.google.common.collect.Lists; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; @@ -134,7 +136,7 @@ private boolean graphEdgeImpliesHbEdge() { } public EventGraph getReadFromKnowledge(Program program, AliasAnalysis alias) { - EventGraph k = new EventGraph(); + MutableEventGraph k = new MapEventGraph(); MemoryCoreEvent current = null; MemoryCoreEvent last = null; List currents; @@ -154,7 +156,7 @@ public EventGraph getReadFromKnowledge(Program program, AliasAnalysis alias) { } public EventGraph getCoherenceKnowledge(Program program, AliasAnalysis alias) { - EventGraph k = new EventGraph(); + MutableEventGraph k = new MapEventGraph(); final List writes = getPathToViolation().stream() .filter(e -> getEventsFromEdge(program, e).size() == 1 && getEventsFromEdge(program, e).get(0) instanceof Store) .map(e -> (Store) getEventsFromEdge(program, e).get(0)).toList(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java index 788a3b8f09..330384b221 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Assumption.java @@ -1,8 +1,6 @@ package com.dat3m.dartagnan.wmm; -import com.dat3m.dartagnan.wmm.utils.EventGraph; -import org.apache.logging.log4j.LogManager; -import org.apache.logging.log4j.Logger; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java index 73929a897f..f549444074 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -5,7 +5,7 @@ import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.wmm.axiom.*; import com.dat3m.dartagnan.wmm.definition.*; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import org.sosy_lab.java_smt.api.BooleanFormula; import java.util.Collection; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java index 34ac4b120f..dc2a4a39e4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/CoarseRelationAnalysis.java @@ -8,7 +8,8 @@ import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.wmm.*; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -64,19 +65,19 @@ protected Initializer getInitializer() { } private final class EmptyInitializer extends NativeRelationAnalysis.Initializer { - final Knowledge defaultKnowledge; + final MutableKnowledge defaultKnowledge; EmptyInitializer() { - EventGraph may = new EventGraph(); + MutableEventGraph may = new MapEventGraph(); Set events = program.getThreadEvents().stream().filter(e -> e.hasTag(VISIBLE)).collect(toSet()); events.forEach(x -> may.addRange(x, events)); - defaultKnowledge = new Knowledge(may, EventGraph.empty()); + defaultKnowledge = new MutableKnowledge(may, new MapEventGraph()); } @Override - public Knowledge visitDefinition(Definition def) { + public MutableKnowledge visitDefinition(Definition def) { return !def.getDefinedRelation().isInternal() ? defaultKnowledge - : new Knowledge(new EventGraph(), new EventGraph()); + : new MutableKnowledge(new MapEventGraph(), new MapEventGraph()); } } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java new file mode 100644 index 0000000000..1d36a4185c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java @@ -0,0 +1,651 @@ +package com.dat3m.dartagnan.wmm.analysis; + +import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.ScopeHierarchy; +import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; +import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.filter.Filter; +import com.dat3m.dartagnan.verification.Context; +import com.dat3m.dartagnan.verification.VerificationTask; +import com.dat3m.dartagnan.wmm.Definition; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.definition.*; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.LazyEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; +import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Sets; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.sosy_lab.common.configuration.Configuration; + +import java.util.*; +import java.util.concurrent.ConcurrentHashMap; +import java.util.stream.Collectors; + +import static com.dat3m.dartagnan.configuration.Arch.RISCV; +import static com.dat3m.dartagnan.program.Register.UsageType.*; +import static com.dat3m.dartagnan.program.event.Tag.FENCE; +import static com.dat3m.dartagnan.program.event.Tag.VISIBLE; +import static java.util.stream.Collectors.toSet; + +public class LazyRelationAnalysis extends NativeRelationAnalysis { + + private static final Logger logger = LogManager.getLogger(LazyRelationAnalysis.class); + + private final Map lazyKnowledgeMap = new HashMap<>(); + private final LazyInitializer lazyInitializer; + private final Initializer nativeInitializer; + + private LazyRelationAnalysis(VerificationTask task, Context context, Configuration config) { + super(task, context, config); + // TODO: Support for recursive relations + if (task.getMemoryModel().getRelations().stream().anyMatch(Relation::isRecursive)) { + throw new UnsupportedOperationException( + "LazyRelationAnalysis does not support recursive relations yet. " + + "Use another relation analysis method."); + } + this.lazyInitializer = new LazyInitializer(task, context); + this.nativeInitializer = super.getInitializer(); + } + + public static LazyRelationAnalysis fromConfig(VerificationTask task, Context context, Configuration config) { + return new LazyRelationAnalysis(task, context, config); + } + + @Override + public RelationAnalysis.Knowledge getKnowledge(Relation relation) { + return lazyInitializer.getKnowledge(relation); + } + + @Override + public EventGraph getContradictions() { + return ImmutableEventGraph.empty(); + } + + @Override + public void run() { + for (Relation relation : task.getMemoryModel().getRelations()) { + lazyKnowledgeMap.put(relation, lazyInitializer.getKnowledge(relation)); + } + } + + @Override + public void runExtended() { + // TODO: Implementation + } + + @Override + public long countMaySet() { + return lazyKnowledgeMap.values().stream().mapToLong(k -> k.getMaySet().size()).sum(); + } + + @Override + public long countMustSet() { + return lazyKnowledgeMap.values().stream().mapToLong(k -> k.getMustSet().size()).sum(); + } + + private class LazyInitializer implements Definition.Visitor { + private final Program program; + private final ExecutionAnalysis exec; + private final AliasAnalysis alias; + private final ReachingDefinitionsAnalysis definitions; + private final Set visibleEvents; + + public LazyInitializer(VerificationTask task, Context context) { + this.program = task.getProgram(); + this.exec = context.requires(ExecutionAnalysis.class); + this.alias = context.requires(AliasAnalysis.class); + this.definitions = context.requires(ReachingDefinitionsAnalysis.class); + this.visibleEvents = new HashSet<>(program.getThreadEventsWithAllTags(VISIBLE)); + } + + public RelationAnalysis.Knowledge getKnowledge(Relation relation) { + if (!lazyKnowledgeMap.containsKey(relation)) { + RelationAnalysis.Knowledge knowledge = relation.getDefinition().accept(this); + lazyKnowledgeMap.put(relation, knowledge); + } + return lazyKnowledgeMap.get(relation); + } + + @Override + public RelationAnalysis.Knowledge visitDefinition(Definition def) { + throw new UnsupportedOperationException("Unsupported relation " + def.getDefinedRelation().getNameOrTerm()); + } + + @Override + public RelationAnalysis.Knowledge visitFree(Free definition) { + long start = System.currentTimeMillis(); + EventGraph may = new LazyEventGraph(visibleEvents, visibleEvents, (e1, e2) -> true); + EventGraph must = ImmutableEventGraph.empty(); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitProduct(CartesianProduct definition) { + Filter domainFilter = definition.getFirstFilter(); + Filter rangeFilter = definition.getSecondFilter(); + long start = System.currentTimeMillis(); + Set domain = program.getThreadEvents().stream().filter(domainFilter::apply).collect(toSet()); + Set range = program.getThreadEvents().stream().filter(rangeFilter::apply).collect(toSet()); + EventGraph must = new LazyEventGraph(domain, range, (e1, e2) -> !exec.areMutuallyExclusive(e1, e2)); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitSetIdentity(SetIdentity definition) { + Filter filter = definition.getFilter(); + long start = System.currentTimeMillis(); + Map> data = program.getThreadEvents().stream() + .filter(filter::apply) + .collect(Collectors.toMap(e -> e, ImmutableSet::of)); + EventGraph must = new ImmutableMapEventGraph(data); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitInternal(Internal definition) { + long start = System.currentTimeMillis(); + EventGraph must = new LazyEventGraph(visibleEvents, visibleEvents, + (e1, e2) -> e1.getThread().equals(e2.getThread()) + && !exec.areMutuallyExclusive(e1, e2)); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitExternal(External definition) { + long start = System.currentTimeMillis(); + EventGraph must = new LazyEventGraph(visibleEvents, visibleEvents, + (e1, e2) -> !e1.getThread().equals(e2.getThread())); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitProgramOrder(ProgramOrder definition) { + long start = System.currentTimeMillis(); + Set domain = visibleEvents.stream().filter(e1 -> visibleEvents.stream() + .anyMatch(e2 -> e1.getThread().equals(e2.getThread()) + && e1.getGlobalId() < e2.getGlobalId() + && !exec.areMutuallyExclusive(e1, e2))) + .collect(toSet()); + Set range = visibleEvents.stream().filter(e2 -> visibleEvents.stream() + .anyMatch(e1 -> e1.getThread().equals(e2.getThread()) + && e1.getGlobalId() < e2.getGlobalId() + && !exec.areMutuallyExclusive(e1, e2))) + .collect(toSet()); + EventGraph must = new LazyEventGraph(domain, range, + (e1, e2) -> e1.getThread().equals(e2.getThread()) + && e1.getGlobalId() < e2.getGlobalId() + && !exec.areMutuallyExclusive(e1, e2)); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitControlDependency(DirectControlDependency definition) { + long start = System.currentTimeMillis(); + Map> data = new HashMap<>(); + program.getThreads().forEach(t -> t.getEvents(CondJump.class).forEach(j -> { + if (!j.isGoto() && !j.isDead()) { + ImmutableSet range = ((j instanceof IfAsJump ifJump) + ? ifJump.getBranchesEvents() + : j.getSuccessor().getSuccessors()).stream() + .filter(e -> !exec.areMutuallyExclusive(j, e)) + .collect(ImmutableSet.toImmutableSet()); + if (!range.isEmpty()) { + data.put(j, range); + } + } + })); + ImmutableEventGraph must = new ImmutableMapEventGraph(data); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitAddressDependency(DirectAddressDependency definition) { + long start = System.currentTimeMillis(); + EventGraph must = computeInternalDependencies(EnumSet.of(ADDR)); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitInternalDataDependency(DirectDataDependency definition) { + long start = System.currentTimeMillis(); + EventGraph must = computeInternalDependencies(EnumSet.of(DATA, CTRL, OTHER)); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + private EventGraph computeInternalDependencies(Set usageTypes) { + Map> data = new HashMap<>(); + program.getThreadEvents(RegReader.class).forEach(reader -> { + ReachingDefinitionsAnalysis.Writers state = definitions.getWriters(reader); + reader.getRegisterReads().forEach(read -> { + if (usageTypes.contains(read.usageType())) { + Register register = read.register(); + // Register x0 is hardwired to the constant 0 in RISCV + // https://en.wikichip.org/wiki/risc-v/registers, + // and thus it generates no dependency, see + // https://github.com/herd/herdtools7/issues/408 + if (!program.getArch().equals(RISCV) || !register.getName().equals("x0")) { + state.ofRegister(register).getMayWriters().forEach(writer -> + data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader)); + } + } + }); + }); + if (usageTypes.contains(DATA)) { + program.getThreadEvents(ExecutionStatus.class).forEach(execStatus -> { + if (execStatus.doesTrackDep()) { + data.computeIfAbsent(execStatus.getStatusEvent(), x -> new HashSet<>()).add(execStatus); + } + }); + } + return new ImmutableMapEventGraph(data); + } + + @Override + public RelationAnalysis.Knowledge visitCASDependency(CASDependency definition) { + long start = System.currentTimeMillis(); + Map> data = program.getThreadEvents().stream() + .filter(e1 -> e1.hasTag(Tag.IMM.CASDEPORIGIN)) + .collect(Collectors.toMap(e1 -> e1, e1 -> Set.of(e1.getSuccessor()))); + ImmutableEventGraph must = new ImmutableMapEventGraph(data); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitLinuxCriticalSections(LinuxCriticalSections definition) { + long start = System.currentTimeMillis(); + RelationAnalysis.Knowledge base = nativeInitializer.visitLinuxCriticalSections(definition); + EventGraph may = ImmutableMapEventGraph.from(base.getMaySet()); + EventGraph must = ImmutableMapEventGraph.from(base.getMustSet()); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitReadModifyWrites(ReadModifyWrites definition) { + long start = System.currentTimeMillis(); + RelationAnalysis.Knowledge base = nativeInitializer.visitReadModifyWrites(definition); + EventGraph may = ImmutableMapEventGraph.from(base.getMaySet()); + EventGraph must = ImmutableMapEventGraph.from(base.getMustSet()); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitCoherence(Coherence definition) { + long start = System.currentTimeMillis(); + RelationAnalysis.Knowledge base = nativeInitializer.visitCoherence(definition); + EventGraph may = ImmutableMapEventGraph.from(base.getMaySet()); + EventGraph must = ImmutableMapEventGraph.from(base.getMustSet()); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitReadFrom(ReadFrom definition) { + long start = System.currentTimeMillis(); + RelationAnalysis.Knowledge base = nativeInitializer.visitReadFrom(definition); + EventGraph may = ImmutableMapEventGraph.from(base.getMaySet()); + EventGraph must = ImmutableMapEventGraph.from(base.getMustSet()); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitSameLocation(SameLocation definition) { + long start = System.currentTimeMillis(); + List memoryEvents = program.getThreadEvents(MemoryCoreEvent.class); + Map> mayData = new HashMap<>(); + Map> mustData = new HashMap<>(); + for (int i = 0; i < memoryEvents.size(); i++) { + MemoryCoreEvent e1 = memoryEvents.get(i); + for (int j = i; j < memoryEvents.size(); j++) { + MemoryCoreEvent e2 = memoryEvents.get(j); + if (!exec.areMutuallyExclusive(e1, e2) && alias.mayAlias(e1, e2)) { + mayData.computeIfAbsent(e1, x -> new HashSet<>()).add(e2); + mayData.computeIfAbsent(e2, x -> new HashSet<>()).add(e1); + if (alias.mustAlias(e1, e2)) { + mustData.computeIfAbsent(e1, x -> new HashSet<>()).add(e2); + mustData.computeIfAbsent(e2, x -> new HashSet<>()).add(e1); + } + } + } + } + // Cannot be a LazyEventGraph because AliasAnalysis is not thread safe + EventGraph may = new ImmutableMapEventGraph(mayData); + EventGraph must = new ImmutableMapEventGraph(mustData); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitSameScope(SameScope definition) { + long start = System.currentTimeMillis(); + String scope = definition.getSpecificScope(); + Arch arch = program.getArch(); + Map> data = new HashMap<>(); + List events = program.getThreads().stream() + .filter(Thread::hasScope) + .flatMap(t -> t.getEventsWithAllTags(VISIBLE).stream()) + .toList(); + events.forEach(e1 -> { + ScopeHierarchy e1Scope = e1.getThread().getScopeHierarchy(); + ImmutableSet range = events.stream() + .filter(e2 -> !exec.areMutuallyExclusive(e1, e2)) + .filter(e2 -> { + ScopeHierarchy e2Scope = e2.getThread().getScopeHierarchy(); + if (scope != null) { + return e1Scope.canSyncAtScope(e2Scope, scope); + } + String scope1 = Tag.getScopeTag(e1, arch); + String scope2 = Tag.getScopeTag(e2, arch); + return !scope1.isEmpty() && !scope2.isEmpty() + && e1Scope.canSyncAtScope(e2Scope, scope1) + && e2Scope.canSyncAtScope(e1Scope, scope2); + }).collect(ImmutableSet.toImmutableSet()); + if (!range.isEmpty()) { + data.put(e1, range); + } + }); + EventGraph must = new ImmutableMapEventGraph(data); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitSyncBarrier(SyncBar definition) { + long start = System.currentTimeMillis(); + Map> mayData = new HashMap<>(); + Map> mustData = new HashMap<>(); + List barriers = program.getThreadEvents(ControlBarrier.class); + barriers.forEach(e1 -> { + Expression id = e1.getId(); + Set mustRange = new HashSet<>(); + mayData.put(e1, barriers.stream().filter(e2 -> { + if (!exec.areMutuallyExclusive(e1, e2) && !e2.hasTag(Tag.PTX.ARRIVE)) { + if (id.equals(e2.getId())) { + mustRange.add(e2); + } + return true; + } + return false; + }).collect(ImmutableSet.toImmutableSet())); + mustData.put(e1, mustRange); + }); + EventGraph may = new ImmutableMapEventGraph(mayData); + EventGraph must = new ImmutableMapEventGraph(mustData); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitSyncFence(SyncFence definition) { + long start = System.currentTimeMillis(); + Map> data = new HashMap<>(); + List events = program.getThreadEventsWithAllTags(VISIBLE, FENCE, Tag.PTX.SC); + events.forEach(e1 -> data.put(e1, events.stream() + .filter(e2 -> !exec.areMutuallyExclusive(e1, e2)) + .collect(ImmutableSet.toImmutableSet()))); + EventGraph may = new ImmutableMapEventGraph(data); + EventGraph must = ImmutableEventGraph.empty(); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitSameVirtualLocation(SameVirtualLocation definition) { + long start = System.currentTimeMillis(); + RelationAnalysis.Knowledge base = nativeInitializer.visitSameVirtualLocation(definition); + EventGraph may = ImmutableMapEventGraph.from(base.getMaySet()); + EventGraph must = ImmutableMapEventGraph.from(base.getMustSet()); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitSyncWith(SyncWith definition) { + long start = System.currentTimeMillis(); + Map> data = new HashMap<>(); + List events = new ArrayList<>(visibleEvents); + events.removeIf(Init.class::isInstance); + for (Event e1 : events) { + Thread thread1 = e1.getThread(); + if (thread1.hasSyncSet()) { + Set syncSet = thread1.getSyncSet(); + data.put(e1, events.stream() + .filter(e2 -> thread1 != e2.getThread() + && syncSet.contains(e2.getThread()) + && !exec.areMutuallyExclusive(e1, e2)) + .collect(ImmutableSet.toImmutableSet())); + } + } + EventGraph must = new ImmutableMapEventGraph(data); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(must, must); + } + + @Override + public RelationAnalysis.Knowledge visitDomainIdentity(DomainIdentity definition) { + RelationAnalysis.Knowledge knowledge = getKnowledge(definition.getOperand()); + long start = System.currentTimeMillis(); + Map> mayMap = knowledge.getMaySet().getDomain().stream() + .collect(Collectors.toMap(e -> e, ImmutableSet::of)); + EventGraph may = new ImmutableMapEventGraph(mayMap); + Map> mustMap = knowledge.getMustSet() + .filter(exec::isImplied).getDomain().stream() + .collect(Collectors.toMap(e -> e, ImmutableSet::of)); + EventGraph must = new ImmutableMapEventGraph(mustMap); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitRangeIdentity(RangeIdentity definition) { + RelationAnalysis.Knowledge knowledge = getKnowledge(definition.getOperand()); + long start = System.currentTimeMillis(); + Map> mayMap = knowledge.getMaySet().getRange().stream() + .collect(Collectors.toMap(e -> e, ImmutableSet::of)); + EventGraph may = new ImmutableMapEventGraph(mayMap); + Map> mustMap = knowledge.getMustSet() + .filter((e1, e2) -> exec.isImplied(e2, e1)).getRange().stream() + .collect(Collectors.toMap(e -> e, ImmutableSet::of)); + EventGraph must = new ImmutableMapEventGraph(mustMap); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitInverse(Inverse definition) { + RelationAnalysis.Knowledge knowledge = getKnowledge(definition.getOperand()); + long start = System.currentTimeMillis(); + EventGraph may = knowledge.getMaySet().inverse(); + EventGraph must = knowledge.getMustSet().inverse(); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitTransitiveClosure(TransitiveClosure definition) { + EventGraph may = getKnowledge(definition.getOperand()).getMaySet(); + EventGraph must = getKnowledge(definition.getOperand()).getMustSet(); + long start = System.currentTimeMillis(); + EventGraph maySet = computeTransitiveClosureMay(may); + EventGraph mustSet = computeTransitiveClosureMust(must); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(maySet, mustSet); + } + + private EventGraph computeTransitiveClosureMay(EventGraph inner) { + MutableEventGraph outer = MutableEventGraph.from(inner); + Map> innerOut = inner.getOutMap(); + Map> update = new HashMap<>(inner.getOutMap()); + while (!update.isEmpty()) { + Map> next = new ConcurrentHashMap<>(); + Map> current = update; + innerOut.keySet().stream().unordered().parallel().forEach(e1 -> { + Set known = outer.getRange(e1); + Set range = innerOut.get(e1).stream() + .flatMap(e -> current.getOrDefault(e, Set.of()).stream()) + .collect(Collectors.toSet()).stream() + .filter(e -> !known.contains(e)) + .filter(e -> !exec.areMutuallyExclusive(e1, e)) + .collect(Collectors.toSet()); + if (!range.isEmpty()) { + next.put(e1, range); + } + }); + next.forEach(outer::addRange); + update = next; + } + return ImmutableMapEventGraph.from(outer); + } + + private EventGraph computeTransitiveClosureMust(EventGraph inner) { + MutableEventGraph outer = MutableEventGraph.from(inner); + Map> innerOut = inner.getOutMap(); + Map> update = new HashMap<>(inner.getOutMap()); + while (!update.isEmpty()) { + Map> next = new ConcurrentHashMap<>(); + Map> current = update; + innerOut.keySet().stream().unordered().parallel().forEach(e1 -> { + Set known = outer.getRange(e1); + Set range = innerOut.get(e1).stream() + .flatMap(e -> { + if (exec.isImplied(e1, e)) { + return current.getOrDefault(e, Set.of()).stream(); + } + return current.getOrDefault(e, Set.of()).stream() + .filter(e2 -> exec.isImplied(e2, e)); + }) + .collect(Collectors.toSet()).stream() + .filter(e -> !known.contains(e)) + .filter(e -> !exec.areMutuallyExclusive(e1, e)) + .collect(Collectors.toSet()); + if (!range.isEmpty()) { + next.put(e1, range); + } + }); + next.forEach(outer::addRange); + update = next; + } + return ImmutableMapEventGraph.from(outer); + } + + @Override + public RelationAnalysis.Knowledge visitUnion(Union definition) { + List operands = definition.getOperands().stream() + .map(o -> getKnowledge(o.getDefinition().getDefinedRelation())) + .toList(); + long start = System.currentTimeMillis(); + EventGraph may = ImmutableEventGraph.union(operands.stream().map(RelationAnalysis.Knowledge::getMaySet).toArray(EventGraph[]::new)); + EventGraph must = ImmutableEventGraph.union(operands.stream().map(RelationAnalysis.Knowledge::getMustSet).toArray(EventGraph[]::new)); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitIntersection(Intersection definition) { + List operands = definition.getOperands().stream() + .map(o -> getKnowledge(o.getDefinition().getDefinedRelation())) + .toList(); + long start = System.currentTimeMillis(); + EventGraph may = ImmutableEventGraph.intersection(operands.stream().map(RelationAnalysis.Knowledge::getMaySet).toArray(EventGraph[]::new)); + EventGraph must = ImmutableEventGraph.intersection(operands.stream().map(RelationAnalysis.Knowledge::getMustSet).toArray(EventGraph[]::new)); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitDifference(Difference definition) { + RelationAnalysis.Knowledge knowledgeMinuend = getKnowledge(definition.getMinuend()); + RelationAnalysis.Knowledge knowledgeSubtrahend = getKnowledge(definition.getSubtrahend()); + long start = System.currentTimeMillis(); + EventGraph may = ImmutableEventGraph.difference(knowledgeMinuend.getMaySet(), knowledgeSubtrahend.getMustSet()); + EventGraph must = ImmutableEventGraph.difference(knowledgeMinuend.getMustSet(), knowledgeSubtrahend.getMaySet()); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitComposition(Composition definition) { + RelationAnalysis.Knowledge left = getKnowledge(definition.getLeftOperand()); + RelationAnalysis.Knowledge right = getKnowledge(definition.getRightOperand()); + long start = System.currentTimeMillis(); + EventGraph may = computeCompositionMay(left.getMaySet(), right.getMaySet()); + EventGraph must = computeCompositionMust(left.getMustSet(), right.getMustSet()); + time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + private EventGraph computeCompositionMay(EventGraph left, EventGraph right) { + if (left.isEmpty() || right.isEmpty()) { + return ImmutableEventGraph.empty(); + } + Map> result = new ConcurrentHashMap<>(); + Map> leftOut = left.getOutMap(); + Map> rightOut = right.getOutMap(); + Set middle = Sets.intersection(left.getRange(), rightOut.keySet()); + leftOut.keySet().stream().unordered().parallel() + .forEach(e1 -> result.put(e1, leftOut.get(e1).stream() + .filter(middle::contains) + .flatMap(e -> rightOut.getOrDefault(e, Set.of()).stream()) + .collect(toSet()).stream() + .filter(e2 -> !exec.areMutuallyExclusive(e1, e2)) + .collect(ImmutableSet.toImmutableSet()))); + return new ImmutableMapEventGraph(result); + } + + private EventGraph computeCompositionMust(EventGraph left, EventGraph right) { + if (left.isEmpty() || right.isEmpty()) { + return ImmutableEventGraph.empty(); + } + Map> result = new ConcurrentHashMap<>(); + Map> leftOut = left.getOutMap(); + Map> rightOut = right.getOutMap(); + Set middle = Sets.intersection(left.getRange(), rightOut.keySet()); + leftOut.keySet().stream().unordered().parallel() + .forEach(e1 -> result.put(e1, leftOut.get(e1).stream() + .filter(middle::contains) + .flatMap(e -> { + if (exec.isImplied(e1, e)) { + return rightOut.getOrDefault(e, Set.of()).stream(); + } + return rightOut.getOrDefault(e, Set.of()).stream() + .filter(e2 -> exec.isImplied(e2, e)); + }) + .collect(toSet()).stream() + .filter(e2 -> !exec.areMutuallyExclusive(e1, e2)) + .collect(ImmutableSet.toImmutableSet()))); + return new ImmutableMapEventGraph(result); + } + + private void time(Definition definition, long start, long end) { + if (logger.isDebugEnabled()) { + logger.debug(String.format("LRA initial knowledge %6s ms : %s", end - start, + definition.getDefinedRelation().getNameOrTerm())); + } + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java index c9c1dae705..d700c12a6d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java @@ -26,8 +26,10 @@ import com.dat3m.dartagnan.wmm.axiom.Emptiness; import com.dat3m.dartagnan.wmm.axiom.Irreflexivity; import com.dat3m.dartagnan.wmm.definition.*; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import com.dat3m.dartagnan.wmm.utils.Tuple; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; @@ -40,8 +42,6 @@ import static com.dat3m.dartagnan.configuration.Arch.RISCV; import static com.dat3m.dartagnan.program.Register.UsageType.*; import static com.dat3m.dartagnan.program.event.Tag.*; -import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; -import static com.dat3m.dartagnan.wmm.utils.EventGraph.intersection; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Verify.verify; @@ -60,8 +60,8 @@ public class NativeRelationAnalysis implements RelationAnalysis { protected final ReachingDefinitionsAnalysis definitions; protected final AliasAnalysis alias; protected final WmmAnalysis wmmAnalysis; - protected final Map knowledgeMap = new HashMap<>(); - protected final EventGraph mutex = new EventGraph(); + protected final Map knowledgeMap = new HashMap<>(); + protected final MutableEventGraph mutex = new MapEventGraph(); protected NativeRelationAnalysis(VerificationTask t, Context context, Configuration config) { task = checkNotNull(t); @@ -105,29 +105,29 @@ public EventGraph getContradictions() { public void populateQueue(Map> queue, Set relations) { Propagator p = new Propagator(); for (Relation r : relations) { - EventGraph may = new EventGraph(); - EventGraph must = new EventGraph(); + MutableEventGraph may = new MapEventGraph(); + MutableEventGraph must = new MapEventGraph(); if (r.getDependencies().isEmpty()) { continue; } for (Relation c : r.getDependencies()) { p.setSource(c); - p.setMay(getKnowledge(p.getSource()).getMaySet()); - p.setMust(getKnowledge(p.getSource()).getMustSet()); + p.setMay(getMutableKnowledge(p.getSource()).getMaySet()); + p.setMust(getMutableKnowledge(p.getSource()).getMustSet()); Delta s = r.getDefinition().accept(p); may.addAll(s.may); must.addAll(s.must); } may.removeAll(getKnowledge(r).getMaySet()); - EventGraph must2 = difference(getKnowledge(r).getMustSet(), must); - queue.computeIfAbsent(r, k -> new ArrayList<>()).add(EventGraph.union(may, must2)); + MutableEventGraph must2 = MutableEventGraph.difference(getKnowledge(r).getMustSet(), must); + queue.computeIfAbsent(r, k -> new ArrayList<>()).add(MutableEventGraph.union(may, must2)); } } @Override public EventGraph findTransitivelyImpliedCo(Relation co) { final Knowledge k = getKnowledge(co); - EventGraph transCo = new EventGraph(); + MutableEventGraph transCo = new MapEventGraph(); Map> mustIn = k.getMustSet().getInMap(); Map> mustOut = k.getMustSet().getOutMap(); k.getMaySet().apply((e1, e2) -> { @@ -160,7 +160,7 @@ public void run() { final Initializer initializer = getInitializer(); final Map> qGlobal = new HashMap<>(); for (Relation r : memoryModel.getRelations()) { - Knowledge k = r.getDefinition().accept(initializer); + MutableKnowledge k = r.getDefinition().accept(initializer); knowledgeMap.put(r, k); if (!k.getMaySet().isEmpty() || !k.getMustSet().isEmpty()) { qGlobal.computeIfAbsent(r, x -> new ArrayList<>(1)) @@ -174,6 +174,10 @@ public void run() { logger.trace("End"); } + protected MutableKnowledge getMutableKnowledge(Relation relation) { + return knowledgeMap.get(relation); + } + protected void checkAfterRun(Map> qGlobal) { verify(qGlobal.isEmpty(), "knowledge buildup propagated downwards"); } @@ -210,7 +214,7 @@ protected void processSCC(Propagator propagator, Set.N Delta toAdd = Delta.combine(qLocal.remove(relation)); if (relation.getDefinition() instanceof Difference difference) { // Our propagated update may be "too large" so we reduce it. - Knowledge k = knowledgeMap.get(difference.getSubtrahend()); + MutableKnowledge k = knowledgeMap.get(difference.getSubtrahend()); toAdd.may.removeAll(k.getMustSet()); toAdd.must.removeAll(k.getMaySet()); } @@ -257,13 +261,13 @@ public void runExtended() { while (!q.isEmpty()) { Relation relation = q.keySet().iterator().next(); logger.trace("Extended knowledge update for '{}'", relation); - Knowledge knowledge = knowledgeMap.get(relation); + MutableKnowledge knowledge = knowledgeMap.get(relation); ExtendedDelta delta = join(knowledge, q.remove(relation)); if (delta.disabled.isEmpty() && delta.enabled.isEmpty()) { continue; } - mutex.addAll(difference(delta.enabled, knowledge.getMaySet())); - mutex.addAll(intersection(delta.disabled, knowledge.getMustSet())); + mutex.addAll(MutableEventGraph.difference(delta.enabled, knowledge.getMaySet())); + mutex.addAll(MutableEventGraph.intersection(delta.disabled, knowledge.getMustSet())); propagator.origin = relation; EventGraph disabled = propagator.disabled = delta.disabled; EventGraph enabled = propagator.enabled = delta.enabled; @@ -288,13 +292,13 @@ protected Initializer getInitializer() { return new Initializer(); } - private static Delta joinSet(Knowledge k, List l) { + private static Delta joinSet(MutableKnowledge k, List l) { verify(!l.isEmpty(), "empty update"); - EventGraph may = k.getMaySet(); - EventGraph must = k.getMustSet(); + MutableEventGraph may = k.getMaySet(); + MutableEventGraph must = k.getMustSet(); // NOTE optimization due to initial deltas carrying references to knowledge sets - EventGraph maySet = may.isEmpty() || l.get(0).may == may ? may : new EventGraph(); - EventGraph mustSet = must.isEmpty() || l.get(0).must == must ? must : new EventGraph(); + MutableEventGraph maySet = may.isEmpty() || l.get(0).may == may ? may : new MapEventGraph(); + MutableEventGraph mustSet = must.isEmpty() || l.get(0).must == must ? must : new MapEventGraph(); for (Delta d : l) { d.may.apply((e1, e2) -> { if (may.add(e1, e2)) { @@ -310,23 +314,23 @@ private static Delta joinSet(Knowledge k, List l) { return new Delta(maySet, mustSet); } - private static ExtendedDelta join(Knowledge k, List l) { + private static ExtendedDelta join(MutableKnowledge k, List l) { verify(!l.isEmpty(), "empty update in extended analysis"); - EventGraph may = k.getMaySet(); - EventGraph must = k.getMustSet(); - EventGraph disableSet = new EventGraph(); - EventGraph enableSet = new EventGraph(); - l.stream().map(d -> d.disabled).map(EventGraph::new).forEach(e -> e.filter(may::remove).apply(disableSet::add)); - l.stream().map(d -> d.enabled).map(EventGraph::new).forEach(e -> e.filter(must::remove).apply(enableSet::add)); + MutableEventGraph may = k.getMaySet(); + MutableEventGraph must = k.getMustSet(); + MutableEventGraph disableSet = new MapEventGraph(); + MutableEventGraph enableSet = new MapEventGraph(); + l.stream().map(d -> d.disabled).map(MapEventGraph::from).forEach(e -> e.filter(may::remove).apply(disableSet::add)); + l.stream().map(d -> d.enabled).map(MapEventGraph::from).forEach(e -> e.filter(must::remove).apply(enableSet::add)); return new ExtendedDelta(disableSet, enableSet); } private static final class InitialKnowledgeCloser implements Constraint.Visitor> { - private final Map knowledgeMap; + private final Map knowledgeMap; private final Context analysisContext; public InitialKnowledgeCloser( - Map knowledgeMap, + Map knowledgeMap, Context analysisContext) { this.knowledgeMap = knowledgeMap; this.analysisContext = analysisContext; @@ -340,15 +344,15 @@ public Map visitConstraint(Constraint constraint) { @Override public Map visitEmptiness(Emptiness axiom) { Relation rel = axiom.getRelation(); - return Map.of(rel, new ExtendedDelta(knowledgeMap.get(rel).getMaySet(), EventGraph.empty())); + return Map.of(rel, new ExtendedDelta(knowledgeMap.get(rel).getMaySet(), new MapEventGraph())); } @Override public Map visitIrreflexivity(Irreflexivity axiom) { Relation rel = axiom.getRelation(); - Knowledge k = knowledgeMap.get(rel); - EventGraph d = k.getMaySet().filter(Tuple::isLoop); - return Map.of(rel, new ExtendedDelta(d, EventGraph.empty())); + MutableKnowledge k = knowledgeMap.get(rel); + MutableEventGraph d = k.getMaySet().filter(Tuple::isLoop); + return Map.of(rel, new ExtendedDelta(d, new MapEventGraph())); } @Override @@ -356,16 +360,16 @@ public Map visitAcyclicity(Acyclicity axiom) { long t0 = System.currentTimeMillis(); Relation rel = axiom.getRelation(); ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); - Knowledge knowledge = knowledgeMap.get(rel); + MutableKnowledge knowledge = knowledgeMap.get(rel); EventGraph may = knowledge.getMaySet(); EventGraph must = knowledge.getMustSet(); - EventGraph newDisabled = new EventGraph(); + MutableEventGraph newDisabled = new MapEventGraph(); may.filter((e1, e2) -> Tuple.isLoop(e1, e2) || must.contains(e2, e1)).apply(newDisabled::add); Map> mustOut = new HashMap<>(); must.filter((e1, e2) -> !Tuple.isLoop(e1, e2)).apply((e1, e2) -> mustOut.computeIfAbsent(e1, x -> new ArrayList<>()).add(e2)); EventGraph current = knowledge.getMustSet(); do { - EventGraph next = new EventGraph(); + MutableEventGraph next = new MapEventGraph(); current.filter(Tuple::isLoop).apply((x, y) -> { boolean implied = exec.isImplied(x, y); mustOut.getOrDefault(y, List.of()).stream() @@ -378,15 +382,15 @@ public Map visitAcyclicity(Acyclicity axiom) { } while (!current.isEmpty()); newDisabled.retainAll(knowledge.getMaySet()); logger.debug("disabled {} edges in {}ms", newDisabled.size(), System.currentTimeMillis() - t0); - return Map.of(rel, new ExtendedDelta(newDisabled, EventGraph.empty())); + return Map.of(rel, new ExtendedDelta(newDisabled, new MapEventGraph())); } @Override public Map visitAssumption(Assumption assume) { Relation rel = assume.getRelation(); - Knowledge k = knowledgeMap.get(rel); - EventGraph d = difference(k.getMaySet(), assume.getMaySet()); - EventGraph e = difference(assume.getMustSet(), k.getMustSet()); + MutableKnowledge k = knowledgeMap.get(rel); + MutableEventGraph d = MutableEventGraph.difference(k.getMaySet(), assume.getMaySet()); + MutableEventGraph e = MutableEventGraph.difference(assume.getMustSet(), k.getMustSet()); if (d.size() + e.size() != 0) { logger.info("Assumption disables {} and enables {} at {}", d.size(), e.size(), rel.getNameOrTerm()); } @@ -398,14 +402,14 @@ private static final class IncrementalKnowledgeCloser implements Constraint.Visi private final Relation changed; private final EventGraph disabled; private final EventGraph enabled; - private final Map knowledgeMap; + private final Map knowledgeMap; private final Context analysisContext; public IncrementalKnowledgeCloser( Relation changed, EventGraph disabled, EventGraph enabled, - Map knowledgeMap, + Map knowledgeMap, Context analysisContext) { this.changed = changed; this.disabled = disabled; @@ -426,9 +430,9 @@ public Map visitAcyclicity(Acyclicity axiom) { "misdirected knowledge propagation from relation %s to %s", changed, this); long t0 = System.currentTimeMillis(); ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); - Knowledge knowledge = knowledgeMap.get(rel); + MutableKnowledge knowledge = knowledgeMap.get(rel); EventGraph may = knowledge.getMaySet(); - EventGraph newDisabled = new EventGraph(); + MutableEventGraph newDisabled = new MapEventGraph(); enabled.filter((e1, e2) -> may.contains(e2, e1)).apply((e1, e2) -> newDisabled.add(e2, e1)); Map> mustIn = new HashMap<>(); Map> mustOut = new HashMap<>(); @@ -439,7 +443,7 @@ public Map visitAcyclicity(Acyclicity axiom) { EventGraph current = enabled; do { - EventGraph next = new EventGraph(); + MutableEventGraph next = new MapEventGraph(); current.filter((x, y) -> !Tuple.isLoop(x, y)).apply((x, y) -> { boolean implies = exec.isImplied(x, y); boolean implied = exec.isImplied(y, x); @@ -458,24 +462,24 @@ public Map visitAcyclicity(Acyclicity axiom) { } while (!current.isEmpty()); newDisabled.retainAll(knowledge.getMaySet()); logger.debug("Disabled {} edges in {}ms", newDisabled.size(), System.currentTimeMillis() - t0); - return Map.of(rel, new ExtendedDelta(newDisabled, EventGraph.empty())); + return Map.of(rel, new ExtendedDelta(newDisabled, new MapEventGraph())); } } - protected class Initializer implements Definition.Visitor { + protected class Initializer implements Definition.Visitor { final Program program = task.getProgram(); final WitnessGraph witness = task.getWitness(); @Override - public Knowledge visitDefinition(Definition def) { - return new Knowledge(new EventGraph(), new EventGraph()); + public MutableKnowledge visitDefinition(Definition def) { + return new MutableKnowledge(new MapEventGraph(), new MapEventGraph()); } @Override - public Knowledge visitFree(Free def) { + public MutableKnowledge visitFree(Free def) { final List visibleEvents = program.getThreadEventsWithAllTags(VISIBLE); - EventGraph must = EventGraph.empty(); - EventGraph may = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); + MutableEventGraph may = new MapEventGraph(); for (Event e1 : visibleEvents) { for (Event e2 : visibleEvents) { @@ -483,14 +487,14 @@ public Knowledge visitFree(Free def) { } } - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitProduct(CartesianProduct prod) { + public MutableKnowledge visitProduct(CartesianProduct prod) { final Filter domain = prod.getFirstFilter(); final Filter range = prod.getSecondFilter(); - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); List l1 = program.getThreadEvents().stream().filter(domain::apply).toList(); List l2 = program.getThreadEvents().stream().filter(range::apply).toList(); for (Event e1 : l1) { @@ -499,20 +503,20 @@ public Knowledge visitProduct(CartesianProduct prod) { .collect(toSet()); must.addRange(e1, rangeEvents); } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitSetIdentity(SetIdentity id) { + public MutableKnowledge visitSetIdentity(SetIdentity id) { final Filter set = id.getFilter(); - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); program.getThreadEvents().stream().filter(set::apply).forEach(e -> must.add(e, e)); - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitExternal(External ext) { - EventGraph must = new EventGraph(); + public MutableKnowledge visitExternal(External ext) { + MutableEventGraph must = new MapEventGraph(); List threads = program.getThreads(); for (int i = 0; i < threads.size(); i++) { Thread t1 = threads.get(i); @@ -528,12 +532,12 @@ public Knowledge visitExternal(External ext) { } } } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitInternal(Internal internal) { - EventGraph must = new EventGraph(); + public MutableKnowledge visitInternal(Internal internal) { + MutableEventGraph must = new MapEventGraph(); for (Thread t : program.getThreads()) { List events = visibleEvents(t); for (Event e1 : events) { @@ -543,13 +547,13 @@ public Knowledge visitInternal(Internal internal) { must.addRange(e1, rangeEvents); } } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitProgramOrder(ProgramOrder po) { + public MutableKnowledge visitProgramOrder(ProgramOrder po) { final Filter type = po.getFilter(); - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); for (Thread t : program.getThreads()) { List events = t.getEvents().stream().filter(type::apply).toList(); for (int i = 0; i < events.size(); i++) { @@ -562,14 +566,14 @@ public Knowledge visitProgramOrder(ProgramOrder po) { } } } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitControlDependency(DirectControlDependency ctrlDep) { + public MutableKnowledge visitControlDependency(DirectControlDependency ctrlDep) { //TODO: We can restrict the codomain to visible events as the only usage of this Relation is in // ctrl := idd^+;ctrlDirect & (R*V) - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); for (Thread thread : program.getThreads()) { for (CondJump jump : thread.getEvents(CondJump.class)) { if (jump.isGoto() || jump.isDead()) { @@ -593,36 +597,36 @@ public Knowledge visitControlDependency(DirectControlDependency ctrlDep) { } } } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitAddressDependency(DirectAddressDependency addrDep) { + public MutableKnowledge visitAddressDependency(DirectAddressDependency addrDep) { return computeInternalDependencies(EnumSet.of(ADDR)); } @Override - public Knowledge visitInternalDataDependency(DirectDataDependency idd) { + public MutableKnowledge visitInternalDataDependency(DirectDataDependency idd) { // FIXME: Our "internal data dependency" relation is quite odd an contains all but address dependencies. return computeInternalDependencies(EnumSet.of(DATA, CTRL, OTHER)); } @Override - public Knowledge visitCASDependency(CASDependency casDep) { - EventGraph must = new EventGraph(); + public MutableKnowledge visitCASDependency(CASDependency casDep) { + MutableEventGraph must = new MapEventGraph(); for (Event e : program.getThreadEvents()) { if (e.hasTag(IMM.CASDEPORIGIN)) { // The target of a CASDep is always the successor of the origin must.add(e, e.getSuccessor()); } } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitLinuxCriticalSections(LinuxCriticalSections rscs) { - EventGraph may = new EventGraph(); - EventGraph must = new EventGraph(); + public MutableKnowledge visitLinuxCriticalSections(LinuxCriticalSections rscs) { + MutableEventGraph may = new MapEventGraph(); + MutableEventGraph must = new MapEventGraph(); //assume locks and unlocks are distinct Map> mayMap = new HashMap<>(); Map> mustMap = new HashMap<>(); @@ -657,14 +661,14 @@ public Knowledge visitLinuxCriticalSections(LinuxCriticalSections rscs) { } } } - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitReadModifyWrites(ReadModifyWrites rmw) { + public MutableKnowledge visitReadModifyWrites(ReadModifyWrites rmw) { //NOTE: Changes to the semantics of this method may need to be reflected in RMWGraph for Refinement! // ----- Compute must set ----- - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); // RMWLoad -> RMWStore for (RMWStore store : program.getThreadEvents(RMWStore.class)) { must.add(store.getLoadEvent(), store); @@ -683,7 +687,7 @@ public Knowledge visitReadModifyWrites(ReadModifyWrites rmw) { } } // ----- Compute may set ----- - EventGraph may = new EventGraph(must); + MutableEventGraph may = MapEventGraph.from(must); // LoadExcl -> StoreExcl for (Thread thread : program.getThreads()) { List events = thread.getEvents().stream().filter(e -> e.hasTag(EXCL)).toList(); @@ -714,16 +718,16 @@ public Knowledge visitReadModifyWrites(ReadModifyWrites rmw) { } } } - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitCoherence(Coherence co) { + public MutableKnowledge visitCoherence(Coherence co) { logger.trace("Computing knowledge about memory order"); List allWrites = program.getThreadEvents(Store.class); List nonInitWrites = program.getThreadEvents(Store.class); nonInitWrites.removeIf(Init.class::isInstance); - EventGraph may = new EventGraph(); + MutableEventGraph may = new MapEventGraph(); for (Store w1 : program.getThreadEvents(Store.class)) { // It is possible to have multiple initial writes // to the same memory location via different virtual memory aliases @@ -735,7 +739,7 @@ public Knowledge visitCoherence(Coherence co) { } } } - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); may.apply((e1, e2) -> { MemoryCoreEvent w1 = (MemoryCoreEvent) e1; MemoryCoreEvent w2 = (MemoryCoreEvent) e2; @@ -760,15 +764,15 @@ public Knowledge visitCoherence(Coherence co) { } logger.debug("Initial may set size for memory order: {}", may.size()); - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitReadFrom(ReadFrom rf) { + public MutableKnowledge visitReadFrom(ReadFrom rf) { logger.trace("Computing knowledge about read-from"); final BranchEquivalence eq = analysisContext.requires(BranchEquivalence.class); - EventGraph may = new EventGraph(); - EventGraph must = new EventGraph(); + MutableEventGraph may = new MapEventGraph(); + MutableEventGraph must = new MapEventGraph(); List loadEvents = program.getThreadEvents(Load.class); for (Store e1 : program.getThreadEvents(Store.class)) { for (Load e2 : loadEvents) { @@ -795,7 +799,7 @@ public Knowledge visitReadFrom(ReadFrom rf) { // Remove future reads may.removeIf(Tuple::isBackward); // Remove past reads - EventGraph deletedEdges = new EventGraph(); + MutableEventGraph deletedEdges = new MapEventGraph(); Map> writesByRead = new HashMap<>(); may.apply((e1, e2) -> writesByRead.computeIfAbsent(e2, x -> new ArrayList<>()).add(e1)); for (Load read : program.getThreadEvents(Load.class)) { @@ -876,12 +880,12 @@ public Knowledge visitReadFrom(ReadFrom rf) { } logger.debug("Initial may set size for read-from: {}", may.size()); - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitSameLocation(SameLocation loc) { - EventGraph may = new EventGraph(); + public MutableKnowledge visitSameLocation(SameLocation loc) { + MutableEventGraph may = new MapEventGraph(); List events = program.getThreadEvents(MemoryCoreEvent.class); for (MemoryCoreEvent e1 : events) { for (MemoryCoreEvent e2 : events) { @@ -890,18 +894,18 @@ public Knowledge visitSameLocation(SameLocation loc) { } } } - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); may.apply((e1, e2) -> { if (alias.mustAlias((MemoryCoreEvent) e1, (MemoryCoreEvent) e2)) { must.add(e1, e2); } }); - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } - private Knowledge computeInternalDependencies(Set usageTypes) { - EventGraph may = new EventGraph(); - EventGraph must = new EventGraph(); + private MutableKnowledge computeInternalDependencies(Set usageTypes) { + MutableEventGraph may = new MapEventGraph(); + MutableEventGraph must = new MapEventGraph(); for (RegReader regReader : program.getThreadEvents(RegReader.class)) { final ReachingDefinitionsAnalysis.Writers state = definitions.getWriters(regReader); @@ -939,13 +943,13 @@ private Knowledge computeInternalDependencies(Set usageTypes) { } } - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitSameScope(SameScope sc) { + public MutableKnowledge visitSameScope(SameScope sc) { final String specificScope = sc.getSpecificScope(); - EventGraph must = new EventGraph(); + MutableEventGraph must = new MapEventGraph(); List events = program.getThreadEvents().stream() .filter(e -> e.hasTag(VISIBLE) && e.getThread().hasScope()) .toList(); @@ -970,19 +974,19 @@ public Knowledge visitSameScope(SameScope sc) { } } } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } @Override - public Knowledge visitSyncBarrier(SyncBar syncBar) { - EventGraph may = new EventGraph(); - EventGraph must = new EventGraph(); + public MutableKnowledge visitSyncBarrier(SyncBar syncBar) { + MutableEventGraph may = new MapEventGraph(); + MutableEventGraph must = new MapEventGraph(); List barriers = program.getThreadEvents(ControlBarrier.class); for (ControlBarrier e1 : barriers) { for (ControlBarrier e2 : barriers) { // “A bar.sync or bar.red or bar.arrive operation synchronizes with a bar.sync // or bar.red operation executed on the same barrier.” - if (exec.areMutuallyExclusive(e1, e2) || e2.hasTag(PTX.ARRIVE)) { + if (exec.areMutuallyExclusive(e1, e2) || e2.hasTag(Tag.PTX.ARRIVE)) { continue; } may.add(e1, e2); @@ -991,14 +995,14 @@ public Knowledge visitSyncBarrier(SyncBar syncBar) { } } } - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitSyncFence(SyncFence syncFence) { - EventGraph may = new EventGraph(); - EventGraph must = EventGraph.empty(); - List fenceEventsSC = program.getThreadEventsWithAllTags(VISIBLE, FENCE, PTX.SC); + public MutableKnowledge visitSyncFence(SyncFence syncFence) { + MutableEventGraph may = new MapEventGraph(); + MutableEventGraph must = new MapEventGraph(); + List fenceEventsSC = program.getThreadEventsWithAllTags(VISIBLE, FENCE, Tag.PTX.SC); for (Event e1 : fenceEventsSC) { for (Event e2 : fenceEventsSC) { if (!exec.areMutuallyExclusive(e1, e2)) { @@ -1006,13 +1010,13 @@ public Knowledge visitSyncFence(SyncFence syncFence) { } } } - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } @Override - public Knowledge visitSameVirtualLocation(SameVirtualLocation vloc) { - EventGraph must = new EventGraph(); - EventGraph may = new EventGraph(); + public MutableKnowledge visitSameVirtualLocation(SameVirtualLocation vloc) { + MutableEventGraph must = new MapEventGraph(); + MutableEventGraph may = new MapEventGraph(); Map map = computeViltualAddressMap(); map.forEach((e1, a1) -> map.forEach((e2, a2) -> { if (a1.equals(a2) && !exec.areMutuallyExclusive(e1, e2)) { @@ -1024,7 +1028,7 @@ public Knowledge visitSameVirtualLocation(SameVirtualLocation vloc) { } } })); - return new Knowledge(may, must); + return new MutableKnowledge(may, must); } private Map computeViltualAddressMap() { @@ -1047,8 +1051,8 @@ private Map computeViltualAddressMap() { } @Override - public Knowledge visitSyncWith(SyncWith syncWith) { - EventGraph must = new EventGraph(); + public MutableKnowledge visitSyncWith(SyncWith syncWith) { + MutableEventGraph must = new MapEventGraph(); List events = new ArrayList<>(program.getThreadEventsWithAllTags(VISIBLE)); events.removeIf(Init.class::isInstance); for (Event e1 : events) { @@ -1063,14 +1067,14 @@ public Knowledge visitSyncWith(SyncWith syncWith) { } } } - return new Knowledge(must, new EventGraph(must)); + return new MutableKnowledge(must, MapEventGraph.from(must)); } } private final class ExtendedPropagator implements Definition.Visitor> { Relation origin; - EventGraph disabled; - EventGraph enabled; + MutableEventGraph disabled; + MutableEventGraph enabled; @Override public Map visitDefinition(Definition def) { @@ -1084,11 +1088,11 @@ public Map visitUnion(Union union) { Map map = new HashMap<>(); if (origin.equals(rel)) { for (Relation o : operands) { - map.put(o, new ExtendedDelta(disabled, EventGraph.empty())); + map.put(o, new ExtendedDelta(disabled, new MapEventGraph())); } } if (operands.contains(origin)) { - EventGraph d = new EventGraph(); + MutableEventGraph d = new MapEventGraph(); disabled.apply((e1, e2) -> { if (operands.stream().noneMatch(o -> knowledgeMap.get(o).getMaySet().contains(e1, e2))) { d.add(e1, e2); @@ -1106,19 +1110,19 @@ public Map visitIntersection(Intersection inter) { Map map = new HashMap<>(); if (origin.equals(rel)) { for (Relation o : operands) { - EventGraph d = operands.stream() + MutableEventGraph d = operands.stream() .map(r -> o.equals(r) ? disabled : knowledgeMap.get(r).getMustSet()) .sorted(Comparator.comparingInt(EventGraph::size)) - .reduce(EventGraph::intersection) + .reduce(MutableEventGraph::intersection) .orElseThrow(); map.putIfAbsent(o, new ExtendedDelta(d, enabled)); } } if (operands.contains(origin)) { - EventGraph e = operands.stream() + MutableEventGraph e = operands.stream() .map(r -> origin.equals(r) ? enabled : knowledgeMap.get(r).getMustSet()) .sorted(Comparator.comparingInt(EventGraph::size)) - .reduce(EventGraph::intersection) + .reduce(MutableEventGraph::intersection) .orElseThrow(); map.put(rel, new ExtendedDelta(disabled, e)); } @@ -1132,16 +1136,15 @@ public Map visitDifference(Difference diff) { final Relation r2 = diff.getSubtrahend(); Map map = new HashMap<>(); if (origin.equals(r0)) { - map.put(r1, new ExtendedDelta(difference(disabled, knowledgeMap.get(r2).getMaySet()), enabled)); - //map.put(r2, new ExtendedDelta(EMPTY_SET, intersection(disabled, knowledgeMap.get(r1).getMustSet()))); + map.put(r1, new ExtendedDelta(MutableEventGraph.difference(disabled, knowledgeMap.get(r2).getMaySet()), enabled)); } if (origin.equals(r1)) { - map.put(r0, new ExtendedDelta(disabled, difference(enabled, knowledgeMap.get(r2).getMaySet()))); + map.put(r0, new ExtendedDelta(disabled, MutableEventGraph.difference(enabled, knowledgeMap.get(r2).getMaySet()))); } if (origin.equals(r2)) { - Knowledge k1 = knowledgeMap.get(r1); - map.put(r0, new ExtendedDelta(intersection(enabled, k1.getMaySet()), intersection(disabled, k1.getMustSet()))); - map.put(r1, new ExtendedDelta(difference(disabled, knowledgeMap.get(r0).getMaySet()), EventGraph.empty())); + MutableKnowledge k1 = knowledgeMap.get(r1); + map.put(r0, new ExtendedDelta(MutableEventGraph.intersection(enabled, k1.getMaySet()), MutableEventGraph.intersection(disabled, k1.getMustSet()))); + map.put(r1, new ExtendedDelta(MutableEventGraph.difference(disabled, knowledgeMap.get(r0).getMaySet()), new MapEventGraph())); } return map; } @@ -1151,13 +1154,13 @@ public Map visitComposition(Composition comp) { final Relation r0 = comp.getDefinedRelation(); final Relation r1 = comp.getLeftOperand(); final Relation r2 = comp.getRightOperand(); - EventGraph d0 = new EventGraph(); - EventGraph e0 = new EventGraph(); - EventGraph d1 = new EventGraph(); - EventGraph d2 = new EventGraph(); - Knowledge k0 = knowledgeMap.get(r0); - Knowledge k1 = knowledgeMap.get(r1); - Knowledge k2 = knowledgeMap.get(r2); + MutableEventGraph d0 = new MapEventGraph(); + MutableEventGraph e0 = new MapEventGraph(); + MutableEventGraph d1 = new MapEventGraph(); + MutableEventGraph d2 = new MapEventGraph(); + MutableKnowledge k0 = knowledgeMap.get(r0); + MutableKnowledge k1 = knowledgeMap.get(r1); + MutableKnowledge k2 = knowledgeMap.get(r2); if (origin.equals(r0)) { Map> mustOut1 = k1.getMustSet().getOutMap(); Map> mustIn2 = k2.getMustSet().getInMap(); @@ -1195,8 +1198,8 @@ public Map visitComposition(Composition comp) { Map map = new HashMap<>(); map.put(r0, new ExtendedDelta(d0, e0)); - map.computeIfAbsent(r1, k -> new ExtendedDelta(d1, new EventGraph())).disabled.addAll(d1); - map.computeIfAbsent(r2, k -> new ExtendedDelta(d2, new EventGraph())).disabled.addAll(d2); + map.computeIfAbsent(r1, k -> new ExtendedDelta(d1, new MapEventGraph())).disabled.addAll(d1); + map.computeIfAbsent(r2, k -> new ExtendedDelta(d2, new MapEventGraph())).disabled.addAll(d2); return map; } @@ -1220,7 +1223,7 @@ private EventGraph handleCompositionDisabledSet( EventGraph mayOut1, EventGraph mayOut2 ) { - EventGraph result = new EventGraph(); + MutableEventGraph result = new MapEventGraph(); for (Event e1 : disOut1.getDomain()) { for (Event e : disOut1.getRange(e1)) { Set e2Set = new HashSet<>(mayOut2.getRange(e)); @@ -1246,8 +1249,8 @@ private List handleCompositionEnabledSet( EventGraph mustOut2, EventGraph mayOut0 ) { - EventGraph enOut0 = new EventGraph(); - EventGraph disOut2 = new EventGraph(); + MutableEventGraph enOut0 = new MapEventGraph(); + MutableEventGraph disOut2 = new MapEventGraph(); for (Event e1 : enOut1.getDomain()) { for (Event e : enOut1.getRange(e1)) { Set e2Set = new HashSet<>(mayOut2.getRange(e)); @@ -1275,7 +1278,7 @@ public Map visitInverse(Inverse inv) { final Relation r0 = inv.getDefinedRelation(); final Relation r1 = inv.getOperand(); if (origin.equals(r0)) { - return Map.of(r1, new ExtendedDelta(disabled.inverse(), EventGraph.empty())); + return Map.of(r1, new ExtendedDelta(disabled.inverse(), new MapEventGraph())); } if (origin.equals(r1)) { return Map.of(r0, new ExtendedDelta(disabled.inverse(), enabled.inverse())); @@ -1287,11 +1290,11 @@ public Map visitInverse(Inverse inv) { public Map visitTransitiveClosure(TransitiveClosure trans) { final Relation r0 = trans.getDefinedRelation(); final Relation r1 = trans.getOperand(); - EventGraph d0 = new EventGraph(); - EventGraph e0 = new EventGraph(); - EventGraph d1 = new EventGraph(); - Knowledge k0 = knowledgeMap.get(r0); - Knowledge k1 = knowledgeMap.get(r1); + MutableEventGraph d0 = new MapEventGraph(); + MutableEventGraph e0 = new MapEventGraph(); + MutableEventGraph d1 = new MapEventGraph(); + MutableKnowledge k0 = knowledgeMap.get(r0); + MutableKnowledge k1 = knowledgeMap.get(r1); if (origin.equals(r1)) { Map> mayOut0 = k0.getMaySet().getOutMap(); Map> mayIn0 = k0.getMaySet().getInMap(); @@ -1334,7 +1337,7 @@ public Map visitTransitiveClosure(TransitiveClosure tra Map> mustIn0 = k0.getMustSet().getInMap(); Map> mayIn1 = k1.getMaySet().getInMap(); Map> mustOut1 = k1.getMustSet().getOutMap(); - d1.addAll(intersection(disabled, k1.getMaySet())); + d1.addAll(EventGraph.intersection(disabled, k1.getMaySet())); disabled.apply((x, z) -> { if (!Tuple.isLoop(x, z)) { boolean implied = exec.isImplied(z, x); @@ -1371,7 +1374,7 @@ public Map visitTransitiveClosure(TransitiveClosure tra } return Map.of( r0, new ExtendedDelta(d0, e0), - r1, new ExtendedDelta(d1, EventGraph.empty())); + r1, new ExtendedDelta(d1, new MapEventGraph())); } @Override @@ -1380,13 +1383,13 @@ public Map visitCoherence(Coherence coDef) { return Map.of(); } //TODO use transitivity - EventGraph e = new EventGraph(); + MutableEventGraph e = new MapEventGraph(); disabled.apply((x, y) -> { if (alias.mustAlias((MemoryCoreEvent) x, (MemoryCoreEvent) y)) { e.add(y, x); } }); - return Map.of(coDef.getDefinedRelation(), new ExtendedDelta(EventGraph.empty(), e)); + return Map.of(coDef.getDefinedRelation(), new ExtendedDelta(new MapEventGraph(), e)); } } @@ -1405,12 +1408,12 @@ public long countMustSet() { } protected static final class Delta { - public static final Delta EMPTY = new Delta(EventGraph.empty(), EventGraph.empty()); + public static final Delta EMPTY = new Delta(new MapEventGraph(), new MapEventGraph()); - public final EventGraph may; - public final EventGraph must; + public final MutableEventGraph may; + public final MutableEventGraph must; - public Delta(EventGraph maySet, EventGraph mustSet) { + public Delta(MutableEventGraph maySet, MutableEventGraph mustSet) { may = maySet; must = mustSet; } @@ -1419,8 +1422,8 @@ public static Delta combine(List deltas) { if (deltas.size() == 1) { return deltas.get(0); } - EventGraph mayDelta = new EventGraph(); - EventGraph mustDelta = new EventGraph(); + MutableEventGraph mayDelta = new MapEventGraph(); + MutableEventGraph mustDelta = new MapEventGraph(); for (Delta d : deltas) { mayDelta.addAll(d.may); mustDelta.addAll(d.must); @@ -1431,10 +1434,10 @@ public static Delta combine(List deltas) { //FIXME should be visible only to implementations of Constraint private static final class ExtendedDelta { - final EventGraph disabled; - final EventGraph enabled; + final MutableEventGraph disabled; + final MutableEventGraph enabled; - public ExtendedDelta(EventGraph d, EventGraph e) { + public ExtendedDelta(MutableEventGraph d, MutableEventGraph e) { disabled = d; enabled = e; } @@ -1442,8 +1445,8 @@ public ExtendedDelta(EventGraph d, EventGraph e) { protected final class Propagator implements Definition.Visitor { private Relation source; - private EventGraph may; - private EventGraph must; + private MutableEventGraph may; + private MutableEventGraph must; public Relation getSource() { return source; @@ -1457,7 +1460,7 @@ public EventGraph getMay() { return may; } - public void setMay(EventGraph may) { + public void setMay(MutableEventGraph may) { this.may = may; } @@ -1465,7 +1468,7 @@ public EventGraph getMust() { return must; } - public void setMust(EventGraph must) { + public void setMust(MutableEventGraph must) { this.must = must; } @@ -1481,15 +1484,15 @@ public Delta visitUnion(Union union) { public Delta visitIntersection(Intersection inter) { final List operands = inter.getOperands(); if (operands.contains(source)) { - EventGraph maySet = operands.stream() - .map(r -> source.equals(r) ? may : getKnowledge(r).getMaySet()) - .sorted(Comparator.comparingInt(EventGraph::size)) - .reduce(EventGraph::intersection) + MutableEventGraph maySet = operands.stream() + .map(r -> source.equals(r) ? may : getMutableKnowledge(r).getMaySet()) + .sorted(Comparator.comparingInt(MutableEventGraph::size)) + .reduce(MutableEventGraph::intersection) .orElseThrow(); - EventGraph mustSet = operands.stream() - .map(r -> source.equals(r) ? must : getKnowledge(r).getMustSet()) - .sorted(Comparator.comparingInt(EventGraph::size)) - .reduce(EventGraph::intersection) + MutableEventGraph mustSet = operands.stream() + .map(r -> source.equals(r) ? must : getMutableKnowledge(r).getMustSet()) + .sorted(Comparator.comparingInt(MutableEventGraph::size)) + .reduce(MutableEventGraph::intersection) .orElseThrow(); return new Delta(maySet, mustSet); } @@ -1500,7 +1503,7 @@ public Delta visitIntersection(Intersection inter) { public Delta visitDifference(Difference diff) { if (diff.getMinuend().equals(source)) { Knowledge k = getKnowledge(diff.getSubtrahend()); - return new Delta(difference(may, k.getMustSet()), difference(must, k.getMaySet())); + return new Delta(MutableEventGraph.difference(may, k.getMustSet()), MutableEventGraph.difference(must, k.getMaySet())); } return Delta.EMPTY; } @@ -1509,8 +1512,8 @@ public Delta visitDifference(Difference diff) { public Delta visitComposition(Composition comp) { final Relation r1 = comp.getLeftOperand(); final Relation r2 = comp.getRightOperand(); - EventGraph maySet = new EventGraph(); - EventGraph mustSet = new EventGraph(); + MutableEventGraph maySet = new MapEventGraph(); + MutableEventGraph mustSet = new MapEventGraph(); if (r1.equals(source)) { computeComposition(maySet, may, getKnowledge(r2).getMaySet(), true); computeComposition(mustSet, must, getKnowledge(r2).getMustSet(), false); @@ -1522,7 +1525,7 @@ public Delta visitComposition(Composition comp) { return new Delta(maySet, mustSet); } - private void computeComposition(EventGraph result, EventGraph left, EventGraph right, final boolean isMay) { + private void computeComposition(MutableEventGraph result, EventGraph left, EventGraph right, final boolean isMay) { for (Event e1 : left.getDomain()) { Set update = new HashSet<>(); for (Event e : left.getRange(e1)) { @@ -1541,9 +1544,9 @@ private void computeComposition(EventGraph result, EventGraph left, EventGraph r @Override public Delta visitDomainIdentity(DomainIdentity domId) { if (domId.getOperand().equals(source)) { - EventGraph maySet = new EventGraph(); + MutableEventGraph maySet = new MapEventGraph(); may.getDomain().forEach(e -> maySet.add(e, e)); - EventGraph mustSet = new EventGraph(); + MutableEventGraph mustSet = new MapEventGraph(); must.apply((e1, e2) -> { if (exec.isImplied(e1, e2)) { mustSet.add(e1, e1); @@ -1557,9 +1560,9 @@ public Delta visitDomainIdentity(DomainIdentity domId) { @Override public Delta visitRangeIdentity(RangeIdentity rangeId) { if (rangeId.getOperand().equals(source)) { - EventGraph maySet = new EventGraph(); + MutableEventGraph maySet = new MapEventGraph(); may.getRange().forEach(e -> maySet.add(e, e)); - EventGraph mustSet = new EventGraph(); + MutableEventGraph mustSet = new MapEventGraph(); must.apply((e1, e2) -> { if (exec.isImplied(e2, e1)) { mustSet.add(e2, e2); @@ -1582,25 +1585,42 @@ public Delta visitInverse(Inverse inv) { public Delta visitTransitiveClosure(TransitiveClosure trans) { final Relation rel = trans.getDefinedRelation(); if (trans.getOperand().equals(source)) { - EventGraph maySet = computeTransitiveClosure(getKnowledge(rel).getMaySet(), may, true); - EventGraph mustSet = computeTransitiveClosure(getKnowledge(rel).getMustSet(), must, false); + MutableEventGraph maySet = computeTransitiveClosure(getKnowledge(rel).getMaySet(), may, true); + MutableEventGraph mustSet = computeTransitiveClosure(getKnowledge(rel).getMustSet(), must, false); return new Delta(maySet, mustSet); } return Delta.EMPTY; } - private EventGraph computeTransitiveClosure(EventGraph oldOuter, EventGraph inner, boolean isMay) { - EventGraph outer = new EventGraph(oldOuter); - EventGraph update = inner.filter(outer::add); - EventGraph updateComposition = new EventGraph(); + private MutableEventGraph computeTransitiveClosure(EventGraph oldOuter, MutableEventGraph inner, boolean isMay) { + MutableEventGraph outer = MapEventGraph.from(oldOuter); + MutableEventGraph update = inner.filter(outer::add); + MutableEventGraph updateComposition = new MapEventGraph(); computeComposition(updateComposition, inner, oldOuter, isMay); update.addAll(updateComposition.filter(outer::add)); while (!update.isEmpty()) { - EventGraph t = new EventGraph(); + MutableEventGraph t = new MapEventGraph(); computeComposition(t, inner, update, isMay); update = t.filter(outer::add); } return outer; } } + + protected static class MutableKnowledge extends Knowledge { + + protected MutableKnowledge(MutableEventGraph maySet, MutableEventGraph mustSet) { + super(maySet, mustSet); + } + + @Override + public MutableEventGraph getMaySet() { + return (MutableEventGraph) may; + } + + @Override + public MutableEventGraph getMustSet() { + return (MutableEventGraph) must; + } + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java index 3649ded132..0d4b98d924 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java @@ -8,7 +8,7 @@ import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.wmm.Relation; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; @@ -16,7 +16,9 @@ import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; -import java.util.*; +import java.util.List; +import java.util.Map; +import java.util.Set; import static com.dat3m.dartagnan.configuration.OptionNames.*; import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; @@ -43,19 +45,21 @@ public interface RelationAnalysis { */ static RelationAnalysis fromConfig(VerificationTask task, Context context, Configuration config) throws InvalidConfigurationException { RelationAnalysis.Config c = new RelationAnalysis.Config(config); - logger.info("Selected relation analysis: {}", c.method); - RelationAnalysis a = switch (c.method) { case NONE -> CoarseRelationAnalysis.fromConfig(task, context, config); case NATIVE -> NativeRelationAnalysis.fromConfig(task, context, config); + case LAZY -> LazyRelationAnalysis.fromConfig(task, context, config); }; - final StringBuilder configSummary = new StringBuilder().append("\n"); - configSummary.append("\t").append(RELATION_ANALYSIS).append(": ").append(c.method).append("\n"); - configSummary.append("\t").append(ENABLE_EXTENDED_RELATION_ANALYSIS).append(": ").append(c.enableExtended); - logger.info(configSummary); + if (logger.isInfoEnabled()) { + logger.info("Selected relation analysis: {}", c.method); + final StringBuilder configSummary = new StringBuilder().append("\n"); + configSummary.append("\t").append(RELATION_ANALYSIS).append(": ").append(c.method).append("\n"); + configSummary.append("\t").append(ENABLE_EXTENDED_RELATION_ANALYSIS).append(": ").append(c.enableExtended); + logger.info(configSummary); + } - if (c.enableExtended && c.method == RelationAnalysisMethod.NONE) { + if (c.enableExtended && (c.method == RelationAnalysisMethod.NONE || c.method == RelationAnalysisMethod.LAZY)) { logger.warn("{} implies {}", ENABLE_EXTENDED_RELATION_ANALYSIS, RELATION_ANALYSIS); c.enableExtended = false; } @@ -63,28 +67,37 @@ static RelationAnalysis fromConfig(VerificationTask task, Context context, Confi long t0 = System.currentTimeMillis(); a.run(); long t1 = System.currentTimeMillis(); - logger.info("Finished regular analysis in {}", Utils.toTimeString(t1 - t0)); - - final StringBuilder summary = new StringBuilder() - .append("\n======== RelationAnalysis summary ======== \n"); - summary.append("\t#Relations: ").append(task.getMemoryModel().getRelations().size()).append("\n"); - summary.append("\t#Axioms: ").append(task.getMemoryModel().getAxioms().size()).append("\n"); + final StringBuilder summary = new StringBuilder(); + if (logger.isInfoEnabled()) { + logger.info("Finished regular analysis in {}", Utils.toTimeString(t1 - t0)); + summary.append("\n======== RelationAnalysis summary ======== \n"); + summary.append("\t#Relations: ").append(task.getMemoryModel().getRelations().size()).append("\n"); + summary.append("\t#Axioms: ").append(task.getMemoryModel().getAxioms().size()).append("\n"); + } if (c.enableExtended) { - long mayCount = a.countMaySet(); - long mustCount = a.countMustSet(); + long mayCount = -1; + long mustCount = -1; + if (logger.isInfoEnabled()) { + mayCount = a.countMaySet(); + mustCount = a.countMustSet(); + } a.runExtended(); - logger.info("Finished extended analysis in {}", Utils.toTimeString(System.currentTimeMillis() - t1)); - summary.append("\t#may-edges removed (extended): ").append(mayCount - a.countMaySet()).append("\n"); - summary.append("\t#must-edges added (extended): ").append(a.countMustSet() - mustCount).append("\n"); + if (logger.isInfoEnabled()) { + logger.info("Finished extended analysis in {}", Utils.toTimeString(System.currentTimeMillis() - t1)); + summary.append("\t#may-edges removed (extended): ").append(mayCount - a.countMaySet()).append("\n"); + summary.append("\t#must-edges added (extended): ").append(a.countMustSet() - mustCount).append("\n"); + } + } + if (logger.isInfoEnabled()) { + Knowledge rf = a.getKnowledge(task.getMemoryModel().getRelation(RF)); + Knowledge co = a.getKnowledge(task.getMemoryModel().getRelation(CO)); + summary.append("\ttotal #must|may|exclusive edges: ") + .append(a.countMustSet()).append("|").append(a.countMaySet()).append("|").append(a.getContradictions().size()).append("\n"); + summary.append("\t#must|may rf edges: ").append(rf.must.size()).append("|").append(rf.may.size()).append("\n"); + summary.append("\t#must|may co edges: ").append(co.must.size()).append("|").append(co.may.size()).append("\n"); + summary.append("==========================================="); + logger.info(summary); } - Knowledge rf = a.getKnowledge(task.getMemoryModel().getRelation(RF)); - Knowledge co = a.getKnowledge(task.getMemoryModel().getRelation(CO)); - summary.append("\ttotal #must|may|exclusive edges: ") - .append(a.countMustSet()).append("|").append(a.countMaySet()).append("|").append(a.getContradictions().size()).append("\n"); - summary.append("\t#must|may rf edges: ").append(rf.must.size()).append("|").append(rf.may.size()).append("\n"); - summary.append("\t#must|may co edges: ").append(co.must.size()).append("|").append(co.may.size()).append("\n"); - summary.append("==========================================="); - logger.info(summary); return a; } @@ -161,9 +174,9 @@ There is also a symmetric case where co(w3, w1) is impossible and co(w3, w2) is void populateQueue(Map> queue, Set relations); - final class Knowledge { - private final EventGraph may; - private final EventGraph must; + class Knowledge { + protected final EventGraph may; + protected final EventGraph must; public Knowledge(EventGraph maySet, EventGraph mustSet) { may = checkNotNull(maySet); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclicity.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclicity.java index c30b5bf000..c09fff15b1 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclicity.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclicity.java @@ -8,8 +8,10 @@ import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; import com.dat3m.dartagnan.wmm.utils.Tuple; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -19,9 +21,6 @@ import java.util.*; -import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; -import static com.google.common.base.Preconditions.checkArgument; - public class Acyclicity extends Axiom { private static final Logger logger = LogManager.getLogger(Acyclicity.class); @@ -41,12 +40,12 @@ public Acyclicity(Relation rel) { // if the clauses {@code exec(x) implies before(x,y)} and {@code exec(z) implies before(y,z)} exist. // NOTE: Assumes that the must-set of rel+ is acyclic. private static EventGraph transitivelyDerivableMustEdges(ExecutionAnalysis exec, RelationAnalysis.Knowledge k) { - EventGraph result = new EventGraph(); + MutableEventGraph result = new MapEventGraph(); Map> map = new HashMap<>(); Map> mapInverse = new HashMap<>(); EventGraph current = k.getMustSet(); while (!current.isEmpty()) { - EventGraph next = new EventGraph(); + MutableEventGraph next = new MapEventGraph(); current.apply((x, y) -> { map.computeIfAbsent(x, e -> new HashSet<>()).add(y); mapInverse.computeIfAbsent(y, e -> new HashSet<>()).add(x); @@ -86,7 +85,7 @@ protected EventGraph getEncodeGraph(Context analysisContext) { ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); RelationAnalysis ra = analysisContext.get(RelationAnalysis.class); RelationAnalysis.Knowledge k = ra.getKnowledge(rel); - return difference(getEncodeGraph(exec, ra), k.getMustSet()); + return MutableEventGraph.difference(getEncodeGraph(exec, ra), k.getMustSet()); } public int getEncodeGraphSize(Context analysisContext) { @@ -101,7 +100,7 @@ private EventGraph getEncodeGraph(ExecutionAnalysis exec, RelationAnalysis ra) { // ====== Compute SCCs ====== DependencyGraph depGraph = DependencyGraph.from(succMap.keySet(), succMap); - final EventGraph result = new EventGraph(); + final MutableEventGraph result = new MapEventGraph(); for (Set.Node> scc : depGraph.getSCCs()) { for (DependencyGraph.Node node1 : scc) { for (DependencyGraph.Node node2 : scc) { @@ -123,7 +122,7 @@ private EventGraph getEncodeGraph(ExecutionAnalysis exec, RelationAnalysis ra) { return result; } - private void reduceWithMinSets(EventGraph encodeSet, ExecutionAnalysis exec, RelationAnalysis ra) { + private void reduceWithMinSets(MutableEventGraph encodeSet, ExecutionAnalysis exec, RelationAnalysis ra) { /* ASSUMPTION: MinSet is acyclic! IDEA: @@ -179,7 +178,7 @@ is an intermediate event b such that (a, b) and (b, c) are in must(rel)+ // Note: We reduce the transitive closure which may have more edges // that can be used to perform reduction // Approximative must-transitive reduction of minSet: - EventGraph reduct = new EventGraph(); + MutableEventGraph reduct = new MapEventGraph(); DependencyGraph depGraph = DependencyGraph.from(transMinSet.keySet(), e -> transMinSet.getOrDefault(e, Set.of())); for (DependencyGraph.Node start : depGraph.getNodes()) { Event e1 = start.getContent(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java index ca6ae71730..baa21af248 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Axiom.java @@ -5,7 +5,7 @@ import com.dat3m.dartagnan.wmm.Constraint; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.Wmm; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Emptiness.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Emptiness.java index 0d6173b7d6..fa0816bb1f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Emptiness.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Emptiness.java @@ -4,13 +4,12 @@ import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import java.util.ArrayList; import java.util.List; -import java.util.Map; public class Emptiness extends Axiom { @@ -24,8 +23,7 @@ public Emptiness(Relation rel) { @Override protected EventGraph getEncodeGraph(Context analysisContext) { - final RelationAnalysis ra = analysisContext.get(RelationAnalysis.class); - return ra.getKnowledge(rel).getMaySet(); + return analysisContext.get(RelationAnalysis.class).getKnowledge(rel).getMaySet(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/ForceEncodeAxiom.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/ForceEncodeAxiom.java index cc44c6e465..f5e3ab67fe 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/ForceEncodeAxiom.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/ForceEncodeAxiom.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; -import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Irreflexivity.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Irreflexivity.java index 17f59d2737..3e623236a1 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Irreflexivity.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Irreflexivity.java @@ -4,14 +4,13 @@ import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; -import com.dat3m.dartagnan.wmm.utils.EventGraph; import com.dat3m.dartagnan.wmm.utils.Tuple; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import java.util.ArrayList; import java.util.List; -import java.util.Map; public class Irreflexivity extends Axiom { @@ -25,8 +24,7 @@ public Irreflexivity(Relation rel) { @Override protected EventGraph getEncodeGraph(Context analysisContext) { - final RelationAnalysis ra = analysisContext.get(RelationAnalysis.class); - return ra.getKnowledge(rel).getMaySet().filter(Tuple::isLoop); + return analysisContext.get(RelationAnalysis.class).getKnowledge(rel).getMaySet().filter(Tuple::isLoop); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java deleted file mode 100644 index 91ccb8d16e..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java +++ /dev/null @@ -1,51 +0,0 @@ -package com.dat3m.dartagnan.wmm.utils; - -import com.dat3m.dartagnan.program.event.Event; - -import java.util.Collections; -import java.util.Set; -import java.util.function.BiPredicate; - -public class EmptyEventGraph extends EventGraph { - - protected static final EmptyEventGraph singleton = new EmptyEventGraph(); - - protected EmptyEventGraph() { - super(Collections.emptyMap()); - } - - @Override - public boolean add(Event e1, Event e2) { - throw new UnsupportedOperationException(); - } - - @Override - public boolean remove(Event e1, Event e2) { - return false; - } - - @Override - public boolean addAll(EventGraph other) { - throw new UnsupportedOperationException(); - } - - @Override - public boolean removeAll(EventGraph other) { - return false; - } - - @Override - public boolean retainAll(EventGraph other) { - return false; - } - - @Override - public boolean removeIf(BiPredicate f) { - return false; - } - - @Override - public boolean addRange(Event e, Set range) { - throw new UnsupportedOperationException(); - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java deleted file mode 100644 index 461e692dce..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java +++ /dev/null @@ -1,234 +0,0 @@ -package com.dat3m.dartagnan.wmm.utils; - -import com.dat3m.dartagnan.program.event.Event; - -import java.util.*; -import java.util.function.BiConsumer; -import java.util.function.BiPredicate; -import java.util.stream.Collectors; - -public class EventGraph { - - private final Map> data; - - public EventGraph() { - this.data = new HashMap<>(); - } - - public EventGraph(EventGraph other) { - this.data = new HashMap<>(); - other.data.forEach((k, v) -> this.data.put(k, new HashSet<>(v))); - } - - protected EventGraph(Map> data) { - this.data = data; - } - - public boolean isEmpty() { - return data.isEmpty(); - } - - public int size() { - return data.values().stream() - .map(Set::size) - .reduce(0, Integer::sum); - } - - public boolean contains(Event e1, Event e2) { - Set values = data.get(e1); - if (values != null) { - return values.contains(e2); - } - return false; - } - - public boolean add(Event e1, Event e2) { - return data.computeIfAbsent(e1, e -> new HashSet<>()).add(e2); - } - - public boolean remove(Event e1, Event e2) { - Set set = data.get(e1); - if (set != null && set.remove(e2)) { - if (set.isEmpty()) { - data.remove(e1); - } - return true; - } - return false; - } - - public boolean addAll(EventGraph other) { - boolean modified = false; - for (Map.Entry> otherEntry : other.data.entrySet()) { - modified |= data.computeIfAbsent(otherEntry.getKey(), x -> new HashSet<>()).addAll(otherEntry.getValue()); - } - return modified; - } - - public boolean removeAll(EventGraph other) { - boolean modified = false; - for (Map.Entry> otherEntry : other.data.entrySet()) { - Event key = otherEntry.getKey(); - Set value = data.get(key); - if (value != null) { - modified |= value.removeAll(otherEntry.getValue()); - if (value.isEmpty()) { - data.remove(key); - } - } - } - return modified; - } - - public boolean retainAll(EventGraph other) { - boolean modified = false; - Set removedKeys = new HashSet<>(); - for (Map.Entry> entry : data.entrySet()) { - Event key = entry.getKey(); - Set otherValue = other.data.get(key); - if (otherValue != null) { - Set value = entry.getValue(); - modified |= value.retainAll(otherValue); - if (value.isEmpty()) { - removedKeys.add(key); - } - } else { - modified = true; - removedKeys.add(key); - } - } - removedKeys.forEach(data::remove); - return modified; - } - - public EventGraph inverse() { - EventGraph inverse = new EventGraph(); - data.forEach((e1, value) - -> value.forEach(e2 - -> inverse.data.computeIfAbsent(e2, x -> new HashSet<>()).add(e1))); - return inverse; - } - - public EventGraph filter(BiPredicate f) { - EventGraph filtered = new EventGraph(); - data.forEach((e1, v) -> { - Set set = v.stream() - .filter(e2 -> f.test(e1, e2)) - .collect(Collectors.toCollection(HashSet::new)); - if (!set.isEmpty()) { - filtered.data.put(e1, set); - } - }); - return filtered; - } - - public Map> getOutMap() { - Map> temp = new HashMap<>(); - data.forEach((k, v) -> temp.put(k, Collections.unmodifiableSet(v))); - return Collections.unmodifiableMap(temp); - } - - public Map> getInMap() { - return inverse().getOutMap(); - } - - public Set getDomain() { - return Collections.unmodifiableSet(data.keySet()); - } - - public Set getRange() { - return data.values().stream().flatMap(Collection::stream).collect(Collectors.toUnmodifiableSet()); - } - - public Set getRange(Event e) { - return Collections.unmodifiableSet(data.getOrDefault(e, Set.of())); - } - - public boolean addRange(Event e, Set range) { - if (!range.isEmpty()) { - return data.computeIfAbsent(e, x -> new HashSet<>()).addAll(range); - } - return false; - } - - public boolean removeIf(BiPredicate f) { - boolean modified = false; - Set removedKeys = new HashSet<>(); - for (Map.Entry> entry : data.entrySet()) { - Event key = entry.getKey(); - Set value = entry.getValue(); - modified |= value.removeIf(e2 -> f.test(key, e2)); - if (value.isEmpty()) { - removedKeys.add(key); - } - } - removedKeys.forEach(data::remove); - return modified; - } - - public void apply(BiConsumer f) { - data.forEach((e1, value) -> value.forEach(e2 -> f.accept(e1, e2))); - } - - public static EventGraph union(EventGraph first, EventGraph second) { - EventGraph result = new EventGraph(); - first.data.forEach((e1, set) -> result.data.put(e1, new HashSet<>(set))); - second.data.forEach((e1, set) -> result.data.computeIfAbsent(e1, x -> new HashSet<>()).addAll(set)); - return result; - } - - public static EventGraph intersection(EventGraph first, EventGraph second) { - EventGraph result = new EventGraph(); - first.data.forEach((e1, firstSet) -> { - Set secondSet = second.data.get(e1); - if (secondSet != null) { - Set resultSet = new HashSet<>(); - if (firstSet.size() > secondSet.size()) { - resultSet.addAll(firstSet); - resultSet.retainAll(secondSet); - } else { - resultSet.addAll(secondSet); - resultSet.retainAll(firstSet); - } - if (!resultSet.isEmpty()) { - result.data.put(e1, resultSet); - } - } - }); - return result; - } - - public static EventGraph difference(EventGraph first, EventGraph second) { - EventGraph result = new EventGraph(); - first.data.forEach((e1, firstSet) -> { - Set resultSet = new HashSet<>(firstSet); - Set secondSet = second.data.get(e1); - if (secondSet != null) { - resultSet.removeAll(secondSet); - } - if (!resultSet.isEmpty()) { - result.data.put(e1, resultSet); - } - }); - return result; - } - - public static EventGraph empty() { - return EmptyEventGraph.singleton; - } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder("["); - List keys = data.keySet().stream().sorted().toList(); - for (Event e1 : keys) { - List values = data.get(e1).stream().sorted().toList(); - values.forEach(e2 -> sb.append("(") - .append(e1.getGlobalId()) - .append(",") - .append(e2.getGlobalId()) - .append(")")); - } - return sb.append("]").toString(); - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraph.java new file mode 100644 index 0000000000..7b9b880003 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraph.java @@ -0,0 +1,82 @@ +package com.dat3m.dartagnan.wmm.utils.graph; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.LazyEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; + +import java.util.Arrays; +import java.util.Map; +import java.util.Set; +import java.util.function.BiConsumer; +import java.util.function.BiPredicate; + +public interface EventGraph { + + static EventGraph empty() { + return ImmutableEventGraph.empty(); + } + + boolean isEmpty(); + + int size(); + + boolean contains(Event e1, Event e2); + + EventGraph inverse(); + + EventGraph filter(BiPredicate f); + + Map> getOutMap(); + + Map> getInMap(); + + Set getDomain(); + + Set getRange(); + + Set getRange(Event e); + + void apply(BiConsumer f); + + static EventGraph union(EventGraph... operands) { + operands = Arrays.stream(operands).filter(o -> !o.isEmpty()).toArray(EventGraph[]::new); + if (operands.length == 0) { + return empty(); + } + if (Arrays.stream(operands).anyMatch(LazyEventGraph.class::isInstance)) { + return LazyEventGraph.union(operands); + } + if (Arrays.stream(operands).anyMatch(MapEventGraph.class::isInstance)) { + return MapEventGraph.union(operands); + } + return ImmutableMapEventGraph.union(operands); + } + + static EventGraph intersection(EventGraph... operands) { + if (Arrays.stream(operands).anyMatch(EventGraph::isEmpty)) { + return empty(); + } + if (Arrays.stream(operands).allMatch(LazyEventGraph.class::isInstance)) { + return LazyEventGraph.intersection(operands); + } + if (Arrays.stream(operands).anyMatch(MapEventGraph.class::isInstance)) { + return MapEventGraph.intersection(operands); + } + return ImmutableMapEventGraph.intersection(operands); + } + + static EventGraph difference(EventGraph minuend, EventGraph subtrahend) { + if (minuend.isEmpty()) { + return empty(); + } + if (minuend instanceof LazyEventGraph) { + return LazyEventGraph.difference(minuend, subtrahend); + } + if (minuend instanceof MapEventGraph || subtrahend instanceof MapEventGraph) { + return MapEventGraph.difference(minuend, subtrahend); + } + return ImmutableMapEventGraph.difference(minuend, subtrahend); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableEventGraph.java new file mode 100644 index 0000000000..58e02df386 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableEventGraph.java @@ -0,0 +1,56 @@ +package com.dat3m.dartagnan.wmm.utils.graph.immutable; + +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; + +import java.util.Arrays; + +public interface ImmutableEventGraph extends EventGraph { + + static ImmutableEventGraph empty() { + return ImmutableMapEventGraph.empty(); + } + + static ImmutableEventGraph from(EventGraph other) { + if (other instanceof ImmutableEventGraph iOther) { + return iOther; + } + return ImmutableMapEventGraph.from(other); + } + + static ImmutableEventGraph union(EventGraph... operands) { + operands = Arrays.stream(operands).filter(o -> !o.isEmpty()).toArray(EventGraph[]::new); + if (operands.length == 0) { + return ImmutableEventGraph.empty(); + } + if (operands.length == 1) { + return ImmutableEventGraph.from(operands[0]); + } + if (Arrays.stream(operands).anyMatch(LazyEventGraph.class::isInstance)) { + return LazyEventGraph.union(operands); + } + return ImmutableMapEventGraph.union(operands); + } + + static ImmutableEventGraph intersection(EventGraph... operands) { + if (Arrays.stream(operands).anyMatch(EventGraph::isEmpty)) { + return ImmutableEventGraph.empty(); + } + if (operands.length == 1) { + return ImmutableEventGraph.from(operands[0]); + } + if (Arrays.stream(operands).allMatch(LazyEventGraph.class::isInstance)) { + return LazyEventGraph.intersection(operands); + } + return ImmutableMapEventGraph.intersection(operands); + } + + static ImmutableEventGraph difference(EventGraph minuend, EventGraph subtrahend) { + if (minuend.isEmpty() || subtrahend.isEmpty()) { + return ImmutableEventGraph.from(minuend); + } + if (minuend instanceof LazyEventGraph) { + return LazyEventGraph.difference(minuend, subtrahend); + } + return ImmutableMapEventGraph.difference(minuend, subtrahend); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableMapEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableMapEventGraph.java new file mode 100644 index 0000000000..03a55d3a36 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableMapEventGraph.java @@ -0,0 +1,225 @@ +package com.dat3m.dartagnan.wmm.utils.graph.immutable; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.google.common.collect.ImmutableMap; +import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Sets; + +import java.util.*; +import java.util.concurrent.ConcurrentHashMap; +import java.util.function.BiConsumer; +import java.util.function.BiPredicate; +import java.util.stream.Collectors; + +public class ImmutableMapEventGraph implements ImmutableEventGraph { + + private final Map> data; + private final int size; + private ImmutableMapEventGraph inverse; + + public ImmutableMapEventGraph(Map> data) { + this(data, data.values().stream().map(Set::size).reduce(0, Integer::sum)); + } + + private ImmutableMapEventGraph(Map> data, int size) { + this.data = data.entrySet().stream() + .filter(e -> !e.getValue().isEmpty()) + .collect(ImmutableMap.toImmutableMap( + Map.Entry::getKey, + entry -> entry.getValue() instanceof ImmutableSet + ? entry.getValue() + : ImmutableSet.copyOf(entry.getValue()))); + this.size = size; + } + + public static ImmutableEventGraph empty() { + return EmptyEventGraph.instance; + } + + @Override + public boolean isEmpty() { + return size == 0; + } + + @Override + public int size() { + return size; + } + + @Override + public boolean contains(Event e1, Event e2) { + Set values = data.get(e1); + if (values != null) { + return values.contains(e2); + } + return false; + } + + @Override + public ImmutableMapEventGraph inverse() { + if (inverse == null) { + Map> invData = new HashMap<>(); + data.forEach((e1, value) -> value.forEach(e2 -> invData.computeIfAbsent(e2, x -> new HashSet<>()).add(e1))); + inverse = new ImmutableMapEventGraph(invData, size); + inverse.inverse = this; + } + return inverse; + } + + @Override + public ImmutableMapEventGraph filter(BiPredicate f) { + Map> filteredData = new ConcurrentHashMap<>(); + data.keySet().stream().unordered().parallel() + .forEach(e1 -> filteredData.put(e1, data.get(e1).stream() + .filter(e2 -> f.test(e1, e2)) + .collect(ImmutableSet.toImmutableSet()))); + return new ImmutableMapEventGraph(filteredData); + } + + @Override + public Map> getOutMap() { + return data; + } + + @Override + public Map> getInMap() { + return inverse().getOutMap(); + } + + @Override + public Set getDomain() { + return data.keySet(); + } + + @Override + public Set getRange() { + return inverse().getDomain(); + } + + @Override + public Set getRange(Event e) { + return data.getOrDefault(e, Set.of()); + } + + @Override + public void apply(BiConsumer f) { + data.forEach((e1, value) -> value.forEach(e2 -> f.accept(e1, e2))); + } + + @Override + public boolean equals(Object o) { + if (this == o) + return true; + if (!(o instanceof EventGraph eg)) + return false; + if (!(o instanceof ImmutableMapEventGraph that)) + return data.equals(eg.getOutMap()); + return Objects.equals(data, that.data); + } + + @Override + public int hashCode() { + throw new UnsupportedOperationException(ImmutableMapEventGraph.class.getSimpleName() + + " should not be used as a key"); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder("["); + for (Event e1 : data.keySet().stream().sorted().toList()) { + for (Event e2 : data.get(e1).stream().sorted().toList()) { + sb.append("(") + .append(e1.getGlobalId()) + .append(",") + .append(e2.getGlobalId()) + .append(")"); + } + } + return sb.append("]").toString(); + } + + public static ImmutableMapEventGraph from(EventGraph other) { + if (other.isEmpty()) { + return EmptyEventGraph.instance; + } + if (other instanceof ImmutableMapEventGraph iOther) { + return iOther; + } + if (other instanceof LazyEventGraph || other instanceof MapEventGraph) { + return new ImmutableMapEventGraph(other.getOutMap()); + } + throw new IllegalArgumentException("Unexpected type of event graph " + other.getClass().getSimpleName()); + } + + public static ImmutableMapEventGraph union(EventGraph... operands) { + EventGraph[] nonEmptyOperands = Arrays.stream(operands).filter(o -> !o.isEmpty()).toArray(EventGraph[]::new); + if (nonEmptyOperands.length == 0) { + return EmptyEventGraph.instance; + } + if (nonEmptyOperands.length == 1) { + return ImmutableMapEventGraph.from(nonEmptyOperands[0]); + } + Set domain = Arrays.stream(nonEmptyOperands) + .flatMap(eg -> eg.getDomain().stream()) + .collect(Collectors.toSet()); + Map> data = new ConcurrentHashMap<>(); + domain.stream().unordered().parallel() + .forEach(e1 -> data.put(e1, Arrays.stream(nonEmptyOperands) + .flatMap(eg -> eg.getRange(e1).stream()) + .collect(ImmutableSet.toImmutableSet()))); + return new ImmutableMapEventGraph(data); + } + + public static ImmutableMapEventGraph intersection(EventGraph... operands) { + if (Arrays.stream(operands).anyMatch(EventGraph::isEmpty)) { + return EmptyEventGraph.instance; + } + if (operands.length == 1) { + return ImmutableMapEventGraph.from(operands[0]); + } + Set domain = Arrays.stream(operands) + .map(EventGraph::getDomain) + .sorted(Comparator.comparing(Set::size)) + .reduce(Sets::intersection) + .orElseThrow(); + Map> data = new ConcurrentHashMap<>(); + domain.stream().unordered().parallel() + .forEach(e1 -> data.put(e1, Arrays.stream(operands) + .map(eg -> eg.getRange(e1)) + .sorted(Comparator.comparing(Set::size)) + .reduce(Sets::intersection) + .orElseThrow())); + return new ImmutableMapEventGraph(data); + } + + public static ImmutableMapEventGraph difference(EventGraph minuend, EventGraph subtrahend) { + if (minuend.isEmpty() || subtrahend.isEmpty()) { + ImmutableMapEventGraph.from(minuend); + } + Map> data = new ConcurrentHashMap<>(); + minuend.getDomain().stream().unordered().parallel() + .forEach(e1 -> data.put(e1, Sets.difference(minuend.getRange(e1), subtrahend.getRange(e1)))); + return new ImmutableMapEventGraph(data); + } + + public static class EmptyEventGraph extends ImmutableMapEventGraph { + + private static final EmptyEventGraph instance = new EmptyEventGraph(); + + private EmptyEventGraph() { + super(Map.of()); + } + + @Override + public EmptyEventGraph filter(BiPredicate f) { + return this; + } + + @Override + public EmptyEventGraph inverse() { + return this; + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/LazyEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/LazyEventGraph.java new file mode 100644 index 0000000000..b4cc1c6a0f --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/LazyEventGraph.java @@ -0,0 +1,259 @@ +package com.dat3m.dartagnan.wmm.utils.graph.immutable; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.google.common.collect.ImmutableMap; +import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Sets; + +import java.util.*; +import java.util.function.BiConsumer; +import java.util.function.BiPredicate; + +public class LazyEventGraph implements ImmutableEventGraph { + + private final Set domain; + private final Set range; + private final BiPredicate function; + private final boolean empty; + private int size = -1; + + public LazyEventGraph(Set domain, Set range, + BiPredicate function) { + this.domain = ImmutableSet.copyOf(domain); + this.range = ImmutableSet.copyOf(range); + this.function = function; + this.empty = domain.stream().noneMatch(e1 -> range.stream().anyMatch((e2 -> function.test(e1, e2)))); + } + + public BiPredicate getFunction() { + return function; + } + + @Override + public boolean isEmpty() { + return empty; + } + + @Override + public int size() { + if (size == -1) { + size = domain.stream() + .map(e1 -> range.stream().filter(e2 -> function.test(e1, e2)).count()) + .map(s -> Integer.parseInt(s.toString())) + .reduce(0, Integer::sum); + } + return size; + } + + @Override + public boolean contains(Event e1, Event e2) { + return domain.contains(e1) && range.contains(e2) && function.test(e1, e2); + } + + @Override + public LazyEventGraph inverse() { + return new LazyEventGraph(range, domain, (e1, e2) -> function.test(e2, e1)); + } + + @Override + public LazyEventGraph filter(BiPredicate f) { + Set newDomain = domain.stream().unordered().parallel() + .filter(e1 -> range.stream().anyMatch(e2 -> function.test(e1, e2) && f.test(e1, e2))) + .collect(ImmutableSet.toImmutableSet()); + Set newRange = range.stream().unordered().parallel() + .filter(e2 -> domain.stream().anyMatch(e1 -> function.test(e1, e2) && f.test(e1, e2))) + .collect(ImmutableSet.toImmutableSet()); + return new LazyEventGraph(newDomain, newRange, (e1, e2) -> function.test(e1, e2) && f.test(e1, e2)); + } + + @Override + public Map> getOutMap() { + ImmutableMap.Builder> builder = new ImmutableMap.Builder<>(); + for (Event e1 : domain) { + Set set = range.stream() + .filter(e2 -> function.test(e1, e2)) + .collect(ImmutableSet.toImmutableSet()); + if (!set.isEmpty()) { + builder.put(e1, set); + } + } + return builder.build(); + } + + @Override + public Map> getInMap() { + return inverse().getOutMap(); + } + + @Override + public Set getDomain() { + return domain; + } + + @Override + public Set getRange() { + return range; + } + + @Override + public Set getRange(Event e1) { + if (domain.contains(e1)) { + return range.stream() + .filter(e2 -> function.test(e1, e2)) + .collect(ImmutableSet.toImmutableSet()); + } + return Set.of(); + } + + @Override + public void apply(BiConsumer f) { + for (Event e1 : domain) { + for (Event e2 : range) { + if (function.test(e1, e2)) { + f.accept(e1, e2); + } + } + } + } + + @Override + public boolean equals(Object o) { + if (this == o) + return true; + if (!(o instanceof EventGraph eg)) + return false; + if (!(o instanceof LazyEventGraph that)) + return getOutMap().equals(eg.getOutMap()); + return Objects.equals(domain, that.domain) + && Objects.equals(range, that.range) + && Objects.equals(function, that.function); + } + + @Override + public int hashCode() { + throw new UnsupportedOperationException(LazyEventGraph.class.getSimpleName() + + " should not be used as a key"); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder("["); + for (Event e1 : domain.stream().sorted().toList()) { + for (Event e2 : range.stream().sorted().toList()) { + if (function.test(e1, e2)) { + sb.append("(") + .append(e1.getGlobalId()) + .append(",") + .append(e2.getGlobalId()) + .append(")"); + } + } + } + return sb.append("]").toString(); + } + + public static LazyEventGraph empty() { + return EmptyEventGraph.instance; + } + + public static LazyEventGraph from(EventGraph other) { + if (other.isEmpty()) { + return EmptyEventGraph.instance; + } + if (other instanceof LazyEventGraph iOther) { + return iOther; + } + if (other instanceof ImmutableMapEventGraph) { + return new LazyEventGraph(other.getDomain(), other.getRange(), other::contains); + } + if (other instanceof MapEventGraph) { + return LazyEventGraph.from(ImmutableMapEventGraph.from(other)); + } + throw new IllegalArgumentException("Unexpected type of event graph " + other.getClass().getSimpleName()); + } + + public static LazyEventGraph union(EventGraph... operands) { + operands = Arrays.stream(operands).filter(o -> !o.isEmpty()).toArray(EventGraph[]::new); + if (operands.length == 0) { + return EmptyEventGraph.instance; + } + if (operands.length == 1) { + return LazyEventGraph.from(operands[0]); + } + List iOperands = Arrays.stream(operands).map(ImmutableEventGraph::from).toList(); + BiPredicate function = (e1, e2) -> iOperands.stream().anyMatch(o -> o.contains(e1, e2)); + Set domain = iOperands.stream().unordered().parallel() + .flatMap(o -> o.getDomain().stream()) + .collect(ImmutableSet.toImmutableSet()); + Set range = iOperands.stream().unordered().parallel() + .flatMap(o -> o.getRange().stream()) + .collect(ImmutableSet.toImmutableSet()); + return new LazyEventGraph(domain, range, function); + } + + public static LazyEventGraph intersection(EventGraph... operands) { + if (Arrays.stream(operands).anyMatch(EventGraph::isEmpty)) { + return EmptyEventGraph.instance; + } + if (operands.length == 1) { + return LazyEventGraph.from(operands[0]); + } + List iOperands = Arrays.stream(operands).map(ImmutableEventGraph::from).toList(); + BiPredicate function = (e1, e2) -> iOperands.stream().allMatch(o -> o.contains(e1, e2)); + Set baseDomain = iOperands.stream().unordered().parallel() + .map(EventGraph::getDomain) + .sorted(Comparator.comparing(Set::size)) + .reduce(Sets::intersection) + .orElseThrow(); + Set range = iOperands.stream().unordered().parallel() + .map(EventGraph::getRange) + .sorted(Comparator.comparing(Set::size)) + .reduce(Sets::intersection) + .orElseThrow() + .stream() + .filter(e2 -> baseDomain.stream().anyMatch(e1 -> function.test(e1, e2))) + .collect(ImmutableSet.toImmutableSet()); + Set domain = baseDomain.stream().unordered().parallel() + .filter(e1 -> range.stream().anyMatch(e2 -> function.test(e1, e2))) + .collect(ImmutableSet.toImmutableSet()); + return new LazyEventGraph(domain, range, function); + } + + public static LazyEventGraph difference(EventGraph minuend, EventGraph subtrahend) { + if (minuend.isEmpty() || subtrahend.isEmpty()) { + LazyEventGraph.from(minuend); + } + ImmutableEventGraph iMinuend = ImmutableEventGraph.from(minuend); + ImmutableEventGraph iSubtrahend = ImmutableEventGraph.from(subtrahend); + BiPredicate function = (e1, e2) -> iMinuend.contains(e1, e2) && !iSubtrahend.contains(e1, e2); + Set baseRange = iMinuend.getRange(); + Set domain = iMinuend.getDomain().stream().unordered().parallel() + .filter(e1 -> baseRange.stream().anyMatch(e2 -> function.test(e1, e2))) + .collect(ImmutableSet.toImmutableSet()); + Set range = baseRange.stream().unordered().parallel() + .filter(e2 -> domain.stream().anyMatch(e1 -> function.test(e1, e2))) + .collect(ImmutableSet.toImmutableSet()); + return new LazyEventGraph(domain, range, function); + } + + public static class EmptyEventGraph extends LazyEventGraph { + + private static final EmptyEventGraph instance = new EmptyEventGraph(); + + private EmptyEventGraph() { + super(Set.of(), Set.of(), (e1, e2) -> false); + } + + @Override + public EmptyEventGraph filter(BiPredicate f) { + return this; + } + + @Override + public EmptyEventGraph inverse() { + return this; + } + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MapEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MapEventGraph.java new file mode 100644 index 0000000000..73477f4fef --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MapEventGraph.java @@ -0,0 +1,303 @@ +package com.dat3m.dartagnan.wmm.utils.graph.mutable; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; + +import java.util.*; +import java.util.function.BiConsumer; +import java.util.function.BiPredicate; +import java.util.stream.Collectors; + +public class MapEventGraph implements MutableEventGraph { + + private final Map> data; + + public MapEventGraph() { + this.data = new HashMap<>(); + } + + public MapEventGraph(Map> data) { + this.data = new HashMap<>(); + data.forEach((e1, value) -> { + if (!value.isEmpty()) { + this.data.put(e1, new HashSet<>(value)); + } + }); + } + + @Override + public boolean isEmpty() { + return data.isEmpty(); + } + + @Override + public int size() { + return data.values().stream() + .map(Set::size) + .reduce(0, Integer::sum); + } + + @Override + public boolean contains(Event e1, Event e2) { + Set values = data.get(e1); + if (values != null) { + return values.contains(e2); + } + return false; + } + + @Override + public boolean add(Event e1, Event e2) { + return data.computeIfAbsent(e1, e -> new HashSet<>()).add(e2); + } + + @Override + public boolean remove(Event e1, Event e2) { + Set set = data.get(e1); + if (set != null && set.remove(e2)) { + if (set.isEmpty()) { + data.remove(e1); + } + return true; + } + return false; + } + + @Override + public boolean addAll(EventGraph other) { + boolean modified = false; + Map> copy = other instanceof MapEventGraph mOther ? mOther.data : other.getOutMap(); + for (Map.Entry> entry : copy.entrySet()) { + modified |= data.computeIfAbsent(entry.getKey(), x -> new HashSet<>()).addAll(entry.getValue()); + } + return modified; + } + + @Override + public boolean removeAll(EventGraph other) { + boolean modified = false; + Map> copy = other instanceof MapEventGraph mOther ? mOther.data : other.getOutMap(); + for (Map.Entry> entry : copy.entrySet()) { + Event key = entry.getKey(); + Set value = data.get(key); + if (value != null) { + modified |= value.removeAll(entry.getValue()); + if (value.isEmpty()) { + data.remove(key); + } + } + } + return modified; + } + + @Override + public boolean retainAll(EventGraph other) { + boolean modified = false; + Map> copy = other instanceof MapEventGraph mOther ? mOther.data : other.getOutMap(); + Set removedKeys = new HashSet<>(); + for (Map.Entry> entry : data.entrySet()) { + Event key = entry.getKey(); + Set otherValue = copy.get(key); + if (otherValue != null) { + Set value = entry.getValue(); + modified |= value.retainAll(otherValue); + if (value.isEmpty()) { + removedKeys.add(key); + } + } else { + modified = true; + removedKeys.add(key); + } + } + removedKeys.forEach(data::remove); + return modified; + } + + @Override + public MapEventGraph inverse() { + MapEventGraph inverse = new MapEventGraph(); + data.forEach((e1, value) + -> value.forEach(e2 + -> inverse.data.computeIfAbsent(e2, x -> new HashSet<>()).add(e1))); + return inverse; + } + + @Override + public MapEventGraph filter(BiPredicate f) { + MapEventGraph filtered = new MapEventGraph(); + data.forEach((e1, v) -> { + Set set = v.stream() + .filter(e2 -> f.test(e1, e2)) + .collect(Collectors.toCollection(HashSet::new)); + if (!set.isEmpty()) { + filtered.data.put(e1, set); + } + }); + return filtered; + } + + @Override + public Map> getOutMap() { + Map> outMap = new HashMap<>(); + data.forEach((k, v) -> outMap.put(k, Collections.unmodifiableSet(v))); + return Collections.unmodifiableMap(outMap); + } + + @Override + public Map> getInMap() { + return inverse().getOutMap(); + } + + @Override + public Set getDomain() { + return Collections.unmodifiableSet(data.keySet()); + } + + @Override + public Set getRange() { + return data.values().stream().flatMap(Collection::stream).collect(Collectors.toUnmodifiableSet()); + } + + @Override + public Set getRange(Event e) { + return Collections.unmodifiableSet(data.getOrDefault(e, Set.of())); + } + + @Override + public boolean addRange(Event e, Set range) { + if (!range.isEmpty()) { + return data.computeIfAbsent(e, x -> new HashSet<>()).addAll(range); + } + return false; + } + + @Override + public boolean removeIf(BiPredicate f) { + boolean modified = false; + Set removedKeys = new HashSet<>(); + for (Map.Entry> entry : data.entrySet()) { + Event key = entry.getKey(); + Set value = entry.getValue(); + modified |= value.removeIf(e2 -> f.test(key, e2)); + if (value.isEmpty()) { + removedKeys.add(key); + } + } + removedKeys.forEach(data::remove); + return modified; + } + + @Override + public void apply(BiConsumer f) { + data.forEach((e1, value) -> value.forEach(e2 -> f.accept(e1, e2))); + } + + @Override + public boolean equals(Object o) { + if (this == o) + return true; + if (!(o instanceof EventGraph eg)) + return false; + if (!(o instanceof MapEventGraph that)) + return data.equals(eg.getOutMap()); + return Objects.equals(data, that.data); + } + + @Override + public int hashCode() { + throw new UnsupportedOperationException(MapEventGraph.class.getSimpleName() + + " should not be used as a key"); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder("["); + for (Event e1 : data.keySet().stream().sorted().toList()) { + for (Event e2 : data.get(e1).stream().sorted().toList()) { + sb.append("(") + .append(e1.getGlobalId()) + .append(",") + .append(e2.getGlobalId()) + .append(")"); + } + } + return sb.append("]").toString(); + } + + public static MapEventGraph from(EventGraph other) { + MapEventGraph newInstance = new MapEventGraph(); + newInstance.addAll(other); + return newInstance; + } + + public static MapEventGraph union(EventGraph... operands) { + operands = Arrays.stream(operands).filter(o -> !o.isEmpty()).toArray(EventGraph[]::new); + if (operands.length == 0) { + return new MapEventGraph(); + } + if (operands.length == 1) { + return MapEventGraph.from(operands[0]); + } + List>> maps = Arrays.stream(operands).unordered().parallel() + .map(MapEventGraph::getOtherMap) + .toList(); + MapEventGraph result = new MapEventGraph(); + maps.stream().flatMap(m -> m.keySet().stream()) + .collect(Collectors.toSet()) + .forEach(e1 -> result.data.put(e1, maps.stream() + .flatMap(m -> m.getOrDefault(e1, Set.of()).stream()) + .collect(Collectors.toCollection(HashSet::new)))); + return result; + } + + public static MapEventGraph intersection(EventGraph... operands) { + if (Arrays.stream(operands).anyMatch(EventGraph::isEmpty)) { + return new MapEventGraph(); + } + if (operands.length == 1) { + return MapEventGraph.from(operands[0]); + } + List>> maps = Arrays.stream(operands).unordered().parallel() + .map(MapEventGraph::getOtherMap) + .toList(); + MapEventGraph result = new MapEventGraph(); + setIntersection(maps.stream().map(Map::keySet).toList()).forEach(e1 -> { + Set range = setIntersection(maps.stream().map(m -> m.get(e1)).toList()); + if (!range.isEmpty()) { + result.data.put(e1, range); + } + }); + return result; + } + + public static MapEventGraph difference(EventGraph minuend, EventGraph subtrahend) { + MapEventGraph result = new MapEventGraph(); + Map> subtrahendMap = getOtherMap(subtrahend); + getOtherMap(minuend).forEach((e1, range) -> { + Set copyRange = new HashSet<>(range); + if (subtrahendMap.containsKey(e1)) { + copyRange.removeAll(subtrahendMap.get(e1)); + } + if (!copyRange.isEmpty()) { + result.data.put(e1, copyRange); + } + }); + return result; + } + + private static Set setIntersection(Collection> data) { + List> sorted = data.stream().sorted(Comparator.comparing(Set::size)).toList(); + Set result = new HashSet<>(sorted.get(0)); + for (int i = 1; i < sorted.size(); i++) { + result.retainAll(sorted.get(i)); + } + return result; + } + + private static Map> getOtherMap(EventGraph other) { + if (other instanceof MapEventGraph mapOther) { + return mapOther.data; + } + return other.getOutMap(); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraph.java new file mode 100644 index 0000000000..4adae5e029 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraph.java @@ -0,0 +1,46 @@ +package com.dat3m.dartagnan.wmm.utils.graph.mutable; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; + +import java.util.Set; +import java.util.function.BiPredicate; + +public interface MutableEventGraph extends EventGraph { + + @Override + MutableEventGraph inverse(); + + @Override + MutableEventGraph filter(BiPredicate f); + + boolean add(Event e1, Event e2); + + boolean remove(Event e1, Event e2); + + boolean addAll(EventGraph other); + + boolean removeAll(EventGraph other); + + boolean retainAll(EventGraph other); + + boolean addRange(Event e, Set range); + + boolean removeIf(BiPredicate f); + + static MutableEventGraph from(EventGraph other) { + return MapEventGraph.from(other); + } + + static MutableEventGraph union(EventGraph... operands) { + return MapEventGraph.union(operands); + } + + static MutableEventGraph intersection(EventGraph... operands) { + return MapEventGraph.intersection(operands); + } + + static MutableEventGraph difference(EventGraph minuend, EventGraph subtrahend) { + return MapEventGraph.difference(minuend, subtrahend); + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java new file mode 100644 index 0000000000..e83f0644fc --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java @@ -0,0 +1,185 @@ +package com.dat3m.dartagnan.encoding; + +import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.RelationAnalysisMethod; +import com.dat3m.dartagnan.parsers.cat.ParserCat; +import com.dat3m.dartagnan.parsers.program.ProgramParser; +import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.verification.Context; +import com.dat3m.dartagnan.verification.VerificationTask; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.Wmm; +import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.api.SolverContext; + +import java.io.File; +import java.io.IOException; +import java.nio.file.DirectoryStream; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.*; + +import static com.dat3m.dartagnan.configuration.Alias.FIELD_SENSITIVE; +import static com.dat3m.dartagnan.configuration.OptionNames.*; +import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; +import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; +import static com.dat3m.dartagnan.verification.solving.ModelChecker.*; +import static org.junit.Assert.assertEquals; +import static org.sosy_lab.java_smt.SolverContextFactory.createSolverContext; + +@RunWith(Parameterized.class) +public class RelationAnalysisTest { + + private final String testPath; + private final String modelPath; + private final Arch target; + + public RelationAnalysisTest(String testPath, String modelPath, Arch target) { + this.testPath = testPath; + this.modelPath = modelPath; + this.target = target; + } + + @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}") + public static Iterable data() throws IOException { + return Arrays.asList(new Object[][]{ + { "litmus/AARCH64", "cat/aarch64.cat", Arch.ARM8 }, + { "litmus/C11", "cat/c11.cat", Arch.C11 }, + { "litmus/PTX/Manual", "cat/ptx-v7.5.cat", Arch.PTX }, + { "litmus/PTX/Memalloy", "cat/ptx-v7.5.cat", Arch.PTX }, + { "litmus/PTX/Nvidia", "cat/ptx-v7.5.cat", Arch.PTX }, + { "litmus/VULKAN/Data-Race", "cat/spirv.cat", Arch.VULKAN }, + { "litmus/VULKAN/Kronos-Group", "cat/spirv.cat", Arch.VULKAN }, + { "litmus/VULKAN/Manual", "cat/spirv.cat", Arch.VULKAN }, + { "litmus/X86", "cat/tso.cat", Arch.TSO }, + + { "dartagnan/src/test/resources/lfds", "cat/c11.cat", Arch.C11 }, + { "dartagnan/src/test/resources/locks", "cat/c11.cat", Arch.C11 }, + { "dartagnan/src/test/resources/libvsync", "cat/c11.cat", Arch.C11 }, + { "dartagnan/src/test/resources/miscellaneous", "cat/c11.cat", Arch.C11 }, + + { "dartagnan/src/test/resources/lfds", "cat/imm.cat", Arch.C11 }, + { "dartagnan/src/test/resources/locks", "cat/imm.cat", Arch.C11 }, + { "dartagnan/src/test/resources/libvsync", "cat/imm.cat", Arch.C11 }, + { "dartagnan/src/test/resources/miscellaneous", "cat/imm.cat", Arch.C11 }, + + { "dartagnan/src/test/resources/lfds", "cat/vmm.cat", Arch.C11 }, + { "dartagnan/src/test/resources/locks", "cat/vmm.cat", Arch.C11 }, + { "dartagnan/src/test/resources/libvsync", "cat/vmm.cat", Arch.C11 }, + { "dartagnan/src/test/resources/miscellaneous", "cat/vmm.cat", Arch.C11 }, + + { "dartagnan/src/test/resources/lfds", "cat/rc11.cat", Arch.C11 }, + { "dartagnan/src/test/resources/locks", "cat/rc11.cat", Arch.C11 }, + { "dartagnan/src/test/resources/libvsync", "cat/rc11.cat", Arch.C11 }, + { "dartagnan/src/test/resources/miscellaneous", "cat/rc11.cat", Arch.C11 }, + + { "dartagnan/src/test/resources/lfds", "cat/aarch64.cat", Arch.ARM8 }, + { "dartagnan/src/test/resources/locks", "cat/aarch64.cat", Arch.ARM8 }, + { "dartagnan/src/test/resources/libvsync", "cat/aarch64.cat", Arch.ARM8 }, + { "dartagnan/src/test/resources/miscellaneous", "cat/aarch64.cat", Arch.ARM8 }, + + { "dartagnan/src/test/resources/lfds", "cat/tso.cat", Arch.TSO }, + { "dartagnan/src/test/resources/locks", "cat/tso.cat", Arch.TSO }, + { "dartagnan/src/test/resources/libvsync", "cat/tso.cat", Arch.TSO }, + { "dartagnan/src/test/resources/miscellaneous", "cat/tso.cat", Arch.TSO }, + + { "dartagnan/src/test/resources/lfds", "cat/riscv.cat", Arch.RISCV }, + { "dartagnan/src/test/resources/locks", "cat/riscv.cat", Arch.RISCV }, + { "dartagnan/src/test/resources/libvsync", "cat/riscv.cat", Arch.RISCV }, + { "dartagnan/src/test/resources/miscellaneous", "cat/riscv.cat", Arch.RISCV }, + + { "dartagnan/src/test/resources/spirv/benchmarks", "cat/spirv.cat", Arch.VULKAN }, + }); + } + + @Test + public void compareBaseSets() throws Exception { + for (String program : listFiles(Path.of(getRootPath(testPath)))) { + doCompareSets(program); + } + } + + private List listFiles(Path path) throws IOException { + List result = new LinkedList<>(); + try (DirectoryStream files = Files.newDirectoryStream(path)) { + for (Path file : files) { + if (Files.isDirectory(file)) { + result.addAll(listFiles(file.toAbsolutePath())); + } else { + String filePath = file.toAbsolutePath().toString(); + if (filePath.endsWith(".litmus") || filePath.endsWith(".ll") || + filePath.endsWith(".c") || filePath.endsWith(".spv.dis")) { + result.add(filePath); + } + } + } + } + return result; + } + + private void doCompareSets(String path) throws Exception { + try(SolverContext ctx = createSolverContext(SolverContextFactory.Solvers.Z3)) { + // Base program and consistency model + Program program = new ProgramParser().parse(new File(path)); + Wmm wmm = new ParserCat().parse(new File(getRootPath(modelPath))); + Configuration baseConfig = Configuration.builder().build(); + VerificationTask baseTask = createTask(program, wmm, baseConfig); + wmm.configureAll(baseTask.getConfig()); + preprocessProgram(baseTask, baseTask.getConfig()); + preprocessMemoryModel(baseTask, baseTask.getConfig()); + + // Native analysis + Context nativeContext = Context.create(); + Configuration nativeConfig = Configuration.builder() + .setOption(ALIAS_METHOD, FIELD_SENSITIVE.asStringOption()) + .setOption(ENABLE_EXTENDED_RELATION_ANALYSIS, "false") + .build(); + VerificationTask nativeTask = createTask(program, wmm, nativeConfig); + performStaticProgramAnalyses(nativeTask, nativeContext, nativeTask.getConfig()); + performStaticWmmAnalyses(nativeTask, nativeContext, nativeTask.getConfig()); + RelationAnalysis nativeRa = nativeContext.get(RelationAnalysis.class); + + // Lazy analysis + Context lazyContext = Context.create(); + Configuration lazyConfig = Configuration.builder() + .setOption(ALIAS_METHOD, FIELD_SENSITIVE.asStringOption()) + .setOption(RELATION_ANALYSIS, RelationAnalysisMethod.LAZY.toString()) + .build(); + VerificationTask lazyTask = createTask(program, wmm, lazyConfig); + performStaticProgramAnalyses(lazyTask, lazyContext, lazyTask.getConfig()); + performStaticWmmAnalyses(lazyTask, lazyContext, lazyTask.getConfig()); + RelationAnalysis lazyRa = lazyContext.get(RelationAnalysis.class); + + // Assert may and must sets are equal + for (Relation relation : nativeTask.getMemoryModel().getRelations()) { + assertEquals(nativeRa.getKnowledge(relation).getMaySet(), + lazyRa.getKnowledge(relation).getMaySet()); + assertEquals(nativeRa.getKnowledge(relation).getMustSet(), + lazyRa.getKnowledge(relation).getMustSet()); + } + + // Generate and assert encode sets + WmmEncoder nativeEncoder = WmmEncoder.withContext(EncodingContext.of(nativeTask, nativeContext, ctx.getFormulaManager())); + WmmEncoder lazyEncoder = WmmEncoder.withContext(EncodingContext.of(lazyTask, lazyContext, ctx.getFormulaManager())); + for (Relation relation : nativeTask.getMemoryModel().getRelations()) { + assertEquals(nativeEncoder.encodeSets.get(relation), + lazyEncoder.encodeSets.get(relation)); + } + } + } + + private VerificationTask createTask(Program program, Wmm wmm, Configuration config) + throws InvalidConfigurationException { + return VerificationTask.builder() + .withConfig(config) + .withBound(2) + .withTarget(target) + .build(program, wmm, EnumSet.of(PROGRAM_SPEC)); + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java deleted file mode 100644 index e5bb7198f5..0000000000 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java +++ /dev/null @@ -1,359 +0,0 @@ -package com.dat3m.dartagnan.wmm.utils; - -import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.event.core.Skip; -import org.junit.Test; - -import java.util.HashSet; -import java.util.Map; -import java.util.Set; - -import static org.junit.Assert.*; - -public class EmptyEventGraphTest { - - @Test - public void testIsSingleton() { - // when - EventGraph first = EventGraph.empty(); - EventGraph second = EventGraph.empty(); - - // then - assertSame(first, second); - } - - @Test - public void testIsEmpty() { - // when - EventGraph empty = EventGraph.empty(); - - // then - assertTrue(empty.isEmpty()); - } - - @Test - public void testSize() { - // when - EventGraph empty = EventGraph.empty(); - - // then - assertEquals(0, empty.size()); - } - - @Test - public void testContains() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph empty = EventGraph.empty(); - - // then - assertFalse(empty.contains(e1, e2)); - } - - @Test(expected = UnsupportedOperationException.class) - public void testAdd() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph.empty().add(e1, e2); - } - - @Test - public void testRemove() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - assertFalse(EventGraph.empty().remove(e1, e2)); - } - - @Test(expected = UnsupportedOperationException.class) - public void testAddAll() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph nonEmpty = new EventGraph(); - nonEmpty.add(e1, e2); - - // when - EventGraph.empty().addAll(nonEmpty); - } - - @Test(expected = UnsupportedOperationException.class) - public void testAddAllEmpty() { - // when - EventGraph.empty().addAll(EventGraph.empty()); - } - - @Test - public void testRemoveAll() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph nonEmpty = new EventGraph(); - nonEmpty.add(e1, e2); - - // when - assertFalse(EventGraph.empty().removeAll(nonEmpty)); - } - - @Test - public void testRemoveAllEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph nonEmpty = new EventGraph(); - nonEmpty.add(e1, e2); - - // when - assertFalse(EventGraph.empty().removeAll(nonEmpty)); - } - - @Test - public void testRetainAllEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph nonEmpty = new EventGraph(); - nonEmpty.add(e1, e2); - - // when - assertFalse(EventGraph.empty().retainAll(nonEmpty)); - } - - @Test - public void testInverse() { - // given - EventGraph empty = EventGraph.empty(); - - // when - EventGraph inverse = empty.inverse(); - - // then - assertTrue(inverse.isEmpty()); - assertNotSame(empty, inverse); - } - - @Test - public void testInverseModifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - EventGraph empty = EventGraph.empty(); - EventGraph inverse = empty.inverse(); - - // when - inverse.add(e1, e2); - - // then - assertFalse(empty.contains(e1, e2)); - assertTrue(inverse.contains(e1, e2)); - } - - @Test - public void testFilterTrue() { - // given - EventGraph empty = EventGraph.empty(); - - // when - EventGraph inverse = empty.filter((x, y) -> true); - - // then - assertTrue(inverse.isEmpty()); - assertNotSame(empty, inverse); - } - - @Test - public void testFilterFalse() { - // given - EventGraph empty = EventGraph.empty(); - - // when - EventGraph inverse = empty.filter((x, y) -> false); - - // then - assertTrue(inverse.isEmpty()); - assertNotSame(empty, inverse); - } - - @Test - public void testFilterModifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - EventGraph empty = EventGraph.empty(); - EventGraph inverse = empty.filter((x, y) -> true); - - // when - inverse.add(e1, e2); - - // then - assertFalse(empty.contains(e1, e2)); - assertTrue(inverse.contains(e1, e2)); - } - - @Test - public void testOutMap() { - // given - EventGraph empty = EventGraph.empty(); - - // when - Map> map = empty.getOutMap(); - - // then - assertTrue(map.isEmpty()); - } - - @Test(expected = UnsupportedOperationException.class) - public void testOutMapUnmodifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph empty = EventGraph.empty(); - Map> map = empty.getOutMap(); - - // when - map.put(e1, Set.of(e2)); - } - - @Test - public void testInMap() { - // given - EventGraph empty = EventGraph.empty(); - - // when - Map> map = empty.getInMap(); - - // then - assertTrue(map.isEmpty()); - } - - @Test(expected = UnsupportedOperationException.class) - public void testInMapUnmodifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph empty = EventGraph.empty(); - Map> map = empty.getInMap(); - - // when - map.put(e1, Set.of(e2)); - } - - @Test - public void testGetDomain() { - // given - EventGraph empty = EventGraph.empty(); - - // when - Set set = empty.getDomain(); - - // then - assertTrue(set.isEmpty()); - } - - @Test(expected = UnsupportedOperationException.class) - public void testGetDomainUnmodifiable() { - // given - Event e = new Skip(); - EventGraph empty = EventGraph.empty(); - Set set = empty.getDomain(); - - // when - set.add(e); - } - - @Test - public void testGetRange() { - // given - EventGraph empty = EventGraph.empty(); - - // when - Set set = empty.getRange(); - - // then - assertTrue(set.isEmpty()); - } - - @Test(expected = UnsupportedOperationException.class) - public void testGetRangeUnmodifiable() { - // given - Event e = new Skip(); - EventGraph empty = EventGraph.empty(); - Set set = empty.getRange(); - - // when - set.add(e); - } - - @Test - public void testGetRangeEvent() { - // given - Event e = new Skip(); - EventGraph empty = EventGraph.empty(); - - // when - Set set = empty.getRange(e); - - // then - assertTrue(set.isEmpty()); - } - - @Test(expected = UnsupportedOperationException.class) - public void testGetRangeEventUnmodifiable() { - // given - Event e = new Skip(); - EventGraph empty = EventGraph.empty(); - Set set = empty.getRange(e); - - // when - set.add(e); - } - - @Test - public void testRemoveIfTrue() { - // given - EventGraph empty = EventGraph.empty(); - - // when - assertFalse(empty.removeIf((x, y) -> true)); - } - - @Test - public void testRemoveIfFalse() { - // given - EventGraph empty = EventGraph.empty(); - - // when - assertFalse(empty.removeIf((x, y) -> false)); - } - - @Test - public void testApply() { - // given - EventGraph empty = EventGraph.empty(); - Set set = new HashSet<>(); - - // when - empty.apply((x, y) -> { - if (x.equals(y)) { - set.add(x); - } - }); - - // then - assertTrue(set.isEmpty()); - } -} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java deleted file mode 100644 index 54945cd4c3..0000000000 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java +++ /dev/null @@ -1,1842 +0,0 @@ -package com.dat3m.dartagnan.wmm.utils; - -import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.event.core.Skip; -import org.junit.Test; - -import java.util.HashSet; -import java.util.Map; -import java.util.Set; - -import static org.junit.Assert.*; - -public class EventGraphTest { - - @Test - public void testCopyConstructor() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - EventGraph first = new EventGraph(); - first.add(e1, e2); - - // when - EventGraph second = new EventGraph(first); - - // then - assertEquals(1, second.size()); - - // when - second.remove(e1, e2); - second.add(e2, e1); - - // then - assertEquals(1, first.size()); - assertTrue(first.contains(e1, e2)); - assertEquals(1, second.size()); - assertTrue(second.contains(e2, e1)); - } - - @Test - public void testIsEmptyWhenEmpty() { - // when - EventGraph eventGraph = new EventGraph(); - - // then - assertTrue(eventGraph.isEmpty()); - } - - @Test - public void testIsEmptyWhenNonEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - - // then - assertFalse(eventGraph.isEmpty()); - } - - @Test - public void testIsEmptyWhenRemoved() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.remove(e1, e2); - - // then - assertTrue(eventGraph.isEmpty()); - } - - @Test - public void testSizeEmpty() { - // when - EventGraph eventGraph = new EventGraph(); - - // then - assertEquals(0, eventGraph.size()); - } - - @Test - public void testSizeEmptyRemoval() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.remove(e1, e2); - - // then - assertEquals(0, eventGraph.size()); - } - - @Test - public void testSizeNonEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e1, e3); - eventGraph.add(e2, e3); - - // then - assertEquals(3, eventGraph.size()); - } - - @Test - public void testSizeNotEmptyInverse() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - - // then - assertEquals(2, eventGraph.size()); - } - - @Test - public void testSizeNotEmptyIdentity() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e1); - eventGraph.add(e2, e2); - eventGraph.add(e3, e3); - - // then - assertEquals(3, eventGraph.size()); - } - - @Test - public void testSizeNotEmptyDuplicates() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e1, e2); - eventGraph.add(e1, e2); - - // then - assertEquals(1, eventGraph.size()); - } - - @Test - public void testSizeNotEmptyRemoval() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e1, e3); - eventGraph.add(e2, e3); - eventGraph.remove(e1, e3); - - // then - assertEquals(2, eventGraph.size()); - } - - @Test - public void testSizeNotEmptyRemovalAlt() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e1, e3); - eventGraph.add(e2, e3); - eventGraph.remove(e2, e3); - - // then - assertEquals(2, eventGraph.size()); - } - - @Test - public void testContainsEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - - // then - assertFalse(eventGraph.contains(e1, e2)); - } - - @Test - public void testContainsNonEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e3, e3); - - // then - assertTrue(eventGraph.contains(e1, e2)); - assertTrue(eventGraph.contains(e3, e3)); - assertFalse(eventGraph.contains(e1, e1)); - assertFalse(eventGraph.contains(e1, e3)); - assertFalse(eventGraph.contains(e2, e1)); - } - - @Test - public void testContainsRemoved() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - eventGraph.remove(e1, e2); - - // then - assertFalse(eventGraph.contains(e1, e2)); - assertTrue(eventGraph.contains(e2, e1)); - } - - @Test - public void testAdd() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - boolean result = eventGraph.add(e1, e2); - - // then - assertTrue(result); - assertTrue(eventGraph.contains(e1, e2)); - assertFalse(eventGraph.contains(e2, e1)); - assertEquals(1, eventGraph.size()); - } - - @Test - public void testAddRepeated() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - boolean result1 = eventGraph.add(e1, e2); - boolean result2 = eventGraph.add(e1, e2); - - // then - assertTrue(result1); - assertFalse(result2); - assertTrue(eventGraph.contains(e1, e2)); - assertFalse(eventGraph.contains(e2, e1)); - assertEquals(1, eventGraph.size()); - } - - @Test - public void testRemoveEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - boolean result = eventGraph.remove(e1, e2); - - // then - assertFalse(result); - assertFalse(eventGraph.contains(e1, e2)); - assertFalse(eventGraph.contains(e2, e1)); - assertEquals(0, eventGraph.size()); - } - - @Test - public void testRemove() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - boolean result = eventGraph.remove(e1, e2); - - // then - assertTrue(result); - assertFalse(eventGraph.contains(e1, e2)); - assertTrue(eventGraph.contains(e2, e1)); - assertEquals(1, eventGraph.size()); - } - - @Test - public void testRemoveRepeated() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - boolean result1 = eventGraph.remove(e1, e2); - boolean result2 = eventGraph.remove(e1, e2); - - // then - assertTrue(result1); - assertFalse(result2); - assertFalse(eventGraph.contains(e1, e2)); - assertTrue(eventGraph.contains(e2, e1)); - assertEquals(1, eventGraph.size()); - } - - @Test - public void testAddAll() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e3); - second.add(e3, e3); - boolean result = first.addAll(second); - - // then - assertTrue(result); - - assertEquals(5, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e1, e3)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - assertTrue(first.contains(e3, e3)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e3)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testAddAllPartial() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e3, e3); - boolean result = first.addAll(second); - - // then - assertTrue(result); - - assertEquals(4, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - assertTrue(first.contains(e3, e3)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testAddAllNone() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e3, e1); - boolean result = first.addAll(second); - - // then - assertFalse(result); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testAddLeftEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - boolean result = first.addAll(second); - - // then - assertTrue(result); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testAddRightEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - boolean result = first.addAll(second); - - // then - assertFalse(result); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(0, second.size()); - } - - @Test - public void testRemoveAll() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - boolean result = first.removeAll(second); - - // then - assertTrue(result); - - assertEquals(1, first.size()); - assertTrue(first.contains(e3, e1)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - } - - @Test - public void testRemoveAllPartial() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e3, e3); - boolean result = first.removeAll(second); - - // then - assertTrue(result); - - assertEquals(2, first.size()); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testRemoveAllNone() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e3); - second.add(e3, e3); - boolean result = first.removeAll(second); - - // then - assertFalse(result); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e3)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testRemoveAllEmptied() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - second.add(e3, e3); - boolean result = first.removeAll(second); - - // then - assertTrue(result); - - assertEquals(0, first.size()); - - assertEquals(4, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testRemoveAllLeftEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - boolean result = first.removeAll(second); - - // then - assertFalse(result); - - assertEquals(0, first.size()); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testRemoveAllRightEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - boolean result = first.removeAll(second); - - // then - assertFalse(result); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(0, second.size()); - } - - @Test - public void testRetainAll() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - boolean result = first.retainAll(second); - - // then - assertTrue(result); - - assertEquals(2, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - } - - @Test - public void testRetainAllPartial() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e3, e3); - boolean result = first.retainAll(second); - - // then - assertTrue(result); - - assertEquals(1, first.size()); - assertTrue(first.contains(e1, e2)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testRetainAllNone() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - second.add(e3, e3); - boolean result = first.retainAll(second); - - // then - assertFalse(result); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(4, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testRetainAllEmptied() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - second.add(e3, e3); - boolean result = first.retainAll(second); - - // then - assertTrue(result); - - assertEquals(0, first.size()); - - assertEquals(1, second.size()); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testRetainAllLeftEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - boolean result = first.retainAll(second); - - // then - assertFalse(result); - - assertEquals(0, first.size()); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testRetainAllRightEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - EventGraph second = new EventGraph(); - boolean result = first.retainAll(second); - - // then - assertTrue(result); - - assertEquals(0, first.size()); - - assertEquals(0, second.size()); - } - - @Test - public void testInverse() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - Event e4 = new Skip(); - Event e5 = new Skip(); - - // when - EventGraph original = new EventGraph(); - original.add(e1, e2); - original.add(e2, e1); - original.add(e3, e4); - original.add(e5, e5); - EventGraph inverse = original.inverse(); - - // then - assertEquals(4, inverse.size()); - assertTrue(inverse.contains(e1, e2)); - assertTrue(inverse.contains(e2, e1)); - assertTrue(inverse.contains(e4, e3)); - assertTrue(inverse.contains(e5, e5)); - - assertEquals(4, original.size()); - assertTrue(original.contains(e1, e2)); - assertTrue(original.contains(e2, e1)); - assertTrue(original.contains(e3, e4)); - assertTrue(original.contains(e5, e5)); - } - - @Test - public void testInverseModifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph original = new EventGraph(); - original.add(e1, e2); - - EventGraph inverse = original.inverse(); - - // when - inverse.add(e3, e3); - - // then - assertEquals(1, original.size()); - assertTrue(original.contains(e1, e2)); - - assertEquals(2, inverse.size()); - assertTrue(inverse.contains(e2, e1)); - assertTrue(inverse.contains(e3, e3)); - } - - @Test - public void testInverseEmpty() { - // given - EventGraph original = new EventGraph(); - - // when - EventGraph inverse = original.inverse(); - - // then - assertTrue(original.isEmpty()); - assertTrue(inverse.isEmpty()); - } - - @Test - public void testFilterLoop() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph original = new EventGraph(); - original.add(e1, e1); - original.add(e1, e2); - original.add(e2, e1); - original.add(e3, e3); - EventGraph filtered = original.filter(Object::equals); - - // then - assertEquals(2, filtered.size()); - assertTrue(filtered.contains(e1, e1)); - assertTrue(filtered.contains(e3, e3)); - - assertEquals(4, original.size()); - assertTrue(original.contains(e1, e1)); - assertTrue(original.contains(e1, e2)); - assertTrue(original.contains(e2, e1)); - assertTrue(original.contains(e3, e3)); - } - - @Test - public void testFilterNoLoop() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph original = new EventGraph(); - original.add(e1, e1); - original.add(e1, e2); - original.add(e2, e1); - original.add(e3, e3); - EventGraph filtered = original.filter((x, y) -> !x.equals(y)); - - // then - assertEquals(2, filtered.size()); - assertTrue(filtered.contains(e1, e2)); - assertTrue(filtered.contains(e2, e1)); - - assertEquals(4, original.size()); - assertTrue(original.contains(e1, e1)); - assertTrue(original.contains(e1, e2)); - assertTrue(original.contains(e2, e1)); - assertTrue(original.contains(e3, e3)); - } - - @Test - public void testFilterModifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph original = new EventGraph(); - original.add(e1, e2); - - EventGraph filtered = original.filter((x, y) -> true); - - // when - filtered.add(e3, e3); - - // then - assertEquals(1, original.size()); - assertTrue(original.contains(e1, e2)); - - assertEquals(2, filtered.size()); - assertTrue(filtered.contains(e1, e2)); - assertTrue(filtered.contains(e3, e3)); - } - - @Test - public void testFilterEmpty() { - // given - EventGraph original = new EventGraph(); - - // when - EventGraph filtered = original.filter(Object::equals); - - // then - assertTrue(original.isEmpty()); - assertTrue(filtered.isEmpty()); - } - - @Test - public void testOutMap() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - eventGraph.add(e1, e3); - eventGraph.add(e3, e2); - eventGraph.add(e3, e3); - - // when - Map> actual = eventGraph.getOutMap(); - - // then - Map> expected = Map.of(e1, Set.of(e2, e3), e2, Set.of(e1), e3, Set.of(e2, e3)); - assertEquals(expected, actual); - assertEquals(Set.of(e2, e3), actual.get(e1)); - assertEquals(Set.of(e1, e2, e3), actual.keySet()); - } - - @Test - public void testOutMapUnmodifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e3); - - // when - Map> map = eventGraph.getOutMap(); - - // then - assertThrows(UnsupportedOperationException.class, () -> map.remove(e1)); - assertThrows(UnsupportedOperationException.class, () -> map.remove(e3)); - - Set newSet = Set.of(e3); - assertThrows(UnsupportedOperationException.class, () -> map.put(e3, newSet)); - assertThrows(UnsupportedOperationException.class, () -> map.computeIfAbsent(e3, x -> newSet)); - - Set oldSet = map.get(e1); - assertThrows(UnsupportedOperationException.class, () -> oldSet.remove(e2)); - assertThrows(UnsupportedOperationException.class, () -> oldSet.add(e3)); - } - - @Test - public void testInMap() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - eventGraph.add(e1, e3); - eventGraph.add(e3, e2); - eventGraph.add(e3, e3); - - // when - Map> actual = eventGraph.getInMap(); - - // then - Map> expected = Map.of(e1, Set.of(e2), e2, Set.of(e1, e3), e3, Set.of(e1, e3)); - assertEquals(expected, actual); - assertEquals(Set.of(e1, e3), actual.get(e2)); - assertEquals(Set.of(e1, e2, e3), actual.keySet()); - } - - @Test - public void testInMapUnmodifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e3); - - // when - Map> map = eventGraph.getOutMap(); - - // then - assertThrows(UnsupportedOperationException.class, () -> map.remove(e2)); - assertThrows(UnsupportedOperationException.class, () -> map.remove(e1)); - - Set newSet = Set.of(e1); - assertThrows(UnsupportedOperationException.class, () -> map.put(e1, newSet)); - assertThrows(UnsupportedOperationException.class, () -> map.computeIfAbsent(e1, x -> newSet)); - - Set oldSet = map.get(e2); - assertThrows(UnsupportedOperationException.class, () -> oldSet.remove(e1)); - assertThrows(UnsupportedOperationException.class, () -> oldSet.add(e3)); - } - - @Test - public void testGetDomain() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - Event e4 = new Skip(); - Event e5 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - eventGraph.add(e3, e4); - eventGraph.add(e5, e5); - Set domain = eventGraph.getDomain(); - - // then - assertEquals(Set.of(e1, e2, e3, e5), domain); - } - - @Test(expected = UnsupportedOperationException.class) - public void testGetDomainUnmodifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - - Set set = eventGraph.getDomain(); - - // when - set.add(e2); - } - - @Test - public void testGetDomainEmpty() { - // given - EventGraph eventGraph = new EventGraph(); - - // when - Set domain = eventGraph.getDomain(); - - // then - assertTrue(domain.isEmpty()); - } - - @Test - public void testGetRange() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - Event e4 = new Skip(); - Event e5 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e2, e1); - eventGraph.add(e3, e4); - eventGraph.add(e5, e5); - Set range = eventGraph.getRange(); - - // then - assertEquals(Set.of(e1, e2, e4, e5), range); - } - - @Test(expected = UnsupportedOperationException.class) - public void testGetRangeUnmodifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - - Set set = eventGraph.getRange(); - - // when - set.add(e1); - } - - @Test - public void testGetRangeEmpty() { - // given - EventGraph eventGraph = new EventGraph(); - - // when - Set range = eventGraph.getRange(); - - // then - assertTrue(range.isEmpty()); - } - - @Test - public void testGetRangeEvent() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - Event e4 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e1, e3); - eventGraph.add(e2, e1); - eventGraph.add(e3, e3); - - // then - assertEquals(Set.of(e2,e3), eventGraph.getRange(e1)); - assertEquals(Set.of(e1), eventGraph.getRange(e2)); - assertEquals(Set.of(e3), eventGraph.getRange(e3)); - assertEquals(Set.of(), eventGraph.getRange(e4)); - } - - @Test(expected = UnsupportedOperationException.class) - public void testGetRangeEventUnmodifiable() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - - Set set = eventGraph.getRange(e1); - - // when - set.add(e1); - } - - @Test - public void testGetRangeEventEmpty() { - // given - Event e = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - - // then - assertTrue(eventGraph.getRange(e).isEmpty()); - } - - @Test - public void testAddRangeEvent() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e3, e3); - - // when - assertFalse(eventGraph.addRange(e1, Set.of(e2))); - assertTrue(eventGraph.addRange(e1, Set.of(e2, e3))); - assertFalse(eventGraph.addRange(e3, Set.of(e3))); - assertTrue(eventGraph.addRange(e3, Set.of(e1, e3))); - assertFalse(eventGraph.addRange(e1, Set.of())); - - // then - assertEquals(4, eventGraph.size()); - assertTrue(eventGraph.contains(e1, e2)); - assertTrue(eventGraph.contains(e1, e3)); - assertTrue(eventGraph.contains(e3, e1)); - assertTrue(eventGraph.contains(e3, e3)); - } - - @Test - public void testRemoveIf() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - // when - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e1, e3); - eventGraph.add(e2, e1); - eventGraph.add(e3, e3); - eventGraph.removeIf(Object::equals); - - // then - assertEquals(3, eventGraph.size()); - assertTrue(eventGraph.contains(e1, e2)); - assertTrue(eventGraph.contains(e1, e3)); - assertTrue(eventGraph.contains(e2, e1)); - } - - @Test - public void testRemoveIfEmpty() { - // given - EventGraph eventGraph = new EventGraph(); - - // when - eventGraph.removeIf(Object::equals); - - // then - assertTrue(eventGraph.isEmpty()); - } - - @Test - public void testApply() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - eventGraph.add(e1, e2); - eventGraph.add(e3, e3); - - // when - Set result = new HashSet<>(Set.of(e1, e2, e3)); - eventGraph.apply((x, y) -> { - if (x.equals(y)) { - result.remove(x); - } - }); - - // then - assertEquals(Set.of(e1, e2), result); - - assertEquals(2, eventGraph.size()); - assertTrue(eventGraph.contains(e1, e2)); - assertTrue(eventGraph.contains(e3, e3)); - } - - @Test - public void testApplyEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph eventGraph = new EventGraph(); - - // when - Set result = new HashSet<>(Set.of(e1, e2, e3)); - eventGraph.apply((x, y) -> { - if (x.equals(y)) { - result.remove(x); - } - }); - - // then - assertEquals(Set.of(e1, e2, e3), result); - assertTrue(eventGraph.isEmpty()); - } - - @Test - public void testUnionDisjoint() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e3); - second.add(e2, e1); - second.add(e3, e2); - - // when - EventGraph result = EventGraph.union(first, second); - - // then - assertEquals(6, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - assertTrue(result.contains(e1, e3)); - assertTrue(result.contains(e2, e1)); - assertTrue(result.contains(e3, e2)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e3)); - assertTrue(second.contains(e2, e1)); - assertTrue(second.contains(e3, e2)); - } - - @Test - public void testUnionPartiallyOverlapping() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e3, e3); - - // when - EventGraph result = EventGraph.union(first, second); - - // then - assertEquals(4, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - assertTrue(result.contains(e3, e3)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testUnionEqual() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - - // when - EventGraph result = EventGraph.union(first, second); - - // then - assertEquals(3, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testUnionLeftEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - - // when - EventGraph result = EventGraph.union(first, second); - - // then - assertEquals(3, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - - assertEquals(0, first.size()); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testUnionRightEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - - // when - EventGraph result = EventGraph.union(first, second); - - // then - assertEquals(3, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(0, second.size()); - } - - @Test - public void testIntersectionDisjoint() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e3); - second.add(e2, e1); - second.add(e3, e2); - - // when - EventGraph result = EventGraph.intersection(first, second); - - // then - assertEquals(0, result.size()); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e3)); - assertTrue(second.contains(e2, e1)); - assertTrue(second.contains(e3, e2)); - } - - @Test - public void testIntersectionPartiallyOverlapping() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e3, e3); - - // when - EventGraph result = EventGraph.intersection(first, second); - - // then - assertEquals(1, result.size()); - assertTrue(result.contains(e1, e2)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testIntersectionEqual() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - - // when - EventGraph result = EventGraph.intersection(first, second); - - // then - assertEquals(3, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testIntersectionLeftEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - - // when - EventGraph result = EventGraph.intersection(first, second); - - // then - assertEquals(0, result.size()); - - assertEquals(0, first.size()); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testIntersectionRightEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - - // when - EventGraph result = EventGraph.intersection(first, second); - - // then - assertEquals(0, result.size()); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(0, second.size()); - } - - @Test - public void testDifferenceDisjoint() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e3); - second.add(e2, e1); - second.add(e3, e2); - - // when - EventGraph result = EventGraph.difference(first, second); - - // then - assertEquals(3, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e3)); - assertTrue(second.contains(e2, e1)); - assertTrue(second.contains(e3, e2)); - } - - @Test - public void testDifferencePartiallyOverlapping() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e3, e3); - - // when - EventGraph result = EventGraph.difference(first, second); - - // then - assertEquals(2, result.size()); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(2, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e3, e3)); - } - - @Test - public void testDifferenceEqual() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - - // when - EventGraph result = EventGraph.difference(first, second); - - // then - assertEquals(0, result.size()); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testDifferenceLeftEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - - EventGraph second = new EventGraph(); - second.add(e1, e2); - second.add(e2, e3); - second.add(e3, e1); - - // when - EventGraph result = EventGraph.difference(first, second); - - // then - assertEquals(0, result.size()); - - assertEquals(0, first.size()); - - assertEquals(3, second.size()); - assertTrue(second.contains(e1, e2)); - assertTrue(second.contains(e2, e3)); - assertTrue(second.contains(e3, e1)); - } - - @Test - public void testDifferenceRightEmpty() { - // given - Event e1 = new Skip(); - Event e2 = new Skip(); - Event e3 = new Skip(); - - EventGraph first = new EventGraph(); - first.add(e1, e2); - first.add(e2, e3); - first.add(e3, e1); - - EventGraph second = new EventGraph(); - - // when - EventGraph result = EventGraph.difference(first, second); - - // then - assertEquals(3, result.size()); - assertTrue(result.contains(e1, e2)); - assertTrue(result.contains(e2, e3)); - assertTrue(result.contains(e3, e1)); - - assertEquals(3, first.size()); - assertTrue(first.contains(e1, e2)); - assertTrue(first.contains(e2, e3)); - assertTrue(first.contains(e3, e1)); - - assertEquals(0, second.size()); - } -} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphStaticTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphStaticTest.java new file mode 100644 index 0000000000..e9aecab2a5 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphStaticTest.java @@ -0,0 +1,785 @@ +package com.dat3m.dartagnan.wmm.utils.graph; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.Skip; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.LazyEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.IOException; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.util.Arrays; +import java.util.Collection; +import java.util.Map; +import java.util.Set; +import java.util.function.BiFunction; +import java.util.function.Function; +import java.util.stream.Collectors; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; + +@RunWith(Parameterized.class) +public class EventGraphStaticTest { + + private final Class resultClass; + private final Class leftClass; + private final Class rightClass; + + public EventGraphStaticTest(Class resultClass, Class leftClass, Class rightClass) { + this.resultClass = resultClass; + this.leftClass = leftClass; + this.rightClass = rightClass; + } + + @Parameterized.Parameters + public static Iterable data() throws IOException { + return Arrays.asList(new Object[][]{ + // resultClass, leftClass, rightClass + {MapEventGraph.class, MapEventGraph.class, MapEventGraph.class}, + {MapEventGraph.class, MapEventGraph.class, ImmutableMapEventGraph.class}, + {MapEventGraph.class, MapEventGraph.class, LazyEventGraph.class}, + {MapEventGraph.class, ImmutableMapEventGraph.class, MapEventGraph.class}, + {MapEventGraph.class, ImmutableMapEventGraph.class, ImmutableMapEventGraph.class}, + {MapEventGraph.class, ImmutableMapEventGraph.class, LazyEventGraph.class}, + {MapEventGraph.class, LazyEventGraph.class, MapEventGraph.class}, + {MapEventGraph.class, LazyEventGraph.class, ImmutableMapEventGraph.class}, + {MapEventGraph.class, LazyEventGraph.class, LazyEventGraph.class}, + + {LazyEventGraph.class, MapEventGraph.class, MapEventGraph.class}, + {LazyEventGraph.class, MapEventGraph.class, ImmutableMapEventGraph.class}, + {LazyEventGraph.class, MapEventGraph.class, LazyEventGraph.class}, + {LazyEventGraph.class, ImmutableMapEventGraph.class, MapEventGraph.class}, + {LazyEventGraph.class, ImmutableMapEventGraph.class, ImmutableMapEventGraph.class}, + {LazyEventGraph.class, ImmutableMapEventGraph.class, LazyEventGraph.class}, + {LazyEventGraph.class, LazyEventGraph.class, MapEventGraph.class}, + {LazyEventGraph.class, LazyEventGraph.class, ImmutableMapEventGraph.class}, + {LazyEventGraph.class, LazyEventGraph.class, LazyEventGraph.class}, + + {ImmutableMapEventGraph.class, MapEventGraph.class, MapEventGraph.class}, + {ImmutableMapEventGraph.class, MapEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableMapEventGraph.class, MapEventGraph.class, LazyEventGraph.class}, + {ImmutableMapEventGraph.class, ImmutableMapEventGraph.class, MapEventGraph.class}, + {ImmutableMapEventGraph.class, ImmutableMapEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableMapEventGraph.class, ImmutableMapEventGraph.class, LazyEventGraph.class}, + {ImmutableMapEventGraph.class, LazyEventGraph.class, MapEventGraph.class}, + {ImmutableMapEventGraph.class, LazyEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableMapEventGraph.class, LazyEventGraph.class, LazyEventGraph.class}, + + {MutableEventGraph.class, MapEventGraph.class, MapEventGraph.class}, + {MutableEventGraph.class, MapEventGraph.class, ImmutableMapEventGraph.class}, + {MutableEventGraph.class, MapEventGraph.class, LazyEventGraph.class}, + {MutableEventGraph.class, ImmutableMapEventGraph.class, MapEventGraph.class}, + {MutableEventGraph.class, ImmutableMapEventGraph.class, ImmutableMapEventGraph.class}, + {MutableEventGraph.class, ImmutableMapEventGraph.class, LazyEventGraph.class}, + {MutableEventGraph.class, LazyEventGraph.class, MapEventGraph.class}, + {MutableEventGraph.class, LazyEventGraph.class, ImmutableMapEventGraph.class}, + {MutableEventGraph.class, LazyEventGraph.class, LazyEventGraph.class}, + + {ImmutableEventGraph.class, MapEventGraph.class, MapEventGraph.class}, + {ImmutableEventGraph.class, MapEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableEventGraph.class, MapEventGraph.class, LazyEventGraph.class}, + {ImmutableEventGraph.class, ImmutableMapEventGraph.class, MapEventGraph.class}, + {ImmutableEventGraph.class, ImmutableMapEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableEventGraph.class, ImmutableMapEventGraph.class, LazyEventGraph.class}, + {ImmutableEventGraph.class, LazyEventGraph.class, MapEventGraph.class}, + {ImmutableEventGraph.class, LazyEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableEventGraph.class, LazyEventGraph.class, LazyEventGraph.class}, + + {EventGraph.class, MapEventGraph.class, MapEventGraph.class}, + {EventGraph.class, MapEventGraph.class, ImmutableMapEventGraph.class}, + {EventGraph.class, MapEventGraph.class, LazyEventGraph.class}, + {EventGraph.class, ImmutableMapEventGraph.class, MapEventGraph.class}, + {EventGraph.class, ImmutableMapEventGraph.class, ImmutableMapEventGraph.class}, + {EventGraph.class, ImmutableMapEventGraph.class, LazyEventGraph.class}, + {EventGraph.class, LazyEventGraph.class, MapEventGraph.class}, + {EventGraph.class, LazyEventGraph.class, ImmutableMapEventGraph.class}, + {EventGraph.class, LazyEventGraph.class, LazyEventGraph.class}, + }); + } + + @Test + public void testUnionDisjoint() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e3), + e2, Set.of(e1), + e3, Set.of(e2) + )); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(6, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertTrue(result.contains(e1, e3)); + assertTrue(result.contains(e2, e1)); + assertTrue(result.contains(e3, e2)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e3)); + assertTrue(right.contains(e2, e1)); + assertTrue(right.contains(e3, e2)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testUnionPartiallyOverlapping() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(4, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertTrue(result.contains(e3, e3)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(2, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e3, e3)); + assertEquals(Set.of(e1, e3), right.getDomain()); + assertEquals(Set.of(e2, e3), right.getRange()); + } + + @Test + public void testUnionEqual() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(3, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e2, e3)); + assertTrue(right.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testUnionLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of()); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(3, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(0, left.size()); + assertEquals(Set.of(), left.getDomain()); + assertEquals(Set.of(), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e2, e3)); + assertTrue(right.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testUnionRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of()); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(3, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(0, right.size()); + assertEquals(Set.of(), right.getDomain()); + assertEquals(Set.of(), right.getRange()); + } + + @Test + public void testIntersectionDisjoint() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e3), + e2, Set.of(e1), + e3, Set.of(e2) + )); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e3)); + assertTrue(right.contains(e2, e1)); + assertTrue(right.contains(e3, e2)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testIntersectionPartiallyOverlapping() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(1, result.size()); + assertTrue(result.contains(e1, e2)); + assertEquals(Set.of(e1), result.getDomain()); + assertEquals(Set.of(e2), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(2, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e3, e3)); + assertEquals(Set.of(e1, e3), right.getDomain()); + assertEquals(Set.of(e2, e3), right.getRange()); + } + + @Test + public void testIntersectionEqual() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(3, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e2, e3)); + assertTrue(right.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testIntersectionLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of()); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(0, left.size()); + assertEquals(Set.of(), left.getDomain()); + assertEquals(Set.of(), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e2, e3)); + assertTrue(right.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testIntersectionRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of()); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{left, right}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(0, right.size()); + assertEquals(Set.of(), right.getDomain()); + assertEquals(Set.of(), right.getRange()); + } + + @Test + public void testDifferenceDisjoint() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e3), + e2, Set.of(e1), + e3, Set.of(e2) + )); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(left, right); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(3, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e3)); + assertTrue(right.contains(e2, e1)); + assertTrue(right.contains(e3, e2)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testDifferencePartiallyOverlapping() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(left, right); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(2, result.size()); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertEquals(Set.of(e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(2, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e3, e3)); + assertEquals(Set.of(e1, e3), right.getDomain()); + assertEquals(Set.of(e2, e3), right.getRange()); + } + + @Test + public void testDifferenceEqual() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(left, right); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e2, e3)); + assertTrue(right.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testDifferenceLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of()); + + EventGraph right = makeEventGraph(rightClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(left, right); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(0, left.size()); + assertEquals(Set.of(), left.getDomain()); + assertEquals(Set.of(), left.getRange()); + + assertEquals(3, right.size()); + assertTrue(right.contains(e1, e2)); + assertTrue(right.contains(e2, e3)); + assertTrue(right.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), right.getDomain()); + assertEquals(Set.of(e1, e2, e3), right.getRange()); + } + + @Test + public void testDifferenceRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph left = makeEventGraph(leftClass, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + + EventGraph right = makeEventGraph(rightClass, Map.of()); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(left, right); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(3, result.size()); + assertTrue(result.contains(e1, e2)); + assertTrue(result.contains(e2, e3)); + assertTrue(result.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), result.getDomain()); + assertEquals(Set.of(e1, e2, e3), result.getRange()); + + assertEquals(3, left.size()); + assertTrue(left.contains(e1, e2)); + assertTrue(left.contains(e2, e3)); + assertTrue(left.contains(e3, e1)); + assertEquals(Set.of(e1, e2, e3), left.getDomain()); + assertEquals(Set.of(e1, e2, e3), left.getRange()); + + assertEquals(0, right.size()); + assertEquals(Set.of(), right.getDomain()); + assertEquals(Set.of(), right.getRange()); + } + + private Function getFunction(Class cls, String name) { + return (operands) -> { + try { + Method method = cls.getMethod(name, EventGraph[].class); + return (EventGraph) method.invoke(null, new Object[]{operands}); + } catch (NoSuchMethodException | IllegalAccessException | InvocationTargetException e) { + throw new RuntimeException(e); + } + }; + } + + private BiFunction getDifferenceFunction(Class cls) { + return (left, right) -> { + try { + Method method = cls.getMethod("difference", EventGraph.class, EventGraph.class); + return (EventGraph) method.invoke(null, left, right); + } catch (NoSuchMethodException | IllegalAccessException | InvocationTargetException e) { + throw new RuntimeException(e); + } + }; + } + + private EventGraph makeEventGraph(Class cls, Map> data) { + if (cls.isAssignableFrom(MapEventGraph.class)) { + return new MapEventGraph(data); + } + if (cls.isAssignableFrom(ImmutableMapEventGraph.class)) { + return new ImmutableMapEventGraph(data); + } + if (cls.isAssignableFrom(LazyEventGraph.class)) { + Set range = data.values().stream().flatMap(Collection::stream).collect(Collectors.toSet()); + return new LazyEventGraph(data.keySet(), range, (e1, e2) -> data.getOrDefault(e1, Set.of()).contains(e2)); + } + throw new RuntimeException("Cannot resolve constructor for class " + cls.getSimpleName()); + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphTest.java new file mode 100644 index 0000000000..9ea10afe60 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraphTest.java @@ -0,0 +1,594 @@ +package com.dat3m.dartagnan.wmm.utils.graph; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.Skip; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.immutable.LazyEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.IOException; +import java.util.*; +import java.util.stream.Collectors; + +import static org.junit.Assert.*; + +@RunWith(Parameterized.class) +public class EventGraphTest { + + private final Class cls; + + public EventGraphTest(Class cls) { + this.cls = cls; + } + + @Parameterized.Parameters + public static Iterable data() throws IOException { + return Arrays.asList(new Object[][]{ + {MapEventGraph.class}, + {ImmutableMapEventGraph.class}, + {LazyEventGraph.class}, + }); + } + + @Test + public void testIsEmptyWhenEmpty() { + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // then + assertTrue(eventGraph.isEmpty()); + } + + @Test + public void testIsEmptyWhenNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2) + )); + + // then + assertFalse(eventGraph.isEmpty()); + } + + @Test + public void testSizeEmpty() { + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // then + assertEquals(0, eventGraph.size()); + } + + @Test + public void testSizeNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2, e3), + e2, Set.of(e3) + )); + + // then + assertEquals(3, eventGraph.size()); + } + + @Test + public void testSizeNotEmptyInverse() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e1) + )); + + // then + assertEquals(2, eventGraph.size()); + } + + @Test + public void testSizeNotEmptyIdentity() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e1), + e2, Set.of(e2), + e3, Set.of(e3) + )); + + // then + assertEquals(3, eventGraph.size()); + } + + @Test + public void testContainsEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // then + assertFalse(eventGraph.contains(e1, e2)); + } + + @Test + public void testContainsNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + + // then + assertTrue(eventGraph.contains(e1, e2)); + assertTrue(eventGraph.contains(e3, e3)); + assertFalse(eventGraph.contains(e1, e1)); + assertFalse(eventGraph.contains(e1, e3)); + assertFalse(eventGraph.contains(e2, e1)); + } + + @Test + public void testInverseEmpty() { + // given + EventGraph original = makeEventGraph(cls, Map.of()); + + // when + EventGraph inverse = original.inverse(); + + // then + assertEquals(original.getClass(), inverse.getClass()); + assertTrue(original.isEmpty()); + assertTrue(inverse.isEmpty()); + } + + @Test + public void testInverseNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + Event e4 = new Skip(); + Event e5 = new Skip(); + + // when + EventGraph original = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e1), + e3, Set.of(e4), + e5, Set.of(e5) + )); + EventGraph inverse = original.inverse(); + + // then + assertEquals(original.getClass(), inverse.getClass()); + + assertEquals(4, original.size()); + assertTrue(original.contains(e1, e2)); + assertTrue(original.contains(e2, e1)); + assertTrue(original.contains(e3, e4)); + assertTrue(original.contains(e5, e5)); + + assertEquals(4, inverse.size()); + assertTrue(inverse.contains(e1, e2)); + assertTrue(inverse.contains(e2, e1)); + assertTrue(inverse.contains(e4, e3)); + assertTrue(inverse.contains(e5, e5)); + } + + @Test + public void testFilterEmpty() { + // given + EventGraph original = makeEventGraph(cls, Map.of()); + + // when + EventGraph filtered = original.filter((x, y) -> true); + + // then + assertEquals(original.getClass(), filtered.getClass()); + assertTrue(filtered.isEmpty()); + assertEquals(Set.of(), filtered.getDomain()); + assertEquals(Set.of(), filtered.getRange()); + + assertTrue(original.isEmpty()); + assertEquals(Set.of(), original.getDomain()); + assertEquals(Set.of(), original.getRange()); + } + + @Test + public void testFilterIdentity() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + EventGraph original = makeEventGraph(cls, Map.of( + e1, Set.of(e1, e2), + e2, Set.of(e1), + e3, Set.of(e3) + )); + EventGraph filtered = original.filter(Object::equals); + + // then + assertEquals(original.getClass(), filtered.getClass()); + + assertEquals(2, filtered.size()); + assertTrue(filtered.contains(e1, e1)); + assertTrue(filtered.contains(e3, e3)); + assertEquals(Set.of(e1, e3), filtered.getDomain()); + assertEquals(Set.of(e1, e3), filtered.getRange()); + + assertEquals(4, original.size()); + assertTrue(original.contains(e1, e1)); + assertTrue(original.contains(e1, e2)); + assertTrue(original.contains(e2, e1)); + assertTrue(original.contains(e3, e3)); + assertEquals(Set.of(e1, e2, e3), original.getDomain()); + assertEquals(Set.of(e1, e2, e3), original.getRange()); + } + + @Test + public void testFilterNoIdentity() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + EventGraph original = makeEventGraph(cls, Map.of( + e1, Set.of(e1, e2), + e2, Set.of(e1), + e3, Set.of(e3) + )); + EventGraph filtered = original.filter((x, y) -> !x.equals(y)); + + // then + assertEquals(original.getClass(), filtered.getClass()); + + assertEquals(2, filtered.size()); + assertTrue(filtered.contains(e1, e2)); + assertTrue(filtered.contains(e2, e1)); + assertEquals(Set.of(e1, e2), filtered.getDomain()); + assertEquals(Set.of(e1, e2), filtered.getRange()); + + assertEquals(4, original.size()); + assertTrue(original.contains(e1, e1)); + assertTrue(original.contains(e1, e2)); + assertTrue(original.contains(e2, e1)); + assertTrue(original.contains(e3, e3)); + assertEquals(Set.of(e1, e2, e3), original.getDomain()); + assertEquals(Set.of(e1, e2, e3), original.getRange()); + } + + @Test + public void testOutMap() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2, e3), + e2, Set.of(e1), + e3, Set.of(e2, e3) + )); + Map> actual = eventGraph.getOutMap(); + + // then + Map> expected = Map.of( + e1, Set.of(e2, e3), + e2, Set.of(e1), + e3, Set.of(e2, e3) + ); + assertEquals(expected, actual); + } + + @Test + public void testOutMapUnmodifiable() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2) + )); + + // when + Map> map = eventGraph.getOutMap(); + + // then + assertThrows(UnsupportedOperationException.class, () -> map.remove(e1)); + + Set newSet = Set.of(e1); + assertThrows(UnsupportedOperationException.class, () -> map.put(e2, newSet)); + assertThrows(UnsupportedOperationException.class, () -> map.computeIfAbsent(e2, x -> newSet)); + + Set oldSet = map.get(e1); + assertThrows(UnsupportedOperationException.class, () -> oldSet.remove(e2)); + assertThrows(UnsupportedOperationException.class, () -> oldSet.add(e1)); + } + + @Test + public void testInMap() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2, e3), + e2, Set.of(e1), + e3, Set.of(e2, e3) + )); + Map> actual = eventGraph.getInMap(); + + // then + Map> expected = Map.of( + e1, Set.of(e2), + e2, Set.of(e1, e3), + e3, Set.of(e1, e3) + ); + assertEquals(expected, actual); + } + + @Test + public void testInMapUnmodifiable() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e2, Set.of(e1) + )); + + // when + Map> map = eventGraph.getInMap(); + + // then + assertThrows(UnsupportedOperationException.class, () -> map.remove(e1)); + + Set newSet = Set.of(e1); + assertThrows(UnsupportedOperationException.class, () -> map.put(e2, newSet)); + assertThrows(UnsupportedOperationException.class, () -> map.computeIfAbsent(e2, x -> newSet)); + + Set oldSet = map.get(e1); + assertThrows(UnsupportedOperationException.class, () -> oldSet.remove(e2)); + assertThrows(UnsupportedOperationException.class, () -> oldSet.add(e1)); + } + + @Test + public void testGetDomainEmpty() { + // given + EventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // when + Set domain = eventGraph.getDomain(); + + // then + assertTrue(domain.isEmpty()); + } + + @Test + public void testGetDomainNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + Event e4 = new Skip(); + Event e5 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e1), + e3, Set.of(e4), + e5, Set.of(e5) + )); + Set domain = eventGraph.getDomain(); + + // then + assertEquals(Set.of(e1, e2, e3, e5), domain); + } + + @Test(expected = UnsupportedOperationException.class) + public void testGetDomainUnmodifiable() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2) + )); + + Set set = eventGraph.getDomain(); + + // when + set.add(e2); + } + + @Test + public void testGetRangeEmpty() { + // given + EventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // when + Set range = eventGraph.getRange(); + + // then + assertTrue(range.isEmpty()); + } + + @Test + public void testGetRangeNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + Event e4 = new Skip(); + Event e5 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e1), + e3, Set.of(e4), + e5, Set.of(e5) + )); + Set range = eventGraph.getRange(); + + // then + assertEquals(Set.of(e1, e2, e4, e5), range); + } + + @Test(expected = UnsupportedOperationException.class) + public void testGetRangeUnmodifiable() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2) + )); + + Set set = eventGraph.getRange(); + + // when + set.add(e1); + } + + @Test + public void testGetRangeEventEmpty() { + // given + Event e = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // then + assertTrue(eventGraph.getRange(e).isEmpty()); + } + + @Test + public void testGetRangeEventNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + Event e4 = new Skip(); + + // when + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2, e3, e4), + e2, Set.of(e1), + e3, Set.of(e3) + )); + + // then + assertEquals(Set.of(e2, e3, e4), eventGraph.getRange(e1)); + assertEquals(Set.of(e1), eventGraph.getRange(e2)); + assertEquals(Set.of(e3), eventGraph.getRange(e3)); + assertEquals(Set.of(), eventGraph.getRange(e4)); + } + + @Test(expected = UnsupportedOperationException.class) + public void testGetRangeEventUnmodifiable() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2) + )); + + Set set = eventGraph.getRange(e1); + + // when + set.add(e1); + } + + @Test + public void testApplyEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // when + Set result = new HashSet<>(Set.of(e1, e2, e3)); + eventGraph.apply((x, y) -> { + if (x.equals(y)) { + result.remove(x); + } + }); + + // then + assertEquals(Set.of(e1, e2, e3), result); + assertTrue(eventGraph.isEmpty()); + } + + @Test + public void testApplyNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + EventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + + // when + Set result = new HashSet<>(Set.of(e1, e2, e3)); + eventGraph.apply((x, y) -> { + if (x.equals(y)) { + result.remove(x); + } + }); + + // then + assertEquals(Set.of(e1, e2), result); + assertEquals(2, eventGraph.size()); + assertTrue(eventGraph.contains(e1, e2)); + assertTrue(eventGraph.contains(e3, e3)); + } + + private EventGraph makeEventGraph(Class cls, Map> data) { + if (cls.isAssignableFrom(MapEventGraph.class)) { + return new MapEventGraph(data); + } + if (cls.isAssignableFrom(ImmutableMapEventGraph.class)) { + return new ImmutableMapEventGraph(data); + } + if (cls.isAssignableFrom(LazyEventGraph.class)) { + Set range = data.values().stream().flatMap(Collection::stream).collect(Collectors.toSet()); + return new LazyEventGraph(data.keySet(), range, (e1, e2) -> data.getOrDefault(e1, Set.of()).contains(e2)); + } + throw new RuntimeException("Cannot resolve constructor for class " + cls.getSimpleName()); + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphStaticTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphStaticTest.java new file mode 100644 index 0000000000..b193832960 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphStaticTest.java @@ -0,0 +1,359 @@ +package com.dat3m.dartagnan.wmm.utils.graph.immutable; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.Skip; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; +import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.IOException; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.util.Arrays; +import java.util.Collection; +import java.util.Map; +import java.util.Set; +import java.util.function.BiFunction; +import java.util.function.Function; +import java.util.stream.Collectors; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; + +@RunWith(Parameterized.class) +public class EmptyEventGraphStaticTest { + + private final Class resultClass; + private final Class emptyClass; + private final Class nonEmptyClass; + + public EmptyEventGraphStaticTest(Class resultClass, Class emptyClass, Class nonEmptyClass) { + this.resultClass = resultClass; + this.emptyClass = emptyClass; + this.nonEmptyClass = nonEmptyClass; + } + + @Parameterized.Parameters + public static Iterable data() throws IOException { + return Arrays.asList(new Object[][]{ + // resultClass, emptyClass, nonEmptyClass + {MapEventGraph.class, LazyEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {MapEventGraph.class, LazyEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {MapEventGraph.class, LazyEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + {MapEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {MapEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {MapEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + + {LazyEventGraph.class, LazyEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {LazyEventGraph.class, LazyEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {LazyEventGraph.class, LazyEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + {LazyEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {LazyEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {LazyEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + + {ImmutableMapEventGraph.class, LazyEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {ImmutableMapEventGraph.class, LazyEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableMapEventGraph.class, LazyEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + {ImmutableMapEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {ImmutableMapEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableMapEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + + {MutableEventGraph.class, LazyEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {MutableEventGraph.class, LazyEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {MutableEventGraph.class, LazyEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + {MutableEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {MutableEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {MutableEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + + {ImmutableEventGraph.class, LazyEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {ImmutableEventGraph.class, LazyEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableEventGraph.class, LazyEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + {ImmutableEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, MapEventGraph.class}, + {ImmutableEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, ImmutableMapEventGraph.class}, + {ImmutableEventGraph.class, ImmutableMapEventGraph.EmptyEventGraph.class, LazyEventGraph.class}, + }); + } + + @Test + public void testUnionLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph nonEmpty = makeEventGraph(nonEmptyClass, Map.of( + e1, Set.of(e2) + )); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{empty, nonEmpty}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(1, result.size()); + assertTrue(result.contains(e1, e2)); + assertEquals(Set.of(e1), result.getDomain()); + assertEquals(Set.of(e2), result.getRange()); + + assertEquals(0, empty.size()); + + assertEquals(1, nonEmpty.size()); + assertTrue(nonEmpty.contains(e1, e2)); + assertEquals(Set.of(e1), nonEmpty.getDomain()); + assertEquals(Set.of(e2), nonEmpty.getRange()); + } + + @Test + public void testUnionRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph nonEmpty = makeEventGraph(nonEmptyClass, Map.of( + e1, Set.of(e2) + )); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{nonEmpty, empty}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(1, result.size()); + assertTrue(result.contains(e1, e2)); + assertEquals(Set.of(e1), result.getDomain()); + assertEquals(Set.of(e2), result.getRange()); + + assertEquals(0, empty.size()); + + assertEquals(1, nonEmpty.size()); + assertTrue(nonEmpty.contains(e1, e2)); + assertEquals(Set.of(e1), nonEmpty.getDomain()); + assertEquals(Set.of(e2), nonEmpty.getRange()); + } + + @Test + public void testUnionBothEmpty() { + // given + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph anotherEmpty = makeEventGraph(nonEmptyClass, Map.of()); + + // when + EventGraph result = getFunction(resultClass, "union").apply(new EventGraph[]{empty, anotherEmpty}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(0, empty.size()); + assertEquals(0, anotherEmpty.size()); + } + + @Test + public void testIntersectionLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph nonEmpty = makeEventGraph(nonEmptyClass, Map.of( + e1, Set.of(e2) + )); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{empty, nonEmpty}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(0, empty.size()); + assertEquals(Set.of(), empty.getDomain()); + assertEquals(Set.of(), empty.getRange()); + + assertEquals(1, nonEmpty.size()); + assertTrue(nonEmpty.contains(e1, e2)); + assertEquals(Set.of(e1), nonEmpty.getDomain()); + assertEquals(Set.of(e2), nonEmpty.getRange()); + } + + @Test + public void testIntersectionRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph nonEmpty = makeEventGraph(nonEmptyClass, Map.of( + e1, Set.of(e2) + )); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{nonEmpty, empty}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(0, empty.size()); + assertEquals(Set.of(), empty.getDomain()); + assertEquals(Set.of(), empty.getRange()); + + assertEquals(1, nonEmpty.size()); + assertTrue(nonEmpty.contains(e1, e2)); + assertEquals(Set.of(e1), nonEmpty.getDomain()); + assertEquals(Set.of(e2), nonEmpty.getRange()); + } + + @Test + public void testIntersectionBothEmpty() { + // given + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph anotherEmpty = makeEventGraph(nonEmptyClass, Map.of()); + + // when + EventGraph result = getFunction(resultClass, "intersection").apply(new EventGraph[]{empty, anotherEmpty}); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(0, empty.size()); + assertEquals(0, anotherEmpty.size()); + } + + @Test + public void testDifferenceLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph nonEmpty = makeEventGraph(nonEmptyClass, Map.of( + e1, Set.of(e2) + )); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(empty, nonEmpty); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(Set.of(), result.getDomain()); + assertEquals(Set.of(), result.getRange()); + + assertEquals(0, empty.size()); + assertEquals(Set.of(), empty.getDomain()); + assertEquals(Set.of(), empty.getRange()); + + assertEquals(1, nonEmpty.size()); + assertTrue(nonEmpty.contains(e1, e2)); + assertEquals(Set.of(e1), nonEmpty.getDomain()); + assertEquals(Set.of(e2), nonEmpty.getRange()); + } + + @Test + public void testDifferenceRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph nonEmpty = makeEventGraph(nonEmptyClass, Map.of( + e1, Set.of(e2) + )); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(nonEmpty, empty); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(1, result.size()); + assertTrue(result.contains(e1, e2)); + assertEquals(Set.of(e1), result.getDomain()); + assertEquals(Set.of(e2), result.getRange()); + + assertEquals(1, nonEmpty.size()); + assertTrue(nonEmpty.contains(e1, e2)); + assertEquals(Set.of(e1), nonEmpty.getDomain()); + assertEquals(Set.of(e2), nonEmpty.getRange()); + + assertEquals(0, empty.size()); + assertEquals(Set.of(), empty.getDomain()); + assertEquals(Set.of(), empty.getRange()); + } + + @Test + public void testDifferenceBothEmpty() { + // given + EventGraph empty = makeEventGraph(emptyClass, Map.of()); + EventGraph anotherEmpty = makeEventGraph(nonEmptyClass, Map.of()); + + // when + EventGraph result = getDifferenceFunction(resultClass).apply(empty, anotherEmpty); + + // then + assertTrue(resultClass.isAssignableFrom(result.getClass())); + + assertEquals(0, result.size()); + assertEquals(0, empty.size()); + assertEquals(0, anotherEmpty.size()); + } + + private Function getFunction(Class cls, String name) { + return (operands) -> { + try { + Method method = cls.getMethod(name, EventGraph[].class); + return (EventGraph) method.invoke(null, new Object[]{operands}); + } catch (NoSuchMethodException | IllegalAccessException | InvocationTargetException e) { + throw new RuntimeException(e); + } + }; + } + + private BiFunction getDifferenceFunction(Class cls) { + return (left, right) -> { + try { + Method method = cls.getMethod("difference", EventGraph.class, EventGraph.class); + return (EventGraph) method.invoke(null, left, right); + } catch (NoSuchMethodException | IllegalAccessException | InvocationTargetException e) { + throw new RuntimeException(e); + } + }; + } + + private EventGraph makeEventGraph(Class cls, Map> data) { + if (cls.isMemberClass() && cls.isAssignableFrom(ImmutableMapEventGraph.EmptyEventGraph.class)) { + assertTrue(data.isEmpty()); + return ImmutableMapEventGraph.empty(); + } + if (cls.isMemberClass() && cls.isAssignableFrom(LazyEventGraph.EmptyEventGraph.class)) { + assertTrue(data.isEmpty()); + return LazyEventGraph.empty(); + } + if (cls.isAssignableFrom(MapEventGraph.class)) { + return new MapEventGraph(data); + } + if (cls.isAssignableFrom(ImmutableMapEventGraph.class)) { + return new ImmutableMapEventGraph(data); + } + if (cls.isAssignableFrom(LazyEventGraph.class)) { + Set range = data.values().stream().flatMap(Collection::stream).collect(Collectors.toSet()); + return new LazyEventGraph(data.keySet(), range, (e1, e2) -> data.getOrDefault(e1, Set.of()).contains(e2)); + } + throw new RuntimeException("Cannot resolve constructor for class " + cls.getSimpleName()); + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphTest.java new file mode 100644 index 0000000000..5de9a41666 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/EmptyEventGraphTest.java @@ -0,0 +1,187 @@ +package com.dat3m.dartagnan.wmm.utils.graph.immutable; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.Skip; +import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.IOException; +import java.util.Arrays; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +import static org.junit.Assert.*; + +@RunWith(Parameterized.class) +public class EmptyEventGraphTest { + + private final Class cls; + + public EmptyEventGraphTest(Class cls) { + this.cls = cls; + } + + @Parameterized.Parameters + public static Iterable data() throws IOException { + return Arrays.asList(new Object[][]{ + {ImmutableMapEventGraph.EmptyEventGraph.class}, + {LazyEventGraph.EmptyEventGraph.class}, + }); + } + + private static EventGraph makeEventGraph(Class cls) { + if (cls.isAssignableFrom(ImmutableMapEventGraph.EmptyEventGraph.class)) { + return ImmutableMapEventGraph.empty(); + } + if (cls.isAssignableFrom(LazyEventGraph.EmptyEventGraph.class)) { + return LazyEventGraph.empty(); + } + throw new RuntimeException("Cannot resolve constructor for class " + cls.getSimpleName()); + } + + @Test + public void testIsSingleton() { + // when + EventGraph first = makeEventGraph(cls); + EventGraph second = makeEventGraph(cls); + + // then + assertSame(first, second); + } + + @Test + public void testIsEmpty() { + // when + EventGraph empty = makeEventGraph(cls); + + // then + assertTrue(empty.isEmpty()); + } + + @Test + public void testSize() { + // when + EventGraph empty = makeEventGraph(cls); + + // then + assertEquals(0, empty.size()); + } + + @Test + public void testContains() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + + // when + EventGraph empty = makeEventGraph(cls); + + // then + assertFalse(empty.contains(e1, e2)); + } + + @Test + public void testInverse() { + // given + EventGraph empty = makeEventGraph(cls); + + // when + EventGraph inverse = empty.inverse(); + + // then + assertSame(empty, inverse); + } + + @Test + public void testFilter() { + // given + EventGraph empty = makeEventGraph(cls); + + // when + EventGraph inverse = empty.filter((x, y) -> true); + + // then + assertSame(empty, inverse); + } + + @Test + public void testOutMap() { + // given + EventGraph empty = makeEventGraph(cls); + + // when + Map> map = empty.getOutMap(); + + // then + assertTrue(map.isEmpty()); + } + + @Test + public void testInMap() { + // given + EventGraph empty = makeEventGraph(cls); + + // when + Map> map = empty.getInMap(); + + // then + assertTrue(map.isEmpty()); + } + + @Test + public void testGetDomain() { + // given + EventGraph empty = makeEventGraph(cls); + + // when + Set set = empty.getDomain(); + + // then + assertTrue(set.isEmpty()); + } + + @Test + public void testGetRange() { + // given + EventGraph empty = makeEventGraph(cls); + + // when + Set set = empty.getRange(); + + // then + assertTrue(set.isEmpty()); + } + + @Test + public void testGetRangeEvent() { + // given + Event e = new Skip(); + EventGraph empty = makeEventGraph(cls); + + // when + Set set = empty.getRange(e); + + // then + assertTrue(set.isEmpty()); + } + + @Test + public void testApply() { + // given + EventGraph empty = makeEventGraph(cls); + Set set = new HashSet<>(); + + // when + empty.apply((x, y) -> { + if (x.equals(y)) { + set.add(x); + } + }); + + // then + assertTrue(set.isEmpty()); + } +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraphTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraphTest.java new file mode 100644 index 0000000000..04c0376fb6 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/graph/mutable/MutableEventGraphTest.java @@ -0,0 +1,755 @@ +package com.dat3m.dartagnan.wmm.utils.graph.mutable; + +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.Skip; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.io.IOException; +import java.util.Arrays; +import java.util.Map; +import java.util.Set; + +import static org.junit.Assert.*; + +@RunWith(Parameterized.class) +public class MutableEventGraphTest { + + private final Class cls; + + public MutableEventGraphTest(Class cls) { + this.cls = cls; + } + + @Parameterized.Parameters + public static Iterable data() throws IOException { + return Arrays.asList(new Object[][]{ + {MapEventGraph.class}, + }); + } + + @Test + public void testAddEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // when + boolean result = eventGraph.add(e1, e2); + + // then + assertTrue(result); + assertFalse(eventGraph.isEmpty()); + assertEquals(1, eventGraph.size()); + assertTrue(eventGraph.contains(e1, e2)); + } + + @Test + public void testAddNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2) + )); + + // when + boolean result = eventGraph.add(e1, e1); + + // then + assertTrue(result); + assertFalse(eventGraph.isEmpty()); + assertEquals(2, eventGraph.size()); + assertTrue(eventGraph.contains(e1, e1)); + assertTrue(eventGraph.contains(e1, e2)); + } + + @Test + public void testAddRepeated() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2) + )); + + // when + boolean result1 = eventGraph.add(e1, e2); + boolean result2 = eventGraph.add(e1, e1); + boolean result3 = eventGraph.add(e1, e1); + + // then + assertFalse(result1); + assertTrue(result2); + assertFalse(result3); + assertFalse(eventGraph.isEmpty()); + assertEquals(2, eventGraph.size()); + assertTrue(eventGraph.contains(e1, e2)); + assertFalse(eventGraph.contains(e2, e1)); + } + + @Test + public void testRemoveEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // when + boolean result = eventGraph.remove(e1, e2); + + // then + assertFalse(result); + assertTrue(eventGraph.isEmpty()); + assertEquals(0, eventGraph.size()); + assertFalse(eventGraph.contains(e1, e2)); + } + + @Test + public void testRemoveNonEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e1) + )); + + // when + boolean result = eventGraph.remove(e1, e2); + + // then + assertTrue(result); + assertFalse(eventGraph.isEmpty()); + assertEquals(1, eventGraph.size()); + assertFalse(eventGraph.contains(e1, e2)); + assertTrue(eventGraph.contains(e2, e1)); + } + + @Test + public void testRemoveNonEmptyAllEdges() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e1) + )); + + // when + boolean result1 = eventGraph.remove(e1, e2); + boolean result2 = eventGraph.remove(e2, e1); + + // then + assertTrue(result1); + assertTrue(result2); + assertTrue(eventGraph.isEmpty()); + assertEquals(0, eventGraph.size()); + assertFalse(eventGraph.contains(e1, e2)); + assertFalse(eventGraph.contains(e2, e1)); + } + + @Test + public void testRemoveRepeated() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e1) + )); + + // when + boolean result1 = eventGraph.remove(e1, e2); + boolean result2 = eventGraph.remove(e1, e2); + boolean result3 = eventGraph.remove(e1, e1); + + // then + assertTrue(result1); + assertFalse(result2); + assertFalse(result3); + assertFalse(eventGraph.isEmpty()); + assertEquals(1, eventGraph.size()); + assertFalse(eventGraph.contains(e1, e2)); + assertTrue(eventGraph.contains(e2, e1)); + } + + @Test + public void testAddAllDisjoint() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e3), + e3, Set.of(e3) + )); + boolean result = first.addAll(second); + + // then + assertTrue(result); + + assertEquals(5, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e1, e3)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + assertTrue(first.contains(e3, e3)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e3)); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testAddAllPartial() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + boolean result = first.addAll(second); + + // then + assertTrue(result); + + assertEquals(4, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + assertTrue(first.contains(e3, e3)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testAddAllOverlapping() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e3, Set.of(e1) + )); + boolean result = first.addAll(second); + + // then + assertFalse(result); + + assertEquals(3, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e3, e1)); + } + + @Test + public void testAddAllLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of()); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + boolean result = first.addAll(second); + + // then + assertTrue(result); + + assertEquals(3, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + + assertEquals(3, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e2, e3)); + assertTrue(second.contains(e3, e1)); + } + + @Test + public void testAddAllRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of()); + boolean result = first.addAll(second); + + // then + assertFalse(result); + + assertEquals(3, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + + assertEquals(0, second.size()); + } + + @Test + public void testRemoveAllOverlapping() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3) + )); + boolean result = first.removeAll(second); + + // then + assertTrue(result); + + assertEquals(1, first.size()); + assertTrue(first.contains(e3, e1)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e2, e3)); + } + + @Test + public void testRemoveAllPartial() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + boolean result = first.removeAll(second); + + // then + assertTrue(result); + + assertEquals(2, first.size()); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testRemoveAllDisjoint() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e3), + e3, Set.of(e3) + )); + boolean result = first.removeAll(second); + + // then + assertFalse(result); + + assertEquals(3, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e3)); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testRemoveAllEmptied() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1, e3) + )); + boolean result = first.removeAll(second); + + // then + assertTrue(result); + + assertEquals(0, first.size()); + + assertEquals(4, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e2, e3)); + assertTrue(second.contains(e3, e1)); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testRemoveAllLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of()); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + boolean result = first.removeAll(second); + + // then + assertFalse(result); + + assertEquals(0, first.size()); + + assertEquals(3, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e2, e3)); + assertTrue(second.contains(e3, e1)); + } + + @Test + public void testRemoveAllRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of()); + boolean result = first.removeAll(second); + + // then + assertFalse(result); + + assertEquals(3, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + + assertEquals(0, second.size()); + } + + @Test + public void testRetainAllOverlappingSubset() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3) + )); + boolean result = first.retainAll(second); + + // then + assertTrue(result); + + assertEquals(2, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e2, e3)); + } + + @Test + public void testRetainAllOverlappingSuperset() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1, e3) + )); + boolean result = first.retainAll(second); + + // then + assertFalse(result); + + assertEquals(3, first.size()); + assertTrue(first.contains(e1, e2)); + assertTrue(first.contains(e2, e3)); + assertTrue(first.contains(e3, e1)); + + assertEquals(4, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e2, e3)); + assertTrue(second.contains(e3, e1)); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testRetainAllPartial() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + boolean result = first.retainAll(second); + + // then + assertTrue(result); + + assertEquals(1, first.size()); + assertTrue(first.contains(e1, e2)); + + assertEquals(2, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testRetainAllEmptied() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e3, Set.of(e3) + )); + boolean result = first.retainAll(second); + + // then + assertTrue(result); + + assertEquals(0, first.size()); + + assertEquals(1, second.size()); + assertTrue(second.contains(e3, e3)); + } + + @Test + public void testRetainAllLeftEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of()); + MutableEventGraph second = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + boolean result = first.retainAll(second); + + // then + assertFalse(result); + + assertEquals(0, first.size()); + + assertEquals(3, second.size()); + assertTrue(second.contains(e1, e2)); + assertTrue(second.contains(e2, e3)); + assertTrue(second.contains(e3, e1)); + } + + @Test + public void testRetainAllRightEmpty() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph first = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e2, Set.of(e3), + e3, Set.of(e1) + )); + MutableEventGraph second = makeEventGraph(cls, Map.of()); + boolean result = first.retainAll(second); + + // then + assertTrue(result); + + assertEquals(0, first.size()); + + assertEquals(0, second.size()); + } + + @Test + public void testAddRangeEvent() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2), + e3, Set.of(e3) + )); + + // when + assertFalse(eventGraph.addRange(e1, Set.of(e2))); + assertTrue(eventGraph.addRange(e1, Set.of(e2, e3))); + assertFalse(eventGraph.addRange(e3, Set.of(e3))); + assertTrue(eventGraph.addRange(e3, Set.of(e1, e3))); + assertFalse(eventGraph.addRange(e1, Set.of())); + + // then + assertEquals(4, eventGraph.size()); + assertTrue(eventGraph.contains(e1, e2)); + assertTrue(eventGraph.contains(e1, e3)); + assertTrue(eventGraph.contains(e3, e1)); + assertTrue(eventGraph.contains(e3, e3)); + } + + @Test + public void testRemoveIf() { + // given + Event e1 = new Skip(); + Event e2 = new Skip(); + Event e3 = new Skip(); + + // when + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of( + e1, Set.of(e2, e3), + e2, Set.of(e1), + e3, Set.of(e3) + )); + eventGraph.removeIf(Object::equals); + + // then + assertEquals(3, eventGraph.size()); + assertTrue(eventGraph.contains(e1, e2)); + assertTrue(eventGraph.contains(e1, e3)); + assertTrue(eventGraph.contains(e2, e1)); + } + + @Test + public void testRemoveIfEmpty() { + // given + MutableEventGraph eventGraph = makeEventGraph(cls, Map.of()); + + // when + eventGraph.removeIf(Object::equals); + + // then + assertTrue(eventGraph.isEmpty()); + } + + private MutableEventGraph makeEventGraph(Class cls, Map> data) { + if (cls.isAssignableFrom(MapEventGraph.class)) { + return new MapEventGraph(data); + } + throw new RuntimeException("Cannot resolve constructor for class " + cls.getSimpleName()); + } +}