diff --git a/src/main/java/liquidjava/fsm/StateMachineErrorContext.java b/src/main/java/liquidjava/fsm/StateMachineErrorContext.java index 357147b..97d4a6f 100644 --- a/src/main/java/liquidjava/fsm/StateMachineErrorContext.java +++ b/src/main/java/liquidjava/fsm/StateMachineErrorContext.java @@ -4,5 +4,20 @@ /** * Describes the verification error overlaid on a state machine diagram. + * @param calledMethod the method, constructor or static factory declared at the error's declaration position + * @param actualStates the states mentioned by the found condition for the receiver + * @param receiver the receiver of the failing call (e.g. root) + * @param expectedStates the states accepted by the expected condition, in state set order + * @param expectedCondition the expected condition as text + * @param foundCondition the found condition for the receiver as text + * @param definiteFoundState the single state the found condition establishes, or null if there is none */ -public record StateMachineErrorContext(String calledMethod, List actualStates) {} +public record StateMachineErrorContext( + String calledMethod, + List actualStates, + String receiver, + List expectedStates, + String expectedCondition, + String foundCondition, + String definiteFoundState +) {} diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java index 59f1ea5..f0a36ab 100644 --- a/src/main/java/liquidjava/fsm/StateMachineParser.java +++ b/src/main/java/liquidjava/fsm/StateMachineParser.java @@ -4,16 +4,20 @@ import java.nio.file.Paths; import java.util.ArrayList; import java.util.Collection; +import java.util.Comparator; import java.util.List; import liquidjava.rj_language.ast.*; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.processor.VCImplication; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; +import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.utils.Utils; import spoon.Launcher; import spoon.reflect.CtModel; import spoon.reflect.declaration.CtAnnotation; import spoon.reflect.declaration.CtClass; +import spoon.reflect.declaration.CtConstructor; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtMethod; @@ -79,14 +83,9 @@ private static StateMachine parse(String uri, SourcePosition declarationPosition if (transitions.isEmpty()) return null; // no transitions found - CtMethod calledMethod = declarationPosition == null ? null : ctType.getMethods().stream() - .filter(method -> method.getPosition().equals(declarationPosition)) - .findFirst() - .orElse(null); StateMachineErrorContext errorContext = declarationPosition == null && expectedState == null - && foundState == null ? null : new StateMachineErrorContext( - calledMethod == null ? null : calledMethod.getSimpleName(), - getActualStates(expectedState, foundState, states)); + && foundState == null ? null : getErrorContext(ctType, simpleClassName, states, + declarationPosition, expectedState, foundState); return new StateMachine(className, states, transitions, initialTransitions, errorContext); } catch (Exception e) { @@ -95,6 +94,49 @@ private static StateMachine parse(String uri, SourcePosition declarationPosition } } + private static StateMachineErrorContext getErrorContext(CtType ctType, String className, List states, + SourcePosition declarationPosition, Expression expectedState, VCImplication foundState) { + String receiver = getStateReceiver(expectedState, states); + String receiverName = receiver == null ? null : VariableFormatter.withoutInstance(receiver); + List foundPremises = getReceiverPremises(foundState, receiver); + return new StateMachineErrorContext( + getCalledMethod(ctType, className, declarationPosition), + getActualStates(expectedState, foundState, states), + receiverName, + getExpectedStates(expectedState, states, receiver), + expectedState == null ? null : formatCondition(expectedState, receiver, receiverName), + getFoundCondition(foundState, foundPremises, receiver, receiverName), + getDefiniteState(foundPremises, states, receiver)); + } + + /** + * Gets the name of the method, constructor or static factory whose declaration contains the given position + * The verifier reports the position of the state refinement annotation value, so the position is matched by range + * Constructors are named after the class + */ + private static String getCalledMethod(CtType ctType, String className, SourcePosition declarationPosition) { + if (declarationPosition == null || !declarationPosition.isValidPosition()) return null; + List> executables = new ArrayList<>(ctType.getMethods()); + if (ctType instanceof CtClass ctClass) { + executables.addAll(ctClass.getConstructors()); + } + return executables.stream() + .filter(executable -> contains(executable.getPosition(), declarationPosition)) + .min(Comparator.comparingInt(executable -> executable.getPosition().getSourceEnd() + - executable.getPosition().getSourceStart())) + .map(executable -> executable instanceof CtConstructor ? className : executable.getSimpleName()) + .orElse(null); + } + + private static boolean contains(SourcePosition outer, SourcePosition inner) { + return outer.isValidPosition() + && outer.getFile() != null && inner.getFile() != null + && outer.getFile().toPath().toAbsolutePath().normalize() + .equals(inner.getFile().toPath().toAbsolutePath().normalize()) + && outer.getSourceStart() <= inner.getSourceStart() + && inner.getSourceEnd() <= outer.getSourceEnd(); + } + private static List getActualStates(Expression expectedState, VCImplication foundState, List states) { String receiver = getStateReceiver(expectedState, states); @@ -109,6 +151,95 @@ private static List getActualStates(Expression expectedState, VCImplicat return states.stream().filter(foundStates::contains).toList(); } + /** + * Gets the states accepted by the expected condition for the receiver, in state set order + */ + private static List getExpectedStates(Expression expectedState, List states, String receiver) { + if (expectedState == null || receiver == null) return List.of(); + List expectedStates = getStateExpressions(expectedState, states, receiver); + return states.stream().filter(expectedStates::contains).toList(); + } + + /** + * Gets the found premises about the receiver: those bound to it and unbound ones that mention it + */ + private static List getReceiverPremises(VCImplication foundState, String receiver) { + List premises = new ArrayList<>(); + if (receiver == null) return premises; + for (VCImplication premise = foundState; premise != null; premise = premise.getNext()) { + if (premise.getRefinement() == null) continue; + Expression expr = premise.getRefinement().getExpression(); + boolean bound = premise.hasBinder() && receiver.equals(premise.getName()); + boolean mentioned = !premise.hasBinder() && premise.getRefinement().getVariableNames().contains(receiver); + if ((bound || mentioned) && !expr.isBooleanTrue()) { + premises.add(expr); + } + } + return premises; + } + + private static String getFoundCondition(VCImplication foundState, List foundPremises, + String receiver, String receiverName) { + if (foundState == null) return null; + if (receiver == null) return ExpressionFormatter.format(foundState.toPredicate().getExpression()); + return formatCondition(joinConjunction(foundPremises), receiver, receiverName); + } + + private static Expression joinConjunction(List exprs) { + Expression conjunction = null; + for (Expression expr : exprs) { + conjunction = conjunction == null ? expr : new BinaryExpression(conjunction, "&&", expr); + } + return conjunction == null ? new LiteralBoolean(true) : conjunction; + } + + /** + * Formats a condition for display, showing the receiver by its source name (e.g. root instead of root¹⁷) + */ + private static String formatCondition(Expression expr, String receiver, String receiverName) { + if (receiver != null && receiverName != null) { + expr = expr.substitute(new Var(receiver), new Var(receiverName)); + } + return ExpressionFormatter.format(expr); + } + + /** + * Gets the single state the found premises establish for the receiver, or null if there is none + * A state is established only when it is a top-level conjunct; any other conjunct about the receiver's + * states (disjunction, conditional, ...) makes the result null, except negations of other states. + * Negations alone never establish a state since the verifier does not bound the state set + */ + private static String getDefiniteState(List premises, List states, String receiver) { + if (receiver == null) return null; + List found = new ArrayList<>(); + List excluded = new ArrayList<>(); + for (Expression premise : premises) { + for (Expression conjunct : premise.getConjuncts()) { + String state = getReceiverState(conjunct, states, receiver); + String negated = conjunct instanceof UnaryExpression unary && unary.getOp().equals("!") + ? getReceiverState(unary.getExpression(), states, receiver) : null; + if (state != null) { + if (!found.contains(state)) found.add(state); + } else if (negated != null) { + excluded.add(negated); + } else if (mentionsReceiverState(conjunct, states, receiver)) { + return null; + } + } + } + if (found.size() != 1 || excluded.contains(found.get(0))) return null; + return found.get(0); + } + + private static String getReceiverState(Expression expr, List states, String receiver) { + return expr instanceof FunctionInvocation ? getStateName(expr, states, receiver) : null; + } + + private static boolean mentionsReceiverState(Expression expr, List states, String receiver) { + if (getReceiverState(expr, states, receiver) != null) return true; + return expr.getChildren().stream().anyMatch(child -> mentionsReceiverState(child, states, receiver)); + } + private static String getStateReceiver(Expression expr, List states) { if (expr == null) return null; if (expr instanceof FunctionInvocation invocation diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java index 00eb744..a249c82 100644 --- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java +++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java @@ -3,11 +3,24 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertNull; +import java.io.File; import java.nio.file.Path; import java.util.List; import org.junit.jupiter.api.Test; +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.StateRefinementError; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.parsing.RefinementsParser; +import spoon.Launcher; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtClass; +import spoon.reflect.declaration.CtType; +import spoon.reflect.reference.CtTypeReference; + import static org.junit.jupiter.api.Assertions.assertNotNull; public class StateMachineParserTests { @@ -32,7 +45,7 @@ public void testSimpleStateMachine() { @Test public void testStateMachineGroupsErrorContext() { StateMachineErrorContext errorContext = new StateMachineErrorContext( - "read", List.of("closed")); + "read", List.of("closed"), "file", List.of("open"), "open(file)", "closed(file)", "closed"); StateMachine sm = new StateMachine("Simple", List.of("open", "closed"), List.of(), List.of(), errorContext); assertEquals(errorContext, sm.errorContext()); @@ -267,6 +280,94 @@ public void testExternalFactoryWithoutConstructorHasNoDefaultInitialState() { sm.initialTransitions()); } + @Test + public void testErrorContextForRejectedCall() { + // root.getFirstChild() after add and removeAllChildren + StateRefinementError error = verifyStateError("errors/tree", "root"); + StateMachine sm = parseWithErrorContext(error); + assertNotNull(sm); + assertEquals(new StateMachineErrorContext("getFirstChild", List.of("childrenAllowed"), "root", + List.of("maybeHasChildren"), "maybeHasChildren(root)", "childrenAllowed(root)", "childrenAllowed"), + sm.errorContext()); + } + + @Test + public void testErrorContextForPreconditionWithMultipleStates() { + StateRefinementError error = verifyStateError("errors/door", "twice"); + assertEquals(new StateMachineErrorContext("lock", List.of("locked"), "twice", List.of("open", "closed"), + "open(twice) || closed(twice)", "locked(twice)", "locked"), + parseWithErrorContext(error).errorContext()); + } + + @Test + public void testErrorContextForNegatedPrecondition() { + StateRefinementError error = verifyStateError("errors/door", "pushed"); + assertEquals(new StateMachineErrorContext("push", List.of("locked"), "pushed", List.of("open", "closed"), + "!locked(pushed)", "locked(pushed)", "locked"), + parseWithErrorContext(error).errorContext()); + } + + @Test + public void testErrorContextWithoutDefiniteFoundState() { + // found flag ? open(unknown) : closed(unknown) does not establish one state + StateRefinementError error = verifyStateError("errors/door", "unknown"); + assertEquals(new StateMachineErrorContext("unlock", List.of("open", "closed"), "unknown", + List.of("locked"), "locked(unknown)", "flag ? open(unknown) : closed(unknown)", null), + parseWithErrorContext(error).errorContext()); + } + + @Test + public void testDefiniteFoundState() { + String doorUri = uri("errors/door/Door.java"); + assertEquals("open", definiteFoundState(doorUri, "open(d)")); + assertEquals("open", definiteFoundState(doorUri, "open(d) && !locked(d)")); + assertEquals("open", definiteFoundState(doorUri, "open(d) && open(e)")); + assertEquals("open", definiteFoundState(doorUri, "open(d) && (closed(e) || locked(e))")); + assertNull(definiteFoundState(doorUri, "open(d) || closed(d)")); + assertNull(definiteFoundState(doorUri, "flag ? open(d) : closed(d)")); + assertNull(definiteFoundState(doorUri, "!locked(d)")); + assertNull(definiteFoundState(doorUri, "!open(d) && !locked(d)")); + assertNull(definiteFoundState(doorUri, "!(open(d) || locked(d))")); + assertNull(definiteFoundState(doorUri, "open(d) && closed(d)")); + assertNull(definiteFoundState(doorUri, "open(d) && !open(d)")); + assertNull(definiteFoundState(doorUri, "open(d) && (open(d) || closed(d))")); + assertNull(definiteFoundState(doorUri, "open(e)")); + assertNull(definiteFoundState(doorUri, "true")); + } + + @Test + public void testFoundConditionIsRestrictedToReceiver() { + CtTypeReference doorType = new Launcher().getFactory().Type().createReference("fsm.errors.door.Door"); + VCImplication other = new VCImplication("#e_2", doorType, predicate("closed(#e_2)")); + VCImplication receiver = new VCImplication("#d_3", doorType, predicate("open(#d_3) && x > 0")); + other.setNext(receiver); + StateMachineErrorContext errorContext = StateMachineParser.parseWithErrorContext( + uri("errors/door/Door.java"), null, RefinementsParser.createAST("locked(#d_3)", ""), other) + .errorContext(); + assertEquals(new StateMachineErrorContext(null, List.of("open"), "d", List.of("locked"), "locked(d)", + "open(d) && x > 0", "open"), errorContext); + } + + @Test + public void testCalledConstructorAndStaticFactory() { + CtClass staticFactory = (CtClass) buildType("StaticFactory.java"); + assertEquals("StaticFactory", calledMethod("StaticFactory.java", + staticFactory.getConstructors().iterator().next().getPosition())); + assertEquals("of", calledMethod("StaticFactory.java", + staticFactory.getMethodsByName("of").get(0).getPosition())); + assertEquals("close", calledMethod("StaticFactory.java", + staticFactory.getMethodsByName("close").get(0).getPosition())); + + // interfaces declare constructors as methods named after the class + CtType refinements = buildType("errors/tree/DefaultMutableTreeNodeRefinements.java"); + assertEquals("DefaultMutableTreeNode", calledMethod("errors/tree/DefaultMutableTreeNodeRefinements.java", + refinements.getMethodsByName("DefaultMutableTreeNode").get(0).getPosition())); + + // positions outside the state machine's type resolve to no method + assertNull(calledMethod("errors/tree/DefaultMutableTreeNodeRefinements.java", + staticFactory.getMethodsByName("close").get(0).getPosition())); + } + private static void assertStateMachineEquals(StateMachine expected, StateMachine actual) { assertNotNull(actual, "State machine should not be null"); assertEquals(expected.className(), actual.className(), "Class names should match"); @@ -283,4 +384,45 @@ private static StateMachine stateMachine(String className, List states, String qualifiedName = className.contains(".") ? className : "fsm." + className; return new StateMachine(qualifiedName, states, transitions, initialTransitions, null); } + + private static StateRefinementError verifyStateError(String directory, String receiver) { + CommandLineLauncher.launch(BASE_PATH.resolve(directory).toAbsolutePath().toString()); + return Diagnostics.getInstance().getErrors().stream() + .filter(StateRefinementError.class::isInstance) + .map(StateRefinementError.class::cast) + .filter(error -> error.getFound().toString().contains("#" + receiver + "_")) + .findFirst() + .orElseThrow(() -> new AssertionError("No state refinement error found for " + receiver)); + } + + // same arguments as the vscode-liquidjava server + private static StateMachine parseWithErrorContext(StateRefinementError error) { + return StateMachineParser.parseWithErrorContext( + new File(error.getDeclarationPosition().getFile().getPath()).toURI().toString(), + error.getDeclarationPosition(), error.getExpected().getExpression(), error.getFound()); + } + + private static String definiteFoundState(String uri, String found) { + CtTypeReference doorType = new Launcher().getFactory().Type().createReference("fsm.errors.door.Door"); + VCImplication foundState = new VCImplication("d", doorType, predicate(found)); + return StateMachineParser.parseWithErrorContext(uri, null, RefinementsParser.createAST("locked(d)", ""), + foundState).errorContext().definiteFoundState(); + } + + private static Predicate predicate(String expr) { + return new Predicate(RefinementsParser.createAST(expr, "")); + } + + private static String calledMethod(String file, SourcePosition declarationPosition) { + return StateMachineParser.parseWithErrorContext(uri(file), declarationPosition, null, null) + .errorContext().calledMethod(); + } + + private static CtType buildType(String file) { + Launcher launcher = new Launcher(); + launcher.getEnvironment().setNoClasspath(true); + launcher.addInputResource(BASE_PATH.resolve(file).toAbsolutePath().toString()); + launcher.buildModel(); + return launcher.getModel().getAllTypes().iterator().next(); + } } diff --git a/src/test/resources/fsm/errors/door/Door.java b/src/test/resources/fsm/errors/door/Door.java new file mode 100644 index 0000000..80a8748 --- /dev/null +++ b/src/test/resources/fsm/errors/door/Door.java @@ -0,0 +1,24 @@ +package fsm.errors.door; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed", "locked"}) +public class Door { + + @StateRefinement(to="open(this)") + public Door() {} + + @StateRefinement(to="flag ? open(this) : closed(this)") + public Door(boolean flag) {} + + // accepts more than one state + @StateRefinement(from="open(this) || closed(this)", to="locked(this)") + public void lock() {} + + @StateRefinement(from="locked(this)", to="closed(this)") + public void unlock() {} + + @StateRefinement(from="!locked(this)", to="open(this)") + public void push() {} +} diff --git a/src/test/resources/fsm/errors/door/DoorClient.java b/src/test/resources/fsm/errors/door/DoorClient.java new file mode 100644 index 0000000..e9ea05e --- /dev/null +++ b/src/test/resources/fsm/errors/door/DoorClient.java @@ -0,0 +1,21 @@ +package fsm.errors.door; + +public class DoorClient { + + public static void lockTwice() { + Door twice = new Door(); + twice.lock(); + twice.lock(); // state error: found locked, expected open || closed + } + + public static void unlockUnknown(boolean flag) { + Door unknown = new Door(flag); + unknown.unlock(); // state error: found flag ? open : closed, expected locked + } + + public static void pushLocked() { + Door pushed = new Door(); + pushed.lock(); + pushed.push(); // state error: found locked, expected !locked + } +} diff --git a/src/test/resources/fsm/errors/tree/DefaultMutableTreeNodeRefinements.java b/src/test/resources/fsm/errors/tree/DefaultMutableTreeNodeRefinements.java new file mode 100644 index 0000000..0d87ebb --- /dev/null +++ b/src/test/resources/fsm/errors/tree/DefaultMutableTreeNodeRefinements.java @@ -0,0 +1,26 @@ +package fsm.errors.tree; + +import javax.swing.tree.MutableTreeNode; +import javax.swing.tree.TreeNode; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// example from vscode-liquidjava#117 +@ExternalRefinementsFor("javax.swing.tree.DefaultMutableTreeNode") +@StateSet({"childrenAllowed", "maybeHasChildren"}) +public interface DefaultMutableTreeNodeRefinements { + + @StateRefinement(to="childrenAllowed(this)") + void DefaultMutableTreeNode(Object value); + + @StateRefinement(from="childrenAllowed(this)", to="maybeHasChildren(this)") + void add(MutableTreeNode child); + + @StateRefinement(from="maybeHasChildren(this)", to="childrenAllowed(this)") + void removeAllChildren(); + + @StateRefinement(from="maybeHasChildren(this)") + TreeNode getFirstChild(); +} diff --git a/src/test/resources/fsm/errors/tree/TreeNodeClient.java b/src/test/resources/fsm/errors/tree/TreeNodeClient.java new file mode 100644 index 0000000..9351252 --- /dev/null +++ b/src/test/resources/fsm/errors/tree/TreeNodeClient.java @@ -0,0 +1,14 @@ +package fsm.errors.tree; + +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.TreeNode; + +public class TreeNodeClient { + + public static void main(String[] args) { + DefaultMutableTreeNode root = new DefaultMutableTreeNode("outline"); + root.add(new DefaultMutableTreeNode("section")); + root.removeAllChildren(); + TreeNode landing = root.getFirstChild(); // state error: found childrenAllowed, expected maybeHasChildren + } +}