diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java index 8fd36e37a..70960d4fa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java +++ b/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; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 0adcccd60..466b3d9b6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/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); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 6b9af7879..0b3127660 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/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 getMethods() { public Map> 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"); + } + } + } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 5cc2a09d6..00736a0db 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/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 void visitCtClass(CtClass ctClass) { // System.out.println("CTCLASS:"+ctClass.getSimpleName()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 5a65cf615..9b429c10a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/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 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 ;}, { or + * } — used to bound multi-line snippet extraction. + */ + private static boolean endsStatement(String trimmedLine) { + return !trimmedLine.isEmpty() && "{};".indexOf(trimmedLine.charAt(trimmedLine.length() - 1)) >= 0; } }