From a684f45bb2f679e71da613b80354be5f3e2c473f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 9 Jun 2026 14:55:24 +0100 Subject: [PATCH 1/3] Change flag to dump context info --- .../java/liquidjava/api/CommandLineArgs.java | 3 ++ .../java/liquidjava/diagnostics/DebugLog.java | 36 +++++++++++++++++++ .../processor/context/ContextHistory.java | 29 ++++++++++++++- .../RefinementTypeChecker.java | 17 +++++++++ .../src/main/java/liquidjava/utils/Utils.java | 34 ++++++++++++++++-- 5 files changed, 116 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java index 8fd36e37a..a47489808 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-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; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 0adcccd60..3d0270c9e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/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); + + } } 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..b1a4f840e 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,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 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..44b663b5b 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-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 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..dabf64793 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/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 ;}, { or + * } — 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 == '}'; + } } From baefe3d4ada87bfcaacd330e29099ef44fd56a85 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 13 Jun 2026 19:13:58 +0200 Subject: [PATCH 2/3] Flag all shows both context and the debug info --- .../java/liquidjava/api/CommandLineArgs.java | 4 ++-- .../java/liquidjava/diagnostics/DebugLog.java | 16 +++------------- .../processor/context/ContextHistory.java | 5 ++--- .../RefinementTypeChecker.java | 8 ++++---- 4 files changed, 11 insertions(+), 22 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java index a47489808..70960d4fa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java @@ -22,8 +22,8 @@ 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 = { "-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 3d0270c9e..466b3d9b6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -4,8 +4,6 @@ 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; @@ -38,12 +36,12 @@ 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-context} flag (independent of debug). */ + /** 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.printContext; + return CommandLineLauncher.cmdArgs.all; } /** @@ -473,12 +471,4 @@ public static void contextAtElement(CtElement element, String contextInfo) { System.out.println(header); System.out.println(contextInfo); } - - public static void log(String string) { - if (!enabled()) { - return; - } - System.out.println(string); - - } } 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 b1a4f840e..0b3127660 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -46,8 +46,7 @@ public void clearHistory() { } public void saveContext(CtElement element, Context context) { - if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.debugMode - && !CommandLineLauncher.cmdArgs.printContext) + if (!CommandLineLauncher.cmdArgs.lspMode && !CommandLineLauncher.cmdArgs.all) return; String file = Utils.getFile(element); @@ -67,7 +66,7 @@ public void saveContext(CtElement element, Context context) { aliases.addAll(context.getAliases()); methods.addAll(context.getCtxFunctions()); - // Gate lives inside DebugLog.contextAtElement (-a / --all-context); no-op unless that flag is set. + // Gate lives inside DebugLog.contextAtElement (-a / --all); no-op unless that flag is set. DebugLog.contextAtElement(element, prettyPrint()); } 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 44b663b5b..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 @@ -75,10 +75,10 @@ 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))}. + * 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) { From e593f79856460e26fef6a9647d5d23d96e953748 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 13 Jun 2026 21:55:54 +0200 Subject: [PATCH 3/3] less changes in utils --- .../src/main/java/liquidjava/utils/Utils.java | 38 +++++++------------ 1 file changed, 14 insertions(+), 24 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index dabf64793..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; @@ -121,30 +121,23 @@ public static SourcePosition getRealPosition(CtElement element) { 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())) { + try { + List lines = Files.readAllLines(position.getFile().toPath()); StringBuilder sb = new StringBuilder(); - int currentLine = 1; - while (scanner.hasNextLine()) { - String line = scanner.nextLine(); - 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++; + 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; } /** @@ -152,9 +145,6 @@ public static String getExpressionFromPosition(SourcePosition position) { * } — 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 == '}'; + return !trimmedLine.isEmpty() && "{};".indexOf(trimmedLine.charAt(trimmedLine.length() - 1)) >= 0; } }