diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 3dd2d1cf..0adcccd6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -2,15 +2,12 @@ import java.util.ArrayList; import java.util.List; -import java.util.stream.Collectors; - 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.smt.Counterexample; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.reference.CtTypeReference; @@ -128,14 +125,152 @@ public static void smtStart(VCImplication chain, Predicate extraPremise, Predica /** * 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. + * callers continue using the simplified expression for user-facing diagnostics. Long predicates are split on + * top-level {@code &&} so each conjunct lands on its own line. */ public static void simplification(Expression input, Expression output) { if (!enabled()) { return; } - 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); + printSplitConjunction("Before simplification:", Colors.YELLOW, input); + printSplitConjunction("After simplification: ", Colors.BOLD_YELLOW, output); + } + + private static void printSplitConjunction(String header, String color, Expression exp) { + List conjuncts = new ArrayList<>(); + flattenConjunction(exp, conjuncts); + if (conjuncts.size() <= 1) { + System.out.println(SMP_TAG + " " + header + " " + color + exp + Colors.RESET); + return; + } + System.out.println(SMP_TAG + " " + header); + String joiner = " " + Colors.GREY + "&&" + Colors.RESET; + for (int i = 0; i < conjuncts.size(); i++) { + String suffix = (i < conjuncts.size() - 1) ? joiner : ""; + System.out.println(SMP_TAG + " " + color + conjuncts.get(i) + Colors.RESET + suffix); + } + } + + private static final String PASS_NAME_COLOR = Colors.GOLD; + private static final int PASS_NAME_WIDTH = 28; + private static int simplificationPass; + private static String previousSimplification; + + /** + * Start a simplification log. DebugLog owns the running pass number and the previous expression snapshot because + * both are only needed for debug output. + */ + public static void simplificationStart(Expression input) { + if (!enabled()) { + return; + } + previousSimplification = input.toString(); + simplificationPass = 0; + printSimplificationPass(simplificationPass, "initial expression", previousSimplification); + } + + /** + * One line per simplifier phase. + */ + public static void simplificationPass(String name, Expression result) { + if (!enabled()) { + return; + } + String resultStr = result.toString(); + printSimplificationPass(++simplificationPass, name, previousSimplification, resultStr); + previousSimplification = resultStr; + } + + /** + * Prints {@code (no change)} when the step left the expression unchanged, and otherwise emits a unified-diff-style + * pair (red {@code -} for the previous expression with removed tokens highlighted, green {@code +} for the new one + * with added tokens highlighted), so substitutions inside a long predicate are obvious at a glance. + * + *

+ * {@code previous} is taken as a string rather than an {@link Expression} because the simplifier mutates the AST in + * place: caching an {@code Expression} reference and re-stringifying it after a later pass would yield the + * already-mutated form, masking real changes as "no change". + */ + private static void printSimplificationPass(int pass, String name, String previous, String result) { + if (previous != null && previous.equals(result)) { + System.out.printf("%s pass %02d: %s %s(no change)%s%n", SMP_TAG, pass, paintPassName(name), Colors.GREY, + Colors.RESET); + return; + } + System.out.printf("%s pass %02d: %s%s%s%n", SMP_TAG, pass, PASS_NAME_COLOR, name, Colors.RESET); + if (previous == null) { + System.out.printf("%s %s%n", SMP_TAG, result); + return; + } + String[] diff = wordDiff(previous, result); + System.out.printf("%s %s-%s %s%n", SMP_TAG, Colors.RED, Colors.RESET, diff[0]); + System.out.printf("%s %s+%s %s%n", SMP_TAG, Colors.GREEN, Colors.RESET, diff[1]); + } + + private static void printSimplificationPass(int pass, String name, String result) { + System.out.printf("%s pass %02d: %s%n %s%n", SMP_TAG, pass, paintPassName(name), result); + } + + /** + * Color the pass name without breaking column alignment: pad to {@link #PASS_NAME_WIDTH} first, then wrap only the + * visible characters in {@link #PASS_NAME_COLOR}. The trailing spaces stay uncolored so {@code printf}'s width + * accounting stays correct. + */ + private static String paintPassName(String name) { + int pad = Math.max(0, PASS_NAME_WIDTH - name.length()); + return PASS_NAME_COLOR + name + Colors.RESET + " ".repeat(pad); + } + + /** + * Word-level LCS diff. Returns {@code [previousColored, currentColored]} where tokens that don't appear in the LCS + * are wrapped in red (for the previous string) and green (for the current string). Splitting on a single space is + * intentional — the {@link Expression#toString()} output spaces operators and operands. + */ + private static String[] wordDiff(String previous, String current) { + String[] prev = previous.split(" "); + String[] curr = current.split(" "); + int[][] dp = new int[prev.length + 1][curr.length + 1]; + for (int i = 1; i <= prev.length; i++) { + for (int j = 1; j <= curr.length; j++) { + if (prev[i - 1].equals(curr[j - 1])) { + dp[i][j] = dp[i - 1][j - 1] + 1; + } else { + dp[i][j] = Math.max(dp[i - 1][j], dp[i][j - 1]); + } + } + } + boolean[] prevKept = new boolean[prev.length]; + boolean[] currKept = new boolean[curr.length]; + int i = prev.length; + int j = curr.length; + while (i > 0 && j > 0) { + if (prev[i - 1].equals(curr[j - 1])) { + prevKept[i - 1] = true; + currKept[j - 1] = true; + i--; + j--; + } else if (dp[i - 1][j] >= dp[i][j - 1]) { + i--; + } else { + j--; + } + } + return new String[] { colorizeDiff(prev, prevKept, Colors.RED), colorizeDiff(curr, currKept, Colors.GREEN) }; + } + + private static String colorizeDiff(String[] tokens, boolean[] kept, String color) { + StringBuilder sb = new StringBuilder(); + for (int k = 0; k < tokens.length; k++) { + if (k > 0) { + sb.append(' '); + } + if (kept[k]) { + sb.append(tokens[k]); + } else { + sb.append(color).append(tokens[k]).append(Colors.RESET); + } + } + return sb.toString(); } private static String plainLabel(VCImplication node) { 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 821eddf7..e94d2574 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 @@ -1,5 +1,6 @@ package liquidjava.rj_language.opt; +import liquidjava.diagnostics.DebugLog; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import java.util.Map; @@ -23,10 +24,16 @@ public class ExpressionSimplifier { * expanding aliases Returns a derivation node representing the tree of simplifications applied */ public static ValDerivationNode simplify(Expression exp, Map aliases) { + DebugLog.simplificationStart(exp); ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp); + DebugLog.simplificationPass("fixed-point reached", fixedPoint.getValue()); ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint); + DebugLog.simplificationPass("remove redundant &&", simplified.getValue()); ValDerivationNode unwrapped = unwrapBooleanLiterals(simplified); - return AliasExpansion.expand(unwrapped, aliases); + DebugLog.simplificationPass("unwrap boolean literals", unwrapped.getValue()); + ValDerivationNode expanded = AliasExpansion.expand(unwrapped, aliases); + DebugLog.simplificationPass("expand aliases", expanded.getValue()); + return expanded; } public static ValDerivationNode simplify(Expression exp) { @@ -35,17 +42,15 @@ public static ValDerivationNode simplify(Expression exp) { /** * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the - * expression simplifies to a boolean literal, which means we've simplified too much + * expression simplifies to a boolean literal, which means we've simplified too much. */ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) { - // apply propagation and folding - ValDerivationNode prop = VariablePropagation.propagate(prevExp, current); - ValDerivationNode fold = ExpressionFolding.fold(prop); - ValDerivationNode simplified = simplifyValDerivationNode(fold); + ValDerivationNode simplified = simplifyOnce(current, prevExp); Expression currExp = simplified.getValue(); - // fixed point reached - if (current != null && currExp.equals(current.getValue())) { + // fixed point reached — compare on toString() because propagate/fold/reduce mutate the AST in place, so a + // reference-level .equals() can trivially be true on shared (mutated) nodes + if (current != null && currExp.toString().equals(current.getValue().toString())) { return current; } @@ -58,6 +63,16 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, return simplifyToFixedPoint(simplified, simplified.getValue()); } + private static ValDerivationNode simplifyOnce(ValDerivationNode current, Expression prevExp) { + ValDerivationNode prop = VariablePropagation.propagate(prevExp, current); + DebugLog.simplificationPass("variable propagation", prop.getValue()); + ValDerivationNode fold = ExpressionFolding.fold(prop); + DebugLog.simplificationPass("expression folding", fold.getValue()); + ValDerivationNode simplified = simplifyValDerivationNode(fold); + DebugLog.simplificationPass("remove redundant && (loop)", simplified.getValue()); + return simplified; + } + /** * Recursively simplifies the derivation tree by removing redundant conjuncts */ @@ -84,8 +99,9 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod if (isRedundant(rightSimplified.getValue())) return leftSimplified; - // collapse identical sides (x && x => x) - if (leftSimplified.getValue().equals(rightSimplified.getValue())) { + // collapse identical sides (x && x => x) — toString() avoids false positives when the two sides share a + // mutated AST node and false negatives are harmless (we just keep the conjunction) + if (leftSimplified.getValue().toString().equals(rightSimplified.getValue().toString())) { return leftSimplified; }