diff --git a/liquidjava-example/src/main/java/testSuite/ErrorOutOfDomainArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorOutOfDomainArgument.java new file mode 100644 index 00000000..cff53c84 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorOutOfDomainArgument.java @@ -0,0 +1,12 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorOutOfDomainArgument { + + static void take(@Refinement("_ > 0") int amount) {} + + static void use() { + take(-1); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorPathDependentOtherStateSet.java b/liquidjava-example/src/main/java/testSuite/ErrorPathDependentOtherStateSet.java new file mode 100644 index 00000000..6c0987f2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorPathDependentOtherStateSet.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"closed", "opened"}) +@StateSet({"unlocked", "locked"}) +public class ErrorPathDependentOtherStateSet { + + @StateRefinement(to = "closed(this) && unlocked(this)") + public ErrorPathDependentOtherStateSet() {} + + @StateRefinement(from = "closed(this)", to = "opened(this)") + public void open() {} + + @StateRefinement(from = "unlocked(this)", to = "locked(this)") + public void lock() {} + + @StateRefinement(from = "opened(this)") + public void pass() {} + + // the states differ only in the lock, which pass() does not check, so the path is not what is wrong + public static void use(boolean secure) { + ErrorPathDependentOtherStateSet d = new ErrorPathDependentOtherStateSet(); + if (secure) + d.lock(); + d.pass(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOfAllStates.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOfAllStates.java new file mode 100644 index 00000000..15a503a2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintJoinOfAllStates.java @@ -0,0 +1,24 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"created", "open"}) +public class ErrorStateHintJoinOfAllStates { + + @StateRefinement(to = "created(this)") + public ErrorStateHintJoinOfAllStates() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + public static void use(boolean ready) { + ErrorStateHintJoinOfAllStates f = new ErrorStateHintJoinOfAllStates(); + if (ready) + f.open(); + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnprovableArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorUnprovableArgument.java new file mode 100644 index 00000000..bc6cf97d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnprovableArgument.java @@ -0,0 +1,13 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorUnprovableArgument { + + static void take(@Refinement("_ > 0") int amount) {} + + // nothing is known about amount, so its refinement can be neither violated nor proved + static void use(int amount) { + take(amount); // Expect: Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index eedc84ae..955db914 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -6,8 +6,10 @@ import java.util.Collections; import java.util.List; import java.util.Objects; +import java.util.Optional; import java.util.stream.Collectors; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; import spoon.reflect.cu.SourcePosition; @@ -21,6 +23,7 @@ public class LJDiagnostic extends RuntimeException { private SourcePosition position; private final List hints = new ArrayList<>(); private String counterexample; + private ErrorCategory category; private static final String PIPE = " | "; public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) { @@ -86,6 +89,14 @@ public void addHint(Hint hint) { hints.add(hint); } + public Optional getCategory() { + return Optional.ofNullable(category); + } + + public void setCategory(ErrorCategory category) { + this.category = category; + } + public void setCounterexampleStr(String counterexample) { this.counterexample = counterexample; } @@ -110,10 +121,11 @@ public String toString() { sb.append(" --> ").append(String.join("\n ", counterexample.split("\n"))).append("\n"); } - // hint - String hint = getHint(); - if (hint != null && !hint.isBlank()) { - sb.append(" --> ").append(String.join("\n ", hint.split("\n"))).append("\n"); + // hints + if (!hints.isEmpty()) { + sb.append("\nHints:\n"); + for (Hint hint : hints) + sb.append(" - ").append(String.join("\n ", hint.message().split("\n"))).append("\n"); } // location diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java new file mode 100644 index 00000000..7ae8fbda --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java @@ -0,0 +1,30 @@ +package liquidjava.diagnostics.categories; + +/** + * The kind of mistake an error shows, named after the categories of the LiquidJava bug codebook. A category describes + * the program according to its specification, so it cannot tell whether the specification itself is wrong. + */ +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"), + 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"); + + private final String id; + private final String title; + + ErrorCategory(String id, String title) { + this.id = id; + this.title = title; + } + + /** The id of the category in the codebook */ + public String id() { + return id; + } + + public String title() { + return title; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index e358b299..81b93eaf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -5,6 +5,7 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.TranslationTable; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; @@ -46,11 +47,19 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi .collect(Collectors.joining(" && ")); setCounterexampleStr("Counterexample: " + counterexampleString); } + setCategory(categoryOf(expected, found)); if (isTrue(found.getImplication().toPredicate().getExpression())) addHint(Hint.general( "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.")); } + /** Unprovable when what was found says nothing about the values the expected refinement constrains */ + private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) { + List foundVariables = found.getImplication().toPredicate().getVariableNames(); + boolean constrained = expected.getVariableNames().stream().anyMatch(foundVariables::contains); + return constrained ? ErrorCategory.OUT_OF_DOMAIN : ErrorCategory.UNPROVABLE; + } + @Override public SourcePosition getDeclarationPosition() { return declarationPosition; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index d034618b..27068ab8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -5,6 +5,7 @@ import java.util.List; import liquidjava.diagnostics.TranslationTable; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; @@ -23,7 +24,8 @@ public class StateRefinementError extends LJError { private final SourcePosition declarationPosition; public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, - VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints) { + VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints, + ErrorCategory category) { super("State Refinement Error", String.format("found %s but expected %s", found.getImplication().toPredicate().getExpression().toDisplayString(), @@ -33,6 +35,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP this.expected = expected; this.found = found; hints.forEach(this::addHint); + setCategory(category); if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression())) addHint(Hint.general( "No state information is known for this object. Make sure its state is initialized and available at this point.")); 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 a706e39d..06ae4244 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -10,6 +10,7 @@ import java.util.stream.Collectors; import java.util.stream.Stream; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint.Kind; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.Variable; @@ -20,8 +21,9 @@ import spoon.reflect.reference.CtTypeReference; /** - * Hints for a call made in a state that does not allow it, read from the class's {@link StateMachine}. Each hint only - * states what the machine proves, so a suggested sequence of calls always makes the failing call verify. + * Hints for a call made in a state that does not allow it, read from the class's {@link StateMachine}. The error's + * category decides which kinds of hints are given, and each hint only states what the machine proves, so a suggested + * sequence of calls always makes the failing call verify. */ public final class StateHints { @@ -44,8 +46,11 @@ private StateHints(StateMachine machine, String receiver) { * the states the receiver can be in before the call * @param receiver * the receiver as written in the code + * @param category + * the error's category, or {@code null} if it has none */ - public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver) { + public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver, + ErrorCategory category) { if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) return List.of(); // the machine cannot explain why the call failed Set goal = machine.statesAllowing(call); @@ -53,10 +58,11 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set return List.of(); StateHints hints = new StateHints(machine, receiver); - if (hints.isUnknown(current)) + if (category == ErrorCategory.UNPROVABLE) return hints.reachingCalls(call, goal); - return Stream.concat(hints.howToReach(current, call, goal).stream(), hints.allowedCalls(current).stream()) - .toList(); + boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; + return Stream.concat(hints.howToReach(current, call, goal, pathDependent).stream(), + hints.allowedCalls(current).stream()).toList(); } /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */ @@ -74,13 +80,13 @@ private List reachingCalls(RefinedFunction call, Set goal) { "The state of %s is unknown here. To get it to %s, use: %s", receiver, names(goal), list(ways)))); } - private List howToReach(Set current, RefinedFunction call, Set goal) { + private List howToReach(Set current, RefinedFunction call, Set goal, boolean pathDependent) { Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); if (search.isEmpty()) return List.of(); List> sequences = search.get(); if (sequences.isEmpty()) - return machine.complete() ? List.of(unreachable(current, call, goal)) : List.of(); + return machine.complete() ? List.of(unreachable(current, call, goal, pathDependent)) : List.of(); if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); return sequences.stream().map(sequence -> callSequence(current, sequence)).toList(); @@ -95,8 +101,8 @@ private Hint callSequence(Set current, List sequence) { receiver, names(current), names(reached))); } - private Hint unreachable(Set current, RefinedFunction call, Set goal) { - if (current.size() > 1) + private Hint unreachable(Set current, RefinedFunction call, Set goal, boolean pathDependent) { + if (pathDependent) return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( "%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. " + "Make %s reach this line in the same state on every path", @@ -125,11 +131,6 @@ private List allowedCalls(Set current) { return List.of(); } - /** Whether nothing is known about the state of the receiver */ - private boolean isUnknown(Set current) { - return current.size() == machine.states().size(); - } - private String call(RefinedFunction method) { return receiver + "." + signature(method); } 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 f0c51e18..c889d8e0 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 @@ -9,6 +9,7 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.*; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning; import liquidjava.processor.context.AliasWrapper; @@ -425,12 +426,13 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage) throws LJError { - throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of()); + throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null); } public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, - Predicate expected, String customMessage, List hints) throws LJError { - vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints); + Predicate expected, String customMessage, List hints, ErrorCategory category) throws LJError { + vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints, + category); } 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 cc5aebe8..a3bf1819 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 @@ -12,6 +12,7 @@ import liquidjava.diagnostics.errors.*; import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.TranslationTable; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; @@ -437,11 +438,12 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl } protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, - Predicate found, Predicate expected, String customMessage, List hints) throws StateRefinementError { + Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category) + throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map, - customMessage, hints); + customMessage, hints, category); } protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError { 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 69eb89ff..95477a0e 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 @@ -5,6 +5,7 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.DebugLog; +import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.errors.IllegalConstructorTransitionError; import liquidjava.diagnostics.errors.InvalidRefinementError; import liquidjava.diagnostics.errors.LJError; @@ -15,6 +16,7 @@ import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; import liquidjava.processor.state_machine.State; +import liquidjava.processor.state_machine.StateErrorCategories; import liquidjava.processor.state_machine.StateMachine; import liquidjava.processor.state_machine.StateMachineBuilder; import liquidjava.processor.state_machine.StateSolver; @@ -643,35 +645,48 @@ 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 hints = stateHints(tc, function, instanceName, prevState, 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()); tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState, - expectedStatesDisjunction, message, hints); + expectedStatesDisjunction, message, hints, category); } } + /** The state machine of the receiver's class and the states the receiver can be in before a call */ + private record ReceiverStates(StateMachine machine, Set current) { + } + /** - * Hints on how to fix a call to {@code function} made in a state that does not allow it. They are best effort: if - * they cannot be computed, the error is reported without them + * The receiver's states before a call to {@code function} that its state does not allow. Best effort: if they + * cannot be computed, the error is reported without hints or category */ - private static List stateHints(TypeChecker tc, RefinedFunction function, String instanceName, Predicate state, - CtElement invocation) { - Optional receiver = receiverOf(invocation); - if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) - return List.of(); + private static Optional receiverStates(TypeChecker tc, RefinedFunction function, + String instanceName, Predicate state, CtElement invocation) { try { Optional machine = tc.getStateMachine(function.getTargetClass(), invocation); if (machine.isEmpty()) - return List.of(); + return Optional.empty(); Set current = new StateSolver(tc, invocation.getPosition()).possibleStates(machine.get().states(), state, instanceName); - return StateHints.forCall(machine.get(), function, current, receiver.get()); + return Optional.of(new ReceiverStates(machine.get(), current)); } catch (RuntimeException e) { - // a failure to compute hints must not replace the error being reported - DebugLog.warn("Could not compute state hints: " + e.getMessage()); - return List.of(); + // a failure to analyse the states must not replace the error being reported + DebugLog.warn("Could not compute the receiver's states: " + 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) { + Optional receiver = receiverOf(invocation); + if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) + return List.of(); + return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category); + } + /** * The receiver of {@code invocation} as written in the code, if it names an object that calls can be added to: a * variable, a field or {@code this} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java new file mode 100644 index 00000000..4a2c08e8 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateErrorCategories.java @@ -0,0 +1,43 @@ +package liquidjava.processor.state_machine; + +import java.util.List; +import java.util.Optional; +import java.util.Set; + +import liquidjava.diagnostics.categories.ErrorCategory; +import liquidjava.processor.context.GhostState; +import liquidjava.rj_language.Predicate; + +/** + * The {@link ErrorCategory} of a call made in a state that does not allow it + */ +public final class StateErrorCategories { + + private StateErrorCategories() { + } + + /** + * @param current + * the states the receiver can be in before the call + * @param found + * what is known about the receiver before the call + * @param ghostStates + * the ghost states of the receiver's class + * + * @return the category, or nothing if it cannot be decided + */ + public static Optional categorize(StateMachine machine, Set current, Predicate found, + List ghostStates) { + List states = ghostStates.stream().filter(g -> g.getParent() != null).toList(); + // all states are possible and none is mentioned: nothing is known, which differs from a join of every state + if (current.size() == machine.states().size() && found.getStateInvocations(states).isEmpty()) + return Optional.of(ErrorCategory.UNPROVABLE); + if (current.size() == 1) + return Optional.of(ErrorCategory.OUT_OF_ORDER); + // with several state sets, the states may differ only in a set the call does not check + boolean oneStateSet = states.stream().map(GhostState::getParent).distinct().count() == 1; + if (current.size() > 1 && oneStateSet) + return Optional.of(ErrorCategory.PATH_DEPENDENT_STATE); + return Optional.empty(); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java new file mode 100644 index 00000000..f444910a --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestErrorCategories.java @@ -0,0 +1,79 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; +import java.util.Optional; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.categories.ErrorCategory; +import liquidjava.diagnostics.errors.LJError; + +class TestErrorCategories { + + private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; + + @Test + void callInTheWrongSingleStateIsOutOfOrder() { + assertCategory("ErrorStateHintCallSequence.java", ErrorCategory.OUT_OF_ORDER); + } + + @Test + void stateCombiningSeveralStateSetsIsOutOfOrder() { + assertCategory("ErrorStateHintMultipleSets.java", ErrorCategory.OUT_OF_ORDER); + } + + @Test + void stateDependingOnTheBranchIsPathDependent() { + assertCategory("ErrorStateHintPathDependent.java", ErrorCategory.PATH_DEPENDENT_STATE); + assertCategory("ErrorStateHintJoinOfAllStates.java", ErrorCategory.PATH_DEPENDENT_STATE); + } + + @Test + void statesDifferingInAnotherStateSetGetNoCategory() { + assertNoCategory("ErrorPathDependentOtherStateSet.java"); + } + + @Test + void unknownStateIsUnprovable() { + assertCategory("ErrorStateHintUnknownState.java", ErrorCategory.UNPROVABLE); + } + + @Test + void stateErrorWithoutStateSetGetsNoCategory() { + assertNoCategory("ErrorUnconstrainedStateRefinement.java"); + } + + @Test + void argumentOutsideItsRefinementIsOutOfDomain() { + assertCategory("ErrorOutOfDomainArgument.java", ErrorCategory.OUT_OF_DOMAIN); + } + + @Test + void returnValueOutsideItsRefinementIsOutOfDomain() { + assertCategory("ErrorIntegerDivision.java", ErrorCategory.OUT_OF_DOMAIN); + } + + @Test + void argumentWithNothingKnownIsUnprovable() { + assertCategory("ErrorUnprovableArgument.java", ErrorCategory.UNPROVABLE); + } + + private static void assertCategory(String test, ErrorCategory expected) { + assertEquals(Optional.of(expected), verify(test).getCategory()); + } + + private static void assertNoCategory(String test) { + assertEquals(Optional.empty(), verify(test).getCategory()); + } + + 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/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 0521fbfd..191b2931 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -65,6 +65,13 @@ void stateDependingOnThePathAsksForTheSameStateOnEveryPath() { + "Make f reach this line in the same state on every path")); } + @Test + void stateDependingOnThePathInEveryStateIsNotReportedAsUnknown() { + assertHints("ErrorStateHintJoinOfAllStates.java", new Hint(Kind.PATH_DEPENDENT_STATE, + "f can be in created or open here, depending on the path taken, and no sequence of calls moves all of them to open. " + + "Make f reach this line in the same state on every path")); + } + @Test void callAllowedByDifferentRefinementsInEachStateIsNotSuggested() { assertHints("ErrorStateHintSeveralRefinements.java", new Hint(Kind.PATH_DEPENDENT_STATE, diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/LJDiagnosticTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/LJDiagnosticTest.java index 86d70218..3969cbae 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/LJDiagnosticTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/LJDiagnosticTest.java @@ -24,4 +24,12 @@ void hintsKeepTheirOrderAndAreJoinedOnePerLine() { assertEquals(List.of(Hint.general("first"), Hint.general("second")), error.getHints()); assertEquals("first\nsecond", error.getHint()); } + + @Test + void hintsArePrintedInTheirOwnSection() { + CustomError error = new CustomError("message", null); + error.addHint(Hint.general("first")); + error.addHint(Hint.general("second")); + assertTrue(error.toString().endsWith("\nHints:\n - first\n - second\n")); + } }