Skip to content

Commit

Permalink
Cleanup VisitorXML (#598)
Browse files Browse the repository at this point in the history 
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>
  • Loading branch information
@hernanponcedeleon @hernan-poncedeleon @ThomasHaas
3 people authored Jan 3, 2024
1 parent 3577e0e commit c1371f9
Show file tree
Hide file tree
Showing 2 changed files with 47 additions and 52 deletions.
86 changes: 39 additions & 47 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/witness/visitors/VisitorXML.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 +5,17 @@
import com.dat3m.dartagnan.parsers.XMLParser.ElementContext;
import com.dat3m.dartagnan.parsers.XMLParserBaseVisitor;
import com.dat3m.dartagnan.witness.Edge;
import com.dat3m.dartagnan.witness.ElemWithAttributes;
import com.dat3m.dartagnan.witness.Node;
import com.dat3m.dartagnan.witness.WitnessGraph;

import static com.dat3m.dartagnan.witness.GraphAttributes.*;
import static com.dat3m.dartagnan.witness.NodeAttributes.*;

import java.util.stream.Collectors;
import static com.dat3m.dartagnan.witness.GraphAttributes.PRODUCER;
import static com.dat3m.dartagnan.witness.GraphAttributes.WITNESSTYPE;

public class VisitorXML extends XMLParserBaseVisitor<Object> {

private final WitnessGraph graph = new WitnessGraph();
private String lastAddedNodeId;
private ElemWithAttributes current = graph;

@Override
public WitnessGraph visitDocument(XMLParser.DocumentContext ctx) {
Expand All @@ -29,52 +28,45 @@ public WitnessGraph visitDocument(XMLParser.DocumentContext ctx) {

@Override
public Object visitElement(XMLParser.ElementContext ctx) {
if (ctx.content() != null) {
if (ctx.Name(0).getText().equals("data")) {
if (ctx.content() != null) {
String key = ctx.attribute(0).STRING().getText();
key = key.substring(1, key.length() - 1);
String value = ctx.content().getText();
if (key.equals(PROGRAMFILE.toString()) || key.equals(PRODUCER.toString())
|| key.equals(UNROLLBOUND.toString())) {
graph.addAttribute(key, value);
}
if (key.equals(WITNESSTYPE.toString()) && !value.equals("violation_witness")) {
throw new ParsingException("Dartagnan can only validate violation witnesses");
}
if (key.equals(ENTRY.toString()) || key.equals(VIOLATION.toString())) {
graph.getNode(lastAddedNodeId).addAttribute(key, value);
}
final String elementType = ctx.Name(0).getText();
return switch (elementType) {
case "data" -> {
final String key = getAttributeString(ctx, 0);
final String value = ctx.content().getText();
if (key.equals(WITNESSTYPE.toString()) && !value.equals("violation_witness")) {
throw new ParsingException("Dartagnan can only validate violation witnesses");
}
current.addAttribute(key, value);
yield null;
}
if (ctx.Name(0).getText().equals("node")) {
String name = ctx.attribute(0).STRING().toString();
lastAddedNodeId = name.substring(1, name.length() - 1);
graph.addNode(lastAddedNodeId);
case "node" -> {
final String name = getAttributeString(ctx, 0);
graph.addNode(name);
current = graph.getNode(name);
visitChildren(ctx);
current = graph;
yield null;
}
if (ctx.Name(0).getText().equals("edge")) {
int idx = ctx.attribute().stream().map(a -> a.Name().toString()).collect(Collectors.toList())
.indexOf("source");
String name = ctx.attribute(idx).STRING().toString();
name = name.substring(1, name.length() - 1);
Node v0 = graph.hasNode(name) ? graph.getNode(name) : new Node(name);
idx = ctx.attribute().stream().map(a -> a.Name().toString()).collect(Collectors.toList())
.indexOf("target");
name = ctx.attribute(idx).STRING().toString();
name = name.substring(1, name.length() - 1);
Node v1 = graph.hasNode(name) ? graph.getNode(name) : new Node(name);
Edge edge = new Edge(v0, v1);
if (ctx.content() != null) {
for (ElementContext elem : ctx.content().element()) {
String key = elem.attribute(0).STRING().getText();
key = key.substring(1, key.length() - 1);
String value = elem.content().getText();
edge.addAttribute(key, value);
}
}
case "edge" -> {
final Edge edge = new Edge(getNode(ctx, "source"), getNode(ctx, "target"));
graph.addEdge(edge);
current = edge;
visitChildren(ctx);
current = graph;
yield null;
}
}
return visitChildren(ctx);
default -> visitChildren(ctx);
};
}

private Node getNode(ElementContext ctx, String vertex) {
final int idx = ctx.attribute().stream().map(a -> a.Name().toString()).toList().indexOf(vertex);
final String name = getAttributeString(ctx, idx);
return graph.hasNode(name) ? graph.getNode(name) : new Node(name);
}

private String getAttributeString(ElementContext ctx, int index) {
final String attributeStr = ctx.attribute(index).STRING().toString();
return attributeStr.substring(1, attributeStr.length() - 1);
}
}
13 changes: 8 additions & 5 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessGraph.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,18 @@
import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
import com.dat3m.dartagnan.wmm.utils.EventGraph;
import com.google.common.collect.Lists;
import org.sosy_lab.java_smt.api.*;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.BooleanFormulaManager;

import java.io.FileWriter;
import java.io.IOException;
import java.util.*;

import static com.dat3m.dartagnan.GlobalSettings.getOrCreateOutputDirectory;
import static com.dat3m.dartagnan.witness.GraphAttributes.*;
import static com.dat3m.dartagnan.witness.NodeAttributes.*;
import static com.dat3m.dartagnan.witness.GraphAttributes.PRODUCER;
import static com.dat3m.dartagnan.witness.GraphAttributes.PROGRAMFILE;
import static com.dat3m.dartagnan.witness.NodeAttributes.ENTRY;
import static com.dat3m.dartagnan.witness.NodeAttributes.VIOLATION;

public class WitnessGraph extends ElemWithAttributes {

Expand Down Expand Up @@ -140,9 +143,9 @@ public EventGraph getReadFromKnowledge(Program program, AliasAnalysis alias) {
current = currents.size() == 1 ? currents.get(0) : null;
// If a graph edge implies a hb-relation, inter-thread communication guarantees
// same address and thus rf.
if (last != null && current != null && last instanceof Store && current instanceof Load
if (last instanceof Store && current instanceof Load
&& ((graphEdgeImpliesHbEdge() && !last.getThread().equals(current.getThread()))
|| alias.mustAlias(last, current))) {
|| alias.mustAlias(last, current))) {
k.add(last, current);
}
last = current;
Expand Down

0 comments on commit c1371f9

Please sign in to comment.