Added missing declarations for native compilation

Minor cleanup
Fix in SVCOMPRunner.java which referenced old method

Author: ThomasHaas

dartagnan/pom.xml

@@ -253,6 +253,7 @@
                         </buildArgs>
                         <initializeAtBuildTime>
                             <!-- Every class should also be registered in OptionsInfo and reflect-config.json -->
+                            <className>com.dat3m.dartagnan.verification.TaskSolver</className>
                             <className>com.dat3m.dartagnan.wmm.RelationNameRepository</className>
                             <className>com.dat3m.dartagnan.configuration.OptionNames</className>
                             <className>com.dat3m.dartagnan.wmm.axiom.Acyclicity</className>

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -113,14 +113,15 @@ public static void main(String[] args) throws Exception {
             }
             output.addResult(summary);
         }
-        output.toStdOut(isBatchMode);
+
+        output.toStdOut();
         // Running batch mode results in normal termination independent of the individual results
         System.exit((isBatchMode ? NORMAL_TERMINATION : summary.code()).asInt());
     }
 
     // ----------------------------------------------------------------------------------------------------
 
-    private static void printOptions() {
+    public static void printOptions() {
         OptionInfo.stream().sorted().forEach(System.out::print);
     }
 
@@ -186,16 +187,16 @@ private static List<File> getProgramFiles(Path path) {
         }
     }
 
-    private static WitnessGraph getWitnessGraph(Dartagnan o, boolean isBatchMode) throws IOException {
-        if (!o.runValidator()) {
+    private static WitnessGraph getWitnessGraph(BaseOptions options, boolean isBatchMode) throws IOException {
+        if (!options.runValidator()) {
             return new WitnessGraph();
         }
 
         if (isBatchMode) {
             throw new IllegalArgumentException("Cannot run validator in batch mode.");
         }
-        logger.info("Witness path: {}", o.getWitnessPath());
-        return new ParserWitness().parse(new File(o.getWitnessPath()));
+        logger.info("Witness path: {}", options.getWitnessPath());
+        return new ParserWitness().parse(new File(options.getWitnessPath()));
     }
 
     private static String getWitnessFileName(Program program, Dartagnan o) {

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionInfo.java

@@ -9,6 +9,7 @@
 import com.dat3m.dartagnan.solver.caat4wmm.coreReasoning.CoreReasoner;
 import com.dat3m.dartagnan.utils.options.BaseOptions;
 import com.dat3m.dartagnan.utils.printer.Printer;
+import com.dat3m.dartagnan.verification.TaskSolver;
 import com.dat3m.dartagnan.verification.solving.ModelChecker;
 import com.dat3m.dartagnan.verification.solving.RefinementSolver;
 import com.dat3m.dartagnan.wmm.RelationNameRepository;
@@ -37,6 +38,7 @@ public static Stream<OptionInfo> stream() {
 
     private static Stream<Class<?>> classes() {
         return Stream.of(
+                TaskSolver.class,
                 RelationNameRepository.class,
                 OptionNames.class,
                 Acyclicity.class,

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

@@ -26,18 +26,22 @@ public void addResult(ResultSummary result) {
         results.add(result);
     }
 
-    public void toStdOut(boolean batchMode) {
-        if (batchMode) {
+    public void toStdOut() {
+        if (results.isEmpty()) {
+            return;
+        }
+
+        if (results.size() == 1) {
+            System.out.println(results.get(0));
+        } else {
             System.out.println("================ Configuration ==================");
             System.out.println("cat = " + modelFile);
             System.out.print(config.asPropertiesString()); // it already contains its own \n
             System.out.println("=================================================");
-        }
-        for (ResultSummary r : results) {
-            if (batchMode) {
+            for (ResultSummary r : results) {
                 System.out.println();
+                System.out.println(r);
             }
-            System.out.println(r);
         }
     }
 

dartagnan/src/main/resources/META-INF/native-image/com.dat3m.dartagnan/dartagnan/reflect-config.json

@@ -1,4 +1,9 @@
 [
+    {
+        "name":"com.dat3m.dartagnan.verification.TaskSolver",
+        "allDeclaredFields": true,
+        "queryAllDeclaredMethods": true
+    },
     {
         "name": "com.dat3m.dartagnan.wmm.RelationNameRepository",
         "allDeclaredFields": true,

svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java

@@ -1,5 +1,6 @@
 package com.dat3m.svcomp;
 
+import com.dat3m.dartagnan.Dartagnan;
 import com.dat3m.dartagnan.parsers.witness.ParserWitness;
 import com.dat3m.dartagnan.utils.options.BaseOptions;
 import com.dat3m.dartagnan.witness.graphml.WitnessGraph;
@@ -69,7 +70,7 @@ private void property(String p) {
     public static void main(String[] args) throws Exception {
 
         if(Arrays.asList(args).contains("--help")) {
-            collectOptions();
+            Dartagnan.printOptions();
             return;
         }
 
@@ -98,9 +99,8 @@ public static void main(String[] args) throws Exception {
             return;
         }
 
-        WitnessGraph witness = new WitnessGraph(); 
         if(r.witnessPath != null) {
-            witness = new ParserWitness().parse(new File(r.witnessPath));
+            WitnessGraph witness = new ParserWitness().parse(new File(r.witnessPath));
             if(!fileProgram.getName().equals(Paths.get(witness.getProgram()).getFileName().toString())) {
                 System.out.println("The witness was generated from a different program than " + fileProgram);
                 System.exit(WRONG_WITNESS_FILE.asInt());
@@ -161,9 +161,8 @@ private static boolean isExternalError(int exitCode) {
     }
 
     private static List<String> filterOptions(Configuration config) {
-    	
         List<String> skip = Arrays.asList(PROPERTYPATH, NATIVE);
-    	
+
         return Arrays.stream(config.asPropertiesString().split("\n")).
             filter(p -> skip.stream().noneMatch(s -> s.equals(p.split(" = ")[0]))).
             map(p -> "--" + p.split(" = ")[0] + "=" + p.split(" = ")[1]).