diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java index 7b72d190..50aa3ae8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java @@ -4,6 +4,28 @@ public class Colors { public static final String RESET = "\u001B[0m"; public static final String GREY = "\u001B[90m"; + public static final String RED = "\u001B[31m"; + public static final String GREEN = "\u001B[32m"; + public static final String YELLOW = "\u001B[33m"; + public static final String BLUE = "\u001B[34m"; + public static final String CYAN = "\u001B[36m"; public static final String BOLD_RED = "\u001B[1;31m"; public static final String BOLD_YELLOW = "\u001B[1;33m"; -} \ No newline at end of file + public static final String ORANGE = "\u001B[38;5;208m"; + public static final String PINK = "\u001B[38;5;205m"; + public static final String CORAL = "\u001B[38;5;203m"; + public static final String SALMON = "\u001B[38;5;209m"; + public static final String GOLD = "\u001B[38;5;220m"; + public static final String BRIGHT_YELLOW = "\u001B[38;5;226m"; + public static final String LIME = "\u001B[38;5;118m"; + public static final String BRIGHT_GREEN = "\u001B[38;5;46m"; + public static final String TEAL = "\u001B[38;5;37m"; + public static final String LIGHT_BLUE = "\u001B[38;5;39m"; + public static final String BRIGHT_CYAN = "\u001B[38;5;51m"; + public static final String PURPLE = "\u001B[38;5;129m"; + public static final String BRIGHT_MAGENTA = "\u001B[38;5;201m"; + public static final String BROWN = "\u001B[38;5;94m"; + public static final String NAVY = "\u001B[38;5;17m"; + public static final String LIGHT_GREY = "\u001B[38;5;250m"; + public static final String DARK_GREY = "\u001B[38;5;240m"; +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java new file mode 100644 index 00000000..2b2ee5a3 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -0,0 +1,298 @@ +package liquidjava.diagnostics; + +import java.util.ArrayList; +import java.util.List; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.processor.VCImplication; +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.reference.CtTypeReference; + +/** + * Centralised debug-mode logging for verification activity. Output is gated on the global {@code --debug} / {@code -d} + * flag and is purely informational. + * + *

+ * Layers of output, from outermost to innermost: + *

+ */ +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 DebugLog() { + } + + public static boolean enabled() { + return CommandLineLauncher.cmdArgs.debugMode; + } + + /** + * 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) { + return; + } + String where = position.getFile().getAbsolutePath() + ":" + position.getLine(); + String exp = Utils.getExpressionFromPosition(position); + System.out.println(SMT_CHECK); + System.out.println(SMT_TAG + " Verifying " + Colors.CYAN + where + Colors.RESET + + (exp != null ? " on '" + exp + "'" : "")); + } + + private static final String SEPARATOR = Colors.GREY + " ────────────────────────────────────────" + Colors.RESET; + + /** + * Flat-predicate fallback: prints top-level conjuncts in order with no per-variable grouping. Used by SMT entry + * 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()) { + return; + } + List conjuncts = new ArrayList<>(); + flattenConjunction(premises.getExpression(), conjuncts); + System.out.println(SMT_TAG); + for (Expression c : conjuncts) { + System.out.println(SMT_TAG + " " + c); + } + System.out.println(SMT_TAG + SEPARATOR); + System.out.println(SMT_TAG + " " + formatConclusion(conclusion)); + } + + /** + * Structured form: walks the {@link VCImplication} chain produced by {@code joinPredicates}, printing one line per + * refined variable with all of its refinements together. + */ + public static void smtStart(VCImplication chain, Predicate conclusion) { + smtStart(chain, null, conclusion); + } + + /** + * Structured form with an extra unattributed premise (e.g. the "found" type appended in + * {@code verifySMTSubtypeStates}). + */ + public static void smtStart(VCImplication chain, Predicate extraPremise, Predicate conclusion) { + if (!enabled()) { + return; + } + // Pre-compute label widths for column alignment across all printed rows. + int labelWidth = 0; + for (VCImplication node = chain; node != null; node = node.getNext()) { + if (node.getName() == null && node.getType() == null) { + continue; + } + labelWidth = Math.max(labelWidth, plainLabel(node).length()); + } + if (extraPremise != null && !extraPremise.isBooleanTrue()) { + labelWidth = Math.max(labelWidth, "found".length()); + } + + System.out.println(SMT_TAG + " "); + List printedRefinements = new ArrayList<>(); + for (VCImplication node = chain; node != null; node = node.getNext()) { + if (node.getName() == null && node.getType() == null) { + continue; // skip the empty trailing tail node + } + String refinement = formatRefinement(node.getRefinement()); + printedRefinements.add(refinement); + System.out.println(SMT_TAG + " " + paintLabel(node, labelWidth) + " " + refinement); + } + if (extraPremise != null && !extraPremise.isBooleanTrue()) { + String extra = formatRefinement(extraPremise); + // Skip when the appended "found" type is identical to a premise we just printed + // (common in verifySMTSubtypeStates when `type` IS the variable's current refinement). + if (!printedRefinements.contains(extra)) { + String label = Colors.GREY + padRight("found", labelWidth) + Colors.RESET; + System.out.println(SMT_TAG + " " + label + " " + extra); + } + } + System.out.println(SMT_TAG + SEPARATOR); + System.out.println(SMT_TAG + " " + formatConclusion(conclusion)); + } + + private static String plainLabel(VCImplication node) { + return node.getName() + " : " + simpleType(node.getType()); + } + + private static String paintLabel(VCImplication node, int width) { + String name = node.getName(); + String type = simpleType(node.getType()); + String padded = padRight(name + " : " + type, width); + // Color only the name; keep alignment by computing padding on the plain string. + String coloredName = Colors.CYAN + name + Colors.RESET; + String coloredType = Colors.GREY + type + Colors.RESET; + String tail = padded.substring((name + " : " + type).length()); // padding spaces + return coloredName + Colors.GREY + " : " + Colors.RESET + coloredType + tail; + } + + private static String simpleType(CtTypeReference type) { + if (type == null) { + return "?"; + } + String qual = type.getQualifiedName(); + return qual.contains(".") ? Utils.getSimpleName(qual) : qual; + } + + private static String padRight(String s, int width) { + if (s.length() >= width) { + return s; + } + StringBuilder sb = new StringBuilder(s); + for (int i = s.length(); i < width; i++) { + sb.append(' '); + } + return sb.toString(); + } + + /** + * Render a refinement so multi-conjunct predicates are unambiguous on a single line: each top-level conjunct is + * wrapped in parens and joined with ∧. + */ + private static String formatRefinement(Predicate p) { + List conjuncts = new ArrayList<>(); + flattenConjunction(p.getExpression(), conjuncts); + if (conjuncts.size() <= 1) { + return p.toString(); + } + StringBuilder sb = new StringBuilder(); + for (int i = 0; i < conjuncts.size(); i++) { + if (i > 0) { + sb.append(Colors.GREY).append(" ∧ ").append(Colors.RESET); + } + sb.append('(').append(conjuncts.get(i)).append(')'); + } + return sb.toString(); + } + + /** + * Conclusion needs its own painter: nesting {@link #formatRefinement} (which already emits ANSI {@code RESET} + * around its operators) inside an outer color would clear the outer color after the first inner reset, leaving the + * tail of the line uncoloured. Paint each conjunct individually instead. + */ + private static String formatConclusion(Predicate p) { + List conjuncts = new ArrayList<>(); + flattenConjunction(p.getExpression(), conjuncts); + if (conjuncts.size() <= 1) { + return Colors.BOLD_YELLOW + p + Colors.RESET; + } + StringBuilder sb = new StringBuilder(); + for (int i = 0; i < conjuncts.size(); i++) { + if (i > 0) { + sb.append(Colors.GREY).append(" ∧ ").append(Colors.RESET); + } + sb.append(Colors.BOLD_YELLOW).append('(').append(conjuncts.get(i)).append(')').append(Colors.RESET); + } + return sb.toString(); + } + + private static void flattenConjunction(Expression e, List out) { + if (e instanceof GroupExpression g) { + flattenConjunction(g.getExpression(), out); + return; + } + if (e instanceof BinaryExpression b && "&&".equals(b.getOperator())) { + flattenConjunction(b.getFirstOperand(), out); + flattenConjunction(b.getSecondOperand(), out); + return; + } + out.add(e); + } + + public static void smtUnsat() { + if (!enabled()) { + return; + } + System.out.println(SMT_TAG + " result: " + Colors.GREEN + "UNSAT (subtype holds)" + Colors.RESET); + } + + public static void smtSat(Object counterexample) { + if (!enabled()) { + return; + } + String header = SMT_TAG + " result: " + Colors.RED + "SAT (subtype fails)" + Colors.RESET; + String pretty = formatCounterexample(counterexample); + if (pretty == null) { + System.out.println(header); + } else if (pretty.contains("\n")) { + System.out.println(header + Colors.GREY + " — counterexample:" + Colors.RESET); + System.out.println(pretty); + } else { + System.out.println(header + Colors.GREY + " — counterexample: " + Colors.RESET + pretty); + } + } + + /** + * Render a {@link liquidjava.smt.Counterexample} as {@code lhs = value} pairs. Single assignment goes inline; + * multiple assignments are listed one per indented line. Returns {@code null} when there is nothing useful to show + * — caller prints just the SAT header. + */ + private static String formatCounterexample(Object counterexample) { + if (!(counterexample instanceof liquidjava.smt.Counterexample ce)) { + return counterexample == null ? null : counterexample.toString(); + } + var pairs = ce.assignments(); + if (pairs == null || pairs.isEmpty()) { + return null; + } + if (pairs.size() == 1) { + var p = pairs.get(0); + return p.first() + " = " + p.second(); + } + StringBuilder sb = new StringBuilder(); + for (int i = 0; i < pairs.size(); i++) { + var p = pairs.get(i); + if (i > 0) { + sb.append('\n'); + } + sb.append(SMT_TAG).append(" ").append(p.first()).append(" = ").append(p.second()); + } + return sb.toString(); + } + + public static void smtUnknown() { + if (!enabled()) { + return; + } + System.out.println(SMT_TAG + " result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET); + } + + /** + * Print the result of an SMT check whose {@code smtStart} was emitted by the caller (e.g. VCChecker's structured + * 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()) { + return; + } + if (result.isError()) { + smtSat(result.getCounterexample()); + } else { + smtUnsat(); + } + } + + /** + * Print an SMT-side failure (e.g. Z3 sort mismatch) so the trace doesn't end with a dangling header. Caller is + * still responsible for surfacing the user-facing error. + */ + public static void smtError(String message) { + if (!enabled()) { + return; + } + System.out.println(SMT_TAG + " result: " + Colors.RED + "ERROR" + Colors.RESET + " — " + + (message == null ? "(no message)" : message)); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 152488a8..a5b44f1d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -27,6 +27,26 @@ public void setNext(VCImplication c) { next = c; } + public String getName() { + return name; + } + + public CtTypeReference getType() { + return type; + } + + public Predicate getRefinement() { + return refinement; + } + + public void setRefinement(Predicate refinement) { + this.refinement = refinement; + } + + public VCImplication getNext() { + return next; + } + public String toString() { if (name != null && type != null) { String qualType = type.getQualifiedName(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 20c1e7af..57cf8b0b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -373,8 +373,13 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen } public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { + return checkStateSMT(prevState, expectedState, p, false); + } + + public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent) + throws LJError { SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, - factory); + factory, silent); return result.isOk(); } 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 80014606..1e88bebb 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 @@ -10,7 +10,7 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.*; -import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; @@ -52,13 +52,15 @@ public void processSubtyping(Predicate expectedType, List list, CtEl TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; - Predicate premisesBeforeChange = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); + VCImplication impl = joinPredicates(expectedType, mainVars, lrv, map); + Predicate premisesBeforeChange = impl.toConjunctions(); Predicate premises; Predicate expected; try { List filtered = filterGhostStatesForVariables(list, mainVars, lrv); premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); + transformChainForDebug(impl, filtered, s, f); } catch (LJError e) { // add location info to error if (e.getPosition() == null) { @@ -68,7 +70,16 @@ public void processSubtyping(Predicate expectedType, List list, CtEl throw e; } SourcePosition annotationValuePos = Utils.getFirstLJAnnotationValuePosition(element); - SMTResult result = verifySMTSubtype(expected, premises, annotationValuePos); + DebugLog.smtVerifying(annotationValuePos); + DebugLog.smtStart(impl, expected); + SMTResult result; + try { + result = dischargeToSMT(expected, premises, annotationValuePos, true); + } catch (RuntimeException ex) { + DebugLog.smtError(ex.getMessage()); + throw ex; + } + DebugLog.smtResult(result); if (result.isError()) { throw new RefinementError(element.getPosition(), expectedType.simplify(context), premisesBeforeChange.simplify(context), map, result.getCounterexample(), customMessage); @@ -103,14 +114,14 @@ public void processSubtyping(Predicate type, Predicate expectedType, List states, SourcePosition position, Factory factory) throws LJError { + return verifySMTSubtypeStates(type, expectedType, states, position, factory, false); + } + + public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, List states, + SourcePosition position, Factory factory, boolean silent) throws LJError { + if (!silent) { + DebugLog.smtVerifying(position); + } List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); @@ -142,15 +161,33 @@ public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; - Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); + VCImplication impl = joinPredicates(expectedType, mainVars, lrv, map); + Predicate premisesJoined = impl.toConjunctions(); List filtered = filterGhostStatesForVariables(states, mainVars, lrv); - premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s) + Predicate premises = Predicate.createConjunction(premisesJoined, type).changeStatesToRefinements(filtered, s) .changeAliasToRefinement(context, factory); Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, factory); + if (!silent) { + transformChainForDebug(impl, filtered, s, factory); + Predicate foundExtra = type.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, + factory); + DebugLog.smtStart(impl, foundExtra, expected); + } - // check subtyping - return verifySMTSubtype(expected, premises, position); + SMTResult result; + try { + result = dischargeToSMT(expected, premises, position, true); + } catch (RuntimeException ex) { + if (!silent) { + DebugLog.smtError(ex.getMessage()); + } + throw ex; + } + if (!silent) { + DebugLog.smtResult(result); + } + return result; } /** @@ -190,6 +227,26 @@ private List filterGhostStatesForVariables(List list, Li return filtered.isEmpty() ? list : filtered; } + /** + * Apply the same {@code changeStatesToRefinements} / {@code changeAliasToRefinement} pipeline to each node of a + * {@link VCImplication} chain so the structured debug print mirrors the predicates Z3 actually sees. Mutates the + * chain in place; safe because {@code joinPredicates} returns a clone. + */ + private void transformChainForDebug(VCImplication chain, List filtered, String[] s, Factory f) { + if (!DebugLog.enabled()) + return; + for (VCImplication n = chain; n != null; n = n.getNext()) { + if (n.getRefinement() == null) + continue; + try { + n.setRefinement( + n.getRefinement().changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f)); + } catch (LJError ignored) { + // best-effort transformation for debug; leave node as-is on failure + } + } + } + private VCImplication joinPredicates(Predicate expectedType, List mainVars, List vars, TranslationTable map) { @@ -350,4 +407,5 @@ private TranslationTable createMap(Predicate expectedType) { joinPredicates(expectedType, mainVars, lrv, map); return map; } + } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index c47994da..d8402d48 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -220,7 +220,7 @@ private static Predicate createStatePredicate(String value, String targetClass, Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p; Predicate c = c1.substituteVariable(Keys.THIS, name); c = c.changeOldMentions(nameOld, name); - boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition()); + boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition(), true); if (ok) { SourcePosition pos = Utils.getLJAnnotationPosition(e, value); tc.throwStateConflictError(pos, p); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 07a8432f..821eddf7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -212,7 +212,7 @@ private static ValDerivationNode unwrapBooleanLiterals(ValDerivationNode node) { private static boolean implies(Expression stronger, Expression weaker) { try { SMTResult result = new SMTEvaluator().verifySubtype(new Predicate(stronger), new Predicate(weaker), - Context.getInstance()); + Context.getInstance(), true); return result.isOk(); } catch (Exception e) { return false; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 10f1bae2..c44c9579 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -7,6 +7,7 @@ import com.microsoft.z3.Status; import com.microsoft.z3.Z3Exception; +import liquidjava.diagnostics.DebugLog; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; @@ -16,14 +17,22 @@ public class SMTEvaluator { /** * Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser * for our SMT-ready refinement language and discharges the verification to Z3 - * + * * @param subRef * @param supRef * @param context - * + * * @return the result of the verification, containing a counterexample if the verification fails */ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception { + return verifySubtype(subRef, supRef, context, false); + } + + public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context, boolean silent) + throws Exception { + if (!silent) { + DebugLog.smtStart(subRef, supRef); + } Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate()); try { Expression exp = toVerify.getExpression(); @@ -37,8 +46,18 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte if (result.equals(Status.SATISFIABLE)) { Model model = solver.getModel(); Counterexample counterexample = tz3.getCounterexample(model); + if (!silent) { + DebugLog.smtSat(counterexample); + } return SMTResult.error(counterexample); } + if (!silent) { + if (result.equals(Status.UNKNOWN)) { + DebugLog.smtUnknown(); + } else { + DebugLog.smtUnsat(); + } + } } } catch (SyntaxException e) { System.out.println("Could not parse: " + toVerify);