Skip to content

Commit 14dc9f9

Browse files
committed
Resolve Source Static Final Fields
1 parent 1c9644c commit 14dc9f9

3 files changed

Lines changed: 79 additions & 10 deletions

File tree

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class CorrectSourceStaticFinalInPredicate {
6+
7+
static void requireBelowLimit(@Refinement("_ < LIMITS.MAX") double x) {
8+
}
9+
10+
public static void main(String[] args) {
11+
requireBelowLimit(5.0);
12+
}
13+
14+
static class LIMITS {
15+
static final double MAX = 10.0;
16+
}
17+
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class ErrorSourceStaticFinalInPredicate {
6+
7+
static void requireBelowLimit(@Refinement("_ < LIMITS.MAX") double x) {
8+
}
9+
10+
public static void main(String[] args) {
11+
requireBelowLimit(15.0); // Refinement Error
12+
}
13+
14+
static class LIMITS {
15+
static final double MAX = 10.0;
16+
}
17+
}

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

Lines changed: 45 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -38,8 +38,9 @@ public static Object resolve(CtFieldReference<?> ref) {
3838
if (!ref.isStatic() || !ref.isFinal())
3939
return null;
4040
CtField<?> decl = ref.getFieldDeclaration();
41-
if (decl != null && decl.getDefaultExpression()instanceof CtLiteral<?> lit && lit.getValue() != null)
42-
return lit.getValue();
41+
Object v = sourceLiteralValue(decl);
42+
if (v != null)
43+
return v;
4344
try {
4445
return ref.getActualField()instanceof Field jf ? readStaticFinal(jf) : null;
4546
} catch (RuntimeException | LinkageError ignored) {
@@ -49,18 +50,19 @@ public static Object resolve(CtFieldReference<?> ref) {
4950
}
5051

5152
/**
52-
* Resolve a {@code TypeName.CONST_NAME} reference (as it appears inside a refinement predicate string) via
53-
* reflection. Resolution order matches Java scoping rules: fully-qualified name → explicit imports of
54-
* {@code context}'s compilation unit (single-type and on-demand) → implicit {@code java.lang}. {@code context} may
55-
* be {@code null}.
53+
* Resolve a {@code TypeName.CONST_NAME} reference (as it appears inside a refinement predicate string). Resolution
54+
* order matches Java scoping rules: fully-qualified/source-model name → explicit imports of {@code context}'s
55+
* compilation unit (single-type and on-demand) → implicit {@code java.lang}. {@code context} may be {@code null}.
5656
*/
5757
public static Object resolve(String typeName, String constName, CtElement context) {
58-
Object v = lookup(typeName, constName);
58+
Object v = lookupConstant(typeName, constName, context);
5959
if (v != null)
6060
return v;
61-
String fqn = findFqnInImports(typeName, constName, localImports(context));
62-
if (fqn != null)
63-
return lookup(fqn, constName);
61+
for (CtImport imp : localImports(context)) {
62+
String candidate = importCandidate(imp, typeName);
63+
if (candidate != null && (v = lookupConstant(candidate, constName, context)) != null)
64+
return v;
65+
}
6466
return lookup("java.lang." + typeName, constName);
6567
}
6668

@@ -123,6 +125,39 @@ private static String importCandidate(CtImport imp, String typeName) {
123125
return null; // FIELD / METHOD / ALL_STATIC_MEMBERS / UNRESOLVED — not relevant for type resolution.
124126
}
125127

128+
private static Object lookupConstant(String typeName, String constName, CtElement context) {
129+
Object v = lookup(typeName, constName);
130+
return v != null ? v : lookupSource(typeName, constName, context);
131+
}
132+
133+
private static Object lookupSource(String typeName, String constName, CtElement context) {
134+
if (context == null || context.getFactory() == null)
135+
return null;
136+
String currentPackage = packageName(context.getParent(CtType.class));
137+
for (CtType<?> t : context.getFactory().Type().getAll(true)) {
138+
boolean matches = typeName.equals(t.getQualifiedName())
139+
|| typeName.equals(t.getSimpleName()) && packageName(t).equals(currentPackage);
140+
if (matches) {
141+
Object v = sourceLiteralValue(t.getField(constName));
142+
if (v != null)
143+
return v;
144+
}
145+
}
146+
return null;
147+
}
148+
149+
private static Object sourceLiteralValue(CtField<?> field) {
150+
if (field == null || !field.isStatic() || !field.isFinal())
151+
return null;
152+
return field.getDefaultExpression()instanceof CtLiteral<?> lit ? lit.getValue() : null;
153+
}
154+
155+
private static String packageName(CtType<?> type) {
156+
if (type == null || type.getPackage() == null)
157+
return "";
158+
return type.getPackage().getQualifiedName();
159+
}
160+
126161
/** Wrap a resolved value as an RJ literal predicate, or {@code null} if its type is not modeled. */
127162
public static Predicate asLiteralPredicate(Object value) {
128163
if (value instanceof Boolean)

0 commit comments

Comments
 (0)