Merge branch 'main' into fix-has-usage

Author: rcosta358

CONTRIBUTING.md

@@ -23,6 +23,8 @@ To verify a single file from the CLI, run:
 ./liquidjava path/to/File.java
 ```
 
+This script recompiles `liquidjava-api` and `liquidjava-verifier` when local sources or Maven files have changed.
+
 ## Testing
 
 To run all tests, run:

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/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,13 +2,15 @@
 
 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;
@@ -29,6 +31,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 +126,18 @@ 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.
+     */
+    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);
+    }
+
     private static String plainLabel(VCImplication node) {
         return node.getName() + " : " + simpleType(node.getType());
     }
@@ -215,14 +230,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 +281,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 +307,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/processor/context/ContextHistory.java

@@ -5,6 +5,7 @@
 import java.util.Map;
 import java.util.Set;
 
+import liquidjava.api.CommandLineLauncher;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
@@ -44,6 +45,9 @@ public void clearHistory() {
     }
 
     public void saveContext(CtElement element, Context context) {
+        if (!CommandLineLauncher.cmdArgs.lspMode)
+            return;
+
         String file = Utils.getFile(element);
         if (file == null)
             return;

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;
@@ -257,11 +257,10 @@ public ValDerivationNode simplify(Context context) {
         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);
+        ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases);
+        DebugLog.simplification(this.getExpression(), result.getValue());
+        return result;
     }
 
     private static boolean isBooleanLiteral(Expression expr, boolean value) {