Show counterexample values in the final expected refinement

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -1,14 +1,19 @@
 package liquidjava.diagnostics.errors;
 
+import java.util.ArrayList;
 import java.util.List;
 import java.util.Set;
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.LiteralString;
+import liquidjava.rj_language.ast.UnaryExpression;
+import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
+import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.smt.Counterexample;
 import liquidjava.utils.Pair;
 import spoon.reflect.cu.SourcePosition;
@@ -23,27 +28,49 @@
 public class RefinementError extends LJError {
 
     private final Predicate expected;
+    private final Predicate finalExpected;
+    private final Predicate expectedWithWitness;
     private final VCSimplificationResult found;
     private final Counterexample counterexample;
     private final SourcePosition declarationPosition;
 
     public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
             String customMessage) {
+        this(position, declarationPosition, expected, null, found, translationTable, counterexample, customMessage);
+    }
+
+    public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
+            Predicate finalExpected, VCSimplificationResult found, TranslationTable translationTable,
+            Counterexample counterexample, String customMessage) {
         super("Refinement Error",
                 String.format("%s is not a subtype of %s",
                         found.getImplication().toPredicate().getExpression().toDisplayString(),
                         expected.getExpression().toDisplayString()),
                 position, translationTable, customMessage);
         this.expected = expected;
+        this.finalExpected = finalExpected;
         this.found = found;
         this.counterexample = filterCounterexample(counterexample);
+        this.expectedWithWitness = substituteWitness(finalExpected, this.counterexample);
         this.declarationPosition = declarationPosition;
         if (!this.counterexample.isEmpty()) {
             String counterexampleString = this.counterexample.assignments().stream()
                     .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
                     .collect(Collectors.joining(" && "));
-            setCounterexampleStr("Counterexample: " + counterexampleString);
+            StringBuilder detail = new StringBuilder();
+            if (finalExpected != null) {
+                detail.append("Final expected: ").append(finalExpected.getExpression().toDisplayString()).append("\n");
+            }
+            detail.append("Counterexample: ").append(counterexampleString);
+            if (expectedWithWitness != null) {
+                detail.append("\nWith witness: ").append(expectedWithWitness.getExpression().toDisplayString());
+                List<String> remainingVariables = new ArrayList<>();
+                expectedWithWitness.getExpression().getVariableNames(remainingVariables);
+                if (remainingVariables.isEmpty())
+                    detail.append(" ✗");
+            }
+            setCounterexampleStr(detail.toString());
         }
         if (isTrue(found.getImplication().toPredicate().getExpression()))
             setHint("Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.");
@@ -62,10 +89,48 @@ public Predicate getExpected() {
         return expected;
     }
 
+    public Predicate getFinalExpected() {
+        return finalExpected;
+    }
+
+    public Predicate getExpectedWithWitness() {
+        return expectedWithWitness;
+    }
+
     public VCSimplificationResult getFound() {
         return found;
     }
 
+    private static Predicate substituteWitness(Predicate finalExpected, Counterexample counterexample) {
+        if (finalExpected == null || counterexample.isEmpty())
+            return null;
+        Expression expression = finalExpected.getExpression().clone();
+        boolean substituted = false;
+        for (Pair<String, String> assignment : counterexample.assignments()) {
+            List<String> variableNames = new ArrayList<>();
+            expression.getVariableNames(variableNames);
+            if (!variableNames.contains(assignment.first()))
+                continue;
+            try {
+                Expression value = RefinementsParser.createAST(assignment.second(), "");
+                if (!isLiteralValue(value))
+                    continue;
+                expression = expression.substitute(new Var(assignment.first()), value);
+                substituted = true;
+            } catch (SyntaxError ignored) {
+                // Some SMT values cannot be represented in the refinement language.
+            }
+        }
+        return substituted ? new Predicate(expression) : null;
+    }
+
+    private static boolean isLiteralValue(Expression value) {
+        if (value.isLiteral() || value instanceof LiteralString)
+            return true;
+        return value instanceof UnaryExpression unary && ("-".equals(unary.getOp()) || "+".equals(unary.getOp()))
+                && isLiteralValue(unary.getExpression());
+    }
+
     // Filters counterexample assignments only in found VC and sorts them in the order of its binders
     private Counterexample filterCounterexample(Counterexample counterexample) {
         if (counterexample == null)

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -76,7 +76,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
         DebugLog.smtResult(result);
         if (result.isError()) {
-            throw new RefinementError(element.getPosition(), declarationPosition, expectedType,
+            throw new RefinementError(element.getPosition(), declarationPosition, expectedType, expected,
                     implBeforeChange.simplify(), map, result.getCounterexample(), customMessage);
         }
     }
@@ -96,8 +96,8 @@ public void processSubtyping(Predicate type, Predicate expectedType, List<GhostS
             SourcePosition declarationPosition, Factory f) throws LJError {
         SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
         if (result.isError())
-            throwRefinementError(element.getPosition(), declarationPosition, expectedType, type,
-                    result.getCounterexample(), null);
+            throwRefinementError(element.getPosition(), declarationPosition, expectedType, result.getFinalExpected(),
+                    type, result.getCounterexample(), null);
     }
 
     /**
@@ -183,7 +183,7 @@ public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType,
         if (!silent) {
             DebugLog.smtResult(result);
         }
-        return result;
+        return result.withFinalExpected(expected);
     }
 
     /**
@@ -404,10 +404,16 @@ private VCImplication buildPremiseChain(TranslationTable map, Predicate... predi
 
     protected void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             Predicate found, Counterexample counterexample, String customMessage) throws RefinementError {
+        throwRefinementError(position, declarationPosition, expected, null, found, counterexample, customMessage);
+    }
+
+    protected void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
+            Predicate finalExpected, Predicate found, Counterexample counterexample, String customMessage)
+            throws RefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication premises = buildPremiseChain(map, expected, found);
-        throw new RefinementError(position, declarationPosition, expected, premises.simplify(), map, counterexample,
-                customMessage);
+        throw new RefinementError(position, declarationPosition, expected, finalExpected, premises.simplify(), map,
+                counterexample, customMessage);
     }
 
     protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,

liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java

@@ -1,18 +1,26 @@
 package liquidjava.smt;
 
+import liquidjava.rj_language.Predicate;
+
 public class SMTResult {
     private final Counterexample counterexample;
+    private final Predicate finalExpected;
 
-    private SMTResult(Counterexample counterexample) {
+    private SMTResult(Counterexample counterexample, Predicate finalExpected) {
         this.counterexample = counterexample;
+        this.finalExpected = finalExpected;
     }
 
     public static SMTResult ok() {
-        return new SMTResult(null);
+        return new SMTResult(null, null);
     }
 
     public static SMTResult error(Counterexample counterexample) {
-        return new SMTResult(counterexample);
+        return new SMTResult(counterexample, null);
+    }
+
+    public SMTResult withFinalExpected(Predicate expected) {
+        return new SMTResult(counterexample, expected);
     }
 
     public boolean isOk() {
@@ -26,4 +34,8 @@ public boolean isError() {
     public Counterexample getCounterexample() {
         return counterexample;
     }
+
+    public Predicate getFinalExpected() {
+        return finalExpected;
+    }
 }

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java

@@ -32,6 +32,17 @@ void integerDivisionIncludesInputAndGeneratedReturn() {
     void dependentUpperBoundIncludesBoundaryValuesInBinderOrder() {
         RefinementError error = verify("ErrorDependentUpperBound.java");
         assertAssignments(error, assignment("len", "1"), assignment("i", "0"), assignment("#ret", "1"));
+        assertNotNull(error.getFinalExpected());
+        assertNotNull(error.getExpectedWithWitness());
+        assertTrue(error.getCounterexampleStr().contains("With witness:"));
+    }
+
+    @Test
+    void aliasFailureRetainsOriginalAndExpandedExpectedPredicates() {
+        RefinementError error = verify("ErrorAliasSimple.java");
+        assertTrue(error.getExpected().getExpression().toDisplayString().contains("PtGrade"));
+        assertNotNull(error.getFinalExpected());
+        assertFalse(error.getFinalExpected().getExpression().toDisplayString().contains("PtGrade"));
     }
 
     @Test

liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementWitnessTest.java

@@ -0,0 +1,76 @@
+package liquidjava.diagnostics.errors;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertNotNull;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.opt.VCSimplificationResult;
+import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.smt.Counterexample;
+import liquidjava.utils.Pair;
+import spoon.Launcher;
+import spoon.reflect.factory.Factory;
+
+class RefinementWitnessTest {
+
+    private static final Factory FACTORY = new Launcher().getFactory();
+
+    @Test
+    void expandsTheFinalExpectedPredicateBeforeShowingTheWitness() {
+        RefinementError error = error("Positive(buffered)", "buffered > 0", List.of("buffered"),
+                new Pair<>("buffered", "0"));
+
+        assertEquals("Positive(buffered)", error.getExpected().getExpression().toDisplayString());
+        assertEquals("buffered > 0", error.getFinalExpected().getExpression().toDisplayString());
+        assertEquals("0 > 0", error.getExpectedWithWitness().getExpression().toDisplayString());
+        assertTrue(error.getCounterexampleStr().contains("With witness: 0 > 0 ✗"));
+    }
+
+    @Test
+    void substitutesEveryAvailableValueAndEveryOccurrence() {
+        RefinementError error = error("x < y && x != 0", "x < y && x != 0", List.of("x", "y"), new Pair<>("x", "0"),
+                new Pair<>("y", "1"));
+
+        assertEquals("0 < 1 && 0 != 0", error.getExpectedWithWitness().getExpression().toDisplayString());
+    }
+
+    @Test
+    void leavesValuesThatAreNotSafeLiteralsUnchanged() {
+        RefinementError error = error("x < y", "x < y", List.of("x", "y"), new Pair<>("x", "-1"),
+                new Pair<>("y", "other"));
+
+        assertNotNull(error.getExpectedWithWitness());
+        assertEquals("-1 < y", error.getExpectedWithWitness().getExpression().toDisplayString());
+        assertTrue(error.getCounterexampleStr().contains("With witness: -1 < y"));
+    }
+
+    @SafeVarargs
+    private static RefinementError error(String original, String finalExpression, List<String> binders,
+            Pair<String, String>... assignments) {
+        VCImplication first = null;
+        VCImplication last = null;
+        for (String binder : binders) {
+            VCImplication current = new VCImplication(binder, FACTORY.Type().INTEGER_PRIMITIVE, new Predicate());
+            if (last != null)
+                last.setNext(current);
+            if (first == null)
+                first = current;
+            last = current;
+        }
+        assertNotNull(first);
+        return new RefinementError(null, null, predicate(original), predicate(finalExpression),
+                new VCSimplificationResult(first), new TranslationTable(), new Counterexample(List.of(assignments)),
+                null);
+    }
+
+    private static Predicate predicate(String source) {
+        return new Predicate(RefinementsParser.createAST(source, ""));
+    }
+}