Skip to content

Commit 1df915f

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
committed
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) <noreply@anthropic.com>
1 parent 87c0a99 commit 1df915f

8 files changed

Lines changed: 256 additions & 39 deletions

File tree

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

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
package testSuite;
2+
3+
import javax.imageio.ImageWriteParam;
4+
5+
import liquidjava.specification.Refinement;
6+
7+
@SuppressWarnings("unused")
8+
public class CorrectImageWriteParamModes {
9+
10+
static void requireExplicit(
11+
@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) {
12+
}
13+
14+
static void requireKnownMode(
15+
@Refinement("_ == ImageWriteParam.MODE_DISABLED || _ == ImageWriteParam.MODE_DEFAULT "
16+
+ "|| _ == ImageWriteParam.MODE_EXPLICIT || _ == ImageWriteParam.MODE_COPY_FROM_METADATA") int mode) {
17+
}
18+
19+
public static void main(String[] args) {
20+
requireExplicit(ImageWriteParam.MODE_EXPLICIT);
21+
requireKnownMode(ImageWriteParam.MODE_DEFAULT);
22+
requireKnownMode(ImageWriteParam.MODE_DISABLED);
23+
requireKnownMode(2);
24+
}
25+
}

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

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class CorrectStaticFinalInPredicate {
7+
8+
// Constants resolved inside the predicate string itself.
9+
static void clampInt(@Refinement("_ >= Integer.MIN_VALUE && _ <= Integer.MAX_VALUE") int x) {
10+
}
11+
12+
static void belowMaxLong(@Refinement("_ <= Long.MAX_VALUE") long x) {
13+
}
14+
15+
static void notMaxByte(@Refinement("_ != Byte.MAX_VALUE") int x) {
16+
}
17+
18+
public static void main(String[] args) {
19+
clampInt(0);
20+
clampInt(Integer.MAX_VALUE);
21+
clampInt(Integer.MIN_VALUE);
22+
belowMaxLong(123L);
23+
notMaxByte(0);
24+
}
25+
}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite;
2+
3+
import javax.imageio.ImageWriteParam;
4+
5+
import liquidjava.specification.Refinement;
6+
7+
@SuppressWarnings("unused")
8+
public class ErrorImageWriteParamModes {
9+
10+
static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) {
11+
}
12+
13+
public static void main(String[] args) {
14+
// MODE_DEFAULT is 1, not 2 (MODE_EXPLICIT).
15+
requireExplicit(ImageWriteParam.MODE_DEFAULT); // Refinement Error
16+
}
17+
}

‎liquidjava-example/src/main/java/testSuite/ErrorMissingImportInPredicate.java‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class ErrorMissingImportInPredicate {
7+
8+
// No import for javax.imageio.ImageWriteParam — the verifier should suggest the import.
9+
static void requireExplicit(@Refinement("_ == ImageWriteParam.MODE_EXPLICIT") int mode) { // Error
10+
}
11+
12+
public static void main(String[] args) {
13+
requireExplicit(2);
14+
}
15+
}

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class ErrorStaticFinalInPredicate {
7+
8+
static void belowMaxByte(@Refinement("_ <= Byte.MAX_VALUE") int x) {
9+
}
10+
11+
public static void main(String[] args) {
12+
// Byte.MAX_VALUE == 127, so 200 violates the bound.
13+
belowMaxByte(200); // Refinement Error
14+
}
15+
}

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

Lines changed: 2 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
1414
import liquidjava.rj_language.BuiltinFunctionPredicate;
1515
import liquidjava.rj_language.Predicate;
16-
import liquidjava.rj_language.ast.LiteralString;
16+
import liquidjava.utils.StaticConstants;
1717
import liquidjava.utils.constants.Formats;
1818
import liquidjava.utils.constants.Keys;
1919
import liquidjava.utils.constants.Types;
@@ -286,50 +286,13 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
286286

287287
/** Resolve a {@code static final} primitive/String constant to {@code #wild == <literal>}. */
288288
private <T> boolean tryStaticFinalConstantRefinement(CtFieldRead<T> fieldRead) {
289-
CtFieldReference<T> ref = fieldRead.getVariable();
290-
if (!ref.isStatic() || !ref.isFinal())
291-
return false;
292-
293-
Object value = null;
294-
CtField<?> decl = ref.getFieldDeclaration();
295-
if (decl != null && decl.getDefaultExpression()instanceof CtLiteral<?> lit)
296-
value = lit.getValue();
297-
if (value == null) {
298-
try {
299-
if (ref.getActualField()instanceof java.lang.reflect.Field jf) {
300-
jf.setAccessible(true);
301-
value = jf.get(null);
302-
}
303-
} catch (Throwable ignored) {
304-
// ClassNotFound / IllegalAccess / ExceptionInInitializerError — fall through.
305-
}
306-
}
307-
308-
Predicate literal = literalPredicateFor(value);
289+
Predicate literal = StaticConstants.asLiteralPredicate(StaticConstants.resolve(fieldRead.getVariable()));
309290
if (literal == null)
310291
return false;
311292
fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), literal));
312293
return true;
313294
}
314295

315-
private static Predicate literalPredicateFor(Object value) {
316-
if (value instanceof Boolean)
317-
return Predicate.createLit(value.toString(), Types.BOOLEAN);
318-
if (value instanceof Integer || value instanceof Short || value instanceof Byte)
319-
return Predicate.createLit(value.toString(), Types.INT);
320-
if (value instanceof Long)
321-
return Predicate.createLit(value.toString(), Types.LONG);
322-
if (value instanceof Float)
323-
return Predicate.createLit(value.toString(), Types.FLOAT);
324-
if (value instanceof Double)
325-
return Predicate.createLit(value.toString(), Types.DOUBLE);
326-
if (value instanceof Character)
327-
return Predicate.createLit("'" + value + "'", Types.CHAR);
328-
if (value instanceof String s)
329-
return new Predicate(new LiteralString("\"" + s + "\""));
330-
return null;
331-
}
332-
333296
@Override
334297
public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
335298
super.visitCtVariableRead(variableRead);

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

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
import liquidjava.processor.context.GhostState;
1515
import liquidjava.processor.facade.AliasDTO;
1616
import liquidjava.rj_language.ast.BinaryExpression;
17+
import liquidjava.rj_language.ast.Enum;
1718
import liquidjava.rj_language.ast.Expression;
1819
import liquidjava.rj_language.ast.FunctionInvocation;
1920
import liquidjava.rj_language.ast.GroupExpression;
@@ -25,6 +26,7 @@
2526
import liquidjava.rj_language.ast.LiteralReal;
2627
import liquidjava.rj_language.ast.UnaryExpression;
2728
import liquidjava.rj_language.ast.Var;
29+
import liquidjava.utils.StaticConstants;
2830
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
2931
import liquidjava.rj_language.opt.ExpressionSimplifier;
3032
import liquidjava.rj_language.parsing.RefinementsParser;
@@ -75,6 +77,42 @@ public Predicate(String ref, CtElement element, String prefix) throws LJError {
7577
if (!(exp instanceof GroupExpression)) {
7678
exp = new GroupExpression(exp);
7779
}
80+
exp = resolveStaticFinalConstants(exp, element);
81+
}
82+
83+
/**
84+
* Walks {@code root}, replacing {@link Enum} nodes that resolve (via reflection, java.lang fallback, or imports
85+
* declared in {@code context}'s compilation unit) to a {@code static final} primitive/String constant with the
86+
* corresponding literal node. User-defined enums and unresolvable references are left untouched.
87+
*/
88+
private static Expression resolveStaticFinalConstants(Expression root, CtElement context) throws LJError {
89+
List<Enum> enums = new ArrayList<>();
90+
collectEnums(root, enums);
91+
Expression e = root;
92+
for (Enum en : enums) {
93+
Object v = StaticConstants.resolve(en.getTypeName(), en.getConstName(), context);
94+
Predicate lit = StaticConstants.asLiteralPredicate(v);
95+
if (lit != null) {
96+
e = e.substitute(en, lit.getExpression());
97+
continue;
98+
}
99+
String suggested = StaticConstants.findJdkImportCandidate(en.getTypeName(), en.getConstName());
100+
if (suggested != null) {
101+
SourcePosition pos = context == null ? null : Utils.getLJAnnotationPosition(context, en.toString());
102+
throw new liquidjava.diagnostics.errors.CustomError(String.format(
103+
"Could not resolve '%s.%s' in refinement. "
104+
+ "If you meant the static final constant, add: import %s;",
105+
en.getTypeName(), en.getConstName(), suggested), pos);
106+
}
107+
}
108+
return e;
109+
}
110+
111+
private static void collectEnums(Expression e, List<Enum> out) {
112+
if (e instanceof Enum en)
113+
out.add(en);
114+
for (Expression c : e.getChildren())
115+
collectEnums(c, out);
78116
}
79117

80118
/** Create a predicate with the expression true */

‎liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
package liquidjava.utils;
2+
3+
import java.lang.reflect.Field;
4+
import java.lang.reflect.Modifier;
5+
6+
import liquidjava.rj_language.Predicate;
7+
import liquidjava.rj_language.ast.LiteralString;
8+
import liquidjava.utils.constants.Types;
9+
import spoon.reflect.code.CtLiteral;
10+
import spoon.reflect.declaration.CtCompilationUnit;
11+
import spoon.reflect.declaration.CtElement;
12+
import spoon.reflect.declaration.CtField;
13+
import spoon.reflect.declaration.CtImport;
14+
import spoon.reflect.reference.CtFieldReference;
15+
16+
/** Resolution of {@code static final} primitive/String constants used in refinement predicates and field reads. */
17+
public final class StaticConstants {
18+
19+
private StaticConstants() {
20+
}
21+
22+
/** Resolve a Spoon field reference to its compile-time constant value, source AST first then reflection. */
23+
public static Object resolve(CtFieldReference<?> ref) {
24+
if (!ref.isStatic() || !ref.isFinal())
25+
return null;
26+
CtField<?> decl = ref.getFieldDeclaration();
27+
if (decl != null && decl.getDefaultExpression()instanceof CtLiteral<?> lit && lit.getValue() != null)
28+
return lit.getValue();
29+
try {
30+
return ref.getActualField()instanceof Field jf ? readStaticFinal(jf) : null;
31+
} catch (Throwable ignored) {
32+
return null;
33+
}
34+
}
35+
36+
/**
37+
* Resolve a {@code TypeName.CONST_NAME} reference (as it appears inside a refinement predicate string) via
38+
* reflection. Tries {@code typeName} as-given, then {@code java.lang.}, then class names imported by
39+
* {@code context}'s compilation unit (single-type and on-demand imports). {@code context} may be {@code null}.
40+
*/
41+
public static Object resolve(String typeName, String constName, CtElement context) {
42+
Object v = lookup(typeName, constName);
43+
if (v == null)
44+
v = lookup("java.lang." + typeName, constName);
45+
if (v != null || context == null || context.getPosition() == null || !context.getPosition().isValidPosition())
46+
return v;
47+
CtCompilationUnit cu = context.getPosition().getCompilationUnit();
48+
if (cu == null)
49+
return null;
50+
for (CtImport imp : cu.getImports()) {
51+
if (imp.getReference() == null)
52+
continue;
53+
String full = imp.getReference().toString();
54+
String candidate = full.endsWith("." + typeName) || full.equals(typeName) ? full
55+
: full.endsWith(".*") ? full.substring(0, full.length() - 1) + typeName : null;
56+
if (candidate != null && (v = lookup(candidate, constName)) != null)
57+
return v;
58+
}
59+
return null;
60+
}
61+
62+
/** Wrap a resolved value as an RJ literal predicate, or {@code null} if its type is not modeled. */
63+
public static Predicate asLiteralPredicate(Object value) {
64+
if (value instanceof Boolean)
65+
return Predicate.createLit(value.toString(), Types.BOOLEAN);
66+
if (value instanceof Integer || value instanceof Short || value instanceof Byte)
67+
return Predicate.createLit(value.toString(), Types.INT);
68+
if (value instanceof Long)
69+
return Predicate.createLit(value.toString(), Types.LONG);
70+
if (value instanceof Float)
71+
return Predicate.createLit(value.toString(), Types.FLOAT);
72+
if (value instanceof Double)
73+
return Predicate.createLit(value.toString(), Types.DOUBLE);
74+
if (value instanceof Character)
75+
return Predicate.createLit("'" + value + "'", Types.CHAR);
76+
if (value instanceof String s)
77+
return new Predicate(new LiteralString("\"" + s + "\""));
78+
return null;
79+
}
80+
81+
/**
82+
* Speculative scan of common JDK packages for a class named {@code typeName} that has a {@code static final}
83+
* primitive/String field {@code constName}. Returns the fully-qualified class name (e.g.
84+
* {@code "javax.imageio.ImageWriteParam"}) of the first match, or {@code null} if no JDK match is found. Used to
85+
* suggest a missing import when {@link #resolve(String, String, CtElement)} fails.
86+
*/
87+
public static String findJdkImportCandidate(String typeName, String constName) {
88+
for (String pkg : JDK_PACKAGE_HINTS) {
89+
String fqn = pkg + "." + typeName;
90+
if (lookup(fqn, constName) != null)
91+
return fqn;
92+
}
93+
return null;
94+
}
95+
96+
private static final String[] JDK_PACKAGE_HINTS = { "java.io", "java.util", "java.util.concurrent",
97+
"java.util.regex", "java.nio", "java.nio.charset", "java.nio.file", "java.text", "java.time", "java.math",
98+
"java.net", "java.awt", "java.awt.event", "javax.swing", "javax.imageio", "javax.sound.sampled",
99+
"java.security", "java.sql" };
100+
101+
private static Object lookup(String className, String fieldName) {
102+
try {
103+
return readStaticFinal(Class.forName(className).getField(fieldName));
104+
} catch (ClassNotFoundException | LinkageError | NoSuchFieldException | SecurityException ignored) {
105+
return null;
106+
}
107+
}
108+
109+
private static Object readStaticFinal(Field jf) {
110+
if (!Modifier.isStatic(jf.getModifiers()) || !Modifier.isFinal(jf.getModifiers()))
111+
return null;
112+
try {
113+
jf.setAccessible(true);
114+
return jf.get(null);
115+
} catch (Throwable ignored) {
116+
return null;
117+
}
118+
}
119+
}

0 commit comments

Comments
 (0)