Skip to content

Commit

Permalink
Decouple EncodingContext and SMT Model from ExecutionModelNext
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 26, 2024
1 parent b1609e7 commit 89107bd
Show file tree
Hide file tree
Showing 7 changed files with 99 additions and 156 deletions.
4 changes: 2 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 @@ -233,8 +233,8 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir

final EncodingContext encodingContext = modelChecker instanceof RefinementSolver refinementSolver ?
refinementSolver.getContextWithFullWmm() : modelChecker.getEncodingContext();
final ExecutionModelNext m = ExecutionModelManager.newManager(encodingContext)
.initializeModel(prover.getModel());
final ExecutionModelManager manager = new ExecutionModelManager();
final ExecutionModelNext m = manager.buildExecutionModel(encodingContext, prover.getModel());
final SyntacticContextAnalysis synContext = newInstance(task.getProgram());
final String progName = task.getProgram().getName();
final int fileSuffixIndex = progName.lastIndexOf('.');
Expand Down
65 changes: 36 additions & 29 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@
import com.dat3m.dartagnan.program.memory.MemoryObject;
import com.dat3m.dartagnan.verification.model.event.EventModelManager;
import com.dat3m.dartagnan.verification.model.relation.RelationModelManager;
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 org.sosy_lab.common.configuration.InvalidConfigurationException;

Expand All @@ -12,54 +14,59 @@


public class ExecutionModelManager {
private final ExecutionModelNext executionModel;
private final EventModelManager eMManager;
private final RelationModelManager rMManager;

private ExecutionModelManager(EncodingContext encodingContext) throws InvalidConfigurationException {
executionModel = new ExecutionModelNext(encodingContext);
eMManager = EventModelManager.newEMManager(executionModel);
rMManager = RelationModelManager.newRMManager(executionModel);
}
private EncodingContext context;
private Model model;
private ExecutionModelNext executionModel;

public static ExecutionModelManager newManager(EncodingContext encodingContext)
throws InvalidConfigurationException
{
return new ExecutionModelManager(encodingContext);
public ExecutionModelManager(){
eMManager = new EventModelManager(this);
rMManager = new RelationModelManager(this);
}

public ExecutionModelNext getExecutionModel() {
return executionModel;
}
public ExecutionModelNext buildExecutionModel(EncodingContext context, Model model) {
if (this.context != null && this.model != null) {
if (this.context == context && this.model == model) {
return executionModel;
}
}

this.context = context;
this.model = model;
executionModel = new ExecutionModelNext(this);

public ExecutionModelNext initializeModel(Model model) {
executionModel.clear();
executionModel.setModel(model);
eMManager.initialize();
eMManager.buildEventModels(executionModel, context);
extractMemoryLayout();
rMManager.initialize();
rMManager.buildRelationModels(executionModel, context);

executionModel.setManager(this);
return executionModel;
}

public EncodingContext getContext() {
return context;
}

public boolean isTrue(BooleanFormula formula) {
return Boolean.TRUE.equals(model.evaluate(formula));
}

public Object evaluateByModel(Formula formula) {
return model.evaluate(formula);
}

public void extractRelations(List<String> relationNames) {
rMManager.extractRelations(relationNames);
}

private void extractMemoryLayout() {
for (MemoryObject obj : executionModel.getProgram().getMemory().getObjects()) {
for (MemoryObject obj : context.getTask().getProgram().getMemory().getObjects()) {
final boolean isAllocated = obj.isStaticallyAllocated()
|| executionModel.isTrue(
executionModel.getEncodingContext().execution(obj.getAllocationSite())
);
|| isTrue(context.execution(obj.getAllocationSite()));
if (isAllocated) {
final BigInteger address = (BigInteger) executionModel.evaluateByModel(
executionModel.getEncodingContext().address(obj)
);
final BigInteger size = (BigInteger) executionModel.evaluateByModel(
executionModel.getEncodingContext().size(obj)
);
final BigInteger address = (BigInteger) evaluateByModel(context.address(obj));
final BigInteger size = (BigInteger) evaluateByModel(context.size(obj));
executionModel.addMemoryObject(obj, new MemoryObjectModel(obj, address, size));
}
}
Expand Down
72 changes: 6 additions & 66 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,6 +1,5 @@
package com.dat3m.dartagnan.verification.model;

import com.dat3m.dartagnan.encoding.EncodingContext;
import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.memory.MemoryObject;
Expand All @@ -9,10 +8,6 @@
import com.dat3m.dartagnan.verification.model.event.*;
import com.dat3m.dartagnan.verification.model.relation.RelationModel;
import com.dat3m.dartagnan.wmm.Relation;
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.math.BigInteger;
import java.util.*;
Expand All @@ -22,13 +17,9 @@

// 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.
// and RelationModel for relations. It is used only by ExecutionGraphVisualizer so far.
public class ExecutionModelNext {
private final EncodingContext encodingContext;
private Model model;
private ExecutionModelManager manager;
private final ExecutionModelManager manager;

private final List<Thread> threadList;
private final List<EventModel> eventList;
Expand Down Expand Up @@ -68,12 +59,12 @@ public class ExecutionModelNext {
private Map<StoreModel, Set<LoadModel>> writeReadsMapView;
private Map<BigInteger, List<StoreModel>> coherenceMapView;

ExecutionModelNext(EncodingContext encodingContext) {
this.encodingContext = checkNotNull(encodingContext);
ExecutionModelNext(ExecutionModelManager manager) {
this.manager = manager;

threadList = new ArrayList<>(getProgram().getThreads().size());
threadList = new ArrayList<>();
eventList = new ArrayList<>();
threadEventsMap = new HashMap<>(getProgram().getThreads().size() * 4 / 3, 0.75f);
threadEventsMap = new HashMap<>();
eventMap = new HashMap<>();
relationMap = new HashMap<>();
relationNameMap = new HashMap<>();
Expand Down Expand Up @@ -113,33 +104,6 @@ private void createViews() {
coherenceMapView = Collections.unmodifiableMap(coherenceMap);
}

void clear() {
threadList.clear();
eventList.clear();
threadEventsMap.clear();
eventMap.clear();
relationMap.clear();
relationNameMap.clear();
memoryLayoutMap.clear();
addressReadsMap.clear();
addressWritesMap.clear();
addressAccessesMap.clear();
addressInitMap.clear();
fenceMap.clear();
atomicBlocksMap.clear();
readWriteMap.clear();
writeReadsMap.clear();
coherenceMap.clear();
}

void setModel(Model model) {
this.model = model;
}

void setManager(ExecutionModelManager manager) {
this.manager = manager;
}

public void addThreadEvents(Thread thread, List<EventModel> events) {
threadList.add(thread);
threadEventsMap.put(thread, events);
Expand Down Expand Up @@ -208,26 +172,10 @@ public void addCoherenceWrites(BigInteger address, List<StoreModel> writes) {
coherenceMap.put(address, writes);
}

public EncodingContext getEncodingContext() {
return encodingContext;
}

public ExecutionModelManager getManager() {
return manager;
}

public EncodingContext getContext() {
return encodingContext;
}

public Program getProgram() {
return encodingContext.getTask().getProgram();
}

public Wmm getMemoryModel() {
return encodingContext.getTask().getMemoryModel();
}

public List<Thread> getThreads() {
return threadList;
}
Expand Down Expand Up @@ -281,12 +229,4 @@ public Map<BigInteger, StoreModel> getAddressInitMap() {
public Map<Thread, List<List<EventModel>>> getAtomicBlocksMap() {
return atomicBlocksMapView;
}

public boolean isTrue(BooleanFormula formula) {
return Boolean.TRUE.equals(model.evaluate(formula));
}

public Object evaluateByModel(Formula formula) {
return model.evaluate(formula);
}
}
35 changes: 15 additions & 20 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 @@ -7,6 +7,7 @@
import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic;
import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic;
import com.dat3m.dartagnan.program.filter.Filter;
import com.dat3m.dartagnan.verification.model.ExecutionModelManager;
import com.dat3m.dartagnan.verification.model.ExecutionModelNext;

import static com.google.common.base.Preconditions.checkNotNull;
Expand All @@ -17,33 +18,29 @@


public class EventModelManager {
private final ExecutionModelNext executionModel;
private final ExecutionModelManager manager;
private final Map<Event, EventModel> eventCache;

private ExecutionModelNext executionModel;
private EncodingContext context;
private Filter eventFilter;

private EventModelManager(ExecutionModelNext executionModel) {
this.executionModel = checkNotNull(executionModel);
public EventModelManager(ExecutionModelManager manager) {
this.manager = manager;
eventCache = new HashMap<>();
}

public static EventModelManager newEMManager(ExecutionModelNext executionModel) {
return new EventModelManager(executionModel);
}

public EncodingContext getEncodingContext() {
return executionModel.getEncodingContext();
}

public void initialize() {
public void buildEventModels(ExecutionModelNext executionModel, EncodingContext context) {
this.executionModel = executionModel;
this.context = context;
eventCache.clear();
eventFilter = Filter.byTag(Tag.VISIBLE);
extractEvents();
}

private void extractEvents() {
int id = 0;
List<Thread> threadList = new ArrayList<>(executionModel.getProgram().getThreads());
List<Thread> threadList = new ArrayList<>(context.getTask().getProgram().getThreads());

for (Thread t : threadList) {
int localId = 0;
Expand All @@ -53,7 +50,7 @@ private void extractEvents() {
Event e = t.getEntry();

do {
if (!executionModel.isTrue(getEncodingContext().execution(e))) {
if (!manager.isTrue(context.execution(e))) {
e = e.getSuccessor();
continue;
}
Expand All @@ -72,7 +69,7 @@ private void extractEvents() {
}

if (e instanceof CondJump jump
&& executionModel.isTrue(getEncodingContext().jumpCondition(jump))
&& manager.isTrue(context.jumpCondition(jump))
) {
e = jump.getLabel();
} else {
Expand Down Expand Up @@ -118,7 +115,7 @@ private EventModel getOrCreateModel(Event e, int id, int localId) {
em.setLocalId(localId);
if (e instanceof CondJump) {
em.setWasExecuted(
executionModel.isTrue(getEncodingContext().jumpCondition((CondJump) e))
manager.isTrue(context.jumpCondition((CondJump) e))
);
} else { em.setWasExecuted(true); }
eventCache.put(e, em);
Expand All @@ -130,7 +127,7 @@ private EventModel createAndInitializeModel(Event e) {
EventModel em;
if (e.hasTag(Tag.MEMORY)) {
Object addressObj = checkNotNull(
executionModel.evaluateByModel(getEncodingContext().address((MemoryEvent) e))
manager.evaluateByModel(context.address((MemoryEvent) e))
);
BigInteger address = new BigInteger(addressObj.toString());
executionModel.addAccessedAddress(address);
Expand All @@ -152,9 +149,7 @@ private EventModel createAndInitializeModel(Event e) {

if (em.isRead() || em.isWrite()) {
String valueString = String.valueOf(
executionModel.evaluateByModel(
getEncodingContext().value((MemoryCoreEvent) e)
)
manager.evaluateByModel(context.value((MemoryCoreEvent) e))
);
BigInteger value = switch(valueString) {
// NULL case can happen if the solver optimized away a variable.
Expand Down
Loading

0 comments on commit 89107bd

Please sign in to comment.