Support for class Constants (#207)

CatarinaGamboa · claude · rcosta358 · web-flow · commit 46f69223e565 · 2026-05-06T19:08:18.000+01:00
We did not support using static final fields from classes in predicates or using the values in Java code. For example, both these cases would not have been possible before, and now are acceptable ```java static void clampInt(@refinement("_ >= Integer.MIN_VALUE && _ <= Integer.MAX_VALUE") int x) { } public static void main(String[] args) { clampInt(0); clampInt(Integer.MAX_VALUE); } ``` - Resolution follows Java scoping rules: fully-qualified name → compilation-unit imports (single + on-demand) → implicit java.lang, with reflection as the source-of-truth. User-defined enums/classes are left untouched for the existing SMT path. - Based on reflection, find the declaration and get the value assigned to it, and add it as a value. --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Ricardo Costa <rcosta.ms358@gmail.com>
diff --git a/CLAUDE.md b/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.
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectImageWriteParamModes.java b/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);
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectSourceStaticFinalInPredicate.java b/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;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStaticFinalCharInPredicate.java b/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);
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStaticFinalConstant.java b/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;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStaticFinalInPredicate.java b/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);
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStaticImportInPredicate.java b/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);
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java b/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
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSourceStaticFinalInPredicate.java b/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;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalCharInPredicate.java b/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
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java b/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
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java b/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
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassImporting.java b/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;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java b/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);
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/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();
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/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);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/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
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java
