From 6486cd985af4b7d6da4126f7cd140d900d37b700 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 20 Oct 2026 23:33:17 +0100 Subject: [PATCH] Add the failing call's context to StateMachineErrorContext StateMachineErrorContext now also carries the receiver of the failing call, the states accepted by the Expected condition, the Expected and Found conditions as readable text (receiver shown by its source name), and the single state Found establishes for the receiver, if any. The called method is resolved by checking which method, constructor or static factory declaration contains the verifier's declaration position (the position of the state refinement annotation value), instead of exact position equality, which never matched real verifier errors. Tests run the verifier on new fixtures, including the DefaultMutableTreeNode example, a multi-state precondition and a Found condition that does not establish a single state. Co-Authored-By: Claude Opus 5.5 --- .../fsm/StateMachineErrorContext.java | 17 +- .../liquidjava/fsm/StateMachineParser.java | 145 +++++++++++++++++- .../fsm/StateMachineParserTests.java | 144 ++++++++++++++++- src/test/resources/fsm/errors/door/Door.java | 24 +++ .../resources/fsm/errors/door/DoorClient.java | 21 +++ .../DefaultMutableTreeNodeRefinements.java | 26 ++++ .../fsm/errors/tree/TreeNodeClient.java | 14 ++ 7 files changed, 382 insertions(+), 9 deletions(-) create mode 100644 src/test/resources/fsm/errors/door/Door.java create mode 100644 src/test/resources/fsm/errors/door/DoorClient.java create mode 100644 src/test/resources/fsm/errors/tree/DefaultMutableTreeNodeRefinements.java create mode 100644 src/test/resources/fsm/errors/tree/TreeNodeClient.java 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 + } +}