Add -a/--all flag to show all SMT verification conditions

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

@@ -22,6 +22,9 @@ public class CommandLineArgs {
     @Option(names = { "-d", "--debug" }, description = "Enable debug mode for more detailed output")
     public boolean debugMode;
 
+    @Option(names = { "-a", "--all" }, description = "Print the full context plus the debug trace (implies -d)")
+    public boolean all;
+
     @Option(names = { "-lsp", "--language-server" }, description = "Enable language server mode for editor support")
     public boolean lspMode;
 

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

@@ -10,6 +10,7 @@
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtElement;
 import spoon.reflect.reference.CtTypeReference;
 
 /**
@@ -29,12 +30,18 @@ public final class DebugLog {
     private static final String SMT_TAG = Colors.BLUE + "[SMT]" + Colors.RESET;
     private static final String SMT_CHECK = Colors.SALMON + "[SMT CHECK]" + Colors.RESET;
     private static final String SMP_TAG = Colors.YELLOW + "[SMP]" + Colors.RESET;
+    private static final String CTX_TAG = Colors.BRIGHT_MAGENTA + "[CTX]" + Colors.RESET;
 
     private DebugLog() {
     }
 
     public static boolean enabled() {
-        return CommandLineLauncher.cmdArgs.debugMode;
+        return CommandLineLauncher.cmdArgs.debugMode || CommandLineLauncher.cmdArgs.all;
+    }
+
+    /** Gate for the full-context dump, driven by the {@code -a} / {@code --all} flag (the verbose tier of debug). */
+    public static boolean contextEnabled() {
+        return CommandLineLauncher.cmdArgs.all;
     }
 
     /**
@@ -445,4 +452,23 @@ public static void smtError(String message) {
         System.out.println(SMT_TAG + " Result: " + Colors.RED + "ERROR" + Colors.RESET + " — "
                 + (message == null ? "(no message)" : message));
     }
+
+    public static void contextAtElement(CtElement element, String contextInfo) {
+        if (!contextEnabled()) {
+            return;
+        }
+        SourcePosition position = element.getPosition();
+        String header;
+        if (position != null && position.getFile() != null) {
+            // file:line so terminals make it ⌘/Ctrl-clickable (same form as smtVerifying), plus the source line itself.
+            String where = position.getFile().getAbsolutePath() + ":" + position.getLine();
+            String code = Utils.getExpressionFromPosition(position);
+            header = CTX_TAG + " Context at " + Colors.CYAN + where + Colors.RESET
+                    + (code != null ? "  \n" + Colors.BOLD_YELLOW + code + Colors.RESET : ":");
+        } else {
+            header = CTX_TAG + " Context at " + position + ":";
+        }
+        System.out.println(header);
+        System.out.println(contextInfo);
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java

@@ -6,6 +6,7 @@
 import java.util.Set;
 
 import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
@@ -45,7 +46,7 @@ public void clearHistory() {
     }
 
     public void saveContext(CtElement element, Context context) {
-        if (!CommandLineLauncher.cmdArgs.lspMode)
+        if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.all)
             return;
 
         String file = Utils.getFile(element);
@@ -64,6 +65,9 @@ public void saveContext(CtElement element, Context context) {
         ghosts.addAll(context.getGhostStates());
         aliases.addAll(context.getAliases());
         methods.addAll(context.getCtxFunctions());
+
+        // Gate lives inside DebugLog.contextAtElement (-a / --all); no-op unless that flag is set.
+        DebugLog.contextAtElement(element, prettyPrint());
     }
 
     private String getScopePosition(CtElement element) {
@@ -96,4 +100,26 @@ public Set<RefinedFunction> getMethods() {
     public Map<String, Set<String>> getFileScopes() {
         return fileScopes;
     }
+
+    public String prettyPrint() {
+        StringBuilder sb = new StringBuilder("ContextHistory:\n");
+
+        // FileScopes are intentionally omitted here — they drive LSP hover ranges (see getFileScopes), not debug
+        // output.
+        appendSection(sb, "LocalVars", localVars);
+        appendSection(sb, "GlobalVars", globalVars);
+        appendSection(sb, "Ghosts", ghosts);
+        appendSection(sb, "Aliases", aliases);
+        appendSection(sb, "Methods", methods);
+
+        return sb.toString();
+    }
+
+    private static void appendSection(StringBuilder sb, String label, Iterable<?> items) {
+        sb.append(label).append(":\n");
+        for (Object item : items) {
+            sb.append("  - ").append(item).append("\n");
+        }
+    }
+
 }

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

@@ -5,6 +5,7 @@
 import java.util.List;
 import java.util.Optional;
 
+import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.processor.context.*;
@@ -48,6 +49,7 @@
 import spoon.reflect.code.CtVariableRead;
 import spoon.reflect.declaration.*;
 import spoon.reflect.factory.Factory;
+import spoon.reflect.path.CtRole;
 import spoon.reflect.reference.CtFieldReference;
 import spoon.reflect.reference.CtTypeReference;
 import spoon.reflect.reference.CtVariableReference;
@@ -72,6 +74,21 @@ public RefinementTypeChecker(Context context, Factory factory) {
 
     // --------------------- Visitors -----------------------------------
 
+    /**
+     * Under {@code -a} / {@code --all}, dump the context after every top-level statement. {@code super.scan} runs the
+     * full {@code visitCtXxx} override first, so the statement's refinement effect is already applied to the context by
+     * the time we save it. The {@code STATEMENT} role filter keeps this to actual statements (direct block / case
+     * children), skipping sub-expressions like the {@code g(x)} in {@code f(g(x))}.
+     */
+    @Override
+    public void scan(CtElement element) {
+        super.scan(element);
+        if (DebugLog.contextEnabled() && element instanceof CtStatement
+                && element.getRoleInParent() == CtRole.STATEMENT) {
+            contextHistory.saveContext(element, context);
+        }
+    }
+
     @Override
     public <T> void visitCtClass(CtClass<T> ctClass) {
         // System.out.println("CTCLASS:"+ctClass.getSimpleName());

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

@@ -1,8 +1,8 @@
 package liquidjava.utils;
 
+import java.nio.file.Files;
 import java.util.List;
 import java.util.Map;
-import java.util.Scanner;
 import java.util.Set;
 import java.util.stream.Stream;
 
@@ -110,21 +110,41 @@ public static SourcePosition getRealPosition(CtElement element) {
         return element.getPosition();
     }
 
+    /**
+     * The source text of the element at {@code position}. The first line is taken from the element's column (leading
+     * indentation / preceding tokens dropped); a statement that wraps across lines has its continuation lines appended
+     * (joined with a space) until a line ends in a statement terminator ({@code ;}, {@code {} or {@code }}) or the
+     * element's end line is reached. The terminator stop keeps multi-line statements whole while halting block-bodied
+     * elements (methods, ifs, loops) at their opening brace instead of swallowing the whole body. Single-line elements
+     * read exactly one line, unchanged.
+     */
     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++;
+        try {
+            List<String> lines = Files.readAllLines(position.getFile().toPath());
+            StringBuilder sb = new StringBuilder();
+            for (int n = position.getLine(); n <= position.getEndLine() && n <= lines.size(); n++) {
+                // First line starts at the element's column; continuation lines are taken whole.
+                String piece = (n == position.getLine() ? lines.get(n - 1).substring(position.getColumn() - 2)
+                        : lines.get(n - 1)).trim();
+                if (sb.length() > 0)
+                    sb.append(' ');
+                sb.append(piece);
+                if (endsStatement(piece))
+                    break;
             }
+            return sb.length() == 0 ? null : sb.toString();
         } catch (Exception e) {
-            // ignore
+            return null; // unreadable file / out-of-range column → no snippet
         }
-        return null;
+    }
+
+    /**
+     * A trimmed source line ends a statement / opens a block when its last char is {@code ;}, <code>{</code> or
+     * <code>}</code> — used to bound multi-line snippet extraction.
+     */
+    private static boolean endsStatement(String trimmedLine) {
+        return !trimmedLine.isEmpty() && "{};".indexOf(trimmedLine.charAt(trimmedLine.length() - 1)) >= 0;
     }
 }