diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java new file mode 100644 index 000000000..486ab222d --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java index 42f18673d..d593bc629 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java +++ b/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 } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java new file mode 100644 index 000000000..0310089a1 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java b/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java new file mode 100644 index 000000000..a88c80918 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java b/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java new file mode 100644 index 000000000..6f6e616c7 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java b/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java new file mode 100644 index 000000000..8490425ad --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java new file mode 100644 index 000000000..a9477c971 --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index cbb415ce9..844998556 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.27 + 0.0.28 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava 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 78b5e0aad..e258425aa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/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 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 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 binderNames = getFound().getBinders(); + Set knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream() + .map(Expression::toString).collect(Collectors.toSet()); + List> 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); + } } 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 d2ba3cc17..45cb68138 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 @@ -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; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java index 6f35822d0..05228afc9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java +++ b/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 getBinders() { + ArrayList 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) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java index 3d72973ec..93820e05b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java @@ -5,4 +5,7 @@ import liquidjava.utils.Pair; public record Counterexample(List> assignments) { + public boolean isEmpty() { + return assignments.isEmpty(); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 981f5a138..8eb366eaf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/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; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java new file mode 100644 index 000000000..9d45cde00 --- /dev/null +++ b/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 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... expectedAssignments) { + // get counterexample assignments without instance numbers in variable names + List> actualAssignments = error.getCounterexample().assignments().stream() + .map(assignment -> assignment(assignment.first().replaceAll("_[0-9]+$", ""), assignment.second())) + .toList(); + assertEquals(List.of(expectedAssignments), actualAssignments); + } + + private static Pair assignment(String name, String value) { + return new Pair<>(name, value); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index c2464d708..e739915fb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/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;