Split args into a separate file

Arguments are now accessed via an object in the CommandLineLauncher class, so that it's easier in the future to implement new flags.

Author: cheestree

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java

@@ -0,0 +1,20 @@
+package liquidjava.api;
+
+import java.util.List;
+import java.util.concurrent.Callable;
+
+import picocli.CommandLine.Command;
+import picocli.CommandLine.Option;
+import picocli.CommandLine.Parameters;
+
+@Command(name = "liquidjava", mixinStandardHelpOptions = false, customSynopsis = "./liquidjava <...paths> <options>")
+public class CommandLineArgs {
+    @Option(names = {"-h", "--help"}, usageHelp = true, description = "Display this help message")
+    public boolean help;
+
+    @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output")
+    public boolean debugMode;
+
+    @Parameters(arity = "1..*", paramLabel = "<...paths>", description = "Paths to be verified by LiquidJava")
+    public List<String> paths;
+}

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

@@ -2,18 +2,13 @@
 
 import java.io.File;
 import java.util.Arrays;
-import java.util.List;
-import java.util.concurrent.Callable;
 
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.CustomError;
 import liquidjava.diagnostics.warnings.CustomWarning;
 import liquidjava.processor.RefinementProcessor;
 import liquidjava.processor.context.ContextHistory;
 import picocli.CommandLine;
-import picocli.CommandLine.Command;
-import picocli.CommandLine.Option;
-import picocli.CommandLine.Parameters;
 import spoon.Launcher;
 import spoon.compiler.Environment;
 import spoon.processing.ProcessingManager;
@@ -25,46 +20,29 @@ public class CommandLineLauncher {
 
     private static final Diagnostics diagnostics = Diagnostics.getInstance();
     private static final ContextHistory contextHistory = ContextHistory.getInstance();
+    public static final CommandLineArgs cmdArgs = new CommandLineArgs();
 
     public static void main(String[] args) {
-        CommandLine commandLine = new CommandLine(new CliArguments());
-        int exitCode = commandLine.execute(args);
-        if (exitCode != 0) {
-            System.exit(exitCode);
-        }
-    }
-
-    @Command(name = "liquidjava", mixinStandardHelpOptions = true, customSynopsis = "./liquidjava <...paths> <options>")
-    private static class CliArguments implements Callable<Integer> {
-
-        @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output")
-        private boolean debugMode;
-
-        @Parameters(arity = "1..*", paramLabel = "<...paths>", description = "Paths to be verified by LiquidJava")
-        private List<String> paths;
-
-        @Override
-        public Integer call() {
-            if (debugMode) {
-                System.out.println("Debug mode enabled");
-                System.out.println("Input paths: " + paths);
-                diagnostics.setDebugMode();
-            }
+        CommandLine cmd = new CommandLine(cmdArgs);
+        cmd.parseArgs(args);
 
-            launch(paths.stream().toArray(String[]::new));
+        if (cmd.isUsageHelpRequested()) {
+            cmd.usage(System.out);
+            return;
+        }
 
-            // print diagnostics
-            if (diagnostics.foundWarning()) {
-                System.out.println(diagnostics.getWarningOutput());
-            }
-            if (diagnostics.foundError()) {
-                System.out.println(diagnostics.getErrorOutput());
-                return 1;
-            }
+        launch(cmdArgs.paths.stream().toArray(String[]::new));
 
-            System.out.println("Correct! Passed Verification.");
-            return 0;
+        // print diagnostics
+        if (diagnostics.foundWarning()) {
+            System.out.println(diagnostics.getWarningOutput());
+        }
+        if (diagnostics.foundError()) {
+            System.out.println(diagnostics.getErrorOutput());
+            return;
         }
+
+        System.out.println("Correct! Passed Verification.");
     }
 
     public static void launch(String... paths) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -4,6 +4,7 @@
 import java.util.List;
 import java.util.stream.Collectors;
 
+import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.smt.Counterexample;
@@ -45,7 +46,7 @@ public String getCounterExampleString() {
         found.getValue().getVariableNames(foundVarNames);
         String counterexampleString = counterexample.assignments().stream()
                 // only include variables that appear in the found value
-                .filter(a -> foundVarNames.contains(a.first()))
+                .filter(a -> CommandLineLauncher.cmdArgs.debugMode || foundVarNames.contains(a.first()))
                 // format as "var == value"
                 .map(a -> a.first() + " == " + a.second())
                 // join with "&&"

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -6,6 +6,7 @@
 import java.util.Map;
 import java.util.stream.Collectors;
 
+import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
@@ -188,6 +189,9 @@ public Expression getExpression() {
     }
 
     public ValDerivationNode simplify() {
+        if (CommandLineLauncher.cmdArgs.debugMode) {
+            return new ValDerivationNode(exp.clone(), null);
+        }
         return ExpressionSimplifier.simplify(exp.clone());
     }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java

@@ -10,19 +10,13 @@
 
 public class ExpressionSimplifier {
 
-    private static final Diagnostics diagnostics = Diagnostics.getInstance();
-
     /**
      * Simplifies an expression by applying constant propagation, constant folding and removing redundant conjuncts
      * Returns a derivation node representing the tree of simplifications applied
      */
     public static ValDerivationNode simplify(Expression exp) {
         ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp);
-        ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint);
-        if (diagnostics.isDebugMode()) {
-            System.out.println("Simplified expression: original: " + exp + " | simplified: " + simplified.getValue());
-        }
-        return simplified;
+        return simplifyValDerivationNode(fixedPoint);
     }
 
     /**

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -1,23 +1,19 @@
 package liquidjava.smt;
 
-import java.util.Set;
-
 import com.martiansoftware.jsap.SyntaxException;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.Model;
 import com.microsoft.z3.Solver;
 import com.microsoft.z3.Status;
 import com.microsoft.z3.Z3Exception;
 
-import liquidjava.diagnostics.Diagnostics;
+import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 
 public class SMTEvaluator {
 
-    private static final Diagnostics diagnostics = Diagnostics.getInstance();
-
     /**
      * Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser
      * for our SMT-ready refinement language and discharges the verification to Z3
@@ -30,8 +26,8 @@ public class SMTEvaluator {
      */
     public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception {
         Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
-        if (diagnostics.isDebugMode()) {
-            System.out.println("Verifying: " + toVerify);
+        if (CommandLineLauncher.cmdArgs.debugMode) {
+            System.out.println("Verifying: " + subRef + " <: " + supRef);
         }
         try {
             Expression exp = toVerify.getExpression();
@@ -45,10 +41,6 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
                 if (result.equals(Status.SATISFIABLE)) {
                     Model model = solver.getModel();
                     Counterexample counterexample = tz3.getCounterexample(model);
-                    if (diagnostics.isDebugMode()) {
-                        System.out.println("Verification failed. Counterexample:");
-                        System.out.println(counterexample);
-                    }
                     return SMTResult.error(counterexample);
                 }
             }