From f7adec3dce9984e3502957f3a83e328787988c60 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 2 Jun 2026 14:30:07 +0100 Subject: [PATCH 1/2] Add -a/--all flag to show all SMT verification conditions --- .../java/liquidjava/api/CommandLineArgs.java | 3 + .../java/liquidjava/diagnostics/DebugLog.java | 62 ++++++++++++++++--- .../refinement_checker/VCChecker.java | 2 +- .../java/liquidjava/smt/SMTEvaluator.java | 5 +- 4 files changed, 62 insertions(+), 10 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineArgs.java index 8fd36e37..bda830b6 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 = "Show every verification condition sent to the SMT solver") + public boolean showAllVCs; + @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 0adcccd6..4bfb2102 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -37,12 +37,56 @@ public static boolean enabled() { return CommandLineLauncher.cmdArgs.debugMode; } + /** + * Gate for the SMT-query trace (verification conditions fed to Z3 and their outcomes). Enabled by either + * {@code --debug} / {@code -d} or the lighter {@code --all} / {@code -a}, which shows every query without the rest + * of the debug output (e.g. simplification passes). + */ + public static boolean smtEnabled() { + return CommandLineLauncher.cmdArgs.debugMode || CommandLineLauncher.cmdArgs.showAllVCs; + } + + /** + * Set by {@link #smtStart} (the structured / flat VC printers) and consumed by {@link #smtRawQuery}. Lets the + * low-level Z3 boundary trace skip a query that a higher layer already printed in full, so {@code -a} shows every + * query exactly once. Single-threaded: each {@code smtStart} is immediately followed by one {@code solver.check()}. + */ + private static boolean structuredQueryPending = false; + + /** + * Catch-all trace emitted at the actual {@code solver.check()} boundary so {@code -a} / {@code -d} show EVERY query + * sent to Z3 — including those that bypass the structured {@link #smtStart} path (the simplifier's implication + * checks, refinement satisfiability checks, speculative typestate checks). Suppressed for queries a structured + * print already covered, to avoid duplication. + * + * @param sent + * the predicate actually handed to Z3 + * @param result + * the raw Z3 {@code Status} + */ + public static void smtRawQuery(Predicate sent, String result) { + if (!smtEnabled()) { + return; + } + if (structuredQueryPending) { + structuredQueryPending = false; // already shown by the structured print that preceded this check + return; + } + List conjuncts = new ArrayList<>(); + flattenConjunction(sent.getExpression(), conjuncts); + System.out.println(SMT_TAG + " " + Colors.GREY + "query → Z3" + Colors.RESET); + for (Expression c : conjuncts) { + System.out.println(SMT_TAG + " " + c); + } + System.out.println(SMT_TAG + " Result: " + Colors.CYAN + result + Colors.RESET); + } + /** * 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. */ public static void smtVerifying(SourcePosition position) { - if (!enabled() || position == null) { + if (!smtEnabled() || position == null) { return; } String where = position.getFile().getAbsolutePath() + ":" + position.getLine(); @@ -59,9 +103,10 @@ public static void smtVerifying(SourcePosition position) { * points that don't carry the structured per-variable {@link VCImplication} chain (e.g. ExpressionSimplifier). */ public static void smtStart(Predicate premises, Predicate conclusion) { - if (!enabled()) { + if (!smtEnabled()) { return; } + structuredQueryPending = true; List conjuncts = new ArrayList<>(); flattenConjunction(premises.getExpression(), conjuncts); System.out.println(SMT_TAG); @@ -85,9 +130,10 @@ public static void smtStart(VCImplication chain, Predicate conclusion) { * {@code verifySMTSubtypeStates}). */ public static void smtStart(VCImplication chain, Predicate extraPremise, Predicate conclusion) { - if (!enabled()) { + if (!smtEnabled()) { return; } + structuredQueryPending = true; // Pre-compute label widths for column alignment across all printed rows. int labelWidth = 0; for (VCImplication node = chain; node != null; node = node.getNext()) { @@ -362,14 +408,14 @@ private static void flattenConjunction(Expression e, List out) { } public static void smtUnsat() { - if (!enabled()) { + if (!smtEnabled()) { return; } System.out.println(SMT_TAG + " Result: " + Colors.GREEN + "UNSAT (subtype holds)" + Colors.RESET); } public static void smtSat(Object counterexample) { - if (!enabled()) { + if (!smtEnabled()) { return; } String header = SMT_TAG + " Result: " + Colors.RED + "SAT (subtype fails)" + Colors.RESET; @@ -413,7 +459,7 @@ private static String formatCounterexample(Object counterexample) { } public static void smtUnknown() { - if (!enabled()) { + if (!smtEnabled()) { return; } System.out.println(SMT_TAG + " Result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET); @@ -424,7 +470,7 @@ public static void smtUnknown() { * print). {@link liquidjava.smt.SMTResult} doesn't preserve UNKNOWN, so this maps OK → UNSAT and ERROR → SAT. */ public static void smtResult(liquidjava.smt.SMTResult result) { - if (!enabled()) { + if (!smtEnabled()) { return; } if (result.isError()) { @@ -439,7 +485,7 @@ public static void smtResult(liquidjava.smt.SMTResult result) { * still responsible for surfacing the user-facing error. */ public static void smtError(String message) { - if (!enabled()) { + if (!smtEnabled()) { return; } System.out.println(SMT_TAG + " Result: " + Colors.RED + "ERROR" + Colors.RESET + " — " diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 39a155d3..19718323 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -233,7 +233,7 @@ private List filterGhostStatesForVariables(List list, Li * chain in place; safe because {@code joinPredicates} returns a clone. */ private void transformChainForDebug(VCImplication chain, List filtered, String[] s, Factory f) { - if (!DebugLog.enabled()) + if (!DebugLog.smtEnabled()) return; for (VCImplication n = chain; n != null; n = n.getNext()) { if (n.getRefinement() == null) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index c44c9579..c0078aca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -41,6 +41,7 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte Expr e = exp.accept(visitor); Solver solver = tz3.makeSolverForExpression(e); Status result = solver.check(); + DebugLog.smtRawQuery(toVerify, result.toString()); // subRef is not a subtype of supRef if (result.equals(Status.SATISFIABLE)) { @@ -75,7 +76,9 @@ public boolean isUnsatisfiable(Predicate predicate, Context context) throws Exce ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3); Expr e = exp.accept(visitor); Solver solver = tz3.makeSolverForExpression(e); - return solver.check().equals(Status.UNSATISFIABLE); + Status result = solver.check(); + DebugLog.smtRawQuery(predicate, result.toString()); + return result.equals(Status.UNSATISFIABLE); } } catch (Z3Exception e) { throw new Z3Exception(e.getLocalizedMessage()); From f5b880ea0553e020723e45ac3bb2039cab81b8b9 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 2 Jun 2026 16:25:45 +0100 Subject: [PATCH 2/2] clear debug info --- .../src/main/java/liquidjava/diagnostics/DebugLog.java | 6 ++++++ .../src/main/java/liquidjava/smt/SMTEvaluator.java | 2 ++ 2 files changed, 8 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 4bfb2102..983efa9f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -50,9 +50,15 @@ public static boolean smtEnabled() { * Set by {@link #smtStart} (the structured / flat VC printers) and consumed by {@link #smtRawQuery}. Lets the * low-level Z3 boundary trace skip a query that a higher layer already printed in full, so {@code -a} shows every * query exactly once. Single-threaded: each {@code smtStart} is immediately followed by one {@code solver.check()}. + * Callers that may abort a structured check before {@code solver.check()} (e.g. a translation failure) must clear + * the flag via {@link #clearStructuredQueryPending} so suppression cannot leak onto the next, unrelated query. */ private static boolean structuredQueryPending = false; + public static void clearStructuredQueryPending() { + structuredQueryPending = false; + } + /** * Catch-all trace emitted at the actual {@code solver.check()} boundary so {@code -a} / {@code -d} show EVERY query * sent to Z3 — including those that bypass the structured {@link #smtStart} path (the simplifier's implication diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index c0078aca..07f79311 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -65,6 +65,8 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte e.printStackTrace(); } catch (Z3Exception e) { throw new Z3Exception(e.getLocalizedMessage()); + } finally { + DebugLog.clearStructuredQueryPending(); } return SMTResult.ok(); }