Skip to content

Commit

Permalink
Generate knowledge from SVCOMP witness (#597)
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]>
  • Loading branch information
@hernanponcedeleon @hernan-poncedeleon
hernanponcedeleon and hernan-poncedeleon authored Jan 2, 2024
1 parent 024bd43 commit 3577e0e
Show file tree
Hide file tree
Showing 5 changed files with 262 additions and 225 deletions.
124 changes: 63 additions & 61 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 @@ -9,70 +9,72 @@
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;

public class VisitorXML extends XMLParserBaseVisitor<Object> {

private final WitnessGraph graph = new WitnessGraph();

@Override
public WitnessGraph visitDocument(XMLParser.DocumentContext ctx) {
visitChildren(ctx);
if(!graph.hasAttributed(PRODUCER.toString())) {
throw new ParsingException("The witness does not have a producer tag");
}
return graph;
}

@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())) {
graph.addAttribute(key, value);
}
if(key.equals(PRODUCER.toString())) {
graph.addAttribute(key, value);
}
if(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(ctx.Name(0).getText().equals("node")) {
String name = ctx.attribute(0).STRING().toString();
name = name.substring(1, name.length()-1);
graph.addNode(name);
}
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);
}
}
graph.addEdge(edge);
}
}
return visitChildren(ctx);
}
private final WitnessGraph graph = new WitnessGraph();
private String lastAddedNodeId;

@Override
public WitnessGraph visitDocument(XMLParser.DocumentContext ctx) {
visitChildren(ctx);
if (!graph.hasAttributed(PRODUCER.toString())) {
throw new ParsingException("The witness does not have a producer tag");
}
return graph;
}

@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);
}
}
}
if (ctx.Name(0).getText().equals("node")) {
String name = ctx.attribute(0).STRING().toString();
lastAddedNodeId = name.substring(1, name.length() - 1);
graph.addNode(lastAddedNodeId);
}
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);
}
}
graph.addEdge(edge);
}
}
return visitChildren(ctx);
}
}
10 changes: 1 addition & 9 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/EdgeAttributes.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,7 @@

public enum EdgeAttributes {

CREATETHREAD, THREADID, ENTERFUNCTION, STARTLINE,
// Dartagnan specific attributes
EVENTID, LOADEDVALUE, STOREDVALUE;
CREATETHREAD, THREADID, ENTERFUNCTION, STARTLINE;

@Override
public String toString() {
Expand All @@ -17,12 +15,6 @@ public String toString() {
return "enterFunction";
case STARTLINE:
return "startline";
case EVENTID:
return "event-id";
case LOADEDVALUE:
return "loaded-value";
case STOREDVALUE:
return "stored-value";
default:
throw new UnsupportedOperationException(this + " cannot be converted to String");
}
Expand Down
17 changes: 0 additions & 17 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.event.core.Assert;
import com.dat3m.dartagnan.program.event.core.Event;
import com.dat3m.dartagnan.program.event.core.Load;
import com.dat3m.dartagnan.program.event.core.Store;
import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic;
import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
Expand Down Expand Up @@ -156,22 +155,6 @@ public WitnessGraph build() {
threads++;
}

// FIXME: The tracking of "globalId" here is very fragile
// If we generate a Witness and try to use it after adapting any processing pass
// the matching will fail. In particular, a Witness can only be validated
// by the version of Dartagnan that created it and only with identical
// configurations.
if (e instanceof Load l) {
edge.addAttribute(EVENTID.toString(), valueOf(e.getGlobalId()));
edge.addAttribute(LOADEDVALUE.toString(), String.valueOf(model.evaluate(context.result(l))));
}

if (e instanceof Store s) {
edge.addAttribute(EVENTID.toString(), valueOf(e.getGlobalId()));
Object valueObject = checkNotNull(model.evaluate(context.value(s)));
edge.addAttribute(STOREDVALUE.toString(), valueObject.toString());
}

graph.addEdge(edge);

nextNode++;
Expand Down
Loading

0 comments on commit 3577e0e

Please sign in to comment.