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/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/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) { // Error
+    }
+
+    public static void main(String[] args) {
+        requireExplicit(2);
+    }
+}

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

@@ -46,7 +46,10 @@ public String getCounterExampleString() {
 
         List<String> foundVarNames = new ArrayList<>();
         found.getValue().getVariableNames(foundVarNames);
-        List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
+        // 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);
         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())

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -13,6 +13,7 @@
 import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
 import liquidjava.rj_language.BuiltinFunctionPredicate;
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.StaticConstants;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
@@ -274,13 +275,24 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
             String enumLiteral = String.format(Formats.ENUM, target, fieldName);
             fieldRead.putMetadata(Keys.REFINEMENT,
                     Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral)));
+        } else if (tryStaticFinalConstantRefinement(fieldRead)) {
+            // refinement metadata set by helper
         } else {
             fieldRead.putMetadata(Keys.REFINEMENT, new Predicate());
             // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE?
         }
         super.visitCtFieldRead(fieldRead);
     }
 
+    /** Resolve a {@code static final} primitive/String constant to {@code #wild == <literal>}. */
+    private <T> boolean tryStaticFinalConstantRefinement(CtFieldRead<T> fieldRead) {
+        Predicate literal = StaticConstants.asLiteralPredicate(StaticConstants.resolve(fieldRead.getVariable()));
+        if (literal == null)
+            return false;
+        fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), literal));
+        return true;
+    }
+
     @Override
     public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
         super.visitCtVariableRead(variableRead);

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -14,6 +14,7 @@
 import liquidjava.processor.context.GhostState;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Enum;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.GroupExpression;
@@ -25,6 +26,7 @@
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.utils.StaticConstants;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.rj_language.opt.ExpressionSimplifier;
 import liquidjava.rj_language.parsing.RefinementsParser;
@@ -75,9 +77,55 @@ public Predicate(String ref, CtElement element, String prefix) throws LJError {
         if (!(exp instanceof GroupExpression)) {
             exp = new GroupExpression(exp);
         }
+        exp = resolveStaticFinalConstants(exp, element);
     }
 
-    /** Create a predicate with the expression true */
+    /**
+     * Walks {@code root}, decorating {@link Enum} nodes that resolve (via reflection, java.lang fallback, or imports
+     * declared in {@code context}'s compilation unit) to a {@code static final} primitive/String constant with the
+     * corresponding literal expression via {@link Enum#setResolvedLiteral}. The AST shape is preserved, so error
+     * messages and counterexamples can render the symbolic {@code Type.CONST} form; the SMT translator emits the
+     * literal binding axiom from the decoration. User-defined enums and unresolvable-but-known-type references are left
+     * untouched (the SMT side handles them as user enum constants).
+     */
+    private static Expression resolveStaticFinalConstants(Expression root, CtElement context) throws LJError {
+        List<Enum> enums = new ArrayList<>();
+        collectEnums(root, enums);
+        for (Enum en : enums) {
+            Object v = StaticConstants.resolve(en.getTypeName(), en.getConstName(), context);
+            Predicate lit = StaticConstants.asLiteralPredicate(v);
+            if (lit != null) {
+                en.setResolvedLiteral(lit.getExpression());
+                continue;
+            }
+            if (StaticConstants.userTypeExists(en.getTypeName(), context))
+                continue; // likely a user-defined enum/class — let SMT translation handle it
+            // unresolvable reference — throw an error with a helpful message and import suggestion if possible
+            SourcePosition pos = context == null ? null : Utils.getLJAnnotationPosition(context, en.toString());
+            String suggested = StaticConstants.findImportCandidate(en.getTypeName(), en.getConstName(), context);
+            String hint = suggested != null ? "add: import " + suggested + ";"
+                    : "add an import for '" + en.getTypeName() + "' if it is a Java class with a static final field.";
+            throw new liquidjava.diagnostics.errors.CustomError(
+                    String.format("Could not resolve '%s.%s' in refinement. If you meant the static final constant, %s",
+                            en.getTypeName(), en.getConstName(), hint),
+                    pos);
+        }
+        return root;
+    }
+
+    private static void collectEnums(Expression e, List<Enum> out) {
+        if (e instanceof Enum en)
+            out.add(en);
+        for (Expression c : e.getChildren())
+            collectEnums(c, out);
+    }
+
+    /**
+     * Wrap an already-built expression in a {@link Predicate}. Unlike the string-parsing constructors, this does NOT
+     * run static-final-constant resolution. Callers are responsible for ensuring {@code e} contains no
+     * {@link liquidjava.rj_language.ast.Enum Enum} nodes that should be resolved to literals; in practice this is fine
+     * for AST clones and rewrites that started life from the string constructor.
+     */
     public Predicate(Expression e) {
         exp = e;
     }