Merge remote-tracking branch 'origin/main' into derive-states

Author: CatarinaGamboa

CONTRIBUTING.md

@@ -7,26 +7,40 @@ Thanks for your interest in contributing! This guide covers the essentials.
 - Java 20+
 - Maven 3.6+
 
-## Build & test
+## Build and Run
+
+To build the project, run:
 
 ```bash
-mvn clean install   # build everything
-mvn test            # run the test suite
+mvn clean install
 ```
 
-Run a single test:
+Code formatting runs automatically via `formatter-maven-plugin` during the `validate` phase.
+
+To verify a single file from the CLI, run:
 
 ```bash
-mvn -pl liquidjava-verifier -Dtest=TestExamples#testMultiplePaths test
+./liquidjava path/to/File.java
 ```
 
-Verify a single file from the CLI:
+This script recompiles `liquidjava-api` and `liquidjava-verifier` when local sources or Maven files have changed.
+
+## Testing
+
+To run all tests, run:
 
 ```bash
-./liquidjava path/to/File.java
+mvn test
 ```
 
-Code formatting runs automatically via `formatter-maven-plugin` during the `validate` phase.
+To run specific tests, run:
+
+```bash
+mvn -pl liquidjava-verifier -Dtest=ExpressionFormatterTest test
+mvn -pl liquidjava-verifier -Dtest=ExpressionSimplifierTest test
+mvn -pl liquidjava-verifier -Dtest=RefinementsParserTest test
+mvn -pl liquidjava-verifier -Dtest=VariableResolverTest test
+```
 
 ## Release
 

README.md

@@ -83,6 +83,17 @@ mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLi
 ```
 
 If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process.
+The script recompiles the verifier only when local sources or Maven files have changed.
+
+The LiquidJava verifier can be run from the command line with the following options:
+
+| Option | Description |
+| --- | --- |
+| `<...paths>` | Paths (files or directories) to be verified by LiquidJava |
+| `-h`, `--help` | Show the help message with available options |
+| `-v`, `--version` | Show the current version of the verifier |
+| `-d`, `--debug` | Enable debug logging and skip expression simplification for troubleshooting |
+| `-lsp`, `--language-server` | Enable language server mode for editor support |
 
 **Test a correct case**:
 ```bash

liquidjava

@@ -1,4 +1,20 @@
 #!/bin/bash
+set -e
+
+cd "$(dirname "$0")"
+
+MARKER="liquidjava-verifier/target/.liquidjava-last-compile"
+
+if [ ! -d liquidjava-api/target/classes ] || \
+   [ ! -d liquidjava-verifier/target/classes ] || \
+   [ ! -f "$MARKER" ] || \
+   find pom.xml liquidjava-api/pom.xml liquidjava-api/src/main/java \
+     liquidjava-verifier/pom.xml liquidjava-verifier/src/main/java liquidjava-verifier/src/main/antlr4 \
+     -newer "$MARKER" -print -quit | grep -q .; then
+  mvn compile -pl liquidjava-verifier -am -Dmaven.compiler.useIncrementalCompilation=false
+  touch "$MARKER"
+fi
+
 mvn exec:java -pl liquidjava-verifier \
   -Dexec.mainClass="liquidjava.api.CommandLineLauncher" \
   -Dexec.args="$*"

liquidjava-verifier/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.22</version>
+	<version>0.0.25</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

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 = { "-lsp", "--language-server" }, description = "Enable language server mode for editor support")
+    public boolean lspMode;
+
     @Parameters(arity = "1..*", paramLabel = "<...paths>", description = "Paths to be verified by LiquidJava")
     public List<String> paths;
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -2,7 +2,6 @@
 
 import java.util.ArrayList;
 import java.util.List;
-
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
@@ -29,6 +28,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() {
     }
@@ -123,6 +123,156 @@ public static void smtStart(VCImplication chain, Predicate extraPremise, Predica
         System.out.println(SMT_TAG + " " + formatConclusion(conclusion));
     }
 
+    /**
+     * 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. 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;
+        }
+        printSplitConjunction("Before simplification:", Colors.YELLOW, input);
+        printSplitConjunction("After simplification: ", Colors.BOLD_YELLOW, output);
+    }
+
+    private static void printSplitConjunction(String header, String color, Expression exp) {
+        List<Expression> 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.
+     *
+     * <p>
+     * {@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) {
         return node.getName() + " : " + simpleType(node.getType());
     }
@@ -215,14 +365,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);
@@ -266,7 +416,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);
     }
 
     /**
@@ -292,7 +442,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));
     }
 }

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.api.CommandLineLauncher;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
@@ -53,8 +52,8 @@ public String getCounterExampleString() {
         List<String> 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 "&&"

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -1,7 +1,7 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -11,23 +11,23 @@
  */
 public class StateRefinementError extends LJError {
 
-    private final String expected;
-    private final String found;
+    private final ValDerivationNode expected;
+    private final ValDerivationNode found;
 
-    public StateRefinementError(SourcePosition position, Expression expected, Expression found,
+    public StateRefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
             TranslationTable translationTable, String customMessage) {
-        super("State Refinement Error",
-                String.format("Expected state %s but found %s", expected.toDisplayString(), found.toDisplayString()),
-                position, translationTable, customMessage);
-        this.expected = expected.toDisplayString();
-        this.found = found.toDisplayString();
+        super("State Refinement Error", String.format("Expected state %s but found %s",
+                expected.getValue().toDisplayString(), found.getValue().toDisplayString()), position, translationTable,
+                customMessage);
+        this.expected = expected;
+        this.found = found;
     }
 
-    public String getExpected() {
+    public ValDerivationNode getExpected() {
         return expected;
     }
 
-    public String getFound() {
+    public ValDerivationNode getFound() {
         return found;
     }
 }