Show a counterexample for state errors, restricted to the shown Found

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<String, String> assignment, List<Expression> facts) {
+    static boolean isKnown(Pair<String, String> assignment, List<Expression> facts) {
         return facts.stream()
                 .anyMatch(fact -> fact instanceof BinaryExpression binary && "==".equals(binary.getOperator())
                         && (states(binary.getFirstOperand(), binary.getSecondOperand(), assignment)

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<String> variables = new ArrayList<>();
+        shown.getVariableNames(variables);
+        List<Expression> 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) {

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<Hint> hints, ErrorCategory category,
             StateErrorContext context, List<String> 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 {

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<Hint> hints, ErrorCategory category,
-            StateErrorContext context, List<String> declarationNotes) throws StateRefinementError {
+            StateErrorContext context, List<String> 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 */

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<LJError> 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<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();