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 00000000..1d11931d --- /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 00000000..498627a4 --- /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 00000000..7f53f6c3 --- /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 00000000..787b9287 --- /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 7ae8fbda..0554206d 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 625922ed..bb6834dc 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 06ae4244..ef9e1ba9 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 00000000..f201649c --- /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 b4bebb0c..3253fca0 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 c889d8e0..d88a4a45 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 95477a0e..089ef693 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 00000000..134cbb0d --- /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 0281058a..21c47717 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 d41b7c06..ce7f5d84 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 f444910a..04a4c12f 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 191b2931..8f5b4282 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(