From a7809f37054196859c50e4b12f918d19da39de21 Mon Sep 17 00:00:00 2001 From: Tianrui Zheng Date: Fri, 6 Dec 2024 16:26:31 +0100 Subject: [PATCH] Optimize some logics in ExecutionModelManager Signed-off-by: Tianrui Zheng --- .../java/com/dat3m/dartagnan/Dartagnan.java | 1 - .../solver/caat4wmm/EventDomainNext.java | 2 + .../model/ExecutionModelManager.java | 65 +++++++++---------- .../verification/model/event/FenceModel.java | 4 +- .../verification/model/event/LoadModel.java | 5 +- .../model/event/MemoryEventModel.java | 6 +- .../model/event/RegReaderModel.java | 2 +- .../verification/model/event/StoreModel.java | 5 +- .../dartagnan/witness/graphviz/ColorMap.java | 2 - 9 files changed, 42 insertions(+), 50 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index b1ba46f1ff..91422d0c40 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -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()), diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java index b21fb7bb1b..40ee4beb56 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/EventDomainNext.java @@ -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 { private final ExecutionModelNext executionModel; private final List eventList; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java index 88a44131f3..29e6936ab7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -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(); @@ -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. @@ -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) { @@ -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); @@ -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)); @@ -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; } @@ -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())); } } } @@ -369,8 +367,7 @@ public Void visitReadFrom(ReadFrom readFrom) { SimpleGraph rg = (SimpleGraph) relGraphCache.get(relation); EncodingContext.EdgeEncoder rf = context.edge(relation); - for (Map.Entry> reads : executionModel.getAddressReadsMap() - .entrySet()) { + for (Map.Entry> reads : executionModel.getAddressReadsMap().entrySet()) { BigInteger address = reads.getKey(); if (!executionModel.getAddressWritesMap().containsKey(address)) { continue; } for (LoadModel read : reads.getValue()) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/FenceModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/FenceModel.java index f188742785..a9b9cf1855 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/FenceModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/FenceModel.java @@ -1,6 +1,6 @@ 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; @@ -8,7 +8,7 @@ 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; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java index b468f33f52..685272ddf2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/LoadModel.java @@ -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; @@ -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); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java index 0d28d03392..4be096d165 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/MemoryEventModel.java @@ -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; @@ -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; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java index eed42394d5..8daffd24fb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/RegReaderModel.java @@ -9,5 +9,5 @@ public interface RegReaderModel extends EventModel { default Set getRegisterReads() { return ((RegReader) this.getEvent()).getRegisterReads(); - }; + } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java index b511f2e2b6..0102d67143 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/StoreModel.java @@ -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; @@ -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); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java index 49db3f50c1..4a42a24e6c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ColorMap.java @@ -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()); }