From aa250a326cc91a9cfcba69ce151ffc8f9352aa9b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Nov 2026 18:41:50 +0000 Subject: [PATCH 1/7] Give state hints when the state set or methods come from the receiver's supertypes Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateHintInheritedStates.java | 30 ++++ .../testSuite/ErrorStateHintOverride.java | 30 ++++ .../testSuite/ErrorStateHintSubclass.java | 2 +- .../Use.java | 12 ++ .../WindowRefinements.java | 25 +++ .../Use.java | 11 ++ .../WindowRefinements.java | 28 ++++ .../Use.java | 11 ++ .../WindowRefinements.java | 25 +++ .../AuxHierarchyRefinementsPassage.java | 6 +- .../object_checkers/AuxStateHandler.java | 39 +++-- .../state_machine/StateMachineBuilder.java | 154 +++++++++++++++--- .../liquidjava/api/tests/TestStateHints.java | 39 +++++ 13 files changed, 372 insertions(+), 40 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintInheritedStates.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintOverride.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/Use.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/WindowRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/Use.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/WindowRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/Use.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/WindowRefinements.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintInheritedStates.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintInheritedStates.java new file mode 100644 index 000000000..08ef9899a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintInheritedStates.java @@ -0,0 +1,30 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"a", "b", "c"}) +public class ErrorStateHintInheritedStates { + + @StateRefinement(to = "a(this)") + public ErrorStateHintInheritedStates() {} + + @StateRefinement(from = "a(this)", to = "b(this)") + public void ab() {} + + @StateRefinement(from = "c(this)") + public void useC() {} + + public static void use() { + ErrorStateHintInheritedStatesChild s = new ErrorStateHintInheritedStatesChild(); + s.ab(); + s.useC(); // Expect: State Refinement Error + } +} + +// adds a transition to the states it inherits +class ErrorStateHintInheritedStatesChild extends ErrorStateHintInheritedStates { + + @StateRefinement(from = "b(this)", to = "c(this)") + public void bc() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintOverride.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintOverride.java new file mode 100644 index 000000000..f363db9ed --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintOverride.java @@ -0,0 +1,30 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"a", "b", "c"}) +public class ErrorStateHintOverride { + + @StateRefinement(to = "a(this)") + public ErrorStateHintOverride() {} + + @StateRefinement(from = "a(this)", to = "b(this) || c(this)") + public void next() {} + + @StateRefinement(from = "c(this)") + public void useC() {} + + public static void use() { + ErrorStateHintOverrideChild s = new ErrorStateHintOverrideChild(); + s.useC(); // Expect: State Refinement Error + } +} + +// the override always moves to c, which the superclass's refinement does not promise +class ErrorStateHintOverrideChild extends ErrorStateHintOverride { + + @Override + @StateRefinement(from = "a(this)", to = "c(this)") + public void next() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java index b8fa2cde1..7024cd76c 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java @@ -16,7 +16,7 @@ public void ab() {} public void useC() {} public static void use() { - ErrorStateHintSubclassChild s = new ErrorStateHintSubclassChild(); + ErrorStateHintSubclass s = new ErrorStateHintSubclassChild(); s.ab(); s.useC(); // Expect: State Refinement Error } diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/Use.java new file mode 100644 index 000000000..46ad67656 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/Use.java @@ -0,0 +1,12 @@ +package testSuite.classes.state_hints_grandchild_spec_error; + +import javax.swing.JFrame; + +// JFrame has no spec: its state set comes from Window's, and setUndecorated from Frame's +public class Use { + static void borderless() { + JFrame window = new JFrame("Playfield"); + window.pack(); + window.setUndecorated(true); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/WindowRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/WindowRefinements.java new file mode 100644 index 000000000..72254f4bd --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/WindowRefinements.java @@ -0,0 +1,25 @@ +package testSuite.classes.state_hints_grandchild_spec_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +public interface WindowRefinements { + @StateRefinement(to = "notDisplayable(this)") + void dispose(); + + @StateRefinement(to = "displayable(this)") + void pack(); +} + +// the state set is declared in the superclass's spec +@ExternalRefinementsFor("java.awt.Frame") +interface FrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Frame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/Use.java new file mode 100644 index 000000000..7e159f2e1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/Use.java @@ -0,0 +1,11 @@ +package testSuite.classes.state_hints_redeclared_method_error; + +import java.awt.Frame; + +public class Use { + static void borderless() { + Frame host = new Frame("Playfield"); + host.pack(); + host.setUndecorated(true); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/WindowRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/WindowRefinements.java new file mode 100644 index 000000000..183cd55a0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/WindowRefinements.java @@ -0,0 +1,28 @@ +package testSuite.classes.state_hints_redeclared_method_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +public interface WindowRefinements { + @StateRefinement(to = "notDisplayable(this)") + void dispose(); + + @StateRefinement(to = "displayable(this)") + void pack(); + + // Frame redeclares addNotify, so on a Frame the verifier does not apply this refinement + @StateRefinement(to = "displayable(this)") + void addNotify(); +} + +@ExternalRefinementsFor("java.awt.Frame") +interface FrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Frame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/Use.java new file mode 100644 index 000000000..e71790058 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/Use.java @@ -0,0 +1,11 @@ +package testSuite.classes.state_hints_superclass_spec_error; + +import java.awt.Frame; + +public class Use { + static void borderless() { + Frame host = new Frame("Playfield"); + host.pack(); + host.setUndecorated(true); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/WindowRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/WindowRefinements.java new file mode 100644 index 000000000..782afea87 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/WindowRefinements.java @@ -0,0 +1,25 @@ +package testSuite.classes.state_hints_superclass_spec_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +public interface WindowRefinements { + @StateRefinement(to = "notDisplayable(this)") + void dispose(); + + @StateRefinement(to = "displayable(this)") + void pack(); +} + +// the state set is declared in the superclass's spec +@ExternalRefinementsFor("java.awt.Frame") +interface FrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Frame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 2b391cef9..f974424fd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java @@ -139,7 +139,7 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi ObjectState subState = subStates.get(i); String thisName = String.format(Formats.FRESH, tc.getContext().getCounter()); - createVariableInContext(thisName, tc, subFunction, superFunction, method.getParameters().get(i)); + createVariableInContext(thisName, tc, subFunction, superFunction, method); Predicate superConst = matchVariableNames(thisName, superState.getFrom()); Predicate subConst = matchVariableNames(thisName, superFunction, subFunction, subState.getFrom()); @@ -164,9 +164,9 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi } private static void createVariableInContext(String thisName, TypeChecker tc, RefinedFunction subFunction, - RefinedFunction superFunction, CtParameter ctParameter) { + RefinedFunction superFunction, CtMethod method) { RefinedVariable rv = tc.getContext().addVarToContext(thisName, - Utils.getType(subFunction.getTargetClass(), tc.getFactory()), new Predicate(), ctParameter); + Utils.getType(subFunction.getTargetClass(), tc.getFactory()), new Predicate(), method); rv.addSuperType(Utils.getType(superFunction.getTargetClass(), tc.getFactory())); // TODO: change: this only // works for one superclass } 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 6d17712b6..16872d873 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 @@ -793,14 +793,13 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc .orElse(function.getPlacementInCode().getPosition()); List ghostStates = getGhostStatesFor(function.getTargetClass(), tc); Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); - Optional states = receiverStates(tc, function, instanceName, prevState, invocation); + Optional states = receiverStates(tc, function, vi, prevState, invocation); Predicate expected = expectedStatesDisjunction; boolean checked = deciding.isEmpty() && states - .map(r -> checkedElsewhere(tc, r, prevState, expected, instanceName, ghostStates, invocation)) - .orElse(false); - ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE : states.flatMap( - r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, checked, ghostStates)) - .orElse(null); + .map(r -> checkedElsewhere(tc, r, prevState, expected, instanceName, invocation)).orElse(false); + ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE + : states.flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, checked, + StateMachineBuilder.ghostStatesOf(tc, r.className()))).orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() : states.map(r -> stateHints(r, function, category, checked, invocation)).orElse(List.of()); @@ -813,7 +812,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc } /** The state machine of the receiver's class and the states the receiver can be in before a call */ - private record ReceiverStates(StateMachine machine, Set current) { + private record ReceiverStates(String className, StateMachine machine, Set current) { } /** @@ -821,14 +820,15 @@ private record ReceiverStates(StateMachine machine, Set current) { * cannot be computed, the error is reported without hints or category */ private static Optional receiverStates(TypeChecker tc, RefinedFunction function, - String instanceName, Predicate state, CtElement invocation) { + VariableInstance receiver, Predicate state, CtElement invocation) { try { - Optional machine = tc.getStateMachine(function.getTargetClass(), invocation); + String className = receiverClass(tc, function, receiver); + Optional machine = tc.getStateMachine(className, invocation); if (machine.isEmpty()) return Optional.empty(); Set current = new StateSolver(tc, invocation.getPosition()).possibleStates(machine.get().states(), - state, instanceName); - return Optional.of(new ReceiverStates(machine.get(), current)); + state, receiver.getName()); + return Optional.of(new ReceiverStates(className, machine.get(), current)); } catch (RuntimeException e) { // a failure to analyse the states must not replace the error being reported DebugLog.warn("Could not compute the receiver's states: " + e.getMessage()); @@ -838,10 +838,11 @@ private static Optional receiverStates(TypeChecker tc, RefinedFu /** Best effort, like {@link #receiverStates}: see {@link StateErrorCategories#checkedElsewhere} */ private static boolean checkedElsewhere(TypeChecker tc, ReceiverStates states, Predicate found, Predicate expected, - String instanceName, List ghostStates, CtElement invocation) { + String instanceName, CtElement invocation) { try { return StateErrorCategories.checkedElsewhere(states.machine(), states.current(), found, - () -> tc.shownFound(found, expected), instanceName, ghostStates, + () -> tc.shownFound(found, expected), instanceName, + StateMachineBuilder.ghostStatesOf(tc, states.className()), new StateSolver(tc, invocation.getPosition())); } catch (RuntimeException e) { DebugLog.warn("Could not tell whether the receiver's state was checked: " + e.getMessage()); @@ -849,6 +850,18 @@ private static boolean checkedElsewhere(TypeChecker tc, ReceiverStates states, P } } + /** + * The class whose machine explains the call: the receiver's own type, which inherits the state sets and methods of + * its supertypes, or the class the method is specified for if the receiver's type is not one of its subtypes + */ + private static String receiverClass(TypeChecker tc, RefinedFunction function, VariableInstance receiver) { + String target = function.getTargetClass(); + CtTypeReference type = receiver.getType(); + if (type == null || type.isPrimitive() || type.getQualifiedName().equals(target)) + return target; + return type.isSubtypeOf(tc.getFactory().Type().createReference(target)) ? type.getQualifiedName() : target; + } + /** Best effort, like {@link #receiverStates} */ private static Optional decidingArgument(TypeChecker tc, VariableInstance receiver, RefinedFunction function, List ghostStates, CtElement invocation) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 053148490..07d5f54c2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -1,6 +1,9 @@ package liquidjava.processor.state_machine; +import java.util.ArrayDeque; import java.util.ArrayList; +import java.util.Deque; +import java.util.HashSet; import java.util.LinkedHashMap; import java.util.List; import java.util.Map; @@ -11,7 +14,6 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; -import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.context.ObjectState; import liquidjava.processor.context.RefinedFunction; @@ -27,11 +29,11 @@ import spoon.reflect.reference.CtTypeReference; /** - * Builds the {@link StateMachine} of a class from its {@code @StateSet}s and {@code @StateRefinement}s. Every - * transition is proven by the SMT solver, so the machine never contains a call that would not verify. Methods whose - * state refinements mention anything besides the states of {@code this} (parameters, return values, other ghosts) are - * left out, and the machine is then marked incomplete, as it is when a superclass or subclass has state refinements of - * its own. + * Builds the {@link StateMachine} of a class from its {@code @StateSet}s and {@code @StateRefinement}s, and those of + * its supertypes, which it inherits. Every transition is proven by the SMT solver, so the machine never contains a call + * that would not verify. Methods whose state refinements mention anything besides the states of {@code this} + * (parameters, return values, other ghosts) are left out, and the machine is then marked incomplete, as it is when a + * subclass has state refinements of its own or an inherited refinement may not be the one the verifier applies. */ public class StateMachineBuilder { @@ -68,21 +70,78 @@ public static boolean canModel(RefinedFunction function) { */ public static Optional build(TypeChecker tc, StateSolver solver, String className, CtElement element) throws LJError { - List states = statesOf(tc.getContext(), className, false); + CtTypeReference type = tc.getFactory().Type().createReference(className); + List> supertypes = supertypesOf(type); + List states = statesOf(ghostStatesOf(tc.getContext(), type, supertypes), false); if (states.isEmpty() || states.size() > MAX_STATES) return Optional.empty(); Context context = tc.getContext(); context.enterContext(); try { - CtTypeReference type = tc.getFactory().Type().createReference(className); context.addVarToContext(BEFORE, type, new Predicate(), element); context.addVarToContext(AFTER, type, new Predicate(), element); - return Optional.of(new StateMachineBuilder(tc, solver, states).build(className, type)); + return Optional.of(new StateMachineBuilder(tc, solver, states).build(type, supertypes)); } finally { context.exitContext(); } } + /** The ghost states of {@code className} and of its supertypes, which its objects also have */ + public static List ghostStatesOf(TypeChecker tc, String className) { + CtTypeReference type = tc.getFactory().Type().createReference(className); + return ghostStatesOf(tc.getContext(), type, supertypesOf(type)); + } + + private static List ghostStatesOf(Context context, CtTypeReference type, + List> supertypes) { + // a state set can be registered more than once, so states are told apart by name + Map ghostStates = new LinkedHashMap<>(); + for (CtTypeReference t : Stream.concat(Stream.of(type), supertypes.stream()).toList()) { + List declared = context.getGhostState(Utils.getSimpleName(t.getQualifiedName())); + if (declared != null) + declared.forEach(g -> ghostStates.putIfAbsent(g.getQualifiedName(), g)); + } + return List.copyOf(ghostStates.values()); + } + + /** Every supertype of {@code type}, nearest first: its superclasses, then the interfaces they implement */ + private static List> supertypesOf(CtTypeReference type) { + List> superclasses = new ArrayList<>(); + Deque> interfaces = new ArrayDeque<>(); + Set seen = new HashSet<>(Set.of(type.getQualifiedName())); + for (CtTypeReference t = type; t != null; t = superclassOf(t)) { + if (t != type && seen.add(t.getQualifiedName())) + superclasses.add(t); + interfaces.addAll(superInterfacesOf(t)); + } + List> supertypes = new ArrayList<>(superclasses); + while (!interfaces.isEmpty()) { + CtTypeReference t = interfaces.poll(); + if (seen.add(t.getQualifiedName())) { + supertypes.add(t); + interfaces.addAll(superInterfacesOf(t)); + } + } + return supertypes; + } + + // a supertype that cannot be resolved (no source, not on the classpath) ends the walk on that branch + private static CtTypeReference superclassOf(CtTypeReference type) { + try { + return type.getSuperclass(); + } catch (RuntimeException e) { + return null; + } + } + + private static Set> superInterfacesOf(CtTypeReference type) { + try { + return type.getSuperInterfaces(); + } catch (RuntimeException e) { + return Set.of(); + } + } + /** * Every combination of one state from each state set of the class * @@ -92,10 +151,12 @@ public static Optional build(TypeChecker tc, StateSolver solver, S */ public static List statesOf(Context context, String className, boolean withNone) { List ghostStates = context.getGhostState(Utils.getSimpleName(className)); - if (ghostStates == null) - return List.of(); - Map> stateSets = ghostStates.stream().filter(g -> g.getParent() != null) - .collect(Collectors.groupingBy(GhostState::getParent, LinkedHashMap::new, Collectors.toList())); + return ghostStates == null ? List.of() : statesOf(ghostStates, withNone); + } + + private static List statesOf(List ghostStates, boolean withNone) { + Map> stateSets = ghostStates.stream().filter(g -> g.getParent() != null).collect( + Collectors.groupingBy(g -> g.getParent().getQualifiedName(), LinkedHashMap::new, Collectors.toList())); if (stateSets.isEmpty()) return List.of(); @@ -125,21 +186,34 @@ private static State combine(State state, State inSet) { return new State(names, Predicate.createConjunction(state.predicate(), inSet.predicate())); } - private StateMachine build(String className, CtTypeReference type) throws LJError { + private StateMachine build(CtTypeReference type, List> supertypes) throws LJError { + String className = type.getQualifiedName(); + Set inherited = supertypes.stream().map(CtTypeReference::getQualifiedName).collect(Collectors.toSet()); List methods = new ArrayList<>(); List transitions = new ArrayList<>(); Map> constructors = new LinkedHashMap<>(); - boolean complete = !relatedClassChangesState(className, type); + boolean complete = !subclassChangesState(className, type, inherited); for (RefinedFunction function : tc.getContext().getCtxFunctions()) { - if (!className.equals(function.getTargetClass()) || !function.hasStateChange()) + if (!function.hasStateChange()) continue; - if (CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())) { + boolean constructor = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName()); + if (className.equals(function.getTargetClass()) && constructor) { if (abstractType(type) || privateConstructor(function, type)) continue; // cannot be suggested as a new object Optional> created = createdStates(function); created.ifPresent(s -> constructors.put(function, s)); continue; } + if (!className.equals(function.getTargetClass())) { + if (constructor || !inherited.contains(function.getTargetClass())) + continue; + if (overridden(function, className)) + continue; // the class's own refinement for it is the one in the machine + if (!inheritedFrom(function, type, supertypes)) { + complete = false; + continue; + } + } Optional> calls = transitionsOf(function); if (calls.isPresent()) { methods.add(function); @@ -151,12 +225,46 @@ private StateMachine build(String className, CtTypeReference type) throws LJE return new StateMachine(states, methods, transitions, constructors, complete); } - /** Whether a superclass or subclass has state refinements of its own, which the machine does not include */ - private boolean relatedClassChangesState(String className, CtTypeReference type) { + /** Whether a subclass has state refinements of its own, which the machine does not include */ + private boolean subclassChangesState(String className, CtTypeReference type, Set inherited) { return tc.getContext().getCtxFunctions().stream().filter(RefinedFunction::hasStateChange) - .map(RefinedFunction::getTargetClass).filter(c -> c != null && !c.equals(className)).distinct() - .map(c -> tc.getFactory().Type().createReference(c)) - .anyMatch(other -> other.isSubtypeOf(type) || type.isSubtypeOf(other)); + .map(RefinedFunction::getTargetClass) + .filter(c -> c != null && !c.equals(className) && !inherited.contains(c)).distinct() + .map(c -> tc.getFactory().Type().createReference(c)).anyMatch(other -> other.isSubtypeOf(type)); + } + + /** Whether {@code className} has its own refinement for {@code method}, with the same parameter types */ + private boolean overridden(RefinedFunction method, String className) { + String name = Utils.getSimpleName(method.getName()); + List parameters = parameterTypes(method); + return tc.getContext().getCtxFunctions().stream().anyMatch(f -> className.equals(f.getTargetClass()) + && name.equals(Utils.getSimpleName(f.getName())) && parameters.equals(parameterTypes(f))); + } + + private static List parameterTypes(RefinedFunction function) { + return function.getArguments().stream().map(a -> typeName(a.getType())).toList(); + } + + /** + * Whether the verifier checks a call to {@code method}, specified for a supertype, on an object of {@code type} + * that has no refinement of its own for it. Like the verifier, it uses the refinement for the nearest type that + * declares the method. Methods are matched by name and number of parameters, so an overload can hide an inherited + * method, which only leaves the machine incomplete. + */ + private boolean inheritedFrom(RefinedFunction method, CtTypeReference type, + List> supertypes) { + String name = Utils.getSimpleName(method.getName()); + int arity = method.getArguments().size(); + for (CtTypeReference t : Stream.concat(Stream.of(type), supertypes.stream()).toList()) { + CtType declaration = t.getTypeDeclaration(); + if (declaration == null) + return false; // cannot tell which type declares it + boolean declares = declaration.getMethods().stream() + .anyMatch(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity); + if (declares) + return t.getQualifiedName().equals(method.getTargetClass()); + } + return false; } private static boolean abstractType(CtTypeReference type) { @@ -176,7 +284,7 @@ private static boolean privateConstructor(RefinedFunction constructor, CtTypeRef return true; if (!(declaration instanceof CtClass declared)) return false; - List parameters = constructor.getArguments().stream().map(a -> typeName(a.getType())).toList(); + List parameters = parameterTypes(constructor); return declared.getConstructors().stream() .filter(c -> c.getParameters().stream().map(p -> typeName(p.getType())).toList().equals(parameters)) .anyMatch(CtModifiable::isPrivate); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index ce9eded21..d986ffbb6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -60,6 +60,45 @@ void subclassTransitionsPreventClaimingStateIsUnreachable() { assertHints("ErrorStateHintSubclass.java"); } + @Test + void subclassReceiverCanUseItsOwnTransitionsOnInheritedStates() { + assertHints("ErrorStateHintInheritedStates.java", + new Hint(Kind.CALL_SEQUENCE, "Call s.bc() before this call to move s from b to c"), + new Hint(Kind.AVAILABLE_CALLS, "In state b, s can call: bc()")); + } + + @Test + void overrideInTheReceiversClassReplacesTheInheritedTransition() { + assertHints("ErrorStateHintOverride.java", + new Hint(Kind.CALL_SEQUENCE, "Call s.next() before this call to move s from a to c"), + new Hint(Kind.AVAILABLE_CALLS, "In state a, s can call: next()")); + } + + @Test + void stateSetAndMethodsFromSpecsOfTheReceiversSuperclasses() { + assertHints("classes/state_hints_grandchild_spec_error", + new Hint(Kind.CALL_SEQUENCE, + "Call window.dispose() before this call to move window from displayable to notDisplayable"), + new Hint(Kind.AVAILABLE_CALLS, "In state displayable, window can call: dispose(), pack()")); + } + + @Test + void superclassRefinementOfAMethodTheReceiversClassRedeclaresIsNotSuggested() { + assertHints("classes/state_hints_redeclared_method_error", + new Hint(Kind.CALL_SEQUENCE, + "Call host.dispose() before this call to move host from displayable to notDisplayable"), + new Hint(Kind.AVAILABLE_CALLS, + "In state displayable, host can call: dispose(), pack() (and possibly others)")); + } + + @Test + void stateSetAndMethodsFromTheReceiversSuperclassSpec() { + assertHints("classes/state_hints_superclass_spec_error", + new Hint(Kind.CALL_SEQUENCE, + "Call host.dispose() before this call to move host from displayable to notDisplayable"), + new Hint(Kind.AVAILABLE_CALLS, "In state displayable, host can call: dispose(), pack()")); + } + @Test void stateDependingOnThePathAsksForTheSameStateOnEveryPath() { assertHints("ErrorStateHintPathDependent.java", new Hint(Kind.PATH_DEPENDENT_STATE, From dabe96419e0a6d5d46d02f72957f2b163fee7ada Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Nov 2026 19:57:58 +0000 Subject: [PATCH 2/7] Leave out refinements the verifier would not apply and states of same-named classes Co-Authored-By: Claude Opus 5.5 --- .../StackRefinements.java | 19 ++++++++++ .../Use.java | 10 ++++++ .../ArrayListRefinements.java | 18 ++++++++++ .../Collection.java | 14 ++++++++ .../Use.java | 10 ++++++ .../diagnostics/hints/StateHints.java | 3 +- .../state_machine/StateMachineBuilder.java | 36 ++++++++++++++----- .../liquidjava/api/tests/TestStateHints.java | 12 +++++++ 8 files changed, 112 insertions(+), 10 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/StackRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/Use.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/ArrayListRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Collection.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Use.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/StackRefinements.java new file mode 100644 index 000000000..d402fccda --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/StackRefinements.java @@ -0,0 +1,19 @@ +package testSuite.classes.state_hints_generic_inherited_method_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"empty", "nonEmpty"}) +@ExternalRefinementsFor("java.util.Stack") +public interface StackRefinements { + @StateRefinement(to = "empty(this)") + void Stack(); + + // Stack inherits add from Vector, and the verifier does not find this refinement for a call to it + @StateRefinement(to = "nonEmpty(this)") + boolean add(E e); + + @StateRefinement(from = "nonEmpty(this)") + E pop(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/Use.java new file mode 100644 index 000000000..b938bf719 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/Use.java @@ -0,0 +1,10 @@ +package testSuite.classes.state_hints_generic_inherited_method_error; + +import java.util.Stack; + +public class Use { + static void popEmpty() { + Stack s = new Stack<>(); + s.pop(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/ArrayListRefinements.java new file mode 100644 index 000000000..0431592f3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/ArrayListRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.state_hints_same_simple_name_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"empty", "nonEmpty"}) +@ExternalRefinementsFor("java.util.ArrayList") +public interface ArrayListRefinements { + @StateRefinement(to = "empty(this)") + void ArrayList(); + + @StateRefinement(to = "nonEmpty(this)") + boolean add(E e); + + @StateRefinement(from = "nonEmpty(this)") + E remove(int index); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Collection.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Collection.java new file mode 100644 index 000000000..01d4ac521 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Collection.java @@ -0,0 +1,14 @@ +package testSuite.classes.state_hints_same_simple_name_error; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// shares its simple name with java.util.Collection, a supertype of ArrayList, but its states are not ArrayList's +@StateSet({"fresh", "used"}) +public class Collection { + @StateRefinement(to = "fresh(this)") + public Collection() {} + + @StateRefinement(from = "fresh(this)", to = "used(this)") + public void use() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Use.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Use.java new file mode 100644 index 000000000..01424d36e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Use.java @@ -0,0 +1,10 @@ +package testSuite.classes.state_hints_same_simple_name_error; + +import java.util.ArrayList; + +public class Use { + static void removeFromEmpty() { + ArrayList l = new ArrayList<>(); + l.remove(0); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index f173b3837..fccb2e6ec 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -170,7 +170,8 @@ private List allowedCalls(Set current) { private Optional newObjects(RefinedFunction call) { if (receiver.equals(Keys.THIS)) return Optional.empty(); - List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); + List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor) + .distinct().toList(); return constructors.isEmpty() ? Optional.empty() : Optional.of(String.join(" or ", constructors)); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 07d5f54c2..06d7358f4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -26,6 +26,7 @@ import spoon.reflect.declaration.CtModifiable; import spoon.reflect.declaration.CtType; import spoon.reflect.reference.CtExecutableReference; +import spoon.reflect.reference.CtTypeParameterReference; import spoon.reflect.reference.CtTypeReference; /** @@ -94,12 +95,14 @@ public static List ghostStatesOf(TypeChecker tc, String className) { private static List ghostStatesOf(Context context, CtTypeReference type, List> supertypes) { - // a state set can be registered more than once, so states are told apart by name + // a state set can be registered more than once, so states are told apart by name, and states are kept by + // simple class name, so those of another class with the same simple name are left out Map ghostStates = new LinkedHashMap<>(); for (CtTypeReference t : Stream.concat(Stream.of(type), supertypes.stream()).toList()) { List declared = context.getGhostState(Utils.getSimpleName(t.getQualifiedName())); if (declared != null) - declared.forEach(g -> ghostStates.putIfAbsent(g.getQualifiedName(), g)); + declared.stream().filter(g -> t.getQualifiedName().equals(g.getPrefix())) + .forEach(g -> ghostStates.putIfAbsent(g.getQualifiedName(), g)); } return List.copyOf(ghostStates.values()); } @@ -204,12 +207,16 @@ private StateMachine build(CtTypeReference type, List> sup created.ifPresent(s -> constructors.put(function, s)); continue; } + if (className.equals(function.getTargetClass()) && !appliesToOwnType(function, type, supertypes)) { + complete = false; + continue; + } if (!className.equals(function.getTargetClass())) { if (constructor || !inherited.contains(function.getTargetClass())) continue; if (overridden(function, className)) continue; // the class's own refinement for it is the one in the machine - if (!inheritedFrom(function, type, supertypes)) { + if (!resolvesTo(function, type, supertypes)) { complete = false; continue; } @@ -233,6 +240,19 @@ private boolean subclassChangesState(String className, CtTypeReference type, .map(c -> tc.getFactory().Type().createReference(c)).anyMatch(other -> other.isSubtypeOf(type)); } + /** + * Whether the verifier checks a call to {@code method}, specified for {@code type}, on an object of that type. It + * looks the refinement up by the receiver's type, which needs the parameter types to match those of the method it + * resolves to, and otherwise by the type that declares that method. A parameter whose type is a type variable may + * not match, so then {@code type} must declare the method. + */ + private boolean appliesToOwnType(RefinedFunction method, CtTypeReference type, + List> supertypes) { + boolean concreteParameters = method.getArguments().stream() + .noneMatch(a -> a.getType() instanceof CtTypeParameterReference); + return concreteParameters || resolvesTo(method, type, supertypes); + } + /** Whether {@code className} has its own refinement for {@code method}, with the same parameter types */ private boolean overridden(RefinedFunction method, String className) { String name = Utils.getSimpleName(method.getName()); @@ -246,13 +266,11 @@ private static List parameterTypes(RefinedFunction function) { } /** - * Whether the verifier checks a call to {@code method}, specified for a supertype, on an object of {@code type} - * that has no refinement of its own for it. Like the verifier, it uses the refinement for the nearest type that - * declares the method. Methods are matched by name and number of parameters, so an overload can hide an inherited - * method, which only leaves the machine incomplete. + * Whether the nearest type in the hierarchy of {@code type} that declares {@code method} is the one it is specified + * for, which is where the verifier looks up the refinement of a call. Methods are matched by name and number of + * parameters, so an overload can hide an inherited method, which only leaves the machine incomplete. */ - private boolean inheritedFrom(RefinedFunction method, CtTypeReference type, - List> supertypes) { + private boolean resolvesTo(RefinedFunction method, CtTypeReference type, List> supertypes) { String name = Utils.getSimpleName(method.getName()); int arity = method.getArguments().size(); for (CtTypeReference t : Stream.concat(Stream.of(type), supertypes.stream()).toList()) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index d986ffbb6..35a24d39e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -99,6 +99,18 @@ void stateSetAndMethodsFromTheReceiversSuperclassSpec() { new Hint(Kind.AVAILABLE_CALLS, "In state displayable, host can call: dispose(), pack()")); } + @Test + void ownGenericRefinementOfAnInheritedMethodIsNotSuggested() { + assertHints("classes/state_hints_generic_inherited_method_error"); + } + + @Test + void statesOfAnotherClassWithTheSimpleNameOfASupertypeAreLeftOut() { + assertHints("classes/state_hints_same_simple_name_error", + new Hint(Kind.CALL_SEQUENCE, "Call l.add(E) before this call to move l from empty to nonEmpty"), + new Hint(Kind.AVAILABLE_CALLS, "In state empty, l can call: add(E)")); + } + @Test void stateDependingOnThePathAsksForTheSameStateOnEveryPath() { assertHints("ErrorStateHintPathDependent.java", new Hint(Kind.PATH_DEPENDENT_STATE, From 7537f6201e2117fc66e8d85201ad5f0c20c4ace6 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 20:19:25 +0000 Subject: [PATCH 3/7] Format the files merged with main Co-Authored-By: Claude Opus 5.5 --- .../java/liquidjava/diagnostics/hints/StateHints.java | 4 ++-- .../object_checkers/AuxStateHandler.java | 9 ++++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index fccb2e6ec..899f0d138 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -170,8 +170,8 @@ private List allowedCalls(Set current) { private Optional newObjects(RefinedFunction call) { if (receiver.equals(Keys.THIS)) return Optional.empty(); - List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor) - .distinct().toList(); + List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).distinct() + .toList(); return constructors.isEmpty() ? Optional.empty() : Optional.of(String.join(" or ", constructors)); } 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 16872d873..d2983fca6 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 @@ -797,9 +797,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc Predicate expected = expectedStatesDisjunction; boolean checked = deciding.isEmpty() && states .map(r -> checkedElsewhere(tc, r, prevState, expected, instanceName, invocation)).orElse(false); - ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE - : states.flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, checked, - StateMachineBuilder.ghostStatesOf(tc, r.className()))).orElse(null); + ErrorCategory category = deciding + .isPresent() + ? ErrorCategory.ARGUMENT_PICKS_THE_STATE : states + .flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, + checked, StateMachineBuilder.ghostStatesOf(tc, r.className()))) + .orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() : states.map(r -> stateHints(r, function, category, checked, invocation)).orElse(List.of()); From 86e7ded64f3e5cb58e7793898443fae57becd356 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 20:19:25 +0000 Subject: [PATCH 4/7] Leave out inherited methods the receiver cannot call A private method is not inherited, nor is a package-private one by a class in another package, so suggesting it gives a call that does not compile. Such methods leave the machine incomplete instead. Co-Authored-By: Claude Opus 5.5 --- .../Hatch.java | 28 +++++++++++++++++++ .../OtherPackageHatch.java | 11 ++++++++ .../state_machine/StateMachineBuilder.java | 23 ++++++++++++++- .../liquidjava/api/tests/TestStateHints.java | 11 ++++++++ 4 files changed, 72 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java new file mode 100644 index 000000000..f39ebec91 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java @@ -0,0 +1,28 @@ +package testSuite.classes.state_hints_inaccessible_inherited_error; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"closed", "open"}) +public class Hatch { + + @StateRefinement(to = "closed(this)") + public Hatch() {} + + @StateRefinement(from = "closed(this)", to = "open(this)") + private void open() {} + + @StateRefinement(from = "closed(this)", to = "open(this)") + void openInPackage() {} + + @StateRefinement(from = "open(this)") + public void use() {} +} + +class SamePackageHatch extends Hatch { + + static void useClosed() { + SamePackageHatch hatch = new SamePackageHatch(); + hatch.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java new file mode 100644 index 000000000..cb4d62042 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java @@ -0,0 +1,11 @@ +package testSuite.classes.state_hints_inaccessible_inherited_error.elsewhere; + +import testSuite.classes.state_hints_inaccessible_inherited_error.Hatch; + +public class OtherPackageHatch extends Hatch { + + static void useClosed() { + OtherPackageHatch hatch = new OtherPackageHatch(); + hatch.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 06d7358f4..0168054f9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -7,6 +7,7 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; @@ -216,7 +217,7 @@ private StateMachine build(CtTypeReference type, List> sup continue; if (overridden(function, className)) continue; // the class's own refinement for it is the one in the machine - if (!resolvesTo(function, type, supertypes)) { + if (!resolvesTo(function, type, supertypes) || !inheritedBy(function, type)) { complete = false; continue; } @@ -285,6 +286,26 @@ private boolean resolvesTo(RefinedFunction method, CtTypeReference type, List return false; } + /** + * Whether objects of {@code type} inherit {@code method}, so it can be called on them: a private method is not + * inherited, nor is a package-private one by a class in another package. Methods are matched by name and number of + * parameters, so an inaccessible overload also leaves the method out, which only leaves the machine incomplete. + */ + private boolean inheritedBy(RefinedFunction method, CtTypeReference type) { + CtType declaring = tc.getFactory().Type().createReference(method.getTargetClass()).getTypeDeclaration(); + CtType declaration = type.getTypeDeclaration(); + if (declaring == null || declaration == null) + return false; // cannot tell whether it is inherited + if (declaring.isInterface()) + return true; + String name = Utils.getSimpleName(method.getName()); + int arity = method.getArguments().size(); + boolean samePackage = Objects.equals(declaring.getPackage(), declaration.getPackage()); + return declaring.getMethods().stream() + .filter(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity) + .noneMatch(m -> m.isPrivate() || (!samePackage && !m.isPublic() && !m.isProtected())); + } + private static boolean abstractType(CtTypeReference type) { CtType declaration = type.getTypeDeclaration(); return declaration == null || declaration.isInterface() || declaration.isAbstract(); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 35a24d39e..99cf7dcba 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -212,6 +212,17 @@ void onlyConstructorsThatCanBeCalledAreSuggested() { new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); } + @Test + void inheritedMethodsTheReceiverCannotCallAreNotSuggested() { + List errors = errors("classes/state_hints_inaccessible_inherited_error", 2); + assertHints(errors.get(0), + new Hint(Kind.CALL_SEQUENCE, + "Call hatch.openInPackage() before this call to move hatch from closed to open"), + new Hint(Kind.AVAILABLE_CALLS, + "In state closed, hatch can call: openInPackage() (and possibly others)")); + assertHints(errors.get(1)); + } + @Test void argumentThatDecidedTheStateIsShownWithAValueThatWouldWork() { assertHints("ErrorArgumentPicksTheState.java", new Hint(Kind.DECIDING_ARGUMENT, From 2f97168f83f44ab5d4574ce20595e2a39bc5afa4 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 20:39:12 +0000 Subject: [PATCH 5/7] Suggest only public inherited methods The machine is shared by every caller, so a protected or package-private method is left out as well: some callers cannot call it. Co-Authored-By: Claude Opus 5.5 --- .../Hatch.java | 7 +++++++ .../OtherPackageHatch.java | 11 ----------- .../state_machine/StateMachineBuilder.java | 19 ++++++++----------- .../liquidjava/api/tests/TestStateHints.java | 10 ++++------ 4 files changed, 19 insertions(+), 28 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java index f39ebec91..26dd28984 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java @@ -15,10 +15,17 @@ private void open() {} @StateRefinement(from = "closed(this)", to = "open(this)") void openInPackage() {} + @StateRefinement(from = "closed(this)", to = "open(this)") + protected void openInSubclass() {} + + @StateRefinement(from = "closed(this)", to = "open(this)") + public void openPublicly() {} + @StateRefinement(from = "open(this)") public void use() {} } +// only openPublicly() can be called on a subclass by every caller class SamePackageHatch extends Hatch { static void useClosed() { diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java deleted file mode 100644 index cb4d62042..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/OtherPackageHatch.java +++ /dev/null @@ -1,11 +0,0 @@ -package testSuite.classes.state_hints_inaccessible_inherited_error.elsewhere; - -import testSuite.classes.state_hints_inaccessible_inherited_error.Hatch; - -public class OtherPackageHatch extends Hatch { - - static void useClosed() { - OtherPackageHatch hatch = new OtherPackageHatch(); - hatch.use(); // Expect: State Refinement Error - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 0168054f9..b149819a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -7,7 +7,6 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; -import java.util.Objects; import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; @@ -217,7 +216,7 @@ private StateMachine build(CtTypeReference type, List> sup continue; if (overridden(function, className)) continue; // the class's own refinement for it is the one in the machine - if (!resolvesTo(function, type, supertypes) || !inheritedBy(function, type)) { + if (!resolvesTo(function, type, supertypes) || !publiclyInherited(function)) { complete = false; continue; } @@ -287,23 +286,21 @@ private boolean resolvesTo(RefinedFunction method, CtTypeReference type, List } /** - * Whether objects of {@code type} inherit {@code method}, so it can be called on them: a private method is not - * inherited, nor is a package-private one by a class in another package. Methods are matched by name and number of - * parameters, so an inaccessible overload also leaves the method out, which only leaves the machine incomplete. + * Whether any caller can call {@code method} on an object of a subtype of the type it is specified for. The machine + * is shared by every caller, so a method that only some callers can reach (private, package-private or protected) + * is left out, which only leaves the machine incomplete. Methods are matched by name and number of parameters. */ - private boolean inheritedBy(RefinedFunction method, CtTypeReference type) { + private boolean publiclyInherited(RefinedFunction method) { CtType declaring = tc.getFactory().Type().createReference(method.getTargetClass()).getTypeDeclaration(); - CtType declaration = type.getTypeDeclaration(); - if (declaring == null || declaration == null) - return false; // cannot tell whether it is inherited + if (declaring == null) + return false; // cannot tell whether it is public if (declaring.isInterface()) return true; String name = Utils.getSimpleName(method.getName()); int arity = method.getArguments().size(); - boolean samePackage = Objects.equals(declaring.getPackage(), declaration.getPackage()); return declaring.getMethods().stream() .filter(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity) - .noneMatch(m -> m.isPrivate() || (!samePackage && !m.isPublic() && !m.isProtected())); + .allMatch(CtModifiable::isPublic); } private static boolean abstractType(CtTypeReference type) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 99cf7dcba..e3e59ce38 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -213,14 +213,12 @@ void onlyConstructorsThatCanBeCalledAreSuggested() { } @Test - void inheritedMethodsTheReceiverCannotCallAreNotSuggested() { - List errors = errors("classes/state_hints_inaccessible_inherited_error", 2); - assertHints(errors.get(0), + void onlyPublicInheritedMethodsAreSuggested() { + assertHints("classes/state_hints_inaccessible_inherited_error", new Hint(Kind.CALL_SEQUENCE, - "Call hatch.openInPackage() before this call to move hatch from closed to open"), + "Call hatch.openPublicly() before this call to move hatch from closed to open"), new Hint(Kind.AVAILABLE_CALLS, - "In state closed, hatch can call: openInPackage() (and possibly others)")); - assertHints(errors.get(1)); + "In state closed, hatch can call: openPublicly() (and possibly others)")); } @Test From 343c7f6c50106a4ae042afd29a1d6d942c4a9fb3 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 20:57:15 +0000 Subject: [PATCH 6/7] Keep private interface methods out of inherited suggestions Co-Authored-By: Claude Opus 5.5 --- .../Door.java | 29 +++++++++++++++++++ .../state_machine/StateMachineBuilder.java | 5 ++-- .../liquidjava/api/tests/TestStateHints.java | 16 +++++++--- 3 files changed, 43 insertions(+), 7 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Door.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Door.java b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Door.java new file mode 100644 index 000000000..d062f4fc3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Door.java @@ -0,0 +1,29 @@ +package testSuite.classes.state_hints_inaccessible_inherited_error; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"shut", "ajar"}) +public interface Door { + + @StateRefinement(from = "shut(this)", to = "ajar(this)") + private void pry() {} + + @StateRefinement(from = "shut(this)", to = "ajar(this)") + default void push() {} + + @StateRefinement(from = "ajar(this)") + default void walkThrough() {} +} + +// only push() can be called on an implementing class: pry() is private +class FrontDoor implements Door { + + @StateRefinement(to = "shut(this)") + FrontDoor() {} + + static void walkThroughShut() { + FrontDoor door = new FrontDoor(); + door.walkThrough(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index b149819a7..c4d3bebdc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -294,13 +294,12 @@ private boolean publiclyInherited(RefinedFunction method) { CtType declaring = tc.getFactory().Type().createReference(method.getTargetClass()).getTypeDeclaration(); if (declaring == null) return false; // cannot tell whether it is public - if (declaring.isInterface()) - return true; String name = Utils.getSimpleName(method.getName()); int arity = method.getArguments().size(); + // interface methods are public unless declared private return declaring.getMethods().stream() .filter(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity) - .allMatch(CtModifiable::isPublic); + .allMatch(m -> declaring.isInterface() ? !m.isPrivate() : m.isPublic()); } private static boolean abstractType(CtTypeReference type) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index e3e59ce38..47eede868 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -4,6 +4,8 @@ import java.util.List; import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; import org.junit.jupiter.api.Test; @@ -214,11 +216,17 @@ void onlyConstructorsThatCanBeCalledAreSuggested() { @Test void onlyPublicInheritedMethodsAreSuggested() { - assertHints("classes/state_hints_inaccessible_inherited_error", - new Hint(Kind.CALL_SEQUENCE, + List errors = errors("classes/state_hints_inaccessible_inherited_error", 2); + // the files are verified in no fixed order + assertEquals(Set.of( + List.of(new Hint(Kind.CALL_SEQUENCE, "Call hatch.openPublicly() before this call to move hatch from closed to open"), - new Hint(Kind.AVAILABLE_CALLS, - "In state closed, hatch can call: openPublicly() (and possibly others)")); + new Hint(Kind.AVAILABLE_CALLS, + "In state closed, hatch can call: openPublicly() (and possibly others)")), + List.of(new Hint(Kind.CALL_SEQUENCE, + "Call door.push() before this call to move door from shut to ajar"), + new Hint(Kind.AVAILABLE_CALLS, "In state shut, door can call: push() (and possibly others)"))), + errors.stream().map(StateRefinementError::getHints).collect(Collectors.toSet())); } @Test From 20e7a45d2e2a5e9bb6820fcddae4be2cbf8e6580 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 21:22:44 +0000 Subject: [PATCH 7/7] Compute the receiver's ghost states once and share the method lookup by name and arity Co-Authored-By: Claude Opus 5.5 --- .../object_checkers/AuxStateHandler.java | 22 +++++----- .../state_machine/StateMachineBuilder.java | 42 +++++++++---------- 2 files changed, 31 insertions(+), 33 deletions(-) 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 d2983fca6..978e005af 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 @@ -797,12 +797,9 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc Predicate expected = expectedStatesDisjunction; boolean checked = deciding.isEmpty() && states .map(r -> checkedElsewhere(tc, r, prevState, expected, instanceName, invocation)).orElse(false); - ErrorCategory category = deciding - .isPresent() - ? ErrorCategory.ARGUMENT_PICKS_THE_STATE : states - .flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, - checked, StateMachineBuilder.ghostStatesOf(tc, r.className()))) - .orElse(null); + ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE : states.flatMap( + r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, checked, r.ghostStates())) + .orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() : states.map(r -> stateHints(r, function, category, checked, invocation)).orElse(List.of()); @@ -814,8 +811,11 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc } } - /** The state machine of the receiver's class and the states the receiver can be in before a call */ - private record ReceiverStates(String className, StateMachine machine, Set current) { + /** + * The state machine of the receiver's class, the states the receiver can be in before a call, and the ghost states + * of the class and its supertypes + */ + private record ReceiverStates(StateMachine machine, Set current, List ghostStates) { } /** @@ -831,7 +831,8 @@ private static Optional receiverStates(TypeChecker tc, RefinedFu return Optional.empty(); Set current = new StateSolver(tc, invocation.getPosition()).possibleStates(machine.get().states(), state, receiver.getName()); - return Optional.of(new ReceiverStates(className, machine.get(), current)); + List ghostStates = StateMachineBuilder.ghostStatesOf(tc, className); + return Optional.of(new ReceiverStates(machine.get(), current, ghostStates)); } catch (RuntimeException e) { // a failure to analyse the states must not replace the error being reported DebugLog.warn("Could not compute the receiver's states: " + e.getMessage()); @@ -844,8 +845,7 @@ private static boolean checkedElsewhere(TypeChecker tc, ReceiverStates states, P String instanceName, CtElement invocation) { try { return StateErrorCategories.checkedElsewhere(states.machine(), states.current(), found, - () -> tc.shownFound(found, expected), instanceName, - StateMachineBuilder.ghostStatesOf(tc, states.className()), + () -> tc.shownFound(found, expected), instanceName, states.ghostStates(), new StateSolver(tc, invocation.getPosition())); } catch (RuntimeException e) { DebugLog.warn("Could not tell whether the receiver's state was checked: " + e.getMessage()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index c4d3bebdc..9a83e0b30 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -23,6 +23,7 @@ import liquidjava.utils.constants.Keys; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtModifiable; import spoon.reflect.declaration.CtType; import spoon.reflect.reference.CtExecutableReference; @@ -200,27 +201,24 @@ private StateMachine build(CtTypeReference type, List> sup if (!function.hasStateChange()) continue; boolean constructor = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName()); - if (className.equals(function.getTargetClass()) && constructor) { + boolean own = className.equals(function.getTargetClass()); + if (own && constructor) { if (abstractType(type) || privateConstructor(function, type)) continue; // cannot be suggested as a new object Optional> created = createdStates(function); created.ifPresent(s -> constructors.put(function, s)); continue; } - if (className.equals(function.getTargetClass()) && !appliesToOwnType(function, type, supertypes)) { + if (!own && (constructor || !inherited.contains(function.getTargetClass()))) + continue; + if (!own && overridden(function, className)) + continue; // the class's own refinement for it is the one in the machine + boolean applies = own ? appliesToOwnType(function, type, supertypes) + : resolvesTo(function, type, supertypes) && publiclyInherited(function); + if (!applies) { complete = false; continue; } - if (!className.equals(function.getTargetClass())) { - if (constructor || !inherited.contains(function.getTargetClass())) - continue; - if (overridden(function, className)) - continue; // the class's own refinement for it is the one in the machine - if (!resolvesTo(function, type, supertypes) || !publiclyInherited(function)) { - complete = false; - continue; - } - } Optional> calls = transitionsOf(function); if (calls.isPresent()) { methods.add(function); @@ -271,15 +269,11 @@ private static List parameterTypes(RefinedFunction function) { * parameters, so an overload can hide an inherited method, which only leaves the machine incomplete. */ private boolean resolvesTo(RefinedFunction method, CtTypeReference type, List> supertypes) { - String name = Utils.getSimpleName(method.getName()); - int arity = method.getArguments().size(); for (CtTypeReference t : Stream.concat(Stream.of(type), supertypes.stream()).toList()) { CtType declaration = t.getTypeDeclaration(); if (declaration == null) return false; // cannot tell which type declares it - boolean declares = declaration.getMethods().stream() - .anyMatch(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity); - if (declares) + if (declarationsOf(method, declaration).findAny().isPresent()) return t.getQualifiedName().equals(method.getTargetClass()); } return false; @@ -288,18 +282,22 @@ private boolean resolvesTo(RefinedFunction method, CtTypeReference type, List /** * Whether any caller can call {@code method} on an object of a subtype of the type it is specified for. The machine * is shared by every caller, so a method that only some callers can reach (private, package-private or protected) - * is left out, which only leaves the machine incomplete. Methods are matched by name and number of parameters. + * is left out, which only leaves the machine incomplete. */ private boolean publiclyInherited(RefinedFunction method) { CtType declaring = tc.getFactory().Type().createReference(method.getTargetClass()).getTypeDeclaration(); if (declaring == null) return false; // cannot tell whether it is public + // interface methods are public unless declared private + return declarationsOf(method, declaring).allMatch(m -> declaring.isInterface() ? !m.isPrivate() : m.isPublic()); + } + + /** The methods of {@code type} that {@code method} may refer to: those with its name and number of parameters */ + private static Stream> declarationsOf(RefinedFunction method, CtType type) { String name = Utils.getSimpleName(method.getName()); int arity = method.getArguments().size(); - // interface methods are public unless declared private - return declaring.getMethods().stream() - .filter(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity) - .allMatch(m -> declaring.isInterface() ? !m.isPrivate() : m.isPublic()); + return type.getMethods().stream() + .filter(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity); } private static boolean abstractType(CtTypeReference type) {