From a23cf065618080298fff7dae3a7e298f4816e72e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 14 May 2026 14:44:16 +0100 Subject: [PATCH 1/5] Unsimplified Expression Debug Log --- .../src/main/java/liquidjava/diagnostics/DebugLog.java | 7 +++++++ .../src/main/java/liquidjava/rj_language/Predicate.java | 7 +++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 2b2ee5a3..371c06a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -123,6 +123,13 @@ public static void smtStart(VCImplication chain, Predicate extraPremise, Predica System.out.println(SMT_TAG + " " + formatConclusion(conclusion)); } + public static void simplificationInput(Predicate predicate) { + if (!enabled()) { + return; + } + System.out.println(SMT_TAG + " unsimplified: " + predicate); + } + private static String plainLabel(VCImplication node) { return node.getName() + " : " + simpleType(node.getType()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 70ae8ede..da7b32b5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -6,7 +6,7 @@ import java.util.Map; import java.util.stream.Collectors; -import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; @@ -252,14 +252,13 @@ public Expression getExpression() { } public ValDerivationNode simplify(Context context) { + DebugLog.simplificationInput(this); + // collect aliases from context Map aliases = new HashMap<>(); for (AliasWrapper aw : context.getAliases()) { aliases.put(aw.getName(), aw.createAliasDTO()); } - if (CommandLineLauncher.cmdArgs.debugMode) { - return new ValDerivationNode(exp.clone(), null); - } // simplify expression return ExpressionSimplifier.simplify(exp.clone(), aliases); } From d7a437c34e95a720fb8d9cdf608bb0fea4301691 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 14 May 2026 14:53:41 +0100 Subject: [PATCH 2/5] Counterexample Debug Log --- .../main/java/liquidjava/diagnostics/DebugLog.java | 11 +++++++++++ .../diagnostics/errors/RefinementError.java | 8 +++++--- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 371c06a7..c055ce53 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -9,6 +9,7 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.smt.Counterexample; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.reference.CtTypeReference; @@ -130,6 +131,16 @@ public static void simplificationInput(Predicate predicate) { System.out.println(SMT_TAG + " unsimplified: " + predicate); } + public static void counterexampleAssignments(Counterexample counterexample) { + if (!enabled() || counterexample == null || counterexample.assignments().isEmpty()) { + return; + } + System.out.println(SMT_TAG + " counterexample assignments:"); + for (var assignment : counterexample.assignments()) { + System.out.println(SMT_TAG + " " + assignment.first() + " = " + assignment.second()); + } + } + private static String plainLabel(VCImplication node) { return node.getName() + " : " + simpleType(node.getType()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 1bd39ab1..32d3f061 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -4,7 +4,7 @@ import java.util.List; import java.util.stream.Collectors; -import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; @@ -44,6 +44,8 @@ public String getCounterExampleString() { if (counterexample == null || counterexample.assignments().isEmpty()) return null; + DebugLog.counterexampleAssignments(counterexample); + List foundVarNames = new ArrayList<>(); found.getValue().getVariableNames(foundVarNames); // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the @@ -53,8 +55,8 @@ public String getCounterExampleString() { List foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList(); String counterexampleString = counterexample.assignments().stream() // only include variables that appear in the found value and are not already fixed there - .filter(a -> CommandLineLauncher.cmdArgs.debugMode || (foundVarNames.contains(a.first()) - && !foundAssignments.contains(a.first() + " == " + a.second()))) + .filter(a -> foundVarNames.contains(a.first()) + && !foundAssignments.contains(a.first() + " == " + a.second())) // format as "var == value" .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) // join with "&&" From f39fff2795bb04ebdd02e1dcd08543db62cc7902 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 14 May 2026 14:55:32 +0100 Subject: [PATCH 3/5] Minor Change --- .../src/main/java/liquidjava/diagnostics/DebugLog.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index c055ce53..a97c916a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -135,7 +135,7 @@ public static void counterexampleAssignments(Counterexample counterexample) { if (!enabled() || counterexample == null || counterexample.assignments().isEmpty()) { return; } - System.out.println(SMT_TAG + " counterexample assignments:"); + System.out.println(SMT_TAG + " unfiltered counterexample assignments:"); for (var assignment : counterexample.assignments()) { System.out.println(SMT_TAG + " " + assignment.first() + " = " + assignment.second()); } From c23424f018ccdcf54d059d1129c5f8515b0984d6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 14 May 2026 16:17:39 +0100 Subject: [PATCH 4/5] Requested Changes --- .../java/liquidjava/diagnostics/DebugLog.java | 35 +++++++++++++------ .../diagnostics/errors/RefinementError.java | 2 +- .../liquidjava/rj_language/Predicate.java | 6 ++-- 3 files changed, 28 insertions(+), 15 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index a97c916a..16c1f013 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -2,6 +2,7 @@ import java.util.ArrayList; import java.util.List; +import java.util.stream.Collectors; import liquidjava.api.CommandLineLauncher; import liquidjava.processor.VCImplication; @@ -9,6 +10,7 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.smt.Counterexample; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; @@ -30,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 DebugLog() { } @@ -124,21 +127,31 @@ public static void smtStart(VCImplication chain, Predicate extraPremise, Predica System.out.println(SMT_TAG + " " + formatConclusion(conclusion)); } - public static void simplificationInput(Predicate predicate) { + /** + * Print the simplifier input and output side by side. This keeps the raw expression visible in debug traces while + * callers continue using the simplified expression for user-facing diagnostics. + */ + public static void simplification(Expression input, Expression output) { if (!enabled()) { return; } - System.out.println(SMT_TAG + " unsimplified: " + predicate); + System.out.println(SMP_TAG + " Simplified " + Colors.CYAN + input + Colors.RESET + " to " + Colors.YELLOW + + output + Colors.RESET); } - public static void counterexampleAssignments(Counterexample counterexample) { + /** + * Print every assignment returned by the solver before error reporting filters the user-facing counterexample down + * to the variables mentioned in the diagnostic. + */ + public static void counterexample(Counterexample counterexample) { if (!enabled() || counterexample == null || counterexample.assignments().isEmpty()) { return; } - System.out.println(SMT_TAG + " unfiltered counterexample assignments:"); - for (var assignment : counterexample.assignments()) { - System.out.println(SMT_TAG + " " + assignment.first() + " = " + assignment.second()); - } + System.out + .println(SMP_TAG + + " Counterexample: " + Colors.RED + counterexample.assignments().stream() + .map(a -> a.first() + " = " + a.second()).collect(Collectors.joining(" && ")) + + Colors.RESET); } private static String plainLabel(VCImplication node) { @@ -233,14 +246,14 @@ public static void smtUnsat() { if (!enabled()) { return; } - System.out.println(SMT_TAG + " result: " + Colors.GREEN + "UNSAT (subtype holds)" + Colors.RESET); + 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 header = SMT_TAG + " Result: " + Colors.RED + "SAT (subtype fails)" + Colors.RESET; String pretty = formatCounterexample(counterexample); if (pretty == null) { System.out.println(header); @@ -284,7 +297,7 @@ public static void smtUnknown() { if (!enabled()) { return; } - System.out.println(SMT_TAG + " result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET); + System.out.println(SMT_TAG + " Result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET); } /** @@ -310,7 +323,7 @@ public static void smtError(String message) { if (!enabled()) { return; } - System.out.println(SMT_TAG + " result: " + Colors.RED + "ERROR" + Colors.RESET + " — " + 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/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 32d3f061..2f5fc615 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -44,7 +44,7 @@ public String getCounterExampleString() { if (counterexample == null || counterexample.assignments().isEmpty()) return null; - DebugLog.counterexampleAssignments(counterexample); + DebugLog.counterexample(counterexample); List foundVarNames = new ArrayList<>(); found.getValue().getVariableNames(foundVarNames); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index da7b32b5..64da35b2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -252,15 +252,15 @@ public Expression getExpression() { } public ValDerivationNode simplify(Context context) { - DebugLog.simplificationInput(this); - // collect aliases from context Map aliases = new HashMap<>(); for (AliasWrapper aw : context.getAliases()) { aliases.put(aw.getName(), aw.createAliasDTO()); } // simplify expression - return ExpressionSimplifier.simplify(exp.clone(), aliases); + ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases); + DebugLog.simplification(this.getExpression(), result.getValue()); + return result; } private static boolean isBooleanLiteral(Expression expr, boolean value) { From 51858fa49c1e22569e33d8a9fb56586fcebd1cfc Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 14 May 2026 20:57:17 +0100 Subject: [PATCH 5/5] Requested Change --- .../java/liquidjava/diagnostics/DebugLog.java | 20 ++----------------- .../diagnostics/errors/RefinementError.java | 3 --- 2 files changed, 2 insertions(+), 21 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 16c1f013..3dd2d1cf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -10,7 +10,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.GroupExpression; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.smt.Counterexample; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; @@ -135,23 +134,8 @@ public static void simplification(Expression input, Expression output) { if (!enabled()) { return; } - System.out.println(SMP_TAG + " Simplified " + Colors.CYAN + input + Colors.RESET + " to " + Colors.YELLOW - + output + Colors.RESET); - } - - /** - * Print every assignment returned by the solver before error reporting filters the user-facing counterexample down - * to the variables mentioned in the diagnostic. - */ - public static void counterexample(Counterexample counterexample) { - if (!enabled() || counterexample == null || counterexample.assignments().isEmpty()) { - return; - } - System.out - .println(SMP_TAG - + " Counterexample: " + Colors.RED + counterexample.assignments().stream() - .map(a -> a.first() + " = " + a.second()).collect(Collectors.joining(" && ")) - + Colors.RESET); + System.out.println(SMP_TAG + " Before simplification: " + Colors.YELLOW + input + Colors.RESET); + System.out.println(SMP_TAG + " After simplification: " + Colors.BOLD_YELLOW + output + Colors.RESET); } private static String plainLabel(VCImplication node) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 2f5fc615..3095bb91 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -4,7 +4,6 @@ import java.util.List; import java.util.stream.Collectors; -import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; @@ -44,8 +43,6 @@ public String getCounterExampleString() { if (counterexample == null || counterexample.assignments().isEmpty()) return null; - DebugLog.counterexample(counterexample); - List foundVarNames = new ArrayList<>(); found.getValue().getVariableNames(foundVarNames); // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the