From 69e65141b8f1030ff5886e09f02e346c7f885ade Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 6 Jun 2025 14:53:36 +0200 Subject: [PATCH 01/17] Support unary predicates in cat --- dartagnan/src/main/antlr4/Cat.g4 | 6 +- .../dat3m/dartagnan/encoding/EncodeSets.java | 30 ++++- .../dat3m/dartagnan/encoding/IREvaluator.java | 10 ++ .../dartagnan/encoding/LazyEncodeSets.java | 4 +- .../dat3m/dartagnan/encoding/WmmEncoder.java | 38 +++++- .../dartagnan/parsers/cat/VisitorCat.java | 123 ++++++++---------- .../dartagnan/program/filter/Filter.java | 14 +- .../predicates/misc/PredicateVisitor.java | 2 +- .../solver/caat/predicates/sets/Element.java | 2 +- .../caat/predicates/sets/SetPredicate.java | 5 - .../sets/derived/IntersectionSet.java | 52 ++++---- .../derived/ProjectionSet.java} | 21 +-- .../predicates/sets/derived/UnionSet.java | 25 ++-- .../solver/caat/reasoning/Reasoner.java | 20 +-- .../solver/caat4wmm/ExecutionGraph.java | 56 +++++--- .../solver/caat4wmm/RefinementModel.java | 2 +- .../basePredicates/AbstractWMMSet.java | 29 +++++ .../DynamicDefaultWMMGraph.java | 1 + .../basePredicates/DynamicDefaultWMMSet.java | 50 +++++++ .../basePredicates/MaterializedWMMSet.java | 56 ++++++++ .../model/ExecutionModelManager.java | 116 ++++++++++++----- .../solving/RefinementSolver.java | 17 ++- .../com/dat3m/dartagnan/wmm/Constraint.java | 5 +- .../com/dat3m/dartagnan/wmm/Relation.java | 28 +++- .../java/com/dat3m/dartagnan/wmm/Wmm.java | 55 ++++---- .../wmm/analysis/LazyRelationAnalysis.java | 42 ++++-- .../wmm/analysis/NativeRelationAnalysis.java | 76 +++++++---- .../dat3m/dartagnan/wmm/axiom/Acyclicity.java | 2 + .../dartagnan/wmm/axiom/Irreflexivity.java | 2 + .../dartagnan/wmm/definition/AMOPairs.java | 1 + .../wmm/definition/CASDependency.java | 1 + .../wmm/definition/CartesianProduct.java | 32 +++-- .../dartagnan/wmm/definition/Coherence.java | 1 + .../dartagnan/wmm/definition/Composition.java | 3 + .../dartagnan/wmm/definition/Difference.java | 1 + .../definition/DirectAddressDependency.java | 1 + .../definition/DirectControlDependency.java | 1 + .../wmm/definition/DirectDataDependency.java | 1 + .../{DomainIdentity.java => Domain.java} | 13 +- .../dartagnan/wmm/definition/External.java | 1 + .../dartagnan/wmm/definition/Internal.java | 1 + .../wmm/definition/Intersection.java | 1 + .../dartagnan/wmm/definition/Inverse.java | 2 + .../dartagnan/wmm/definition/LXSXPairs.java | 1 + .../wmm/definition/LinuxCriticalSections.java | 1 + .../wmm/definition/ProgramOrder.java | 1 + .../{RangeIdentity.java => Range.java} | 10 +- .../dartagnan/wmm/definition/ReadFrom.java | 1 + .../wmm/definition/SameLocation.java | 1 + .../dartagnan/wmm/definition/SameScope.java | 1 + .../wmm/definition/SameVirtualLocation.java | 1 + .../dartagnan/wmm/definition/SetIdentity.java | 21 +-- .../dartagnan/wmm/definition/SyncBar.java | 1 + .../dartagnan/wmm/definition/SyncFence.java | 1 + .../dartagnan/wmm/definition/SyncWith.java | 1 + .../dartagnan/wmm/definition/TagSet.java | 36 +++++ .../wmm/definition/TransitiveClosure.java | 2 + .../dat3m/dartagnan/wmm/definition/Union.java | 1 + .../processing/MergeEquivalentRelations.java | 10 +- .../dartagnan/wmm/utils/ConstraintCopier.java | 17 ++- 60 files changed, 721 insertions(+), 335 deletions(-) rename dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/{relationGraphs/derived/ProjectionIdentityGraph.java => sets/derived/ProjectionSet.java} (68%) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/AbstractWMMSet.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/MaterializedWMMSet.java rename dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/{DomainIdentity.java => Domain.java} (70%) rename dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/{RangeIdentity.java => Range.java} (70%) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4 index d1494b4253..af1dc930ff 100755 --- a/dartagnan/src/main/antlr4/Cat.g4 +++ b/dartagnan/src/main/antlr4/Cat.g4 @@ -48,8 +48,8 @@ expression | e1 = expression BSLASH e2 = expression # exprMinus | e1 = expression SEMI e2 = expression # exprComposition | e1 = expression BAR e2 = expression # exprUnion - | LBRAC DOMAIN LPAR e = expression RPAR RBRAC # exprDomainIdentity - | LBRAC RANGE LPAR e = expression RPAR RBRAC # exprRangeIdentity + | DOMAIN LPAR e = expression RPAR # exprDomain + | RANGE LPAR e = expression RPAR # exprRange | (TOID LPAR e = expression RPAR | LBRAC e = expression RBRAC) # exprIdentity | LPAR e = expression RPAR # expr | n = NAME # exprBasic @@ -105,7 +105,7 @@ COMMA : ','; DOMAIN : 'domain'; RANGE : 'range'; -NEW : 'new'; +NEW : '[n|N]ew'; FLAG : 'flag'; UNDEFINED : 'undefined_unless'; 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 d2f239da5d..6a8054704a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java @@ -84,7 +84,7 @@ public Map visitComposition(Composition comp) { } @Override - public Map visitDomainIdentity(DomainIdentity domId) { + public Map visitDomain(Domain domId) { final RelationAnalysis.Knowledge k1 = ra.getKnowledge(domId.getOperand()); Map> out = k1.getMaySet().getOutMap(); MutableEventGraph result = new MapEventGraph(); @@ -99,7 +99,7 @@ public Map visitDomainIdentity(DomainIdentity domId) { } @Override - public Map visitRangeIdentity(RangeIdentity rangeId) { + public Map visitRange(Range rangeId) { final RelationAnalysis.Knowledge k1 = ra.getKnowledge(rangeId.getOperand()); Map> in = k1.getMaySet().getInMap(); MutableEventGraph result = new MapEventGraph(); @@ -113,6 +113,13 @@ public Map visitRangeIdentity(RangeIdentity rangeId) { return Map.of(rangeId.getOperand(), result); } + @Override + public Map visitSetIdentity(SetIdentity id) { + final RelationAnalysis.Knowledge k1 = ra.getKnowledge(id.getDomain()); + return Map.of(id.getDomain(), + news.filter((e1, e2) -> k1.getMaySet().contains(e1, e2) && !k1.getMustSet().contains(e1, e2))); + } + @Override public Map visitInverse(Inverse inv) { final RelationAnalysis.Knowledge k1 = ra.getKnowledge(inv.getOperand()); @@ -120,6 +127,25 @@ public Map visitInverse(Inverse inv) { news.inverse().filter((e1, e2) -> k1.getMaySet().contains(e1, e2) && !k1.getMustSet().contains(e1, e2))); } + @Override + public Map visitProduct(CartesianProduct product) { + final RelationAnalysis.Knowledge k1 = ra.getKnowledge(product.getDomain()); + final RelationAnalysis.Knowledge k2 = ra.getKnowledge(product.getRange()); + final MutableEventGraph set1 = new MapEventGraph(); + final MutableEventGraph set2 = new MapEventGraph(); + for (Event e1 : news.getDomain()) { + if (k1.getMaySet().contains(e1, e1) && !k1.getMustSet().contains(e1, e1)) { + set1.add(e1, e1); + } + for (Event e2 : news.getRange(e1)) { + if (k2.getMaySet().contains(e2, e2) && !k2.getMustSet().contains(e2, e2)) { + set2.add(e2, e2); + } + } + } + return Map.of(product.getDomain(), set1, product.getRange(), set2); + } + @Override public Map visitTransitiveClosure(TransitiveClosure trans) { final Relation rel = trans.getDefinedRelation(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java index cdd96b12ff..20c545e63d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java @@ -112,7 +112,17 @@ public TypedValue size(MemoryObject memoryObject) { // ==================================================================================== // Memory Model + public boolean hasElement(Relation rel, Event a) { + Preconditions.checkArgument(rel.isUnaryRelation(), "Non-unary relation %s", rel); + return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, a))); + } + + public boolean hasElement(EncodingContext.EdgeEncoder edgeEncoder, Event a) { + return TRUE.equals(smtModel.evaluate(edgeEncoder.encode(a, a))); + } + public boolean hasEdge(Relation rel, Event a, Event b) { + Preconditions.checkArgument(rel.isBinaryRelation(), "Non-binary relation %s", rel); return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, b))); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java index b051493c02..9ed9b91c44 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java @@ -152,7 +152,7 @@ public Boolean visitSyncWith(SyncWith definition) { } @Override - public Boolean visitDomainIdentity(DomainIdentity definition) { + public Boolean visitDomain(Domain definition) { if (doUpdateSelf(definition)) { long start = System.currentTimeMillis(); MutableEventGraph operandUpdate = new MapEventGraph(); @@ -167,7 +167,7 @@ public Boolean visitDomainIdentity(DomainIdentity definition) { } @Override - public Boolean visitRangeIdentity(RangeIdentity definition) { + public Boolean visitRange(Range definition) { if (doUpdateSelf(definition)) { long start = System.currentTimeMillis(); MutableEventGraph operandUpdate = new MapEventGraph(); 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 46aa229fa7..73fb9e9e71 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -378,7 +378,7 @@ public Void visitComposition(Composition comp) { } @Override - public Void visitDomainIdentity(DomainIdentity domId) { + public Void visitDomain(Domain domId) { final Relation rel = domId.getDefinedRelation(); final Relation r1 = domId.getOperand(); Map> mayOut = ra.getKnowledge(r1).getMaySet().getOutMap(); @@ -396,7 +396,7 @@ public Void visitDomainIdentity(DomainIdentity domId) { } @Override - public Void visitRangeIdentity(RangeIdentity rangeId) { + public Void visitRange(Range rangeId) { final Relation rel = rangeId.getDefinedRelation(); final Relation r1 = rangeId.getOperand(); Map> mayIn = ra.getKnowledge(r1).getMaySet().getInMap(); @@ -444,6 +444,22 @@ public Void visitTransitiveClosure(TransitiveClosure trans) { return null; } + @Override + public Void visitSetIdentity(SetIdentity id) { + final Relation rel = id.getDefinedRelation(); + final Relation r1 = id.getDomain(); + EventGraph mustSet = ra.getKnowledge(rel).getMustSet(); + EncodingContext.EdgeEncoder enc0 = context.edge(rel); + EncodingContext.EdgeEncoder enc1 = context.edge(r1); + encodeSets.get(rel).apply((e1, e2) -> + enc.add(bmgr.equivalence( + enc0.encode(e1, e2), + mustSet.contains(e1, e2) ? + execution(e1, e2) : + enc1.encode(e1, e2)))); + return null; + } + @Override public Void visitInverse(Inverse inv) { final Relation rel = inv.getDefinedRelation(); @@ -460,6 +476,24 @@ public Void visitInverse(Inverse inv) { return null; } + @Override + public Void visitProduct(CartesianProduct product) { + final Relation rel = product.getDefinedRelation(); + final Relation r1 = product.getDomain(); + final Relation r2 = product.getRange(); + EventGraph mustSet = ra.getKnowledge(rel).getMustSet(); + EncodingContext.EdgeEncoder enc0 = context.edge(rel); + EncodingContext.EdgeEncoder enc1 = context.edge(r1); + EncodingContext.EdgeEncoder enc2 = context.edge(r2); + encodeSets.get(rel).apply((e1, e2) -> + enc.add(bmgr.equivalence( + enc0.encode(e1, e2), + mustSet.contains(e1, e2) ? + execution(e1, e2) : + bmgr.and(enc1.encode(e1, e1), enc2.encode(e2, e2))))); + return null; + } + @Override public Void visitInternalDataDependency(DirectDataDependency idd) { return visitDirectDependency(idd.getDefinedRelation()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index 71a4e8a2d9..7e372ccae9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -8,7 +8,6 @@ import com.dat3m.dartagnan.parsers.CatLexer; import com.dat3m.dartagnan.parsers.CatParser; import com.dat3m.dartagnan.parsers.CatParser.*; -import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.RelationNameRepository; @@ -133,7 +132,7 @@ public Void visitAxiomDefinition(AxiomDefinitionContext ctx) { } private String createUniqueName(String name) { - if (namespace.containsKey(name) && !nameOccurrenceCounter.containsKey(name)) { + if ((namespace.containsKey(name) || wmm.getRelation(name) != null) && !nameOccurrenceCounter.containsKey(name)) { // If we have already seen the name, but not counted it yet, we do so now. nameOccurrenceCounter.put(name, 1); } @@ -150,13 +149,6 @@ public Void visitLetDefinition(LetDefinitionContext ctx) { if (definedPredicate instanceof Relation rel) { String alias = createUniqueName(name); wmm.addAlias(alias, rel); - } else if (definedPredicate instanceof Filter filter) { - String alias = createUniqueName(name); - // NOTE: The support for re-defined filters is limited: - // The Wmm will recognize all aliases, but the filter itself has a single name, - // which we set to the most recent alias we used. - filter.setName(alias); - wmm.addFilter(filter); } namespace.put(name, definedPredicate); return null; @@ -214,15 +206,30 @@ public Object visitExpr(ExprContext ctx) { @Override public Object visitExprNew(ExprNewContext ctx) { - return addDefinition(new Free(wmm.newRelation())); + final boolean unary = ctx.call.getText().equals("New"); + return addDefinition(new Free(wmm.newRelation(unary))); } @Override public Object visitExprBasic(ExprBasicContext ctx) { - String name = ctx.n.getText(); - Object predicate = namespace.computeIfAbsent(name, - k -> RelationNameRepository.contains(name) ? wmm.getOrCreatePredefinedRelation(k) : Filter.byTag(k)); - return predicate; + final String name = ctx.n.getText(); + final Object boundObject = namespace.get(name); + if (boundObject != null) { + return boundObject; + } + if (RelationNameRepository.contains(name)) { + return wmm.getOrCreatePredefinedRelation(name); + } + final Relation namedRelation = wmm.getRelation(name); + final Relation existingSet = namedRelation != null && namedRelation.getDefinition() instanceof TagSet s && s.getTag().equals(name) ? + namedRelation : wmm.getRelations().stream() + .filter(r -> r.getDefinition() instanceof TagSet s && s.getTag().equals(name)) + .findAny().orElse(null); + if (existingSet != null) { + return existingSet; + } + final Relation newRelation = namedRelation != null ? wmm.newRelation(true) : wmm.newRelation(name, true); + return addDefinition(new TagSet(newRelation, name)); } @Override @@ -255,52 +262,43 @@ public Object visitExprCall(ExprCallContext ctx) { @Override public Object visitExprIntersection(ExprIntersectionContext c) { - Optional defRel = getAndResetRelationToBeDefined(); - Object o1 = c.e1.accept(this); - Object o2 = c.e2.accept(this); - if (o1 instanceof Relation) { - Relation r0 = defRel.orElseGet(wmm::newRelation); - return addDefinition(new Intersection(r0, (Relation) o1, parseAsRelation(o2, c))); - } - return Filter.intersection(parseAsFilter(o1, c), parseAsFilter(o2, c)); + final Optional defRel = getAndResetRelationToBeDefined(); + final Relation r1 = parseAsRelation(c.e1); + final Relation r2 = parseAsRelation(c.e2); + final Relation r0 = defRel.orElseGet(() -> wmm.newRelation(r1.isUnaryRelation())); + return addDefinition(new Intersection(r0, r1, r2)); } @Override public Object visitExprMinus(ExprMinusContext c) { checkNoRecursion(c); - Object o1 = c.e1.accept(this); - Object o2 = c.e2.accept(this); - if (o1 instanceof Relation) { - Relation r0 = wmm.newRelation(); - return addDefinition(new Difference(r0, (Relation) o1, parseAsRelation(o2, c))); - } - return Filter.difference(parseAsFilter(o1, c), parseAsFilter(o2, c)); + final Relation r1 = parseAsRelation(c.e1); + final Relation r2 = parseAsRelation(c.e2); + final Relation r0 = wmm.newRelation(r1.isUnaryRelation()); + return addDefinition(new Difference(r0, r1, r2)); } @Override public Object visitExprUnion(ExprUnionContext c) { - Optional defRel = getAndResetRelationToBeDefined(); - Object o1 = c.e1.accept(this); - Object o2 = c.e2.accept(this); - if (o1 instanceof Relation) { - Relation r0 = defRel.orElseGet(wmm::newRelation); - return addDefinition(new Union(r0, (Relation) o1, parseAsRelation(o2, c))); - } - return Filter.union(parseAsFilter(o1, c), parseAsFilter(o2, c)); + final Optional defRel = getAndResetRelationToBeDefined(); + final Relation r1 = parseAsRelation(c.e1); + final Relation r2 = parseAsRelation(c.e2); + final Relation r0 = defRel.orElseGet(() -> wmm.newRelation(r1.isUnaryRelation())); + return addDefinition(new Union(r0, r1, r2)); } @Override public Object visitExprComplement(ExprComplementContext c) { checkNoRecursion(c); - Object o1 = c.e.accept(this); - Filter visible = Filter.byTag(VISIBLE); - if (o1 instanceof Relation) { - Relation r0 = wmm.newRelation(); - Relation all = wmm.newRelation(); - Relation r1 = wmm.addDefinition(new CartesianProduct(all, visible, visible)); - return addDefinition(new Difference(r0, r1, (Relation) o1)); + final Relation r1 = parseAsRelation(c.e); + final Relation visible = wmm.newSet(); + wmm.addDefinition(new TagSet(visible, VISIBLE)); + final Relation r0 = wmm.newRelation(r1.isUnaryRelation()); + final Relation all = r1.isUnaryRelation() ? visible : wmm.newRelation(); + if (!r1.isUnaryRelation()) { + wmm.addDefinition(new CartesianProduct(all, visible, visible)); } - return Filter.difference(visible, parseAsFilter(o1, c)); + return addDefinition(new Difference(r0, all, r1)); } @Override @@ -334,17 +332,19 @@ public Relation visitExprTransRef(ExprTransRefContext c) { } @Override - public Relation visitExprDomainIdentity(ExprDomainIdentityContext c) { - Relation r0 = getAndResetRelationToBeDefined().orElseGet(wmm::newRelation); + public Relation visitExprDomain(ExprDomainContext c) { + checkNoRecursion(c); + Relation r0 = wmm.newSet(); Relation r1 = parseAsRelation(c.e); - return addDefinition(new DomainIdentity(r0, r1)); + return addDefinition(new Domain(r0, r1)); } @Override - public Relation visitExprRangeIdentity(ExprRangeIdentityContext c) { - Relation r0 = getAndResetRelationToBeDefined().orElseGet(wmm::newRelation); + public Relation visitExprRange(ExprRangeContext c) { + checkNoRecursion(c); + Relation r0 = wmm.newSet(); Relation r1 = parseAsRelation(c.e); - return addDefinition(new RangeIdentity(r0, r1)); + return addDefinition(new Range(r0, r1)); } @Override @@ -357,17 +357,17 @@ public Relation visitExprOptional(ExprOptionalContext c) { @Override public Relation visitExprIdentity(ExprIdentityContext c) { Relation r0 = getAndResetRelationToBeDefined().orElseGet(wmm::newRelation); - Filter s1 = parseAsFilter(c.e); - return addDefinition(new SetIdentity(r0, s1)); + final Relation r1 = parseAsRelation(c.e); + return addDefinition(new SetIdentity(r0, r1)); } @Override public Relation visitExprCartesian(ExprCartesianContext c) { checkNoRecursion(c); Relation r0 = wmm.newRelation(); - Filter s1 = parseAsFilter(c.e1); - Filter s2 = parseAsFilter(c.e2); - return addDefinition(new CartesianProduct(r0, s1, s2)); + Relation r1 = parseAsRelation(c.e1); + Relation r2 = parseAsRelation(c.e2); + return addDefinition(new CartesianProduct(r0, r1, r2)); } // ============================ Utility ============================ @@ -403,17 +403,6 @@ private Relation parseAsRelation(Object o, ExpressionContext t) { throw new ParsingException("Expected relation, got " + o.getClass().getSimpleName() + " " + o + " from expression " + t.getText()); } - private Filter parseAsFilter(ExpressionContext t) { - return parseAsFilter(t.accept(this), t); - } - - private static Filter parseAsFilter(Object o, ExpressionContext t) { - if (o instanceof Filter filter) { - return filter; - } - throw new ParsingException("Expected set, got " + o.getClass().getSimpleName() + " " + o + " from expression " + t.getText()); - } - private static CatParser getParser(CharStream input) { final Lexer lexer = new CatLexer(input); lexer.addErrorListener(new AbortErrorListener()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java index 8c91a0514e..4681c42b2b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java @@ -6,20 +6,8 @@ import java.util.Map; /* -TODO: Filters are currently used in two distinct settings: - (1) as general ways to extract program-events - (2) as unary predicates in the Wmm - These two use-cases have conflicting requirements: - Use-case (1) needs the "apply"-method but not require named filters. - Use-case (2) requires named filters, but cannot (in general) support an "apply"-method (dynamic unary predicates). - - SOLUTION: Use-case (1) is rather rare and can be replaced by explicit checking for tags - (e.g. getEvents().stream().filter(e -> e.hasTag(TAG1) &&/|| e.hasTag(TAG2)). - With only use-case (2), Filters can be lifted to proper unary predicates - (no "apply"-method, but lower and upper bounds (must/may) instead). - +Filters are used as general ways to extract program-events. */ - public abstract class Filter { protected String name; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java index c3b66c2b39..74e490ed5c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/misc/PredicateVisitor.java @@ -17,7 +17,6 @@ public interface PredicateVisitor { default TRet visitCartesian(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); } default TRet visitInverse(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); } default TRet visitSetIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); } - default TRet visitProjectionIdentity(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); } default TRet visitReflexiveClosure(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); } default TRet visitTransitiveClosure(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); } default TRet visitRecursiveGraph(RelationGraph graph, TData data, TContext context) { return visitGraph(graph, data, context); } @@ -26,6 +25,7 @@ public interface PredicateVisitor { // ============================================== SetPredicates ============================================== default TRet visitSet(SetPredicate set, TData data, TContext context) { return visit(set, data, context); } + default TRet visitProjection(SetPredicate set, TData data, TContext context) { return visitSet(set, data, context); } default TRet visitSetUnion(SetPredicate set, TData data, TContext context) { return visitSet(set, data, context); } default TRet visitSetIntersection(SetPredicate set, TData data, TContext context) { return visitSet(set, data, context); } default TRet visitSetDifference(SetPredicate set, TData data, TContext context) { return visitSet(set, data, context); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/Element.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/Element.java index 170df1f489..55ab4b524a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/Element.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/Element.java @@ -18,7 +18,7 @@ public Element(int id) { } @Override - public Element with(int time, int derivationLength) { return new Element(dId, time, derivLength); } + public Element with(int time, int derivationLength) { return new Element(dId, time, derivationLength); } @Override public Element withTime(int time) { return with(time, derivLength); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/SetPredicate.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/SetPredicate.java index 8dd0124da9..021fe1692f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/SetPredicate.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/SetPredicate.java @@ -7,7 +7,6 @@ import java.util.Collection; import java.util.Iterator; -import java.util.List; import java.util.Set; import java.util.stream.Stream; @@ -16,10 +15,6 @@ public interface SetPredicate extends CAATPredicate { @Override Collection forwardPropagate(CAATPredicate changedSource, Collection added); - @Override - List getDependencies(); // SetPredicates only depend on other SetPredicates - // In case we add something like projections, we would also have sets dependent on graphs - Element get(Element e); // Gets the metadata associated with // We only require a stream implementation, because it is the easiest diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/IntersectionSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/IntersectionSet.java index 25e8cae4b4..7c69eee86d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/IntersectionSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/IntersectionSet.java @@ -9,45 +9,37 @@ import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate; import java.util.*; +import java.util.stream.Stream; public class IntersectionSet extends MaterializedSet { - private final SetPredicate first; - private final SetPredicate second; + private final SetPredicate[] operands; @Override public List getDependencies() { - return Arrays.asList(first, second); + return Arrays.asList(operands); } - public SetPredicate getFirst() { return first; } - public SetPredicate getSecond() { return second; } - - public IntersectionSet(SetPredicate first, SetPredicate second) { - this.first = first; - this.second = second; + public IntersectionSet(SetPredicate... o) { + operands = o; } - private Element derive(Element a, Element b) { - return a.with(Math.max(a.getTime(), b.getTime()), - Math.max(a.getDerivationLength(), b.getDerivationLength()) + 1); + private Element derive(Element... elements) { + final int time = Stream.of(elements).mapToInt(Element::getTime).max().orElseThrow(); + final int length = Stream.of(elements).mapToInt(Element::getDerivationLength).max().orElseThrow(); + return elements[0].with(time, length + 1); } @Override public void repopulate() { - if (first.getEstimatedSize() < second.getEstimatedSize()) { - for (Element e1 : first.elements()) { - Element e2 = second.get(e1); - if (e2 != null) { - simpleSet.add(derive(e1, e2)); - } + final SetPredicate smallest = Stream.of(operands).min(Comparator.comparingInt(CAATPredicate::getEstimatedSize)).orElseThrow(); + for (Element e1 : smallest.elements()) { + final Element[] elements = new Element[operands.length]; + for (int i = 0; i < operands.length; i++) { + elements[i] = operands[i] == smallest ? e1 : operands[i].get(e1); } - } else { - for (Element e2 : second.elements()) { - Element e1 = first.get(e2); - if (e1 != null) { - simpleSet.add(derive(e1, e2)); - } + if (Stream.of(elements).allMatch(Objects::nonNull)) { + simpleSet.add(derive(elements)); } } } @@ -55,14 +47,16 @@ public void repopulate() { @Override @SuppressWarnings("unchecked") public Collection forwardPropagate(CAATPredicate changedSource, Collection added) { - if (changedSource == first || changedSource == second) { - SetPredicate other = (changedSource == first) ? second : first; + if (Stream.of(operands).anyMatch(o -> changedSource == o)) { Collection addedElems = (Collection)added; List newlyAdded = new ArrayList<>(); for (Element e1 : addedElems) { - Element e2 = other.get(e1); - if (e2 != null) { - Element e = derive(e1, e2); + final Element[] elements = new Element[operands.length]; + for (int i = 0; i < operands.length; i++) { + elements[i] = operands[i] == changedSource ? e1 : operands[i].get(e1); + } + if (Stream.of(elements).allMatch(Objects::nonNull)) { + final Element e = derive(elements); simpleSet.add(e); newlyAdded.add(e); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/ProjectionIdentityGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/ProjectionSet.java similarity index 68% rename from dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/ProjectionIdentityGraph.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/ProjectionSet.java index abc04b25c5..0f1e87e1e3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/relationGraphs/derived/ProjectionIdentityGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/ProjectionSet.java @@ -1,18 +1,19 @@ -package com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived; +package com.dat3m.dartagnan.solver.caat.predicates.sets.derived; import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; import com.dat3m.dartagnan.solver.caat.predicates.Derivable; import com.dat3m.dartagnan.solver.caat.predicates.misc.PredicateVisitor; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge; -import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.MaterializedGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph; +import com.dat3m.dartagnan.solver.caat.predicates.sets.Element; +import com.dat3m.dartagnan.solver.caat.predicates.sets.MaterializedSet; import java.util.Collection; import java.util.Collections; import java.util.List; import java.util.stream.Collectors; -public class ProjectionIdentityGraph extends MaterializedGraph { +public class ProjectionSet extends MaterializedSet { public enum Dimension { DOMAIN, @@ -29,32 +30,32 @@ public List getDependencies() { public Dimension getProjectionDimension() { return dimension; } - public ProjectionIdentityGraph(RelationGraph inner, Dimension dimension) { + public ProjectionSet(RelationGraph inner, Dimension dimension) { this.inner = inner; this.dimension = dimension; } - private Edge derive(Edge e) { + private Element derive(Edge e) { int id = switch (this.dimension) { case RANGE -> e.getSecond(); case DOMAIN -> e.getFirst(); }; - return new Edge(id, id, e.getTime(), e.getDerivationLength() + 1); + return new Element(id, e.getTime(), e.getDerivationLength() + 1); } @Override public void repopulate() { - inner.edgeStream().forEach(e -> simpleGraph.add(derive(e))); + inner.edgeStream().forEach(e -> simpleSet.add(derive(e))); } @Override @SuppressWarnings("unchecked") - public Collection forwardPropagate(CAATPredicate changedSource, Collection added) { + public Collection forwardPropagate(CAATPredicate changedSource, Collection added) { if (changedSource == inner) { Collection addedEdges = (Collection) added; return addedEdges.stream() .map(this::derive) - .filter(simpleGraph::add) + .filter(simpleSet::add) .collect(Collectors.toList()); } else { return Collections.emptyList(); @@ -63,7 +64,7 @@ public Collection forwardPropagate(CAATPredicate changedSource, Collection @Override public TRet accept(PredicateVisitor visitor, TData data, TContext context) { - return visitor.visitProjectionIdentity(this, data, context); + return visitor.visitProjection(this, data, context); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/UnionSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/UnionSet.java index 106a786516..ebdb504360 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/UnionSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/derived/UnionSet.java @@ -9,25 +9,21 @@ import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate; import java.util.*; +import java.util.stream.Stream; // A materialized Union Graph. // This seems to be more efficient than the virtualized UnionGraph we used before. public class UnionSet extends MaterializedSet { - private final SetPredicate first; - private final SetPredicate second; + private final SetPredicate[] operands; @Override public List getDependencies() { - return Arrays.asList(first, second); + return Arrays.asList(operands); } - public SetPredicate getFirst() { return first; } - public SetPredicate getSecond() { return second; } - - public UnionSet(SetPredicate first, SetPredicate second) { - this.first = first; - this.second = second; + public UnionSet(SetPredicate... o) { + operands = o; } private Element derive(Element e) { @@ -37,18 +33,17 @@ private Element derive(Element e) { @Override public void repopulate() { //TODO: Maybe try to minimize the derivation length initially - for (Element e : first.elements()) { - simpleSet.add(derive(e)); - } - for (Element e : second.elements()) { - simpleSet.add(derive(e)); + for (SetPredicate o : operands) { + for (Element e : o.elements()) { + simpleSet.add(derive(e)); + } } } @Override @SuppressWarnings("unchecked") public Collection forwardPropagate(CAATPredicate changedSource, Collection added) { - if (changedSource == first || changedSource == second) { + if (Stream.of(operands).anyMatch(o -> changedSource == o)) { ArrayList newlyAdded = new ArrayList<>(); Collection addedElems = (Collection)added; for (Element e : addedElems) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java index 50a3121fa0..4a5fcafd5e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java @@ -8,7 +8,7 @@ import com.dat3m.dartagnan.solver.caat.predicates.misc.PredicateVisitor; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph; -import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.ProjectionIdentityGraph; +import com.dat3m.dartagnan.solver.caat.predicates.sets.derived.ProjectionSet; import com.dat3m.dartagnan.solver.caat.predicates.sets.Element; import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate; import com.dat3m.dartagnan.utils.logic.Conjunction; @@ -221,11 +221,11 @@ public Conjunction visitSetIdentity(RelationGraph graph, Edge edge, } @Override - public Conjunction visitProjectionIdentity(RelationGraph graph, Edge edge, Void unused) { + public Conjunction visitProjection(SetPredicate set, Edge edge, Void unused) { assert edge.isLoop(); - RelationGraph inner = (RelationGraph) graph.getDependencies().get(0); - ProjectionIdentityGraph.Dimension dim = ((ProjectionIdentityGraph)graph).getProjectionDimension(); + RelationGraph inner = (RelationGraph) set.getDependencies().get(0); + ProjectionSet.Dimension dim = ((ProjectionSet)set).getProjectionDimension(); Iterable edges = switch (dim) { case RANGE -> inner.inEdges(edge.getSecond()); case DOMAIN -> inner.outEdges(edge.getFirst()); @@ -286,10 +286,10 @@ public Conjunction visitSetUnion(SetPredicate set, Element ele, Voi // We try to compute a shortest reason based on the distance to the base graphs Element min = ele; SetPredicate next = set; - for (SetPredicate s : set.getDependencies()) { - Element e = s.get(ele); + for (CAATPredicate s : set.getDependencies()) { + Element e = ((SetPredicate) s).get(ele); if (e != null && e.getDerivationLength() < min.getDerivationLength()) { - next = s; + next = (SetPredicate) s; min = e; } } @@ -304,7 +304,7 @@ public Conjunction visitSetUnion(SetPredicate set, Element ele, Voi @Override public Conjunction visitSetIntersection(SetPredicate set, Element ele, Void unused) { Conjunction reason = Conjunction.TRUE(); - for (SetPredicate s : set.getDependencies()) { + for (CAATPredicate s : set.getDependencies()) { Element e = set.get(ele); reason = reason.and(computeReason(s, e)); } @@ -314,8 +314,8 @@ public Conjunction visitSetIntersection(SetPredicate set, Element e @Override public Conjunction visitSetDifference(SetPredicate set, Element ele, Void unused) { - SetPredicate lhs = set.getDependencies().get(0); - SetPredicate rhs = set.getDependencies().get(1); + SetPredicate lhs = (SetPredicate) set.getDependencies().get(0); + SetPredicate rhs = (SetPredicate) set.getDependencies().get(1); if (!rhs.getDependencies().isEmpty()) { throw new IllegalStateException(String.format("Cannot compute reason of element %s in " + diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index 9b4d2fb949..59c7b44f66 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -10,6 +10,7 @@ import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.base.EmptyGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.*; import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate; +import com.dat3m.dartagnan.solver.caat.predicates.sets.derived.*; import com.dat3m.dartagnan.solver.caat4wmm.basePredicates.*; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; import com.dat3m.dartagnan.verification.model.ExecutionModel; @@ -216,6 +217,7 @@ private RelationGraph getOrCreateGraphFromRelation(Relation rel) { } private RelationGraph createGraphFromRelation(Relation rel) { + rel.checkBinaryRelation(); final RelationGraph graph; final Class relClass = rel.getDefinition().getClass(); final List dependencies = rel.getDependencies(); @@ -230,12 +232,6 @@ private RelationGraph createGraphFromRelation(Relation rel) { graph = new ProgramOrderGraph(); } else if (relClass == Coherence.class) { graph = new CoherenceGraph(); - } else if (relClass == RangeIdentity.class || relClass == DomainIdentity.class) { - RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0)); - ProjectionIdentityGraph.Dimension dim = relClass == RangeIdentity.class ? - ProjectionIdentityGraph.Dimension.RANGE : - ProjectionIdentityGraph.Dimension.DOMAIN; - graph = new ProjectionIdentityGraph(g, dim); } else if (relClass == Inverse.class || relClass == TransitiveClosure.class) { RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0)); graph = relClass == Inverse.class ? new InverseGraph(g) : new TransitiveGraph(g); @@ -244,24 +240,22 @@ private RelationGraph createGraphFromRelation(Relation rel) { for (int i = 0; i < graphs.length; i++) { graphs[i] = getOrCreateGraphFromRelation(dependencies.get(i)); } - graph = relClass == Union.class ? new UnionGraph(graphs) : - new IntersectionGraph(graphs); + graph = relClass == Union.class ? new UnionGraph(graphs) : new IntersectionGraph(graphs); } else if (relClass == Composition.class || relClass == Difference.class) { RelationGraph g1 = getOrCreateGraphFromRelation(dependencies.get(0)); RelationGraph g2 = getOrCreateGraphFromRelation(dependencies.get(1)); - graph = relClass == Composition.class ? new CompositionGraph(g1, g2) : - new DifferenceGraph(g1, g2); + graph = relClass == Composition.class ? new CompositionGraph(g1, g2) : new DifferenceGraph(g1, g2); } else if (relClass == CartesianProduct.class) { CartesianProduct cartRel = (CartesianProduct)rel.getDefinition(); - SetPredicate lhs = getOrCreateSetFromFilter(cartRel.getFirstFilter()); - SetPredicate rhs = getOrCreateSetFromFilter(cartRel.getSecondFilter()); + SetPredicate lhs = getOrCreateSetFromRelation(cartRel.getDomain()); + SetPredicate rhs = getOrCreateSetFromRelation(cartRel.getRange()); graph = new CartesianGraph(lhs, rhs); } else if (relClass == External.class) { graph = new ExternalGraph(); } else if (relClass == Internal.class) { graph = new InternalGraph(); } else if (relClass == SetIdentity.class) { - SetPredicate set = getOrCreateSetFromFilter(((SetIdentity) rel.getDefinition()).getFilter()); + SetPredicate set = getOrCreateSetFromRelation(((SetIdentity) rel.getDefinition()).getDomain()); graph = new SetIdentityGraph(set); } else if (relClass == Empty.class) { graph = new EmptyGraph(); @@ -275,16 +269,36 @@ private RelationGraph createGraphFromRelation(Relation rel) { return graph; } - private SetPredicate getOrCreateSetFromFilter(Filter filter) { - if (filterSetMap.containsKey(filter)) { - return filterSetMap.get(filter); + private SetPredicate getOrCreateSetFromRelation(Relation relation) { + relation.checkUnaryRelation(); + final Class relClass = relation.getDefinition().getClass(); + final List dependencies = relation.getDependencies(); + final SetPredicate set; + if (cutRelations.contains(relation)) { + set = new DynamicDefaultWMMSet(refinementModel.translateToBase(relation)); + } else if (relClass == TagSet.class) { + set = new StaticWMMSet(Filter.byTag(((TagSet) relation.getDefinition()).getTag())); + } else if (relClass == Range.class || relClass == Domain.class) { + RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0)); + ProjectionSet.Dimension dim = relClass == Range.class ? + ProjectionSet.Dimension.RANGE : + ProjectionSet.Dimension.DOMAIN; + set = new ProjectionSet(g, dim); + } else if (relClass == Union.class || relClass == Intersection.class) { + SetPredicate[] graphs = new SetPredicate[dependencies.size()]; + for (int i = 0; i < graphs.length; i++) { + graphs[i] = getOrCreateSetFromRelation(dependencies.get(i)); + } + set = relClass == Union.class ? new UnionSet(graphs) : new IntersectionSet(graphs); + } else if (relClass == Difference.class) { + SetPredicate s1 = getOrCreateSetFromRelation(dependencies.get(0)); + SetPredicate s2 = getOrCreateSetFromRelation(dependencies.get(1)); + set = new DifferenceSet(s1, s2); + } else { + throw new UnsupportedOperationException(String.format("Cannot handle set %s with definition of type %s", relation, relClass.getSimpleName())); } - - SetPredicate set = new StaticWMMSet(filter); - set.setName(filter.toString()); - filterSetMap.put(filter, set); + set.setName(relation.getNameOrTerm()); return set; - } // ======================================================= diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java index 2209b617b3..38678a7b58 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java @@ -112,7 +112,7 @@ public static RefinementModel fromCut(Cut cut) { // Skip the anarchic relations we already copied above continue; } - final Relation copy = base.newRelation(); + final Relation copy = base.newRelation(rel.isUnaryRelation()); rel.getNames().forEach(n -> base.addAlias(n, copy)); orig2BaseRelations.put(rel, copy); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/AbstractWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/AbstractWMMSet.java new file mode 100644 index 0000000000..3b91e1b6ba --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/AbstractWMMSet.java @@ -0,0 +1,29 @@ +package com.dat3m.dartagnan.solver.caat4wmm.basePredicates; + +import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; +import com.dat3m.dartagnan.solver.caat.predicates.Derivable; +import com.dat3m.dartagnan.solver.caat.predicates.misc.PredicateVisitor; +import com.dat3m.dartagnan.solver.caat.predicates.sets.Element; +import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate; + +import java.util.Collection; +import java.util.Collections; +import java.util.List; + +public abstract class AbstractWMMSet extends AbstractWMMPredicate implements SetPredicate { + + @Override + public List getDependencies() { + return Collections.emptyList(); + } + + @Override + public TRet accept(PredicateVisitor visitor, TData tData, TContext context) { + return visitor.visitBaseSet(this, tData, context); + } + + @Override + public Collection forwardPropagate(CAATPredicate changedSource, Collection added) { + return Collections.emptyList(); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java index 6035da6597..c0534c7b82 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java @@ -12,6 +12,7 @@ public class DynamicDefaultWMMGraph extends MaterializedWMMGraph { private final Relation relation; public DynamicDefaultWMMGraph(Relation rel) { + rel.checkBinaryRelation(); this.relation = rel; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java new file mode 100644 index 0000000000..a4aa2040ae --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java @@ -0,0 +1,50 @@ +package com.dat3m.dartagnan.solver.caat4wmm.basePredicates; + +import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.encoding.IREvaluator; +import com.dat3m.dartagnan.solver.caat.predicates.sets.Element; +import com.dat3m.dartagnan.verification.model.EventData; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; + +// A default implementation for any encoded relation, e.g. base relations or non-base but cut relations. +public class DynamicDefaultWMMSet extends MaterializedWMMSet { + + private final Relation relation; + + public DynamicDefaultWMMSet(Relation rel) { + rel.checkUnaryRelation(); + this.relation = rel; + } + + @Override + public void repopulate() { + // Careful: The wrapped model might get closed/disposed while ExecutionModel as a whole is + // still in use. The caller should make sure that the underlying model is still alive right now. + final EncodingContext ctx = model.getContext(); + final IREvaluator m = new IREvaluator(ctx, model.getModel()); + final EncodingContext.EdgeEncoder edge = ctx.edge(relation); + final RelationAnalysis.Knowledge k = ctx.getAnalysisContext().get(RelationAnalysis.class).getKnowledge(relation); + + if (k.getMaySet().size() < domain.size() * domain.size()) { + k.getMaySet().apply((e1, e2) -> { + final EventData d1 = !e1.equals(e2) ? null : model.getData(e1).orElse(null); + final Element e = d1 == null ? null : getEdgeFromEventData(edge, d1, m); + if (e != null) { + simpleSet.add(e); + } + }); + } else { + for (EventData e1 : model.getEventList()) { + final Element e = getEdgeFromEventData(edge, e1, m); + if (e != null) { + simpleSet.add(e); + } + } + } + } + + private Element getEdgeFromEventData(EncodingContext.EdgeEncoder edge, EventData e1, IREvaluator m) { + return m.hasElement(edge, e1.getEvent()) ? new Element(e1.getId()) : null; + } +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/MaterializedWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/MaterializedWMMSet.java new file mode 100644 index 0000000000..db71db045c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/MaterializedWMMSet.java @@ -0,0 +1,56 @@ +package com.dat3m.dartagnan.solver.caat4wmm.basePredicates; + +import com.dat3m.dartagnan.solver.caat.domain.Domain; +import com.dat3m.dartagnan.solver.caat.predicates.sets.Element; +import com.dat3m.dartagnan.solver.caat.predicates.sets.base.SimpleSet; + +import java.util.Iterator; +import java.util.stream.Stream; + +public abstract class MaterializedWMMSet extends AbstractWMMSet { + + protected final SimpleSet simpleSet; + + protected MaterializedWMMSet() { + this.simpleSet = new SimpleSet(); + } + + @Override + public Element get(Element element) { return simpleSet.get(element); } + + @Override + public boolean containsById(int a) { return simpleSet.containsById(a); } + + @Override + public boolean contains(Element element) { return simpleSet.contains(element); } + + @Override + public void backtrackTo(int time) { simpleSet.backtrackTo(time); } + + @Override + public void initializeToDomain(Domain domain) { + super.initializeToDomain(domain); + simpleSet.initializeToDomain(domain); + } + + @Override + public int getEstimatedSize() { return simpleSet.getEstimatedSize(); } + + @Override + public int getMinSize() { return simpleSet.getMinSize(); } + + @Override + public int getMaxSize() { return simpleSet.getMaxSize(); } + + @Override + public Stream elementStream() { return simpleSet.elementStream(); } + + @Override + public Iterator elementIterator() { return simpleSet.elementIterator(); } + + @Override + public int size() { return simpleSet.size(); } + + @Override + public boolean isEmpty() { return simpleSet.isEmpty(); } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java index 1f68477b18..38f5b39fed 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -6,6 +6,7 @@ import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.smt.ModelExt; import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; @@ -14,6 +15,12 @@ import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.base.SimpleGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.*; +import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate; +import com.dat3m.dartagnan.solver.caat.predicates.sets.base.SimpleSet; +import com.dat3m.dartagnan.solver.caat.predicates.sets.derived.DifferenceSet; +import com.dat3m.dartagnan.solver.caat.predicates.sets.derived.IntersectionSet; +import com.dat3m.dartagnan.solver.caat.predicates.sets.derived.ProjectionSet; +import com.dat3m.dartagnan.solver.caat.predicates.sets.derived.UnionSet; import com.dat3m.dartagnan.solver.caat4wmm.EventDomainNext; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; import com.dat3m.dartagnan.verification.model.RelationModel.EdgeModel; @@ -31,10 +38,12 @@ public class ExecutionModelManager { + private final SetPredicateBuilder setBuilder; private final RelationGraphBuilder graphBuilder; private final RelationGraphPopulator graphPopulator; private final Map relModelCache; + private final BiMap setCache; private final BiMap relGraphCache; private final Map edgeModelCache; @@ -44,10 +53,12 @@ public class ExecutionModelManager { private Wmm wmm; private EventDomainNext domain; - public ExecutionModelManager(){ + public ExecutionModelManager() { + setBuilder = new SetPredicateBuilder(); graphBuilder = new RelationGraphBuilder(); graphPopulator = new RelationGraphPopulator(); relModelCache = new HashMap<>(); + setCache = HashBiMap.create(); relGraphCache = HashBiMap.create(); edgeModelCache = new HashMap<>(); } @@ -232,6 +243,15 @@ private void createModel(Relation r) { relModelCache.put(r, new RelationModel(r)); } + private SetPredicate createSet(Relation r) { + SetPredicate set = r.getDependencies().isEmpty() ? new SimpleSet() : r.getDefinition().accept(setBuilder); + set.setName(r.getNameOrTerm()); + if (!r.isRecursive()) { + setCache.put(r, set); + } + return set; + } + private RelationGraph createGraph(Relation r) { RelationGraph rg = r.getDependencies().isEmpty() ? new SimpleGraph() : r.getDefinition().accept(graphBuilder); rg.setName(r.getNameOrTerm()); @@ -241,7 +261,14 @@ private RelationGraph createGraph(Relation r) { return rg; } + private SetPredicate getOrCreateSet(Relation r) { + r.checkUnaryRelation(); + final SetPredicate existing = setCache.get(r); + return existing != null ? existing : createSet(r); + } + private RelationGraph getOrCreateGraph(Relation r) { + r.checkBinaryRelation(); if (relGraphCache.containsKey(r)) { return relGraphCache.get(r); } @@ -262,6 +289,14 @@ private EdgeModel getOrCreateEdgeModel(Edge e) { // based on the information from ExecutionModelNext. private final class RelationGraphPopulator implements Visitor { + @Override + public Void visitTagSet(TagSet tagSet) { + SimpleGraph rg = (SimpleGraph) relGraphCache.get(tagSet.getDefinedRelation()); + executionModel.getEventModelsByFilter(Filter.byTag(tagSet.getTag())) + .forEach(e -> rg.add(new Edge(e.getId(), e.getId()))); + return null; + } + @Override public Void visitProgramOrder(ProgramOrder po) { SimpleGraph rg = (SimpleGraph) relGraphCache.get(po.getDefinedRelation()); @@ -432,27 +467,6 @@ public Void visitExternal(External ext) { return null; } - @Override - public Void visitSetIdentity(SetIdentity si) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(si.getDefinedRelation()); - executionModel.getEventModelsByFilter(si.getFilter()) - .stream().forEach(e -> rg.add(new Edge(e.getId(), e.getId()))); - return null; - } - - @Override - public Void visitProduct(CartesianProduct cp) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(cp.getDefinedRelation()); - List first = executionModel.getEventModelsByFilter(cp.getFirstFilter()); - List second = executionModel.getEventModelsByFilter(cp.getSecondFilter()); - for (EventModel e1 : first) { - for (EventModel e2 : second) { - rg.add(new Edge(e1.getId(), e2.getId())); - } - } - return null; - } - @Override public Void visitControlDependency(DirectControlDependency ctrlDirect) { SimpleGraph rg = (SimpleGraph) relGraphCache.get(ctrlDirect.getDefinedRelation()); @@ -503,6 +517,49 @@ public void populateDynamicDefaultGraph(Relation r) { } + private final class SetPredicateBuilder implements Visitor { + + @Override + public SetPredicate visitDifference(Difference diff) { + return new DifferenceSet(getOrCreateSet(diff.getMinuend()), getOrCreateSet(diff.getSubtrahend())); + } + + @Override + public SetPredicate visitUnion(Union un) { + List ops = un.getOperands(); + SetPredicate[] rgs = new SetPredicate[ops.size()]; + for (int i = 0; i < rgs.length; i++) { + rgs[i] = getOrCreateSet(ops.get(i)); + } + return new UnionSet(rgs); + } + + @Override + public SetPredicate visitIntersection(Intersection inter) { + List ops = inter.getOperands(); + SetPredicate[] rgs = new SetPredicate[ops.size()]; + for (int i = 0; i < rgs.length; i++) { + rgs[i] = getOrCreateSet(ops.get(i)); + } + return new IntersectionSet(rgs); + } + + @Override + public SetPredicate visitRange(Range range) { + return new ProjectionSet( + getOrCreateGraph(range.getOperand()), + ProjectionSet.Dimension.RANGE + ); + } + + @Override + public SetPredicate visitDomain(Domain domain) { + return new ProjectionSet( + getOrCreateGraph(domain.getOperand()), + ProjectionSet.Dimension.DOMAIN + ); + } + } // Create a the specific graph for derived relations, so that edges of them // can be computed automatically by PredicateHierarchy. @@ -551,20 +608,13 @@ public RelationGraph visitTransitiveClosure(TransitiveClosure trans) { } @Override - public RelationGraph visitRangeIdentity(RangeIdentity ri) { - return new ProjectionIdentityGraph( - getOrCreateGraph(ri.getOperand()), - ProjectionIdentityGraph.Dimension.RANGE - ); + public RelationGraph visitProduct(CartesianProduct product) { + return new CartesianGraph(getOrCreateSet(product.getDomain()), getOrCreateSet(product.getRange())); } @Override - public RelationGraph visitDomainIdentity(DomainIdentity di) { - return new ProjectionIdentityGraph( - getOrCreateGraph(di.getOperand()), - ProjectionIdentityGraph.Dimension.DOMAIN - ); + public RelationGraph visitSetIdentity(SetIdentity id) { + return new SetIdentityGraph(getOrCreateSet(id.getDomain())); } - } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 69d0e084ac..e6c962086a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -15,7 +15,6 @@ import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.metadata.OriginalId; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; -import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.smt.ModelExt; import com.dat3m.dartagnan.solver.caat.CAATSolver; import com.dat3m.dartagnan.solver.caat4wmm.RefinementModel; @@ -569,15 +568,15 @@ private static void addBiases(Wmm wmm, EnumSet biases) { final Relation rfinv = wmm.addDefinition(new Inverse(wmm.newRelation(), rf)); final Relation frStandard = wmm.addDefinition(new Composition(wmm.newRelation(), rfinv, co)); - // ([R] \ [range(rf)]);loc;[W] - final Relation reads = wmm.addDefinition(new SetIdentity(wmm.newRelation(), wmm.getFilter(Tag.READ))); - final Relation rfRange = wmm.addDefinition(new RangeIdentity(wmm.newRelation(), rf)); - final Relation writes = wmm.addDefinition(new SetIdentity(wmm.newRelation(), Filter.byTag(Tag.WRITE))); - final Relation ur = wmm.addDefinition(new Difference(wmm.newRelation(), reads, rfRange)); - final Relation urloc = wmm.addDefinition(new Composition(wmm.newRelation(), ur, loc)); - final Relation urlocwrites = wmm.addDefinition(new Composition(wmm.newRelation(), urloc, writes)); + // ((R \ range(rf)) * W) & loc + final Relation reads = wmm.addDefinition(new TagSet(wmm.newSet(), Tag.READ)); + final Relation rfRange = wmm.addDefinition(new Range(wmm.newSet(), rf)); + final Relation writes = wmm.addDefinition(new TagSet(wmm.newSet(), Tag.WRITE)); + final Relation ur = wmm.addDefinition(new Difference(wmm.newSet(), reads, rfRange)); + final Relation urw = wmm.addDefinition(new CartesianProduct(wmm.newRelation(), ur, writes)); + final Relation urlocwrites = wmm.addDefinition(new Intersection(wmm.newRelation(), urw, loc)); - // let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W] + // let fr = rf^-1;co | (((R \ range(rf)) * W) & loc) final Relation fr = wmm.addDefinition(new Union(wmm.newRelation(), frStandard, urlocwrites)); if (biases.contains(Baseline.UNIPROC)) { 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 780ee102ad..1830463918 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -63,8 +63,8 @@ default T visitConstraint(Constraint constraint) { default T visitIntersection(Intersection def) { return visitDefinition(def); } default T visitDifference(Difference def) { return visitDefinition(def); } default T visitComposition(Composition def) { return visitDefinition(def); } - default T visitDomainIdentity(DomainIdentity def) { return visitDefinition(def); } - default T visitRangeIdentity(RangeIdentity def) { return visitDefinition(def); } + default T visitDomain(Domain def) { return visitDefinition(def); } + default T visitRange(Range def) { return visitDefinition(def); } default T visitInverse(Inverse def) { return visitDefinition(def); } default T visitTransitiveClosure(TransitiveClosure def) { return visitDefinition(def); } // These three are semi-derived (they are derived from sets/filters and not from relations). @@ -75,6 +75,7 @@ default T visitConstraint(Constraint constraint) { default T visitUndefined(Definition.Undefined def) { return visitDefinition(def); } default T visitFree(Free def) { return visitDefinition(def); } default T visitEmpty(Empty def) { return visitDefinition(def); } + default T visitTagSet(TagSet def) { return visitDefinition(def); } default T visitProgramOrder(ProgramOrder po) { return visitDefinition(po); } default T visitExternal(External ext) { return visitDefinition(ext); } default T visitInternal(Internal internal) { return visitDefinition(internal); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java index 43550e237a..16518c704e 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.utils.dependable.Dependent; import com.dat3m.dartagnan.wmm.definition.Composition; import com.dat3m.dartagnan.wmm.definition.Union; +import com.google.common.base.Preconditions; import java.util.ArrayList; import java.util.List; @@ -14,12 +15,37 @@ public final class Relation implements Dependent { private final Wmm wmm; + private final boolean unary; Definition definition = new Definition.Undefined(this); private boolean isRecursive; final List names = new ArrayList<>(); - Relation(Wmm wmm) { + Relation(Wmm wmm, boolean unary) { this.wmm = wmm; + this.unary = unary; + } + + public boolean isUnaryRelation() { + return unary; + } + + public boolean isBinaryRelation() { + return !unary; + } + + public void checkUnaryRelation() { + Preconditions.checkArgument(isUnaryRelation(), "Non-unary relation %s.", this); + } + + public void checkBinaryRelation() { + Preconditions.checkArgument(isBinaryRelation(), "Non-binary relation %s.", this); + } + + public void checkEqualArityRelation(List others) { + Preconditions.checkArgument(!isUnaryRelation() || others.stream().allMatch(Relation::isUnaryRelation), + "Non-unary relation in %s", others); + Preconditions.checkArgument(!isBinaryRelation() || others.stream().allMatch(Relation::isBinaryRelation), + "Non-binary relation in %s", others); } /** diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java index be7b075120..78c670fca9 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java @@ -77,7 +77,6 @@ public Relation getOrCreatePredefinedRelation(String name) { checkArgument(RelationNameRepository.contains(name), "Undefined relation name %s.", name); final Relation rel = getRelation(name); return rel != null ? rel : makePredefinedRelation(name); - } public void addAlias(String name, Relation relation) { @@ -85,15 +84,27 @@ public void addAlias(String name, Relation relation) { relation.names.add(name); } + public Relation newSet() { + return newRelation(true); + } + public Relation newRelation() { - final Relation relation = new Relation(this); + return newRelation(false); + } + + public Relation newRelation(boolean unary) { + final Relation relation = new Relation(this, unary); relations.add(relation); return relation; } public Relation newRelation(String name) { + return newRelation(name, false); + } + + public Relation newRelation(String name, boolean unary) { checkArgument(!containsRelation(name), "Already bound name %s.", name); - final Relation relation = new Relation(this); + final Relation relation = new Relation(this, unary); relation.names.add(name); relations.add(relation); return relation; @@ -190,7 +201,7 @@ private Relation makePredefinedRelation(String name) { final Definition def = switch (name) { case PO -> new ProgramOrder(r, Filter.byTag(Tag.VISIBLE)); case LOC -> new SameLocation(r); - case ID -> new SetIdentity(r, Filter.byTag(Tag.VISIBLE)); + case ID -> new SetIdentity(r, set(Tag.VISIBLE)); case INT -> new Internal(r); case EXT -> new External(r); case CO -> new Coherence(r); @@ -205,22 +216,16 @@ private Relation makePredefinedRelation(String name) { case CTRLDIRECT -> new DirectControlDependency(r); case EMPTY -> new Empty(r); case IDDTRANS -> new TransitiveClosure(r, getOrCreatePredefinedRelation(IDD)); - case DATA -> intersection(r, - getOrCreatePredefinedRelation(IDDTRANS), - addDefinition(product(newRelation(), Tag.MEMORY, Tag.MEMORY)) - ); + case DATA -> new Intersection(r, getOrCreatePredefinedRelation(IDDTRANS), product(Tag.MEMORY, Tag.MEMORY)); case ADDR -> { - Relation addrdirect = getOrCreatePredefinedRelation(ADDRDIRECT); - Relation comp = addDefinition(composition(newRelation(), getOrCreatePredefinedRelation(IDDTRANS), addrdirect)); - Relation union = addDefinition(union(newRelation(), addrdirect, comp)); - Relation mm = addDefinition(product(newRelation(), Tag.MEMORY, Tag.MEMORY)); - yield intersection(r, union, mm); + final Relation idd = getOrCreatePredefinedRelation(IDDTRANS); + final Relation addr = getOrCreatePredefinedRelation(ADDRDIRECT); + yield new Intersection(r, union(addr, composition(idd, addr)), product(Tag.MEMORY, Tag.MEMORY)); } case CTRL -> { - Relation comp = addDefinition(composition(newRelation(), getOrCreatePredefinedRelation(IDDTRANS), - getOrCreatePredefinedRelation(CTRLDIRECT))); - Relation mv = addDefinition(product(newRelation(), Tag.MEMORY, Tag.VISIBLE)); - yield intersection(r, comp, mv); + final Relation idd = getOrCreatePredefinedRelation(IDDTRANS); + final Relation ctrl = getOrCreatePredefinedRelation(CTRLDIRECT); + yield new Intersection(r, composition(idd, ctrl), product(Tag.MEMORY, Tag.VISIBLE)); } case SR -> new SameScope(r); case SCTA -> new SameScope(r, Tag.PTX.CTA); @@ -238,19 +243,19 @@ private Relation makePredefinedRelation(String name) { return addDefinition(def); } - private Definition union(Relation r0, Relation r1, Relation r2) { - return new Union(r0, r1, r2); + private Relation union(Relation r1, Relation r2) { + return addDefinition(new Union(newRelation(), r1, r2)); } - private Definition intersection(Relation r0, Relation r1, Relation r2) { - return new Intersection(r0, r1, r2); + private Relation composition(Relation r1, Relation r2) { + return addDefinition(new Composition(newRelation(), r1, r2)); } - private Definition composition(Relation r0, Relation r1, Relation r2) { - return new Composition(r0, r1, r2); + private Relation set(String tag) { + return addDefinition(new TagSet(newSet(), tag)); } - private Definition product(Relation r0, String tag1, String tag2) { - return new CartesianProduct(r0, Filter.byTag(tag1), Filter.byTag(tag2)); + private Relation product(String tag1, String tag2) { + return addDefinition(new CartesianProduct(newRelation(), set(tag1), set(tag2))); } } 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 index 6a43920cc8..b517381b5d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java @@ -12,7 +12,6 @@ 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; @@ -133,25 +132,40 @@ public RelationAnalysis.Knowledge visitFree(Free definition) { @Override public RelationAnalysis.Knowledge visitProduct(CartesianProduct definition) { - Filter domainFilter = definition.getFirstFilter(); - Filter rangeFilter = definition.getSecondFilter(); + final RelationAnalysis.Knowledge domain = getKnowledge(definition.getDomain()); + final RelationAnalysis.Knowledge range = getKnowledge(definition.getRange()); + final EventGraph mayDomain = domain.getMaySet(); + final EventGraph mustDomain = domain.getMustSet(); + final EventGraph mayRange = range.getMaySet(); + final EventGraph mustRange = range.getMustSet(); 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)); + final EventGraph may = new LazyEventGraph(mayDomain.getDomain(), mayRange.getDomain(), + (e1, e2) -> mayDomain.contains(e1, e1) && mayRange.contains(e2, e2)); + final EventGraph must = new LazyEventGraph(mustDomain.getDomain(), mustRange.getDomain(), + (e1, e2) -> mustDomain.contains(e1, e1) && mustRange.contains(e2, e2) && + !exec.areMutuallyExclusive(e1, e2)); time(definition, start, System.currentTimeMillis()); - return new RelationAnalysis.Knowledge(must, must); + return new RelationAnalysis.Knowledge(may, must); } @Override public RelationAnalysis.Knowledge visitSetIdentity(SetIdentity definition) { - Filter filter = definition.getFilter(); + final RelationAnalysis.Knowledge domain = getKnowledge(definition.getDomain()); + final EventGraph mayDomain = domain.getMaySet(); + final EventGraph mustDomain = domain.getMustSet(); long start = System.currentTimeMillis(); - Map> data = program.getThreadEvents().stream() - .filter(filter::apply) - .collect(Collectors.toMap(e -> e, ImmutableSet::of)); - EventGraph must = new ImmutableMapEventGraph(data); + final EventGraph may = new LazyEventGraph(mayDomain.getDomain(), mayDomain.getDomain(), + (e1, e2) -> e1.equals(e2) && mayDomain.contains(e1, e2)); + final EventGraph must = new LazyEventGraph(mustDomain.getDomain(), mustDomain.getDomain(), + (e1, e2) -> e1.equals(e2) && mustDomain.contains(e1, e2)); time(definition, start, System.currentTimeMillis()); + return new RelationAnalysis.Knowledge(may, must); + } + + @Override + public RelationAnalysis.Knowledge visitTagSet(TagSet definition) { + final Set domain = Set.copyOf(program.getThreadEventsWithAllTags(definition.getTag())); + final EventGraph must = new LazyEventGraph(domain, domain, Object::equals); return new RelationAnalysis.Knowledge(must, must); } @@ -455,7 +469,7 @@ public RelationAnalysis.Knowledge visitSyncWith(SyncWith definition) { } @Override - public RelationAnalysis.Knowledge visitDomainIdentity(DomainIdentity definition) { + public RelationAnalysis.Knowledge visitDomain(Domain definition) { RelationAnalysis.Knowledge knowledge = getKnowledge(definition.getOperand()); long start = System.currentTimeMillis(); Map> mayMap = knowledge.getMaySet().getDomain().stream() @@ -470,7 +484,7 @@ public RelationAnalysis.Knowledge visitDomainIdentity(DomainIdentity definition) } @Override - public RelationAnalysis.Knowledge visitRangeIdentity(RangeIdentity definition) { + public RelationAnalysis.Knowledge visitRange(Range definition) { RelationAnalysis.Knowledge knowledge = getKnowledge(definition.getOperand()); long start = System.currentTimeMillis(); Map> mayMap = knowledge.getMaySet().getRange().stream() 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 36916e9b51..080cb292eb 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 @@ -506,30 +506,6 @@ public MutableKnowledge visitFree(Free def) { return new MutableKnowledge(may, must); } - @Override - public MutableKnowledge visitProduct(CartesianProduct prod) { - final Filter domain = prod.getFirstFilter(); - final Filter range = prod.getSecondFilter(); - 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) { - Set rangeEvents = l2.stream() - .filter(e2 -> !exec.areMutuallyExclusive(e1, e2)) - .collect(toSet()); - must.addRange(e1, rangeEvents); - } - return new MutableKnowledge(must, MapEventGraph.from(must)); - } - - @Override - public MutableKnowledge visitSetIdentity(SetIdentity id) { - final Filter set = id.getFilter(); - MutableEventGraph must = new MapEventGraph(); - program.getThreadEvents().stream().filter(set::apply).forEach(e -> must.add(e, e)); - return new MutableKnowledge(must, MapEventGraph.from(must)); - } - @Override public MutableKnowledge visitExternal(External ext) { MutableEventGraph must = new MapEventGraph(); @@ -566,6 +542,13 @@ public MutableKnowledge visitInternal(Internal internal) { return new MutableKnowledge(must, MapEventGraph.from(must)); } + @Override + public MutableKnowledge visitTagSet(TagSet tagSet) { + final MutableEventGraph must = new MapEventGraph(); + program.getThreadEventsWithAllTags(tagSet.getTag()).forEach(e -> must.add(e, e)); + return new MutableKnowledge(must, MapEventGraph.from(must)); + } + @Override public MutableKnowledge visitProgramOrder(ProgramOrder po) { final Filter type = po.getFilter(); @@ -1652,7 +1635,7 @@ private void computeComposition(MutableEventGraph result, EventGraph left, Event } @Override - public Delta visitDomainIdentity(DomainIdentity domId) { + public Delta visitDomain(Domain domId) { if (domId.getOperand().equals(source)) { MutableEventGraph maySet = new MapEventGraph(); may.getDomain().forEach(e -> maySet.add(e, e)); @@ -1668,7 +1651,7 @@ public Delta visitDomainIdentity(DomainIdentity domId) { } @Override - public Delta visitRangeIdentity(RangeIdentity rangeId) { + public Delta visitRange(Range rangeId) { if (rangeId.getOperand().equals(source)) { MutableEventGraph maySet = new MapEventGraph(); may.getRange().forEach(e -> maySet.add(e, e)); @@ -1683,6 +1666,47 @@ public Delta visitRangeIdentity(RangeIdentity rangeId) { return Delta.EMPTY; } + @Override + public Delta visitProduct(CartesianProduct product) { + final boolean isDomain = product.getDomain().equals(source); + final boolean isRange = product.getRange().equals(source); + if (!isDomain && !isRange) { + return Delta.EMPTY; + } + final Knowledge domain = knowledgeMap.get(product.getDomain()); + final Knowledge range = knowledgeMap.get(product.getRange()); + final MutableEventGraph maySet = new MapEventGraph(); + final MutableEventGraph mustSet = new MapEventGraph(); + if (isRange) { + computeCartesianProduct(maySet, domain.getMaySet(), may); + computeCartesianProduct(mustSet, domain.getMustSet(), must); + } + if (isDomain) { + computeCartesianProduct(maySet, may, range.getMaySet()); + computeCartesianProduct(mustSet, must, range.getMustSet()); + } + return new Delta(maySet, mustSet); + } + + private void computeCartesianProduct(MutableEventGraph target, EventGraph domain, EventGraph range) { + for (Event e1 : domain.getDomain()) { + if (domain.contains(e1, e1)) { + final Set newRange = new HashSet<>(range.getDomain()); + newRange.removeIf(e2 -> !range.contains(e2, e2)); + newRange.removeIf(e2 -> exec.areMutuallyExclusive(e1, e2)); + target.addRange(e1, newRange); + } + } + } + + @Override + public Delta visitSetIdentity(SetIdentity id) { + if (!id.getDomain().equals(source)) { + return Delta.EMPTY; + } + return new Delta(MutableEventGraph.from(may), MutableEventGraph.from(must)); + } + @Override public Delta visitInverse(Inverse inv) { if (inv.getOperand().equals(source)) { 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 f622b113ec..24fa71fd06 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 @@ -27,10 +27,12 @@ public class Acyclicity extends Axiom { public Acyclicity(Relation rel, boolean negated, boolean flag) { super(rel, negated, flag); + rel.checkBinaryRelation(); } public Acyclicity(Relation rel) { super(rel, false, false); + rel.checkBinaryRelation(); } // Under-approximates the must-set of (rel+ ; rel). 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 43d8d5f121..136f0269a2 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 @@ -16,10 +16,12 @@ public class Irreflexivity extends Axiom { public Irreflexivity(Relation rel, boolean negated, boolean flag) { super(rel, negated, flag); + rel.checkBinaryRelation(); } public Irreflexivity(Relation rel) { super(rel, false, false); + rel.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java index bed4af3a9a..fb0821b1eb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java @@ -8,6 +8,7 @@ public class AMOPairs extends Definition { public AMOPairs(Relation r0) { super(r0, RelationNameRepository.AMO); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java index 6dae804856..d1b8251e95 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java @@ -9,6 +9,7 @@ public class CASDependency extends Definition { public CASDependency(Relation r0) { super(r0, CASDEP); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java index 69629371b6..82c0666629 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java @@ -1,25 +1,31 @@ package com.dat3m.dartagnan.wmm.definition; -import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; +import java.util.List; + public class CartesianProduct extends Definition { - private final Filter filter1; - private final Filter filter2; - public Filter getFirstFilter() { - return filter1; - } - - public Filter getSecondFilter() { - return filter2; + private final Relation domain; + private final Relation range; + + public CartesianProduct(Relation r0, Relation r1, Relation r2) { + super(r0, "%s*%s"); + domain = r1; + range = r2; + r0.checkBinaryRelation(); + r1.checkUnaryRelation(); + r2.checkUnaryRelation(); } - public CartesianProduct(Relation r0, Filter s1, Filter s2) { - super(r0, s1 + "*" + s2); - filter1 = s1; - filter2 = s2; + public Relation getDomain() { return domain; } + + public Relation getRange() { return range; } + + @Override + public List getConstrainedRelations() { + return List.of(definedRelation, domain, range); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java index 33c3a08fcc..022df92f59 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java @@ -9,6 +9,7 @@ public class Coherence extends Definition { public Coherence(Relation r0) { super(r0, CO); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java index 317b6259b8..363f114df3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java @@ -16,6 +16,9 @@ public Composition(Relation r0, Relation r1, Relation r2) { super(r0, "%s ; %s"); left = checkNotNull(r1); right = checkNotNull(r2); + r0.checkBinaryRelation(); + r1.checkBinaryRelation(); + r2.checkBinaryRelation(); } public Relation getLeftOperand() { return left; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Difference.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Difference.java index 1364aa5df3..e6c916426b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Difference.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Difference.java @@ -16,6 +16,7 @@ public Difference(Relation r0, Relation r1, Relation r2) { super(r0, "%s \\ %s"); minuend = checkNotNull(r1); subtrahend = checkNotNull(r2); + r0.checkEqualArityRelation(List.of(r1, r2)); } public Relation getMinuend() { return minuend; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java index 85b48f8a92..15a080efeb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java @@ -9,6 +9,7 @@ public class DirectAddressDependency extends Definition { public DirectAddressDependency(Relation r0) { super(r0, RelationNameRepository.ADDRDIRECT); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java index c21bb826d7..2de24bfc50 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java @@ -11,6 +11,7 @@ public class DirectControlDependency extends Definition { public DirectControlDependency(Relation r0) { super(r0, CTRLDIRECT); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java index a80bdf9c54..71986d4046 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java @@ -9,6 +9,7 @@ public class DirectDataDependency extends Definition { public DirectDataDependency(Relation r0) { super(r0, RelationNameRepository.IDD); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DomainIdentity.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java similarity index 70% rename from dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DomainIdentity.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java index 5cc87c0236..66377354a9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DomainIdentity.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java @@ -7,13 +7,15 @@ import static com.google.common.base.Preconditions.checkNotNull; -public class DomainIdentity extends Definition { +public class Domain extends Definition { private final Relation r1; - public DomainIdentity(Relation r0, Relation r1) { - super(r0, "[domain(%s)]"); + public Domain(Relation r0, Relation r1) { + super(r0, "domain(%s)"); this.r1 = checkNotNull(r1); + r0.checkUnaryRelation(); + r1.checkBinaryRelation(); } public Relation getOperand() { return r1; } @@ -25,7 +27,6 @@ public List getConstrainedRelations() { @Override public T accept(Visitor v) { - return v.visitDomainIdentity(this); + return v.visitDomain(this); } - -} +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java index b240831ad8..0ce66e5c5d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java @@ -9,6 +9,7 @@ public class External extends Definition { public External(Relation r0) { super(r0, EXT); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java index ef9552b3fb..5faf6e5a10 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java @@ -9,6 +9,7 @@ public class Internal extends Definition { public Internal(Relation r0) { super(r0, INT); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Intersection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Intersection.java index 894fd494de..022ac3bad6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Intersection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Intersection.java @@ -17,6 +17,7 @@ public class Intersection extends Definition { public Intersection(Relation r0, Relation... o) { super(r0, Stream.of(o).map(r -> "%s").collect(Collectors.joining(" & "))); operands = Stream.of(o).map(Preconditions::checkNotNull).toArray(Relation[]::new); + r0.checkEqualArityRelation(List.of(o)); } public List getOperands() { return Arrays.asList(operands); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java index fc769d5fae..72dd85e53a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java @@ -16,6 +16,8 @@ public class Inverse extends Definition { public Inverse(Relation r0, Relation r1) { super(r0, "%s^-1"); this.r1 = checkNotNull(r1); + r0.checkBinaryRelation(); + r1.checkBinaryRelation(); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java index fc007616ff..d3ab16dbec 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java @@ -8,6 +8,7 @@ public class LXSXPairs extends Definition { public LXSXPairs(Relation r0) { super(r0, RelationNameRepository.LXSX); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java index c016923860..6a071bf508 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java @@ -8,6 +8,7 @@ public class LinuxCriticalSections extends Definition { public LinuxCriticalSections(Relation r0) { super(r0, RelationNameRepository.CRIT); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java index 3712c10c89..37df6c0070 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java @@ -11,6 +11,7 @@ public class ProgramOrder extends Definition { public ProgramOrder(Relation r0, Filter s1) { super(r0, "po(" + s1 + ")"); filter = s1; + r0.checkBinaryRelation(); } public Filter getFilter() { return filter; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/RangeIdentity.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java similarity index 70% rename from dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/RangeIdentity.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java index 6384993164..e7c91f762f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/RangeIdentity.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java @@ -7,13 +7,15 @@ import static com.google.common.base.Preconditions.checkNotNull; -public class RangeIdentity extends Definition { +public class Range extends Definition { private final Relation r1; - public RangeIdentity(Relation r0, Relation r1) { - super(r0, "[range(%s)]"); + public Range(Relation r0, Relation r1) { + super(r0, "range(%s)"); this.r1 = checkNotNull(r1); + r0.checkUnaryRelation(); + r1.checkBinaryRelation(); } public Relation getOperand() { return r1; } @@ -25,6 +27,6 @@ public List getConstrainedRelations() { @Override public T accept(Visitor v) { - return v.visitRangeIdentity(this); + return v.visitRange(this); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java index 350d874e01..b875f7e37e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java @@ -8,6 +8,7 @@ public class ReadFrom extends Definition { public ReadFrom(Relation r0) { super(r0, RelationNameRepository.RF); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java index 9df8309677..e29c19b732 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java @@ -8,6 +8,7 @@ public class SameLocation extends Definition { public SameLocation(Relation r0) { super(r0, RelationNameRepository.LOC); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java index 05d96e4262..57d8110c87 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java @@ -8,6 +8,7 @@ public class SameScope extends Definition { public SameScope(Relation r) { this(r, null); + r.checkBinaryRelation(); } public SameScope(Relation r, String specificScope) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java index 40940801a1..2f28fffba8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java @@ -8,6 +8,7 @@ public class SameVirtualLocation extends Definition { public SameVirtualLocation(Relation r0) { super(r0, RelationNameRepository.VLOC); + r0.checkBinaryRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java index 2e6d60c2bf..625aae6a92 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java @@ -1,21 +1,26 @@ package com.dat3m.dartagnan.wmm.definition; -import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; -//TODO: This relation may contain non-visible events. Is this reasonable? +import java.util.List; + public class SetIdentity extends Definition { - private final Filter filter; + private final Relation domain; - public SetIdentity(Relation r0, Filter s1) { - super(r0, "[" + s1 + "]"); - filter = s1; + public SetIdentity(Relation r0, Relation r1) { + super(r0, "[%s]"); + domain = r1; + r0.checkBinaryRelation(); + r1.checkUnaryRelation(); } - public Filter getFilter() { - return filter; + public Relation getDomain() { return domain; } + + @Override + public List getConstrainedRelations() { + return List.of(definedRelation, domain); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java index 1167a8bf64..7800003846 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java @@ -8,6 +8,7 @@ public class SyncBar extends Definition { public SyncBar(Relation r) { super(r, RelationNameRepository.SYNCBAR); + r.checkBinaryRelation(); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java index 31ceae3af9..67fdd05edd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java @@ -8,6 +8,7 @@ public class SyncFence extends Definition { public SyncFence(Relation r) { super(r, RelationNameRepository.SYNC_FENCE); + r.checkBinaryRelation(); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java index 6978d78e16..4d08f9e112 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java @@ -12,6 +12,7 @@ public class SyncWith extends Definition { public SyncWith(Relation r) { super(r, RelationNameRepository.SSW); + r.checkBinaryRelation(); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java new file mode 100644 index 0000000000..56cd9b05e1 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java @@ -0,0 +1,36 @@ +package com.dat3m.dartagnan.wmm.definition; + +import com.dat3m.dartagnan.wmm.Definition; +import com.dat3m.dartagnan.wmm.Relation; + +//TODO: This relation may contain non-visible events. Is this reasonable? +public class TagSet extends Definition { + + private final String tag; + + public TagSet(Relation r, String tag) { + super(r, tag); + this.tag = tag; + r.checkUnaryRelation(); + } + + protected TagSet(Relation r, String tag, String termPattern) { + super(r, termPattern); + this.tag = tag; + r.checkUnaryRelation(); + } + + public String getTag() { + return tag; + } + + @Override + public T accept(Visitor visitor) { + return visitor.visitTagSet(this); + } + + @Override + public String getTerm() { + return super.getTerm(); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java index 4157611739..cc4639883e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java @@ -14,6 +14,8 @@ public class TransitiveClosure extends Definition { public TransitiveClosure(Relation r0, Relation r1) { super(r0, "%s^+"); this.r1 = checkNotNull(r1); + r0.checkBinaryRelation(); + r1.checkBinaryRelation(); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Union.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Union.java index 45ba26e1a2..8f1ebdf16c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Union.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Union.java @@ -17,6 +17,7 @@ public class Union extends Definition { public Union(Relation r0, Relation... o) { super(r0, Stream.of(o).map(r -> "%s").collect(Collectors.joining(" | "))); operands = Stream.of(o).map(Preconditions::checkNotNull).toArray(Relation[]::new); + r0.checkEqualArityRelation(List.of(o)); } public List getOperands() { return Arrays.asList(operands); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java index f9ca0337ab..7982151936 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java @@ -73,18 +73,16 @@ private boolean areEquivalent(Relation r1, Relation r2) { return false; } + if (def1 instanceof TagSet set1 && def2 instanceof TagSet set2) { + return set1.getTag().equals(set2.getTag()); + } + if (def1 instanceof Definition.Undefined || def1 instanceof Free) { // Different undefined or free relations are never equal. return false; } // Special case for "semi-derived" relations - if (def1 instanceof SetIdentity s1 && def2 instanceof SetIdentity s2) { - return s1.getFilter().equals(s2.getFilter()); - } - if (def1 instanceof CartesianProduct p1 && def2 instanceof CartesianProduct p2) { - return p1.getFirstFilter().equals(p2.getFirstFilter()) && p1.getSecondFilter().equals(p2.getSecondFilter()); - } if (def1 instanceof SameScope s1 && def2 instanceof SameScope s2) { return Objects.equals(s1.getSpecificScope(), s2.getSpecificScope()); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java index f1f218815b..976a0efbba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java @@ -92,13 +92,13 @@ public Composition visitComposition(Composition def) { } @Override - public DomainIdentity visitDomainIdentity(DomainIdentity def) { - return new DomainIdentity(translate(def.getDefinedRelation()), translate(def.getOperand())); + public Domain visitDomain(Domain def) { + return new Domain(translate(def.getDefinedRelation()), translate(def.getOperand())); } @Override - public RangeIdentity visitRangeIdentity(RangeIdentity def) { - return new RangeIdentity(translate(def.getDefinedRelation()), translate(def.getOperand())); + public Range visitRange(Range def) { + return new Range(translate(def.getDefinedRelation()), translate(def.getOperand())); } @Override @@ -113,12 +113,12 @@ public TransitiveClosure visitTransitiveClosure(TransitiveClosure def) { @Override public SetIdentity visitSetIdentity(SetIdentity def) { - return new SetIdentity(translate(def.getDefinedRelation()), def.getFilter()); + return new SetIdentity(translate(def.getDefinedRelation()), translate(def.getDomain())); } @Override public CartesianProduct visitProduct(CartesianProduct def) { - return new CartesianProduct(translate(def.getDefinedRelation()), def.getFirstFilter(), def.getSecondFilter()); + return new CartesianProduct(translate(def.getDefinedRelation()), translate(def.getDomain()), translate(def.getRange())); } @Override @@ -131,6 +131,11 @@ public Empty visitEmpty(Empty def) { return new Empty(translate(def.getDefinedRelation())); } + @Override + public TagSet visitTagSet(TagSet def) { + return new TagSet(translate(def.getDefinedRelation()), def.getTag()); + } + @Override public ProgramOrder visitProgramOrder(ProgramOrder po) { return new ProgramOrder(translate(po.getDefinedRelation()), po.getFilter()); From ad81a9e6444c4d1575dc784ce8d7161de4e508b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Thu, 19 Jun 2025 12:42:16 +0200 Subject: [PATCH 02/17] Fix SimpleSet.initializeToDomain(Domain) --- .../solver/caat/predicates/sets/base/SimpleSet.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/base/SimpleSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/base/SimpleSet.java index caafbc8052..4af9eda9e9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/base/SimpleSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/predicates/sets/base/SimpleSet.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.solver.caat.predicates.sets.base; +import com.dat3m.dartagnan.solver.caat.domain.Domain; import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; import com.dat3m.dartagnan.solver.caat.predicates.Derivable; import com.dat3m.dartagnan.solver.caat.predicates.sets.Element; @@ -53,6 +54,12 @@ public Set setView() { return keySet; } + @Override + public void initializeToDomain(Domain domain) { + super.initializeToDomain(domain); + elements.clear(); + } + @Override public void backtrackTo(int time) { keySet.removeIf(e -> e.getTime() > time); From 35b460ca1553a2a27b58dd56e4297aa631b67760 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 20 Jun 2025 05:55:42 +0200 Subject: [PATCH 03/17] fixup! Support unary predicates in cat --- .../solver/caat/reasoning/Reasoner.java | 40 +++++++++---------- 1 file changed, 19 insertions(+), 21 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java index 4a5fcafd5e..64f1364142 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java @@ -220,27 +220,6 @@ public Conjunction visitSetIdentity(RelationGraph graph, Edge edge, return computeReason(inner, e); } - @Override - public Conjunction visitProjection(SetPredicate set, Edge edge, Void unused) { - assert edge.isLoop(); - - RelationGraph inner = (RelationGraph) set.getDependencies().get(0); - ProjectionSet.Dimension dim = ((ProjectionSet)set).getProjectionDimension(); - Iterable edges = switch (dim) { - case RANGE -> inner.inEdges(edge.getSecond()); - case DOMAIN -> inner.outEdges(edge.getFirst()); - }; - for (Edge e : edges) { - // We use the first edge we find - if (e.getDerivationLength() < edge.getDerivationLength()) { - Conjunction reason = computeReason(inner, e); - assert !reason.isFalse(); - return reason; - } - } - throw new IllegalStateException("ProjectionIdentityGraph: No matching edge is found"); - } - @Override public Conjunction visitReflexiveClosure(RelationGraph graph, Edge edge, Void unused) { if (edge.isLoop()) { @@ -332,5 +311,24 @@ public Conjunction visitSetDifference(SetPredicate set, Element ele public Conjunction visitBaseSet(SetPredicate set, Element ele, Void unused) { return new ElementLiteral(set, ele, true).toSingletonReason(); } + + @Override + public Conjunction visitProjection(SetPredicate set, Element ele, Void unused) { + RelationGraph inner = (RelationGraph) set.getDependencies().get(0); + ProjectionSet.Dimension dim = ((ProjectionSet)set).getProjectionDimension(); + Iterable edges = switch (dim) { + case RANGE -> inner.inEdges(ele.getId()); + case DOMAIN -> inner.outEdges(ele.getId()); + }; + for (Edge e : edges) { + // We use the first edge we find + if (e.getDerivationLength() < ele.getDerivationLength()) { + Conjunction reason = computeReason(inner, e); + assert !reason.isFalse(); + return reason; + } + } + throw new IllegalStateException("ProjectionIdentityGraph: No matching edge is found"); + } } } From 8b6753c94a9a74a686001ec8dc9f828eadbf8fcc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 20 Jun 2025 05:55:42 +0200 Subject: [PATCH 04/17] fixup! Support unary predicates in cat --- .../dartagnan/encoding/LazyEncodeSets.java | 42 ++++++--- .../solver/caat4wmm/ExecutionGraph.java | 38 +++++---- .../caat4wmm/basePredicates/StaticWMMSet.java | 11 ++- .../caat4wmm/coreReasoning/CoreReasoner.java | 15 ++-- .../model/ExecutionModelManager.java | 85 ++++++++++--------- .../wmm/analysis/LazyRelationAnalysis.java | 3 +- .../encoding/RelationAnalysisTest.java | 3 - 7 files changed, 115 insertions(+), 82 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java index 9ed9b91c44..0d0f8f503e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java @@ -46,16 +46,6 @@ 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); @@ -151,6 +141,38 @@ public Boolean visitSyncWith(SyncWith definition) { return doUpdateSelf(definition); } + @Override + public Boolean visitProduct(CartesianProduct definition) { + if (doUpdateSelf(definition)) { + long start = System.currentTimeMillis(); + MutableEventGraph domainUpdate = new MapEventGraph(); + MutableEventGraph rangeUpdate = new MapEventGraph(); + update.getDomain().forEach(e1 -> domainUpdate.add(e1, e1)); + update.getRange().forEach(e2 -> rangeUpdate.add(e2, e2)); + operandTime(definition, start, System.currentTimeMillis()); + setUpdate(domainUpdate); + definition.getDomain().getDefinition().accept(this); + setUpdate(rangeUpdate); + definition.getRange().getDefinition().accept(this); + return true; + } + return false; + } + + @Override + public Boolean visitSetIdentity(SetIdentity definition) { + if (doUpdateSelf(definition)) { + long start = System.currentTimeMillis(); + MutableEventGraph domainUpdate = new MapEventGraph(); + update.apply((e1, e2) -> domainUpdate.add(e1, e1)); + operandTime(definition, start, System.currentTimeMillis()); + setUpdate(domainUpdate); + definition.getDomain().getDefinition().accept(this); + return true; + } + return false; + } + @Override public Boolean visitDomain(Domain definition) { if (doUpdateSelf(definition)) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index 59c7b44f66..354c509dc9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -1,11 +1,11 @@ package com.dat3m.dartagnan.solver.caat4wmm; -import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.solver.caat.CAATModel; import com.dat3m.dartagnan.solver.caat.constraints.AcyclicityConstraint; import com.dat3m.dartagnan.solver.caat.constraints.Constraint; import com.dat3m.dartagnan.solver.caat.constraints.EmptinessConstraint; import com.dat3m.dartagnan.solver.caat.constraints.IrreflexivityConstraint; +import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.base.EmptyGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.*; @@ -42,8 +42,7 @@ public class ExecutionGraph { // assigned during construction. private final RefinementModel refinementModel; - private final BiMap relationGraphMap; - private final BiMap filterSetMap; + private final BiMap predicateToRelationMap; private final BiMap constraintMap; private final Set cutRelations; @@ -56,8 +55,7 @@ public class ExecutionGraph { public ExecutionGraph(RefinementModel refinementModel) { this.refinementModel = refinementModel; - relationGraphMap = HashBiMap.create(); - filterSetMap = HashBiMap.create(); + predicateToRelationMap = HashBiMap.create(); constraintMap = HashBiMap.create(); cutRelations = refinementModel.computeBoundaryRelations().stream() .filter(r -> r.getName().map(n -> !(n.equals(CO) || n.equals(RF))).orElse(true)) @@ -97,14 +95,14 @@ private void constructMappings() { RecursiveGraph graph = new RecursiveGraph(); graph.setName(relation.getNameOrTerm() + "_rec"); graphs.add(graph); - relationGraphMap.put(relation, graph); + predicateToRelationMap.put(relation, graph); } } for (DependencyGraph.Node node : component) { Relation relation = node.getContent(); if (relation.isRecursive()) { // side effect leads to calculation of children - RecursiveGraph graph = (RecursiveGraph) relationGraphMap.get(relation); + RecursiveGraph graph = (RecursiveGraph) predicateToRelationMap.get(relation); graph.setConcreteGraph(createGraphFromRelation(relation)); } } @@ -130,8 +128,8 @@ private void constructMappings() { public EventDomain getDomain() { return domain; } - public BiMap getRelationGraphMap() { - return Maps.unmodifiableBiMap(relationGraphMap); + public Relation getRelation(CAATPredicate predicate) { + return predicateToRelationMap.inverse().get(predicate); } public BiMap getAxiomConstraintMap() { @@ -140,12 +138,12 @@ public BiMap getAxiomConstraintMap() { public Set getCutRelations() { return cutRelations; } - public RelationGraph getRelationGraph(Relation rel) { - return relationGraphMap.get(rel); + public CAATPredicate getPredicate(Relation rel) { + return predicateToRelationMap.get(rel); } - public RelationGraph getRelationGraphByName(String name) { - return getRelationGraph(refinementModel.getOriginalModel().getRelation(name)); + public CAATPredicate getPredicateByName(String name) { + return getPredicate(refinementModel.getOriginalModel().getRelation(name)); } public Constraint getConstraint(Axiom axiom) { @@ -208,11 +206,12 @@ private Constraint getOrCreateConstraintFromAxiom(Axiom axiom) { } private RelationGraph getOrCreateGraphFromRelation(Relation rel) { - if (relationGraphMap.containsKey(rel)) { - return relationGraphMap.get(rel); + rel.checkBinaryRelation(); + if (predicateToRelationMap.containsKey(rel)) { + return (RelationGraph) predicateToRelationMap.get(rel); } RelationGraph graph = createGraphFromRelation(rel); - relationGraphMap.put(rel, graph); + predicateToRelationMap.put(rel, graph); return graph; } @@ -271,13 +270,17 @@ private RelationGraph createGraphFromRelation(Relation rel) { private SetPredicate getOrCreateSetFromRelation(Relation relation) { relation.checkUnaryRelation(); + final CAATPredicate existing = predicateToRelationMap.get(relation); + if (existing != null) { + return (SetPredicate) existing; + } final Class relClass = relation.getDefinition().getClass(); final List dependencies = relation.getDependencies(); final SetPredicate set; if (cutRelations.contains(relation)) { set = new DynamicDefaultWMMSet(refinementModel.translateToBase(relation)); } else if (relClass == TagSet.class) { - set = new StaticWMMSet(Filter.byTag(((TagSet) relation.getDefinition()).getTag())); + set = new StaticWMMSet(((TagSet) relation.getDefinition()).getTag()); } else if (relClass == Range.class || relClass == Domain.class) { RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0)); ProjectionSet.Dimension dim = relClass == Range.class ? @@ -297,6 +300,7 @@ private SetPredicate getOrCreateSetFromRelation(Relation relation) { } else { throw new UnsupportedOperationException(String.format("Cannot handle set %s with definition of type %s", relation, relClass.getSimpleName())); } + predicateToRelationMap.put(relation, set); set.setName(relation.getNameOrTerm()); return set; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/StaticWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/StaticWMMSet.java index 95416c5acd..837e71e19f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/StaticWMMSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/StaticWMMSet.java @@ -1,6 +1,5 @@ package com.dat3m.dartagnan.solver.caat4wmm.basePredicates; -import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; import com.dat3m.dartagnan.solver.caat.predicates.Derivable; import com.dat3m.dartagnan.solver.caat.predicates.misc.PredicateVisitor; @@ -16,11 +15,11 @@ public class StaticWMMSet extends AbstractWMMPredicate implements SetPredicate { - private final Filter filter; + private final String tag; private List events; - public StaticWMMSet(Filter filter) { - this.filter = filter; + public StaticWMMSet(String filter) { + this.tag = filter; } @Override @@ -31,7 +30,7 @@ public TRet accept(PredicateVisitor filter.apply(e.getEvent())) + .filter(e -> e.getEvent().hasTag(tag)) .map(e -> new Element(e.getId())).collect(Collectors.toList()); } @@ -56,7 +55,7 @@ public int size() { @Override public boolean containsById(int id) { - return filter.apply(getEvent(id).getEvent()); + return getEvent(id).getEvent().hasTag(tag); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java index f1e34e3641..daa3533168 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java @@ -15,6 +15,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.definition.TagSet; import com.google.common.collect.BiMap; import com.google.common.collect.HashBiMap; import org.sosy_lab.common.configuration.Option; @@ -150,17 +151,19 @@ private List getPermuted(List reason, Function toUnreducedCoreReason(Conjunction baseReason, EventDomain domain) { final List coreReason = new ArrayList<>(baseReason.getSize()); for (CAATLiteral lit : baseReason.getLiterals()) { + final Relation rel = executionGraph.getRelation(lit.getPredicate()); if (lit instanceof ElementLiteral eleLit) { - // FIXME: This step is not really faithful because we forget the unary predicate - // from which we derived the exec literals. - // This should be fine for now because all unary sets are static so they behave similarly. - // If we ever support dynamic unary predicates, this code needs to get updated. final Event e = domain.getObjectById(eleLit.getData().getId()).getEvent(); - coreReason.add(new ExecLiteral(e, lit.isPositive())); + final CoreLiteral coreLiteral; + if (rel.getDefinition() instanceof TagSet) { + coreLiteral = new ExecLiteral(e, true); + } else { + coreLiteral = new RelLiteral(rel, e, e, eleLit.isPositive()); + } + coreReason.add(coreLiteral); } else if (lit instanceof EdgeLiteral edgeLit) { final Event e1 = domain.getObjectById(edgeLit.getData().getFirst()).getEvent(); final Event e2 = domain.getObjectById(edgeLit.getData().getSecond()).getEvent(); - final Relation rel = executionGraph.getRelationGraphMap().inverse().get(edgeLit.getPredicate()); coreReason.add(new RelLiteral(rel, e1, e2, edgeLit.isPositive())); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java index 38f5b39fed..e83af55a9f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -10,11 +10,13 @@ import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.smt.ModelExt; import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate; +import com.dat3m.dartagnan.solver.caat.predicates.Derivable; import com.dat3m.dartagnan.solver.caat.predicates.PredicateHierarchy; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.base.SimpleGraph; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.derived.*; +import com.dat3m.dartagnan.solver.caat.predicates.sets.Element; import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate; import com.dat3m.dartagnan.solver.caat.predicates.sets.base.SimpleSet; import com.dat3m.dartagnan.solver.caat.predicates.sets.derived.DifferenceSet; @@ -43,8 +45,7 @@ public class ExecutionModelManager { private final RelationGraphPopulator graphPopulator; private final Map relModelCache; - private final BiMap setCache; - private final BiMap relGraphCache; + private final BiMap predicateCache; private final Map edgeModelCache; private ExecutionModelNext executionModel; @@ -58,8 +59,7 @@ public ExecutionModelManager() { graphBuilder = new RelationGraphBuilder(); graphPopulator = new RelationGraphPopulator(); relModelCache = new HashMap<>(); - setCache = HashBiMap.create(); - relGraphCache = HashBiMap.create(); + predicateCache = HashBiMap.create(); edgeModelCache = new HashMap<>(); } @@ -75,7 +75,7 @@ public ExecutionModelNext buildExecutionModel(EncodingContext context, ModelExt extractMemoryLayout(); relModelCache.clear(); - relGraphCache.clear(); + predicateCache.clear(); edgeModelCache.clear(); extractRelations(); @@ -181,7 +181,7 @@ private void extractRelations() { Set relsToExtract = new HashSet<>(wmm.getRelations()); for (Relation r : relsToExtract) { createModel(r); } - Set relGraphs = new HashSet<>(); + Set predicates = new HashSet<>(); DependencyGraph dependencyGraph = DependencyGraph.from(relsToExtract); for (Set.Node> component : dependencyGraph.getSCCs()) { @@ -190,29 +190,28 @@ private void extractRelations() { if (r.isRecursive()) { RecursiveGraph recGraph = new RecursiveGraph(); recGraph.setName(r.getNameOrTerm() + "_rec"); - relGraphs.add(recGraph); - relGraphCache.put(r, recGraph); + predicates.add(recGraph); + predicateCache.put(r, recGraph); } } for (DependencyGraph.Node node : component) { Relation r = node.getContent(); - RelationGraph rg = createGraph(r); + CAATPredicate predicate = createPredicate(r); if (r.isRecursive()) { - RecursiveGraph recGraph = (RecursiveGraph) relGraphCache.get(r); - recGraph.setConcreteGraph(rg); + RecursiveGraph recGraph = (RecursiveGraph) predicateCache.get(r); + recGraph.setConcreteGraph((RelationGraph) predicate); } else { - relGraphs.add(rg); + predicates.add(predicate); } } } - Set predicates = new HashSet<>(relGraphs); PredicateHierarchy hierarchy = new PredicateHierarchy(predicates); hierarchy.initializeToDomain(domain); // Populate graphs of base relations. for (CAATPredicate basePred : hierarchy.getBasePredicates()) { - Relation r = relGraphCache.inverse().get((RelationGraph) basePred); + Relation r = predicateCache.inverse().get(basePred); try { r.getDefinition().accept(graphPopulator); } catch (UnsupportedOperationException e) { @@ -224,12 +223,11 @@ private void extractRelations() { // Do the computation. hierarchy.populate(); - for (CAATPredicate pred : hierarchy.getPredicateList()) { - Relation r = relGraphCache.inverse().get((RelationGraph) pred); + for (CAATPredicate predicate : hierarchy.getPredicateList()) { + Relation r = predicateCache.inverse().get(predicate); if (relModelCache.containsKey(r)) { RelationModel rm = relModelCache.get(r); - ((RelationGraph) pred).edgeStream() - .forEach(e -> rm.addEdgeModel(getOrCreateEdgeModel(e))); + predicate.valueStream().forEach(e -> rm.addEdgeModel(getOrCreateEdgeModel(e))); } } @@ -243,39 +241,48 @@ private void createModel(Relation r) { relModelCache.put(r, new RelationModel(r)); } + private CAATPredicate createPredicate(Relation r) { + return r.isUnaryRelation() ? createSet(r) : createGraph(r); + } + private SetPredicate createSet(Relation r) { + r.checkUnaryRelation(); SetPredicate set = r.getDependencies().isEmpty() ? new SimpleSet() : r.getDefinition().accept(setBuilder); set.setName(r.getNameOrTerm()); if (!r.isRecursive()) { - setCache.put(r, set); + predicateCache.put(r, set); } return set; } private RelationGraph createGraph(Relation r) { + r.checkBinaryRelation(); RelationGraph rg = r.getDependencies().isEmpty() ? new SimpleGraph() : r.getDefinition().accept(graphBuilder); rg.setName(r.getNameOrTerm()); if (!r.isRecursive()) { - relGraphCache.put(r, rg); + predicateCache.put(r, rg); } return rg; } private SetPredicate getOrCreateSet(Relation r) { r.checkUnaryRelation(); - final SetPredicate existing = setCache.get(r); - return existing != null ? existing : createSet(r); + return (SetPredicate) getOrCreatePredicate(r); } private RelationGraph getOrCreateGraph(Relation r) { r.checkBinaryRelation(); - if (relGraphCache.containsKey(r)) { - return relGraphCache.get(r); - } - return createGraph(r); + return (RelationGraph) getOrCreatePredicate(r); + } + + private CAATPredicate getOrCreatePredicate(Relation r) { + final CAATPredicate cached = predicateCache.get(r); + return cached != null ? cached : createPredicate(r); } - private EdgeModel getOrCreateEdgeModel(Edge e) { + private EdgeModel getOrCreateEdgeModel(Derivable derivable) { + final int id = derivable instanceof Element x ? x.getId() : -1; + final Edge e = derivable instanceof Edge x ? x : new Edge(id, id); if (edgeModelCache.containsKey(e)) { return edgeModelCache.get(e); } @@ -291,15 +298,15 @@ private final class RelationGraphPopulator implements Visitor { @Override public Void visitTagSet(TagSet tagSet) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(tagSet.getDefinedRelation()); + SimpleSet rg = (SimpleSet) predicateCache.get(tagSet.getDefinedRelation()); executionModel.getEventModelsByFilter(Filter.byTag(tagSet.getTag())) - .forEach(e -> rg.add(new Edge(e.getId(), e.getId()))); + .forEach(e -> rg.add(new Element(e.getId()))); return null; } @Override public Void visitProgramOrder(ProgramOrder po) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(po.getDefinedRelation()); + SimpleGraph rg = (SimpleGraph) predicateCache.get(po.getDefinedRelation()); for (ThreadModel tm : executionModel.getThreadModels()) { List eventList = tm.getVisibleEventModels(); if (eventList.size() <= 1) { @@ -319,7 +326,7 @@ public Void visitProgramOrder(ProgramOrder po) { @Override public Void visitSameInstruction(SameInstruction si) { - final SimpleGraph rg = (SimpleGraph) relGraphCache.get(si.getDefinedRelation()); + final SimpleGraph rg = (SimpleGraph) predicateCache.get(si.getDefinedRelation()); final Map> instructionMap = new HashMap<>(); for (InstructionBoundary end : context.getTask().getProgram().getThreadEvents(InstructionBoundary.class)) { // NOTE begin markers return empty transaction event lists @@ -342,7 +349,7 @@ public Void visitSameInstruction(SameInstruction si) { @Override public Void visitReadFrom(ReadFrom readFrom) { Relation relation = readFrom.getDefinedRelation(); - SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation); + SimpleGraph rg = (SimpleGraph) predicateCache.get(relation); EncodingContext.EdgeEncoder rf = context.edge(relation); for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { @@ -362,7 +369,7 @@ public Void visitReadFrom(ReadFrom readFrom) { @Override public Void visitCoherence(Coherence coherence) { Relation relation = coherence.getDefinedRelation(); - SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation); + SimpleGraph rg = (SimpleGraph) predicateCache.get(relation); EncodingContext.EdgeEncoder co = context.edge(relation); for (Set writes : executionModel.getAddressWritesMap().values()) { @@ -388,7 +395,7 @@ public Void visitLXSXPairs(LXSXPairs lxsx) { } private Void visitReadModifyWrites(Relation relation) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation); + SimpleGraph rg = (SimpleGraph) predicateCache.get(relation); EncodingContext.EdgeEncoder rel = context.edge(relation); for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { @@ -407,7 +414,7 @@ private Void visitReadModifyWrites(Relation relation) { @Override public Void visitSameLocation(SameLocation loc) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(loc.getDefinedRelation()); + SimpleGraph rg = (SimpleGraph) predicateCache.get(loc.getDefinedRelation()); final Map> addressAccesses = new HashMap<>(); for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { @@ -438,7 +445,7 @@ public Void visitSameLocation(SameLocation loc) { @Override public Void visitInternal(Internal in) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(in.getDefinedRelation()); + SimpleGraph rg = (SimpleGraph) predicateCache.get(in.getDefinedRelation()); for (ThreadModel tm : executionModel.getThreadModels()) { List eventList = tm.getVisibleEventModels(); for (EventModel e1 : eventList) { @@ -452,7 +459,7 @@ public Void visitInternal(Internal in) { @Override public Void visitExternal(External ext) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(ext.getDefinedRelation()); + SimpleGraph rg = (SimpleGraph) predicateCache.get(ext.getDefinedRelation()); List threadList = executionModel.getThreadModels(); for (int i = 0; i < threadList.size(); i ++) { for (int j = i + 1; j < threadList.size(); j ++) { @@ -469,7 +476,7 @@ public Void visitExternal(External ext) { @Override public Void visitControlDependency(DirectControlDependency ctrlDirect) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(ctrlDirect.getDefinedRelation()); + SimpleGraph rg = (SimpleGraph) predicateCache.get(ctrlDirect.getDefinedRelation()); for (ThreadModel tm : executionModel.getThreadModels()) { for (EventModel em : tm.getEventModels()) { if (em instanceof CondJumpModel cjm) { @@ -488,7 +495,7 @@ public Void visitEmpty(Empty empty) { } public void populateDynamicDefaultGraph(Relation r) { - SimpleGraph rg = (SimpleGraph) relGraphCache.get(r); + SimpleGraph rg = (SimpleGraph) predicateCache.get(r); EncodingContext.EdgeEncoder edge = context.edge(r); RelationAnalysis.Knowledge k = context.getAnalysisContext() .get(RelationAnalysis.class) 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 index b517381b5d..07f839f0f1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java @@ -140,7 +140,8 @@ public RelationAnalysis.Knowledge visitProduct(CartesianProduct definition) { final EventGraph mustRange = range.getMustSet(); long start = System.currentTimeMillis(); final EventGraph may = new LazyEventGraph(mayDomain.getDomain(), mayRange.getDomain(), - (e1, e2) -> mayDomain.contains(e1, e1) && mayRange.contains(e2, e2)); + (e1, e2) -> mayDomain.contains(e1, e1) && mayRange.contains(e2, e2) && + !exec.areMutuallyExclusive(e1, e2)); final EventGraph must = new LazyEventGraph(mustDomain.getDomain(), mustRange.getDomain(), (e1, e2) -> mustDomain.contains(e1, e1) && mustRange.contains(e2, e2) && !exec.areMutuallyExclusive(e1, e2)); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java index 3772f65253..81f34fc7fc 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java @@ -2,8 +2,6 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.RelationAnalysisMethod; -import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.encoding.WmmEncoder; import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.program.Program; @@ -29,7 +27,6 @@ import java.util.EnumSet; import java.util.LinkedList; import java.util.List; -import com.dat3m.dartagnan.parsers.program.ProgramParser; import static com.dat3m.dartagnan.configuration.OptionNames.*; import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; From fcb23d02959fbd7ce5b0fb997d9398db0766f5d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Sat, 26 Jul 2025 01:04:02 +0200 Subject: [PATCH 05/17] Relation.Arity Add predefined relations M and _ Restore composition-based relations in RefinementSolver.addBiases() --- .../dat3m/dartagnan/encoding/EncodeSets.java | 8 +--- .../dat3m/dartagnan/encoding/WmmEncoder.java | 38 +++++++-------- .../dartagnan/parsers/cat/VisitorCat.java | 30 +++++------- .../solver/caat/reasoning/Reasoner.java | 2 +- .../solver/caat4wmm/RefinementModel.java | 2 +- .../basePredicates/DynamicDefaultWMMSet.java | 8 ++-- .../solving/RefinementSolver.java | 10 ++-- .../com/dat3m/dartagnan/wmm/Relation.java | 16 +++++-- .../dartagnan/wmm/RelationNameRepository.java | 4 ++ .../java/com/dat3m/dartagnan/wmm/Wmm.java | 48 ++++++++++++------- .../dartagnan/wmm/definition/TagSet.java | 5 -- 11 files changed, 89 insertions(+), 82 deletions(-) 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 6a8054704a..4ff257ba8b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java @@ -115,16 +115,12 @@ public Map visitRange(Range rangeId) { @Override public Map visitSetIdentity(SetIdentity id) { - final RelationAnalysis.Knowledge k1 = ra.getKnowledge(id.getDomain()); - return Map.of(id.getDomain(), - news.filter((e1, e2) -> k1.getMaySet().contains(e1, e2) && !k1.getMustSet().contains(e1, e2))); + return Map.of(id.getDomain(), filterUnknowns(news, id.getDomain())); } @Override public Map visitInverse(Inverse inv) { - final RelationAnalysis.Knowledge k1 = ra.getKnowledge(inv.getOperand()); - return Map.of(inv.getOperand(), - news.inverse().filter((e1, e2) -> k1.getMaySet().contains(e1, e2) && !k1.getMustSet().contains(e1, e2))); + return Map.of(inv.getOperand(), filterUnknowns(news.inverse(), inv.getOperand())); } @Override 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 73fb9e9e71..e329e0f3ac 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -446,17 +446,17 @@ public Void visitTransitiveClosure(TransitiveClosure trans) { @Override public Void visitSetIdentity(SetIdentity id) { - final Relation rel = id.getDefinedRelation(); - final Relation r1 = id.getDomain(); - EventGraph mustSet = ra.getKnowledge(rel).getMustSet(); - EncodingContext.EdgeEncoder enc0 = context.edge(rel); - EncodingContext.EdgeEncoder enc1 = context.edge(r1); - encodeSets.get(rel).apply((e1, e2) -> + final Relation setId = id.getDefinedRelation(); + final Relation domain = id.getDomain(); + EventGraph mustSet = ra.getKnowledge(setId).getMustSet(); + EncodingContext.EdgeEncoder encSetId = context.edge(setId); + EncodingContext.EdgeEncoder encDomain = context.edge(domain); + encodeSets.get(setId).apply((e1, e2) -> enc.add(bmgr.equivalence( - enc0.encode(e1, e2), + encSetId.encode(e1, e2), mustSet.contains(e1, e2) ? execution(e1, e2) : - enc1.encode(e1, e2)))); + encDomain.encode(e1, e2)))); return null; } @@ -477,20 +477,20 @@ public Void visitInverse(Inverse inv) { } @Override - public Void visitProduct(CartesianProduct product) { - final Relation rel = product.getDefinedRelation(); - final Relation r1 = product.getDomain(); - final Relation r2 = product.getRange(); - EventGraph mustSet = ra.getKnowledge(rel).getMustSet(); - EncodingContext.EdgeEncoder enc0 = context.edge(rel); - EncodingContext.EdgeEncoder enc1 = context.edge(r1); - EncodingContext.EdgeEncoder enc2 = context.edge(r2); - encodeSets.get(rel).apply((e1, e2) -> + public Void visitProduct(CartesianProduct cartesianProduct) { + final Relation product = cartesianProduct.getDefinedRelation(); + final Relation domain = cartesianProduct.getDomain(); + final Relation range = cartesianProduct.getRange(); + EventGraph mustSet = ra.getKnowledge(product).getMustSet(); + EncodingContext.EdgeEncoder encProduct = context.edge(product); + EncodingContext.EdgeEncoder encDomain = context.edge(domain); + EncodingContext.EdgeEncoder encRange = context.edge(range); + encodeSets.get(product).apply((e1, e2) -> enc.add(bmgr.equivalence( - enc0.encode(e1, e2), + encProduct.encode(e1, e2), mustSet.contains(e1, e2) ? execution(e1, e2) : - bmgr.and(enc1.encode(e1, e1), enc2.encode(e2, e2))))); + bmgr.and(encDomain.encode(e1, e1), encRange.encode(e2, e2))))); return null; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index 7e372ccae9..aea269e672 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -132,7 +132,7 @@ public Void visitAxiomDefinition(AxiomDefinitionContext ctx) { } private String createUniqueName(String name) { - if ((namespace.containsKey(name) || wmm.getRelation(name) != null) && !nameOccurrenceCounter.containsKey(name)) { + if (namespace.containsKey(name) && !nameOccurrenceCounter.containsKey(name)) { // If we have already seen the name, but not counted it yet, we do so now. nameOccurrenceCounter.put(name, 1); } @@ -207,7 +207,7 @@ public Object visitExpr(ExprContext ctx) { @Override public Object visitExprNew(ExprNewContext ctx) { final boolean unary = ctx.call.getText().equals("New"); - return addDefinition(new Free(wmm.newRelation(unary))); + return addDefinition(new Free(wmm.newRelation(unary ? Relation.Arity.UNARY : Relation.Arity.BINARY))); } @Override @@ -217,19 +217,11 @@ public Object visitExprBasic(ExprBasicContext ctx) { if (boundObject != null) { return boundObject; } - if (RelationNameRepository.contains(name)) { - return wmm.getOrCreatePredefinedRelation(name); - } - final Relation namedRelation = wmm.getRelation(name); - final Relation existingSet = namedRelation != null && namedRelation.getDefinition() instanceof TagSet s && s.getTag().equals(name) ? - namedRelation : wmm.getRelations().stream() - .filter(r -> r.getDefinition() instanceof TagSet s && s.getTag().equals(name)) - .findAny().orElse(null); - if (existingSet != null) { - return existingSet; - } - final Relation newRelation = namedRelation != null ? wmm.newRelation(true) : wmm.newRelation(name, true); - return addDefinition(new TagSet(newRelation, name)); + final boolean predefinedName = RelationNameRepository.contains(name); + final Relation predefined = predefinedName ? wmm.getOrCreatePredefinedRelation(name) : null; + final Relation newRelation = predefinedName ? predefined : addDefinition(new TagSet(wmm.newSet(name), name)); + namespace.put(name, newRelation); + return newRelation; } @Override @@ -265,7 +257,7 @@ public Object visitExprIntersection(ExprIntersectionContext c) { final Optional defRel = getAndResetRelationToBeDefined(); final Relation r1 = parseAsRelation(c.e1); final Relation r2 = parseAsRelation(c.e2); - final Relation r0 = defRel.orElseGet(() -> wmm.newRelation(r1.isUnaryRelation())); + final Relation r0 = defRel.orElseGet(() -> wmm.newRelation(r1.getArity())); return addDefinition(new Intersection(r0, r1, r2)); } @@ -274,7 +266,7 @@ public Object visitExprMinus(ExprMinusContext c) { checkNoRecursion(c); final Relation r1 = parseAsRelation(c.e1); final Relation r2 = parseAsRelation(c.e2); - final Relation r0 = wmm.newRelation(r1.isUnaryRelation()); + final Relation r0 = wmm.newRelation(r1.getArity()); return addDefinition(new Difference(r0, r1, r2)); } @@ -283,7 +275,7 @@ public Object visitExprUnion(ExprUnionContext c) { final Optional defRel = getAndResetRelationToBeDefined(); final Relation r1 = parseAsRelation(c.e1); final Relation r2 = parseAsRelation(c.e2); - final Relation r0 = defRel.orElseGet(() -> wmm.newRelation(r1.isUnaryRelation())); + final Relation r0 = defRel.orElseGet(() -> wmm.newRelation(r1.getArity())); return addDefinition(new Union(r0, r1, r2)); } @@ -293,7 +285,7 @@ public Object visitExprComplement(ExprComplementContext c) { final Relation r1 = parseAsRelation(c.e); final Relation visible = wmm.newSet(); wmm.addDefinition(new TagSet(visible, VISIBLE)); - final Relation r0 = wmm.newRelation(r1.isUnaryRelation()); + final Relation r0 = wmm.newRelation(r1.getArity()); final Relation all = r1.isUnaryRelation() ? visible : wmm.newRelation(); if (!r1.isUnaryRelation()) { wmm.addDefinition(new CartesianProduct(all, visible, visible)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java index 64f1364142..df0653965c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat/reasoning/Reasoner.java @@ -328,7 +328,7 @@ public Conjunction visitProjection(SetPredicate set, Element ele, V return reason; } } - throw new IllegalStateException("ProjectionIdentityGraph: No matching edge is found"); + throw new IllegalStateException("ProjectionSet: No matching element found."); } } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java index 38678a7b58..55164d523d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/RefinementModel.java @@ -112,7 +112,7 @@ public static RefinementModel fromCut(Cut cut) { // Skip the anarchic relations we already copied above continue; } - final Relation copy = base.newRelation(rel.isUnaryRelation()); + final Relation copy = base.newRelation(rel.getArity()); rel.getNames().forEach(n -> base.addAlias(n, copy)); orig2BaseRelations.put(rel, copy); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java index a4aa2040ae..90825cb9c7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java @@ -26,17 +26,17 @@ public void repopulate() { final EncodingContext.EdgeEncoder edge = ctx.edge(relation); final RelationAnalysis.Knowledge k = ctx.getAnalysisContext().get(RelationAnalysis.class).getKnowledge(relation); - if (k.getMaySet().size() < domain.size() * domain.size()) { + if (k.getMaySet().size() < domain.size()) { k.getMaySet().apply((e1, e2) -> { final EventData d1 = !e1.equals(e2) ? null : model.getData(e1).orElse(null); - final Element e = d1 == null ? null : getEdgeFromEventData(edge, d1, m); + final Element e = d1 == null ? null : getElementFromEventData(edge, d1, m); if (e != null) { simpleSet.add(e); } }); } else { for (EventData e1 : model.getEventList()) { - final Element e = getEdgeFromEventData(edge, e1, m); + final Element e = getElementFromEventData(edge, e1, m); if (e != null) { simpleSet.add(e); } @@ -44,7 +44,7 @@ public void repopulate() { } } - private Element getEdgeFromEventData(EncodingContext.EdgeEncoder edge, EventData e1, IREvaluator m) { + private Element getElementFromEventData(EncodingContext.EdgeEncoder edge, EventData e1, IREvaluator m) { return m.hasElement(edge, e1.getEvent()) ? new Element(e1.getId()) : null; } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index e6c962086a..9bc6dcb9f3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -568,15 +568,17 @@ private static void addBiases(Wmm wmm, EnumSet biases) { final Relation rfinv = wmm.addDefinition(new Inverse(wmm.newRelation(), rf)); final Relation frStandard = wmm.addDefinition(new Composition(wmm.newRelation(), rfinv, co)); - // ((R \ range(rf)) * W) & loc + // [R \ range(rf)];loc;[W] final Relation reads = wmm.addDefinition(new TagSet(wmm.newSet(), Tag.READ)); final Relation rfRange = wmm.addDefinition(new Range(wmm.newSet(), rf)); final Relation writes = wmm.addDefinition(new TagSet(wmm.newSet(), Tag.WRITE)); + final Relation writesSet = wmm.addDefinition(new SetIdentity(wmm.newRelation(), writes)); final Relation ur = wmm.addDefinition(new Difference(wmm.newSet(), reads, rfRange)); - final Relation urw = wmm.addDefinition(new CartesianProduct(wmm.newRelation(), ur, writes)); - final Relation urlocwrites = wmm.addDefinition(new Intersection(wmm.newRelation(), urw, loc)); + final Relation urSet = wmm.addDefinition(new SetIdentity(wmm.newRelation(), ur)); + final Relation urloc = wmm.addDefinition(new Composition(wmm.newRelation(), urSet, loc)); + final Relation urlocwrites = wmm.addDefinition(new Composition(wmm.newRelation(), urloc, writesSet)); - // let fr = rf^-1;co | (((R \ range(rf)) * W) & loc) + // let fr = rf^-1;co | [R \ range(rf)];loc;[W] final Relation fr = wmm.addDefinition(new Union(wmm.newRelation(), frStandard, urlocwrites)); if (biases.contains(Baseline.UNIPROC)) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java index 16518c704e..2a19ba44f6 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java @@ -15,22 +15,28 @@ public final class Relation implements Dependent { private final Wmm wmm; - private final boolean unary; + private final Arity arity; Definition definition = new Definition.Undefined(this); private boolean isRecursive; final List names = new ArrayList<>(); - Relation(Wmm wmm, boolean unary) { + public enum Arity { UNARY, BINARY } + + Relation(Wmm wmm, Arity arity) { this.wmm = wmm; - this.unary = unary; + this.arity = arity; + } + + public Arity getArity() { + return arity; } public boolean isUnaryRelation() { - return unary; + return arity == Arity.UNARY; } public boolean isBinaryRelation() { - return !unary; + return arity == Arity.BINARY; } public void checkUnaryRelation() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java index 73fd1571e7..dbf77a0a12 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.wmm; +import com.dat3m.dartagnan.program.event.Tag; import com.google.common.collect.ImmutableSet; import java.util.Arrays; @@ -38,6 +39,9 @@ public class RelationNameRepository { public static final String CTRLDIRECT = "__ctrlDirect"; public static final String IDDTRANS = "__iddTrans"; + public static final String VISIBLE = Tag.VISIBLE; + public static final String MEMORY = Tag.MEMORY; + public static final ImmutableSet RELATION_NAMES; static { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java index 78c670fca9..7304bdf28b 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java @@ -85,26 +85,30 @@ public void addAlias(String name, Relation relation) { } public Relation newSet() { - return newRelation(true); + return newRelation(Relation.Arity.UNARY); + } + + public Relation newSet(String name) { + return newRelation(name, Relation.Arity.UNARY); } public Relation newRelation() { - return newRelation(false); + return newRelation(Relation.Arity.BINARY); } - public Relation newRelation(boolean unary) { - final Relation relation = new Relation(this, unary); + public Relation newRelation(Relation.Arity arity) { + final Relation relation = new Relation(this, arity); relations.add(relation); return relation; } public Relation newRelation(String name) { - return newRelation(name, false); + return newRelation(name, Relation.Arity.BINARY); } - public Relation newRelation(String name, boolean unary) { + public Relation newRelation(String name, Relation.Arity arity) { checkArgument(!containsRelation(name), "Already bound name %s.", name); - final Relation relation = new Relation(this, unary); + final Relation relation = new Relation(this, arity); relation.names.add(name); relations.add(relation); return relation; @@ -197,11 +201,15 @@ private Relation makePredefinedRelation(String name) { will get constructed even if they already exist in the model. TODO: Clarify what the intended behaviour should be. */ - final Relation r = newRelation(name); + final Relation.Arity arity = switch (name) { + case VISIBLE, MEMORY -> Relation.Arity.UNARY; + default -> Relation.Arity.BINARY; + }; + final Relation r = newRelation(name, arity); final Definition def = switch (name) { case PO -> new ProgramOrder(r, Filter.byTag(Tag.VISIBLE)); case LOC -> new SameLocation(r); - case ID -> new SetIdentity(r, set(Tag.VISIBLE)); + case ID -> new SetIdentity(r, getOrCreatePredefinedRelation(VISIBLE)); case INT -> new Internal(r); case EXT -> new External(r); case CO -> new Coherence(r); @@ -216,16 +224,22 @@ private Relation makePredefinedRelation(String name) { case CTRLDIRECT -> new DirectControlDependency(r); case EMPTY -> new Empty(r); case IDDTRANS -> new TransitiveClosure(r, getOrCreatePredefinedRelation(IDD)); - case DATA -> new Intersection(r, getOrCreatePredefinedRelation(IDDTRANS), product(Tag.MEMORY, Tag.MEMORY)); + case DATA -> { + final Relation memory = getOrCreatePredefinedRelation(MEMORY); + yield new Intersection(r, getOrCreatePredefinedRelation(IDDTRANS), product(memory, memory)); + } case ADDR -> { + final Relation memory = getOrCreatePredefinedRelation(MEMORY); final Relation idd = getOrCreatePredefinedRelation(IDDTRANS); final Relation addr = getOrCreatePredefinedRelation(ADDRDIRECT); - yield new Intersection(r, union(addr, composition(idd, addr)), product(Tag.MEMORY, Tag.MEMORY)); + yield new Intersection(r, union(addr, composition(idd, addr)), product(memory, memory)); } case CTRL -> { + final Relation memory = getOrCreatePredefinedRelation(MEMORY); + final Relation visible = getOrCreatePredefinedRelation(VISIBLE); final Relation idd = getOrCreatePredefinedRelation(IDDTRANS); final Relation ctrl = getOrCreatePredefinedRelation(CTRLDIRECT); - yield new Intersection(r, composition(idd, ctrl), product(Tag.MEMORY, Tag.VISIBLE)); + yield new Intersection(r, composition(idd, ctrl), product(memory, visible)); } case SR -> new SameScope(r); case SCTA -> new SameScope(r, Tag.PTX.CTA); @@ -237,6 +251,8 @@ private Relation makePredefinedRelation(String name) { case SYNCBAR -> new SyncBar(r); case SYNC_FENCE -> new SyncFence(r); case VLOC -> new SameVirtualLocation(r); + case VISIBLE -> new TagSet(r, Tag.VISIBLE); + case MEMORY -> new TagSet(r, Tag.MEMORY); default -> throw new RuntimeException(name + " is part of RelationNameRepository but it has no associated relation."); }; @@ -251,11 +267,7 @@ private Relation composition(Relation r1, Relation r2) { return addDefinition(new Composition(newRelation(), r1, r2)); } - private Relation set(String tag) { - return addDefinition(new TagSet(newSet(), tag)); - } - - private Relation product(String tag1, String tag2) { - return addDefinition(new CartesianProduct(newRelation(), set(tag1), set(tag2))); + private Relation product(Relation domain, Relation range) { + return addDefinition(new CartesianProduct(newRelation(), domain, range)); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java index 56cd9b05e1..761a26a641 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java @@ -28,9 +28,4 @@ public String getTag() { public T accept(Visitor visitor) { return visitor.visitTagSet(this); } - - @Override - public String getTerm() { - return super.getTerm(); - } } From f91f7796ad27ab6d4b05f889540e98857c8ffdd1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 28 Jul 2025 13:22:46 +0200 Subject: [PATCH 06/17] fixup! Relation.Arity --- .../dartagnan/parsers/cat/VisitorCat.java | 10 +++---- .../com/dat3m/dartagnan/wmm/Relation.java | 27 ++++++++++++++++++- 2 files changed, 30 insertions(+), 7 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index aea269e672..ab702faca6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -144,12 +144,10 @@ private String createUniqueName(String name) { @Override public Void visitLetDefinition(LetDefinitionContext ctx) { - String name = ctx.n.getText(); - Object definedPredicate = ctx.e.accept(this); - if (definedPredicate instanceof Relation rel) { - String alias = createUniqueName(name); - wmm.addAlias(alias, rel); - } + final String name = ctx.n.getText(); + final Relation definedPredicate = (Relation) ctx.e.accept(this); + final String alias = createUniqueName(name); + wmm.addAlias(alias, definedPredicate); namespace.put(name, definedPredicate); return null; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java index 2a19ba44f6..24acadaf62 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java @@ -6,12 +6,17 @@ import com.google.common.base.Preconditions; import java.util.ArrayList; +import java.util.Collection; import java.util.List; import java.util.Optional; import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; import static com.google.common.base.Preconditions.checkState; +/** + * Given an execution, describes a set of events or a binary relation between events, + * constrained by the associated {@link Definition}. + */ public final class Relation implements Dependent { private final Wmm wmm; @@ -27,27 +32,47 @@ public enum Arity { UNARY, BINARY } this.arity = arity; } + /** + * @return {@link Arity#UNARY UNARY} if this instance describes an event set in executions. + * {@link Arity#BINARY BINARY} if this instance describes an event relation in executions. + */ public Arity getArity() { return arity; } + /** + * @return {@code true} if this instance describes an event set in executions. Otherwise {@code false}. + */ public boolean isUnaryRelation() { return arity == Arity.UNARY; } + /** + * @return {@code true} if this instance describes an event relation in executions. Otherwise {@code false}. + */ public boolean isBinaryRelation() { return arity == Arity.BINARY; } + /** + * @throws IllegalArgumentException This instance does not describe an event set in executions. + */ public void checkUnaryRelation() { Preconditions.checkArgument(isUnaryRelation(), "Non-unary relation %s.", this); } + /** + * @throws IllegalArgumentException This instance does not describe an event relation in executions. + */ public void checkBinaryRelation() { Preconditions.checkArgument(isBinaryRelation(), "Non-binary relation %s.", this); } - public void checkEqualArityRelation(List others) { + /** + * @param others Instances of this class. + * @throws IllegalArgumentException At least one instance in {@code others} has a different arity than this. + */ + public void checkEqualArityRelation(Collection others) { Preconditions.checkArgument(!isUnaryRelation() || others.stream().allMatch(Relation::isUnaryRelation), "Non-unary relation in %s", others); Preconditions.checkArgument(!isBinaryRelation() || others.stream().allMatch(Relation::isBinaryRelation), From 2d74f251a7564ca8cc444fa7c9ccecef312fba37 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 28 Jul 2025 14:27:50 +0200 Subject: [PATCH 07/17] fixup! Relation.Arity --- .../java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index ab702faca6..8d629dcb79 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -211,15 +211,14 @@ public Object visitExprNew(ExprNewContext ctx) { @Override public Object visitExprBasic(ExprBasicContext ctx) { final String name = ctx.n.getText(); - final Object boundObject = namespace.get(name); + final Object localObject = namespace.get(name); + final Object boundObject = localObject != null ? localObject : wmm.getRelation(name); if (boundObject != null) { return boundObject; } final boolean predefinedName = RelationNameRepository.contains(name); final Relation predefined = predefinedName ? wmm.getOrCreatePredefinedRelation(name) : null; - final Relation newRelation = predefinedName ? predefined : addDefinition(new TagSet(wmm.newSet(name), name)); - namespace.put(name, newRelation); - return newRelation; + return predefinedName ? predefined : addDefinition(new TagSet(wmm.newSet(name), name)); } @Override From 186256ff833e15e0471d80126a3aff208c4bcbe2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 28 Jul 2025 14:47:32 +0200 Subject: [PATCH 08/17] fixup! Relation.Arity --- .../main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index 8d629dcb79..e134cb4e82 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -132,9 +132,9 @@ public Void visitAxiomDefinition(AxiomDefinitionContext ctx) { } private String createUniqueName(String name) { - if (namespace.containsKey(name) && !nameOccurrenceCounter.containsKey(name)) { + if (wmm.containsRelation(name)) { // If we have already seen the name, but not counted it yet, we do so now. - nameOccurrenceCounter.put(name, 1); + nameOccurrenceCounter.putIfAbsent(name, 1); } final int occurrenceNumber = nameOccurrenceCounter.compute(name, (k, v) -> v == null ? 1 : v + 1); From 70140c8fb0f80fb57e5b511e40d527994e6dd516 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Mon, 28 Jul 2025 17:06:27 +0200 Subject: [PATCH 09/17] Refactor --- .../dat3m/dartagnan/encoding/IREvaluator.java | 4 ++-- .../dat3m/dartagnan/parsers/cat/VisitorCat.java | 4 ++-- .../solver/caat4wmm/ExecutionGraph.java | 6 +++--- .../basePredicates/DynamicDefaultWMMGraph.java | 2 +- .../basePredicates/DynamicDefaultWMMSet.java | 2 +- .../model/ExecutionModelManager.java | 10 +++++----- .../java/com/dat3m/dartagnan/wmm/Relation.java | 16 ++++++++-------- .../dat3m/dartagnan/wmm/axiom/Acyclicity.java | 4 ++-- .../dat3m/dartagnan/wmm/axiom/Irreflexivity.java | 4 ++-- .../dat3m/dartagnan/wmm/definition/AMOPairs.java | 2 +- .../dartagnan/wmm/definition/CASDependency.java | 2 +- .../wmm/definition/CartesianProduct.java | 6 +++--- .../dartagnan/wmm/definition/Coherence.java | 2 +- .../dartagnan/wmm/definition/Composition.java | 6 +++--- .../wmm/definition/DirectAddressDependency.java | 2 +- .../wmm/definition/DirectControlDependency.java | 2 +- .../wmm/definition/DirectDataDependency.java | 2 +- .../dat3m/dartagnan/wmm/definition/Domain.java | 4 ++-- .../dat3m/dartagnan/wmm/definition/External.java | 2 +- .../dat3m/dartagnan/wmm/definition/Internal.java | 2 +- .../dat3m/dartagnan/wmm/definition/Inverse.java | 4 ++-- .../dartagnan/wmm/definition/LXSXPairs.java | 2 +- .../wmm/definition/LinuxCriticalSections.java | 2 +- .../dartagnan/wmm/definition/ProgramOrder.java | 2 +- .../dat3m/dartagnan/wmm/definition/Range.java | 4 ++-- .../dat3m/dartagnan/wmm/definition/ReadFrom.java | 2 +- .../dartagnan/wmm/definition/SameLocation.java | 2 +- .../dartagnan/wmm/definition/SameScope.java | 2 +- .../wmm/definition/SameVirtualLocation.java | 2 +- .../dartagnan/wmm/definition/SetIdentity.java | 4 ++-- .../dat3m/dartagnan/wmm/definition/SyncBar.java | 2 +- .../dartagnan/wmm/definition/SyncFence.java | 2 +- .../dat3m/dartagnan/wmm/definition/SyncWith.java | 2 +- .../dat3m/dartagnan/wmm/definition/TagSet.java | 4 ++-- .../wmm/definition/TransitiveClosure.java | 4 ++-- 35 files changed, 62 insertions(+), 62 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java index 20c545e63d..917287a118 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/IREvaluator.java @@ -113,7 +113,7 @@ public TypedValue size(MemoryObject memoryObject) { // Memory Model public boolean hasElement(Relation rel, Event a) { - Preconditions.checkArgument(rel.isUnaryRelation(), "Non-unary relation %s", rel); + Preconditions.checkArgument(rel.isSet(), "Non-unary relation %s", rel); return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, a))); } @@ -122,7 +122,7 @@ public boolean hasElement(EncodingContext.EdgeEncoder edgeEncoder, Event a) { } public boolean hasEdge(Relation rel, Event a, Event b) { - Preconditions.checkArgument(rel.isBinaryRelation(), "Non-binary relation %s", rel); + Preconditions.checkArgument(rel.isRelation(), "Non-binary relation %s", rel); return TRUE.equals(smtModel.evaluate(ctx.edge(rel, a, b))); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index e134cb4e82..60e8f11643 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -283,8 +283,8 @@ public Object visitExprComplement(ExprComplementContext c) { final Relation visible = wmm.newSet(); wmm.addDefinition(new TagSet(visible, VISIBLE)); final Relation r0 = wmm.newRelation(r1.getArity()); - final Relation all = r1.isUnaryRelation() ? visible : wmm.newRelation(); - if (!r1.isUnaryRelation()) { + final Relation all = r1.isSet() ? visible : wmm.newRelation(); + if (!r1.isSet()) { wmm.addDefinition(new CartesianProduct(all, visible, visible)); } return addDefinition(new Difference(r0, all, r1)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index 354c509dc9..136136c5a7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -206,7 +206,7 @@ private Constraint getOrCreateConstraintFromAxiom(Axiom axiom) { } private RelationGraph getOrCreateGraphFromRelation(Relation rel) { - rel.checkBinaryRelation(); + rel.checkRelation(); if (predicateToRelationMap.containsKey(rel)) { return (RelationGraph) predicateToRelationMap.get(rel); } @@ -216,7 +216,7 @@ private RelationGraph getOrCreateGraphFromRelation(Relation rel) { } private RelationGraph createGraphFromRelation(Relation rel) { - rel.checkBinaryRelation(); + rel.checkRelation(); final RelationGraph graph; final Class relClass = rel.getDefinition().getClass(); final List dependencies = rel.getDependencies(); @@ -269,7 +269,7 @@ private RelationGraph createGraphFromRelation(Relation rel) { } private SetPredicate getOrCreateSetFromRelation(Relation relation) { - relation.checkUnaryRelation(); + relation.checkSet(); final CAATPredicate existing = predicateToRelationMap.get(relation); if (existing != null) { return (SetPredicate) existing; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java index c0534c7b82..c699a2b84b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java @@ -12,7 +12,7 @@ public class DynamicDefaultWMMGraph extends MaterializedWMMGraph { private final Relation relation; public DynamicDefaultWMMGraph(Relation rel) { - rel.checkBinaryRelation(); + rel.checkRelation(); this.relation = rel; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java index 90825cb9c7..c49af84eaa 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java @@ -13,7 +13,7 @@ public class DynamicDefaultWMMSet extends MaterializedWMMSet { private final Relation relation; public DynamicDefaultWMMSet(Relation rel) { - rel.checkUnaryRelation(); + rel.checkSet(); this.relation = rel; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java index e83af55a9f..c7f0313f84 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -242,11 +242,11 @@ private void createModel(Relation r) { } private CAATPredicate createPredicate(Relation r) { - return r.isUnaryRelation() ? createSet(r) : createGraph(r); + return r.isSet() ? createSet(r) : createGraph(r); } private SetPredicate createSet(Relation r) { - r.checkUnaryRelation(); + r.checkSet(); SetPredicate set = r.getDependencies().isEmpty() ? new SimpleSet() : r.getDefinition().accept(setBuilder); set.setName(r.getNameOrTerm()); if (!r.isRecursive()) { @@ -256,7 +256,7 @@ private SetPredicate createSet(Relation r) { } private RelationGraph createGraph(Relation r) { - r.checkBinaryRelation(); + r.checkRelation(); RelationGraph rg = r.getDependencies().isEmpty() ? new SimpleGraph() : r.getDefinition().accept(graphBuilder); rg.setName(r.getNameOrTerm()); if (!r.isRecursive()) { @@ -266,12 +266,12 @@ private RelationGraph createGraph(Relation r) { } private SetPredicate getOrCreateSet(Relation r) { - r.checkUnaryRelation(); + r.checkSet(); return (SetPredicate) getOrCreatePredicate(r); } private RelationGraph getOrCreateGraph(Relation r) { - r.checkBinaryRelation(); + r.checkRelation(); return (RelationGraph) getOrCreatePredicate(r); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java index 24acadaf62..d449424e30 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java @@ -43,29 +43,29 @@ public Arity getArity() { /** * @return {@code true} if this instance describes an event set in executions. Otherwise {@code false}. */ - public boolean isUnaryRelation() { + public boolean isSet() { return arity == Arity.UNARY; } /** * @return {@code true} if this instance describes an event relation in executions. Otherwise {@code false}. */ - public boolean isBinaryRelation() { + public boolean isRelation() { return arity == Arity.BINARY; } /** * @throws IllegalArgumentException This instance does not describe an event set in executions. */ - public void checkUnaryRelation() { - Preconditions.checkArgument(isUnaryRelation(), "Non-unary relation %s.", this); + public void checkSet() { + Preconditions.checkArgument(isSet(), "Non-unary relation %s.", this); } /** * @throws IllegalArgumentException This instance does not describe an event relation in executions. */ - public void checkBinaryRelation() { - Preconditions.checkArgument(isBinaryRelation(), "Non-binary relation %s.", this); + public void checkRelation() { + Preconditions.checkArgument(isRelation(), "Non-binary relation %s.", this); } /** @@ -73,9 +73,9 @@ public void checkBinaryRelation() { * @throws IllegalArgumentException At least one instance in {@code others} has a different arity than this. */ public void checkEqualArityRelation(Collection others) { - Preconditions.checkArgument(!isUnaryRelation() || others.stream().allMatch(Relation::isUnaryRelation), + Preconditions.checkArgument(!isSet() || others.stream().allMatch(Relation::isSet), "Non-unary relation in %s", others); - Preconditions.checkArgument(!isBinaryRelation() || others.stream().allMatch(Relation::isBinaryRelation), + Preconditions.checkArgument(!isRelation() || others.stream().allMatch(Relation::isRelation), "Non-binary relation in %s", others); } 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 24fa71fd06..2166239245 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 @@ -27,12 +27,12 @@ public class Acyclicity extends Axiom { public Acyclicity(Relation rel, boolean negated, boolean flag) { super(rel, negated, flag); - rel.checkBinaryRelation(); + rel.checkRelation(); } public Acyclicity(Relation rel) { super(rel, false, false); - rel.checkBinaryRelation(); + rel.checkRelation(); } // Under-approximates the must-set of (rel+ ; rel). 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 136f0269a2..5b07676483 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 @@ -16,12 +16,12 @@ public class Irreflexivity extends Axiom { public Irreflexivity(Relation rel, boolean negated, boolean flag) { super(rel, negated, flag); - rel.checkBinaryRelation(); + rel.checkRelation(); } public Irreflexivity(Relation rel) { super(rel, false, false); - rel.checkBinaryRelation(); + rel.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java index fb0821b1eb..5c3f690992 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java @@ -8,7 +8,7 @@ public class AMOPairs extends Definition { public AMOPairs(Relation r0) { super(r0, RelationNameRepository.AMO); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java index d1b8251e95..0241b95a13 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java @@ -9,7 +9,7 @@ public class CASDependency extends Definition { public CASDependency(Relation r0) { super(r0, CASDEP); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java index 82c0666629..30dea30f0a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java @@ -14,9 +14,9 @@ public CartesianProduct(Relation r0, Relation r1, Relation r2) { super(r0, "%s*%s"); domain = r1; range = r2; - r0.checkBinaryRelation(); - r1.checkUnaryRelation(); - r2.checkUnaryRelation(); + r0.checkRelation(); + r1.checkSet(); + r2.checkSet(); } public Relation getDomain() { return domain; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java index 022df92f59..cceab19d99 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java @@ -9,7 +9,7 @@ public class Coherence extends Definition { public Coherence(Relation r0) { super(r0, CO); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java index 363f114df3..12cf96dd20 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java @@ -16,9 +16,9 @@ public Composition(Relation r0, Relation r1, Relation r2) { super(r0, "%s ; %s"); left = checkNotNull(r1); right = checkNotNull(r2); - r0.checkBinaryRelation(); - r1.checkBinaryRelation(); - r2.checkBinaryRelation(); + r0.checkRelation(); + r1.checkRelation(); + r2.checkRelation(); } public Relation getLeftOperand() { return left; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java index 15a080efeb..318585b051 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java @@ -9,7 +9,7 @@ public class DirectAddressDependency extends Definition { public DirectAddressDependency(Relation r0) { super(r0, RelationNameRepository.ADDRDIRECT); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java index 2de24bfc50..9c7abbf105 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java @@ -11,7 +11,7 @@ public class DirectControlDependency extends Definition { public DirectControlDependency(Relation r0) { super(r0, CTRLDIRECT); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java index 71986d4046..c2f4c5ec93 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java @@ -9,7 +9,7 @@ public class DirectDataDependency extends Definition { public DirectDataDependency(Relation r0) { super(r0, RelationNameRepository.IDD); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java index 66377354a9..075d525eff 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java @@ -14,8 +14,8 @@ public class Domain extends Definition { public Domain(Relation r0, Relation r1) { super(r0, "domain(%s)"); this.r1 = checkNotNull(r1); - r0.checkUnaryRelation(); - r1.checkBinaryRelation(); + r0.checkSet(); + r1.checkRelation(); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java index 0ce66e5c5d..14f2ea14f4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java @@ -9,7 +9,7 @@ public class External extends Definition { public External(Relation r0) { super(r0, EXT); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java index 5faf6e5a10..3d6a671052 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java @@ -9,7 +9,7 @@ public class Internal extends Definition { public Internal(Relation r0) { super(r0, INT); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java index 72dd85e53a..f5c2929a6d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java @@ -16,8 +16,8 @@ public class Inverse extends Definition { public Inverse(Relation r0, Relation r1) { super(r0, "%s^-1"); this.r1 = checkNotNull(r1); - r0.checkBinaryRelation(); - r1.checkBinaryRelation(); + r0.checkRelation(); + r1.checkRelation(); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java index d3ab16dbec..9f6a43b0ed 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java @@ -8,7 +8,7 @@ public class LXSXPairs extends Definition { public LXSXPairs(Relation r0) { super(r0, RelationNameRepository.LXSX); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java index 6a071bf508..db2b59f741 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java @@ -8,7 +8,7 @@ public class LinuxCriticalSections extends Definition { public LinuxCriticalSections(Relation r0) { super(r0, RelationNameRepository.CRIT); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java index 37df6c0070..10a709e7f3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java @@ -11,7 +11,7 @@ public class ProgramOrder extends Definition { public ProgramOrder(Relation r0, Filter s1) { super(r0, "po(" + s1 + ")"); filter = s1; - r0.checkBinaryRelation(); + r0.checkRelation(); } public Filter getFilter() { return filter; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java index e7c91f762f..0161a08d66 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java @@ -14,8 +14,8 @@ public class Range extends Definition { public Range(Relation r0, Relation r1) { super(r0, "range(%s)"); this.r1 = checkNotNull(r1); - r0.checkUnaryRelation(); - r1.checkBinaryRelation(); + r0.checkSet(); + r1.checkRelation(); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java index b875f7e37e..91dd12ef85 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java @@ -8,7 +8,7 @@ public class ReadFrom extends Definition { public ReadFrom(Relation r0) { super(r0, RelationNameRepository.RF); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java index e29c19b732..1a4dc4a190 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java @@ -8,7 +8,7 @@ public class SameLocation extends Definition { public SameLocation(Relation r0) { super(r0, RelationNameRepository.LOC); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java index 57d8110c87..7c81b44d95 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java @@ -8,7 +8,7 @@ public class SameScope extends Definition { public SameScope(Relation r) { this(r, null); - r.checkBinaryRelation(); + r.checkRelation(); } public SameScope(Relation r, String specificScope) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java index 2f28fffba8..2d20c080fb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java @@ -8,7 +8,7 @@ public class SameVirtualLocation extends Definition { public SameVirtualLocation(Relation r0) { super(r0, RelationNameRepository.VLOC); - r0.checkBinaryRelation(); + r0.checkRelation(); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java index 625aae6a92..4d9e6b12b7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java @@ -12,8 +12,8 @@ public class SetIdentity extends Definition { public SetIdentity(Relation r0, Relation r1) { super(r0, "[%s]"); domain = r1; - r0.checkBinaryRelation(); - r1.checkUnaryRelation(); + r0.checkRelation(); + r1.checkSet(); } public Relation getDomain() { return domain; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java index 7800003846..ea5792436e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java @@ -8,7 +8,7 @@ public class SyncBar extends Definition { public SyncBar(Relation r) { super(r, RelationNameRepository.SYNCBAR); - r.checkBinaryRelation(); + r.checkRelation(); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java index 67fdd05edd..3d4f91842d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java @@ -8,7 +8,7 @@ public class SyncFence extends Definition { public SyncFence(Relation r) { super(r, RelationNameRepository.SYNC_FENCE); - r.checkBinaryRelation(); + r.checkRelation(); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java index 4d08f9e112..a3c348fceb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java @@ -12,7 +12,7 @@ public class SyncWith extends Definition { public SyncWith(Relation r) { super(r, RelationNameRepository.SSW); - r.checkBinaryRelation(); + r.checkRelation(); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java index 761a26a641..7426dff918 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java @@ -11,13 +11,13 @@ public class TagSet extends Definition { public TagSet(Relation r, String tag) { super(r, tag); this.tag = tag; - r.checkUnaryRelation(); + r.checkSet(); } protected TagSet(Relation r, String tag, String termPattern) { super(r, termPattern); this.tag = tag; - r.checkUnaryRelation(); + r.checkSet(); } public String getTag() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java index cc4639883e..4f7fd915af 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java @@ -14,8 +14,8 @@ public class TransitiveClosure extends Definition { public TransitiveClosure(Relation r0, Relation r1) { super(r0, "%s^+"); this.r1 = checkNotNull(r1); - r0.checkBinaryRelation(); - r1.checkBinaryRelation(); + r0.checkRelation(); + r1.checkRelation(); } public Relation getOperand() { return r1; } From 053678de226d32d93e9d1dd8ac74695044ef3bbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Tue, 29 Jul 2025 12:44:40 +0200 Subject: [PATCH 10/17] Relation.checkIsRelation(Relation) --- .../solver/caat4wmm/ExecutionGraph.java | 6 ++-- .../DynamicDefaultWMMGraph.java | 3 +- .../basePredicates/DynamicDefaultWMMSet.java | 5 ++-- .../model/ExecutionModelManager.java | 10 +++---- .../com/dat3m/dartagnan/wmm/Relation.java | 30 ++++--------------- .../dat3m/dartagnan/wmm/axiom/Acyclicity.java | 6 ++-- .../dartagnan/wmm/axiom/Irreflexivity.java | 6 ++-- .../dartagnan/wmm/definition/AMOPairs.java | 3 +- .../wmm/definition/CASDependency.java | 3 +- .../wmm/definition/CartesianProduct.java | 9 ++---- .../dartagnan/wmm/definition/Coherence.java | 3 +- .../dartagnan/wmm/definition/Composition.java | 11 ++----- .../definition/DirectAddressDependency.java | 3 +- .../definition/DirectControlDependency.java | 3 +- .../wmm/definition/DirectDataDependency.java | 3 +- .../dartagnan/wmm/definition/Domain.java | 8 ++--- .../dartagnan/wmm/definition/External.java | 3 +- .../dartagnan/wmm/definition/Internal.java | 3 +- .../dartagnan/wmm/definition/Inverse.java | 8 ++--- .../dartagnan/wmm/definition/LXSXPairs.java | 3 +- .../wmm/definition/LinuxCriticalSections.java | 3 +- .../wmm/definition/ProgramOrder.java | 3 +- .../dat3m/dartagnan/wmm/definition/Range.java | 8 ++--- .../dartagnan/wmm/definition/ReadFrom.java | 3 +- .../wmm/definition/SameLocation.java | 3 +- .../dartagnan/wmm/definition/SameScope.java | 3 +- .../wmm/definition/SameVirtualLocation.java | 3 +- .../dartagnan/wmm/definition/SetIdentity.java | 6 ++-- .../dartagnan/wmm/definition/SyncBar.java | 3 +- .../dartagnan/wmm/definition/SyncFence.java | 3 +- .../dartagnan/wmm/definition/SyncWith.java | 3 +- .../dartagnan/wmm/definition/TagSet.java | 5 +--- .../wmm/definition/TransitiveClosure.java | 8 ++--- 33 files changed, 55 insertions(+), 128 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index 136136c5a7..660469b01f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -206,7 +206,7 @@ private Constraint getOrCreateConstraintFromAxiom(Axiom axiom) { } private RelationGraph getOrCreateGraphFromRelation(Relation rel) { - rel.checkRelation(); + Relation.checkIsRelation(rel); if (predicateToRelationMap.containsKey(rel)) { return (RelationGraph) predicateToRelationMap.get(rel); } @@ -216,7 +216,7 @@ private RelationGraph getOrCreateGraphFromRelation(Relation rel) { } private RelationGraph createGraphFromRelation(Relation rel) { - rel.checkRelation(); + Relation.checkIsRelation(rel); final RelationGraph graph; final Class relClass = rel.getDefinition().getClass(); final List dependencies = rel.getDependencies(); @@ -269,7 +269,7 @@ private RelationGraph createGraphFromRelation(Relation rel) { } private SetPredicate getOrCreateSetFromRelation(Relation relation) { - relation.checkSet(); + Relation.checkIsSet(relation); final CAATPredicate existing = predicateToRelationMap.get(relation); if (existing != null) { return (SetPredicate) existing; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java index c699a2b84b..abc7ee56f3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMGraph.java @@ -12,8 +12,7 @@ public class DynamicDefaultWMMGraph extends MaterializedWMMGraph { private final Relation relation; public DynamicDefaultWMMGraph(Relation rel) { - rel.checkRelation(); - this.relation = rel; + this.relation = Relation.checkIsRelation(rel); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java index c49af84eaa..6a288c9282 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java @@ -12,9 +12,8 @@ public class DynamicDefaultWMMSet extends MaterializedWMMSet { private final Relation relation; - public DynamicDefaultWMMSet(Relation rel) { - rel.checkSet(); - this.relation = rel; + public DynamicDefaultWMMSet(Relation predicate) { + this.relation = Relation.checkIsSet(predicate); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java index c7f0313f84..da43e51d30 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -246,7 +246,7 @@ private CAATPredicate createPredicate(Relation r) { } private SetPredicate createSet(Relation r) { - r.checkSet(); + Relation.checkIsSet(r); SetPredicate set = r.getDependencies().isEmpty() ? new SimpleSet() : r.getDefinition().accept(setBuilder); set.setName(r.getNameOrTerm()); if (!r.isRecursive()) { @@ -256,7 +256,7 @@ private SetPredicate createSet(Relation r) { } private RelationGraph createGraph(Relation r) { - r.checkRelation(); + Relation.checkIsRelation(r); RelationGraph rg = r.getDependencies().isEmpty() ? new SimpleGraph() : r.getDefinition().accept(graphBuilder); rg.setName(r.getNameOrTerm()); if (!r.isRecursive()) { @@ -266,13 +266,11 @@ private RelationGraph createGraph(Relation r) { } private SetPredicate getOrCreateSet(Relation r) { - r.checkSet(); - return (SetPredicate) getOrCreatePredicate(r); + return (SetPredicate) getOrCreatePredicate(Relation.checkIsSet(r)); } private RelationGraph getOrCreateGraph(Relation r) { - r.checkRelation(); - return (RelationGraph) getOrCreatePredicate(r); + return (RelationGraph) getOrCreatePredicate(Relation.checkIsRelation(r)); } private CAATPredicate getOrCreatePredicate(Relation r) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java index d449424e30..09289c2566 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java @@ -32,46 +32,28 @@ public enum Arity { UNARY, BINARY } this.arity = arity; } - /** - * @return {@link Arity#UNARY UNARY} if this instance describes an event set in executions. - * {@link Arity#BINARY BINARY} if this instance describes an event relation in executions. - */ public Arity getArity() { return arity; } - /** - * @return {@code true} if this instance describes an event set in executions. Otherwise {@code false}. - */ public boolean isSet() { return arity == Arity.UNARY; } - /** - * @return {@code true} if this instance describes an event relation in executions. Otherwise {@code false}. - */ public boolean isRelation() { return arity == Arity.BINARY; } - /** - * @throws IllegalArgumentException This instance does not describe an event set in executions. - */ - public void checkSet() { - Preconditions.checkArgument(isSet(), "Non-unary relation %s.", this); + public static Relation checkIsSet(Relation relation) { + Preconditions.checkArgument(relation.isSet(), "Non-unary relation %s.", relation); + return relation; } - /** - * @throws IllegalArgumentException This instance does not describe an event relation in executions. - */ - public void checkRelation() { - Preconditions.checkArgument(isRelation(), "Non-binary relation %s.", this); + public static Relation checkIsRelation(Relation relation) { + Preconditions.checkArgument(relation.isRelation(), "Non-binary relation %s.", relation); + return relation; } - /** - * @param others Instances of this class. - * @throws IllegalArgumentException At least one instance in {@code others} has a different arity than this. - */ public void checkEqualArityRelation(Collection others) { Preconditions.checkArgument(!isSet() || others.stream().allMatch(Relation::isSet), "Non-unary relation in %s", others); 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 2166239245..a3da80f47b 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 @@ -26,13 +26,11 @@ public class Acyclicity extends Axiom { private static final Logger logger = LogManager.getLogger(Acyclicity.class); public Acyclicity(Relation rel, boolean negated, boolean flag) { - super(rel, negated, flag); - rel.checkRelation(); + super(Relation.checkIsRelation(rel), negated, flag); } public Acyclicity(Relation rel) { - super(rel, false, false); - rel.checkRelation(); + this(rel, false, false); } // Under-approximates the must-set of (rel+ ; rel). 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 5b07676483..469c349653 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 @@ -15,13 +15,11 @@ public class Irreflexivity extends Axiom { public Irreflexivity(Relation rel, boolean negated, boolean flag) { - super(rel, negated, flag); - rel.checkRelation(); + super(Relation.checkIsRelation(rel), negated, flag); } public Irreflexivity(Relation rel) { - super(rel, false, false); - rel.checkRelation(); + this(rel, false, false); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java index 5c3f690992..66f3f2dddc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/AMOPairs.java @@ -7,8 +7,7 @@ public class AMOPairs extends Definition { public AMOPairs(Relation r0) { - super(r0, RelationNameRepository.AMO); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.AMO); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java index 0241b95a13..0edee782df 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CASDependency.java @@ -8,8 +8,7 @@ public class CASDependency extends Definition { public CASDependency(Relation r0) { - super(r0, CASDEP); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), CASDEP); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java index 30dea30f0a..df3e9987f7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/CartesianProduct.java @@ -11,12 +11,9 @@ public class CartesianProduct extends Definition { private final Relation range; public CartesianProduct(Relation r0, Relation r1, Relation r2) { - super(r0, "%s*%s"); - domain = r1; - range = r2; - r0.checkRelation(); - r1.checkSet(); - r2.checkSet(); + super(Relation.checkIsRelation(r0), "%s*%s"); + domain = Relation.checkIsSet(r1); + range = Relation.checkIsSet(r2); } public Relation getDomain() { return domain; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java index cceab19d99..aef5b398e2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Coherence.java @@ -8,8 +8,7 @@ public class Coherence extends Definition { public Coherence(Relation r0) { - super(r0, CO); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), CO); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java index 12cf96dd20..a51a24ad64 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Composition.java @@ -5,20 +5,15 @@ import java.util.List; -import static com.google.common.base.Preconditions.checkNotNull; - public class Composition extends Definition { private final Relation left; private final Relation right; public Composition(Relation r0, Relation r1, Relation r2) { - super(r0, "%s ; %s"); - left = checkNotNull(r1); - right = checkNotNull(r2); - r0.checkRelation(); - r1.checkRelation(); - r2.checkRelation(); + super(Relation.checkIsRelation(r0), "%s ; %s"); + left = Relation.checkIsRelation(r1); + right = Relation.checkIsRelation(r2); } public Relation getLeftOperand() { return left; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java index 318585b051..83581af2dc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectAddressDependency.java @@ -8,8 +8,7 @@ public class DirectAddressDependency extends Definition { public DirectAddressDependency(Relation r0) { - super(r0, RelationNameRepository.ADDRDIRECT); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.ADDRDIRECT); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java index 9c7abbf105..5fc769c91f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java @@ -10,8 +10,7 @@ public class DirectControlDependency extends Definition { public DirectControlDependency(Relation r0) { - super(r0, CTRLDIRECT); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), CTRLDIRECT); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java index c2f4c5ec93..c8c4aa0db0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectDataDependency.java @@ -8,8 +8,7 @@ public class DirectDataDependency extends Definition { public DirectDataDependency(Relation r0) { - super(r0, RelationNameRepository.IDD); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.IDD); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java index 075d525eff..36192d88b1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java @@ -5,17 +5,13 @@ import java.util.List; -import static com.google.common.base.Preconditions.checkNotNull; - public class Domain extends Definition { private final Relation r1; public Domain(Relation r0, Relation r1) { - super(r0, "domain(%s)"); - this.r1 = checkNotNull(r1); - r0.checkSet(); - r1.checkRelation(); + super(Relation.checkIsSet(r0), "domain(%s)"); + this.r1 = Relation.checkIsRelation(r1); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java index 14f2ea14f4..39c66b9881 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/External.java @@ -8,8 +8,7 @@ public class External extends Definition { public External(Relation r0) { - super(r0, EXT); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), EXT); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java index 3d6a671052..0ea982c149 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Internal.java @@ -8,8 +8,7 @@ public class Internal extends Definition { public Internal(Relation r0) { - super(r0, INT); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), INT); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java index f5c2929a6d..d6a5df3ea9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Inverse.java @@ -5,8 +5,6 @@ import java.util.List; -import static com.google.common.base.Preconditions.checkNotNull; - public class Inverse extends Definition { //TODO/Note: We can forward getSMTVar calls // to avoid encoding this completely! @@ -14,10 +12,8 @@ public class Inverse extends Definition { private final Relation r1; public Inverse(Relation r0, Relation r1) { - super(r0, "%s^-1"); - this.r1 = checkNotNull(r1); - r0.checkRelation(); - r1.checkRelation(); + super(Relation.checkIsRelation(r0), "%s^-1"); + this.r1 = Relation.checkIsRelation(r1); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java index 9f6a43b0ed..e9ac3ab275 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LXSXPairs.java @@ -7,8 +7,7 @@ public class LXSXPairs extends Definition { public LXSXPairs(Relation r0) { - super(r0, RelationNameRepository.LXSX); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.LXSX); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java index db2b59f741..6e2882f178 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/LinuxCriticalSections.java @@ -7,8 +7,7 @@ public class LinuxCriticalSections extends Definition { public LinuxCriticalSections(Relation r0) { - super(r0, RelationNameRepository.CRIT); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.CRIT); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java index 10a709e7f3..23e2e012e3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ProgramOrder.java @@ -9,9 +9,8 @@ public class ProgramOrder extends Definition { private final Filter filter; //TODO: Do we ever need a po on other events than all visible one's? public ProgramOrder(Relation r0, Filter s1) { - super(r0, "po(" + s1 + ")"); + super(Relation.checkIsRelation(r0), "po(" + s1 + ")"); filter = s1; - r0.checkRelation(); } public Filter getFilter() { return filter; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java index 0161a08d66..9d018a8c89 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java @@ -5,17 +5,13 @@ import java.util.List; -import static com.google.common.base.Preconditions.checkNotNull; - public class Range extends Definition { private final Relation r1; public Range(Relation r0, Relation r1) { - super(r0, "range(%s)"); - this.r1 = checkNotNull(r1); - r0.checkSet(); - r1.checkRelation(); + super(Relation.checkIsSet(r0), "range(%s)"); + this.r1 = Relation.checkIsRelation(r1); } public Relation getOperand() { return r1; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java index 91dd12ef85..b699676f49 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/ReadFrom.java @@ -7,8 +7,7 @@ public class ReadFrom extends Definition { public ReadFrom(Relation r0) { - super(r0, RelationNameRepository.RF); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.RF); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java index 1a4dc4a190..e8f7180aac 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameLocation.java @@ -7,8 +7,7 @@ public class SameLocation extends Definition { public SameLocation(Relation r0) { - super(r0, RelationNameRepository.LOC); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.LOC); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java index 7c81b44d95..35272e7889 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameScope.java @@ -7,8 +7,7 @@ public class SameScope extends Definition { private final String specificScope; public SameScope(Relation r) { - this(r, null); - r.checkRelation(); + this(Relation.checkIsRelation(r), null); } public SameScope(Relation r, String specificScope) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java index 2d20c080fb..c0921bbcc2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameVirtualLocation.java @@ -7,8 +7,7 @@ public class SameVirtualLocation extends Definition { public SameVirtualLocation(Relation r0) { - super(r0, RelationNameRepository.VLOC); - r0.checkRelation(); + super(Relation.checkIsRelation(r0), RelationNameRepository.VLOC); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java index 4d9e6b12b7..7877511340 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SetIdentity.java @@ -10,10 +10,8 @@ public class SetIdentity extends Definition { private final Relation domain; public SetIdentity(Relation r0, Relation r1) { - super(r0, "[%s]"); - domain = r1; - r0.checkRelation(); - r1.checkSet(); + super(Relation.checkIsRelation(r0), "[%s]"); + domain = Relation.checkIsSet(r1); } public Relation getDomain() { return domain; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java index ea5792436e..4275eaa4bd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java @@ -7,8 +7,7 @@ public class SyncBar extends Definition { public SyncBar(Relation r) { - super(r, RelationNameRepository.SYNCBAR); - r.checkRelation(); + super(Relation.checkIsRelation(r), RelationNameRepository.SYNCBAR); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java index 3d4f91842d..66f402b1ee 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncFence.java @@ -7,8 +7,7 @@ public class SyncFence extends Definition { public SyncFence(Relation r) { - super(r, RelationNameRepository.SYNC_FENCE); - r.checkRelation(); + super(Relation.checkIsRelation(r), RelationNameRepository.SYNC_FENCE); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java index a3c348fceb..f828535a38 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncWith.java @@ -11,8 +11,7 @@ public class SyncWith extends Definition { public SyncWith(Relation r) { - super(r, RelationNameRepository.SSW); - r.checkRelation(); + super(Relation.checkIsRelation(r), RelationNameRepository.SSW); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java index 7426dff918..5d5579f525 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TagSet.java @@ -9,15 +9,12 @@ public class TagSet extends Definition { private final String tag; public TagSet(Relation r, String tag) { - super(r, tag); - this.tag = tag; - r.checkSet(); + this(Relation.checkIsSet(r), tag, tag); } protected TagSet(Relation r, String tag, String termPattern) { super(r, termPattern); this.tag = tag; - r.checkSet(); } public String getTag() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java index 4f7fd915af..d1f1707ec9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/TransitiveClosure.java @@ -5,17 +5,13 @@ import java.util.List; -import static com.google.common.base.Preconditions.checkNotNull; - public class TransitiveClosure extends Definition { private final Relation r1; public TransitiveClosure(Relation r0, Relation r1) { - super(r0, "%s^+"); - this.r1 = checkNotNull(r1); - r0.checkRelation(); - r1.checkRelation(); + super(Relation.checkIsRelation(r0), "%s^+"); + this.r1 = Relation.checkIsRelation(r1); } public Relation getOperand() { return r1; } From f367c6101ba9645cdfd3caa9fe333ece07d6b3c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Wed, 1 Oct 2025 18:45:15 +0200 Subject: [PATCH 11/17] Rename cat built-in 'New()' to 'newSet()'. Rename 'new()' to 'newRelation()'. --- dartagnan/src/main/antlr4/Cat.g4 | 10 ++++++---- .../com/dat3m/dartagnan/parsers/cat/VisitorCat.java | 10 +++++++--- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4 index af1dc930ff..4d3afd0099 100755 --- a/dartagnan/src/main/antlr4/Cat.g4 +++ b/dartagnan/src/main/antlr4/Cat.g4 @@ -53,7 +53,8 @@ expression | (TOID LPAR e = expression RPAR | LBRAC e = expression RBRAC) # exprIdentity | LPAR e = expression RPAR # expr | n = NAME # exprBasic - | call = NEW LPAR RPAR # exprNew + | NEW_SET LPAR RPAR # exprNewSet + | NEW_RELATION LPAR RPAR # exprNewRelation | call = NAME LPAR args = argumentList RPAR # exprCall ; @@ -103,9 +104,10 @@ LBRAC : '['; RBRAC : ']'; COMMA : ','; -DOMAIN : 'domain'; -RANGE : 'range'; -NEW : '[n|N]ew'; +DOMAIN : 'domain'; +RANGE : 'range'; +NEW_SET : 'newSet'; +NEW_RELATION : 'newRelation'; FLAG : 'flag'; UNDEFINED : 'undefined_unless'; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index 60e8f11643..94cf8fa7dc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -203,9 +203,13 @@ public Object visitExpr(ExprContext ctx) { } @Override - public Object visitExprNew(ExprNewContext ctx) { - final boolean unary = ctx.call.getText().equals("New"); - return addDefinition(new Free(wmm.newRelation(unary ? Relation.Arity.UNARY : Relation.Arity.BINARY))); + public Object visitExprNewSet(ExprNewSetContext ctx) { + return addDefinition(new Free(wmm.newRelation(Relation.Arity.UNARY))); + } + + @Override + public Object visitExprNewRelation(ExprNewRelationContext ctx) { + return addDefinition(new Free(wmm.newRelation(Relation.Arity.BINARY))); } @Override From 56dedcde23e7c61e8e5f3150f56b427ca7be7955 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Thu, 2 Oct 2025 10:21:16 +0200 Subject: [PATCH 12/17] Add cat parsing support for recursive sets. --- .../dartagnan/encoding/EncodingContext.java | 1 + .../dartagnan/parsers/cat/VisitorCat.java | 84 +++++++++++++++++-- .../basePredicates/DynamicDefaultWMMSet.java | 2 +- .../dartagnan/parsers/cat/CatParserTest.java | 19 +++++ 4 files changed, 96 insertions(+), 10 deletions(-) create mode 100644 dartagnan/src/test/java/com/dat3m/dartagnan/parsers/cat/CatParserTest.java 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 3056a6a6ba..507d4d5c9a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java @@ -255,6 +255,7 @@ public EdgeEncoder edge(Relation relation) { EventGraph must = k.getMustSet(); EdgeEncoder variable = relation.getDefinition().getEdgeVariableEncoder(this); return (e1, e2) -> { + checkArgument(!relation.isSet() || e1.equals(e2), "Cannot encode pairs of events in an event set"); if (!may.contains(e1, e2)) { return booleanFormulaManager.makeFalse(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index 94cf8fa7dc..ec5755e418 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -157,8 +157,8 @@ public Void visitLetRecDefinition(LetRecDefinitionContext ctx) { final int recSize = ctx.letRecAndDefinition().size() + 1; final Relation[] recursiveGroup = new Relation[recSize]; final String[] lhsNames = new String[recSize]; - - // Create the recursive relations + final ExpressionContext[] rhsContexts = new ExpressionContext[recSize]; + // Recompose the syntax. for (int i = 0; i < recSize; i++) { // First relation needs special treatment due to syntactic difference final String relName = i == 0 ? ctx.n.getText() : ctx.letRecAndDefinition(i - 1).n.getText(); @@ -167,14 +167,18 @@ public Void visitLetRecDefinition(LetRecDefinitionContext ctx) { throw new MalformedMemoryModelException(errorMsg); } lhsNames[i] = relName; - recursiveGroup[i] = wmm.newRelation(createUniqueName(relName)); + rhsContexts[i] = i == 0 ? ctx.e : ctx.letRecAndDefinition(i - 1).e; + } + // Create the recursive relations. + for (int i = 0; i < recSize; i++) { + final Relation.Arity arity = rhsContexts[i].accept(new ArityInspector()); + recursiveGroup[i] = wmm.newRelation(createUniqueName(lhsNames[i]), arity); recursiveGroup[i].setRecursive(); - namespace.put(relName, recursiveGroup[i]); + namespace.put(lhsNames[i], recursiveGroup[i]); } - - // Parse recursive definitions + // Parse recursive definitions. for (int i = 0; i < recSize; i++) { - final ExpressionContext rhs = i == 0 ? ctx.e : ctx.letRecAndDefinition(i - 1).e; + final ExpressionContext rhs = rhsContexts[i]; final Relation lhs = recursiveGroup[i]; setRelationToBeDefined(lhs); final Relation parsedRhs = parseAsRelation(rhs); @@ -326,7 +330,6 @@ public Relation visitExprTransRef(ExprTransRefContext c) { @Override public Relation visitExprDomain(ExprDomainContext c) { - checkNoRecursion(c); Relation r0 = wmm.newSet(); Relation r1 = parseAsRelation(c.e); return addDefinition(new Domain(r0, r1)); @@ -334,7 +337,6 @@ public Relation visitExprDomain(ExprDomainContext c) { @Override public Relation visitExprRange(ExprRangeContext c) { - checkNoRecursion(c); Relation r0 = wmm.newSet(); Relation r1 = parseAsRelation(c.e); return addDefinition(new Range(r0, r1)); @@ -407,5 +409,69 @@ private static CatParser getParser(CharStream input) { parser.addErrorListener(new DiagnosticErrorListener(true)); return parser; } + + private final class ArityInspector extends CatBaseVisitor { + + private ArityInspector() {} + + @Override + public Relation.Arity visitExprBasic(ExprBasicContext c) { + final Object object = namespace.get(c.n.getText()); + return object instanceof Relation r ? r.getArity() : null; + } + + @Override + public Relation.Arity visitExprDomain(ExprDomainContext c) { + return Relation.Arity.UNARY; + } + + @Override + public Relation.Arity visitExprRange(ExprRangeContext c) { + return Relation.Arity.UNARY; + } + + @Override + public Relation.Arity visitExprCartesian(ExprCartesianContext c) { + return Relation.Arity.BINARY; + } + + @Override + public Relation.Arity visitExprComposition(ExprCompositionContext c) { + return Relation.Arity.BINARY; + } + + @Override + public Relation.Arity visitExprIdentity(ExprIdentityContext c) { + return Relation.Arity.BINARY; + } + + @Override + public Relation.Arity visitExprUnion(ExprUnionContext c) { + return join(c.e1, c.e2); + } + + @Override + public Relation.Arity visitExprIntersection(ExprIntersectionContext c) { + return join(c.e1, c.e2); + } + + @Override + public Relation.Arity visitExprMinus(ExprMinusContext c) { + return join(c.e1, c.e2); + } + + private Relation.Arity join(ExpressionContext e1, ExpressionContext e2) { + final Relation.Arity k1 = e1.accept(this); + final Relation.Arity k2 = e2.accept(this); + checkCompatible(k1, k2); + return k1 == null ? k2 : k1; + } + + private static void checkCompatible(Relation.Arity k1, Relation.Arity k2) { + if (k1 != null && k2 != null && !k1.equals(k2)) { + throw new ParsingException("Incompatible kinds %s and %s".formatted(k1, k2)); + } + } + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java index 6a288c9282..71b5ebd682 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/DynamicDefaultWMMSet.java @@ -7,7 +7,7 @@ import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; -// A default implementation for any encoded relation, e.g. base relations or non-base but cut relations. +// A default implementation for any encoded set, e.g. base sets or non-base but cut sets. public class DynamicDefaultWMMSet extends MaterializedWMMSet { private final Relation relation; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/cat/CatParserTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/cat/CatParserTest.java new file mode 100644 index 0000000000..c99dd7d19f --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/cat/CatParserTest.java @@ -0,0 +1,19 @@ +package com.dat3m.dartagnan.parsers.cat; + +import com.dat3m.dartagnan.wmm.Wmm; +import org.junit.Test; + +import static org.junit.Assert.assertTrue; + +public class CatParserTest { + + @Test + public void recursiveSet() { + final String text = """ + let rec r0 = domain(loc & ([W]; po; [F]; po; [R])) | domain([r0]; addr) + acyclic (po & loc) | addr | data | ctrl | rf | co | fr | po ; [r0] + """; + final Wmm memoryModel = new ParserCat().parse(text); + assertTrue(memoryModel.getRelation("r0").isRecursive()); + } +} From 0c01bc92fd696ad4ef5d812a9411004e39fe3893 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Thu, 2 Oct 2025 14:13:45 +0200 Subject: [PATCH 13/17] fixup! Merge remote-tracking branch 'origin/development' into wmm-unary-predicates --- .../src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java | 2 ++ 1 file changed, 2 insertions(+) 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 e329e0f3ac..b8d2de92eb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -19,6 +19,7 @@ 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.definition.TagSet; import com.dat3m.dartagnan.wmm.utils.Flag; import com.dat3m.dartagnan.wmm.utils.graph.EventGraph; import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph; @@ -235,6 +236,7 @@ private final class RelationEncoder implements Constraint.Visitor { SyncWith.class, SameVirtualLocation.class, // FIXME?! Empty.class, + TagSet.class, // Static because the underlying sets are static: SetIdentity.class, CartesianProduct.class From d1b33c1b99c8b9726f88b0833f31d1b75d0ab4b6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Thu, 2 Oct 2025 15:26:09 +0200 Subject: [PATCH 14/17] fixup! Add cat parsing support for recursive sets. --- .../java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index ec5755e418..b9d1f6d5ea 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -171,7 +171,8 @@ public Void visitLetRecDefinition(LetRecDefinitionContext ctx) { } // Create the recursive relations. for (int i = 0; i < recSize; i++) { - final Relation.Arity arity = rhsContexts[i].accept(new ArityInspector()); + final Relation.Arity probedArity = rhsContexts[i].accept(new ArityInspector()); + final Relation.Arity arity = probedArity != null ? probedArity : Relation.Arity.BINARY; recursiveGroup[i] = wmm.newRelation(createUniqueName(lhsNames[i]), arity); recursiveGroup[i].setRecursive(); namespace.put(lhsNames[i], recursiveGroup[i]); @@ -414,6 +415,11 @@ private final class ArityInspector extends CatBaseVisitor { private ArityInspector() {} + @Override + public Relation.Arity visitExpr(ExprContext c) { + return c.e.accept(this); + } + @Override public Relation.Arity visitExprBasic(ExprBasicContext c) { final Object object = namespace.get(c.n.getText()); From d84adcad27ae03ded38d9f236c129c63a1e62307 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Thu, 2 Oct 2025 16:21:36 +0200 Subject: [PATCH 15/17] fixup! Merge remote-tracking branch 'origin/development' into wmm-unary-predicates --- .../main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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 b8d2de92eb..424a5568cb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -236,10 +236,7 @@ private final class RelationEncoder implements Constraint.Visitor { SyncWith.class, SameVirtualLocation.class, // FIXME?! Empty.class, - TagSet.class, - // Static because the underlying sets are static: - SetIdentity.class, - CartesianProduct.class + TagSet.class )); final Program program = context.getTask().getProgram(); From 713aa129121d4b5e6fbf20e2c3811c28a78c4613 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 10 Oct 2025 19:09:09 +0200 Subject: [PATCH 16/17] Merge Domain with Range into Projection --- .../dat3m/dartagnan/encoding/EncodeSets.java | 41 +++++++----------- .../dartagnan/encoding/LazyEncodeSets.java | 31 +++++--------- .../dat3m/dartagnan/encoding/WmmEncoder.java | 42 ++++++------------- .../dartagnan/parsers/cat/VisitorCat.java | 4 +- .../solver/caat4wmm/ExecutionGraph.java | 9 ++-- .../model/ExecutionModelManager.java | 18 +++----- .../solving/RefinementSolver.java | 2 +- .../com/dat3m/dartagnan/wmm/Constraint.java | 3 +- .../wmm/analysis/LazyRelationAnalysis.java | 41 +++++++----------- .../wmm/analysis/NativeRelationAnalysis.java | 32 ++++---------- .../{Domain.java => Projection.java} | 15 +++++-- .../dat3m/dartagnan/wmm/definition/Range.java | 28 ------------- .../dartagnan/wmm/utils/ConstraintCopier.java | 9 +--- 13 files changed, 90 insertions(+), 185 deletions(-) rename dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/{Domain.java => Projection.java} (51%) delete mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java 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 4ff257ba8b..216f8e61be 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java @@ -84,33 +84,22 @@ public Map visitComposition(Composition comp) { } @Override - public Map visitDomain(Domain domId) { - final RelationAnalysis.Knowledge k1 = ra.getKnowledge(domId.getOperand()); - Map> out = k1.getMaySet().getOutMap(); - MutableEventGraph result = new MapEventGraph(); - news.apply((e1, e2) -> - out.getOrDefault(e1, Set.of()).forEach(e -> { - if (!k1.getMustSet().contains(e1, e)) { - result.add(e1, e); - } - }) - ); - return Map.of(domId.getOperand(), result); - } - - @Override - public Map visitRange(Range rangeId) { - final RelationAnalysis.Knowledge k1 = ra.getKnowledge(rangeId.getOperand()); - Map> in = k1.getMaySet().getInMap(); - MutableEventGraph result = new MapEventGraph(); - news.apply((e1, e2) -> - in.getOrDefault(e2, Set.of()).forEach(e -> { - if (!k1.getMustSet().contains(e, e2)) { - result.add(e, e2); + public Map visitProjection(Projection projection) { + final MutableEventGraph result = new MapEventGraph(); + final RelationAnalysis.Knowledge k1 = ra.getKnowledge(projection.getOperand()); + final EventGraph mayGraph = k1.getMaySet(); + final EventGraph mustGraph = k1.getMustSet(); + final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN; + final Map> altMap = dom ? mayGraph.getOutMap() : mayGraph.getInMap(); + news.apply((e1, e2) -> { + assert e1.equals(e2); + for (Event alt : altMap.getOrDefault(e1, Set.of())) { + if (!mustGraph.contains(dom ? e1 : alt, dom ? alt : e1)) { + result.add(dom ? e1 : alt, dom ? alt : e1); } - }) - ); - return Map.of(rangeId.getOperand(), result); + } + }); + return Map.of(projection.getOperand(), result); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java index 0d0f8f503e..c99c284f6d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/LazyEncodeSets.java @@ -174,27 +174,18 @@ public Boolean visitSetIdentity(SetIdentity definition) { } @Override - public Boolean visitDomain(Domain definition) { + public Boolean visitProjection(Projection 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 visitRange(Range 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))); + final long start = System.currentTimeMillis(); + final MutableEventGraph operandUpdate = new MapEventGraph(); + final boolean dom = definition.getDimension() == Projection.Dimension.DOMAIN; + final EventGraph maySet = ra.getKnowledge(definition.getOperand()).getMaySet(); + final Map> altMap = dom ? maySet.getOutMap() : maySet.getInMap(); + if (dom) { + update.getDomain().forEach(e1 -> operandUpdate.addRange(e1, altMap.get(e1))); + } else { + update.getDomain().forEach(e2 -> altMap.get(e2).forEach(e1 -> operandUpdate.add(e1, e2))); + } setUpdate(operandUpdate); operandTime(definition, start, System.currentTimeMillis()); definition.getOperand().getDefinition().accept(this); 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 424a5568cb..afb6354a98 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -377,37 +377,21 @@ public Void visitComposition(Composition comp) { } @Override - public Void visitDomain(Domain domId) { - final Relation rel = domId.getDefinedRelation(); - final Relation r1 = domId.getOperand(); - Map> mayOut = ra.getKnowledge(r1).getMaySet().getOutMap(); - EncodingContext.EdgeEncoder enc0 = context.edge(rel); - EncodingContext.EdgeEncoder enc1 = context.edge(r1); - encodeSets.get(rel).apply((e1, e2) -> { - BooleanFormula opt = bmgr.makeFalse(); - //TODO: Optimize using minSets (but no CAT uses this anyway) - for (Event e2Alt : mayOut.getOrDefault(e1, Set.of())) { - opt = bmgr.or(opt, enc1.encode(e1, e2Alt)); - } - enc.add(bmgr.equivalence(enc0.encode(e1, e2), opt)); - }); - return null; - } - - @Override - public Void visitRange(Range rangeId) { - final Relation rel = rangeId.getDefinedRelation(); - final Relation r1 = rangeId.getOperand(); - Map> mayIn = ra.getKnowledge(r1).getMaySet().getInMap(); - EncodingContext.EdgeEncoder enc0 = context.edge(rel); - EncodingContext.EdgeEncoder enc1 = context.edge(r1); - //TODO: Optimize using minSets (but no CAT uses this anyway) + public Void visitProjection(Projection projection) { + final Relation rel = projection.getDefinedRelation(); + final Relation r1 = projection.getOperand(); + final EncodingContext.EdgeEncoder enc0 = context.edge(rel); + final EncodingContext.EdgeEncoder enc1 = context.edge(r1); + final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN; + final EventGraph may1 = ra.getKnowledge(r1).getMaySet(); + final Map> altMap = dom ? may1.getOutMap() : may1.getInMap(); encodeSets.get(rel).apply((e1, e2) -> { - BooleanFormula opt = bmgr.makeFalse(); - for (Event e1Alt : mayIn.getOrDefault(e1, Set.of())) { - opt = bmgr.or(opt, enc1.encode(e1Alt, e2)); + assert e1.equals(e2); + final var opt = new ArrayList(); + for (Event alt : altMap.getOrDefault(e1, Set.of())) { + opt.add(enc1.encode(dom ? e1 : alt, dom ? alt : e1)); } - enc.add(bmgr.equivalence(enc0.encode(e1, e2), opt)); + enc.add(bmgr.equivalence(enc0.encode(e1, e1), bmgr.or(opt))); }); return null; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index b9d1f6d5ea..5c99029a99 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -333,14 +333,14 @@ public Relation visitExprTransRef(ExprTransRefContext c) { public Relation visitExprDomain(ExprDomainContext c) { Relation r0 = wmm.newSet(); Relation r1 = parseAsRelation(c.e); - return addDefinition(new Domain(r0, r1)); + return addDefinition(new Projection(r0, r1, Projection.Dimension.DOMAIN)); } @Override public Relation visitExprRange(ExprRangeContext c) { Relation r0 = wmm.newSet(); Relation r1 = parseAsRelation(c.e); - return addDefinition(new Range(r0, r1)); + return addDefinition(new Projection(r0, r1, Projection.Dimension.RANGE)); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index 660469b01f..bf4f6002ca 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -281,11 +281,10 @@ private SetPredicate getOrCreateSetFromRelation(Relation relation) { set = new DynamicDefaultWMMSet(refinementModel.translateToBase(relation)); } else if (relClass == TagSet.class) { set = new StaticWMMSet(((TagSet) relation.getDefinition()).getTag()); - } else if (relClass == Range.class || relClass == Domain.class) { - RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0)); - ProjectionSet.Dimension dim = relClass == Range.class ? - ProjectionSet.Dimension.RANGE : - ProjectionSet.Dimension.DOMAIN; + } else if (relClass == Projection.class) { + final RelationGraph g = getOrCreateGraphFromRelation(dependencies.get(0)); + final boolean dom = ((Projection) relation.getDefinition()).getDimension() == Projection.Dimension.DOMAIN; + final ProjectionSet.Dimension dim = dom ? ProjectionSet.Dimension.DOMAIN : ProjectionSet.Dimension.RANGE; set = new ProjectionSet(g, dim); } else if (relClass == Union.class || relClass == Intersection.class) { SetPredicate[] graphs = new SetPredicate[dependencies.size()]; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java index da43e51d30..8e144bdfa0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -550,19 +550,11 @@ public SetPredicate visitIntersection(Intersection inter) { } @Override - public SetPredicate visitRange(Range range) { - return new ProjectionSet( - getOrCreateGraph(range.getOperand()), - ProjectionSet.Dimension.RANGE - ); - } - - @Override - public SetPredicate visitDomain(Domain domain) { - return new ProjectionSet( - getOrCreateGraph(domain.getOperand()), - ProjectionSet.Dimension.DOMAIN - ); + public SetPredicate visitProjection(Projection projection) { + final RelationGraph graph = getOrCreateGraph(projection.getOperand()); + final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN; + final ProjectionSet.Dimension dim = dom ? ProjectionSet.Dimension.DOMAIN : ProjectionSet.Dimension.RANGE; + return new ProjectionSet(graph, dim); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 9bc6dcb9f3..a38d25053b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -570,7 +570,7 @@ private static void addBiases(Wmm wmm, EnumSet biases) { // [R \ range(rf)];loc;[W] final Relation reads = wmm.addDefinition(new TagSet(wmm.newSet(), Tag.READ)); - final Relation rfRange = wmm.addDefinition(new Range(wmm.newSet(), rf)); + final Relation rfRange = wmm.addDefinition(new Projection(wmm.newSet(), rf, Projection.Dimension.RANGE)); final Relation writes = wmm.addDefinition(new TagSet(wmm.newSet(), Tag.WRITE)); final Relation writesSet = wmm.addDefinition(new SetIdentity(wmm.newRelation(), writes)); final Relation ur = wmm.addDefinition(new Difference(wmm.newSet(), reads, rfRange)); 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 1830463918..6e9c386791 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -63,8 +63,7 @@ default T visitConstraint(Constraint constraint) { default T visitIntersection(Intersection def) { return visitDefinition(def); } default T visitDifference(Difference def) { return visitDefinition(def); } default T visitComposition(Composition def) { return visitDefinition(def); } - default T visitDomain(Domain def) { return visitDefinition(def); } - default T visitRange(Range def) { return visitDefinition(def); } + default T visitProjection(Projection def) { return visitDefinition(def); } default T visitInverse(Inverse def) { return visitDefinition(def); } default T visitTransitiveClosure(TransitiveClosure def) { return visitDefinition(def); } // These three are semi-derived (they are derived from sets/filters and not from relations). 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 index 07f839f0f1..0228145b33 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java @@ -23,6 +23,7 @@ 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.Maps; import com.google.common.collect.Sets; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -470,31 +471,21 @@ public RelationAnalysis.Knowledge visitSyncWith(SyncWith definition) { } @Override - public RelationAnalysis.Knowledge visitDomain(Domain 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 visitRange(Range 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); + public RelationAnalysis.Knowledge visitProjection(Projection definition) { + final RelationAnalysis.Knowledge knowledge = getKnowledge(definition.getOperand()); + final EventGraph mayGraph = knowledge.getMaySet(); + final EventGraph mustGraph = knowledge.getMustSet(); + final boolean dom = definition.getDimension() == Projection.Dimension.DOMAIN; + final long start = System.currentTimeMillis(); + final Set maySet = dom ? mayGraph.getDomain() : mayGraph.getRange(); + final Set mustSet = new HashSet<>(); + mustGraph.apply((e1, e2) -> { + if (exec.isImplied(dom ? e1 : e2, dom ? e2 : e1)) { + mustSet.add(dom ? e1 : e2); + } + }); + final EventGraph may = new ImmutableMapEventGraph(Maps.asMap(maySet, Set::of)); + final EventGraph must = new ImmutableMapEventGraph(Maps.asMap(mustSet, Set::of)); time(definition, start, System.currentTimeMillis()); return new RelationAnalysis.Knowledge(may, must); } 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 080cb292eb..a1be711440 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 @@ -1635,30 +1635,16 @@ private void computeComposition(MutableEventGraph result, EventGraph left, Event } @Override - public Delta visitDomain(Domain domId) { - if (domId.getOperand().equals(source)) { - MutableEventGraph maySet = new MapEventGraph(); - may.getDomain().forEach(e -> maySet.add(e, e)); - MutableEventGraph mustSet = new MapEventGraph(); + public Delta visitProjection(Projection projection) { + if (projection.getOperand().equals(source)) { + final boolean dom = projection.getDimension() == Projection.Dimension.DOMAIN; + final MutableEventGraph maySet = new MapEventGraph(); + (dom ? may.getDomain() : may.getRange()).forEach(e -> maySet.add(e, e)); + final MutableEventGraph mustSet = new MapEventGraph(); must.apply((e1, e2) -> { - if (exec.isImplied(e1, e2)) { - mustSet.add(e1, e1); - } - }); - return new Delta(maySet, mustSet); - } - return Delta.EMPTY; - } - - @Override - public Delta visitRange(Range rangeId) { - if (rangeId.getOperand().equals(source)) { - MutableEventGraph maySet = new MapEventGraph(); - may.getRange().forEach(e -> maySet.add(e, e)); - MutableEventGraph mustSet = new MapEventGraph(); - must.apply((e1, e2) -> { - if (exec.isImplied(e2, e1)) { - mustSet.add(e2, e2); + final Event e = dom ? e1 : e2; + if (exec.isImplied(e, dom ? e2 : e1)) { + mustSet.add(e, e); } }); return new Delta(maySet, mustSet); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Projection.java similarity index 51% rename from dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Projection.java index 36192d88b1..bff2d213b0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Domain.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Projection.java @@ -5,17 +5,24 @@ import java.util.List; -public class Domain extends Definition { +public class Projection extends Definition { private final Relation r1; - public Domain(Relation r0, Relation r1) { - super(Relation.checkIsSet(r0), "domain(%s)"); + private final Dimension dimension; + + public enum Dimension { DOMAIN, RANGE } + + public Projection(Relation r0, Relation r1, Dimension dimension) { + super(Relation.checkIsSet(r0), switch (dimension) { case DOMAIN -> "domain(%s)"; case RANGE -> "range(%s)"; }); this.r1 = Relation.checkIsRelation(r1); + this.dimension = dimension; } public Relation getOperand() { return r1; } + public Dimension getDimension() { return dimension; } + @Override public List getConstrainedRelations() { return List.of(definedRelation, r1); @@ -23,6 +30,6 @@ public List getConstrainedRelations() { @Override public T accept(Visitor v) { - return v.visitDomain(this); + return v.visitProjection(this); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java deleted file mode 100644 index 9d018a8c89..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Range.java +++ /dev/null @@ -1,28 +0,0 @@ -package com.dat3m.dartagnan.wmm.definition; - -import com.dat3m.dartagnan.wmm.Definition; -import com.dat3m.dartagnan.wmm.Relation; - -import java.util.List; - -public class Range extends Definition { - - private final Relation r1; - - public Range(Relation r0, Relation r1) { - super(Relation.checkIsSet(r0), "range(%s)"); - this.r1 = Relation.checkIsRelation(r1); - } - - public Relation getOperand() { return r1; } - - @Override - public List getConstrainedRelations() { - return List.of(definedRelation, r1); - } - - @Override - public T accept(Visitor v) { - return v.visitRange(this); - } -} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java index 976a0efbba..c2e5a2ff91 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java @@ -92,13 +92,8 @@ public Composition visitComposition(Composition def) { } @Override - public Domain visitDomain(Domain def) { - return new Domain(translate(def.getDefinedRelation()), translate(def.getOperand())); - } - - @Override - public Range visitRange(Range def) { - return new Range(translate(def.getDefinedRelation()), translate(def.getOperand())); + public Projection visitProjection(Projection def) { + return new Projection(translate(def.getDefinedRelation()), translate(def.getOperand()), def.getDimension()); } @Override From f35a515e0261b800e48a0e2fa00273198120e640 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ren=C3=A9=20Pascal=20Maseli?= Date: Fri, 10 Oct 2025 19:22:22 +0200 Subject: [PATCH 17/17] UnsupportedOperationException, if RefinementSolver is invoked with a memory model with a recursive set --- .../com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index bf4f6002ca..e95bf46ba1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -92,6 +92,9 @@ private void constructMappings() { for (DependencyGraph.Node node : component) { Relation relation = node.getContent(); if (relation.isRecursive()) { + if (relation.isSet()) { + throw new UnsupportedOperationException("No support for recursive sets"); + } RecursiveGraph graph = new RecursiveGraph(); graph.setName(relation.getNameOrTerm() + "_rec"); graphs.add(graph);