From 13693c50b21ed01ea16ea5ff4d076647b7dc3668 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 1 May 2026 22:09:35 +0100 Subject: [PATCH 1/6] get value of final static vars --- CLAUDE.md | 77 +++++++++++++++++++ .../testSuite/CorrectStaticFinalConstant.java | 27 +++++++ .../testSuite/ErrorStaticFinalConstant.java | 14 ++++ .../RefinementTypeChecker.java | 49 ++++++++++++ 4 files changed, 167 insertions(+) create mode 100644 CLAUDE.md create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStaticFinalConstant.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 00000000..156c04b3 --- /dev/null +++ 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/CorrectStaticFinalConstant.java b/liquidjava-example/src/main/java/testSuite/CorrectStaticFinalConstant.java new file mode 100644 index 00000000..903f771e --- /dev/null +++ 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/ErrorStaticFinalConstant.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstant.java new file mode 100644 index 00000000..b954e34e --- /dev/null +++ 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-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 82988819..fe31a98f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/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,6 +275,8 @@ public void visitCtFieldRead(CtFieldRead 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? @@ -281,6 +284,52 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { super.visitCtFieldRead(fieldRead); } + /** Resolve a {@code static final} primitive/String constant to {@code #wild == }. */ + private boolean tryStaticFinalConstantRefinement(CtFieldRead fieldRead) { + CtFieldReference 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 void visitCtVariableRead(CtVariableRead variableRead) { super.visitCtVariableRead(variableRead); From 7e17ba48e84219dd838effd17825f2c9477e2fcf Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 1 May 2026 22:39:45 +0100 Subject: [PATCH 2/6] Resolve static final constants inside refinement predicates Predicates can now use static final primitive/String constants like Integer.MAX_VALUE or javax.imageio.ImageWriteParam.MODE_DEFAULT directly inside @Refinement strings. Resolution honors the surrounding source file's imports (single-type and on-demand). When resolution fails but the reference matches a class in a common JDK package, the verifier suggests the missing import in the error message. Refactors the previous Java-side field-read resolution into a single StaticConstants utility shared by both paths. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../CorrectImageWriteParamModes.java | 25 ++++ .../CorrectStaticFinalInPredicate.java | 25 ++++ .../testSuite/ErrorImageWriteParamModes.java | 17 +++ .../ErrorMissingImportInPredicate.java | 15 +++ .../ErrorStaticFinalInPredicate.java | 15 +++ .../RefinementTypeChecker.java | 41 +----- .../liquidjava/rj_language/Predicate.java | 38 ++++++ .../liquidjava/utils/StaticConstants.java | 119 ++++++++++++++++++ 8 files changed, 256 insertions(+), 39 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectImageWriteParamModes.java create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStaticFinalInPredicate.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorMissingImportInPredicate.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectImageWriteParamModes.java b/liquidjava-example/src/main/java/testSuite/CorrectImageWriteParamModes.java new file mode 100644 index 00000000..021f12fd --- /dev/null +++ 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/CorrectStaticFinalInPredicate.java b/liquidjava-example/src/main/java/testSuite/CorrectStaticFinalInPredicate.java new file mode 100644 index 00000000..06dffd9b --- /dev/null +++ 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/ErrorImageWriteParamModes.java b/liquidjava-example/src/main/java/testSuite/ErrorImageWriteParamModes.java new file mode 100644 index 00000000..aecfff10 --- /dev/null +++ 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/ErrorMissingImportInPredicate.java b/liquidjava-example/src/main/java/testSuite/ErrorMissingImportInPredicate.java new file mode 100644 index 00000000..6b33a84e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorMissingImportInPredicate.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorMissingImportInPredicate { + + // No import for javax.imageio.ImageWriteParam — the verifier should suggest the import. + static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) { // Error + } + + public static void main(String[] args) { + requireExplicit(2); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInPredicate.java new file mode 100644 index 00000000..2e271b32 --- /dev/null +++ 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-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index fe31a98f..e15b44a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -13,7 +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.StaticConstants; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Types; @@ -286,50 +286,13 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { /** Resolve a {@code static final} primitive/String constant to {@code #wild == }. */ private boolean tryStaticFinalConstantRefinement(CtFieldRead fieldRead) { - CtFieldReference 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); + 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; } - 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 void visitCtVariableRead(CtVariableRead variableRead) { super.visitCtVariableRead(variableRead); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index be70b652..473ec119 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/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,6 +77,42 @@ public Predicate(String ref, CtElement element, String prefix) throws LJError { if (!(exp instanceof GroupExpression)) { exp = new GroupExpression(exp); } + exp = resolveStaticFinalConstants(exp, element); + } + + /** + * Walks {@code root}, replacing {@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 node. User-defined enums and unresolvable references are left untouched. + */ + private static Expression resolveStaticFinalConstants(Expression root, CtElement context) throws LJError { + List enums = new ArrayList<>(); + collectEnums(root, enums); + Expression e = root; + for (Enum en : enums) { + Object v = StaticConstants.resolve(en.getTypeName(), en.getConstName(), context); + Predicate lit = StaticConstants.asLiteralPredicate(v); + if (lit != null) { + e = e.substitute(en, lit.getExpression()); + continue; + } + String suggested = StaticConstants.findJdkImportCandidate(en.getTypeName(), en.getConstName()); + if (suggested != null) { + SourcePosition pos = context == null ? null : Utils.getLJAnnotationPosition(context, en.toString()); + throw new liquidjava.diagnostics.errors.CustomError(String.format( + "Could not resolve '%s.%s' in refinement. " + + "If you meant the static final constant, add: import %s;", + en.getTypeName(), en.getConstName(), suggested), pos); + } + } + return e; + } + + private static void collectEnums(Expression e, List out) { + if (e instanceof Enum en) + out.add(en); + for (Expression c : e.getChildren()) + collectEnums(c, out); } /** Create a predicate with the expression true */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java new file mode 100644 index 00000000..2d074d55 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java @@ -0,0 +1,119 @@ +package liquidjava.utils; + +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; + +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.LiteralString; +import liquidjava.utils.constants.Types; +import spoon.reflect.code.CtLiteral; +import spoon.reflect.declaration.CtCompilationUnit; +import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtField; +import spoon.reflect.declaration.CtImport; +import spoon.reflect.reference.CtFieldReference; + +/** Resolution of {@code static final} primitive/String constants used in refinement predicates and field reads. */ +public final class StaticConstants { + + private StaticConstants() { + } + + /** Resolve a Spoon field reference to its compile-time constant value, source AST first then reflection. */ + public static Object resolve(CtFieldReference ref) { + if (!ref.isStatic() || !ref.isFinal()) + return null; + CtField decl = ref.getFieldDeclaration(); + if (decl != null && decl.getDefaultExpression()instanceof CtLiteral lit && lit.getValue() != null) + return lit.getValue(); + try { + return ref.getActualField()instanceof Field jf ? readStaticFinal(jf) : null; + } catch (Throwable ignored) { + return null; + } + } + + /** + * Resolve a {@code TypeName.CONST_NAME} reference (as it appears inside a refinement predicate string) via + * reflection. Tries {@code typeName} as-given, then {@code java.lang.}, then class names imported by + * {@code context}'s compilation unit (single-type and on-demand imports). {@code context} may be {@code null}. + */ + public static Object resolve(String typeName, String constName, CtElement context) { + Object v = lookup(typeName, constName); + if (v == null) + v = lookup("java.lang." + typeName, constName); + if (v != null || context == null || context.getPosition() == null || !context.getPosition().isValidPosition()) + return v; + CtCompilationUnit cu = context.getPosition().getCompilationUnit(); + if (cu == null) + return null; + for (CtImport imp : cu.getImports()) { + if (imp.getReference() == null) + continue; + String full = imp.getReference().toString(); + String candidate = full.endsWith("." + typeName) || full.equals(typeName) ? full + : full.endsWith(".*") ? full.substring(0, full.length() - 1) + typeName : null; + if (candidate != null && (v = lookup(candidate, constName)) != null) + return v; + } + return null; + } + + /** Wrap a resolved value as an RJ literal predicate, or {@code null} if its type is not modeled. */ + public static Predicate asLiteralPredicate(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; + } + + /** + * Speculative scan of common JDK packages for a class named {@code typeName} that has a {@code static final} + * primitive/String field {@code constName}. Returns the fully-qualified class name (e.g. + * {@code "javax.imageio.ImageWriteParam"}) of the first match, or {@code null} if no JDK match is found. Used to + * suggest a missing import when {@link #resolve(String, String, CtElement)} fails. + */ + public static String findJdkImportCandidate(String typeName, String constName) { + for (String pkg : JDK_PACKAGE_HINTS) { + String fqn = pkg + "." + typeName; + if (lookup(fqn, constName) != null) + return fqn; + } + return null; + } + + private static final String[] JDK_PACKAGE_HINTS = { "java.io", "java.util", "java.util.concurrent", + "java.util.regex", "java.nio", "java.nio.charset", "java.nio.file", "java.text", "java.time", "java.math", + "java.net", "java.awt", "java.awt.event", "javax.swing", "javax.imageio", "javax.sound.sampled", + "java.security", "java.sql" }; + + private static Object lookup(String className, String fieldName) { + try { + return readStaticFinal(Class.forName(className).getField(fieldName)); + } catch (ClassNotFoundException | LinkageError | NoSuchFieldException | SecurityException ignored) { + return null; + } + } + + private static Object readStaticFinal(Field jf) { + if (!Modifier.isStatic(jf.getModifiers()) || !Modifier.isFinal(jf.getModifiers())) + return null; + try { + jf.setAccessible(true); + return jf.get(null); + } catch (Throwable ignored) { + return null; + } + } +} From 3a5d2fec6293af56b3a426124a69a277d1f4344d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 4 May 2026 12:03:52 +0100 Subject: [PATCH 3/6] change class names --- .../CorrectStaticImportInPredicate.java | 26 +++++ .../ClassImporting.java | 10 ++ .../ClassNoImport.java} | 7 +- .../liquidjava/rj_language/Predicate.java | 25 ++-- .../liquidjava/utils/StaticConstants.java | 109 ++++++++++++------ 5 files changed, 128 insertions(+), 49 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStaticImportInPredicate.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassImporting.java rename liquidjava-example/src/main/java/testSuite/{ErrorMissingImportInPredicate.java => classes/missing_import_final_error/ClassNoImport.java} (53%) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStaticImportInPredicate.java b/liquidjava-example/src/main/java/testSuite/CorrectStaticImportInPredicate.java new file mode 100644 index 00000000..f2682320 --- /dev/null +++ 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/classes/missing_import_final_error/ClassImporting.java b/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassImporting.java new file mode 100644 index 00000000..0903fae0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassImporting.java @@ -0,0 +1,10 @@ +package testSuite.classes.error_missing_import; + +import javax.imageio.ImageWriteParam; + +/** Sibling file that imports the class so the verifier knows where to find it. */ +public class Helper { + public static int explicit() { + return ImageWriteParam.MODE_EXPLICIT; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMissingImportInPredicate.java b/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java similarity index 53% rename from liquidjava-example/src/main/java/testSuite/ErrorMissingImportInPredicate.java rename to liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java index 6b33a84e..e9284a6a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorMissingImportInPredicate.java +++ b/liquidjava-example/src/main/java/testSuite/classes/missing_import_final_error/ClassNoImport.java @@ -1,11 +1,12 @@ -package testSuite; +package testSuite.classes.missing_import_final_error; import liquidjava.specification.Refinement; @SuppressWarnings("unused") -public class ErrorMissingImportInPredicate { +public class ClassNoImport { - // No import for javax.imageio.ImageWriteParam — the verifier should suggest the import. + // 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 } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 473ec119..1785c347 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -96,14 +96,16 @@ private static Expression resolveStaticFinalConstants(Expression root, CtElement e = e.substitute(en, lit.getExpression()); continue; } - String suggested = StaticConstants.findJdkImportCandidate(en.getTypeName(), en.getConstName()); - if (suggested != null) { - SourcePosition pos = context == null ? null : Utils.getLJAnnotationPosition(context, en.toString()); - throw new liquidjava.diagnostics.errors.CustomError(String.format( - "Could not resolve '%s.%s' in refinement. " - + "If you meant the static final constant, add: import %s;", - en.getTypeName(), en.getConstName(), suggested), pos); - } + if (StaticConstants.userTypeExists(en.getTypeName(), context)) + continue; // likely a user-defined enum/class — let SMT translation handle it + 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 e; } @@ -115,7 +117,12 @@ private static void collectEnums(Expression e, List out) { collectEnums(c, out); } - /** Create a predicate with the expression true */ + /** + * 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; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java index 2d074d55..82b3b3c5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java @@ -11,7 +11,11 @@ import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtField; import spoon.reflect.declaration.CtImport; +import spoon.reflect.declaration.CtImportKind; +import spoon.reflect.declaration.CtType; import spoon.reflect.reference.CtFieldReference; +import spoon.reflect.reference.CtPackageReference; +import spoon.reflect.reference.CtTypeReference; /** Resolution of {@code static final} primitive/String constants used in refinement predicates and field reads. */ public final class StaticConstants { @@ -28,37 +32,87 @@ public static Object resolve(CtFieldReference ref) { return lit.getValue(); try { return ref.getActualField()instanceof Field jf ? readStaticFinal(jf) : null; - } catch (Throwable ignored) { + } catch (RuntimeException | LinkageError ignored) { + // Spoon throws SpoonClassNotFoundException; reflection can throw LinkageError. Fall through. return null; } } /** * Resolve a {@code TypeName.CONST_NAME} reference (as it appears inside a refinement predicate string) via - * reflection. Tries {@code typeName} as-given, then {@code java.lang.}, then class names imported by - * {@code context}'s compilation unit (single-type and on-demand imports). {@code context} may be {@code null}. + * reflection. Resolution order matches Java scoping rules: fully-qualified name → explicit imports of + * {@code context}'s compilation unit (single-type and on-demand) → implicit {@code java.lang}. {@code context} may + * be {@code null}. */ public static Object resolve(String typeName, String constName, CtElement context) { Object v = lookup(typeName, constName); - if (v == null) - v = lookup("java.lang." + typeName, constName); - if (v != null || context == null || context.getPosition() == null || !context.getPosition().isValidPosition()) + if (v != null) return v; - CtCompilationUnit cu = context.getPosition().getCompilationUnit(); - if (cu == null) + String fqn = findFqnInImports(typeName, constName, localImports(context)); + if (fqn != null) + return lookup(fqn, constName); + return lookup("java.lang." + typeName, constName); + } + + /** + * Look for a candidate class in any compilation unit's imports across the same Spoon model — useful for "did you + * forget an import?" hints when the user already imported {@code typeName} in another file. Returns the + * fully-qualified class name of the first match, or {@code null}. + */ + public static String findImportCandidate(String typeName, String constName, CtElement context) { + if (context == null || context.getFactory() == null) return null; - for (CtImport imp : cu.getImports()) { - if (imp.getReference() == null) - continue; - String full = imp.getReference().toString(); - String candidate = full.endsWith("." + typeName) || full.equals(typeName) ? full - : full.endsWith(".*") ? full.substring(0, full.length() - 1) + typeName : null; - if (candidate != null && (v = lookup(candidate, constName)) != null) - return v; + for (CtCompilationUnit cu : context.getFactory().CompilationUnit().getMap().values()) { + String fqn = findFqnInImports(typeName, constName, cu.getImports()); + if (fqn != null) + return fqn; + } + return null; + } + + /** Whether a {@link CtType} with the given simple name is present in {@code context}'s Spoon model. */ + public static boolean userTypeExists(String simpleName, CtElement context) { + if (context == null || context.getFactory() == null) + return false; + for (CtType t : context.getFactory().Type().getAll(true)) + if (simpleName.equals(t.getSimpleName())) + return true; + return false; + } + + private static Iterable localImports(CtElement context) { + if (context == null || context.getPosition() == null || !context.getPosition().isValidPosition()) + return java.util.Collections.emptyList(); + CtCompilationUnit cu = context.getPosition().getCompilationUnit(); + return cu == null ? java.util.Collections.emptyList() : cu.getImports(); + } + + private static String findFqnInImports(String typeName, String constName, Iterable imports) { + for (CtImport imp : imports) { + String candidate = importCandidate(imp, typeName); + if (candidate != null && lookup(candidate, constName) != null) + return candidate; } return null; } + private static String importCandidate(CtImport imp, String typeName) { + if (imp.getReference() == null) + return null; + // Use Spoon's typed APIs so nested classes get their binary name (Map$Entry, not Map.Entry). + if (imp.getImportKind() == CtImportKind.TYPE && imp.getReference()instanceof CtTypeReference tref) { + String fqn = tref.getQualifiedName(); + if (fqn.equals(typeName) || fqn.endsWith("." + typeName) || fqn.endsWith("$" + typeName)) + return fqn; + return null; + } + if (imp.getImportKind() == CtImportKind.ALL_TYPES && imp.getReference()instanceof CtPackageReference pref) { + String pkg = pref.getQualifiedName(); + return pkg.isEmpty() ? typeName : pkg + "." + typeName; + } + return null; // FIELD / METHOD / ALL_STATIC_MEMBERS / UNRESOLVED — not relevant for type resolution. + } + /** Wrap a resolved value as an RJ literal predicate, or {@code null} if its type is not modeled. */ public static Predicate asLiteralPredicate(Object value) { if (value instanceof Boolean) @@ -78,26 +132,6 @@ public static Predicate asLiteralPredicate(Object value) { return null; } - /** - * Speculative scan of common JDK packages for a class named {@code typeName} that has a {@code static final} - * primitive/String field {@code constName}. Returns the fully-qualified class name (e.g. - * {@code "javax.imageio.ImageWriteParam"}) of the first match, or {@code null} if no JDK match is found. Used to - * suggest a missing import when {@link #resolve(String, String, CtElement)} fails. - */ - public static String findJdkImportCandidate(String typeName, String constName) { - for (String pkg : JDK_PACKAGE_HINTS) { - String fqn = pkg + "." + typeName; - if (lookup(fqn, constName) != null) - return fqn; - } - return null; - } - - private static final String[] JDK_PACKAGE_HINTS = { "java.io", "java.util", "java.util.concurrent", - "java.util.regex", "java.nio", "java.nio.charset", "java.nio.file", "java.text", "java.time", "java.math", - "java.net", "java.awt", "java.awt.event", "javax.swing", "javax.imageio", "javax.sound.sampled", - "java.security", "java.sql" }; - private static Object lookup(String className, String fieldName) { try { return readStaticFinal(Class.forName(className).getField(fieldName)); @@ -112,7 +146,8 @@ private static Object readStaticFinal(Field jf) { try { jf.setAccessible(true); return jf.get(null); - } catch (Throwable ignored) { + } catch (IllegalAccessException | LinkageError ignored) { + // LinkageError covers ExceptionInInitializerError, NoClassDefFoundError, etc. return null; } } From 9cacea7dd1a40dad6e85cb37987ec2e6c2e3657f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 4 May 2026 16:41:41 +0100 Subject: [PATCH 4/6] forgot to save --- .../classes/missing_import_final_error/ClassImporting.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 index 0903fae0..b0f1941e 100644 --- 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 @@ -1,9 +1,9 @@ -package testSuite.classes.error_missing_import; +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 Helper { +public class ClassImporting { public static int explicit() { return ImageWriteParam.MODE_EXPLICIT; } From 2e77dfa22ed8a3e53d31624c48f6709ca55bcca8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 4 May 2026 17:19:29 +0100 Subject: [PATCH 5/6] add more javadoc --- .../liquidjava/rj_language/Predicate.java | 1 + .../liquidjava/utils/StaticConstants.java | 20 ++++++++++++++++++- 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 1785c347..59d86f40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -98,6 +98,7 @@ private static Expression resolveStaticFinalConstants(Expression root, CtElement } 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 + ";" diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java index 82b3b3c5..0198225e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java @@ -23,7 +23,16 @@ public final class StaticConstants { private StaticConstants() { } - /** Resolve a Spoon field reference to its compile-time constant value, source AST first then reflection. */ + /** + * Resolve a Spoon {@code static final} field reference to its compile-time value, so reads like + * {@code Integer.MAX_VALUE} or {@code MyConfig.LIMIT} fold to literals before SMT translation. + * + *

Tries the source AST first ({@link CtLiteral} initializer in Spoon's model), then reflection via + * {@link CtFieldReference#getActualField()} + {@link #readStaticFinal}. Returns {@code null} if the field + * isn't static-final, has a non-literal initializer, or any lookup step fails. + * + * @see #resolve(String, String, CtElement) sibling for refinement-string {@code Type.CONST} references + */ public static Object resolve(CtFieldReference ref) { if (!ref.isStatic() || !ref.isFinal()) return null; @@ -132,6 +141,15 @@ public static Predicate asLiteralPredicate(Object value) { return null; } + /** + * Reflectively read {@code className.fieldName} as a {@code public static final} constant — e.g. + * {@code lookup("java.lang.Integer", "MAX_VALUE")} returns {@code 2147483647}, which is how + * {@code Integer.MAX_VALUE} gets baked into the AST before SMT translation. + * + *

Returns {@code null} on any failure ({@link ClassNotFoundException}, {@link NoSuchFieldException}, + * {@link LinkageError}, {@link SecurityException}, or non-static-final) so callers can fall through to the + * next resolution strategy without a try/catch. Only public fields are visible to {@link Class#getField}. + */ private static Object lookup(String className, String fieldName) { try { return readStaticFinal(Class.forName(className).getField(fieldName)); From faaeb06e74b9a81f46db964767375cb3a2e84d3a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 5 May 2026 11:46:32 +0100 Subject: [PATCH 6/6] keep translation from final to literal value --- .../diagnostics/errors/RefinementError.java | 5 ++- .../liquidjava/rj_language/Predicate.java | 12 ++++--- .../java/liquidjava/rj_language/ast/Enum.java | 19 +++++++++++- .../rj_language/ast/Expression.java | 12 +++++++ .../liquidjava/smt/ExpressionToZ3Visitor.java | 2 ++ .../java/liquidjava/smt/TranslatorToZ3.java | 31 +++++++++++++++++++ .../liquidjava/utils/StaticConstants.java | 14 +++++---- 7 files changed, 82 insertions(+), 13 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index a775b6c2..f5b647d8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -46,7 +46,10 @@ public String getCounterExampleString() { List foundVarNames = new ArrayList<>(); found.getValue().getVariableNames(foundVarNames); - List 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()) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 59d86f40..410ef761 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -81,19 +81,21 @@ public Predicate(String ref, CtElement element, String prefix) throws LJError { } /** - * Walks {@code root}, replacing {@link Enum} nodes that resolve (via reflection, java.lang fallback, or imports + * 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 node. User-defined enums and unresolvable references are left untouched. + * 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 enums = new ArrayList<>(); collectEnums(root, enums); - Expression e = root; for (Enum en : enums) { Object v = StaticConstants.resolve(en.getTypeName(), en.getConstName(), context); Predicate lit = StaticConstants.asLiteralPredicate(v); if (lit != null) { - e = e.substitute(en, lit.getExpression()); + en.setResolvedLiteral(lit.getExpression()); continue; } if (StaticConstants.userTypeExists(en.getTypeName(), context)) @@ -108,7 +110,7 @@ private static Expression resolveStaticFinalConstants(Expression root, CtElement en.getTypeName(), en.getConstName(), hint), pos); } - return e; + return root; } private static void collectEnums(Expression e, List out) { 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 index 17c8e17b..386b50d6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java @@ -9,6 +9,13 @@ public class Enum extends Expression { private final String typeName; private final String constName; + /** + * If this {@code Type.CONST} reference resolved to a Java {@code static final} primitive/String constant, the + * corresponding RJ literal expression is stashed here so the SMT translator can emit a binding axiom + * ({@code Type.CONST == literalValue}) while preserving the symbolic name in the AST. {@code null} for user-defined + * enum constants and for unresolvable references. + */ + private Expression resolvedLiteral; public Enum(String typeName, String constName) { this.typeName = typeName; @@ -23,6 +30,14 @@ public String getConstName() { return constName; } + public Expression getResolvedLiteral() { + return resolvedLiteral; + } + + public void setResolvedLiteral(Expression resolvedLiteral) { + this.resolvedLiteral = resolvedLiteral; + } + @Override public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitEnum(this); @@ -69,6 +84,8 @@ public boolean equals(Object obj) { @Override public Expression clone() { - return new Enum(typeName, constName); + Enum c = new Enum(typeName, constName); + c.resolvedLiteral = resolvedLiteral == null ? null : resolvedLiteral.clone(); + return c; } } 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 index 6e5a51c4..ee638262 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -25,6 +25,18 @@ public abstract class Expression { public abstract void getVariableNames(List toAdd); + /** + * Collect dotted names ({@code Type.CONST}) of {@link Enum} nodes that have been resolved to a Java + * {@code static final} literal value. Used by the counterexample renderer to keep these constants in the displayed + * model even though they are not program variables. + */ + public void getResolvedConstantNames(List toAdd) { + if (this instanceof liquidjava.rj_language.ast.Enum en && en.getResolvedLiteral() != null) + toAdd.add(en.getTypeName() + "." + en.getConstName()); + for (Expression c : getChildren()) + c.getResolvedConstantNames(toAdd); + } + public abstract void getStateInvocations(List toAdd, List all); public abstract boolean isBooleanTrue(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index 8bb46c05..464cd989 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -124,6 +124,8 @@ public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { @Override public Expr visitEnum(Enum en) throws LJError { + if (en.getResolvedLiteral() != null) + return ctx.makeStaticConstant(en.getTypeName(), en.getConstName(), en.getResolvedLiteral().accept(this)); return ctx.makeEnum(en.getTypeName(), en.getConstName()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 920c0b70..cf568927 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -42,6 +42,17 @@ public class TranslatorToZ3 implements AutoCloseable { private final Map> funcTranslation = new HashMap<>(); private final Map> funcAppTranslation = new HashMap<>(); private final Map, String> exprToNameTranslation = new HashMap<>(); + /** + * Z3 constants for resolved {@code static final} references (e.g. {@code Integer.MAX_VALUE}). Keyed by the dotted + * symbolic name so the same constant is reused across the query and the binding axiom is emitted once. + */ + private final Map> staticConstantTranslation = new HashMap<>(); + /** + * Equality axioms binding each {@link #staticConstantTranslation} entry to its compile-time literal value. + * Conjoined into every solver built by {@link #makeSolverForExpression} so the constant is always pinned but still + * appears symbolically in counterexample models. + */ + private final List staticConstantAxioms = new ArrayList<>(); public TranslatorToZ3(liquidjava.processor.context.Context context) { TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation); @@ -54,6 +65,8 @@ public TranslatorToZ3(liquidjava.processor.context.Context context) { @SuppressWarnings("unchecked") public Solver makeSolverForExpression(Expr e) { Solver solver = z3.mkSolver(); + for (BoolExpr axiom : staticConstantAxioms) + solver.add(axiom); solver.add((BoolExpr) e); return solver; } @@ -128,6 +141,24 @@ public Expr makeEnum(String enumTypeName, String enumConstantName) throws LJE return getVariableTranslation(varName); } + /** + * Declare (or look up) a Z3 constant named {@code Type.CONST} for a resolved Java {@code static final} reference, + * and emit a single equality axiom binding it to its compile-time literal value. Subsequent calls with the same + * name reuse the existing constant. The axiom is added to every solver built via {@link #makeSolverForExpression}, + * so the constant always evaluates to its literal value while still appearing symbolically in error messages and + * counterexample models. + */ + public Expr makeStaticConstant(String typeName, String constName, Expr literalValue) { + String name = String.format(Formats.ENUM, typeName, constName); + Expr cached = staticConstantTranslation.get(name); + if (cached != null) + return cached; + Expr constant = z3.mkConst(name, literalValue.getSort()); + staticConstantTranslation.put(name, constant); + staticConstantAxioms.add(z3.mkEq(constant, literalValue)); + return constant; + } + public Expr makeFunctionInvocation(String name, Expr[] params) throws LJError { if (name.equals("addToIndex")) return makeStore(params); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java index 0198225e..ed0cd057 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java @@ -27,9 +27,10 @@ private StaticConstants() { * Resolve a Spoon {@code static final} field reference to its compile-time value, so reads like * {@code Integer.MAX_VALUE} or {@code MyConfig.LIMIT} fold to literals before SMT translation. * - *

Tries the source AST first ({@link CtLiteral} initializer in Spoon's model), then reflection via - * {@link CtFieldReference#getActualField()} + {@link #readStaticFinal}. Returns {@code null} if the field - * isn't static-final, has a non-literal initializer, or any lookup step fails. + *

+ * Tries the source AST first ({@link CtLiteral} initializer in Spoon's model), then reflection via + * {@link CtFieldReference#getActualField()} + {@link #readStaticFinal}. Returns {@code null} if the field isn't + * static-final, has a non-literal initializer, or any lookup step fails. * * @see #resolve(String, String, CtElement) sibling for refinement-string {@code Type.CONST} references */ @@ -146,9 +147,10 @@ public static Predicate asLiteralPredicate(Object value) { * {@code lookup("java.lang.Integer", "MAX_VALUE")} returns {@code 2147483647}, which is how * {@code Integer.MAX_VALUE} gets baked into the AST before SMT translation. * - *

Returns {@code null} on any failure ({@link ClassNotFoundException}, {@link NoSuchFieldException}, - * {@link LinkageError}, {@link SecurityException}, or non-static-final) so callers can fall through to the - * next resolution strategy without a try/catch. Only public fields are visible to {@link Class#getField}. + *

+ * Returns {@code null} on any failure ({@link ClassNotFoundException}, {@link NoSuchFieldException}, + * {@link LinkageError}, {@link SecurityException}, or non-static-final) so callers can fall through to the next + * resolution strategy without a try/catch. Only public fields are visible to {@link Class#getField}. */ private static Object lookup(String className, String fieldName) { try {