From 1f009657d29e25aad7750b81cda76a6af3b86ba8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Fri, 25 Sep 2026 00:44:58 +0100 Subject: [PATCH] Show counterexample values in the final expected refinement --- .../diagnostics/errors/RefinementError.java | 67 +++++++++++++++- .../refinement_checker/VCChecker.java | 18 +++-- .../main/java/liquidjava/smt/SMTResult.java | 18 ++++- .../api/tests/TestCounterexamples.java | 11 +++ .../errors/RefinementWitnessTest.java | 76 +++++++++++++++++++ 5 files changed, 180 insertions(+), 10 deletions(-) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementWitnessTest.java 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 9b46376d1..9ee8d5150 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,5 +1,6 @@ package liquidjava.diagnostics.errors; +import java.util.ArrayList; import java.util.List; import java.util.Set; import java.util.stream.Collectors; @@ -7,8 +8,12 @@ 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,6 +28,8 @@ 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; @@ -30,20 +37,40 @@ public class RefinementError extends LJError { 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 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 assignment : counterexample.assignments()) { + List 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) 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 b51d1c3e4..3a8157afb 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 @@ -76,7 +76,7 @@ public void processSubtyping(Predicate expectedType, List 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 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 binders, + Pair... 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, "")); + } +}