From c4ad23c6531ce85f65828c44df5081f19e17ce2e Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:50:20 +0100 Subject: [PATCH 1/2] Fix crash when a constant is compared in an if condition (#302) Comparing a value with a constant accessed through a type (an enum constant or a static field such as Format.JPG or Limits.max) directly in an if condition crashed with an NPE: the field read was looked up as an instance field (this#X), which is not in the context, and the if path did not fall back to the field read refinement. Such field reads now use the value from their refinement (e.g. Format.JPG, or the resolved literal of a static final constant), so the branches keep the meaning of the comparison, and an unconstrained fresh value when the constant has no known value. Enum constants are only represented as Type.CONST when the enum is declared in the analyzed sources; constants of other enums (e.g. java.time.DayOfWeek) could not be translated to SMT ("Variable not found"), so they now carry no information instead. Co-Authored-By: Claude Opus 5.5 --- .../CorrectEnumConstantInCondition.java | 109 ++++++++++++++++++ .../ErrorEnumConstantInCondition.java | 64 ++++++++++ .../RefinementTypeChecker.java | 3 +- .../general_checkers/OperationsChecker.java | 5 + 4 files changed, 180 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java new file mode 100644 index 00000000..2d4a27d6 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java @@ -0,0 +1,109 @@ +package testSuite; + +import java.time.DayOfWeek; + +import javax.imageio.ImageWriteParam; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +class CorrectEnumConstantInCondition { + enum Format { + JPG, PNG, GIF + } + + static class Limits { + static final int max = 10; // lowercase: int fields get a generated @Ghost, which must be lowercase + static int counter = 0; // not final: no known value + } + + static void onlyJpg(@Refinement("f == Format.JPG") Format f) {} + + static void notJpg(@Refinement("f != Format.JPG") Format f) {} + + static void notGif(@Refinement("f != Format.GIF") Format f) {} + + static String extension(Format format) { + if (format == Format.JPG) { + return "jpg"; + } + return "png"; + } + + static void thenBranch(Format format) { + if (format == Format.JPG) { + onlyJpg(format); + } + } + + static void elseBranch(Format format) { + if (format == Format.JPG) { + onlyJpg(format); + } else { + notJpg(format); + } + } + + static void notEquals(Format format) { + if (format != Format.JPG) { + notJpg(format); + } else { + onlyJpg(format); + } + } + + static void constantOnTheLeft(Format format) { + if (Format.JPG == format) { + onlyJpg(format); + } + } + + static void and(Format format, int n) { + if (format == Format.JPG && n > 0) { + onlyJpg(format); + @Refinement("_ > 0") + int m = n; + } + } + + static void or(Format format) { + if (format == Format.JPG || format == Format.PNG) { + notGif(format); + } + } + + static void staticFinalOfUserClass(int n) { + if (n == Limits.max) { + @Refinement("_ == 10") + int m = n; + } + } + + static void jdkStaticFinal(int mode) { + if (mode != ImageWriteParam.MODE_COPY_FROM_METADATA) { + mode = ImageWriteParam.MODE_EXPLICIT; + } + } + + // a constant of an enum outside the analyzed sources carries no information, but does not crash + static int jdkEnum(DayOfWeek day) { + if (day == DayOfWeek.SUNDAY) { + return 0; + } else { + return 1; + } + } + + // a constant without a known value carries no information, but does not crash + static void unknownStaticField(int n) { + if (n == Limits.counter) { + n = 1; + } else { + n = 2; + } + } + + public static void main(String[] args) { + extension(Format.PNG); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java new file mode 100644 index 00000000..5f76c7d0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java @@ -0,0 +1,64 @@ +package testSuite; + +import java.time.DayOfWeek; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +class ErrorEnumConstantInCondition { + enum Format { + JPG, PNG, GIF + } + + static class Limits { + static final int max = 10; // lowercase: int fields get a generated @Ghost, which must be lowercase + } + + static void onlyJpg(@Refinement("f == Format.JPG") Format f) {} + + static void onlyPng(@Refinement("f == Format.PNG") Format f) {} + + static void thenBranch(Format format) { + if (format == Format.JPG) { + onlyPng(format); // Expect: Refinement Error + } + } + + // the else-branch is reachable: the condition is not the constant true + static void elseBranch(Format format) { + if (format == Format.JPG) { + onlyJpg(format); + } else { + onlyJpg(format); // Expect: Refinement Error + } + } + + static void notEquals(Format format) { + if (format != Format.JPG) { + onlyJpg(format); // Expect: Refinement Error + } + } + + static void or(Format format) { + if (format == Format.JPG || format == Format.PNG) { + onlyJpg(format); // Expect: Refinement Error + } + } + + static void staticFinalOfUserClass(int n) { + if (n == Limits.max) { + @Refinement("_ == 11") + int m = n; // Expect: Refinement Error + } + } + + // a constant that cannot be represented is unknown, so the else-branch is still checked + static void jdkEnumElse(DayOfWeek day, int n) { + if (day == DayOfWeek.SUNDAY) { + n = 1; + } else { + @Refinement("_ > 0") + int m = n; // Expect: 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 bf6dcc99..3cbd0d20 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 @@ -301,7 +301,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { String targetName = fieldRead.getTarget().toString(); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), BuiltinFunctionPredicate.length(targetName, fieldRead))); - } else if (fieldRead.getVariable().getDeclaringType().isEnum()) { + } else if (fieldRead.getVariable().getDeclaringType().getDeclaration() instanceof CtEnum) { + // only enums declared in the analyzed sources can be translated to SMT String target = fieldRead.getVariable().getDeclaringType().getSimpleName(); String enumLiteral = String.format(Formats.ENUM, target, fieldName); fieldRead.putMetadata(Keys.REFINEMENT, diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 550d6781..68e2d7ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -207,6 +207,11 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab elemName = String.format(Formats.THIS, elemName); Predicate elemRef = rtc.getContext().getVariableRefinements(elemName); + // Not a field of this class (e.g. an enum constant or a static constant): use the value given by the + // field read refinement (e.g. Format.JPG), or an unconstrained fresh value when there is none + if (elemRef == null && elemVar instanceof CtFieldRead) + return valueFromRefinement(elemVar, rtc.getRefinement(elemVar)); + String returnName = elemName; CtElement parent = operator.getParent(); From c1a706fe06749cc13338433540af4304ba4efc12 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Fri, 2 Oct 2026 14:08:04 +0100 Subject: [PATCH 2/2] Test more shapes of constants compared in conditions (#302) Add else-if chains over enum constants, arithmetic with a static final constant, a null check or-ed with a constant, and a comparison between two different constants. Co-Authored-By: Claude Opus 5.5 --- .../CorrectEnumConstantInCondition.java | 21 +++++++++++- .../ErrorEnumConstantInCondition.java | 34 ++++++++++++++++++- 2 files changed, 53 insertions(+), 2 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java index 2d4a27d6..8c63373e 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumConstantInCondition.java @@ -13,7 +13,7 @@ enum Format { } static class Limits { - static final int max = 10; // lowercase: int fields get a generated @Ghost, which must be lowercase + static final int max = 10; // lowercase until #307 is fixed static int counter = 0; // not final: no known value } @@ -23,6 +23,8 @@ static void notJpg(@Refinement("f != Format.JPG") Format f) {} static void notGif(@Refinement("f != Format.GIF") Format f) {} + static void onlyGif(@Refinement("f == Format.GIF") Format f) {} + static String extension(Format format) { if (format == Format.JPG) { return "jpg"; @@ -79,6 +81,23 @@ static void staticFinalOfUserClass(int n) { } } + static void elseIfChain(Format format) { + if (format == Format.JPG) { + onlyJpg(format); + } else if (format == Format.PNG) { + notJpg(format); + } else { + onlyGif(format); + } + } + + static void arithmetic(int n) { + if (n + Limits.max > 15) { + @Refinement("_ > 5") + int m = n; + } + } + static void jdkStaticFinal(int mode) { if (mode != ImageWriteParam.MODE_COPY_FROM_METADATA) { mode = ImageWriteParam.MODE_EXPLICIT; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java index 5f76c7d0..9f163f3a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumConstantInCondition.java @@ -11,7 +11,7 @@ enum Format { } static class Limits { - static final int max = 10; // lowercase: int fields get a generated @Ghost, which must be lowercase + static final int max = 10; // lowercase until #307 is fixed } static void onlyJpg(@Refinement("f == Format.JPG") Format f) {} @@ -45,6 +45,31 @@ static void or(Format format) { } } + static void elseIfChain(Format format) { + if (format == Format.JPG) { + } else if (format == Format.PNG) { + } else { + onlyPng(format); // Expect: Refinement Error + } + } + + // null comparisons carry no information: format may still be anything + static void nullOrConstant(Format format) { + if (format == null || format == Format.JPG) { + onlyJpg(format); // Expect: Refinement Error + } + } + + // two different constants are never equal, so the else-branch is always taken + static void twoConstants(int n) { + if (Format.JPG == Format.PNG) { + n = 1; + } else { + @Refinement("_ > 0") + int m = n; // Expect: Refinement Error + } + } + static void staticFinalOfUserClass(int n) { if (n == Limits.max) { @Refinement("_ == 11") @@ -52,6 +77,13 @@ static void staticFinalOfUserClass(int n) { } } + static void arithmetic(int n) { + if (n + Limits.max > 15) { + @Refinement("_ > 6") + int m = n; // Expect: Refinement Error + } + } + // a constant that cannot be represented is unknown, so the else-branch is still checked static void jdkEnumElse(DayOfWeek day, int n) { if (day == DayOfWeek.SUNDAY) {