Skip to content

Commit

Permalink
Fix recursion in the name visitor
Browse files Browse the repository at this point in the history
  • Loading branch information
Dmitry Ivanov committed Aug 13, 2024
1 parent bfb98eb commit 4272c85
Showing 1 changed file with 36 additions and 42 deletions.
78 changes: 36 additions & 42 deletions dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/DatalogRelationAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -378,10 +378,8 @@ private String getRelationDatalogName(Relation r) {
}

public String getRelationDatalogName(Relation r, boolean full) {
//String name = relationToDatalogName.computeIfAbsent(r, k -> sanitize(r.getName()
// .filter(n -> n.matches("[A-Za-z0-9\\-_.]+"))
// .orElseGet(() -> { logger.info("getting name for " + r.getName()); return r.getDefinition().accept(new DatalogNameVisitor(r)).toString(); })));
return "rel" + System.identityHashCode(r);
String name = relationToDatalogName.computeIfAbsent(r, k -> r.getDefinition().accept(new DatalogNameVisitor()).toString());
return full ? name : "rel" + System.identityHashCode(name);
}

private String getFilterDatalogName(Filter f) {
Expand Down Expand Up @@ -557,67 +555,63 @@ private String sanitize(String s) {
private class DatalogNameVisitor implements Definition.Visitor<StringBuilder>, Filter.Visitor<StringBuilder> {

private final StringBuilder name = new StringBuilder();
private final Object target;
private boolean recursive = false;
private String recursiveName = null;

public DatalogNameVisitor(Filter filter) {
target = filter;
}

public DatalogNameVisitor(Relation relation) {
target = relation;
}
private final Map<Object, Integer> termToOffset = new HashMap<>();
private final Map<Object, String> termToName = new HashMap<>();
private int recursiveCount = 0;

private boolean checkRecursion(Object target) {
if (!Objects.equals(this.target, target)) {
return false;
}
if (!recursive) {
recursive = true;
Integer offset = termToOffset.get(target);
if (offset == null) {
termToOffset.put(target, name.length());
return false;
}
if (recursiveName == null) {
recursiveName = "name" + System.identityHashCode(this.target);
name.insert(0, "recursive_" + recursiveName);
}
String recursiveName = termToName.computeIfAbsent(target, k -> {
String result = "name" + recursiveCount++;
String prefix = String.format("recursive_%s_", result);
name.insert(offset, prefix);
int prefixLength = prefix.length();
termToOffset.entrySet().stream().filter(e -> e.getValue() > offset)
.forEach(e -> termToOffset.put(e.getKey(), e.getValue() + prefixLength));
return result;
});
name.append(recursiveName);
return true;
}

@Override
public StringBuilder visitUnion(Union def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
verify(!def.getOperands().isEmpty());
name.append("union_".repeat(def.getOperands().size() - 1));
name.setLength(name.length() - 1);
def.getOperands().forEach(r -> {
def.getOperands().stream().map(Relation::getDefinition).forEachOrdered(d -> {
name.append("_");
name.append(getRelationDatalogName(r));
d.accept(this);
});
return name;
}

@Override
public StringBuilder visitIntersection(Intersection def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
verify(!def.getOperands().isEmpty());
name.append("intersection_".repeat(def.getOperands().size() - 1));
name.setLength(name.length() - 1);
def.getOperands().forEach(r -> {
def.getOperands().stream().map(Relation::getDefinition).forEachOrdered(d -> {
name.append("_");
name.append(getRelationDatalogName(r));
d.accept(this);
});
return name;
}

@Override
public StringBuilder visitDifference(Difference def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("difference");
Stream.of(def.getMinuend(), def.getSubtrahend()).map(Relation::getDefinition).forEachOrdered(d -> {
Expand All @@ -630,7 +624,7 @@ public StringBuilder visitDifference(Difference def) {
@Override
public StringBuilder visitComposition(Composition def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("composition");
Stream.of(def.getLeftOperand(), def.getRightOperand()).map(Relation::getDefinition).forEachOrdered(d -> {
Expand All @@ -643,7 +637,7 @@ public StringBuilder visitComposition(Composition def) {
@Override
public StringBuilder visitDomainIdentity(DomainIdentity def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("domain_");
return def.getOperand().getDefinition().accept(this);
Expand All @@ -652,7 +646,7 @@ public StringBuilder visitDomainIdentity(DomainIdentity def) {
@Override
public StringBuilder visitRangeIdentity(RangeIdentity def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("identity_range_");
return def.getOperand().getDefinition().accept(this);
Expand All @@ -661,7 +655,7 @@ public StringBuilder visitRangeIdentity(RangeIdentity def) {
@Override
public StringBuilder visitInverse(Inverse def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("inverse_");
return def.getOperand().getDefinition().accept(this);
Expand All @@ -670,7 +664,7 @@ public StringBuilder visitInverse(Inverse def) {
@Override
public StringBuilder visitTransitiveClosure(TransitiveClosure def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("closure_");
return def.getOperand().getDefinition().accept(this);
Expand All @@ -679,7 +673,7 @@ public StringBuilder visitTransitiveClosure(TransitiveClosure def) {
@Override
public StringBuilder visitSetIdentity(SetIdentity def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("identity_");
return def.getFilter().accept(this);
Expand All @@ -688,7 +682,7 @@ public StringBuilder visitSetIdentity(SetIdentity def) {
@Override
public StringBuilder visitProduct(CartesianProduct def) {
if (checkRecursion(def.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("product_");
def.getFirstFilter().accept(this);
Expand All @@ -699,7 +693,7 @@ public StringBuilder visitProduct(CartesianProduct def) {
@Override
public StringBuilder visitFences(Fences fence) {
if (checkRecursion(fence.getDefinedRelation())) {
return name.append(recursiveName);
return name;
}
name.append("fence_");
return fence.getFilter().accept(this);
Expand Down Expand Up @@ -808,7 +802,7 @@ public StringBuilder visitTagFilter(TagFilter tagFilter) {
@Override
public StringBuilder visitIntersectionFilter(IntersectionFilter intersectionFilter) {
if (checkRecursion(intersectionFilter)) {
return name.append(recursiveName);
return name;
}
name.append("intersection");
Stream.of(intersectionFilter.getLeft(), intersectionFilter.getRight()).forEachOrdered(f -> {
Expand All @@ -821,7 +815,7 @@ public StringBuilder visitIntersectionFilter(IntersectionFilter intersectionFilt
@Override
public StringBuilder visitDifferenceFilter(DifferenceFilter differenceFilter) {
if (checkRecursion(differenceFilter)) {
return name.append(recursiveName);
return name;
}
name.append("difference");
Stream.of(differenceFilter.getLeft(), differenceFilter.getRight()).forEachOrdered(f -> {
Expand All @@ -834,7 +828,7 @@ public StringBuilder visitDifferenceFilter(DifferenceFilter differenceFilter) {
@Override
public StringBuilder visitUnionFilter(UnionFilter unionFilter) {
if (checkRecursion(unionFilter)) {
return name.append(recursiveName);
return name;
}
name.append("union");
Stream.of(unionFilter.getLeft(), unionFilter.getRight()).forEachOrdered(f -> {
Expand Down

0 comments on commit 4272c85

Please sign in to comment.