diff --git a/README.md b/README.md index a2e0c83..3e97b2f 100644 --- a/README.md +++ b/README.md @@ -38,8 +38,16 @@ StateMachine stateMachine = StateMachineParser.parse(path.toUri().toString()); StateMachine named = StateMachineParser.parse(path.toUri().toString(), "example.File"); // one state machine per @StateSet, in declaration order List stateMachines = StateMachineParser.parseAll(path.toUri().toString()); +// with the state sets and methods java.awt.Frame inherits from the specs of its supertypes in these files +List inherited = StateMachineParser.parseAll(List.of(frameSpec, windowSpec), "java.awt.Frame"); ``` +A class inherits the state sets and methods of the specs of its supertypes in the parsed files, as in the verifier. +Its own state sets come first, then those of its supertypes, nearest first. A call uses the class's own refinement of a +method, otherwise that of the nearest type that declares the method, so an inherited refinement is left out when a +nearer spec refines the method, when a nearer type redeclares it, or when not every caller can call it. Constructors are +the class's own. + A class with several `@StateSet` annotations has one state machine per state set, since each changes independently. `stateSet` is the index of the state set, the same order the verifier uses in `StateErrorContext`. A state machine only has the transitions that mention its states. States of other state sets in a `from` are kept as diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index 1325903..06c333b 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -1,10 +1,18 @@ package liquidjava.fsm; import java.net.URI; +import java.net.URISyntaxException; +import java.nio.file.Files; +import java.nio.file.Path; import java.nio.file.Paths; +import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Collection; +import java.util.Deque; +import java.util.HashSet; import java.util.List; +import java.util.Set; +import java.util.stream.Stream; import liquidjava.rj_language.ast.*; import liquidjava.rj_language.parsing.RefinementsParser; @@ -16,6 +24,7 @@ import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtType; +import spoon.reflect.reference.CtTypeReference; public class StateMachineParser { @@ -63,22 +72,32 @@ public static List parseAll(String uri) { * @return the state machines of the state sets with transitions, in declaration order */ public static List parseAll(String uri, String className) { + return parseAll(List.of(uri), className); + } + + /** + * Parses the class or interface with the given name in the given uris, with the state sets and methods it inherits + * from the specs of its supertypes in them, and extracts one state machine per state set + * As in the verifier, the state sets of the class come first, then those of its supertypes, nearest first, and a + * call uses the class's own refinement of a method, otherwise that of the nearest type that declares the method + * @param uris the document URIs + * @param className the qualified class name, or the name given by ExternalRefinementsFor + * @return the state machines of the state sets with transitions, in declaration order + */ + public static List parseAll(List uris, String className) { try { - String filePath = Paths.get(new URI(uri)).toString(); - Launcher launcher = new Launcher(); - launcher.getEnvironment().setNoClasspath(true); - launcher.getEnvironment().setAutoImports(true); - launcher.addInputResource(filePath); - launcher.buildModel(); - CtModel model = launcher.getModel(); + CtModel model = buildModel(uris); // get class or interface CtType ctType = getType(model, className); if (ctType == null) return List.of(); // no class or interface found - // extract class name and state sets - List> stateSets = getStateSets(ctType); + // extract class name, state sets and methods, with those inherited from the specs of the supertypes + List> supertypes = getSupertypes(model, ctType); + List> specs = getSpecs(model, ctType, supertypes); + List> stateSets = specs.stream().flatMap(spec -> getStateSets(spec).stream()).toList(); + List> methods = getMethods(specs, supertypes); String qualifiedName = getClassName(ctType); List stateMachines = new ArrayList<>(); for (int i = 0; i < stateSets.size(); i++) { @@ -87,7 +106,7 @@ public static List parseAll(String uri, String className) { if (j != i) otherStates.addAll(stateSets.get(j)); } - StateMachine sm = parseStateSet(ctType, qualifiedName, i, stateSets.get(i), otherStates); + StateMachine sm = parseStateSet(ctType, methods, qualifiedName, i, stateSets.get(i), otherStates); if (sm != null) stateMachines.add(sm); } @@ -99,17 +118,32 @@ public static List parseAll(String uri, String className) { } } + // a file that no longer exists is skipped, so that it does not discard the specs in the others + private static CtModel buildModel(List uris) throws URISyntaxException { + Launcher launcher = new Launcher(); + launcher.getEnvironment().setNoClasspath(true); + launcher.getEnvironment().setAutoImports(true); + for (String uri : uris.stream().distinct().toList()) { + Path path = Paths.get(new URI(uri)); + if (Files.isRegularFile(path)) + launcher.addInputResource(path.toString()); + } + launcher.buildModel(); + return launcher.getModel(); + } + /** * Extracts the state machine of one state set * @param ctType the CtType (class or interface) + * @param methods the methods of the class, with those it inherits * @param qualifiedName the class name * @param stateSet the index of the state set * @param states the states of the state set * @param otherStates the states of the other state sets * @return StateMachine or null if the state set has no transitions */ - private static StateMachine parseStateSet(CtType ctType, String qualifiedName, int stateSet, - List states, List otherStates) { + private static StateMachine parseStateSet(CtType ctType, List> methods, String qualifiedName, + int stateSet, List states, List otherStates) { if (states.isEmpty()) return null; // no states found String simpleClassName = Utils.getSimpleName(qualifiedName); @@ -124,7 +158,7 @@ private static StateMachine parseStateSet(CtType ctType, String qualifiedName initialTransitions = new ArrayList<>(initialTransitions); initialTransitions.addAll(factoryTransitions); List entryTransitions = new ArrayList<>(); - List transitions = getTransitions(ctType, simpleClassName, states, otherStates, entryTransitions); + List transitions = getTransitions(methods, states, otherStates, entryTransitions); if (transitions.isEmpty() && entryTransitions.isEmpty()) return null; // no transitions found @@ -145,6 +179,164 @@ private static CtType getType(CtModel model, String className) { return null; } + /** + * Gets the supertypes of a class whose specs it may inherit, nearest first: its superclasses, then the interfaces + * they implement, as in the verifier + * @param model the CtModel + * @param ctType the CtType (class or interface) + * @return the supertypes, or none if the model has no other type with a spec + */ + private static List> getSupertypes(CtModel model, CtType ctType) { + if (model.getAllTypes().size() == 1) + return List.of(); + CtTypeReference type = getClassReference(ctType); + List> superclasses = new ArrayList<>(); + Deque> interfaces = new ArrayDeque<>(); + Set seen = new HashSet<>(Set.of(type.getQualifiedName())); + for (CtTypeReference t = type; t != null; t = getSuperclass(t)) { + if (t != type && seen.add(t.getQualifiedName())) + superclasses.add(t); + interfaces.addAll(getSuperInterfaces(t)); + } + List> supertypes = new ArrayList<>(superclasses); + while (!interfaces.isEmpty()) { + CtTypeReference t = interfaces.poll(); + if (seen.add(t.getQualifiedName())) { + supertypes.add(t); + interfaces.addAll(getSuperInterfaces(t)); + } + } + return supertypes; + } + + // a supertype that cannot be resolved (no source, not on the classpath) ends the walk on that branch + private static CtTypeReference getSuperclass(CtTypeReference type) { + try { + return type.getSuperclass(); + } catch (RuntimeException e) { + return null; + } + } + + private static Set> getSuperInterfaces(CtTypeReference type) { + try { + return type.getSuperInterfaces(); + } catch (RuntimeException e) { + return Set.of(); + } + } + + /** + * Gets the reference to the class a class or interface specifies + * @param ctType the CtType (class or interface) + * @return the reference to the class named by ExternalRefinementsFor, or to the class itself + */ + private static CtTypeReference getClassReference(CtType ctType) { + return ctType.getFactory().Type().createReference(getClassName(ctType)); + } + + /** + * Gets the specs of a class and of its supertypes in the model + * @param model the CtModel + * @param ctType the CtType (class or interface) of the class + * @param supertypes the supertypes of the class, nearest first + * @return the CtType of the class, followed by those of its supertypes that have one + */ + private static List> getSpecs(CtModel model, CtType ctType, List> supertypes) { + List> specs = new ArrayList<>(List.of(ctType)); + for (CtTypeReference supertype : supertypes) { + CtType spec = getType(model, supertype.getQualifiedName()); + if (spec != null) + specs.add(spec); + } + return specs; + } + + /** + * Gets the methods of a class and those it inherits from the specs of its supertypes, as the verifier applies them + * An inherited method is left out if a nearer spec refines it, if the nearest type that declares it is not the one + * it is specified for, or if not every caller can call it + * @param specs the CtType of the class, followed by those of its supertypes + * @param supertypes the supertypes of the class, nearest first + * @return the methods, without the constructors of interfaces + */ + private static List> getMethods(List> specs, List> supertypes) { + CtType ctType = specs.get(0); + List> hierarchy = new ArrayList<>(List.of(getClassReference(ctType))); + hierarchy.addAll(supertypes); + List> methods = new ArrayList<>(getDeclaredMethods(ctType)); + for (CtType spec : specs.subList(1, specs.size())) { + for (CtMethod method : getDeclaredMethods(spec)) { + if (!isRefinedIn(method, methods) && resolvesTo(method, spec, hierarchy) && isPublic(method, spec)) + methods.add(method); + } + } + return methods; + } + + /** + * Gets the methods of a class or interface, without the methods of interfaces that stand for constructors + * @param ctType the CtType (class or interface) + * @return the methods + */ + private static List> getDeclaredMethods(CtType ctType) { + String className = Utils.getSimpleName(getClassName(ctType)); + return ctType.getMethods().stream() + .filter(method -> !(ctType.isInterface() && method.getSimpleName().equals(className))).toList(); + } + + private static boolean isRefinedIn(CtMethod method, List> methods) { + return methods.stream().anyMatch(m -> m.getSimpleName().equals(method.getSimpleName()) + && getQualifiedParameterTypes(m).equals(getQualifiedParameterTypes(method))); + } + + private static List getQualifiedParameterTypes(CtMethod method) { + return method.getParameters().stream() + .map(parameter -> parameter.getType() == null ? "" : parameter.getType().getQualifiedName()).toList(); + } + + /** + * Checks whether the nearest type in the hierarchy that declares a method is the one a spec is for, which is where + * the verifier looks up the refinement of a call + * @param method the method of the spec + * @param spec the CtType (class or interface) of the spec + * @param hierarchy the class, followed by its supertypes, nearest first + * @return whether a call on the class uses the spec's refinement of the method + */ + private static boolean resolvesTo(CtMethod method, CtType spec, List> hierarchy) { + for (CtTypeReference type : hierarchy) { + CtType declaration = type.getTypeDeclaration(); + if (declaration == null) + return false; // cannot tell which type declares it + if (getDeclarations(method, declaration).findAny().isPresent()) + return type.getQualifiedName().equals(getClassName(spec)); + } + return false; + } + + /** + * Checks whether every caller can call a method on a subtype of the class a spec is for, since the diagram is + * shared by every caller + * @param method the method of the spec + * @param spec the CtType (class or interface) of the spec + * @return whether the method is public in the class + */ + private static boolean isPublic(CtMethod method, CtType spec) { + CtType declaring = getClassReference(spec).getTypeDeclaration(); + if (declaring == null) + return false; // cannot tell whether it is public + // interface methods are public unless declared private + return getDeclarations(method, declaring).allMatch(m -> declaring.isInterface() ? !m.isPrivate() : m.isPublic()); + } + + /** + * Gets the methods of a type that a method of a spec may refer to: those with its name and number of parameters + */ + private static Stream> getDeclarations(CtMethod method, CtType type) { + return type.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName()) + && m.getParameters().size() == method.getParameters().size()); + } + /** * Gets the qualified name from a class or interface * Uses name from ExternalRefinementsFor if present, otherwise uses class or interface name @@ -273,21 +465,17 @@ private static String getParameterTypes(CtExecutable element) { } /** - * Gets transitions from a class or interface - * @param ctType the CtType (class or interface) - * @param className the class name + * Gets transitions from the methods of a class or interface + * @param methods the methods, without the constructors of interfaces * @param states the list of states * @param otherStates the states of the other state sets * @param entryTransitions the list where the entry transitions are added * @return list of StateMachineTransition */ - private static List getTransitions(CtType ctType, String className, List states, + private static List getTransitions(List> methods, List states, List otherStates, List entryTransitions) { List transitions = new ArrayList<>(); - for (CtMethod method : ctType.getMethods()) { - // for interfaces we skip constructor methods (methods with same name as class) - if (ctType.isInterface() && method.getSimpleName().equals(className)) - continue; + for (CtMethod method : methods) { // the verifier uses the first StateRefinement whose from matches, so the states that an earlier from // always matches are not reached by the later ones List coveredStates = new ArrayList<>(); diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java index 2072f0a..3876961 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java @@ -342,6 +342,64 @@ public void testStateMachinePerStateSet() { assertEquals(List.of(), StateMachineParser.parseAll(uri("TwoStateClasses.java"), "fsm.Missing")); } + private static final StateMachine FRAME = new StateMachine("java.awt.Frame", 0, + List.of("displayable", "notDisplayable"), + List.of(new StateMachineTransition("notDisplayable", "notDisplayable", "setUndecorated"), + new StateMachineTransition("displayable", "notDisplayable", "dispose"), + new StateMachineTransition("notDisplayable", "notDisplayable", "dispose"), + new StateMachineTransition("displayable", "displayable", "pack"), + new StateMachineTransition("notDisplayable", "displayable", "pack")), + List.of(new StateMachineInitialTransition("notDisplayable"))); + + @Test + public void testStateSetAndMethodsInheritedFromTheSuperclassSpec() { + // addNotify is left out: Frame redeclares it, so a call on a Frame does not use the Window spec's refinement + List sms = StateMachineParser.parseAll(uri("InheritedStateSet.java"), "java.awt.Frame"); + assertEquals(1, sms.size()); + assertStateMachineEquals(FRAME, sms.get(0)); + assertTrue(StateMachineParser.parse(uri("InheritedStateSet.java"), "java.awt.Window").transitions().stream() + .anyMatch(transition -> transition.label().equals("addNotify"))); + } + + @Test + public void testSpecsInheritedFromOtherFiles() { + List sms = StateMachineParser.parseAll( + List.of(uri("inherited/FrameRefinements.java"), uri("inherited/WindowRefinements.java")), + "java.awt.Frame"); + assertEquals(1, sms.size()); + assertStateMachineEquals(FRAME, sms.get(0)); + assertEquals(List.of(), StateMachineParser.parseAll(uri("inherited/FrameRefinements.java"), "java.awt.Frame")); + } + + @Test + public void testMethodsInheritedFromASpecWithoutStateSet() { + StateMachine sm = StateMachineParser.parseAll(List.of(uri("inherited/JFrameRefinements.java"), + uri("inherited/FrameRefinements.java"), uri("inherited/WindowRefinements.java")), "javax.swing.JFrame") + .get(0); + assertEquals(List.of("setDefaultCloseOperation", "setUndecorated", "dispose", "pack"), + sm.transitions().stream().map(StateMachineTransition::label).distinct().toList()); + assertEquals(List.of(new StateMachineInitialTransition("notDisplayable", null, "new JFrame(String)")), + sm.initialTransitions()); + } + + @Test + public void testMissingFileDoesNotDiscardTheOthers() { + List sms = StateMachineParser.parseAll(List.of(uri("inherited/FrameRefinements.java"), + uri("inherited/WindowRefinements.java"), uri("inherited/Missing.java")), "java.awt.Frame"); + assertEquals(List.of(FRAME.transitions()), sms.stream().map(StateMachine::transitions).toList()); + } + + @Test + public void testOverriddenAndPackagePrivateInheritedMethods() { + // the child's next replaces its parent's, and inPackage cannot be called by every caller + StateMachine sm = StateMachineParser.parse(uri("InheritedOverride.java"), "fsm.InheritedOverrideChild"); + assertStateMachineEquals(stateMachine("InheritedOverrideChild", List.of("a", "b", "c"), + List.of(new StateMachineTransition("a", "c", "next"), + new StateMachineTransition("b", "a", "reset"), + new StateMachineTransition("c", "c", "useC")), + List.of(new StateMachineInitialTransition("a"))), sm); + } + @Test public void testVerifierStatesAreStatesOfTheDiagram() { for (String directory : List.of("errors/door", "errors/tree", "errors/udp", "errors/image")) { diff --git a/src/test/resources/fsm/InheritedOverride.java b/src/test/resources/fsm/InheritedOverride.java new file mode 100644 index 0000000..5822028 --- /dev/null +++ b/src/test/resources/fsm/InheritedOverride.java @@ -0,0 +1,31 @@ +package fsm; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"a", "b", "c"}) +public class InheritedOverride { + + @StateRefinement(from = "a(this)", to = "b(this)") + public void next() {} + + @StateRefinement(from = "c(this)") + public void useC() {} + + @StateRefinement(from = "a(this)", to = "c(this)") + void inPackage() {} +} + +// overrides next with a stronger transition and adds one to the states it inherits +class InheritedOverrideChild extends InheritedOverride { + + @StateRefinement(to = "a(this)") + public InheritedOverrideChild() {} + + @Override + @StateRefinement(from = "a(this)", to = "c(this)") + public void next() {} + + @StateRefinement(from = "b(this)", to = "a(this)") + public void reset() {} +} diff --git a/src/test/resources/fsm/InheritedStateSet.java b/src/test/resources/fsm/InheritedStateSet.java new file mode 100644 index 0000000..0977587 --- /dev/null +++ b/src/test/resources/fsm/InheritedStateSet.java @@ -0,0 +1,32 @@ +package fsm; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("java.awt.Window") +interface WindowRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Window(java.awt.Frame owner); + + @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(); +} + +// 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/src/test/resources/fsm/inherited/FrameRefinements.java b/src/test/resources/fsm/inherited/FrameRefinements.java new file mode 100644 index 0000000..63637bf --- /dev/null +++ b/src/test/resources/fsm/inherited/FrameRefinements.java @@ -0,0 +1,14 @@ +package fsm.inherited; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; + +// the state set is declared in the superclass's spec, in another file +@ExternalRefinementsFor("java.awt.Frame") +public interface FrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void Frame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/src/test/resources/fsm/inherited/JFrameRefinements.java b/src/test/resources/fsm/inherited/JFrameRefinements.java new file mode 100644 index 0000000..51f040c --- /dev/null +++ b/src/test/resources/fsm/inherited/JFrameRefinements.java @@ -0,0 +1,14 @@ +package fsm.inherited; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; + +// inherits the state set from Window's spec and setUndecorated from Frame's, which has no state set +@ExternalRefinementsFor("javax.swing.JFrame") +public interface JFrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void JFrame(String title); + + @StateRefinement(from = "notDisplayable(this)") + void setDefaultCloseOperation(int operation); +} diff --git a/src/test/resources/fsm/inherited/WindowRefinements.java b/src/test/resources/fsm/inherited/WindowRefinements.java new file mode 100644 index 0000000..2814511 --- /dev/null +++ b/src/test/resources/fsm/inherited/WindowRefinements.java @@ -0,0 +1,15 @@ +package fsm.inherited; + +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(); +}