From c63ff7878f0a36054169a03287bec9a48681725d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 24 Oct 2026 13:05:17 +0100 Subject: [PATCH] Point out the argument that decided a state a call does not allow Each object now remembers the last call that changed its state, through constructors and state-preserving calls. When a call fails, the verifier follows that chain back to the last call that changed a state set the failing call checks. If that call's transition depends on its arguments or result, and the SMT solver finds values for which the failing call would have been allowed, the error gets the "Argument picks the state" category and a hint with those values. Co-Authored-By: Claude Opus 5.5 --- .../ErrorArgumentCannotPickTheState.java | 24 ++++ .../testSuite/ErrorArgumentPicksTheState.java | 23 ++++ .../ErrorArgumentPicksTheStateEarlier.java | 29 ++++ ...ErrorConstructorArgumentPicksTheState.java | 19 +++ .../diagnostics/categories/ErrorCategory.java | 1 + .../liquidjava/diagnostics/hints/Hint.java | 2 + .../diagnostics/hints/StateHints.java | 14 ++ .../processor/context/StateChange.java | 25 ++++ .../processor/context/VariableInstance.java | 10 ++ .../refinement_checker/TypeChecker.java | 10 +- .../object_checkers/AuxStateHandler.java | 37 ++++- .../state_machine/DecidingArgument.java | 127 ++++++++++++++++++ .../processor/state_machine/StateSolver.java | 9 ++ .../java/liquidjava/utils/constants/Keys.java | 1 + .../api/tests/TestErrorCategories.java | 12 ++ .../liquidjava/api/tests/TestStateHints.java | 12 ++ 16 files changed, 346 insertions(+), 9 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArgumentCannotPickTheState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheStateEarlier.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorConstructorArgumentPicksTheState.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/context/StateChange.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArgumentCannotPickTheState.java b/liquidjava-example/src/main/java/testSuite/ErrorArgumentCannotPickTheState.java new file mode 100644 index 000000000..1d11931d7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorArgumentCannotPickTheState.java @@ -0,0 +1,24 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"empty", "filled", "closed"}) +public class ErrorArgumentCannotPickTheState { + + @StateRefinement(to = "empty(this)") + public ErrorArgumentCannotPickTheState() {} + + @StateRefinement(from = "!closed(this)", to = "keep ? filled(this) : empty(this)") + public void reset(boolean keep) {} + + @StateRefinement(from = "closed(this)") + public void reopen() {} + + // no value of keep closes the object, so the argument is not what went wrong + public static void use() { + ErrorArgumentCannotPickTheState buffer = new ErrorArgumentCannotPickTheState(); + buffer.reset(true); + buffer.reopen(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheState.java b/liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheState.java new file mode 100644 index 000000000..498627a4b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheState.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"empty", "filled", "closed"}) +public class ErrorArgumentPicksTheState { + + @StateRefinement(to = "empty(this)") + public ErrorArgumentPicksTheState() {} + + @StateRefinement(from = "!closed(this)", to = "keep ? filled(this) : empty(this)") + public void reset(boolean keep) {} + + @StateRefinement(from = "filled(this)") + public void read() {} + + public static void use() { + ErrorArgumentPicksTheState buffer = new ErrorArgumentPicksTheState(); + buffer.reset(false); + buffer.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheStateEarlier.java b/liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheStateEarlier.java new file mode 100644 index 000000000..7f53f6c3d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheStateEarlier.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"tilingOff", "tilingOn"}) +@StateSet({"uncompressed", "compressed"}) +public class ErrorArgumentPicksTheStateEarlier { + + @StateRefinement(to = "tilingOff(this) && uncompressed(this)") + public ErrorArgumentPicksTheStateEarlier() {} + + @StateRefinement(to = "mode == 2 ? tilingOn(this) : tilingOff(this)") + public void setTilingMode(int mode) {} + + @StateRefinement(from = "uncompressed(this)", to = "compressed(this)") + public void compress() {} + + @StateRefinement(from = "tilingOn(this)") + public void setTiling() {} + + // compress() changes another state set, so the tiling mode is what decided the state + public static void use() { + ErrorArgumentPicksTheStateEarlier param = new ErrorArgumentPicksTheStateEarlier(); + param.setTilingMode(1); + param.compress(); + param.setTiling(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorConstructorArgumentPicksTheState.java b/liquidjava-example/src/main/java/testSuite/ErrorConstructorArgumentPicksTheState.java new file mode 100644 index 000000000..787b9287f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorConstructorArgumentPicksTheState.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"readOnly", "writable"}) +public class ErrorConstructorArgumentPicksTheState { + + @StateRefinement(to = "write ? writable(this) : readOnly(this)") + public ErrorConstructorArgumentPicksTheState(boolean write) {} + + @StateRefinement(from = "writable(this)") + public void append() {} + + public static void use() { + ErrorConstructorArgumentPicksTheState file = new ErrorConstructorArgumentPicksTheState(false); + file.append(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java index 7ae8fbdad..0554206d6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java @@ -8,6 +8,7 @@ public enum ErrorCategory { OUT_OF_ORDER("A1", "Out of order: the operation is legal for this object, but not right now"), OUT_OF_DOMAIN("A2", "Out of domain: the value is outside what is accepted"), + ARGUMENT_PICKS_THE_STATE("C3.1", "Argument picks the state: the value passed decides where the object lands"), PATH_DEPENDENT_STATE("C4.1", "Path-dependent state: the state differs depending on which branch ran"), UNPROVABLE("C4.2", "Unprovable: nothing is known that could prove the requirement"); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index 625922edf..bb6834dca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -13,6 +13,8 @@ public record Hint(Kind kind, String message) { public enum Kind { /** A suggestion that does not come from a specific analysis */ GENERAL, + /** An earlier call whose arguments decided the state, and values that would allow the failing call */ + DECIDING_ARGUMENT, /** Calls to add before the failing call so the object reaches a state that allows it */ CALL_SEQUENCE, /** The calls allowed in the object's current state */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 06ae42443..ef9e1ba96 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -14,10 +14,12 @@ import liquidjava.diagnostics.hints.Hint.Kind; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.Variable; +import liquidjava.processor.state_machine.DecidingArgument; import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; import liquidjava.processor.state_machine.Transition; import liquidjava.utils.Utils; +import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtTypeReference; /** @@ -65,6 +67,18 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set hints.allowedCalls(current).stream()).toList(); } + /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */ + public static Hint decidingArgument(DecidingArgument deciding, String receiver) { + RefinedFunction function = deciding.call().function(); + String call = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName()) ? constructor(function) + : receiver + "." + signature(function); + String values = deciding.values().isEmpty() ? "other arguments" : deciding.values().entrySet().stream() + .map(e -> e.getKey() + " == " + e.getValue()).collect(Collectors.joining(" and ")); + return new Hint(Kind.DECIDING_ARGUMENT, + String.format("%s on line %d decides the state of %s: with %s, this call would be allowed", call, + deciding.call().position().getLine(), receiver, values)); + } + /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */ private List reachingCalls(RefinedFunction call, Set goal) { Map> sources = new LinkedHashMap<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/StateChange.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/StateChange.java new file mode 100644 index 000000000..f201649c4 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/StateChange.java @@ -0,0 +1,25 @@ +package liquidjava.processor.context; + +import java.util.Optional; + +import spoon.reflect.cu.SourcePosition; + +/** + * The call that put an object in its current state + * + * @param function + * the method or constructor called + * @param change + * the state refinement of {@code function} that applied + * @param before + * the object before the call, or {@code null} for a constructor + * @param position + * where the call is + */ +public record StateChange(RefinedFunction function, ObjectState change, VariableInstance before, + SourcePosition position) { + + public Optional previous() { + return Optional.ofNullable(before); + } +} 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 b4bebb0c1..3253fca05 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java @@ -7,6 +7,7 @@ public class VariableInstance extends RefinedVariable { private Variable parent; + private StateChange stateChange; public VariableInstance(String name, CtTypeReference type, Predicate c) { super(name, type, c); @@ -33,6 +34,15 @@ public void setParent(Variable p) { parent = p; } + /** The last call that changed the state of this object, if it is known */ + public Optional getStateChange() { + return Optional.ofNullable(stateChange); + } + + public void setStateChange(StateChange stateChange) { + this.stateChange = stateChange; + } + public Optional getParent() { return parent == null ? Optional.empty() : Optional.of(parent); } 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 c889d8e07..d88a4a455 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 @@ -414,9 +414,13 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent) throws LJError { - SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, - factory, silent); - return result.isOk(); + return verifyStateSMT(prevState, expectedState, p, silent).isOk(); + } + + /** Checks that {@code prevState} implies {@code expectedState}, with a counterexample when it does not */ + public SMTResult verifyStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent) + throws LJError { + return vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, factory, silent); } public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, 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 95477a0ed..089ef693b 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 @@ -15,6 +15,7 @@ import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; +import liquidjava.processor.state_machine.DecidingArgument; import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateErrorCategories; import liquidjava.processor.state_machine.StateMachine; @@ -420,6 +421,8 @@ public static void constructorStateMetadata(String refKey, RefinedFunction f, Ma c = c.substituteVariable(k, map.get(k)); } ctConstructorCall.putMetadata(refKey, c); + ctConstructorCall.putMetadata(Keys.STATE_CHANGE, + new StateChange(f, f.getAllStates().get(0), null, ctConstructorCall.getPosition())); // add mapping to oc.get(0)-HERE } } @@ -439,6 +442,8 @@ public static void addStateRefinements(TypeChecker tc, String varName, CtExpress Predicate c = (Predicate) e.getMetadata(Keys.REFINEMENT); c = c.substituteVariable(Keys.THIS, vi.getName()).substituteVariable(Keys.WILDCARD, vi.getName()); vi.setRefinement(c); + if (e.getMetadata(Keys.STATE_CHANGE)instanceof StateChange change) + vi.setStateChange(change); } } @@ -626,7 +631,8 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc } transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName); // update of state of new instance of this#n#(whatever it was + 1) - addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation); + addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation) + .setStateChange(new StateChange(function, stateChange, vi, invocation.getPosition())); } } if (!found) { // Reaches the end of stateChange no matching states @@ -645,10 +651,16 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc SourcePosition declarationPosition = stateChanges.stream().filter(ObjectState::hasFrom) .map(ObjectState::getFromPosition).filter(Objects::nonNull).findFirst() .orElse(function.getPlacementInCode().getPosition()); + List ghostStates = getGhostStatesFor(function.getTargetClass(), tc); + Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, instanceName, prevState, invocation); - ErrorCategory category = states.flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(), - prevState, getGhostStatesFor(function.getTargetClass(), tc))).orElse(null); - List hints = states.map(r -> stateHints(r, function, category, invocation)).orElse(List.of()); + ErrorCategory category = deciding.isPresent() ? ErrorCategory.ARGUMENT_PICKS_THE_STATE + : states.flatMap( + r -> StateErrorCategories.categorize(r.machine(), r.current(), prevState, ghostStates)) + .orElse(null); + List hints = deciding.isPresent() + ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() + : states.map(r -> stateHints(r, function, category, invocation)).orElse(List.of()); tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState, expectedStatesDisjunction, message, hints, category); } @@ -678,6 +690,17 @@ private static Optional receiverStates(TypeChecker tc, RefinedFu } } + /** Best effort, like {@link #receiverStates} */ + private static Optional decidingArgument(TypeChecker tc, VariableInstance receiver, + RefinedFunction function, List ghostStates, CtElement invocation) { + try { + return DecidingArgument.find(tc, receiver, function, ghostStates, invocation); + } catch (RuntimeException e) { + DebugLog.warn("Could not find the argument that decided the receiver's state: " + e.getMessage()); + return Optional.empty(); + } + } + /** Hints on how to fix a call to {@code function} made in a state that does not allow it */ private static List stateHints(ReceiverStates states, RefinedFunction function, ErrorCategory category, CtElement invocation) { @@ -722,7 +745,8 @@ 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); + addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation) + .setStateChange(variableInstance.getStateChange().orElse(null)); } } @@ -736,7 +760,7 @@ private static void sameState(TypeChecker tc, VariableInstance variableInstance, * @param transitionedState * @param invocation */ - private static void addInstanceWithState(TypeChecker tc, String superName, String name2, + private static VariableInstance addInstanceWithState(TypeChecker tc, String superName, String name2, VariableInstance prevInstance, Predicate transitionedState, CtElement invocation) throws LJError { VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(name2, prevInstance.getType(), prevInstance.getRefinement(), invocation); @@ -758,6 +782,7 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin } } invocation.putMetadata(Keys.TARGET, vi2); + return vi2; } /** Whether the access denotes the receiver of the enclosing type, including unqualified super. */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java new file mode 100644 index 000000000..134cbb0d8 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java @@ -0,0 +1,127 @@ +package liquidjava.processor.state_machine; + +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + +import liquidjava.diagnostics.errors.LJError; +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.Variable; +import liquidjava.processor.context.VariableInstance; +import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.rj_language.Predicate; +import liquidjava.smt.Counterexample; +import liquidjava.utils.Pair; +import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Types; +import spoon.reflect.declaration.CtElement; +import spoon.reflect.reference.CtTypeReference; + +/** + * An earlier call whose arguments decided the state that a failing call does not allow, with argument values for which + * the failing call would have been allowed + * + * @param call + * the deciding call + * @param values + * the values, by parameter name ({@code return} for the call's result) + */ +public record DecidingArgument(StateChange call, Map values) { + + // the object after the deciding call, and its result, under names nothing else uses + private static final String OBJECT = "#decided"; + private static final String RESULT = "return"; + + /** + * @param receiver + * the receiver of the failing call + * @param failing + * the method that cannot be called + * @param ghostStates + * the ghost states of the receiver's class + * @param invocation + * the failing call + */ + public static Optional find(TypeChecker tc, VariableInstance receiver, RefinedFunction failing, + List ghostStates, CtElement invocation) throws LJError { + List required = failing.getFromStates(); + if (!required.stream().allMatch(DecidingArgument::mentionsOnlyThis)) + return Optional.empty(); + List states = ghostStates.stream().filter(g -> g.getParent() != null).toList(); + Set checked = required.stream().flatMap(p -> p.getStateInvocations(states).stream()) + .map(GhostState::getParent).collect(Collectors.toSet()); + + // the last call that changed a state set the failing call checks; a join of branches breaks the chain + Optional call = receiver.getStateChange(); + while (call.isPresent() && !changes(call.get(), checked, states)) + call = call.get().previous().flatMap(VariableInstance::getStateChange); + if (call.isEmpty() || dependsOnlyOnState(call.get())) + return Optional.empty(); + StateChange deciding = call.get(); + return valuesAllowing(tc, deciding, receiver, required, invocation) + .map(values -> new DecidingArgument(deciding, values)); + } + + private static boolean changes(StateChange call, Set stateSets, List states) { + return call.change().getTo().getStateInvocations(states).stream().map(GhostState::getParent) + .anyMatch(stateSets::contains); + } + + private static boolean dependsOnlyOnState(StateChange call) { + return mentionsOnlyThis(call.change().getFrom()) && mentionsOnlyThis(call.change().getTo()); + } + + private static boolean mentionsOnlyThis(Predicate predicate) { + return predicate.getVariableNames().stream().allMatch(Keys.THIS::equals); + } + + /** Values of the deciding call's parameters and result after which one of {@code required} would hold */ + private static Optional> valuesAllowing(TypeChecker tc, StateChange call, + VariableInstance receiver, List required, CtElement invocation) throws LJError { + Context context = tc.getContext(); + context.enterContext(); + try { + context.addVarToContext(OBJECT, receiver.getType(), new Predicate(), invocation); + Predicate to = call.change().getTo().substituteVariable(Keys.THIS, OBJECT); + if (call.previous().isPresent()) + to = to.changeOldMentions(call.previous().get().getName(), OBJECT); + + Map free = new LinkedHashMap<>(); // fresh name -> name shown + RefinedFunction function = call.function(); + for (Variable parameter : function.getArguments()) + to = leaveFree(context, to, parameter.getName(), parameter.getType(), parameter.getName(), free, + invocation); + boolean returnsValue = function.getType() != null && !"void".equals(function.getType().toString()); + to = returnsValue ? leaveFree(context, to, Keys.WILDCARD, function.getType(), RESULT, free, invocation) + : to.substituteVariable(Keys.WILDCARD, OBJECT); + + Predicate before = call.previous().map(VariableInstance::getRefinement).orElse(new Predicate()); + Predicate allowed = required.stream().map(p -> p.substituteVariable(Keys.THIS, OBJECT)) + .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction); + Optional witness = new StateSolver(tc, invocation.getPosition()) + .witness(Predicate.createConjunction(before, to), allowed); + return witness.map(model -> model.assignments().stream().filter(a -> free.containsKey(a.first())).collect( + Collectors.toMap(a -> free.get(a.first()), Pair::second, (a, b) -> a, LinkedHashMap::new))); + } finally { + context.exitContext(); + } + } + + /** Renames {@code name} in {@code predicate} to a fresh variable with no refinement, if it is mentioned */ + private static Predicate leaveFree(Context context, Predicate predicate, String name, CtTypeReference type, + String shownAs, Map free, CtElement invocation) { + if (!predicate.getVariableNames().contains(name)) + return predicate; + String fresh = "#" + shownAs; + context.addVarToContext(fresh, type, new Predicate(), invocation); + free.put(fresh, shownAs); + return predicate.substituteVariable(name, fresh); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java index 0281058a1..21c477177 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java @@ -2,11 +2,14 @@ import java.util.LinkedHashSet; import java.util.List; +import java.util.Optional; import java.util.Set; import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.rj_language.Predicate; +import liquidjava.smt.Counterexample; +import liquidjava.smt.SMTResult; import liquidjava.utils.constants.Keys; import spoon.reflect.cu.SourcePosition; @@ -32,6 +35,12 @@ public boolean implies(Predicate premise, Predicate conclusion) throws LJError { return tc.checkStateSMT(premise, conclusion, position, true); } + /** Values for which {@code first} and {@code second} hold at the same time, if there are any */ + public Optional witness(Predicate first, Predicate second) throws LJError { + SMTResult result = tc.verifyStateSMT(first, second.negate(), position, true); + return result.isOk() ? Optional.empty() : Optional.of(result.getCounterexample()); + } + /** Whether {@code first} and {@code second} can hold at the same time */ public boolean compatible(Predicate first, Predicate second) throws LJError { return !implies(first, second.negate()); 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 d41b7c068..ce7f5d848 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -6,6 +6,7 @@ public final class Keys { public static final String TARGET = "target"; 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 THIS = "this"; public static final String WILDCARD = "_"; public static final String OLD = "old"; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java index f444910ac..04a4c12ff 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java @@ -26,6 +26,18 @@ void stateCombiningSeveralStateSetsIsOutOfOrder() { assertCategory("ErrorStateHintMultipleSets.java", ErrorCategory.OUT_OF_ORDER); } + @Test + void stateDecidedByAnArgumentIsArgumentPicksTheState() { + assertCategory("ErrorArgumentPicksTheState.java", ErrorCategory.ARGUMENT_PICKS_THE_STATE); + assertCategory("ErrorConstructorArgumentPicksTheState.java", ErrorCategory.ARGUMENT_PICKS_THE_STATE); + assertCategory("ErrorArgumentPicksTheStateEarlier.java", ErrorCategory.ARGUMENT_PICKS_THE_STATE); + } + + @Test + void argumentThatCannotAllowTheCallIsOutOfOrder() { + assertCategory("ErrorArgumentCannotPickTheState.java", ErrorCategory.OUT_OF_ORDER); + } + @Test void stateDependingOnTheBranchIsPathDependent() { assertCategory("ErrorStateHintPathDependent.java", ErrorCategory.PATH_DEPENDENT_STATE); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 191b29318..8f5b42829 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -90,6 +90,18 @@ void unknownStateListsTheCallsThatLeadToTheExpectedState() { "The state of f is unknown here. To get it to open, use: f.open() (from created)")); } + @Test + void argumentThatDecidedTheStateIsShownWithAValueThatWouldWork() { + assertHints("ErrorArgumentPicksTheState.java", new Hint(Kind.DECIDING_ARGUMENT, + "buffer.reset(boolean) on line 20 decides the state of buffer: with keep == true, this call would be allowed")); + } + + @Test + void deciderIsTheLastCallThatChangedTheCheckedStateSet() { + assertHints("ErrorArgumentPicksTheStateEarlier.java", new Hint(Kind.DECIDING_ARGUMENT, + "param.setTilingMode(int) on line 25 decides the state of param: with mode == 2, this call would be allowed")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general(