Debug flag

liquidjava-verifier/pom.xml

@@ -319,6 +319,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;
@@ -48,7 +49,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 -> VariableFormatter.formatVariable(a.first()) + " == " + a.second())
                 // join with "&&"

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -10,6 +10,7 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.*;
+import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
@@ -22,6 +23,7 @@
 import liquidjava.smt.SMTResult;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Keys;
+import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.factory.Factory;
@@ -102,6 +104,12 @@ public void processSubtyping(Predicate type, Predicate expectedType, List<GhostS
      */
     public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePosition position) throws LJError {
         try {
+            if (CommandLineLauncher.cmdArgs.debugMode) {
+                String exp = Utils.getExpressionFromPosition(position);
+                System.out.println(String.format("%s <: %s %s at %s", expected, found,
+                        exp != null ? String.format("on expression '%s'", exp) : "",
+                        position.getFile().getName() + ":" + position.getLine()));
+            }
             return new SMTEvaluator().verifySubtype(found, expected, context);
         } catch (LJError e) {
             if (e.getPosition() == null) {

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;
@@ -207,6 +208,9 @@ public ValDerivationNode simplify(Context context) {
         for (AliasWrapper aw : context.getAliases()) {
             aliases.put(aw.getName(), aw.createAliasDTO());
         }
+        if (CommandLineLauncher.cmdArgs.debugMode) {
+            return new ValDerivationNode(exp.clone(), null);
+        }
         // simplify expression
         return ExpressionSimplifier.simplify(exp.clone(), aliases);
     }

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

@@ -1,7 +1,5 @@
 package liquidjava.smt;
 
-import java.util.Set;
-
 import com.martiansoftware.jsap.SyntaxException;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.Model;

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -2,6 +2,7 @@
 
 import java.util.List;
 import java.util.Map;
+import java.util.Scanner;
 import java.util.Set;
 import java.util.stream.Stream;
 
@@ -108,4 +109,22 @@ public static SourcePosition getRealPosition(CtElement element) {
         }
         return element.getPosition();
     }
+
+    public static String getExpressionFromPosition(SourcePosition position) {
+        if (position == null || position.getFile() == null)
+            return null;
+        try (Scanner scanner = new Scanner(position.getFile())) {
+            int currentLine = 1;
+            while (scanner.hasNextLine()) {
+                String line = scanner.nextLine();
+                if (currentLine == position.getLine()) {
+                    return line.substring(position.getColumn() - 2).trim();
+                }
+                currentLine++;
+            }
+        } catch (Exception e) {
+            // ignore
+        }
+        return null;
+    }
 }