diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStaticFinalInAlias.java b/liquidjava-example/src/main/java/testSuite/CorrectStaticFinalInAlias.java new file mode 100644 index 000000000..865eda1a3 --- /dev/null +++ b/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); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInAlias.java new file mode 100644 index 000000000..955384210 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInAliasMissingImport.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalInAliasMissingImport.java new file mode 100644 index 000000000..62c9fc823 --- /dev/null +++ b/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 { +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/alias_static_final_state_correct/ImageWriteParamRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/alias_static_final_state_correct/ImageWriteParamRefinements.java new file mode 100644 index 000000000..5e0618afe --- /dev/null +++ b/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); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/alias_static_final_state_correct/TilingClient.java b/liquidjava-example/src/main/java/testSuite/classes/alias_static_final_state_correct/TilingClient.java new file mode 100644 index 000000000..04c0d6d3e --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index ca1206153..453be0fa3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/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; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 8a6886ce0..5cf795f90 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/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); 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 aa3d9e4f8..1bac14c9d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/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 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";