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 775c740b..0c3aa855 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -154,7 +154,7 @@ private Counterexample filterCounterexample(Counterexample counterexample) { } // Whether a fact of found is term == value, which the counterexample would only repeat - private static boolean isKnown(Pair assignment, List facts) { + static boolean isKnown(Pair assignment, List facts) { return facts.stream() .anyMatch(fact -> fact instanceof BinaryExpression binary && "==".equals(binary.getOperator()) && (states(binary.getFirstOperand(), binary.getSecondOperand(), assignment) 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 139ebba9..9877ef6b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -1,9 +1,13 @@ package liquidjava.diagnostics.errors; +import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected; +import java.util.ArrayList; import java.util.List; import java.util.function.UnaryOperator; +import java.util.stream.Collectors; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.categories.ErrorCategory; @@ -13,6 +17,8 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.opt.VCSimplificationResult; +import liquidjava.smt.Counterexample; +import liquidjava.utils.GeneratedNames; import spoon.reflect.cu.SourcePosition; /** @@ -54,6 +60,27 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP "No state information is known for this object. Make sure its state is initialized and available at this point.")); } + /** + * Shows the values the counterexample gives the variables of the found the message shows, but those found already + * states. A ghost or state value is never shown: a state is an unconstrained number, and the message already says + * which state each object is in + */ + public void showCounterexample(Counterexample counterexample) { + Expression foundExpression = found.getImplication().toPredicate().getExpression(); + Expression shown = linkedToExpected(foundExpression, expected.getExpression()); + if (counterexample == null || !appliesGhost(shown)) + return; + List variables = new ArrayList<>(); + shown.getVariableNames(variables); + List facts = factsOf(foundExpression); + String values = counterexample.assignments().stream() + .filter(a -> variables.contains(a.first()) && !GeneratedNames.isGenerated(a.first())) + .filter(a -> !RefinementError.isKnown(a, facts) && !a.second().contains("!val!")) + .map(a -> getDisplayNames().get(a.first()) + " == " + a.second()).collect(Collectors.joining(" && ")); + if (!values.isEmpty()) + setCounterexampleStr("Counterexample: " + values); + } + // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a // guard on another value says nothing about the state expected needs private static boolean appliesGhost(Expression expression) { 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 44af4d58..86c02e33 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 @@ -31,6 +31,8 @@ import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.diagnostics.DebugLog; +import liquidjava.smt.Counterexample; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; @@ -621,7 +623,24 @@ public void throwStateRefinementError(SourcePosition position, SourcePosition de Predicate expected, String customMessage, List hints, ErrorCategory category, StateErrorContext context, List declarationNotes) throws LJError { vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints, - category, context, declarationNotes); + category, context, declarationNotes, counterexample(found, expected, position)); + } + + /** + * A model of what is known where {@code expected} fails, or null if the solver gives none or {@code expected} fails + * whatever the values: then no value tells why it fails + */ + private Counterexample counterexample(Predicate found, Predicate expected, SourcePosition position) { + try { + if (verifyStateSMT(found, expected.negate(), position, true).isOk()) + return null; + SMTResult result = verifyStateSMT(found, expected, position, true); + return result.isError() ? result.getCounterexample() : null; + } catch (RuntimeException e) { + // a failure to find a model must not replace the error being reported + DebugLog.warn("Could not find a counterexample for the state error: " + e.getMessage()); + return null; + } } 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 84d285e4..ab5f5270 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 @@ -457,16 +457,19 @@ protected Predicate shownFound(Predicate found, Predicate expected) { protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context, List declarationNotes) throws StateRefinementError { + StateErrorContext context, List declarationNotes, Counterexample counterexample) + 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, declarationPosition, expected, shown, map, customMessage, hints, - category, context, + StateRefinementError error = new StateRefinementError(position, declarationPosition, expected, shown, map, + customMessage, hints, category, context, e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()), declarationNotes); + error.showCounterexample(counterexample); + 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/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 59bc0501..01c96d11 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -234,6 +234,14 @@ void indexIntoLocalArrayShowsTheIndexAndNotTheArray() { assertAssignments(error, assignment("k", "-1")); } + @Test + void stateErrorShowsTheValueThatPicksTheFailingBranchButNoStateValue() { + CommandLineLauncher.launch(TEST_SUITE + "ErrorStateHintPathDependent.java"); + List errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size()); + assertEquals("Counterexample: ready == false", errors.get(0).getCounterexampleStr()); + } + private static RefinementError verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList();