Support for class Constants

CLAUDE.md

@@ -0,0 +1,77 @@
+# CLAUDE.md
+
+This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
+
+## Project Overview
+
+LiquidJava is an additional type checker for Java that adds **liquid types** (refinements) and **typestates** on top of standard Java. Users annotate Java code with `@Refinement`, `@StateRefinement`, `@StateSet` etc. (from `liquidjava-api`); the verifier parses the program with [Spoon](https://spoon.gforge.inria.fr/), translates refinement predicates to SMT, and discharges verification conditions with **Z3**.
+
+Requires **Java 20+** and **Maven 3.6+** (the parent POM declares 1.8 source/target, but the verifier module overrides to 20).
+
+## Module Layout
+
+This is a Maven multi-module build (`pom.xml` is the umbrella):
+
+- `liquidjava-api` — published annotations (`@Refinement`, `@RefinementAlias`, `@StateRefinement`, `@StateSet`, ghost functions). Stable artifact users depend on.
+- `liquidjava-verifier` — the actual checker (Spoon processor + RJ AST + SMT translator). Published as `io.github.liquid-java:liquidjava-verifier`.
+- `liquidjava-example` — sample programs **and the test suite** under `src/main/java/testSuite/`. The verifier's tests scan this directory.
+
+Verifier package map (`liquidjava-verifier/src/main/java/liquidjava/`):
+- `api/` — entrypoints; `CommandLineLauncher` is the CLI main.
+- `processor/` — Spoon processors. `RefinementProcessor` orchestrates; `refinement_checker/` contains `RefinementTypeChecker`, `MethodsFirstChecker`, `ExternalRefinementTypeChecker`, plus `general_checkers/` and `object_checkers/` for typestate.
+- `ast/` — AST of the Refinements Language (RJ).
+- `rj_language/` — parser from refinement strings to RJ AST.
+- `smt/` — Z3 translation (`TranslatorToZ3`, `ExpressionToZ3Visitor`, `SMTEvaluator`, `Counterexample`).
+- `errors/`, `utils/`, `diagnostics/`.
+
+## Commands
+
+Build / install everything:
+```bash
+mvn clean install
+```
+
+Run the test suite (verifier module, runs whole `testSuite/` dir):
+```bash
+mvn test
+```
+
+Run a single test method (JUnit 4/5 mix — both work via Surefire):
+```bash
+mvn -pl liquidjava-verifier -Dtest=TestExamples test
+mvn -pl liquidjava-verifier -Dtest=TestExamples#testMultiplePaths test
+```
+
+Verify a specific file/directory from CLI (uses the `liquidjava` script in repo root, macOS/Linux):
+```bash
+./liquidjava liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java
+```
+Equivalent raw form:
+```bash
+mvn exec:java -pl liquidjava-verifier \
+  -Dexec.mainClass="liquidjava.api.CommandLineLauncher" \
+  -Dexec.args="/path/to/file_or_dir"
+```
+
+Code formatting runs automatically in the `validate` phase via `formatter-maven-plugin` (configured for Java 20 in `liquidjava-verifier/pom.xml`); no separate lint command.
+
+## Test Suite Conventions
+
+Tests are discovered by `TestExamples#testPath` (parameterized) under `liquidjava-example/src/main/java/testSuite/`:
+
+- Single-file cases: filename starts with `Correct…` or `Error…`.
+- Directory cases: directory name contains the substring `correct` or `error`.
+- Anything else is **ignored** (so helper sources can live alongside).
+- Expected error for a failing case:
+  - Single file: write the expected error title in a comment on the **first line** of the file.
+  - Directory: place a `.expected` file in that directory containing the expected error title.
+
+When adding new test cases, place them under `liquidjava-example/src/main/java/testSuite/` following the naming rules above — that is the only way they get picked up.
+
+## Architecture Notes That Span Files
+
+- **Two-pass typechecking.** `MethodsFirstChecker` collects method signatures and refinement contracts before `RefinementTypeChecker` walks bodies, so forward references and recursion resolve. Edits to one usually need a matching change in the other.
+- **Refinement string → AST → Z3.** A `@Refinement("a > 0")` string flows: `rj_language` parser → `ast` nodes → `smt/TranslatorToZ3` / `ExpressionToZ3Visitor`. New predicate forms generally require touching all three.
+- **External refinements.** `ExternalRefinementTypeChecker` plus `*Refinements.java` companion files specify contracts for third-party APIs without modifying their sources. The `co-specifying-liquidjava` skill covers this workflow.
+- **Typestate** lives in `processor/refinement_checker/object_checkers/` and uses `@StateRefinement` / `@StateSet` from the API. Ghost-state predicates flow through the same SMT pipeline as value refinements.
+- **Z3 dependency.** The verifier shells out to Z3 via JNI bindings; failures often surface as `SMTResult` errors or counterexamples, not Java exceptions.

liquidjava-example/src/main/java/testSuite/CorrectImageWriteParamModes.java

@@ -0,0 +1,25 @@
+package testSuite;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectImageWriteParamModes {
+
+    static void requireExplicit(
+            @Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) {
+    }
+
+    static void requireKnownMode(
+            @Refinement("_ == ImageWriteParam.MODE_DISABLED || _ == ImageWriteParam.MODE_DEFAULT "
+                    + "|| _ == ImageWriteParam.MODE_EXPLICIT || _ == ImageWriteParam.MODE_COPY_FROM_METADATA") int mode) {
+    }
+
+    public static void main(String[] args) {
+        requireExplicit(ImageWriteParam.MODE_EXPLICIT);
+        requireKnownMode(ImageWriteParam.MODE_DEFAULT);
+        requireKnownMode(ImageWriteParam.MODE_DISABLED);
+        requireKnownMode(2);
+    }
+}

liquidjava-example/src/main/java/testSuite/CorrectSourceStaticFinalInPredicate.java

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectSourceStaticFinalInPredicate {
+
+    static void requireBelowLimit(@Refinement("_ < LIMITS.MAX") double x) {
+    }
+
+    public static void main(String[] args) {
+        requireBelowLimit(5.0);
+    }
+
+    static class LIMITS {
+        static final double MAX = 10.0;
+    }
+}

liquidjava-example/src/main/java/testSuite/CorrectStaticFinalCharInPredicate.java

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectStaticFinalCharInPredicate {
+
+    static void requireMaxChar(@Refinement("_ == Character.MAX_VALUE") char c) {
+    }
+
+    public static void main(String[] args) {
+        requireMaxChar(Character.MAX_VALUE);
+    }
+}

liquidjava-example/src/main/java/testSuite/CorrectStaticFinalConstant.java

@@ -0,0 +1,27 @@
+package testSuite;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectStaticFinalConstant {
+
+    static void requirePositive(@Refinement("_ > 0") int x) {
+    }
+
+    static void requireAtLeast(@Refinement("_ >= 1024") int x) {
+    }
+
+    public static void main(String[] args) {
+        // Reflective resolution of a JDK static final int constant.
+        requirePositive(Integer.MAX_VALUE);
+
+        // Reflective resolution of a JDK static final int with a known concrete value.
+        requireAtLeast(Short.MAX_VALUE);
+    }
+
+    void other(){
+        @Refinement("_ > 0 && _ <= 1") int x = ImageWriteParam.MODE_DEFAULT;
+    }
+}

liquidjava-example/src/main/java/testSuite/CorrectStaticFinalInPredicate.java

@@ -0,0 +1,25 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectStaticFinalInPredicate {
+
+    // Constants resolved inside the predicate string itself.
+    static void clampInt(@Refinement("_ >= Integer.MIN_VALUE && _ <= Integer.MAX_VALUE") int x) {
+    }
+
+    static void belowMaxLong(@Refinement("_ <= Long.MAX_VALUE") long x) {
+    }
+
+    static void notMaxByte(@Refinement("_ != Byte.MAX_VALUE") int x) {
+    }
+
+    public static void main(String[] args) {
+        clampInt(0);
+        clampInt(Integer.MAX_VALUE);
+        clampInt(Integer.MIN_VALUE);
+        belowMaxLong(123L);
+        notMaxByte(0);
+    }
+}

liquidjava-example/src/main/java/testSuite/CorrectStaticImportInPredicate.java

@@ -0,0 +1,26 @@
+package testSuite;
+
+import static java.lang.Math.PI;
+
+import liquidjava.specification.Refinement;
+
+/**
+ * Locks in that the import walk ignores {@code import static} (kind {@code FIELD}) without confusing the resolver:
+ * the file has a static import for an unrelated symbol, and a refinement that uses a regular {@code Type.CONST}
+ * reference. The verifier must skip the static import and resolve {@code Math.PI} via the implicit {@code java.lang}
+ * fallback (or the static-import target's class — either path is correct here).
+ */
+@SuppressWarnings("unused")
+public class CorrectStaticImportInPredicate {
+
+    static double useUnused() {
+        return PI;
+    }
+
+    static void requireBelowFour(@Refinement("_ < 4.0") double x) {
+    }
+
+    public static void main(String[] args) {
+        requireBelowFour(Math.PI);
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java

@@ -0,0 +1,17 @@
+package testSuite;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorImageWriteParamModes {
+
+    static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) {
+    }
+
+    public static void main(String[] args) {
+        // MODE_DEFAULT is 1, not 2 (MODE_EXPLICIT).
+        requireExplicit(ImageWriteParam.MODE_DEFAULT); // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorSourceStaticFinalInPredicate.java

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorSourceStaticFinalInPredicate {
+
+    static void requireBelowLimit(@Refinement("_ < LIMITS.MAX") double x) {
+    }
+
+    public static void main(String[] args) {
+        requireBelowLimit(15.0); // Refinement Error
+    }
+
+    static class LIMITS {
+        static final double MAX = 10.0;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStaticFinalCharInPredicate.java

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorStaticFinalCharInPredicate {
+
+    static void requireMaxChar(@Refinement("_ == Character.MAX_VALUE") char c) {
+    }
+
+    public static void main(String[] args) {
+        requireMaxChar('\''); // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorStaticFinalConstant {
+
+    static void requirePositive(@Refinement("_ > 0") int x) {
+    }
+
+    public static void main(String[] args) {
+        requirePositive(Integer.MIN_VALUE); // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorStaticFinalInPredicate {
+
+    static void belowMaxByte(@Refinement("_ <= Byte.MAX_VALUE") int x) {
+    }
+
+    public static void main(String[] args) {
+        // Byte.MAX_VALUE == 127, so 200 violates the bound.
+        belowMaxByte(200); // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassImporting.java

@@ -0,0 +1,10 @@
+package testSuite.classes.missing_import_final_error;
+
+import javax.imageio.ImageWriteParam;
+
+/** Sibling file that imports the class so the verifier knows where to find it. */
+public class ClassImporting {
+    public static int explicit() {
+        return ImageWriteParam.MODE_EXPLICIT;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java

@@ -0,0 +1,16 @@
+package testSuite.classes.missing_import_final_error;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ClassNoImport {
+
+    // No import for javax.imageio.ImageWriteParam in this file — the verifier
+    // should suggest it because Helper.java already imports it.
+    static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) { // Not Found Error
+    }
+
+    public static void main(String[] args) {
+        requireExplicit(2);
+    }
+}

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

@@ -14,6 +14,7 @@ public class LJDiagnostic extends RuntimeException {
     private final String customMessage;
     private String file;
     private SourcePosition position;
+    private String hint;
     private static final String PIPE = " | ";
 
     public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
@@ -38,7 +39,7 @@ public String getCustomMessage() {
     }
 
     public String getDetails() {
-        return ""; // to be overridden by subclasses
+        return hint != null ? hint : "";
     }
 
     public SourcePosition getPosition() {
@@ -60,6 +61,10 @@ public String getAccentColor() {
         return accentColor;
     }
 
+    public void setHint(String hint) {
+        this.hint = hint;
+    }
+
     @Override
     public String toString() {
         StringBuilder sb = new StringBuilder();

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

@@ -18,6 +18,10 @@ public NotFoundError(String name, String kind) {
         this(null, name, kind, null);
     }
 
+    public NotFoundError(SourcePosition position, String name, String kind) {
+        this(position, name, kind, null);
+    }
+
     public NotFoundError(SourcePosition position, String name, String kind, TranslationTable translationTable) {
         super("Not Found Error", String.format("%s '%s' not found", kind, name), position, translationTable);
         this.name = Utils.getSimpleName(name);

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

@@ -46,6 +46,10 @@ public String getCounterExampleString() {
 
         List<String> foundVarNames = new ArrayList<>();
         found.getValue().getVariableNames(foundVarNames);
+        // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
+        // subtyping check, so the counterexample maps the symbolic name back to its compile-time value
+        found.getValue().getResolvedConstantNames(foundVarNames);
+        expected.getValue().getResolvedConstantNames(foundVarNames);
         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