Skip to content

Commit

Permalink
Optimize some logics in ExecutionModelManager
Browse files Browse the repository at this point in the history 
Signed-off-by: Tianrui Zheng <[email protected]>
  • Loading branch information
Tianrui Zheng committed Dec 6, 2024
1 parent 8a0518e commit a7809f3
Show file tree
Hide file tree
Showing 9 changed files with 42 additions and 50 deletions.
1 change: 0 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -238,7 +238,6 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir
(fileSuffixIndex == - 1) ? progName : progName.substring(0, fileSuffixIndex);
// RF edges give both ordering and data flow information, thus even when the pair is in PO
// we get some data flow information by observing the edge
// FR edges only give ordering information which is known if the pair is also in PO
// CO edges only give ordering information which is known if the pair is also in PO
return generateGraphvizFile(encodingContext, prover.getModel(), 1, (x, y) -> true,
(x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()),
Expand Down
2 changes: 2 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@
import java.util.List;


// TODO: this class is temporary and needs to be merged into EventDomain
// once there is one ExecutionModel for all use cases.
public class EventDomainNext implements Domain<EventModel> {
private final ExecutionModelNext executionModel;
private final List<EventModel> eventList;
Expand Down
65 changes: 31 additions & 34 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 @@ -114,8 +114,7 @@ private void extractEvents() {
}

if (e instanceof CondJump jump
&& isTrue(context.jumpCondition(jump))
) {
&& isTrue(context.jumpCondition(jump))) {
e = jump.getLabel();
} else {
e = e.getSuccessor();
Expand All @@ -129,14 +128,14 @@ && isTrue(context.jumpCondition(jump))

private void extractEvent(Event e, ThreadModel tm, int id) {
EventModel em;
if (e.hasTag(Tag.MEMORY)) {
if (e instanceof MemoryEvent memEvent) {
Object addressObj = checkNotNull(
evaluateByModel(context.address((MemoryEvent) e))
evaluateByModel(context.address(memEvent))
);
final BigInteger address = new BigInteger(addressObj.toString());

String valueString = String.valueOf(
evaluateByModel(context.value((MemoryCoreEvent) e))
evaluateByModel(context.value(memEvent))
);
final BigInteger value = switch(valueString) {
// NULL case can happen if the solver optimized away a variable.
Expand All @@ -146,21 +145,22 @@ private void extractEvent(Event e, ThreadModel tm, int id) {
default -> new BigInteger(valueString);
};

if (e.hasTag(Tag.READ)) {
em = new LoadModel(e, tm, id, address, value);
if (memEvent.hasTag(Tag.READ)) {
em = new LoadModel(memEvent, tm, id, address, value);
executionModel.addAddressRead(address, (LoadModel) em);
} else if (e.hasTag(Tag.WRITE)) {
em = new StoreModel(e, tm, id, address, value);
} else if (memEvent.hasTag(Tag.WRITE)) {
em = new StoreModel(memEvent, tm, id, address, value);
executionModel.addAddressWrite(address, (StoreModel) em);
} else {
// Should never happen.
logger.warn("Event {} has Tag MEMORY but no READ or WRITE", e);
em = new MemoryEventModel(e, tm, id, address, value);
throw new IllegalArgumentException(String.format(
"Event %s is memory event but neither read nor write", memEvent
));
}

} else if (e.hasTag(Tag.FENCE)) {
final String name = ((GenericVisibleEvent) e).getName();
em = new FenceModel(e, tm, id, name);
} else if (e.hasTag(Tag.FENCE) && e instanceof GenericVisibleEvent visible) {
final String name = (visible).getName();
em = new FenceModel(visible, tm, id, name);
} else if (e instanceof Assert assrt) {
em = new AssertModel(assrt, tm, id);
} else if (e instanceof Local local) {
Expand All @@ -169,8 +169,7 @@ private void extractEvent(Event e, ThreadModel tm, int id) {
em = new CondJumpModel(cj, tm, id);
} else {
// Should never happen.
logger.warn("Extracting the event {} that should not be extracted", e);
em = new DefaultEventModel(e, tm, id);
throw new IllegalArgumentException(String.format("Event %s should not be extracted", e));
}

executionModel.addEvent(e, em);
Expand All @@ -188,7 +187,7 @@ private boolean toExtract(Event e) {
private void extractMemoryLayout() {
for (MemoryObject obj : context.getTask().getProgram().getMemory().getObjects()) {
boolean isAllocated = obj.isStaticallyAllocated()
|| isTrue(context.execution(obj.getAllocationSite()));
|| isTrue(context.execution(obj.getAllocationSite()));
if (isAllocated) {
BigInteger address = (BigInteger) evaluateByModel(context.address(obj));
BigInteger size = (BigInteger) evaluateByModel(context.size(obj));
Expand All @@ -198,28 +197,26 @@ private void extractMemoryLayout() {
}

// Getting the correct relation to extract is tricky.
// In the case of redefinition, we have to find the latest defined one which we care about only.
// If there is no redefinition the original one will be returned simply.
// In the case of redefinition, we care about the one defined last.
// If there is no redefinition, we simply return the original one.
private Relation getRelationWithName(String name) {
// First check if the original definition is asked.
if (name.endsWith("#0")) {
String originalName = name.substring(0, name.lastIndexOf("#"));
Relation r = wmm.getRelation(originalName);
if (r != null) { return r; }
return wmm.getRelation(originalName);
}

int maxId = -1;
for (Relation r : wmm.getRelations()) {
final int defIndex = r.getNames().stream().filter(s -> s.startsWith(name + "#"))
.map(s -> {
try {
return Integer.parseInt(s.substring(s.lastIndexOf("#") + 1));
} catch (NumberFormatException e) {
return Integer.MIN_VALUE;
}
})
.filter(i -> i != Integer.MIN_VALUE)
.max(Comparator.naturalOrder()).orElse(0);
int defIndex = 0;
for (String n : r.getNames()) {
if (n.startsWith(name + "#")) {
try {
defIndex = Integer.parseInt(n.substring(n.lastIndexOf("#") + 1));
break;
} catch (NumberFormatException e) {}
}
}
if (defIndex != 0 && defIndex > maxId) {
maxId = defIndex;
}
Expand Down Expand Up @@ -356,7 +353,8 @@ public Void visitProgramOrder(ProgramOrder po) {
for (int i = 1; i < eventList.size(); i++) {
EventModel e1 = eventList.get(i);
for (int j = i + 1; j < eventList.size(); j++) {
rg.add(new Edge(e1.getId(), eventList.get(j).getId()));
EventModel e2 = eventList.get(j);
rg.add(new Edge(e1.getId(), e2.getId()));
}
}
}
Expand All @@ -369,8 +367,7 @@ public Void visitReadFrom(ReadFrom readFrom) {
SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation);
EncodingContext.EdgeEncoder rf = context.edge(relation);

for (Map.Entry<BigInteger, Set<LoadModel>> reads : executionModel.getAddressReadsMap()
.entrySet()) {
for (Map.Entry<BigInteger, Set<LoadModel>> reads : executionModel.getAddressReadsMap().entrySet()) {
BigInteger address = reads.getKey();
if (!executionModel.getAddressWritesMap().containsKey(address)) { continue; }
for (LoadModel read : reads.getValue()) {
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/FenceModel.java
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
package com.dat3m.dartagnan.verification.model.event;

import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.core.GenericVisibleEvent;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.verification.model.ThreadModel;


public class FenceModel extends DefaultEventModel {
private final String name;

public FenceModel(Event event, ThreadModel thread, int id, String name) {
public FenceModel(GenericVisibleEvent event, ThreadModel thread, int id, String name) {
super(event, thread, id);
assert event.hasTag(Tag.FENCE);
this.name = name;
Expand Down
5 changes: 2 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package com.dat3m.dartagnan.verification.model.event;

import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.MemoryEvent;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.verification.model.ThreadModel;

Expand All @@ -9,8 +9,7 @@

public class LoadModel extends MemoryEventModel implements RegWriterModel {
public LoadModel(
Event event, ThreadModel thread, int id, BigInteger address, BigInteger value
) {
MemoryEvent event, ThreadModel thread, int id, BigInteger address, BigInteger value) {
super(event, thread, id, address, value);
assert event.hasTag(Tag.READ);
}
Expand Down
6 changes: 2 additions & 4 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package com.dat3m.dartagnan.verification.model.event;

import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.MemoryEvent;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.verification.model.ThreadModel;

Expand All @@ -13,10 +13,8 @@ public class MemoryEventModel extends DefaultEventModel implements RegReaderMode
protected final BigInteger value;

public MemoryEventModel(
Event event, ThreadModel thread, int id, BigInteger address, BigInteger value
) {
MemoryEvent event, ThreadModel thread, int id, BigInteger address, BigInteger value) {
super(event, thread, id);
assert event.hasTag(Tag.MEMORY);
this.accessedAddress = address;
this.value = value;
}
Expand Down
2 changes: 1 addition & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,5 @@
public interface RegReaderModel extends EventModel {
default Set<Read> getRegisterReads() {
return ((RegReader) this.getEvent()).getRegisterReads();
};
}
}
5 changes: 2 additions & 3 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package com.dat3m.dartagnan.verification.model.event;

import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.MemoryEvent;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.verification.model.ThreadModel;

Expand All @@ -9,8 +9,7 @@

public class StoreModel extends MemoryEventModel {
public StoreModel(
Event event, ThreadModel thread, int id, BigInteger address, BigInteger value
) {
MemoryEvent event, ThreadModel thread, int id, BigInteger address, BigInteger value) {
super(event, thread, id, address, value);
assert event.hasTag(Tag.WRITE);
}
Expand Down
2 changes: 0 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,6 @@ class ColorMap {
fixedColorMap.put(RF, colorToHex(Color.getHSBColor(0.33f, 1.0f, 1.0f)));
// Red for CO
fixedColorMap.put(CO, colorToHex(Color.getHSBColor(0.0f, 1.0f, 1.0f)));
// Orange for FR
fixedColorMap.put("fr", colorToHex(Color.getHSBColor(0.08f, 1.0f, 1.0f)));

usedColors.addAll(fixedColorMap.values());
}
Expand Down

0 comments on commit a7809f3

Please sign in to comment.