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 00000000..08ef9899 --- /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 00000000..f363db9e --- /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 b8fa2cde..7024cd76 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_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 00000000..d402fccd --- /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 00000000..b938bf71 --- /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_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 00000000..46ad6765 --- /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 00000000..72254f4b --- /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_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 00000000..d062f4fc --- /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-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 00000000..26dd2898 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java @@ -0,0 +1,35 @@ +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 = "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() { + SamePackageHatch hatch = new SamePackageHatch(); + hatch.use(); // Expect: State Refinement Error + } +} 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 00000000..7e159f2e --- /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 00000000..183cd55a --- /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_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 00000000..0431592f --- /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 00000000..01d4ac52 --- /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 00000000..01424d36 --- /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-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 00000000..e7179005 --- /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 00000000..782afea8 --- /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/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index f173b383..899f0d13 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/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 2b391cef..f974424f 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 6d17712b..978e005a 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,13 +793,12 @@ 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); + .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, ghostStates)) + 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() @@ -812,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(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) { } /** @@ -821,14 +823,16 @@ 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()); + 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()); @@ -838,10 +842,10 @@ 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, states.ghostStates(), new StateSolver(tc, invocation.getPosition())); } catch (RuntimeException e) { DebugLog.warn("Could not tell whether the receiver's state was checked: " + e.getMessage()); @@ -849,6 +853,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 05314849..9a83e0b3 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; @@ -21,17 +23,19 @@ 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; +import spoon.reflect.reference.CtTypeParameterReference; 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 +72,80 @@ 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, 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.stream().filter(g -> t.getQualifiedName().equals(g.getPrefix())) + .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 +155,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 +190,35 @@ 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()); + 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 (!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; + } Optional> calls = transitionsOf(function); if (calls.isPresent()) { methods.add(function); @@ -151,12 +230,74 @@ 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 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()); + 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 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 resolvesTo(RefinedFunction method, CtTypeReference type, List> supertypes) { + 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 + if (declarationsOf(method, declaration).findAny().isPresent()) + return t.getQualifiedName().equals(method.getTargetClass()); + } + return false; + } + + /** + * 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. + */ + 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(); + return type.getMethods().stream() + .filter(m -> m.getSimpleName().equals(name) && m.getParameters().size() == arity); } private static boolean abstractType(CtTypeReference type) { @@ -176,7 +317,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 ce9eded2..47eede86 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; @@ -60,6 +62,57 @@ 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 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, @@ -161,6 +214,21 @@ void onlyConstructorsThatCanBeCalledAreSuggested() { new Hint(Kind.NEEDED_STATE, "The state of value is unknown here, and this call needs it to be ready")); } + @Test + void onlyPublicInheritedMethodsAreSuggested() { + 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)")), + 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 void argumentThatDecidedTheStateIsShownWithAValueThatWouldWork() { assertHints("ErrorArgumentPicksTheState.java", new Hint(Kind.DECIDING_ARGUMENT,