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/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/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 5562e1ac..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 @@ -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; } } @@ -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..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 @@ -827,8 +827,25 @@ 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) { + // 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(); } } @@ -1042,8 +1059,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..043d3eac --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java @@ -0,0 +1,366 @@ +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.ObjectState; +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.BinaryOperatorKind; +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; +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; +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.CtMethod; +import spoon.reflect.declaration.CtType; +import spoon.reflect.declaration.CtVariable; +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()); + } + + /** + * Walks back from the receiver to what last gave the shown sets their state. The changes crossed leave the shown + * sets as they were: a state refinement keeps the sets it does not name + */ + private Optional note(Predicate shownFound) throws LJError { + 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(); + at = before.get(); + } + } + + /** + * 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; + CtExecutable scope = invocation.getParent(CtExecutable.class); + 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 uses.stream().filter(use -> mayRunBefore(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(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() + .equals("liquidjava.specification.StateRefinement")); + } + + /** + * 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)) + if (use.hasParent(loop) && (exit == null || !exit.hasParent(loop))) + return true; + return false; + } + + /** 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); + // 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); + } + + /** + * 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, Set sets) { + return factsOn(shownFound, receiver.getName(), sets) + .map(f -> f.substituteVariable(receiver.getName(), at.getName())) + .or(() -> factsOn(shownFound, at.getName(), sets)); + } + + /** + * 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 { + 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(); + // 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()))); + } + + /** + * 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, VariableInstance assigned, Predicate shownFound) + throws LJError { + Optional code = code(call.position()); + if (code.isEmpty()) + return Optional.empty(); + 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(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 + 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) + && !hasAlias(returned.getExpression()); + String sets = shown.stream().map(set -> Utils.getSimpleName(set.getName()) + "(" + written + ")").sorted() + .collect(Collectors.joining(", ")); + return saysNothing ? Optional.of(origin + "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("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 + && constructor.getMetadata(Keys.STATE_CHANGE)instanceof StateChange created + && created.function().getAllStates().size() == 1 && !writtenAfterDeclaration(local) + && !changedByAnotherCall(local))) + return Optional.empty(); + 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()))) + return Optional.empty(); + // 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))); + } + + /** + * 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() + .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, 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() + && sets.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/TestFromNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java deleted file mode 100644 index 48c55373..00000000 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java +++ /dev/null @@ -1,31 +0,0 @@ -package liquidjava.api.tests; - -import static org.junit.jupiter.api.Assertions.*; - -import java.util.List; - -import org.junit.jupiter.api.Test; - -import liquidjava.api.CommandLineLauncher; -import liquidjava.diagnostics.Diagnostics; -import liquidjava.diagnostics.errors.LJError; - -class TestFromNotes { - - 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"), - error.getMessageNotes()); - assertTrue(error.toString().contains(error.getMessage() + "\n From: amount is a parameter")); - } - - private static LJError verify(String test) { - CommandLineLauncher.launch(TEST_SUITE + test); - List errors = Diagnostics.getInstance().getErrors().stream().toList(); - assertEquals(1, errors.size(), "Expected exactly one error from " + test); - return errors.get(0); - } -} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java new file mode 100644 index 00000000..4eaaf74b --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -0,0 +1,51 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; + +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("Origin: line 10, amount is a parameter of use(int) with no refinement"), + error.getMessageNotes()); + assertTrue(error.toString().contains(error.getMessage() + "\n Origin: line 10, amount is a parameter")); + } + + @Test + void stateIsTracedToTheCallThatLastSetTheSetThatIsWrong() { + assertEquals(List.of("Origin: line 27, d.lock() makes lockState(d) == locked"), + verify("ErrorStateHintMultipleSets.java").getMessageNotes()); + } + + @Test + void stateIsTracedToTheReturnRefinementOfTheCallAssigned() { + assertEquals(List.of("Origin: line 27, FromReturnedTask.create() returns phase(task) == idle"), + 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(); + assertEquals(1, errors.size(), "Expected exactly one error from " + test); + return errors.get(0); + } +}