Propagate typestate changes to must-aliases (#337)

A typestate transition creates a new instance of the variable it was made
through (`b#2` with `closed(b#2)`), but other variables bound to the same
object (`Res b = a;` gives `b#1 == a#1`) kept their old instance, so `a`
was still considered open after `b.close()`.

After a transition, every other reference variable of a related type whose
current instance is provably equal to the target's previous instance gets a
new instance equal to the transitioned one, so the new state is seen through
all must-aliases (including aliases of aliases and aliases created by a later
assignment). Reassigning the alias (`b = new Res()`) breaks the proved
equality, so later changes through it no longer affect the original.
Variables that may, but need not, alias the target keep their state.

Fixes #337

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

Author: CatarinaGamboa

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

@@ -0,0 +1,53 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class SeparateResource {
+    @StateRefinement(to = "open(this)")
+    public SeparateResource() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class CorrectStateChangeThroughAlias {
+    static void distinctObjects() {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = new SeparateResource();
+        b.close();
+        a.read();
+    }
+
+    static void reassignmentBreaksAlias() {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = a;
+        b = new SeparateResource();
+        b.close();
+        a.read();
+    }
+
+    static void aliasSeesOpenState() {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = a;
+        b.read();
+        a.read();
+        a.close();
+    }
+
+    static void aliasClosedInBothBranches(boolean done) {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = a;
+        if (done) {
+            b.close();
+        } else {
+            a.close();
+        }
+        SeparateResource c = new SeparateResource();
+        c.read();
+    }
+}

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

@@ -0,0 +1,50 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class AliasedResource {
+    @StateRefinement(to = "open(this)")
+    public AliasedResource() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class ErrorStateChangeThroughAlias {
+    static void localAlias() {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = a;
+        b.close();
+        a.read(); // Expect: State Refinement Error
+    }
+
+    static void aliasOfAlias() {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = a;
+        AliasedResource c = b;
+        a.close();
+        c.read(); // Expect: State Refinement Error
+    }
+
+    static void aliasAssignedLater() {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = new AliasedResource();
+        b = a;
+        b.close();
+        a.read(); // Expect: State Refinement Error
+    }
+
+    static void aliasClosedInBranch(boolean done) {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = a;
+        if (done) {
+            b.close();
+        }
+        a.read(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -618,6 +618,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
                 transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName);
                 // update of state of new instance of this#n#(whatever it was + 1)
                 addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation);
+                updateAliases(tc, name, vi, newInstanceName, invocation);
             }
         }
         if (!found) { // Reaches the end of stateChange no matching states
@@ -699,6 +700,54 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
         invocation.putMetadata(Keys.TARGET, vi2);
     }
 
+    /**
+     * A state change made through one reference changes the state of the object, so every other variable that must
+     * refer to the same object (e.g. {@code b} after {@code Res b = a;}) gets a new instance equal to the transitioned
+     * one. Variables that may, but need not, alias the target keep their state.
+     *
+     * @param tc
+     * @param name
+     *            the variable the state change was made through
+     * @param previous
+     *            the target instance before the state change
+     * @param transitioned
+     *            the name of the target instance after the state change
+     * @param invocation
+     */
+    private static void updateAliases(TypeChecker tc, String name, VariableInstance previous, String transitioned,
+            CtElement invocation) {
+        Context ctx = tc.getContext();
+        for (RefinedVariable rv : ctx.getCtxVars()) {
+            if (!(rv instanceof Variable alias) || alias.getName().equals(name) || !relatedTypes(alias, previous))
+                continue;
+            String current = alias.getLastInstance().map(Refined::getName).orElse(alias.getName());
+            Predicate identity = Predicate.createEquals(Predicate.createVar(current),
+                    Predicate.createVar(previous.getName()));
+            try {
+                if (!tc.checkStateSMT(new Predicate(), identity, invocation.getPosition(), true))
+                    continue;
+            } catch (LJError e) {
+                continue; // identity not provable: not a must-alias
+            }
+            String aliasInstanceName = String.format(Formats.INSTANCE, alias.getName(), ctx.getCounter());
+            RefinedVariable aliasInstance = ctx.addInstanceToContext(aliasInstanceName, alias.getType(),
+                    Predicate.createEquals(Predicate.createVar(aliasInstanceName), Predicate.createVar(transitioned)),
+                    invocation);
+            alias.getSuperTypes().forEach(aliasInstance::addSuperType);
+            ctx.addRefinementInstanceToVariable(alias.getName(), aliasInstanceName);
+        }
+    }
+
+    /** Whether one variable's type is the other's type or one of its recorded supertypes. */
+    private static boolean relatedTypes(RefinedVariable v1, RefinedVariable v2) {
+        if (v1.getType() == null || v2.getType() == null || v1.getType().isPrimitive() || v2.getType().isPrimitive())
+            return false;
+        String t1 = v1.getType().getQualifiedName();
+        String t2 = v2.getType().getQualifiedName();
+        return t1.equals(t2) || v1.getSuperTypes().stream().anyMatch(t -> t.getQualifiedName().equals(t2))
+                || v2.getSuperTypes().stream().anyMatch(t -> t.getQualifiedName().equals(t1));
+    }
+
     /** Whether the access denotes the receiver of the enclosing type, including unqualified super. */
     public static boolean isCurrentReceiver(CtElement target) {
         CtType<?> owner = target.getParent(CtType.class);