Change default value of witness option and add some annotations

Signed-off-by: Tianrui Zheng <[email protected]>
hernanponcedeleon · Dec 9, 2024 · a1d11da · a1d11da
1 parent a7809f3
commit a1d11da
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 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
@@ -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
@@ -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
@@ -47,12 +47,12 @@ public class ExecutionGraphVisualizer {
     private BiPredicate<EventModel, EventModel> rfFilter = (x, y) -> true;
     private BiPredicate<EventModel, EventModel> coFilter = (x, y) -> true;
     private final List<MemoryObjectModel> sortedMemoryObjects = new ArrayList<>();
-    private List<String> relsToShow = List.of(PO, CO, RF);
+    private List<String> 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<String> 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);