Modified CLI

Added picocli to extend flag usage, with the implementation of --debug to presentraw expressions, counterexamples and all expressions sent to the SMT solver.
Logging should be improved as it's not incredibly readable.

Author: cheestree

liquidjava-verifier/pom.xml

@@ -316,6 +316,11 @@
 			<version>2.10.1</version>
 		</dependency>
 
+		<dependency>
+			<groupId>info.picocli</groupId>
+			<artifactId>picocli</artifactId>
+			<version>4.7.7</version>
+		</dependency>
 	</dependencies>
 	<dependencyManagement>
 		<dependencies>

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

@@ -3,12 +3,17 @@
 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;
@@ -22,25 +27,43 @@ public class CommandLineLauncher {
     private static final ContextHistory contextHistory = ContextHistory.getInstance();
 
     public static void main(String[] args) {
-        if (args.length == 0) {
-            System.out.println("No input paths provided");
-            System.out.println("\nUsage: ./liquidjava <...paths>");
-            System.out.println("  <...paths>: Paths to be verified by LiquidJava");
-            System.out.println(
-                    "\nExample: ./liquidjava liquidjava-example/src/main/java/test liquidjava-example/src/main/java/testingInProgress/Account.java");
-            return;
+        CommandLine commandLine = new CommandLine(new CliArguments());
+        int exitCode = commandLine.execute(args);
+        if (exitCode != 0) {
+            System.exit(exitCode);
         }
-        List<String> paths = Arrays.asList(args);
-        launch(paths.toArray(new String[0]));
+    }
+
+    @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();
+            }
+
+            launch(paths.stream().toArray(String[]::new));
+
+            // print diagnostics
+            if (diagnostics.foundWarning()) {
+                System.out.println(diagnostics.getWarningOutput());
+            }
+            if (diagnostics.foundError()) {
+                System.out.println(diagnostics.getErrorOutput());
+                return 1;
+            }
 
-        // print diagnostics
-        if (diagnostics.foundWarning()) {
-            System.out.println(diagnostics.getWarningOutput());
-        }
-        if (diagnostics.foundError()) {
-            System.out.println(diagnostics.getErrorOutput());
-        } else {
             System.out.println("Correct! Passed Verification.");
+            return 0;
         }
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java

@@ -15,10 +15,12 @@ public class Diagnostics {
 
     private final LinkedHashSet<LJError> errors;
     private final LinkedHashSet<LJWarning> warnings;
+    private boolean debugMode;
 
     private Diagnostics() {
         this.errors = new LinkedHashSet<>();
         this.warnings = new LinkedHashSet<>();
+        this.debugMode = false;
     }
 
     public static Diagnostics getInstance() {
@@ -33,6 +35,14 @@ public void add(LJWarning warning) {
         this.warnings.add(warning);
     }
 
+    public boolean isDebugMode() {
+        return this.debugMode;
+    }
+
+    public void setDebugMode() {
+        this.debugMode = true;
+    }
+
     public boolean foundError() {
         return !this.errors.isEmpty();
     }

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

@@ -1,5 +1,6 @@
 package liquidjava.rj_language.opt;
 
+import liquidjava.diagnostics.Diagnostics;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.LiteralBoolean;
@@ -9,13 +10,19 @@
 
 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);
-        return simplifyValDerivationNode(fixedPoint);
+        ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint);
+        if (diagnostics.isDebugMode()) {
+            System.out.println("Simplified expression: original: " + exp + " | simplified: " + simplified.getValue());
+        }
+        return simplified;
     }
 
     /**

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

@@ -9,12 +9,15 @@
 import com.microsoft.z3.Status;
 import com.microsoft.z3.Z3Exception;
 
+import liquidjava.diagnostics.Diagnostics;
 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
@@ -27,6 +30,9 @@ 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);
+        }
         try {
             Expression exp = toVerify.getExpression();
             try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
@@ -39,6 +45,10 @@ 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);
                 }
             }