Keep the meaning of enum and static constants compared in conditions

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

@@ -0,0 +1,128 @@
+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 until #307 is fixed
+        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 void onlyGif(@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 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;
+        }
+    }
+
+    // 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);
+    }
+}

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

@@ -0,0 +1,96 @@
+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 until #307 is fixed
+    }
+
+    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 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")
+            int m = n; // Expect: Refinement Error
+        }
+    }
+
+    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) {
+            n = 1;
+        } else {
+            @Refinement("_ > 0")
+            int m = n; // Expect: Refinement Error
+        }
+    }
+}

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

@@ -301,7 +301,8 @@ public <T> void visitCtFieldRead(CtFieldRead<T> 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,

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();