get value of final static vars

Author: CatarinaGamboa

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/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/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-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.rj_language.ast.LiteralString;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
@@ -274,13 +275,61 @@ 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) {
+        CtFieldReference<T> ref = fieldRead.getVariable();
+        if (!ref.isStatic() || !ref.isFinal())
+            return false;
+
+        Object value = null;
+        CtField<?> decl = ref.getFieldDeclaration();
+        if (decl != null && decl.getDefaultExpression()instanceof CtLiteral<?> lit)
+            value = lit.getValue();
+        if (value == null) {
+            try {
+                if (ref.getActualField()instanceof java.lang.reflect.Field jf) {
+                    jf.setAccessible(true);
+                    value = jf.get(null);
+                }
+            } catch (Throwable ignored) {
+                // ClassNotFound / IllegalAccess / ExceptionInInitializerError — fall through.
+            }
+        }
+
+        Predicate literal = literalPredicateFor(value);
+        if (literal == null)
+            return false;
+        fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), literal));
+        return true;
+    }
+
+    private static Predicate literalPredicateFor(Object value) {
+        if (value instanceof Boolean)
+            return Predicate.createLit(value.toString(), Types.BOOLEAN);
+        if (value instanceof Integer || value instanceof Short || value instanceof Byte)
+            return Predicate.createLit(value.toString(), Types.INT);
+        if (value instanceof Long)
+            return Predicate.createLit(value.toString(), Types.LONG);
+        if (value instanceof Float)
+            return Predicate.createLit(value.toString(), Types.FLOAT);
+        if (value instanceof Double)
+            return Predicate.createLit(value.toString(), Types.DOUBLE);
+        if (value instanceof Character)
+            return Predicate.createLit("'" + value + "'", Types.CHAR);
+        if (value instanceof String s)
+            return new Predicate(new LiteralString("\"" + s + "\""));
+        return null;
+    }
+
     @Override
     public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
         super.visitCtVariableRead(variableRead);