Filter & Sort Counterexamples by Binders

liquidjava-example/src/main/java/testSuite/ErrorBoolean.java

@@ -0,0 +1,11 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorBoolean {
+
+    @Refinement("_ == true")
+    boolean mustBeTrue(boolean value) {
+        return value; // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java

@@ -9,7 +9,7 @@ public static void main(String[] args) {
         int smaller = 5;
         @Refinement("bigger > 20")
         int bigger = 50;
-        @Refinement("_ > smaller  && _ < bigger")
+        @Refinement("_ > smaller && _ < bigger")
         int middle = 21; // Refinement Error
     }
 }

liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorDependentUpperBound {
+
+    @Refinement("0 <= _ && _ < len")
+    int nextIndex(
+            @Refinement("_ > 0") int len,
+            @Refinement("0 <= _ && _ < len") int i) {
+        return i + 1; // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorIdentity.java

@@ -0,0 +1,11 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorIdentity {
+
+    @Refinement("_ > 0")
+    int positiveIdentity(int x) {
+        return x; // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java

@@ -0,0 +1,11 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorIntegerDivision {
+
+    @Refinement("_ > 0")
+    int half(@Refinement("_ > 0") int x) {
+        return x / 2; // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java

@@ -0,0 +1,11 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorLiteralZero {
+
+    @Refinement("_ != 0")
+    int zero() {
+        return 0; // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java

@@ -0,0 +1,10 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorRecursiveDecrement {
+
+    public int f(@Refinement("_ > 0") int x) {
+        return f(x - 1); // Refinement Error
+    }
+}

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

@@ -1,16 +1,16 @@
 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.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.smt.Counterexample;
+import liquidjava.utils.Pair;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -33,43 +33,18 @@ public RefinementError(SourcePosition position, Predicate expected, VCSimplifica
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
-        this.counterexample = counterexample;
+        this.counterexample = filterCounterexample(counterexample);
     }
 
     @Override
     public String getDetails() {
-        String counterexampleString = getCounterExampleString();
-        if (counterexampleString == null)
+        if (counterexample.isEmpty())
             return "";
-        return "Counterexample: " + counterexampleString;
-    }
-
-    public String getCounterExampleString() {
-        if (counterexample == null || counterexample.assignments().isEmpty())
-            return null;
 
-        List<String> foundVarNames = new ArrayList<>();
-        Expression foundExpression = getFound().getImplication().toPredicate().getExpression();
-        Expression expectedExpression = expected.getExpression();
-        foundExpression.getVariableNames(foundVarNames);
-        // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
-        // subtyping check, so the counterexample maps the symbolic name back to its compile-time value
-        foundExpression.getResolvedConstantNames(foundVarNames);
-        expectedExpression.getResolvedConstantNames(foundVarNames);
-        List<String> foundAssignments = foundExpression.getConjuncts().stream().map(Expression::toString).toList();
         String counterexampleString = counterexample.assignments().stream()
-                // only include variables that appear in the found value and are not already fixed there
-                .filter(a -> foundVarNames.contains(a.first())
-                        && !foundAssignments.contains(a.first() + " == " + a.second()))
-                // format as "var == value"
                 .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
-                // join with "&&"
                 .collect(Collectors.joining(" && "));
-
-        if (counterexampleString.isEmpty())
-            return null;
-
-        return counterexampleString;
+        return "Counterexample: " + counterexampleString;
     }
 
     public Counterexample getCounterexample() {
@@ -83,4 +58,18 @@ public Predicate getExpected() {
     public VCSimplificationResult getFound() {
         return found;
     }
+
+    // Filters counterexample assignments only in found VC and sorts them in the order of its binders
+    private Counterexample filterCounterexample(Counterexample counterexample) {
+        List<String> binderNames = getFound().getBinders();
+        Set<String> knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream()
+                .map(Expression::toString).collect(Collectors.toSet());
+        List<Pair<String, String>> assignments = counterexample.assignments().stream()
+                .filter(a -> binderNames.contains(a.first()))
+                .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second()))
+                .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first())))
+                .toList();
+
+        return new Counterexample(assignments);
+    }
 }

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

@@ -23,7 +23,6 @@
 import liquidjava.smt.SMTResult;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Keys;
-import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.factory.Factory;

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java

@@ -1,7 +1,7 @@
 package liquidjava.rj_language.opt;
 
-import java.util.Objects;
-
+import java.util.ArrayList;
+import java.util.List;
 import liquidjava.processor.VCImplication;
 
 /**
@@ -46,6 +46,17 @@ public String getSimplification() {
         return simplification;
     }
 
+    /**
+     * Returns the list of binder names in the simplified VC chain in order of appearance
+     */
+    public List<String> getBinders() {
+        ArrayList<String> binderNames = new ArrayList<>();
+        for (VCImplication current = getImplication(); current != null; current = current.getNext())
+            if (current.hasBinder())
+                binderNames.add(current.getName());
+        return binderNames;
+    }
+
     @Override
     public String toString() {
         if (origin == null)

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

@@ -5,4 +5,7 @@
 import liquidjava.utils.Pair;
 
 public record Counterexample(List<Pair<String, String>> assignments) {
+    public boolean isEmpty() {
+        return assignments.isEmpty();
+    }
 }

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

@@ -3,7 +3,6 @@
 import com.microsoft.z3.ArithExpr;
 import com.microsoft.z3.ArrayExpr;
 import com.microsoft.z3.BoolExpr;
-import com.microsoft.z3.EnumSort;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FPExpr;
 import com.microsoft.z3.FuncDecl;

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

@@ -0,0 +1,104 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.RefinementError;
+import liquidjava.utils.Pair;
+
+class TestCounterexamples {
+
+    private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/";
+
+    @Test
+    void recursiveDecrementIncludesInputAndGeneratedArgument() {
+        RefinementError error = verify("ErrorRecursiveDecrement.java");
+        assertAssignments(error, assignment("x", "1"), assignment("#x", "0"));
+    }
+
+    @Test
+    void integerDivisionIncludesInputAndGeneratedReturn() {
+        RefinementError error = verify("ErrorIntegerDivision.java");
+        assertAssignments(error, assignment("x", "1"), assignment("#ret", "0"));
+    }
+
+    @Test
+    void dependentUpperBoundIncludesBoundaryValuesInBinderOrder() {
+        RefinementError error = verify("ErrorDependentUpperBound.java");
+        assertAssignments(error, assignment("len", "1"), assignment("i", "0"), assignment("#ret", "1"));
+    }
+
+    @Test
+    void literalZeroHasNoCounterexampleBecauseValueIsAlreadyKnown() {
+        RefinementError error = verify("ErrorLiteralZero.java");
+        assertTrue(error.getCounterexample().isEmpty());
+    }
+
+    @Test
+    void identityRetainsInputAndReturnSelectedByTheModel() {
+        RefinementError error = verify("ErrorIdentity.java");
+        assertAssignments(error, assignment("x", "0"), assignment("#ret", "0"));
+    }
+
+    @Test
+    void staticFinalConstantHasNoCounterexampleBecauseValueIsAlreadyKnown() {
+        RefinementError error = verify("ErrorStaticFinalConstant.java");
+        assertTrue(error.getCounterexample().isEmpty());
+    }
+
+    @Test
+    void knownReturnAssignmentIsRemovedWhileDependentAssignmentsRemain() {
+        RefinementError error = verify("ErrorDependentRefinement.java");
+        assertAssignments(error, assignment("smaller", "0"), assignment("bigger", "21"));
+    }
+
+    @Test
+    void multipleParametersAndGeneratedReturnFollowBinderOrder() {
+        RefinementError error = verify("ErrorFunctionDeclarations.java");
+        assertAssignments(error, assignment("d", "0"), assignment("i", "1"), assignment("#ret", "2"));
+    }
+
+    @Test
+    void variableUpdateIncludesNegativeInputAndGeneratedReturn() {
+        RefinementError error = verify("ErrorAssignmentBeforeReturn.java");
+        assertAssignments(error, assignment("x", "-1"), assignment("#ret", "0"));
+    }
+
+    @Test
+    void pathConditionIsOmittedWhileRecursiveArgumentRemains() {
+        RefinementError error = verify("ErrorRecursion.java");
+        assertAssignments(error, assignment("k", "0"), assignment("#k", "-1"));
+    }
+
+    @Test
+    void booleanCounterexampleIncludesInputAndGeneratedReturn() {
+        RefinementError error = verify("ErrorBoolean.java");
+        assertAssignments(error, assignment("value", "false"), assignment("#ret", "false"));
+    }
+
+    private static RefinementError verify(String test) {
+        CommandLineLauncher.launch(TEST_SUITE + test);
+        List<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();
+        assertEquals(1, errors.size(), "Expected exactly one error from " + test);
+        return assertInstanceOf(RefinementError.class, errors.get(0));
+    }
+
+    @SafeVarargs
+    private static void assertAssignments(RefinementError error, Pair<String, String>... expectedAssignments) {
+        // get counterexample assignments without instance numbers in variable names
+        List<Pair<String, String>> actualAssignments = error.getCounterexample().assignments().stream()
+                .map(assignment -> assignment(assignment.first().replaceAll("_[0-9]+$", ""), assignment.second()))
+                .toList();
+        assertEquals(List.of(expectedAssignments), actualAssignments);
+    }
+
+    private static Pair<String, String> assignment(String name, String value) {
+        return new Pair<>(name, value);
+    }
+}

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

@@ -13,8 +13,6 @@
 
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.Diagnostics;
-import liquidjava.diagnostics.errors.*;
-
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.utils.Pair;