From a415821e47a1279e6496eca785facf9a5faad4db Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:19:35 +0100 Subject: [PATCH 1/2] 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 --- .../CorrectStateChangeThroughAlias.java | 53 +++++++++++++++++++ .../ErrorStateChangeThroughAlias.java | 50 +++++++++++++++++ .../object_checkers/AuxStateHandler.java | 49 +++++++++++++++++ 3 files changed, 152 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStateChangeThroughAlias.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateChangeThroughAlias.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateChangeThroughAlias.java b/liquidjava-example/src/main/java/testSuite/CorrectStateChangeThroughAlias.java new file mode 100644 index 00000000..26d3a7a6 --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateChangeThroughAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorStateChangeThroughAlias.java new file mode 100644 index 00000000..88c788ce --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 4ad7852f..5d1fbf49 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/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); From 456ae109c960ca4a241596149459b670c1da0ca8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:46:29 +0100 Subject: [PATCH 2/2] 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 --- .../CorrectDeferredCallbackState.java | 3 +- .../CorrectMutableFieldInitializer.java | 39 +++++++++++++ .../testSuite/ErrorDeferredCallbackState.java | 5 +- .../ErrorMutableFieldInitializer.java | 55 +++++++++++++++++++ .../RefinementTypeChecker.java | 20 +++++++ 5 files changed, 117 insertions(+), 5 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectMutableFieldInitializer.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorMutableFieldInitializer.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java b/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java index dc51fa32..51d30841 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java +++ b/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(); } diff --git a/liquidjava-example/src/main/java/testSuite/CorrectMutableFieldInitializer.java b/liquidjava-example/src/main/java/testSuite/CorrectMutableFieldInitializer.java new file mode 100644 index 00000000..e5017087 --- /dev/null +++ b/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); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java b/liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java index c49e2471..3e495427 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java +++ b/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 } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMutableFieldInitializer.java b/liquidjava-example/src/main/java/testSuite/ErrorMutableFieldInitializer.java new file mode 100644 index 00000000..a88bd71a --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 995c5927..d4dd75b5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -142,6 +142,7 @@ public void visitCtMethod(CtMethod 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 void visitCtMethod(CtMethod 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 void visitCtLocalVariable(CtLocalVariable localVariable) { super.visitCtLocalVariable(localVariable);