Debug flag

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/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,13 +2,13 @@
 
 import java.io.File;
 import java.util.Arrays;
-import java.util.List;
 
 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 spoon.Launcher;
 import spoon.compiler.Environment;
 import spoon.processing.ProcessingManager;
@@ -20,28 +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) {
-        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");
+        CommandLine cmd = new CommandLine(cmdArgs);
+        cmd.parseArgs(args);
+
+        if (cmd.isUsageHelpRequested()) {
+            cmd.usage(System.out);
             return;
         }
-        List<String> paths = Arrays.asList(args);
-        launch(paths.toArray(new String[0]));
+
+        launch(cmdArgs.paths.stream().toArray(String[]::new));
 
         // 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;
         }
+
+        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

@@ -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;

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

@@ -1,14 +1,13 @@
 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.api.CommandLineLauncher;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -27,6 +26,9 @@ public class SMTEvaluator {
      */
     public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception {
         Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
+        if (CommandLineLauncher.cmdArgs.debugMode) {
+            System.out.println(String.format("%s <: %s", subRef, supRef));
+        }
         try {
             Expression exp = toVerify.getExpression();
             try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {