Change flag to dump context info

Author: CatarinaGamboa

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-context" }, description = "Print the full context after every checked element")
+    public boolean printContext;
+
     @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

@@ -4,12 +4,15 @@
 import java.util.List;
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.VCImplication;
+import liquidjava.processor.context.Context;
+import liquidjava.processor.context.ContextHistory;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 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,6 +32,7 @@ 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() {
     }
@@ -37,6 +41,11 @@ public static boolean enabled() {
         return CommandLineLauncher.cmdArgs.debugMode;
     }
 
+    /** Gate for the full-context dump, driven by the {@code -a} / {@code --all-context} flag (independent of debug). */
+    public static boolean contextEnabled() {
+        return CommandLineLauncher.cmdArgs.printContext;
+    }
+
     /**
      * One-line header for a verification check: emits the absolute file path + line so terminals (iTerm2, VS Code,
      * WezTerm, …) make it ⌘/Ctrl-clickable. Replaces the older two-line {@code info()} prints.
@@ -445,4 +454,31 @@ 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);
+    }
+
+    public static void log(String string) {
+        if (!enabled()) {
+            return;
+        }
+        System.out.println(string);
+
+    }
 }

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,8 @@ public void clearHistory() {
     }
 
     public void saveContext(CtElement element, Context context) {
-        if (!CommandLineLauncher.cmdArgs.lspMode)
+        if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.debugMode
+                && !CommandLineLauncher.cmdArgs.printContext)
             return;
 
         String file = Utils.getFile(element);
@@ -64,6 +66,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-context); no-op unless that flag is set.
+        DebugLog.contextAtElement(element, prettyPrint());
     }
 
     private String getScopePosition(CtElement element) {
@@ -96,4 +101,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-context}, 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

@@ -110,21 +110,51 @@ 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;
+        int startLine = position.getLine();
+        int endLine = position.getEndLine();
         try (Scanner scanner = new Scanner(position.getFile())) {
+            StringBuilder sb = new StringBuilder();
             int currentLine = 1;
             while (scanner.hasNextLine()) {
                 String line = scanner.nextLine();
-                if (currentLine == position.getLine()) {
-                    return line.substring(position.getColumn() - 2).trim();
+                if (currentLine >= startLine && currentLine <= endLine) {
+                    // First line starts at the element's column; continuation lines are taken whole.
+                    String piece = ((currentLine == startLine) ? line.substring(position.getColumn() - 2) : line)
+                            .trim();
+                    if (sb.length() > 0)
+                        sb.append(' ');
+                    sb.append(piece);
+                    if (currentLine >= endLine || endsStatement(piece))
+                        break;
                 }
                 currentLine++;
             }
+            return sb.length() == 0 ? null : sb.toString();
         } catch (Exception e) {
             // ignore
         }
         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) {
+        if (trimmedLine.isEmpty())
+            return false;
+        char last = trimmedLine.charAt(trimmedLine.length() - 1);
+        return last == ';' || last == '{' || last == '}';
+    }
 }