From e6b7fd43e1f7468036a0e590f1ed7f94f31c9c62 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 28 Oct 2026 16:55:24 +0000 Subject: [PATCH] Scope the declaration of `return` in state refinement checks createStatePredicate declared `_` (the renamed `return`) and the `this` variables in the current context, outside any scope, and only when `_` was not declared yet. The first non-void method with a `to` fixed the type of `return` for every spec checked after it, and `!return` on a later boolean method crashed with "Expr cannot be cast to BoolExpr". Declare them in a scope of their own, always with the method's return type. Co-Authored-By: Claude Opus 5.5 --- .../AVectorRefinements.java | 16 ++++++++ .../BUndoManagerRefinements.java | 15 ++++++++ .../SimpleTest.java | 10 +++++ .../object_checkers/AuxStateHandler.java | 38 +++++++++++-------- 4 files changed, 63 insertions(+), 16 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/AVectorRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/BUndoManagerRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/SimpleTest.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/AVectorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/AVectorRefinements.java new file mode 100644 index 00000000..c328729a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/AVectorRefinements.java @@ -0,0 +1,16 @@ +package testSuite.classes.state_return_type_scope_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Checked before BUndoManagerRefinements: its return type (E) must not become the type of `return` there +@StateSet({"empty", "nonEmpty"}) +@ExternalRefinementsFor("java.util.Vector") +public interface AVectorRefinements { + @StateRefinement(to = "empty(this)") + public void Vector(); + + @StateRefinement(to = "nonEmpty(this)") + public E set(int index, E element); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/BUndoManagerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/BUndoManagerRefinements.java new file mode 100644 index 00000000..c4c92871 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/BUndoManagerRefinements.java @@ -0,0 +1,15 @@ +package testSuite.classes.state_return_type_scope_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"start", "canEdit"}) +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +public interface BUndoManagerRefinements { + @StateRefinement(to = "start(this)") + public void UndoManager(); + + @StateRefinement(from = "start(this)", to = "!return && start(this)") + public boolean canUndo(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/SimpleTest.java new file mode 100644 index 00000000..946fbe82 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_return_type_scope_correct/SimpleTest.java @@ -0,0 +1,10 @@ +package testSuite.classes.state_return_type_scope_correct; + +import javax.swing.undo.UndoManager; + +public class SimpleTest { + public static void main(String[] args) { + UndoManager manager = new UndoManager(); + boolean b = manager.canUndo(); + } +} 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 11a1f7e4..339584fa 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 @@ -309,22 +309,28 @@ private static Predicate createStatePredicate(Predicate p, String value, String } } CtTypeReference r = tc.getFactory().Type().createReference(targetClass); - String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); - String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); - tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e); - tc.getContext().addVarToContext(name, r, new Predicate(), e); - tc.getContext().addVarToContext(nameOld, r, new Predicate(), e); - if (returnType != null && !tc.getContext().hasVariable(Keys.WILDCARD)) - tc.getContext().addVarToContext(Keys.WILDCARD, returnType, new Predicate(), e); - // TODO REVIEW!! - // what is it for? - Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p; - Predicate c = c1.substituteVariable(Keys.THIS, name); - c = c.changeOldMentions(nameOld, name); - boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), position, true); - if (ok) - tc.throwStateConflictError(position, p); - return c1; + tc.getContext().enterContext(); + try { + String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); + String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); + tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e); + tc.getContext().addVarToContext(name, r, new Predicate(), e); + tc.getContext().addVarToContext(nameOld, r, new Predicate(), e); + // in this scope, so that each method's `return` has its own type + if (returnType != null) + tc.getContext().addVarToContext(Keys.WILDCARD, returnType, new Predicate(), e); + // TODO REVIEW!! + // what is it for? + Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p; + Predicate c = c1.substituteVariable(Keys.THIS, name); + c = c.changeOldMentions(nameOld, name); + boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), position, true); + if (ok) + tc.throwStateConflictError(position, p); + return c1; + } finally { + tc.getContext().exitContext(); + } } /**