Skip to content

Commit

Permalink
Add annotations
Browse files Browse the repository at this point in the history 
Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>
  • Loading branch information
Tianrui Zheng committed Nov 18, 2024
1 parent 524185d commit f57457d
Show file tree
Hide file tree
Showing 8 changed files with 46 additions and 105 deletions.
2 changes: 0 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -239,8 +239,6 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir
manager.setContextWithFullWmm(contextWithFullWmm);
}
final ExecutionModelNext m = manager.initializeModel(prover.getModel());
// final ExecutionModel m = ExecutionModel.withContext(modelChecker.getEncodingContext());
// m.initialize(prover.getModel());
final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
final String progName = task.getProgram().getName();
final int fileSuffixIndex = progName.lastIndexOf('.');
Expand Down
4 changes: 4 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,10 @@ private void extractEventsFromModel() {
e = e.getSuccessor();
continue;
}
// In the new model we extract visible events, Locals and Asserts to show them in the
// witness, and extract also CondJumps for tracking internal dependencies. For consistency
// of the view of events which infects the derived relation computation by CAAT, we need
// to extract the same events here in the old model.
if (eventFilter.apply(e)
|| e instanceof Local
|| e instanceof Assert
Expand Down
21 changes: 14 additions & 7 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java
View file
Original file line number Diff line number Diff line change
@@ -1,29 +1,35 @@
package com.dat3m.dartagnan.verification.model;

import com.dat3m.dartagnan.encoding.EncodingContext;
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.memory.MemoryObject;
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.verification.model.event.*;
import com.dat3m.dartagnan.verification.model.relation.RelationModel;
import com.dat3m.dartagnan.wmm.Wmm;
import com.dat3m.dartagnan.wmm.Relation;
import org.sosy_lab.java_smt.api.Model;
import org.sosy_lab.java_smt.api.Formula;
import com.dat3m.dartagnan.wmm.Wmm;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.Model;

import java.util.*;
import java.math.BigInteger;
import java.util.*;

import static com.google.common.base.Preconditions.checkNotNull;


// This is a new implementation of ExecutionModel which serves as the data structure
// representing an execution in Dartagnan. It contains instances of EventModel for events
// and RelationModel for relations. It holds the information that has the same name and
// format as the old ExecutionModel so that it can replace the old one easily for CAAT also.
// It is used only by ExecutionGraphVisualizer so far.
public class ExecutionModelNext {
private final EncodingContext encodingContext;
private Model model;
private EncodingContext contextWithFullWmm; // This context is needed for extraction of relations when RefinementSolver being used.
// This context is needed for extraction of relations when RefinementSolver being used.
private EncodingContext contextWithFullWmm;
private ExecutionModelManager manager;

private final List<Thread> threadList;
Expand Down Expand Up @@ -152,6 +158,7 @@ public void addEvent(Event e, EventModel eModel) {

public void addRelation(Relation r, RelationModel rModel) {
relationMap.put(r, rModel);
// We add an entry for each name of the relation.
for (String name : rModel.getNames()) {
relationNameMap.put(name, rModel);
}
Expand Down
13 changes: 8 additions & 5 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModelManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@
import static com.google.common.base.Preconditions.checkNotNull;
import static com.google.common.base.Preconditions.checkState;

import java.util.*;
import java.math.BigInteger;
import java.util.*;


public class EventModelManager {
Expand Down Expand Up @@ -116,7 +116,11 @@ private EventModel getOrCreateModel(Event e, int id, int localId) {
EventModel em = createAndInitializeModel(e);
em.setId(id);
em.setLocalId(localId);
em.setWasExecuted(true);
if (e instanceof CondJump) {
em.setWasExecuted(
executionModel.isTrue(getEncodingContext().jumpCondition((CondJump) e))
);
} else { em.setWasExecuted(true); }
eventCache.put(e, em);

return em;
Expand Down Expand Up @@ -171,9 +175,6 @@ private EventModel createAndInitializeModel(Event e) {
em = new LocalModel((Local) e);
} else if (e instanceof CondJump) {
em = new CondJumpModel((CondJump) e);
em.setWasExecuted(
executionModel.isTrue(getEncodingContext().jumpCondition((CondJump) e))
);
} else {
em = new DefaultEventModel(e);
}
Expand All @@ -182,6 +183,8 @@ private EventModel createAndInitializeModel(Event e) {
}

private boolean toExtract(Event e) {
// We extract visible events, Locals and Asserts to show them in the witness,
// and extract also CondJumps for tracking internal dependencies.
return eventFilter.apply(e)
|| e instanceof Local
|| e instanceof Assert
Expand Down
21 changes: 13 additions & 8 deletions ...n/src/main/java/com/dat3m/dartagnan/verification/model/relation/RelationModelManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.solver.caat.predicates.CAATPredicate;
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.relationGraphs.Edge;
import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.RelationGraph;
import com.dat3m.dartagnan.solver.caat.predicates.sets.SetPredicate;
import com.dat3m.dartagnan.solver.caat4wmm.EventDomain;
import com.dat3m.dartagnan.solver.caat4wmm.basePredicates.StaticDefaultWMMGraph;
Expand Down Expand Up @@ -117,11 +117,11 @@ public void extractRelations(List<String> relationNames) {
}
}


Set<CAATPredicate> predicates = new HashSet<>(relGraphs);
PredicateHierarchy hierarchy = new PredicateHierarchy(predicates);
hierarchy.initializeToDomain(new EventDomain(oldModel));

// Populate graphs of base relations.
for (CAATPredicate basePred : hierarchy.getBasePredicates()) {
if (basePred.getClass() == StaticWMMSet.class
|| basePred.getClass() == StaticDefaultWMMGraph.class
Expand All @@ -130,6 +130,7 @@ public void extractRelations(List<String> relationNames) {
r.getDefinition().accept(graphPopulator);
}

// Do the computation.
hierarchy.populate();

for (CAATPredicate pred : hierarchy.getPredicateList()) {
Expand Down Expand Up @@ -175,8 +176,7 @@ private RelationGraph getOrCreateGraph(Relation r) {
if (relGraphCache.containsKey(r)) {
return relGraphCache.get(r);
}
RelationGraph rg = createGraph(r);
return rg;
return createGraph(r);
}

private SetPredicate getOrCreateSetFromFilter(Filter filter) {
Expand All @@ -194,8 +194,8 @@ private EdgeModel getOrCreateEdgeModel(Edge e) {
if (edgeModelCache.containsKey(identifier)) {
return edgeModelCache.get(identifier);
}
final List<EventModel> eventList = executionModel.getEventList();
EdgeModel em = new EdgeModel(eventList.get(e.getFirst()), eventList.get(e.getSecond()));
EdgeModel em = new EdgeModel(executionModel.getEventModelById(e.getFirst()),
executionModel.getEventModelById(e.getSecond()));
edgeModelCache.put(identifier, em);
return em;
}
Expand All @@ -211,6 +211,8 @@ private List<EventModel> getVisibleEvents(Thread t) {
}


// Usage: Populate graph of the base relations with instances of the Edge class
// based on the information from ExecutionModelNext.
private final class BaseRelationGraphPopulator implements Visitor<Void> {

@Override
Expand Down Expand Up @@ -429,7 +431,7 @@ public Void visitAddressDependency(DirectAddressDependency addrDirect) {
writes.add((RegWriterModel) em);
continue;
}
if (em.isWrite()) {
if (em.isRegReader()) {
for (RegWriterModel write : writes) {
for (Register.Read read : ((RegReaderModel) em).getRegisterReads()) {
if (read.register() == write.getResultRegister()
Expand Down Expand Up @@ -492,6 +494,9 @@ public Void visitEmpty(Empty empty) {
}


// Create a SimpleGraph for base relations and the specific graph for derived ones,
// so that edges of base relations are set manually and edges of derived ones can be
// computed automatically by PredicateHierarchy.
private final class RelationGraphBuilder implements Visitor<RelationGraph> {

@Override
Expand Down
1 change: 1 addition & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ public abstract class ModelChecker {

protected Result res = Result.UNKNOWN;
protected EncodingContext context;
// This context is needed for extraction of relations when RefinementSolver being used.
protected EncodingContext contextWithFullWmm;
private String flaggedPairsOutput = "";

Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -891,9 +891,9 @@ private static void generateGraphvizFiles(VerificationTask task, ExecutionModelN
final SyntacticContextAnalysis emptySynContext = getEmptyInstance();
// File with reason edges only
generateGraphvizFile(model, iterationCount, edgeFilter, edgeFilter, edgeFilter, directoryName, fileNameBase,
emptySynContext);
emptySynContext, true);
// File with all edges
generateGraphvizFile(model, iterationCount, (x, y) -> true, (x, y) -> true, (x, y) -> true, directoryName,
fileNameBase + "-full", emptySynContext);
fileNameBase + "-full", emptySynContext, true);
}
}
85 changes: 4 additions & 81 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,9 +83,6 @@ public void generateGraphOfExecutionModel(Writer writer, String graphName, Execu
graphviz.append(String.format("label=\"%s\" \n", graphName));
addAllThreadPos(model);
addRelations(model);
// addReadFrom(model);
// addFromRead(model);
// addCoherence(model);
graphviz.end();
graphviz.generateOutput(writer);
}
Expand Down Expand Up @@ -180,69 +177,6 @@ private ExecutionGraphVisualizer addProgramOrder(ExecutionModelNext model) {
return this;
}

// private ExecutionGraphVisualizer addReadFrom(ExecutionModel model) {

// graphviz.beginSubgraph("ReadFrom");
// graphviz.setEdgeAttributes("color=green");
// for (Map.Entry<EventData, EventData> rw : model.getReadWriteMap().entrySet()) {
// EventData r = rw.getKey();
// EventData w = rw.getValue();

// if (ignore(r) || ignore(w) || !rfFilter.test(w, r)) {
// continue;
// }

// appendEdge(w, r, "label=rf");
// }
// graphviz.end();
// return this;
// }

// private ExecutionGraphVisualizer addFromRead(ExecutionModel model) {

// graphviz.beginSubgraph("FromRead");
// graphviz.setEdgeAttributes("color=orange");
// for (Map.Entry<EventData, EventData> rw : model.getReadWriteMap().entrySet()) {
// EventData r = rw.getKey();
// EventData w = rw.getValue();

// if (ignore(r) || ignore(w)) {
// continue;
// }

// List<EventData> co = model.getCoherenceMap().get(w.getAccessedAddress());
// // Check if exists w2 : co(w, w2)
// if (co.indexOf(w) + 1 < co.size()) {
// EventData w2 = co.get(co.indexOf(w) + 1);
// if (!ignore(w2) && frFilter.test(r, w2)) {
// appendEdge(r, w2, "label=fr");
// }
// }
// }
// graphviz.end();
// return this;
// }

// private ExecutionGraphVisualizer addCoherence(ExecutionModel model) {

// graphviz.beginSubgraph("Coherence");
// graphviz.setEdgeAttributes("color=red");

// for (List<EventData> co : model.getCoherenceMap().values()) {
// for (int i = 2; i < co.size(); i++) {
// // We skip the init writes
// EventData w1 = co.get(i - 1);
// EventData w2 = co.get(i);
// if (ignore(w1) || ignore(w2) || !coFilter.test(w1, w2)) {
// continue;
// }
// appendEdge(w1, w2, "label=co");
// }
// }
// graphviz.end();
// return this;
// }

private ExecutionGraphVisualizer addAllThreadPos(ExecutionModelNext model) {
for (Thread thread : model.getThreads()) {
addThreadPo(thread, model);
Expand All @@ -259,18 +193,7 @@ private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModelNext m

// --- Subgraph start ---
graphviz.beginSubgraph("T" + thread.getId());
// graphviz.setEdgeAttributes("weight=100");
// // --- Node list ---
// for (int i = 1; i < threadEvents.size(); i++) {
// EventData e1 = threadEvents.get(i - 1);
// EventData e2 = threadEvents.get(i);

// if (ignore(e1) || ignore(e2)) {
// continue;
// }

// appendEdge(e1, e2, (String[]) null);
// }

for (EventModel e : threadEvents) {
appendNode(e, (String[]) null);
}
Expand Down Expand Up @@ -303,7 +226,7 @@ private String eventToNode(EventModel e) {
return String.format("\"I(%s, %d)\"", getAddressString(
((StoreModel) e).getAccessedAddress()), ((StoreModel) e).getValue());
}
// We have MemEvent + Fence
// We have MemEvent + Fence + Local + Assert
String tag = e.getEvent().toString();
if (e.isMemoryEvent()) {
String address = getAddressString(((MemoryEventModel) e).getAccessedAddress());
Expand Down Expand Up @@ -369,8 +292,8 @@ public static File generateGraphvizFile(ExecutionModelNext model, int iterationC
public static void generateGraphvizFile(ExecutionModelNext model, int iterationCount,
BiPredicate<EventModel, EventModel> rfFilter, BiPredicate<EventModel, EventModel> frFilter,
BiPredicate<EventModel, EventModel> coFilter, String directoryName, String fileNameBase,
SyntacticContextAnalysis synContext) {
SyntacticContextAnalysis synContext, boolean usedByRefinementSolver) {
generateGraphvizFile(model, iterationCount, rfFilter, frFilter, coFilter, directoryName, fileNameBase,
synContext, true, true);
synContext, true, usedByRefinementSolver);
}
}

0 comments on commit f57457d

Please sign in to comment.