From a1d11da447025fd5ea1edba4572140da2967e7e7 Mon Sep 17 00:00:00 2001 From: Tianrui Zheng Date: Mon, 9 Dec 2024 10:27:52 +0100 Subject: [PATCH] Change default value of witness option and add some annotations Signed-off-by: Tianrui Zheng --- .../model/ExecutionModelManager.java | 4 ++++ .../solving/RefinementSolver.java | 2 +- .../graphviz/ExecutionGraphVisualizer.java | 19 ++++++++----------- 3 files changed, 13 insertions(+), 12 deletions(-) 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 29e6936ab7..40a38cde28 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 @@ -137,6 +137,9 @@ private void extractEvent(Event e, ThreadModel tm, int id) { String valueString = String.valueOf( evaluateByModel(context.value(memEvent)) ); + // The old ExecutionModel represents all values as integers for CAAT-use. + // TODO: A ValueModel representing different types of values could be useful + // for both CAAT and witness. final BigInteger value = switch(valueString) { // NULL case can happen if the solver optimized away a variable. // This should only happen if the value is irrelevant, so we will just pick 0. @@ -189,6 +192,7 @@ private void extractMemoryLayout() { boolean isAllocated = obj.isStaticallyAllocated() || isTrue(context.execution(obj.getAllocationSite())); if (isAllocated) { + // Currently, addresses of memory objects are guaranteed to be integer and assigned. BigInteger address = (BigInteger) evaluateByModel(context.address(obj)); BigInteger size = (BigInteger) evaluateByModel(context.size(obj)); executionModel.addMemoryObject(obj, new MemoryObjectModel(obj, address, size)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index b90e5454f2..42f9f33562 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -740,7 +740,7 @@ private void instrumentPolaritySeparation(Wmm wmm) { if (replacements.containsKey(b)) { bPrime = replacements.get(b); } else { - final String bPrimeName = b.getName().map(n -> n + "#POS").orElse("__POS" + counter++); + final String bPrimeName = b.getName().map(n -> n + "__POS").orElse("__POS" + counter++); bPrime = wmm.addDefinition(new Free(wmm.newRelation(bPrimeName))); replacements.put(b, bPrime); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java index 2828480043..b2ec631fa9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java @@ -47,12 +47,12 @@ public class ExecutionGraphVisualizer { private BiPredicate rfFilter = (x, y) -> true; private BiPredicate coFilter = (x, y) -> true; private final List sortedMemoryObjects = new ArrayList<>(); - private List relsToShow = List.of(PO, CO, RF); + private List relsToShow; @Option(name=WITNESS_SHOW, description="Names of relations to show in the witness graph.", secure=true) - private String relsToShowStr = ""; + private String relsToShowStr = String.format("%s,%s,%s", PO, CO, RF); public ExecutionGraphVisualizer() { this.graphviz = new Graphviz(); @@ -88,9 +88,7 @@ public void generateGraphOfExecutionModel( private List setRelationsToShow(EncodingContext context) throws InvalidConfigurationException { context.getTask().getConfig().inject(this); - if (!relsToShowStr.isEmpty()) { - relsToShow = Arrays.asList(relsToShowStr.split(",\\s*")); - } + relsToShow = Arrays.asList(relsToShowStr.split(",\\s*")); return relsToShow; } @@ -109,15 +107,15 @@ private RelationModel getRelationModelByName(ExecutionModelNext model, String na Relation r = rm.getRelation(); if (r.hasName(name) || r.getNames().stream().anyMatch(n -> n.startsWith(name + "#")) - || (name.endsWith("#0") && r.hasName(name.substring(0, name.lastIndexOf("#"))))) - { return rm; } + || (name.endsWith("#0") && r.hasName(name.substring(0, name.lastIndexOf("#"))))) { + return rm; + } } return null; } private ExecutionGraphVisualizer addRelations( - ExecutionModelNext model, EncodingContext context, Model smtModel - ) { + ExecutionModelNext model, EncodingContext context, Model smtModel) { for (String name : relsToShow) { RelationModel rm = getRelationModelByName(model, name); if (rm == null) { @@ -181,8 +179,7 @@ private ExecutionGraphVisualizer addProgramOrder(ExecutionModelNext model, Strin } private ExecutionGraphVisualizer addCoherence( - RelationModel rm, ExecutionModelNext model, String name, EncodingContext context, Model smtModel - ) { + RelationModel rm, ExecutionModelNext model, String name, EncodingContext context, Model smtModel) { graphviz.beginSubgraph(name); String attributes = String.format("color=%s", colorMap.getColor(CO)); graphviz.setEdgeAttributes(attributes);