Keep a static final constant's name in refinement errors

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

@@ -0,0 +1,21 @@
+package testSuite;
+
+import javax.imageio.ImageWriteParam;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorStaticFinalConstantName {
+
+    static void setProgressiveMode(@Refinement("_ != ImageWriteParam.MODE_EXPLICIT") int mode) {
+    }
+
+    static void direct() {
+        setProgressiveMode(ImageWriteParam.MODE_EXPLICIT); // Expect: Refinement Error
+    }
+
+    static void throughLocal() {
+        int mode = ImageWriteParam.MODE_EXPLICIT;
+        setProgressiveMode(mode); // Expect: Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -187,8 +187,11 @@ private static boolean isKnown(Pair<String, String> assignment, List<Expression>
                                 || states(binary.getSecondOperand(), binary.getFirstOperand(), assignment)));
     }
 
-    // An enum constant is written Format.JPG in found, either as such or as a variable, and JPG in the model
+    // An enum constant is written Format.JPG in found, either as such or as a variable, and JPG in the model; a static
+    // final constant keeps its name in found and is its value in the model
     private static boolean states(Expression term, Expression value, Pair<String, String> assignment) {
+        if (value instanceof Enum constant && constant.getResolvedLiteral() != null)
+            value = constant.getResolvedLiteral();
         String valueName = value instanceof Enum constant ? constant.getConstName()
                 : value instanceof Var var ? Utils.getSimpleName(var.getName()) : value.toString();
         return assignment.first().equals(termName(term)) && assignment.second().equals(valueName);

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java

@@ -23,9 +23,6 @@ protected Expression simplify(Expression expression, Void context) {
      * Folds the first foldable expression found
      */
     private Expression fold(Expression expression) {
-        // enum constant -> literal
-        if (expression instanceof Enum en && en.getResolvedLiteral() != null)
-            return en.getResolvedLiteral().clone();
         if (expression instanceof BinaryExpression binary)
             return foldBinary(binary);
         if (expression instanceof UnaryExpression unary)
@@ -51,7 +48,7 @@ private Expression foldBinary(BinaryExpression binary) {
 
         String op = binary.getOperator();
 
-        Expression foldedBinary = foldLiteralBinary(left, right, op);
+        Expression foldedBinary = foldLiteralBinary(valueOf(left), valueOf(right), op);
         if (foldedBinary != null)
             return foldedBinary;
 
@@ -72,17 +69,18 @@ private Expression foldUnary(UnaryExpression unary) {
             return new UnaryExpression(unary.getOp(), foldedOperand);
 
         String op = unary.getOp();
+        Expression value = valueOf(operand);
 
         // !true -> false
         // !false -> true
-        if ("!".equals(op) && operand instanceof LiteralBoolean literal)
+        if ("!".equals(op) && value instanceof LiteralBoolean literal)
             return new LiteralBoolean(!literal.isBooleanTrue());
 
         if ("-".equals(op)) {
             // -(x) -> -x
-            if (operand instanceof LiteralInt literal)
+            if (value instanceof LiteralInt literal)
                 return new LiteralInt(-literal.getValue());
-            if (operand instanceof LiteralReal literal)
+            if (value instanceof LiteralReal literal)
                 return new LiteralReal(-literal.getValue());
         }
 
@@ -97,7 +95,7 @@ private Expression foldIte(Ite ite) {
 
         // true ? x : y -> x
         // false ? x : y -> y
-        if (condition instanceof LiteralBoolean literal)
+        if (valueOf(condition)instanceof LiteralBoolean literal)
             return literal.isBooleanTrue() ? ite.getThen().clone() : ite.getElse().clone();
 
         Expression foldedCondition = fold(condition);
@@ -121,6 +119,14 @@ private Expression foldIte(Ite ite) {
         return new Ite(condition, thenExpression, elseExpression);
     }
 
+    /**
+     * The value of a static final constant, which only replaces its name when the expression around it folds, so a
+     * constant compared with a variable keeps the name the code or the spec wrote
+     */
+    private Expression valueOf(Expression expression) {
+        return expression instanceof Enum en && en.getResolvedLiteral() != null ? en.getResolvedLiteral() : expression;
+    }
+
     /**
      * Folds a binary expression whose operands are both literals
      */

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java

@@ -0,0 +1,43 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.Map;
+import java.util.TreeMap;
+
+import org.junit.jupiter.api.BeforeAll;
+import org.junit.jupiter.api.Test;
+
+import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.RefinementError;
+
+/** Checks that a static final constant the code passes is shown by its name, as the spec writes it */
+class TestStaticConstantNames {
+
+    private static final Map<Integer, RefinementError> ERRORS = new TreeMap<>();
+
+    @BeforeAll
+    static void verify() {
+        CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstantName.java");
+        for (LJError error : Diagnostics.getInstance().getErrors())
+            ERRORS.put(error.getPosition().getLine(), assertInstanceOf(RefinementError.class, error));
+    }
+
+    @Test
+    void constantPassedDirectlyKeepsItsName() {
+        assertShowsName(ERRORS.get(14));
+    }
+
+    @Test
+    void constantPassedThroughLocalKeepsItsName() {
+        assertShowsName(ERRORS.get(19));
+    }
+
+    private static void assertShowsName(RefinementError error) {
+        assertEquals("mode == ImageWriteParam.MODE_EXPLICIT is not a subtype of mode != ImageWriteParam.MODE_EXPLICIT",
+                error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
+        assertTrue(error.getCounterexample().isEmpty());
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java

@@ -6,6 +6,7 @@
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.ast.Var;
 import org.junit.jupiter.api.Test;
 
 class VCFoldingTest {
@@ -120,7 +121,7 @@ void foldsResolvedEnumLiterals() {
         VCImplication implication = new VCImplication(
                 new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3))));
 
-        assertSimplificationSteps(folding, implication, step("3 == 3"), step("true"));
+        assertSimplificationSteps(folding, implication, step("true"));
     }
 
     @Test
@@ -131,6 +132,15 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() {
         VCImplication implication = new VCImplication(
                 new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5))));
 
-        assertSimplificationSteps(folding, implication, step("3 + 2 == 5"), step("5 == 5"), step("true"));
+        assertSimplificationSteps(folding, implication, step("5 == 5"), step("true"));
+    }
+
+    @Test
+    void keepsResolvedEnumNameWhenNothingFolds() {
+        Enum mode = new Enum("ImageWriteParam", "MODE_EXPLICIT");
+        mode.setResolvedLiteral(new LiteralInt(2));
+        VCImplication implication = new VCImplication(new Predicate(new BinaryExpression(new Var("x"), "==", mode)));
+
+        assertSimplificationSteps(folding, implication, step("x == ImageWriteParam.MODE_EXPLICIT"));
     }
 }