From 797608f3dcb6381366ec9838903ccb7f58fb37ec Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 16:00:39 +0000 Subject: [PATCH 1/2] Show a counterexample for state errors, without state values A state refinement error now shows the values a model of what is known where the call fails gives the variables of the found the message shows. Values found already states, generated names and ghost or state values are left out, so A1_09 shows previousMode == BORDERLESS and an error about states alone shows none. Co-Authored-By: Claude Opus 5.5 --- .../diagnostics/errors/RefinementError.java | 2 +- .../errors/StateRefinementError.java | 27 +++++++++++++++++++ .../refinement_checker/TypeChecker.java | 16 ++++++++++- .../refinement_checker/VCChecker.java | 9 ++++--- .../api/tests/TestCounterexamples.java | 8 ++++++ 5 files changed, 57 insertions(+), 5 deletions(-) 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..a011d68d 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,19 @@ 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 */ + private Counterexample counterexample(Predicate found, Predicate expected, SourcePosition position) { + try { + 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(); From 8b74fa3b6e67b0d82598bbd52fe628d76422f422 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 16:11:30 +0000 Subject: [PATCH 2/2] Show no state counterexample when every value fails the call Co-Authored-By: Claude Opus 5.5 --- .../processor/refinement_checker/TypeChecker.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 a011d68d..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 @@ -626,9 +626,14 @@ public void throwStateRefinementError(SourcePosition position, SourcePosition de category, context, declarationNotes, counterexample(found, expected, position)); } - /** A model of what is known where {@code expected} fails, or null if the solver gives none */ + /** + * 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) {