Added Printer.Mode to only print threads, functions, or both.

Also added short output for skipped init threads when printing.

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DebugPrint.java

@@ -6,18 +6,20 @@
 public class DebugPrint implements ProgramProcessor {
 
     private final String printHeader;
+    private final Printer.Mode printerMode;
 
-    private DebugPrint(String printHeader) {
+    private DebugPrint(String printHeader, Printer.Mode mode) {
         this.printHeader = printHeader;
+        this.printerMode = mode;
     }
 
-    public static DebugPrint withHeader(String header) { return new DebugPrint(header);}
-    public static DebugPrint newInstance() { return withHeader("DebugPrint"); }
+    public static DebugPrint withHeader(String header, Printer.Mode mode) { return new DebugPrint(header, mode);}
+    public static DebugPrint newInstance(Printer.Mode mode) { return withHeader("DebugPrint", mode); }
 
     @Override
     public void run(Program program) {
         System.out.println("======== " + printHeader +  " ========");
-        System.out.println(new Printer().print(program));
+        System.out.println(new Printer().print(program, printerMode));
         System.out.println("======================================");
     }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java

@@ -2,6 +2,7 @@
 
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.processing.compilation.Compilation;
+import com.dat3m.dartagnan.utils.printer.Printer;
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.common.configuration.Option;
@@ -66,7 +67,7 @@ public class ProcessingManager implements ProgramProcessor {
     @Option(name = PRINT_PROGRAM_AFTER_PROCESSING,
             description = "Prints the program after all processing.",
             secure = true)
-    private boolean printAfterProcessing = true;
+    private boolean printAfterProcessing = false;
 
 
 // ======================================================================
@@ -75,7 +76,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
         config.inject(this);
 
         programProcessors.addAll(Arrays.asList(
-                printBeforeProcessing ? DebugPrint.withHeader("Before processing") : null,
+                printBeforeProcessing ? DebugPrint.withHeader("Before processing", Printer.Mode.ALL) : null,
                 StaticMemoryInitializer.newInstance(),
                 ProgramProcessor.fromFunctionProcessor(
                         FunctionProcessor.chain(
@@ -86,16 +87,16 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                                 Simplifier.fromConfig(config)
                         ), Target.FUNCTIONS, true
                 ),
-                printAfterSimplification ? DebugPrint.withHeader("After simplification") : null,
+                printAfterSimplification ? DebugPrint.withHeader("After simplification", Printer.Mode.ALL) : null,
                 LoopFormVerification.fromConfig(config),
                 Compilation.fromConfig(config), // We keep compilation global for now
-                printAfterCompilation ? DebugPrint.withHeader("After compilation") : null,
+                printAfterCompilation ? DebugPrint.withHeader("After compilation", Printer.Mode.ALL) : null,
                 ProgramProcessor.fromFunctionProcessor(
                         SimpleSpinLoopDetection.fromConfig(config),
                         Target.FUNCTIONS, false
                 ),
                 LoopUnrolling.fromConfig(config), // We keep unrolling global for now
-                printAfterUnrolling ? DebugPrint.withHeader("After loop unrolling") : null,
+                printAfterUnrolling ? DebugPrint.withHeader("After loop unrolling", Printer.Mode.ALL) : null,
                 dynamicPureLoopCutting ? DynamicPureLoopCutting.fromConfig(config) : null,
                 ProgramProcessor.fromFunctionProcessor(
                         FunctionProcessor.chain(
@@ -110,7 +111,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                 MemoryAllocation.newInstance(),
                 // --- Statistics + verification ---
                 IdReassignment.newInstance(), // Normalize used Ids (remove any gaps)
-                printAfterProcessing ? DebugPrint.withHeader("After processing") : null,
+                printAfterProcessing ? DebugPrint.withHeader("After processing", Printer.Mode.THREADS) : null,
                 ProgramProcessor.fromFunctionProcessor(
                         CoreCodeVerification.fromConfig(config),
                         Target.THREADS, false

dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java

@@ -12,6 +12,12 @@
 
 public class Printer {
 
+    public enum Mode {
+        THREADS,
+        FUNCTIONS,
+        ALL
+    }
+
     private StringBuilder result;
     private StringBuilder padding;
 
@@ -21,7 +27,7 @@ public class Printer {
 
     private final String paddingBase = "      ";
 
-    public String print(Program program){
+    public String print(Program program, Mode mode) {
         result = new StringBuilder();
         padding = new StringBuilder(paddingBase);
 
@@ -34,17 +40,29 @@ public String print(Program program){
         }
         result.append(name).append("\n");
 
-        for(Thread thread : program.getThreads()) {
-            if(shouldPrintThread(thread)){
-                appendFunction(thread);
+        if (mode == Mode.THREADS || mode == Mode.ALL) {
+            for (Thread thread : program.getThreads()) {
+                if (shouldPrintThread(thread)) {
+                    appendFunction(thread);
+                }
+            }
+
+            if (!showInitThreads && !program.getThreads().isEmpty()) {
+                result.append("\nSkipping init threads...");
+                result.append("\n...");
+                result.append("\n...");
+                result.append("\n...");
+                result.append("\n");
             }
         }
 
-        for (Function function : program.getFunctions()) {
-            if (function instanceof Thread) {
-                continue;
+        if (mode == Mode.FUNCTIONS || mode == Mode.ALL) {
+            for (Function function : program.getFunctions()) {
+                if (function instanceof Thread) {
+                    continue;
+                }
+                appendFunction(function);
             }
-            appendFunction(function);
         }
 
         idType = origType;

dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/PrinterTest.java

@@ -21,60 +21,60 @@ public class PrinterTest {
     @Test()
     public void PrintBpl1() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "boogie/concurrency/fib_bench-1-O0.bpl"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         Compilation.newInstance().run(p);
         LoopUnrolling.newInstance().run(p);
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
     }
 
     @Test()
     public void PrintBpl2() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "locks/linuxrwlock.bpl"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         Compilation.newInstance().run(p);
         LoopUnrolling.newInstance().run(p);
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
     }
 
     @Test()
     public void PrintX86() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/MP+mfence-rmw+rmw-mfence.litmus"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         assertNotNull(p.getSpecification().toString());
     }
 
     @Test()
     public void PrintPPC() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/MP+lwsync+data-wsi-rfi-ctrlisync.litmus"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         assertNotNull(p.getSpecification().toString());
     }
 
     @Test()
     public void PrintAARCH64() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/MP+popl+poap.litmus"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         assertNotNull(p.getSpecification().toString());
     }
 
     @Test()
     public void PrintLinux() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.TEST_RESOURCE_PATH + "litmus/C-rcu-link-after.litmus"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         assertNotNull(p.getSpecification().toString());
     }
 
     @Test()
     public void PrintLinux2() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.LITMUS_RESOURCE_PATH + "litmus/LKMM/dart/C-atomic-fetch-simple-01.litmus"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         assertNotNull(p.getSpecification().toString());
     }
 
     @Test()
     public void PrintLinux3() throws Exception {
         Program p = new ProgramParser().parse(new File(ResourceHelper.LITMUS_RESOURCE_PATH + "litmus/LKMM/manual/atomic/C-atomic-01.litmus"));
-        assertNotNull(new Printer().print(p));
+        assertNotNull(new Printer().print(p, Printer.Mode.ALL));
         assertNotNull(p.getSpecification().toString());
     }