Resolve Static Final Constants in Refinement Aliases

liquidjava-example/src/main/java/testSuite/CorrectStaticFinalInAlias.java

@@ -0,0 +1,26 @@
+package testSuite;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+
+@SuppressWarnings("unused")
+@RefinementAlias("Mode(int x) { x == ImageWriteParam.MODE_DISABLED || x == ImageWriteParam.MODE_DEFAULT "
+        + "|| x == ImageWriteParam.MODE_EXPLICIT || x == ImageWriteParam.MODE_COPY_FROM_METADATA }")
+@RefinementAlias("BelowMaxByte(int x) { x <= Byte.MAX_VALUE }")
+public class CorrectStaticFinalInAlias {
+
+    static void setMode(@Refinement("Mode(_)") int mode) {
+    }
+
+    static void setSmall(@Refinement("BelowMaxByte(_)") int x) {
+    }
+
+    public static void main(String[] args) {
+        setMode(ImageWriteParam.MODE_EXPLICIT);
+        setMode(ImageWriteParam.MODE_DISABLED);
+        setMode(3);
+        setSmall(127);
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInAlias.java

@@ -0,0 +1,20 @@
+package testSuite;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+
+@SuppressWarnings("unused")
+@RefinementAlias("Mode(int x) { x == ImageWriteParam.MODE_DISABLED || x == ImageWriteParam.MODE_DEFAULT "
+        + "|| x == ImageWriteParam.MODE_EXPLICIT || x == ImageWriteParam.MODE_COPY_FROM_METADATA }")
+public class ErrorStaticFinalInAlias {
+
+    static void setMode(@Refinement("Mode(_)") int mode) {
+    }
+
+    public static void main(String[] args) {
+        // Modes range from 0 (MODE_DISABLED) to 3 (MODE_COPY_FROM_METADATA).
+        setMode(4); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInAliasMissingImport.java

@@ -0,0 +1,9 @@
+package testSuite;
+
+import liquidjava.specification.RefinementAlias;
+
+// No import for javax.imageio.ImageWriteParam, so the constant in the alias cannot be resolved
+@SuppressWarnings("unused")
+@RefinementAlias("Explicit(int x) { x == ImageWriteParam.MODE_EXPLICIT }") // Expect: Not Found Error
+public class ErrorStaticFinalInAliasMissingImport {
+}

liquidjava-example/src/main/java/testSuite/classes/alias_static_final_state_correct/ImageWriteParamRefinements.java

@@ -0,0 +1,29 @@
+package testSuite.classes.alias_static_final_state_correct;
+
+import java.util.Locale;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"startTiling", "tilingExplicit", "tilingSet"})
+@RefinementAlias("Mode(int x) { x == ImageWriteParam.MODE_EXPLICIT || x == ImageWriteParam.MODE_DEFAULT "
+        + "|| x == ImageWriteParam.MODE_COPY_FROM_METADATA || x == ImageWriteParam.MODE_DISABLED }")
+@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
+public interface ImageWriteParamRefinements {
+
+    @StateRefinement(to = "startTiling(this)")
+    void ImageWriteParam(Locale locale);
+
+    @StateRefinement(to = "mode == ImageWriteParam.MODE_EXPLICIT ? tilingExplicit(this) : startTiling(this)")
+    void setTilingMode(@Refinement("Mode(_)") int mode);
+
+    @StateRefinement(from = "tilingExplicit(this)", to = "tilingSet(this)")
+    @StateRefinement(from = "tilingSet(this)", to = "tilingSet(this)")
+    void setTiling(@Refinement("_ > 0") int tileWidth, @Refinement("_ > 0") int tileHeight, int tileGridXOffset,
+            int tileGridYOffset);
+}

liquidjava-example/src/main/java/testSuite/classes/alias_static_final_state_correct/TilingClient.java

@@ -0,0 +1,15 @@
+package testSuite.classes.alias_static_final_state_correct;
+
+import java.util.Locale;
+
+import javax.imageio.ImageWriteParam;
+
+class TilingClient {
+
+    ImageWriteParam tiled() {
+        ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
+        param.setTilingMode(ImageWriteParam.MODE_EXPLICIT);
+        param.setTiling(256, 256, 0, 0);
+        return param;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java

@@ -4,8 +4,11 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.LJError;
+import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.parsing.RefinementsParser;
+import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtTypeInformation;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -40,6 +43,13 @@ public void parse(String prefix) throws LJError {
         }
     }
 
+    // Resolve Type.CONST references to static final constants, using the imports of the class declaring the alias
+    public void resolveStaticFinalConstants(CtElement context, SourcePosition position) throws LJError {
+        if (expression != null) {
+            this.expression = Predicate.resolveStaticFinalConstants(expression, context, position);
+        }
+    }
+
     public String getName() {
         return name;
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -333,6 +333,7 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
             }
             if (klass != null && path != null) {
                 a.parse(path);
+                a.resolveStaticFinalConstants(element, position);
                 if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
                     throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
                             ref);

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

@@ -85,6 +85,16 @@ public Predicate(String ref, CtElement element, String prefix) throws LJError {
      * untouched (the SMT side handles them as user enum constants).
      */
     private static Expression resolveStaticFinalConstants(Expression root, CtElement context) throws LJError {
+        return resolveStaticFinalConstants(root, context, null);
+    }
+
+    /**
+     * Same as {@link #resolveStaticFinalConstants(Expression, CtElement)}, but unresolvable references are reported at
+     * {@code errorPosition} when it is non-null (e.g. for refinement aliases, whose annotation value is the whole alias
+     * definition rather than the {@code Type.CONST} reference).
+     */
+    public static Expression resolveStaticFinalConstants(Expression root, CtElement context,
+            SourcePosition errorPosition) throws LJError {
         List<Enum> enums = new ArrayList<>();
         collectEnums(root, enums);
         for (Enum en : enums) {
@@ -97,7 +107,8 @@ 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());
+            SourcePosition pos = errorPosition != null ? errorPosition
+                    : 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";