keep translation from final to literal value

Author: CatarinaGamboa

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

@@ -46,7 +46,10 @@ public String getCounterExampleString() {
 
         List<String> foundVarNames = new ArrayList<>();
         found.getValue().getVariableNames(foundVarNames);
-        List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
+        // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
+        // subtyping check, so the counterexample maps the symbolic name back to its compile-time value
+        found.getValue().getResolvedConstantNames(foundVarNames);
+        expected.getValue().getResolvedConstantNames(foundVarNames);
         String counterexampleString = counterexample.assignments().stream()
                 // only include variables that appear in the found value and are not already fixed there
                 .filter(a -> CommandLineLauncher.cmdArgs.debugMode || (foundVarNames.contains(a.first())

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

@@ -81,19 +81,21 @@ public Predicate(String ref, CtElement element, String prefix) throws LJError {
     }
 
     /**
-     * Walks {@code root}, replacing {@link Enum} nodes that resolve (via reflection, java.lang fallback, or imports
+     * Walks {@code root}, decorating {@link Enum} nodes that resolve (via reflection, java.lang fallback, or imports
      * declared in {@code context}'s compilation unit) to a {@code static final} primitive/String constant with the
-     * corresponding literal node. User-defined enums and unresolvable references are left untouched.
+     * corresponding literal expression via {@link Enum#setResolvedLiteral}. The AST shape is preserved, so error
+     * messages and counterexamples can render the symbolic {@code Type.CONST} form; the SMT translator emits the
+     * literal binding axiom from the decoration. User-defined enums and unresolvable-but-known-type references are left
+     * untouched (the SMT side handles them as user enum constants).
      */
     private static Expression resolveStaticFinalConstants(Expression root, CtElement context) throws LJError {
         List<Enum> enums = new ArrayList<>();
         collectEnums(root, enums);
-        Expression e = root;
         for (Enum en : enums) {
             Object v = StaticConstants.resolve(en.getTypeName(), en.getConstName(), context);
             Predicate lit = StaticConstants.asLiteralPredicate(v);
             if (lit != null) {
-                e = e.substitute(en, lit.getExpression());
+                en.setResolvedLiteral(lit.getExpression());
                 continue;
             }
             if (StaticConstants.userTypeExists(en.getTypeName(), context))
@@ -108,7 +110,7 @@ private static Expression resolveStaticFinalConstants(Expression root, CtElement
                             en.getTypeName(), en.getConstName(), hint),
                     pos);
         }
-        return e;
+        return root;
     }
 
     private static void collectEnums(Expression e, List<Enum> out) {

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java

@@ -9,6 +9,13 @@ public class Enum extends Expression {
 
     private final String typeName;
     private final String constName;
+    /**
+     * If this {@code Type.CONST} reference resolved to a Java {@code static final} primitive/String constant, the
+     * corresponding RJ literal expression is stashed here so the SMT translator can emit a binding axiom
+     * ({@code Type.CONST == literalValue}) while preserving the symbolic name in the AST. {@code null} for user-defined
+     * enum constants and for unresolvable references.
+     */
+    private Expression resolvedLiteral;
 
     public Enum(String typeName, String constName) {
         this.typeName = typeName;
@@ -23,6 +30,14 @@ public String getConstName() {
         return constName;
     }
 
+    public Expression getResolvedLiteral() {
+        return resolvedLiteral;
+    }
+
+    public void setResolvedLiteral(Expression resolvedLiteral) {
+        this.resolvedLiteral = resolvedLiteral;
+    }
+
     @Override
     public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
         return visitor.visitEnum(this);
@@ -69,6 +84,8 @@ public boolean equals(Object obj) {
 
     @Override
     public Expression clone() {
-        return new Enum(typeName, constName);
+        Enum c = new Enum(typeName, constName);
+        c.resolvedLiteral = resolvedLiteral == null ? null : resolvedLiteral.clone();
+        return c;
     }
 }

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java

@@ -25,6 +25,18 @@ public abstract class Expression {
 
     public abstract void getVariableNames(List<String> toAdd);
 
+    /**
+     * Collect dotted names ({@code Type.CONST}) of {@link Enum} nodes that have been resolved to a Java
+     * {@code static final} literal value. Used by the counterexample renderer to keep these constants in the displayed
+     * model even though they are not program variables.
+     */
+    public void getResolvedConstantNames(List<String> toAdd) {
+        if (this instanceof liquidjava.rj_language.ast.Enum en && en.getResolvedLiteral() != null)
+            toAdd.add(en.getTypeName() + "." + en.getConstName());
+        for (Expression c : getChildren())
+            c.getResolvedConstantNames(toAdd);
+    }
+
     public abstract void getStateInvocations(List<String> toAdd, List<String> all);
 
     public abstract boolean isBooleanTrue();

liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java

@@ -124,6 +124,8 @@ public Expr<?> visitUnaryExpression(UnaryExpression exp) throws LJError {
 
     @Override
     public Expr<?> visitEnum(Enum en) throws LJError {
+        if (en.getResolvedLiteral() != null)
+            return ctx.makeStaticConstant(en.getTypeName(), en.getConstName(), en.getResolvedLiteral().accept(this));
         return ctx.makeEnum(en.getTypeName(), en.getConstName());
     }
 }

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -42,6 +42,17 @@ public class TranslatorToZ3 implements AutoCloseable {
     private final Map<String, FuncDecl<?>> funcTranslation = new HashMap<>();
     private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
     private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
+    /**
+     * Z3 constants for resolved {@code static final} references (e.g. {@code Integer.MAX_VALUE}). Keyed by the dotted
+     * symbolic name so the same constant is reused across the query and the binding axiom is emitted once.
+     */
+    private final Map<String, Expr<?>> staticConstantTranslation = new HashMap<>();
+    /**
+     * Equality axioms binding each {@link #staticConstantTranslation} entry to its compile-time literal value.
+     * Conjoined into every solver built by {@link #makeSolverForExpression} so the constant is always pinned but still
+     * appears symbolically in counterexample models.
+     */
+    private final List<BoolExpr> staticConstantAxioms = new ArrayList<>();
 
     public TranslatorToZ3(liquidjava.processor.context.Context context) {
         TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
@@ -54,6 +65,8 @@ public TranslatorToZ3(liquidjava.processor.context.Context context) {
     @SuppressWarnings("unchecked")
     public Solver makeSolverForExpression(Expr<?> e) {
         Solver solver = z3.mkSolver();
+        for (BoolExpr axiom : staticConstantAxioms)
+            solver.add(axiom);
         solver.add((BoolExpr) e);
         return solver;
     }
@@ -128,6 +141,24 @@ public Expr<?> makeEnum(String enumTypeName, String enumConstantName) throws LJE
         return getVariableTranslation(varName);
     }
 
+    /**
+     * Declare (or look up) a Z3 constant named {@code Type.CONST} for a resolved Java {@code static final} reference,
+     * and emit a single equality axiom binding it to its compile-time literal value. Subsequent calls with the same
+     * name reuse the existing constant. The axiom is added to every solver built via {@link #makeSolverForExpression},
+     * so the constant always evaluates to its literal value while still appearing symbolically in error messages and
+     * counterexample models.
+     */
+    public Expr<?> makeStaticConstant(String typeName, String constName, Expr<?> literalValue) {
+        String name = String.format(Formats.ENUM, typeName, constName);
+        Expr<?> cached = staticConstantTranslation.get(name);
+        if (cached != null)
+            return cached;
+        Expr<?> constant = z3.mkConst(name, literalValue.getSort());
+        staticConstantTranslation.put(name, constant);
+        staticConstantAxioms.add(z3.mkEq(constant, literalValue));
+        return constant;
+    }
+
     public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws LJError {
         if (name.equals("addToIndex"))
             return makeStore(params);

liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java

@@ -27,9 +27,10 @@ private StaticConstants() {
      * Resolve a Spoon {@code static final} field reference to its compile-time value, so reads like
      * {@code Integer.MAX_VALUE} or {@code MyConfig.LIMIT} fold to literals before SMT translation.
      *
-     * <p>Tries the source AST first ({@link CtLiteral} initializer in Spoon's model), then reflection via
-     * {@link CtFieldReference#getActualField()} + {@link #readStaticFinal}. Returns {@code null} if the field
-     * isn't static-final, has a non-literal initializer, or any lookup step fails.
+     * <p>
+     * Tries the source AST first ({@link CtLiteral} initializer in Spoon's model), then reflection via
+     * {@link CtFieldReference#getActualField()} + {@link #readStaticFinal}. Returns {@code null} if the field isn't
+     * static-final, has a non-literal initializer, or any lookup step fails.
      *
      * @see #resolve(String, String, CtElement) sibling for refinement-string {@code Type.CONST} references
      */
@@ -146,9 +147,10 @@ public static Predicate asLiteralPredicate(Object value) {
      * {@code lookup("java.lang.Integer", "MAX_VALUE")} returns {@code 2147483647}, which is how
      * {@code Integer.MAX_VALUE} gets baked into the AST before SMT translation.
      *
-     * <p>Returns {@code null} on any failure ({@link ClassNotFoundException}, {@link NoSuchFieldException},
-     * {@link LinkageError}, {@link SecurityException}, or non-static-final) so callers can fall through to the
-     * next resolution strategy without a try/catch. Only public fields are visible to {@link Class#getField}.
+     * <p>
+     * Returns {@code null} on any failure ({@link ClassNotFoundException}, {@link NoSuchFieldException},
+     * {@link LinkageError}, {@link SecurityException}, or non-static-final) so callers can fall through to the next
+     * resolution strategy without a try/catch. Only public fields are visible to {@link Class#getField}.
      */
     private static Object lookup(String className, String fieldName) {
         try {