Forget non-final field initializers inside methods (#340)

A field initializer's instance stayed the field's last instance for the
whole class, so every method read a non-final field as if it still held
its initializer, although any other method (e.g. a setter) may have
reassigned it. Passing such a field to a refined parameter was accepted.

On entry to a method (constructors are unchanged), each non-final field
with a recorded value gets a fresh instance carrying only its declared
refinement. Final fields keep their initializer. Assignments made inside
the method are still tracked as before.

The field cases of the deferred-callback fixtures relied on the
initializer state of a non-final field in a method; they now check that
state in the constructor, where it does hold, so they keep testing that
creating a callback does not run it.

Fixes #340

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

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

@@ -20,7 +20,8 @@ class CorrectDeferredCallbackState {
     UndoManager manager = new UndoManager();
     Runnable listener = () -> { manager.addEdit(null); };
 
-    void fieldCallbackMayNeverRun() {
+    CorrectDeferredCallbackState() {
+        // the field callback may never run: the initializer state still holds in the constructor
         manager.discardAllEdits();
     }
 

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

@@ -0,0 +1,39 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectMutableFieldInitializer {
+    private final float fixed = 0.75f;
+
+    @Refinement("_ >= 0.0 && _ <= 1.0")
+    private float refined = 0.75f;
+
+    private float local = 0.75f;
+
+    public CorrectMutableFieldInitializer() {
+        use(local);
+    }
+
+    public void setRefined(@Refinement("_ >= 0.0 && _ <= 1.0") float v) {
+        this.refined = v;
+    }
+
+    public void setLocal(float v) {
+        this.local = v;
+    }
+
+    static void use(@Refinement("_ >= 0.0 && _ <= 1.0") float quality) {}
+
+    void writeFixed() {
+        use(fixed);
+    }
+
+    void writeRefined() {
+        use(refined);
+    }
+
+    void writeAfterAssignment() {
+        local = 0.5f;
+        use(local);
+    }
+}

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

@@ -23,9 +23,6 @@ class ErrorAnonymousCallbackState {
         Runnable listener = new Runnable() {
             public void run() { manager.addEdit(null); }
         };
-    }
-
-    void undo() {
         manager.undo(); // Expect: State Refinement Error
     }
 }
@@ -42,7 +39,7 @@ class ErrorFieldLambdaCallbackState {
     UndoManager manager = new UndoManager();
     Runnable listener = () -> { manager.addEdit(null); };
 
-    void undo() {
+    ErrorFieldLambdaCallbackState() {
         manager.undo(); // Expect: State Refinement Error
     }
 }

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

@@ -0,0 +1,55 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class FieldResource {
+    @StateRefinement(to = "open(this)")
+    public FieldResource() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class ErrorMutableFieldInitializer {
+    private float q = 0.75f;
+    private static int count = 1;
+    private FieldResource resource = new FieldResource();
+
+    public void setQ(float v) {
+        this.q = v;
+    }
+
+    public static void setCount(int c) {
+        count = c;
+    }
+
+    static void use(@Refinement("_ >= 0.0 && _ <= 1.0") float quality) {}
+
+    static void positive(@Refinement("_ > 0") int n) {}
+
+    void write() {
+        use(q); // Expect: Refinement Error
+    }
+
+    void writeThis() {
+        use(this.q); // Expect: Refinement Error
+    }
+
+    static void report() {
+        positive(count); // Expect: Refinement Error
+    }
+
+    void closeResource() {
+        resource.close(); // Expect: State Refinement Error
+    }
+
+    void readResource() {
+        resource.read(); // Expect: State Refinement Error
+    }
+}

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

@@ -142,6 +142,7 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         context.clearInstanceVariables();
         context.enterContext();
         context.restoreInstanceVariables();
+        forgetMutableFieldValues(method.getDeclaringType());
         if (!method.getSignature().equals("main(java.lang.String[])")) {
             mfc.loadFunctionInfo(method);
         }
@@ -155,6 +156,25 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         vcChecker.clearPathVariables();
     }
 
+    /**
+     * Any method may have reassigned a non-final field before this one runs, so inside a method a non-final field
+     * carries only its declared refinement, not the value of its initializer. Final fields keep their value.
+     */
+    private void forgetMutableFieldValues(CtType<?> type) {
+        if (type == null)
+            return;
+        for (CtField<?> f : type.getFields()) {
+            String name = Utils.qualifyFieldName(f.getReference());
+            if (f.isFinal() || !(context.getVariableByName(name)instanceof Variable field)
+                    || field.getLastInstance().isEmpty())
+                continue;
+            String instanceName = String.format(Formats.INSTANCE, name, context.getCounter());
+            context.addInstanceToContext(instanceName, field.getType(),
+                    field.getMainRefinement().substituteVariable(name, instanceName), f);
+            context.addRefinementInstanceToVariable(name, instanceName);
+        }
+    }
+
     @Override
     public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
         super.visitCtLocalVariable(localVariable);