From 26236834c6a34ba2e92759db08284250dc441d8b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:54:16 +0000 Subject: [PATCH 1/8] Call the note Origin and lead with where the value comes from "From" read like the from of @StateRefinement, which declared-here shows. The note is now "Origin: line L,

is a parameter of with no refinement", the shape every origin note takes. Co-Authored-By: Claude Opus 5.5 --- .../{FromNotes.java => OriginNotes.java} | 14 +++++++------- .../processor/refinement_checker/VCChecker.java | 2 +- .../{TestFromNotes.java => TestOriginNotes.java} | 6 +++--- 3 files changed, 11 insertions(+), 11 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/{FromNotes.java => OriginNotes.java} (89%) rename liquidjava-verifier/src/test/java/liquidjava/api/tests/{TestFromNotes.java => TestOriginNotes.java} (83%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/FromNotes.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java similarity index 89% rename from liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/FromNotes.java rename to liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java index f0a1aed2..863f09a5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/FromNotes.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java @@ -18,12 +18,12 @@ import liquidjava.utils.Utils; /** - * The notes of a refinement error that say where the values its expected refinement is about come from. Each is given - * only when it restates what the verifier used, and is left out otherwise + * The origin notes of a refinement error, which say where the values its expected refinement is about come from. Each + * is given only when it restates what the verifier used, and is left out otherwise */ -final class FromNotes { +final class OriginNotes { - private FromNotes() { + private OriginNotes() { } /** @@ -46,9 +46,9 @@ static List unrefinedParameters(RefinementError error, CtElement checked || !(context.getVariableByName(variable)instanceof Variable declared) || !declared.getMainRefinement().isBooleanTrue() || isRefined(parameter.get(), context)) return List.of(); - notes.add(String.format("From: %s is a parameter of %s (line %d) with no refinement", - error.getDisplayNames().get(variable), signature(method.get()), - parameter.get().getPosition().getLine())); + notes.add(String.format("Origin: line %d, %s is a parameter of %s with no refinement", + parameter.get().getPosition().getLine(), error.getDisplayNames().get(variable), + signature(method.get()))); } return notes; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 5562e1ac..d098937c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -90,7 +90,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl RefinementError error = new RefinementError(element.getPosition(), declarationPosition, expectedType, implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map, result.getCounterexample(), customMessage, context.getAliases()); - FromNotes.unrefinedParameters(error, element, context).forEach(error::addMessageNote); + OriginNotes.unrefinedParameters(error, element, context).forEach(error::addMessageNote); throw error; } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java similarity index 83% rename from liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java rename to liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index 48c55373..898e0a3c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -10,16 +10,16 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; -class TestFromNotes { +class TestOriginNotes { private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; @Test void unrefinedParameterIsNamedWithItsMethod() { LJError error = verify("ErrorUnknownArgument.java"); - assertEquals(List.of("From: amount is a parameter of use(int) (line 10) with no refinement"), + assertEquals(List.of("Origin: line 10, amount is a parameter of use(int) with no refinement"), error.getMessageNotes()); - assertTrue(error.toString().contains(error.getMessage() + "\n From: amount is a parameter")); + assertTrue(error.toString().contains(error.getMessage() + "\n Origin: line 10, amount is a parameter")); } private static LJError verify(String test) { From 548a570e74d55acde4aba32b64ec497f84379ce2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 15:51:44 +0000 Subject: [PATCH 2/8] Say where the wrong state of a receiver comes from A state refinement error now has a From message note when what the verifier knows proves it: - the call that last set the wrong state set, found by walking the receiver's StateChange chain through changes to other sets only, and printed only if that change's instance proves the Found on the set; - else, for a receiver assigned the value of a call and not changed since, what the call's return refinement says about the set, or that it says nothing about it when Found says nothing either; - else, when the walk breaks (a join, a loop head) and the receiver is a local only ever written by its constructor initializer, what the constructor makes it, if Found still says that state. The note names only the sets where no possible state is allowed, when the state machine tells. Instances record the call result they were assigned, and a state-preserving call keeps it, as it keeps the StateChange. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateFromReturnedValue.java | 30 +++ .../processor/context/CallResult.java | 18 ++ .../processor/context/VariableInstance.java | 10 + .../RefinementTypeChecker.java | 11 +- .../refinement_checker/TypeChecker.java | 6 +- .../refinement_checker/VCChecker.java | 9 +- .../MethodsFunctionsChecker.java | 9 + .../object_checkers/AuxStateHandler.java | 23 +- .../object_checkers/StateOrigin.java | 238 ++++++++++++++++++ .../java/liquidjava/utils/constants/Keys.java | 1 + .../liquidjava/api/tests/TestOriginNotes.java | 12 + 11 files changed, 357 insertions(+), 10 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateFromReturnedValue.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/context/CallResult.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateFromReturnedValue.java b/liquidjava-example/src/main/java/testSuite/ErrorStateFromReturnedValue.java new file mode 100644 index 00000000..c2df4553 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateFromReturnedValue.java @@ -0,0 +1,30 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The state of an object assigned the value of a call comes from the call's return refinement +@StateSet(name = "phase", value = {"idle", "running"}) +class FromReturnedTask { + @StateRefinement(to = "idle(this)") + FromReturnedTask() {} + + @StateRefinement(from = "idle(this)", to = "running(this)") + void start() {} + + @StateRefinement(from = "running(this)") + void await() {} + + @Refinement("idle(_)") + static FromReturnedTask create() { + return new FromReturnedTask(); + } +} + +public class ErrorStateFromReturnedValue { + static void use() { + FromReturnedTask task = FromReturnedTask.create(); + task.await(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/CallResult.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/CallResult.java new file mode 100644 index 00000000..411954ad --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/CallResult.java @@ -0,0 +1,18 @@ +package liquidjava.processor.context; + +import liquidjava.rj_language.Predicate; +import spoon.reflect.cu.SourcePosition; + +/** + * The value a call to a refined method returned + * + * @param function + * the method called + * @param returned + * the method's return refinement at this call, with its arguments and receiver substituted and {@code _} for + * the value + * @param position + * where the call is + */ +public record CallResult(RefinedFunction function, Predicate returned, SourcePosition position) { +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java index 3253fca0..83239886 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java @@ -8,6 +8,7 @@ public class VariableInstance extends RefinedVariable { private Variable parent; private StateChange stateChange; + private CallResult returnedBy; public VariableInstance(String name, CtTypeReference type, Predicate c) { super(name, type, c); @@ -43,6 +44,15 @@ public void setStateChange(StateChange stateChange) { this.stateChange = stateChange; } + /** The call whose value this instance was assigned, if it was assigned one and its state has not changed since */ + public Optional getReturnedBy() { + return Optional.ofNullable(returnedBy); + } + + public void setReturnedBy(CallResult returnedBy) { + this.returnedBy = returnedBy; + } + public Optional getParent() { return parent == null ? Optional.empty() : Optional.of(parent); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index f70c4eb7..9081f99f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -99,7 +99,7 @@ public class RefinementTypeChecker extends TypeChecker { ContextHistory contextHistory = ContextHistory.getInstance(); // the metadata that checking an element puts on it private static final List CHECK_METADATA = List.of(Keys.REFINEMENT, Keys.TARGET, Keys.RECEIVER, - Keys.RETURN_VAR_NAME, Keys.STATE_CHANGE); + Keys.RETURN_VAR_NAME, Keys.STATE_CHANGE, Keys.CALL_RESULT); // the loops being checked, innermost first private final Deque loops = new ArrayDeque<>(); @@ -195,9 +195,16 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); AuxStateHandler.addStateRefinements(this, varName, e); + recordReturnedValue(varName, e); } } + /** Records on the new instance of a local variable the call whose value it was assigned, if any */ + private void recordReturnedValue(String name, CtExpression value) { + if (value != null && value.getMetadata(Keys.CALL_RESULT)instanceof CallResult result) + context.getLastVariableInstance(name).ifPresent(instance -> instance.setReturnedBy(result)); + } + @Override public void visitCtCatchVariable(CtCatchVariable catchVariable) { super.visitCtCatchVariable(catchVariable); @@ -271,6 +278,8 @@ private void visitAssignment(CtAssignment assignment) thr CtVariable varDecl = (CtVariable) var.getDeclaration(); String name = var.getSimpleName(); checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl); + if (varDecl instanceof CtLocalVariable && !(assignment instanceof CtOperatorAssignment)) + recordReturnedValue(name, assignment.getAssignment()); } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 7d53e0d1..2cfed2c6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -614,14 +614,14 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage) throws LJError { throwStateRefinementError(position, List.of(declarationPosition), found, expected, customMessage, List.of(), - null, null, List.of()); + null, null, List.of(), List.of()); } public void throwStateRefinementError(SourcePosition position, List declarationPositions, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context, List declarationNotes) throws LJError { + StateErrorContext context, List declarationNotes, List messageNotes) throws LJError { vcChecker.throwStateRefinementError(position, declarationPositions, found, expected, customMessage, hints, - category, context, declarationNotes); + category, context, declarationNotes, messageNotes); } public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index d098937c..d68fdd5a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -459,16 +459,19 @@ protected Predicate shownFound(Predicate found, Predicate expected) { protected void throwStateRefinementError(SourcePosition position, List declarationPositions, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context, List declarationNotes) throws StateRefinementError { + StateErrorContext context, List declarationNotes, List messageNotes) + throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected)); VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified, new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf)); - throw new StateRefinementError(position, declarationPositions, expected, shown, map, customMessage, hints, - category, context, + StateRefinementError error = new StateRefinementError(position, declarationPositions, expected, shown, map, + customMessage, hints, category, context, e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()), declarationNotes); + messageNotes.forEach(error::addMessageNote); + throw error; } /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 0e21f2fb..598d6fc2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -7,6 +7,7 @@ import java.util.Optional; import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.CallResult; import liquidjava.processor.context.Refined; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.RefinedVariable; @@ -358,6 +359,7 @@ private Map checkInvocationRefinements(CtExpression invocatio ? Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(returnViName)) : new Predicate(); invocation.putMetadata(Keys.REFINEMENT, returnRef); + recordCallResult(invocation, f, new Predicate()); return map; } @@ -371,6 +373,12 @@ private Map checkInvocationRefinements(CtExpression invocatio return map; } + /** Records on a call written in the source what it returns, for the variable it is assigned to */ + private static void recordCallResult(CtExpression invocation, RefinedFunction f, Predicate returned) { + if (invocation instanceof CtInvocation && invocation.getPosition().isValidPosition()) + invocation.putMetadata(Keys.CALL_RESULT, new CallResult(f, returned, invocation.getPosition())); + } + /** * Computes a stable return-value instance name so {@code _}/{@code return} in a {@code @StateRefinement to=} clause * matches the post-call VariableInstance. Returns {@code null} for void methods. When the function has no @@ -412,6 +420,7 @@ private void applyReturnRefinement(CtExpression invocation, RefinedFunction f varName = v.getName(); } + recordCallResult(invocation, f, methodRef); String viName = returnViName != null ? returnViName : GeneratedNames.valueOf(invocation, rtc.getContext().getCounter()); VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(), 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 b7497657..eebb613a 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 @@ -827,8 +827,24 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc StateErrorContext context = states .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation))) .orElse(null); + List messageNotes = receiverOf(invocation) + .flatMap(r -> fromNote(tc, vi, r, function, ghostStates, states, prevState, expected, invocation)) + .stream().toList(); tc.throwStateRefinementError(invocation.getPosition(), declarationPositions, prevState, - expectedStatesDisjunction, message, hints, category, context, declarationNotes); + expectedStatesDisjunction, message, hints, category, context, declarationNotes, messageNotes); + } + } + + /** Best effort, like {@link #receiverStates}: see {@link StateOrigin} */ + private static Optional fromNote(TypeChecker tc, VariableInstance receiver, String written, + RefinedFunction function, List ghostStates, Optional states, Predicate found, + Predicate expected, CtElement invocation) { + try { + return StateOrigin.note(tc, receiver, written, function, ghostStates, states.map(ReceiverStates::machine), + states.map(ReceiverStates::current).orElse(Set.of()), found, expected, invocation); + } catch (RuntimeException e) { + DebugLog.warn("Could not tell where the receiver's state comes from: " + e.getMessage()); + return Optional.empty(); } } @@ -1042,8 +1058,9 @@ private static void sameState(TypeChecker tc, VariableInstance variableInstance, Predicate c = variableInstance.getRefinement().substituteVariable(Keys.WILDCARD, newInstanceName) .substituteVariable(variableInstance.getName(), newInstanceName); - addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation) - .setStateChange(variableInstance.getStateChange().orElse(null)); + VariableInstance same = addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation); + same.setStateChange(variableInstance.getStateChange().orElse(null)); + same.setReturnedBy(variableInstance.getReturnedBy().orElse(null)); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java new file mode 100644 index 00000000..67ab7b97 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -0,0 +1,238 @@ +package liquidjava.processor.refinement_checker.object_checkers; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf; + +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + +import liquidjava.diagnostics.DebugLog; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.CallResult; +import liquidjava.processor.context.Context; +import liquidjava.processor.context.GhostFunction; +import liquidjava.processor.context.GhostState; +import liquidjava.processor.context.RefinedFunction; +import liquidjava.processor.context.StateChange; +import liquidjava.processor.context.VariableInstance; +import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.processor.state_machine.State; +import liquidjava.processor.state_machine.StateMachine; +import liquidjava.processor.state_machine.StateSolver; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; +import liquidjava.rj_language.ast.AliasInvocation; +import liquidjava.rj_language.ast.Expression; +import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; +import liquidjava.utils.constants.Keys; +import spoon.reflect.code.CtConstructorCall; +import spoon.reflect.code.CtInvocation; +import spoon.reflect.code.CtLocalVariable; +import spoon.reflect.code.CtVariableRead; +import spoon.reflect.code.CtVariableWrite; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.visitor.filter.TypeFilter; + +/** + * Where the state of the receiver of a call that its state does not allow comes from, as a note of the error: the last + * call that set it, or the call whose value the receiver was assigned. Each note is given only when what the verifier + * knows proves it, and is left out otherwise + */ +final class StateOrigin { + + private final TypeChecker tc; + private final VariableInstance receiver; + private final String written; + private final Set shown; + private final List ghostStates; + private final CtElement invocation; + + /** + * @param receiver + * the receiver's instance before the call + * @param written + * the receiver as written in the call + * @param shown + * the state sets the note is about + */ + private StateOrigin(TypeChecker tc, VariableInstance receiver, String written, Set shown, + List ghostStates, CtElement invocation) { + this.tc = tc; + this.receiver = receiver; + this.written = written; + this.shown = shown; + this.ghostStates = ghostStates; + this.invocation = invocation; + } + + /** + * The note on where the states of the receiver that the failing call checks come from, or of only those of them + * whose state no allowed state has, if the machine tells + * + * @param found + * what is known about the receiver's states before the call + * @param expected + * the states the call needs + */ + static Optional note(TypeChecker tc, VariableInstance receiver, String written, RefinedFunction failing, + List ghostStates, Optional machine, Set current, Predicate found, + Predicate expected, CtElement invocation) throws LJError { + Set checked = setsOf(failing.getFromStates(), ghostStates); + Set wrong = machine.filter(m -> m.models(failing)) + .map(m -> wrongSets(checked, current, m.statesAllowing(failing), ghostStates)).orElse(Set.of()); + StateOrigin origin = new StateOrigin(tc, receiver, written, wrong.isEmpty() ? checked : wrong, ghostStates, + invocation); + return checked.isEmpty() ? Optional.empty() : origin.note(tc.shownFound(found, expected)); + } + + /** The sets where some state the receiver may be in is not the state of any state that allows the call */ + private static Set wrongSets(Set checked, Set current, Set allowing, + List ghostStates) { + return checked.stream() + .filter(set -> !namesIn(allowing, set, ghostStates).containsAll(namesIn(current, set, ghostStates))) + .collect(Collectors.toSet()); + } + + private static Set namesIn(Set states, GhostFunction set, List ghostStates) { + Set names = ghostStates.stream().filter(g -> g.getParent() == set) + .map(g -> Utils.getSimpleName(g.getName())).collect(Collectors.toSet()); + return states.stream().flatMap(s -> s.names().stream()).filter(names::contains).collect(Collectors.toSet()); + } + + private static Set setsOf(List predicates, List ghostStates) { + List states = ghostStates.stream().filter(g -> g.getParent() != null).toList(); + return predicates.stream().flatMap(p -> p.getStateInvocations(states).stream()).map(GhostState::getParent) + .collect(Collectors.toSet()); + } + + private Optional note(Predicate shownFound) throws LJError { + Optional change = receiver.getStateChange(); + if (change.isEmpty()) + return receiver.getReturnedBy().isPresent() ? returnedNote(receiver.getReturnedBy().get(), shownFound) + : creationNote(receiver, shownFound); + VariableInstance after = receiver; + // the changes crossed leave the shown sets as they were: a state refinement keeps the sets it does not name + while (!setsOf(List.of(change.get().change().getTo()), ghostStates).stream().anyMatch(shown::contains)) { + Optional before = change.get().previous(); + if (before.isEmpty()) + return Optional.empty(); + after = before.get(); + change = after.getStateChange(); + if (change.isEmpty()) + return creationNote(after, shownFound); + } + return lastSetNote(change.get(), after, shownFound); + } + + /** That the shown facts of found were last set by {@code change}, if what it gave {@code after} proves them */ + private Optional lastSetNote(StateChange change, VariableInstance after, Predicate shownFound) + throws LJError { + Optional facts = factsOn(shownFound, receiver.getName()); + if (facts.isEmpty() + || !implies(after.getRefinement(), facts.get().substituteVariable(receiver.getName(), after.getName()))) + return Optional.empty(); + return code(change.position()).map(code -> String.format("From: %s, last set at line %d: %s", + display(facts.get(), receiver.getName()), change.position().getLine(), code)); + } + + /** + * What the call the receiver was assigned from returns about the shown sets, if it proves what found says about + * them, or that it says nothing about them when found says nothing either and its return refinement names no state + * of them and no other value the state could come from + */ + private Optional returnedNote(CallResult call, Predicate shownFound) throws LJError { + Optional code = code(call.position()); + if (code.isEmpty()) + return Optional.empty(); + String assigned = String.format("From: %s = %s, line %d, ", written, code.get(), call.position().getLine()); + Optional facts = factsOn(call.returned(), Keys.WILDCARD); + Optional found = factsOn(shownFound, receiver.getName()); + if (facts.isPresent()) + return found.isPresent() + && implies(facts.get().substituteVariable(Keys.WILDCARD, receiver.getName()), found.get()) + ? Optional.of(assigned + "which returns " + display(facts.get(), Keys.WILDCARD)) + : Optional.empty(); + Predicate returned = call.returned(); + // a set declared without a name has a generated one, which the message does not otherwise show + boolean saysNothing = found.isEmpty() + && shown.stream().noneMatch(set -> Utils.getSimpleName(set.getName()).matches(Formats.STATE_SET_NAMES)) + && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains) + && returned.getVariableNames().stream().allMatch(Keys.WILDCARD::equals) + && !hasAlias(returned.getExpression()); + String sets = shown.stream().map(set -> Utils.getSimpleName(set.getName()) + "(" + written + ")").sorted() + .collect(Collectors.joining(", ")); + return saysNothing ? Optional.of(assigned + "which says nothing about " + sets) : Optional.empty(); + } + + /** + * When the receiver is a local variable whose only write is its initializer, a constructor call, what that + * constructor makes it in the shown sets, if found still says it is in that state. It is a fact about the + * constructor only, given when the walk back to the call that last set the state broke, e.g. at a join of branches + */ + private Optional creationNote(VariableInstance unknown, Predicate shownFound) throws LJError { + DebugLog.warn("From note: no known call gives " + unknown.getName() + " its state, e.g. a join of branches"); + if (!(invocation instanceof CtInvocation call && call.getTarget()instanceof CtVariableRead read + && read.getVariable().getDeclaration()instanceof CtLocalVariable local + && local.getDefaultExpression()instanceof CtConstructorCall constructor + && constructor.getMetadata(Keys.STATE_CHANGE)instanceof StateChange created + && created.function().getAllStates().size() == 1 && !writtenAfterDeclaration(local))) + return Optional.empty(); + Optional facts = factsOn(created.change().getTo(), Keys.THIS); + Optional found = factsOn(shownFound, receiver.getName()); + Optional code = code(created.position()); + if (facts.isEmpty() || found.isEmpty() || code.isEmpty() + || !implies(found.get(), facts.get().substituteVariable(Keys.THIS, receiver.getName()))) + return Optional.empty(); + return Optional.of(String.format("From: %s is created at line %d by %s, which makes it %s", written, + created.position().getLine(), code.get(), display(facts.get(), Keys.THIS))); + } + + private static boolean writtenAfterDeclaration(CtLocalVariable local) { + CtExecutable scope = local.getParent(CtExecutable.class); + return scope == null || scope.getElements(new TypeFilter<>(CtVariableWrite.class)).stream() + .anyMatch(write -> write.getVariable().getDeclaration() == local); + } + + /** + * The facts of {@code predicate} on the shown sets of {@code object} alone, e.g. {@code unmarked(object)}, or empty + * if it has none + */ + private Optional factsOn(Predicate predicate, String object) { + return factsOf(predicate.getExpression()).stream().map(Predicate::new) + .filter(fact -> fact.getVariableNames().stream().allMatch(object::equals)) + .filter(fact -> !setsOf(List.of(fact), ghostStates).isEmpty() + && shown.containsAll(setsOf(List.of(fact), ghostStates))) + .reduce(Predicate::createConjunction); + } + + /** The facts as the error shows them, about the receiver as written */ + private String display(Predicate facts, String object) { + Context context = tc.getContext(); + Expression shownFacts = facts.substituteVariable(object, written).getExpression(); + return StateValues.toSetForm(shownFacts, context.getGhostStates(), context.getGhosts()).toDisplayString(); + } + + private boolean implies(Predicate premise, Predicate conclusion) throws LJError { + return new StateSolver(tc, invocation.getPosition()).implies(premise, conclusion); + } + + private static boolean hasAlias(Expression expression) { + return expression instanceof AliasInvocation + || expression.getChildren().stream().anyMatch(StateOrigin::hasAlias); + } + + /** The code at {@code position} on one line, without the semicolon of a statement */ + private static Optional code(SourcePosition position) { + if (position == null || !position.isValidPosition() || position.getCompilationUnit() == null) + return Optional.empty(); + String source = position.getCompilationUnit().getOriginalSourceCode(); + if (source == null || position.getSourceEnd() >= source.length()) + return Optional.empty(); + String code = source.substring(position.getSourceStart(), position.getSourceEnd() + 1); + return Optional.of(code.strip().replaceAll("\\s+", " ").replaceAll(";$", "")); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index ce7f5d84..58a51158 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -7,6 +7,7 @@ public final class Keys { public static final String RECEIVER = "receiver"; public static final String RETURN_VAR_NAME = "return_var_name"; public static final String STATE_CHANGE = "state_change"; + public static final String CALL_RESULT = "call_result"; public static final String THIS = "this"; public static final String WILDCARD = "_"; public static final String OLD = "old"; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index 898e0a3c..13ece662 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -22,6 +22,18 @@ void unrefinedParameterIsNamedWithItsMethod() { assertTrue(error.toString().contains(error.getMessage() + "\n Origin: line 10, amount is a parameter")); } + @Test + void stateIsTracedToTheCallThatLastSetTheSetThatIsWrong() { + assertEquals(List.of("From: lockState(d) == locked, last set at line 27: d.lock()"), + verify("ErrorStateHintMultipleSets.java").getMessageNotes()); + } + + @Test + void stateIsTracedToTheReturnRefinementOfTheCallAssigned() { + assertEquals(List.of("From: task = FromReturnedTask.create(), line 27, which returns phase(task) == idle"), + verify("ErrorStateFromReturnedValue.java").getMessageNotes()); + } + private static LJError verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); From 8f82b3467df494522878ca770037c53ce08b12bc Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 16:35:13 +0000 Subject: [PATCH 3/8] Leave out the From note for an aliased receiver, and follow a returned value across other sets - No note when the receiver may be held by another name before the call: a local or parameter copied, returned or captured by a lambda or local class earlier or in a loop around the call, or a field. - The creation note also needs no other call on the local to a method that changes state, nor a failing call a loop repeats. - A walk that crosses changes to other sets and reaches the call result the receiver was assigned gives the returned-value note, reading what Found says about that instance. Co-Authored-By: Claude Opus 5.5 --- .../object_checkers/StateOrigin.java | 136 ++++++++++++++---- .../liquidjava/api/tests/TestOriginNotes.java | 8 ++ 2 files changed, 119 insertions(+), 25 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java index 67ab7b97..fd28bb6b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -13,6 +13,7 @@ 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; import liquidjava.processor.context.StateChange; import liquidjava.processor.context.VariableInstance; @@ -27,14 +28,24 @@ import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; +import spoon.reflect.code.CtAssignment; +import spoon.reflect.code.CtConditional; import spoon.reflect.code.CtConstructorCall; +import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtFieldRead; +import spoon.reflect.code.CtLambda; +import spoon.reflect.code.CtLoop; +import spoon.reflect.code.CtReturn; +import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLocalVariable; import spoon.reflect.code.CtVariableRead; import spoon.reflect.code.CtVariableWrite; import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtVariable; import spoon.reflect.visitor.filter.TypeFilter; /** @@ -109,34 +120,85 @@ private static Set setsOf(List predicates, List note(Predicate shownFound) throws LJError { - Optional change = receiver.getStateChange(); - if (change.isEmpty()) - return receiver.getReturnedBy().isPresent() ? returnedNote(receiver.getReturnedBy().get(), shownFound) - : creationNote(receiver, shownFound); - VariableInstance after = receiver; - // the changes crossed leave the shown sets as they were: a state refinement keeps the sets it does not name - while (!setsOf(List.of(change.get().change().getTo()), ghostStates).stream().anyMatch(shown::contains)) { + if (mayBeAliased()) + return Optional.empty(); + VariableInstance at = receiver; + while (true) { + Optional change = at.getStateChange(); + if (change.isEmpty()) + return at.getReturnedBy().isPresent() ? returnedNote(at.getReturnedBy().get(), at, shownFound) + : creationNote(at, shownFound); + if (setsOf(List.of(change.get().change().getTo()), ghostStates).stream().anyMatch(shown::contains)) + return lastSetNote(change.get(), at, shownFound); Optional before = change.get().previous(); if (before.isEmpty()) return Optional.empty(); - after = before.get(); - change = after.getStateChange(); - if (change.isEmpty()) - return creationNote(after, shownFound); + at = before.get(); } - return lastSetNote(change.get(), after, shownFound); + } + + /** + * Whether another name may hold the receiver, through which its state may change unseen: a local or parameter + * copied to another variable, returned, or used in a lambda or a local class. A field, which other code may also + * reach, counts as aliased; {@code this} does not + */ + private boolean mayBeAliased() { + CtExpression target = invocation instanceof CtInvocation call ? call.getTarget() : null; + if (target == null || target.isImplicit() || target instanceof CtThisAccess) + return false; + if (!(target instanceof CtVariableRead read && !(read instanceof CtFieldRead))) + return true; + CtVariable variable = read.getVariable().getDeclaration(); + CtExecutable scope = invocation.getParent(CtExecutable.class); + if (variable == null || scope == null) + return true; + return scope.getElements(new TypeFilter<>(CtVariableRead.class)).stream() + .filter(use -> use.getVariable().getDeclaration() == variable && mayRunBefore(use, scope)) + .anyMatch(use -> isCopied(use, scope)); + } + + /** Whether {@code use} may run before the failing call: it comes earlier, or a loop around both repeats it */ + private boolean mayRunBefore(CtElement use, CtExecutable scope) { + if (use.getPosition().getSourceEnd() < invocation.getPosition().getSourceStart()) + return true; + for (CtLoop loop = invocation.getParent(CtLoop.class); loop != null + && loop.hasParent(scope); loop = loop.getParent(CtLoop.class)) + if (use.hasParent(loop)) + return true; + return false; + } + + private static boolean isCopied(CtVariableRead use, CtExecutable scope) { + CtElement parent = use.getParent(); + CtElement nested = use.getParent(e -> e instanceof CtLambda || e instanceof CtClass); + return parent instanceof CtLocalVariable + || parent instanceof CtAssignment assignment && assignment.getAssignment() == use + || parent instanceof CtReturn || parent instanceof CtConditional + || nested != null && nested.hasParent(scope); + } + + /** + * The facts of found on the shown sets, about {@code at}: those about the receiver, which has the state of + * {@code at} in those sets, or else those about {@code at} + */ + private Optional foundAbout(VariableInstance at, Predicate shownFound) { + return factsOn(shownFound, receiver.getName()).map(f -> f.substituteVariable(receiver.getName(), at.getName())) + .or(() -> factsOn(shownFound, at.getName())); } /** That the shown facts of found were last set by {@code change}, if what it gave {@code after} proves them */ private Optional lastSetNote(StateChange change, VariableInstance after, Predicate shownFound) throws LJError { - Optional facts = factsOn(shownFound, receiver.getName()); - if (facts.isEmpty() - || !implies(after.getRefinement(), facts.get().substituteVariable(receiver.getName(), after.getName()))) + Optional facts = foundAbout(after, shownFound); + if (facts.isEmpty() || !implies(after.getRefinement(), facts.get())) return Optional.empty(); return code(change.position()).map(code -> String.format("From: %s, last set at line %d: %s", - display(facts.get(), receiver.getName()), change.position().getLine(), code)); + display(facts.get(), after.getName()), change.position().getLine(), code)); } /** @@ -144,17 +206,18 @@ private Optional lastSetNote(StateChange change, VariableInstance after, * them, or that it says nothing about them when found says nothing either and its return refinement names no state * of them and no other value the state could come from */ - private Optional returnedNote(CallResult call, Predicate shownFound) throws LJError { + private Optional returnedNote(CallResult call, VariableInstance assigned, Predicate shownFound) + throws LJError { Optional code = code(call.position()); if (code.isEmpty()) return Optional.empty(); - String assigned = String.format("From: %s = %s, line %d, ", written, code.get(), call.position().getLine()); + String from = String.format("From: %s = %s, line %d, ", written, code.get(), call.position().getLine()); Optional facts = factsOn(call.returned(), Keys.WILDCARD); - Optional found = factsOn(shownFound, receiver.getName()); + Optional found = foundAbout(assigned, shownFound); if (facts.isPresent()) return found.isPresent() - && implies(facts.get().substituteVariable(Keys.WILDCARD, receiver.getName()), found.get()) - ? Optional.of(assigned + "which returns " + display(facts.get(), Keys.WILDCARD)) + && implies(facts.get().substituteVariable(Keys.WILDCARD, assigned.getName()), found.get()) + ? Optional.of(from + "which returns " + display(facts.get(), Keys.WILDCARD)) : Optional.empty(); Predicate returned = call.returned(); // a set declared without a name has a generated one, which the message does not otherwise show @@ -165,7 +228,7 @@ && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains) && !hasAlias(returned.getExpression()); String sets = shown.stream().map(set -> Utils.getSimpleName(set.getName()) + "(" + written + ")").sorted() .collect(Collectors.joining(", ")); - return saysNothing ? Optional.of(assigned + "which says nothing about " + sets) : Optional.empty(); + return saysNothing ? Optional.of(from + "which says nothing about " + sets) : Optional.empty(); } /** @@ -179,18 +242,41 @@ private Optional creationNote(VariableInstance unknown, Predicate shownF && read.getVariable().getDeclaration()instanceof CtLocalVariable local && local.getDefaultExpression()instanceof CtConstructorCall constructor && constructor.getMetadata(Keys.STATE_CHANGE)instanceof StateChange created - && created.function().getAllStates().size() == 1 && !writtenAfterDeclaration(local))) + && created.function().getAllStates().size() == 1 && !writtenAfterDeclaration(local) + && !changedByAnotherCall(local))) return Optional.empty(); Optional facts = factsOn(created.change().getTo(), Keys.THIS); - Optional found = factsOn(shownFound, receiver.getName()); + Optional found = foundAbout(unknown, shownFound); Optional code = code(created.position()); if (facts.isEmpty() || found.isEmpty() || code.isEmpty() - || !implies(found.get(), facts.get().substituteVariable(Keys.THIS, receiver.getName()))) + || !implies(found.get(), facts.get().substituteVariable(Keys.THIS, unknown.getName()))) return Optional.empty(); return Optional.of(String.format("From: %s is created at line %d by %s, which makes it %s", written, created.position().getLine(), code.get(), display(facts.get(), Keys.THIS))); } + /** + * Whether a call on the local other than the failing one, or the failing one if a loop may repeat it, is to a + * method that changes the state of an object, so the state may come from that call rather than the constructor + */ + private boolean changedByAnotherCall(CtLocalVariable local) { + CtExecutable scope = local.getParent(CtExecutable.class); + boolean repeated = invocation.getParent(CtLoop.class) != null + && invocation.getParent(CtLoop.class).hasParent(scope); + return scope.getElements(new TypeFilter<>(CtInvocation.class)).stream() + .filter(call -> call.getTarget()instanceof CtVariableRead read + && read.getVariable().getDeclaration() == local && (call != invocation || repeated)) + .anyMatch(this::mayChangeState); + } + + /** Whether some method with the name and arity of the invoked one changes the state of its receiver */ + private boolean mayChangeState(CtInvocation call) { + String name = call.getExecutable().getSimpleName(); + int arity = call.getArguments().size(); + return tc.getContext().getCtxFunctions().stream().anyMatch(f -> Utils.getSimpleName(f.getName()).equals(name) + && f.getArguments().size() == arity && f.getAllStates().stream().anyMatch(ObjectState::hasTo)); + } + private static boolean writtenAfterDeclaration(CtLocalVariable local) { CtExecutable scope = local.getParent(CtExecutable.class); return scope == null || scope.getElements(new TypeFilter<>(CtVariableWrite.class)).stream() diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index 13ece662..6e0ceba6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -34,6 +34,14 @@ void stateIsTracedToTheReturnRefinementOfTheCallAssigned() { verify("ErrorStateFromReturnedValue.java").getMessageNotes()); } + @Test + void stateOfAReceiverAnotherNameMayHoldIsNotTraced() { + CommandLineLauncher.launch(TEST_SUITE + "ErrorDeferredCallbackState.java"); + LJError captured = Diagnostics.getInstance().getErrors().stream().filter(e -> e.getPosition().getLine() == 37) + .findFirst().orElseThrow(); + assertEquals(List.of(), captured.getMessageNotes()); + } + private static LJError verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); From 496759c545473e44c9c44d7fe1bce5561ce5ba93 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 16:50:50 +0000 Subject: [PATCH 4/8] Count a receiver passed to a method as aliased, and say only what a change set - A local or parameter used before the call other than as a call's receiver or in a comparison (passed to a method, stored in an array, copied) may be held by another name, so it gets no From note. A use in a return or a throw cannot run again in a loop around the call. - The last-set note shows only the facts on the shown sets the change names, so a change to one of two wrong sets is not given the other. Co-Authored-By: Claude Opus 5.5 --- .../object_checkers/StateOrigin.java | 61 +++++++++++-------- 1 file changed, 37 insertions(+), 24 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java index fd28bb6b..684434ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -28,8 +28,8 @@ import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; -import spoon.reflect.code.CtAssignment; -import spoon.reflect.code.CtConditional; +import spoon.reflect.code.BinaryOperatorKind; +import spoon.reflect.code.CtBinaryOperator; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; @@ -37,6 +37,7 @@ import spoon.reflect.code.CtLoop; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtThisAccess; +import spoon.reflect.code.CtThrow; import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLocalVariable; import spoon.reflect.code.CtVariableRead; @@ -143,9 +144,10 @@ private Optional note(Predicate shownFound) throws LJError { } /** - * Whether another name may hold the receiver, through which its state may change unseen: a local or parameter - * copied to another variable, returned, or used in a lambda or a local class. A field, which other code may also - * reach, counts as aliased; {@code this} does not + * Whether another name may hold the receiver, through which its state may change unseen: a local or parameter used + * before the call other than as the receiver of a call or in a comparison, e.g. copied, passed to a method, stored + * in an array or used in a lambda or a local class. A field, which other code may also reach, counts as aliased; + * {@code this} does not */ private boolean mayBeAliased() { CtExpression target = invocation instanceof CtInvocation call ? call.getTarget() : null; @@ -159,42 +161,53 @@ private boolean mayBeAliased() { return true; return scope.getElements(new TypeFilter<>(CtVariableRead.class)).stream() .filter(use -> use.getVariable().getDeclaration() == variable && mayRunBefore(use, scope)) - .anyMatch(use -> isCopied(use, scope)); + .anyMatch(use -> escapes(use, scope)); } - /** Whether {@code use} may run before the failing call: it comes earlier, or a loop around both repeats it */ + /** + * Whether {@code use} may run before the failing call: it comes earlier, or a loop around both may repeat it, + * unless it is in a return or a throw, which leaves the loop + */ private boolean mayRunBefore(CtElement use, CtExecutable scope) { if (use.getPosition().getSourceEnd() < invocation.getPosition().getSourceStart()) return true; + CtElement exit = use.getParent(e -> e instanceof CtReturn || e instanceof CtThrow); for (CtLoop loop = invocation.getParent(CtLoop.class); loop != null && loop.hasParent(scope); loop = loop.getParent(CtLoop.class)) - if (use.hasParent(loop)) + if (use.hasParent(loop) && (exit == null || !exit.hasParent(loop))) return true; return false; } - private static boolean isCopied(CtVariableRead use, CtExecutable scope) { + /** Whether the object {@code use} reads may afterwards be reached through it by another name */ + private static boolean escapes(CtVariableRead use, CtExecutable scope) { CtElement parent = use.getParent(); CtElement nested = use.getParent(e -> e instanceof CtLambda || e instanceof CtClass); - return parent instanceof CtLocalVariable - || parent instanceof CtAssignment assignment && assignment.getAssignment() == use - || parent instanceof CtReturn || parent instanceof CtConditional - || nested != null && nested.hasParent(scope); + boolean receiver = parent instanceof CtInvocation call && call.getTarget() == use; + boolean compared = parent instanceof CtBinaryOperator operator + && (operator.getKind() == BinaryOperatorKind.EQ || operator.getKind() == BinaryOperatorKind.NE); + return !(receiver || compared) || nested != null && nested.hasParent(scope); } /** * The facts of found on the shown sets, about {@code at}: those about the receiver, which has the state of * {@code at} in those sets, or else those about {@code at} */ - private Optional foundAbout(VariableInstance at, Predicate shownFound) { - return factsOn(shownFound, receiver.getName()).map(f -> f.substituteVariable(receiver.getName(), at.getName())) - .or(() -> factsOn(shownFound, at.getName())); + private Optional foundAbout(VariableInstance at, Predicate shownFound, Set sets) { + return factsOn(shownFound, receiver.getName(), sets) + .map(f -> f.substituteVariable(receiver.getName(), at.getName())) + .or(() -> factsOn(shownFound, at.getName(), sets)); } - /** That the shown facts of found were last set by {@code change}, if what it gave {@code after} proves them */ + /** + * That the facts of found on the shown sets {@code change} names were last set by it, if what it gave {@code after} + * proves them + */ private Optional lastSetNote(StateChange change, VariableInstance after, Predicate shownFound) throws LJError { - Optional facts = foundAbout(after, shownFound); + Set changed = setsOf(List.of(change.change().getTo()), ghostStates).stream() + .filter(shown::contains).collect(Collectors.toSet()); + Optional facts = foundAbout(after, shownFound, changed); if (facts.isEmpty() || !implies(after.getRefinement(), facts.get())) return Optional.empty(); return code(change.position()).map(code -> String.format("From: %s, last set at line %d: %s", @@ -212,8 +225,8 @@ private Optional returnedNote(CallResult call, VariableInstance assigned if (code.isEmpty()) return Optional.empty(); String from = String.format("From: %s = %s, line %d, ", written, code.get(), call.position().getLine()); - Optional facts = factsOn(call.returned(), Keys.WILDCARD); - Optional found = foundAbout(assigned, shownFound); + Optional facts = factsOn(call.returned(), Keys.WILDCARD, shown); + Optional found = foundAbout(assigned, shownFound, shown); if (facts.isPresent()) return found.isPresent() && implies(facts.get().substituteVariable(Keys.WILDCARD, assigned.getName()), found.get()) @@ -245,8 +258,8 @@ private Optional creationNote(VariableInstance unknown, Predicate shownF && created.function().getAllStates().size() == 1 && !writtenAfterDeclaration(local) && !changedByAnotherCall(local))) return Optional.empty(); - Optional facts = factsOn(created.change().getTo(), Keys.THIS); - Optional found = foundAbout(unknown, shownFound); + Optional facts = factsOn(created.change().getTo(), Keys.THIS, shown); + Optional found = foundAbout(unknown, shownFound, shown); Optional code = code(created.position()); if (facts.isEmpty() || found.isEmpty() || code.isEmpty() || !implies(found.get(), facts.get().substituteVariable(Keys.THIS, unknown.getName()))) @@ -287,11 +300,11 @@ private static boolean writtenAfterDeclaration(CtLocalVariable local) { * The facts of {@code predicate} on the shown sets of {@code object} alone, e.g. {@code unmarked(object)}, or empty * if it has none */ - private Optional factsOn(Predicate predicate, String object) { + private Optional factsOn(Predicate predicate, String object, Set sets) { return factsOf(predicate.getExpression()).stream().map(Predicate::new) .filter(fact -> fact.getVariableNames().stream().allMatch(object::equals)) .filter(fact -> !setsOf(List.of(fact), ghostStates).isEmpty() - && shown.containsAll(setsOf(List.of(fact), ghostStates))) + && sets.containsAll(setsOf(List.of(fact), ghostStates))) .reduce(Predicate::createConjunction); } From 160ad7286e4d9e0397e6d47576b5634820cab0c7 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 17:06:28 +0000 Subject: [PATCH 5/8] Leave out the From note after an unspecified method body on the receiver - No note when a method of the analyzed code with no state refinement is called on the receiver before the failing call: the verifier takes it to keep the state, which its body may still change. - "says nothing" also needs the called method to give no state through a state refinement, as to = "running(_)" does. Co-Authored-By: Claude Opus 5.5 --- .../object_checkers/StateOrigin.java | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java index 684434ea..fda20f52 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -46,6 +46,7 @@ import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtVariable; import spoon.reflect.visitor.filter.TypeFilter; @@ -161,7 +162,18 @@ private boolean mayBeAliased() { return true; return scope.getElements(new TypeFilter<>(CtVariableRead.class)).stream() .filter(use -> use.getVariable().getDeclaration() == variable && mayRunBefore(use, scope)) - .anyMatch(use -> escapes(use, scope)); + .anyMatch(use -> escapes(use, scope) || callsUnspecifiedBody(use)); + } + + /** + * Whether {@code use} is the receiver of a call to a method of the analyzed code with no state refinement: the + * verifier takes it to keep the state, which its body may still change + */ + private boolean callsUnspecifiedBody(CtVariableRead use) { + return use.getParent()instanceof CtInvocation call && call != invocation && call.getTarget() == use + && call.getExecutable().getDeclaration()instanceof CtMethod method && method.getBody() != null + && method.getAnnotations().stream().noneMatch(a -> a.getAnnotationType().getQualifiedName() + .equals("liquidjava.specification.StateRefinement")); } /** @@ -234,7 +246,8 @@ && implies(facts.get().substituteVariable(Keys.WILDCARD, assigned.getName()), fo : Optional.empty(); Predicate returned = call.returned(); // a set declared without a name has a generated one, which the message does not otherwise show - boolean saysNothing = found.isEmpty() + // a state refinement of the method may give the value its state, as `to = "running(_)"` does + boolean saysNothing = found.isEmpty() && call.function().getAllStates().stream().noneMatch(ObjectState::hasTo) && shown.stream().noneMatch(set -> Utils.getSimpleName(set.getName()).matches(Formats.STATE_SET_NAMES)) && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains) && returned.getVariableNames().stream().allMatch(Keys.WILDCARD::equals) From 5bb7647f9c5383c0cb3b7f89c9744896baba0e17 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 17:29:50 +0000 Subject: [PATCH 6/8] Apply the alias checks to this and to the failing call's own arguments Co-Authored-By: Claude Opus 5.5 --- .../object_checkers/StateOrigin.java | 50 ++++++++++++------- 1 file changed, 31 insertions(+), 19 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java index fda20f52..7f1497e3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -37,6 +37,7 @@ import spoon.reflect.code.CtLoop; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtThisAccess; +import spoon.reflect.code.CtTargetedExpression; import spoon.reflect.code.CtThrow; import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLocalVariable; @@ -47,6 +48,7 @@ import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtMethod; +import spoon.reflect.declaration.CtType; import spoon.reflect.declaration.CtVariable; import spoon.reflect.visitor.filter.TypeFilter; @@ -145,23 +147,30 @@ private Optional note(Predicate shownFound) throws LJError { } /** - * Whether another name may hold the receiver, through which its state may change unseen: a local or parameter used - * before the call other than as the receiver of a call or in a comparison, e.g. copied, passed to a method, stored - * in an array or used in a lambda or a local class. A field, which other code may also reach, counts as aliased; - * {@code this} does not + * Whether another name may hold the receiver, through which its state may change unseen, or a method body may + * change it: before the call, the receiver is used other than as the target of a call or field access or in a + * comparison (copied, passed to a method, stored in an array, used in a lambda or a local class), or a method of + * the analyzed code with no state refinement is called on it. A field, which other code may also reach, counts as + * aliased */ private boolean mayBeAliased() { CtExpression target = invocation instanceof CtInvocation call ? call.getTarget() : null; - if (target == null || target.isImplicit() || target instanceof CtThisAccess) - return false; - if (!(target instanceof CtVariableRead read && !(read instanceof CtFieldRead))) - return true; - CtVariable variable = read.getVariable().getDeclaration(); CtExecutable scope = invocation.getParent(CtExecutable.class); - if (variable == null || scope == null) + if (scope == null) + return true; + List uses; + if (target == null || target.isImplicit() || target instanceof CtThisAccess) { + CtType owner = invocation.getParent(CtType.class); + uses = scope.getElements(new TypeFilter<>(CtThisAccess.class)).stream() + .filter(use -> use.getParent(CtType.class) == owner).map(CtElement.class::cast).toList(); + } else if (target instanceof CtVariableRead read && !(read instanceof CtFieldRead) + && read.getVariable().getDeclaration() != null) { + CtVariable variable = read.getVariable().getDeclaration(); + uses = scope.getElements(new TypeFilter<>(CtVariableRead.class)).stream() + .filter(use -> use.getVariable().getDeclaration() == variable).map(CtElement.class::cast).toList(); + } else return true; - return scope.getElements(new TypeFilter<>(CtVariableRead.class)).stream() - .filter(use -> use.getVariable().getDeclaration() == variable && mayRunBefore(use, scope)) + return uses.stream().filter(use -> mayRunBefore(use, scope)) .anyMatch(use -> escapes(use, scope) || callsUnspecifiedBody(use)); } @@ -169,7 +178,7 @@ private boolean mayBeAliased() { * Whether {@code use} is the receiver of a call to a method of the analyzed code with no state refinement: the * verifier takes it to keep the state, which its body may still change */ - private boolean callsUnspecifiedBody(CtVariableRead use) { + private boolean callsUnspecifiedBody(CtElement use) { return use.getParent()instanceof CtInvocation call && call != invocation && call.getTarget() == use && call.getExecutable().getDeclaration()instanceof CtMethod method && method.getBody() != null && method.getAnnotations().stream().noneMatch(a -> a.getAnnotationType().getQualifiedName() @@ -177,12 +186,15 @@ private boolean callsUnspecifiedBody(CtVariableRead use) { } /** - * Whether {@code use} may run before the failing call: it comes earlier, or a loop around both may repeat it, - * unless it is in a return or a throw, which leaves the loop + * Whether {@code use} may run before the failing call: it comes earlier, is one of its arguments, or a loop around + * both may repeat it, unless it is in a return or a throw, which leaves the loop */ private boolean mayRunBefore(CtElement use, CtExecutable scope) { if (use.getPosition().getSourceEnd() < invocation.getPosition().getSourceStart()) return true; + if (invocation instanceof CtInvocation call + && call.getArguments().stream().anyMatch(argument -> argument == use || use.hasParent(argument))) + return true; CtElement exit = use.getParent(e -> e instanceof CtReturn || e instanceof CtThrow); for (CtLoop loop = invocation.getParent(CtLoop.class); loop != null && loop.hasParent(scope); loop = loop.getParent(CtLoop.class)) @@ -191,14 +203,14 @@ private boolean mayRunBefore(CtElement use, CtExecutable scope) { return false; } - /** Whether the object {@code use} reads may afterwards be reached through it by another name */ - private static boolean escapes(CtVariableRead use, CtExecutable scope) { + /** Whether the object {@code use} gives may afterwards be reached through it by another name */ + private static boolean escapes(CtElement use, CtExecutable scope) { CtElement parent = use.getParent(); CtElement nested = use.getParent(e -> e instanceof CtLambda || e instanceof CtClass); - boolean receiver = parent instanceof CtInvocation call && call.getTarget() == use; + boolean target = parent instanceof CtTargetedExpression targeted && targeted.getTarget() == use; boolean compared = parent instanceof CtBinaryOperator operator && (operator.getKind() == BinaryOperatorKind.EQ || operator.getKind() == BinaryOperatorKind.NE); - return !(receiver || compared) || nested != null && nested.hasParent(scope); + return !(target || compared) || nested != null && nested.hasParent(scope); } /** From bf683fa4deb935ffea8586b15c80bdc93fd3a51d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 17:41:50 +0000 Subject: [PATCH 7/8] Count a method reference to the receiver as aliasing it Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/object_checkers/AuxStateHandler.java | 1 + .../refinement_checker/object_checkers/StateOrigin.java | 5 ++++- 2 files changed, 5 insertions(+), 1 deletion(-) 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 eebb613a..2f829243 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 @@ -843,6 +843,7 @@ private static Optional fromNote(TypeChecker tc, VariableInstance receiv return StateOrigin.note(tc, receiver, written, function, ghostStates, states.map(ReceiverStates::machine), states.map(ReceiverStates::current).orElse(Set.of()), found, expected, invocation); } catch (RuntimeException e) { + // also an LJError, such as an unknown solver result: the note is left out, the error is still reported DebugLog.warn("Could not tell where the receiver's state comes from: " + e.getMessage()); return Optional.empty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java index 7f1497e3..0ad4af34 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -32,6 +32,7 @@ import spoon.reflect.code.CtBinaryOperator; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtFieldAccess; import spoon.reflect.code.CtFieldRead; import spoon.reflect.code.CtLambda; import spoon.reflect.code.CtLoop; @@ -207,7 +208,9 @@ private boolean mayRunBefore(CtElement use, CtExecutable scope) { private static boolean escapes(CtElement use, CtExecutable scope) { CtElement parent = use.getParent(); CtElement nested = use.getParent(e -> e instanceof CtLambda || e instanceof CtClass); - boolean target = parent instanceof CtTargetedExpression targeted && targeted.getTarget() == use; + // a method reference, such as task::start, keeps its target for later + boolean target = (parent instanceof CtInvocation || parent instanceof CtFieldAccess) + && ((CtTargetedExpression) parent).getTarget() == use; boolean compared = parent instanceof CtBinaryOperator operator && (operator.getKind() == BinaryOperatorKind.EQ || operator.getKind() == BinaryOperatorKind.NE); return !(target || compared) || nested != null && nested.hasParent(scope); From 51666ee921aeaa4b3dec225befc05a4eb8b8b10b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:56:20 +0000 Subject: [PATCH 8/8] Write the state origin notes as Origin: line L, - the call that last set the sets "makes" their state; - a call the receiver was assigned "returns" it, or "says nothing about" the sets; - the creation fact says the constructor "creates" the receiver with its state, not that it makes the current one. Co-Authored-By: Claude Opus 5.5 --- .../object_checkers/StateOrigin.java | 19 ++++++++++--------- .../liquidjava/api/tests/TestOriginNotes.java | 4 ++-- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java index 0ad4af34..043d3eac 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -237,8 +237,9 @@ private Optional lastSetNote(StateChange change, VariableInstance after, Optional facts = foundAbout(after, shownFound, changed); if (facts.isEmpty() || !implies(after.getRefinement(), facts.get())) return Optional.empty(); - return code(change.position()).map(code -> String.format("From: %s, last set at line %d: %s", - display(facts.get(), after.getName()), change.position().getLine(), code)); + // the call last set these sets, so it is what makes them so + return code(change.position()).map(code -> String.format("Origin: line %d, %s makes %s", + change.position().getLine(), code, display(facts.get(), after.getName()))); } /** @@ -251,14 +252,13 @@ private Optional returnedNote(CallResult call, VariableInstance assigned Optional code = code(call.position()); if (code.isEmpty()) return Optional.empty(); - String from = String.format("From: %s = %s, line %d, ", written, code.get(), call.position().getLine()); + String origin = String.format("Origin: line %d, %s ", call.position().getLine(), code.get()); Optional facts = factsOn(call.returned(), Keys.WILDCARD, shown); Optional found = foundAbout(assigned, shownFound, shown); if (facts.isPresent()) return found.isPresent() && implies(facts.get().substituteVariable(Keys.WILDCARD, assigned.getName()), found.get()) - ? Optional.of(from + "which returns " + display(facts.get(), Keys.WILDCARD)) - : Optional.empty(); + ? Optional.of(origin + "returns " + display(facts.get(), Keys.WILDCARD)) : Optional.empty(); Predicate returned = call.returned(); // a set declared without a name has a generated one, which the message does not otherwise show // a state refinement of the method may give the value its state, as `to = "running(_)"` does @@ -269,7 +269,7 @@ && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains) && !hasAlias(returned.getExpression()); String sets = shown.stream().map(set -> Utils.getSimpleName(set.getName()) + "(" + written + ")").sorted() .collect(Collectors.joining(", ")); - return saysNothing ? Optional.of(from + "which says nothing about " + sets) : Optional.empty(); + return saysNothing ? Optional.of(origin + "says nothing about " + sets) : Optional.empty(); } /** @@ -278,7 +278,7 @@ && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains) * constructor only, given when the walk back to the call that last set the state broke, e.g. at a join of branches */ private Optional creationNote(VariableInstance unknown, Predicate shownFound) throws LJError { - DebugLog.warn("From note: no known call gives " + unknown.getName() + " its state, e.g. a join of branches"); + DebugLog.warn("Origin note: no known call gives " + unknown.getName() + " its state, e.g. a join of branches"); if (!(invocation instanceof CtInvocation call && call.getTarget()instanceof CtVariableRead read && read.getVariable().getDeclaration()instanceof CtLocalVariable local && local.getDefaultExpression()instanceof CtConstructorCall constructor @@ -292,8 +292,9 @@ private Optional creationNote(VariableInstance unknown, Predicate shownF if (facts.isEmpty() || found.isEmpty() || code.isEmpty() || !implies(found.get(), facts.get().substituteVariable(Keys.THIS, unknown.getName()))) return Optional.empty(); - return Optional.of(String.format("From: %s is created at line %d by %s, which makes it %s", written, - created.position().getLine(), code.get(), display(facts.get(), Keys.THIS))); + // not "makes": a later call may have set the state again, which found no longer tells + return Optional.of(String.format("Origin: line %d, %s creates %s with %s", created.position().getLine(), + code.get(), written, display(facts.get(), Keys.THIS))); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index 6e0ceba6..4eaaf74b 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -24,13 +24,13 @@ void unrefinedParameterIsNamedWithItsMethod() { @Test void stateIsTracedToTheCallThatLastSetTheSetThatIsWrong() { - assertEquals(List.of("From: lockState(d) == locked, last set at line 27: d.lock()"), + assertEquals(List.of("Origin: line 27, d.lock() makes lockState(d) == locked"), verify("ErrorStateHintMultipleSets.java").getMessageNotes()); } @Test void stateIsTracedToTheReturnRefinementOfTheCallAssigned() { - assertEquals(List.of("From: task = FromReturnedTask.create(), line 27, which returns phase(task) == idle"), + assertEquals(List.of("Origin: line 27, FromReturnedTask.create() returns phase(task) == idle"), verify("ErrorStateFromReturnedValue.java").getMessageNotes()); }