From 4de591575b8bd73a540d415d0097738a2e28aa2a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Nov 2026 17:31:05 +0000 Subject: [PATCH 1/3] Keep the values expected depends on in the counterexample The counterexample kept only the binders of the simplified found, so a variable found knows nothing about (simplified to true) lost its value, while unrelated path conditions and unmentioned path binders stayed. It now keeps the variables and ghost applications of the expected refinement plus those of the found conjuncts linked to them, still hiding values found already states. Terms only expected mentions come first, generated names last, the rest in the order of the VC binders. Co-Authored-By: Claude Opus 5.5 --- .../ErrorCounterexampleAliasedArgument.java | 15 ++++ .../ErrorCounterexampleBranchArgument.java | 17 ++++ .../ErrorCounterexampleCallArgument.java | 18 ++++ .../ErrorCounterexampleFieldArgument.java | 16 ++++ .../ErrorCounterexampleGhostArgument.java | 22 +++++ .../ErrorCounterexampleGuardedArgument.java | 16 ++++ .../ErrorCounterexampleKnownArgument.java | 14 +++ .../ErrorCounterexampleKnownGhost.java | 27 ++++++ ...rrorCounterexampleLinkedPathCondition.java | 16 ++++ .../ErrorCounterexampleNothingKnown.java | 12 +++ .../ErrorCounterexampleRefinementAlias.java | 16 ++++ .../ErrorCounterexampleReturnPath.java | 13 +++ .../ErrorCounterexampleSeveralArguments.java | 16 ++++ ...orCounterexampleUnconstrainedArgument.java | 15 ++++ .../diagnostics/errors/RefinementError.java | 87 +++++++++++++++++-- .../ast/formatter/VariableFormatter.java | 9 ++ .../api/tests/TestCounterexamples.java | 86 ++++++++++++++++++ .../RefinementErrorCounterexampleTest.java | 86 ++++++++++++++++++ .../ast/formatter/VariableFormatterTest.java | 8 ++ 19 files changed, 503 insertions(+), 6 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleAliasedArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleBranchArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCallArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleFieldArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGhostArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardedArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGhost.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleLinkedPathCondition.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleNothingKnown.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleRefinementAlias.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnPath.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleSeveralArguments.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleUnconstrainedArgument.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleAliasedArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleAliasedArgument.java new file mode 100644 index 000000000..d6e69431f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleAliasedArgument.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleAliasedArgument { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(int port, int configured) { + if (port < 0 || port > 65535) + return; + int timeout = configured; + connect(timeout); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleBranchArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleBranchArgument.java new file mode 100644 index 000000000..d84dad160 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleBranchArgument.java @@ -0,0 +1,17 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleBranchArgument { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(boolean secure, int port, int timeout) { + if (secure) { + connect(0); + } else { + if (port > 1024) + connect(timeout); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCallArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCallArgument.java new file mode 100644 index 000000000..fea027ebc --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCallArgument.java @@ -0,0 +1,18 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleCallArgument { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static int read(int key) { + return key; + } + + static void probe(int port, int key) { + if (port < 0) + return; + connect(read(key) - 1); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleFieldArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleFieldArgument.java new file mode 100644 index 000000000..30c25c4df --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleFieldArgument.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleFieldArgument { + + int timeout; + + static void connect(@Refinement("_ >= 0") int timeout) {} + + void probe(int port) { + if (port < 0) + return; + connect(this.timeout); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGhostArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGhostArgument.java new file mode 100644 index 000000000..5b68a3be6 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGhostArgument.java @@ -0,0 +1,22 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; + +@Ghost("int size") +class CounterexampleBag { + @StateRefinement(to = "size(this) == 0") + CounterexampleBag() {} +} + +public class ErrorCounterexampleGhostArgument { + + static void take(@Refinement("size(b) > 0") CounterexampleBag b) {} + + static void probe(int port, CounterexampleBag bag) { + if (port < 0) + return; + take(bag); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardedArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardedArgument.java new file mode 100644 index 000000000..4d10de381 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardedArgument.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleGuardedArgument { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(int port, int timeout) { + if (timeout > 100) + return; + if (port < 0) + return; + connect(timeout); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownArgument.java new file mode 100644 index 000000000..a6b0f8137 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownArgument.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleKnownArgument { + + static void window(@Refinement("_ > size") int capacity, int size) {} + + static void probe(int port, int capacity) { + if (port < 0) + return; + window(capacity, 10); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGhost.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGhost.java new file mode 100644 index 000000000..1f2dbfbf7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGhost.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; + +@Ghost("int size") +class CounterexampleStack { + @StateRefinement(to = "size(this) == 0") + CounterexampleStack() {} + + @StateRefinement(to = "size(this) == size(old(this)) + 1") + void push() {} +} + +public class ErrorCounterexampleKnownGhost { + + static void take(@Refinement("size(s) > 1") CounterexampleStack s) {} + + static void probe(int port) { + CounterexampleStack s = new CounterexampleStack(); + if (port < 0) + return; + s.push(); + take(s); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleLinkedPathCondition.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleLinkedPathCondition.java new file mode 100644 index 000000000..963e604e0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleLinkedPathCondition.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleLinkedPathCondition { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(int port, int retries) { + if (retries > 3) + return; + if (port < 0) + return; + connect(port - 1); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleNothingKnown.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleNothingKnown.java new file mode 100644 index 000000000..ece4c5ca2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleNothingKnown.java @@ -0,0 +1,12 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleNothingKnown { + + static void sleep(@Refinement("_ >= 0") int millis) {} + + static void probe(int millis) { + sleep(millis); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleRefinementAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleRefinementAlias.java new file mode 100644 index 000000000..6f2648e15 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleRefinementAlias.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; + +@RefinementAlias("NonNegative(int v) { v >= 0 }") +public class ErrorCounterexampleRefinementAlias { + + static void connect(@Refinement("NonNegative(_)") int timeout) {} + + static void probe(int port, int timeout) { + if (port < 0) + return; + connect(timeout); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnPath.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnPath.java new file mode 100644 index 000000000..64878907c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnPath.java @@ -0,0 +1,13 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleReturnPath { + + @Refinement("_ >= 0") + static int timeoutOf(int port, int configured) { + if (port < 0) + return 0; + return configured; // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleSeveralArguments.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleSeveralArguments.java new file mode 100644 index 000000000..0f864dfae --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleSeveralArguments.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleSeveralArguments { + + static void range(@Refinement("_ >= 0") int from, @Refinement("_ >= from") int to) {} + + static void probe(int port, int lo, int hi) { + if (port < 0) + return; + if (lo < 0) + return; + range(lo, hi); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleUnconstrainedArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleUnconstrainedArgument.java new file mode 100644 index 000000000..68b7c2789 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleUnconstrainedArgument.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// #453: found knows nothing about timeout, and the port guard does not affect it +public class ErrorCounterexampleUnconstrainedArgument { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(int port, int timeout) { + if (port < 0 || port > 65535) + return; + connect(timeout); // Expect: Refinement Error + } +} 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 42684ce8c..ce7fa70d6 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,9 @@ package liquidjava.diagnostics.errors; +import java.util.ArrayList; +import java.util.Comparator; +import java.util.HashSet; +import java.util.Iterator; import java.util.List; import java.util.Set; import java.util.stream.Collectors; @@ -9,10 +13,13 @@ import liquidjava.diagnostics.hints.Hint; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; import liquidjava.utils.Pair; +import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; @@ -24,6 +31,8 @@ */ public class RefinementError extends LJError { + private static final String FRESH_PREFIX = "#fresh_"; + private final Predicate expected; private final VCSimplificationResult found; private final Counterexample counterexample; @@ -77,20 +86,86 @@ public VCSimplificationResult getFound() { return found; } - // Filters counterexample assignments only in found VC and sorts them in the order of its binders + // Keeps the counterexample assignments to the terms of expected and of the found conjuncts linked to them, except + // values found already states, listing the terms only expected mentions first, generated names last, and the rest + // in the order of the VC binders private Counterexample filterCounterexample(Counterexample counterexample) { if (counterexample == null) return new Counterexample(List.of()); - List binderNames = getFound().getBinders(); - Set knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream() - .map(Expression::toString).collect(Collectors.toSet()); + Expression foundExpression = getFound().getImplication().toPredicate().getExpression(); + List conjuncts = foundExpression.getConjuncts(); + List foundTerms = termsOf(foundExpression); + List expectedTerms = termsOf(getExpected().getExpression()); + Set relevantTerms = expectedTerms.isEmpty() ? new HashSet<>(foundTerms) + : linkedTerms(conjuncts, expectedTerms); + List order = new ArrayList<>(originalBinders()); + order.addAll(foundTerms); + order.addAll(expectedTerms); + Set knownAssignments = conjuncts.stream().map(Expression::toString).collect(Collectors.toSet()); List> assignments = counterexample.assignments().stream() - .filter(a -> binderNames.contains(a.first())) + .filter(a -> relevantTerms.contains(a.first())) .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second())) - .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) + .sorted(Comparator.> comparingInt(a -> relevance(a.first(), foundTerms)) + .thenComparingInt(a -> order.indexOf(a.first()))) .toList(); return new Counterexample(assignments); } + + // Terms of expected plus those of every conjunct sharing a term with them, directly or through other conjuncts. + // The remaining conjuncts constrain other values only, so any values satisfying them make the same counterexample + private static Set linkedTerms(List conjuncts, List expectedTerms) { + Set linked = new HashSet<>(expectedTerms); + List> unlinked = conjuncts.stream().map(RefinementError::termsOf) + .collect(Collectors.toCollection(ArrayList::new)); + boolean changed = true; + while (changed) { + changed = false; + for (Iterator> it = unlinked.iterator(); it.hasNext();) { + List terms = it.next(); + if (terms.stream().anyMatch(linked::contains)) { + linked.addAll(terms); + it.remove(); + changed = true; + } + } + } + return linked; + } + + // Binders of the VC chain before simplification, which keeps the variables in the order they were introduced + private List originalBinders() { + VCSimplificationResult original = getFound(); + while (original.getOrigin() != null) + original = original.getOrigin(); + return original.getBinders(); + } + + // 0 when found says nothing about the term, so its value alone breaks expected; 2 for generated names + private static int relevance(String term, List foundTerms) { + if (!foundTerms.contains(term)) + return 0; + return term.startsWith(FRESH_PREFIX) ? 2 : 1; + } + + // Variables and ghost applications of an expression, named as in the SMT model + private static List termsOf(Expression expression) { + List terms = new ArrayList<>(); + expression.getVariableNames(terms); + addGhostApplications(expression, terms); + return terms; + } + + private static void addGhostApplications(Expression expression, List terms) { + if (expression instanceof FunctionInvocation invocation + && invocation.getArgs().stream().allMatch(Var.class::isInstance)) { + String args = invocation.getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")); + String term = Utils.getSimpleName(invocation.getName()) + "(" + args + ")"; + if (!terms.contains(term)) + terms.add(term); + } + for (Expression child : expression.getChildren()) + addGhostApplications(child, terms); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 0a9422932..4d9f5e1fe 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java @@ -1,19 +1,28 @@ package liquidjava.rj_language.ast.formatter; +import java.util.Arrays; import java.util.regex.Matcher; import java.util.regex.Pattern; +import java.util.stream.Collectors; /** * Formats internal variable names into a cleaner display representation using superscript notation */ public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); + private static final Pattern APPLICATION_PATTERN = Pattern.compile("^([^(]+)\\((.*)\\)$"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; public static String format(String name) { if (name == null) return null; + // ghost applications such as size(#s_2) are named by their arguments + Matcher application = APPLICATION_PATTERN.matcher(name); + if (application.matches()) + return application.group(1) + "(" + Arrays.stream(application.group(2).split(", ")) + .map(VariableFormatter::format).collect(Collectors.joining(", ")) + ")"; + Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); if (!matcher.matches()) return name; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 9d45cde00..7790f8bd2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -82,6 +82,92 @@ void booleanCounterexampleIncludesInputAndGeneratedReturn() { assertAssignments(error, assignment("value", "false"), assignment("#ret", "false")); } + @Test + void argumentFoundKnowsNothingAboutIsKeptWhileUnrelatedGuardIsOmitted() { + RefinementError error = verify("ErrorCounterexampleUnconstrainedArgument.java"); + assertAssignments(error, assignment("timeout", "-1")); + } + + @Test + void argumentIsKeptWhenFoundIsTrue() { + RefinementError error = verify("ErrorCounterexampleNothingKnown.java"); + assertAssignments(error, assignment("millis", "-1")); + } + + @Test + void argumentConstrainedByFoundIsKeptWhileUnrelatedGuardIsOmitted() { + RefinementError error = verify("ErrorCounterexampleGuardedArgument.java"); + assertAssignments(error, assignment("timeout", "-1")); + } + + @Test + void aliasedArgumentKeepsTheVariableItCopiesInBinderOrder() { + RefinementError error = verify("ErrorCounterexampleAliasedArgument.java"); + assertAssignments(error, assignment("configured", "-1"), assignment("#timeout", "-1")); + } + + @Test + void fieldArgumentKeepsTheField() { + RefinementError error = verify("ErrorCounterexampleFieldArgument.java"); + assertAssignments(error, assignment("this#testSuite.ErrorCounterexampleFieldArgument.timeout", "-1"), + assignment("#timeout", "-1")); + } + + @Test + void callInsideArgumentKeepsItsResultAfterTheArgument() { + RefinementError error = verify("ErrorCounterexampleCallArgument.java"); + assertAssignments(error, assignment("#timeout", "-1"), assignment("#fresh", "0")); + } + + @Test + void branchConditionsThatDoNotAffectTheArgumentAreOmitted() { + RefinementError error = verify("ErrorCounterexampleBranchArgument.java"); + assertAssignments(error, assignment("timeout", "-1")); + } + + @Test + void severalExpectedVariablesListTheUnconstrainedOneFirst() { + RefinementError error = verify("ErrorCounterexampleSeveralArguments.java"); + assertAssignments(error, assignment("hi", "0"), assignment("lo", "1")); + } + + @Test + void knownArgumentIsOmittedWhileTheOtherArgumentIsKept() { + RefinementError error = verify("ErrorCounterexampleKnownArgument.java"); + assertAssignments(error, assignment("capacity", "0")); + } + + @Test + void pathConditionLinkedToTheArgumentIsKeptWhileUnlinkedOneIsOmitted() { + RefinementError error = verify("ErrorCounterexampleLinkedPathCondition.java"); + assertAssignments(error, assignment("port", "0"), assignment("#timeout", "-1")); + } + + @Test + void returnKeepsItsSourceWhileUnrelatedPathConditionIsOmitted() { + RefinementError error = verify("ErrorCounterexampleReturnPath.java"); + assertAssignments(error, assignment("configured", "-1"), assignment("#ret", "-1")); + } + + @Test + void refinementAliasArgumentIsKept() { + RefinementError error = verify("ErrorCounterexampleRefinementAlias.java"); + assertAssignments(error, assignment("timeout", "-1")); + } + + @Test + void ghostOfArgumentFoundKnowsNothingAboutIsKept() { + RefinementError error = verify("ErrorCounterexampleGhostArgument.java"); + assertAssignments(error, assignment("size(bag)", "0")); + assertTrue(error.getCounterexampleStr().contains("Counterexample: size(bag) == 0")); + } + + @Test + void ghostValueFoundAlreadyStatesIsOmitted() { + RefinementError error = verify("ErrorCounterexampleKnownGhost.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + private static RefinementError verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java new file mode 100644 index 000000000..e86a91212 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -0,0 +1,86 @@ +package liquidjava.diagnostics.errors; + +import static liquidjava.utils.VCTestUtils.vc; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNull; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.util.Arrays; +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.parsing.RefinementsParser; +import liquidjava.smt.Counterexample; +import liquidjava.utils.Pair; + +class RefinementErrorCounterexampleTest { + + @Test + void keepsExpectedVariableSimplifiedOutOfFound() { + RefinementError error = error("timeout >= 0", vc("∀port:int. port > 0", "∀timeout:int. true", "true"), + "timeout=-1", "port=1"); + assertEquals(List.of(pair("timeout", "-1")), error.getCounterexample().assignments()); + assertEquals("Counterexample: timeout == -1", error.getCounterexampleStr()); + } + + @Test + void omitsFoundConjunctsUnlinkedToExpected() { + RefinementError error = error("x > y", + vc("∀a:int. a > 0", "∀x:int. x == a", "∀b:int. b < 0", "∀y:int. true", "true"), "a=1", "b=-1", "x=1", + "y=5"); + assertEquals(List.of(pair("y", "5"), pair("a", "1"), pair("x", "1")), error.getCounterexample().assignments()); + } + + @Test + void keepsFoundConjunctsLinkedThroughAnEqualityChain() { + RefinementError error = error("c >= 0", vc("∀a:int. a < 0", "∀b:int. b == a", "∀c:int. c == b", "true"), "c=-1", + "b=-1", "a=-1"); + assertEquals(List.of(pair("a", "-1"), pair("c", "-1")), error.getCounterexample().assignments()); + } + + @Test + void omitsUnmentionedPathBinderAndListsGeneratedNamesLast() { + RefinementError error = error("t >= 0", vc("∀#fresh_1:int. true", "∀port:int. true", + "∀#fresh_2:boolean. port > 0", "∀t:int. t == #fresh_1 + port", "true"), "#fresh_2=false", "t=-1", + "#fresh_1=-2", "port=1"); + assertEquals(List.of(pair("port", "1"), pair("t", "-1"), pair("#fresh_1", "-2")), + error.getCounterexample().assignments()); + } + + @Test + void omitsValuesFoundAlreadyStates() { + RefinementError error = error("capacity > size", vc("∀size:int. size == 10", "∀capacity:int. true", "true"), + "size=10", "capacity=0"); + assertEquals(List.of(pair("capacity", "0")), error.getCounterexample().assignments()); + } + + @Test + void keepsGhostApplicationsOfExpectedAndFormatsTheirArguments() { + RefinementError error = error("size(#s_3) > 0", vc("∀port:int. port > 0", "true"), "port=1", "size(#s_3)=0", + "length(#a_1)=4"); + assertEquals(List.of(pair("size(#s_3)", "0")), error.getCounterexample().assignments()); + assertEquals("Counterexample: size(s³) == 0", error.getCounterexampleStr()); + } + + @Test + void hasNoCounterexampleWhenOnlyUnrelatedValuesRemain() { + RefinementError error = error("x > 1", vc("∀x:int. x == 1", "∀port:int. port > 0", "true"), "x=1", "port=1"); + assertTrue(error.getCounterexample().isEmpty()); + assertNull(error.getCounterexampleStr()); + } + + private static RefinementError error(String expected, VCImplication found, String... assignments) { + Counterexample counterexample = new Counterexample( + Arrays.stream(assignments).map(a -> a.split("=")).map(parts -> pair(parts[0], parts[1])).toList()); + return new RefinementError(null, null, new Predicate(RefinementsParser.createAST(expected, "")), + found.simplify(), new TranslationTable(), counterexample, null); + } + + private static Pair pair(String name, String value) { + return new Pair<>(name, value); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java index cf92ff266..e832502a8 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java @@ -14,4 +14,12 @@ void formatsVariables() { assertEquals("#ret³", VariableFormatter.format("#ret_3")); assertEquals("this#Class", VariableFormatter.format("this#Class")); } + + @Test + void formatsGhostApplicationArguments() { + assertEquals("size(s²)", VariableFormatter.format("size(#s_2)")); + assertEquals("size(bag)", VariableFormatter.format("size(bag)")); + assertEquals("at(list³, #fresh¹²)", VariableFormatter.format("at(#list_3, #fresh_12)")); + assertEquals("size(this)", VariableFormatter.format("size(this)")); + } } From 18c5f3249d71791a590d0feabd17e879503077e2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Nov 2026 21:53:08 +0000 Subject: [PATCH 2/3] Split guards, list expected first and hide what found or Z3 alone can read Review follow-ups for the counterexample filter: - Negated disjunctions and double negations are split into separate facts before linking, so one combined guard no longer links every variable in it to expected. - The terms of expected come before the terms linked to them. - Known values are compared structurally, so enum constants (Format.JPG against the model's JPG) and ghost applications with several arguments are recognised. - Array values are left out of the model; their ghosts (length(a)) remain. - When every linked value is known, the counterexample falls back to the other terms found shows, such as the path condition of a constant return. - The fresh name prefix lives in Formats, and ghost application names are formatted with a nesting-aware scanner. Co-Authored-By: Claude Opus 5.5 --- .../ErrorCounterexampleArrayArgument.java | 14 +++ .../ErrorCounterexampleArrayIndex.java | 15 +++ .../ErrorCounterexampleCombinedGuard.java | 14 +++ ...orCounterexampleGuardRelatesArguments.java | 14 +++ .../ErrorCounterexampleKnownEnum.java | 17 +++ .../ErrorCounterexampleMixedGuard.java | 14 +++ .../ErrorCounterexampleReturnConstant.java | 13 +++ .../diagnostics/errors/RefinementError.java | 108 +++++++++++++----- .../ast/formatter/VariableFormatter.java | 41 +++++-- .../opt/VCBinderSimplification.java | 3 +- .../java/liquidjava/smt/TranslatorToZ3.java | 5 +- .../liquidjava/utils/constants/Formats.java | 3 +- .../api/tests/TestCounterexamples.java | 72 +++++++++--- .../RefinementErrorCounterexampleTest.java | 62 +++++++++- .../ast/formatter/VariableFormatterTest.java | 8 +- 15 files changed, 339 insertions(+), 64 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayIndex.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCombinedGuard.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardRelatesArguments.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownEnum.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleMixedGuard.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnConstant.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayArgument.java new file mode 100644 index 000000000..dc30af08c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayArgument.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleArrayArgument { + + static void get(int[] a, @Refinement("_ >= 0 && _ < length(a)") int i) {} + + static void probe(int port, int[] a) { + if (port < 0) + return; + get(a, 3); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayIndex.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayIndex.java new file mode 100644 index 000000000..bba586b34 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleArrayIndex.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleArrayIndex { + + static void get(int[] a, @Refinement("_ >= 0 && _ < length(a)") int i) {} + + static void probe(int port, int k) { + if (port < 0) + return; + int[] a = new int[4]; + get(a, k); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCombinedGuard.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCombinedGuard.java new file mode 100644 index 000000000..658d787e6 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleCombinedGuard.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleCombinedGuard { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(int port, int retries, int backoff, int window, int timeout) { + if (port < 0 || port > 65535 || retries < 0 || backoff < 0 || window < 1 || timeout > 60000) + return; + connect(timeout); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardRelatesArguments.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardRelatesArguments.java new file mode 100644 index 000000000..3601235cf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleGuardRelatesArguments.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleGuardRelatesArguments { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(int port, int retries, int timeout) { + if (port < 0 || retries > timeout + 5) + return; + connect(timeout); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownEnum.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownEnum.java new file mode 100644 index 000000000..462233e0b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownEnum.java @@ -0,0 +1,17 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleKnownEnum { + + enum Format { + JPG, PNG + } + + static void onlyPng(@Refinement("f == Format.PNG") Format f) {} + + static void probe(Format format) { + if (format == Format.JPG) + onlyPng(format); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleMixedGuard.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleMixedGuard.java new file mode 100644 index 000000000..1bfe5cde8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleMixedGuard.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleMixedGuard { + + static void connect(@Refinement("_ >= 0") int timeout) {} + + static void probe(int port, int retries, int backoff, int timeout) { + if (port < 0 || (retries > 3 && backoff > 10) || timeout > 60000) + return; + connect(timeout); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnConstant.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnConstant.java new file mode 100644 index 000000000..baa859cd4 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnConstant.java @@ -0,0 +1,13 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleReturnConstant { + + @Refinement("_ > 10") + static int ten(int port) { + if (port < 0) + return 0; // Expect: Refinement Error + return 11; + } +} 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 ce7fa70d6..183e8d03e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -12,14 +12,18 @@ import liquidjava.diagnostics.categories.ErrorCategory; import liquidjava.diagnostics.hints.Hint; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; +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.smt.Counterexample; import liquidjava.utils.Pair; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; import spoon.reflect.cu.SourcePosition; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; @@ -31,8 +35,6 @@ */ public class RefinementError extends LJError { - private static final String FRESH_PREFIX = "#fresh_"; - private final Predicate expected; private final VCSimplificationResult found; private final Counterexample counterexample; @@ -86,38 +88,62 @@ public VCSimplificationResult getFound() { return found; } - // Keeps the counterexample assignments to the terms of expected and of the found conjuncts linked to them, except - // values found already states, listing the terms only expected mentions first, generated names last, and the rest - // in the order of the VC binders + // Keeps the counterexample assignments to the terms of expected and of the found facts linked to them, except + // values found already states, or to every term found shows when that leaves nothing. The terms of expected come + // first, those found says nothing about before the rest, then the linked terms in the order of the VC binders, with + // generated names last private Counterexample filterCounterexample(Counterexample counterexample) { if (counterexample == null) return new Counterexample(List.of()); Expression foundExpression = getFound().getImplication().toPredicate().getExpression(); - List conjuncts = foundExpression.getConjuncts(); + List facts = factsOf(foundExpression); List foundTerms = termsOf(foundExpression); List expectedTerms = termsOf(getExpected().getExpression()); - Set relevantTerms = expectedTerms.isEmpty() ? new HashSet<>(foundTerms) - : linkedTerms(conjuncts, expectedTerms); + Set linkedTerms = expectedTerms.isEmpty() ? new HashSet<>(foundTerms) + : linkedTerms(facts, expectedTerms); + List> unknown = counterexample.assignments().stream().filter(a -> !isKnown(a, facts)) + .toList(); + List> assignments = unknown.stream().filter(a -> linkedTerms.contains(a.first())).toList(); + // e.g. a return value found states, where the path condition that led to it is what is left to show + if (assignments.isEmpty()) + assignments = unknown.stream().filter(a -> foundTerms.contains(a.first())).toList(); + List order = new ArrayList<>(originalBinders()); order.addAll(foundTerms); order.addAll(expectedTerms); - Set knownAssignments = conjuncts.stream().map(Expression::toString).collect(Collectors.toSet()); - List> assignments = counterexample.assignments().stream() - .filter(a -> relevantTerms.contains(a.first())) - .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second())) - .sorted(Comparator.> comparingInt(a -> relevance(a.first(), foundTerms)) + return new Counterexample(assignments.stream() + .sorted(Comparator + .> comparingInt(a -> relevance(a.first(), expectedTerms, foundTerms)) .thenComparingInt(a -> order.indexOf(a.first()))) - .toList(); + .toList()); + } - return new Counterexample(assignments); + // Conjuncts of found, also splitting negated disjunctions (!(a || b) is !a && !b) and dropping double negations, so + // each fact links only the terms it relates + private static List factsOf(Expression expression) { + List facts = new ArrayList<>(); + if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { + facts.addAll(factsOf(binary.getFirstOperand())); + facts.addAll(factsOf(binary.getSecondOperand())); + } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) + && not.getExpression()instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { + facts.addAll(factsOf(new UnaryExpression("!", binary.getFirstOperand()))); + facts.addAll(factsOf(new UnaryExpression("!", binary.getSecondOperand()))); + } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) + && not.getExpression()instanceof UnaryExpression inner && "!".equals(inner.getOp())) { + facts.addAll(factsOf(inner.getExpression())); + } else { + facts.add(expression); + } + return facts; } - // Terms of expected plus those of every conjunct sharing a term with them, directly or through other conjuncts. - // The remaining conjuncts constrain other values only, so any values satisfying them make the same counterexample - private static Set linkedTerms(List conjuncts, List expectedTerms) { + // Terms of expected plus those of every fact sharing a term with them, directly or through other facts. The + // remaining facts constrain other values only, so any values satisfying them make the same counterexample + private static Set linkedTerms(List facts, List expectedTerms) { Set linked = new HashSet<>(expectedTerms); - List> unlinked = conjuncts.stream().map(RefinementError::termsOf) + List> unlinked = facts.stream().map(RefinementError::termsOf) .collect(Collectors.toCollection(ArrayList::new)); boolean changed = true; while (changed) { @@ -134,6 +160,21 @@ private static Set linkedTerms(List conjuncts, List return linked; } + // Whether a fact of found is term == value, which the counterexample would only repeat + private static boolean isKnown(Pair assignment, List facts) { + return facts.stream() + .anyMatch(fact -> fact instanceof BinaryExpression binary && "==".equals(binary.getOperator()) + && (states(binary.getFirstOperand(), binary.getSecondOperand(), assignment) + || states(binary.getSecondOperand(), binary.getFirstOperand(), assignment))); + } + + // An enum constant is written Format.JPG in found, either as such or as a variable, and JPG in the model + private static boolean states(Expression term, Expression value, Pair assignment) { + String valueName = value instanceof Enum constant ? constant.getConstName() + : value instanceof Var var ? Utils.getSimpleName(var.getName()) : value.toString(); + return assignment.first().equals(termName(term)) && assignment.second().equals(valueName); + } + // Binders of the VC chain before simplification, which keeps the variables in the order they were introduced private List originalBinders() { VCSimplificationResult original = getFound(); @@ -142,11 +183,12 @@ private List originalBinders() { return original.getBinders(); } - // 0 when found says nothing about the term, so its value alone breaks expected; 2 for generated names - private static int relevance(String term, List foundTerms) { - if (!foundTerms.contains(term)) - return 0; - return term.startsWith(FRESH_PREFIX) ? 2 : 1; + // 0 for terms of expected found says nothing about, whose values alone break it, 1 for the other terms of + // expected, 2 for the terms linked to them and 3 for generated names among those + private static int relevance(String term, List expectedTerms, List foundTerms) { + if (expectedTerms.contains(term)) + return foundTerms.contains(term) ? 1 : 0; + return term.startsWith(Formats.FRESH_PREFIX) ? 3 : 2; } // Variables and ghost applications of an expression, named as in the SMT model @@ -158,14 +200,22 @@ private static List termsOf(Expression expression) { } private static void addGhostApplications(Expression expression, List terms) { + String term = expression instanceof FunctionInvocation ? termName(expression) : null; + if (term != null && !terms.contains(term)) + terms.add(term); + for (Expression child : expression.getChildren()) + addGhostApplications(child, terms); + } + + // Name of a variable, or of a ghost application over variables, as in the SMT model; null for other expressions + private static String termName(Expression expression) { + if (expression instanceof Var var) + return var.getName(); if (expression instanceof FunctionInvocation invocation && invocation.getArgs().stream().allMatch(Var.class::isInstance)) { String args = invocation.getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")); - String term = Utils.getSimpleName(invocation.getName()) + "(" + args + ")"; - if (!terms.contains(term)) - terms.add(term); + return Utils.getSimpleName(invocation.getName()) + "(" + args + ")"; } - for (Expression child : expression.getChildren()) - addGhostApplications(child, terms); + return null; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 4d9f5e1fe..7a2571630 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java @@ -1,27 +1,21 @@ package liquidjava.rj_language.ast.formatter; -import java.util.Arrays; import java.util.regex.Matcher; import java.util.regex.Pattern; -import java.util.stream.Collectors; /** * Formats internal variable names into a cleaner display representation using superscript notation */ public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); - private static final Pattern APPLICATION_PATTERN = Pattern.compile("^([^(]+)\\((.*)\\)$"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; public static String format(String name) { if (name == null) return null; - // ghost applications such as size(#s_2) are named by their arguments - Matcher application = APPLICATION_PATTERN.matcher(name); - if (application.matches()) - return application.group(1) + "(" + Arrays.stream(application.group(2).split(", ")) - .map(VariableFormatter::format).collect(Collectors.joining(", ")) + ")"; + if (isApplication(name)) + return formatApplication(name); Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); if (!matcher.matches()) @@ -52,4 +46,35 @@ private static String toSuperscript(String number) { private static boolean isSpecialIdentifier(String id) { return id.equals("fresh") || id.equals("ret"); } + + private static boolean isApplication(String name) { + int open = name.indexOf('('); + return open > 0 && name.endsWith(")"); + } + + /** + * Formats the arguments of a ghost application such as {@code size(#s_2)}, splitting them only at top-level commas + * so nested applications keep theirs + */ + private static String formatApplication(String name) { + int open = name.indexOf('('); + String args = name.substring(open + 1, name.length() - 1); + StringBuilder formatted = new StringBuilder(name.substring(0, open)).append('('); + int depth = 0; + int start = 0; + for (int i = 0; i <= args.length(); i++) { + char c = i < args.length() ? args.charAt(i) : ','; + if (c == '(') + depth++; + else if (c == ')') + depth--; + else if (c == ',' && depth == 0) { + if (start > 0) + formatted.append(", "); + formatted.append(format(args.substring(start, i).trim())); + start = i + 1; + } + } + return formatted.append(')').toString(); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java index 58dc1f173..6241b5b8d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java @@ -9,13 +9,14 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.Var; +import liquidjava.utils.constants.Formats; /** * Simplifies VCImplication chains by removing vacuous binder implications */ public class VCBinderSimplification implements VCSimplificationPass { - private static final String FRESH_PREFIX = "#fresh_"; + private static final String FRESH_PREFIX = Formats.FRESH_PREFIX; /** * Applies one binder simplification in a VC chain diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index ed497c1a2..1834f10fd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -112,8 +112,9 @@ public Counterexample getCounterexample(Model model) { Symbol name = decl.getName(); Expr value = model.getConstInterp(decl); Pair assignment = new Pair<>(name.toString(), value.toString()); - // Skip values of uninterpreted sorts - if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT) + // Skip values of uninterpreted sorts, and arrays, whose values only Z3 can read + Z3_sort_kind kind = value.getSort().getSortKind(); + if (kind != Z3_sort_kind.Z3_UNINTERPRETED_SORT && kind != Z3_sort_kind.Z3_ARRAY_SORT) assignments.add(assignment); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java index 7bd8557e6..1b6d7acb5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -1,7 +1,8 @@ package liquidjava.utils.constants; public final class Formats { - public static final String FRESH = "#fresh_%d"; + public static final String FRESH_PREFIX = "#fresh_"; + public static final String FRESH = FRESH_PREFIX + "%d"; public static final String INSTANCE = "#%s_%d"; public static final String THIS = "this#%s"; public static final String RET = "#ret_%d"; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 7790f8bd2..6e6befa16 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -19,19 +19,19 @@ class TestCounterexamples { @Test void recursiveDecrementIncludesInputAndGeneratedArgument() { RefinementError error = verify("ErrorRecursiveDecrement.java"); - assertAssignments(error, assignment("x", "1"), assignment("#x", "0")); + assertAssignments(error, assignment("#x", "0"), assignment("x", "1")); } @Test void integerDivisionIncludesInputAndGeneratedReturn() { RefinementError error = verify("ErrorIntegerDivision.java"); - assertAssignments(error, assignment("x", "1"), assignment("#ret", "0")); + assertAssignments(error, assignment("#ret", "0"), assignment("x", "1")); } @Test - void dependentUpperBoundIncludesBoundaryValuesInBinderOrder() { + void dependentUpperBoundListsExpectedValuesBeforeLinkedOnes() { RefinementError error = verify("ErrorDependentUpperBound.java"); - assertAssignments(error, assignment("len", "1"), assignment("i", "0"), assignment("#ret", "1")); + assertAssignments(error, assignment("len", "1"), assignment("#ret", "1"), assignment("i", "0")); } @Test @@ -43,7 +43,7 @@ void literalZeroHasNoCounterexampleBecauseValueIsAlreadyKnown() { @Test void identityRetainsInputAndReturnSelectedByTheModel() { RefinementError error = verify("ErrorIdentity.java"); - assertAssignments(error, assignment("x", "0"), assignment("#ret", "0")); + assertAssignments(error, assignment("#ret", "0"), assignment("x", "0")); } @Test @@ -67,19 +67,19 @@ void multipleParametersAndGeneratedReturnFollowBinderOrder() { @Test void variableUpdateIncludesNegativeInputAndGeneratedReturn() { RefinementError error = verify("ErrorAssignmentBeforeReturn.java"); - assertAssignments(error, assignment("x", "-1"), assignment("#ret", "0")); + assertAssignments(error, assignment("#ret", "0"), assignment("x", "-1")); } @Test void pathConditionIsOmittedWhileRecursiveArgumentRemains() { RefinementError error = verify("ErrorRecursion.java"); - assertAssignments(error, assignment("k", "0"), assignment("#k", "-1")); + assertAssignments(error, assignment("#k", "-1"), assignment("k", "0")); } @Test void booleanCounterexampleIncludesInputAndGeneratedReturn() { RefinementError error = verify("ErrorBoolean.java"); - assertAssignments(error, assignment("value", "false"), assignment("#ret", "false")); + assertAssignments(error, assignment("#ret", "false"), assignment("value", "false")); } @Test @@ -101,16 +101,16 @@ void argumentConstrainedByFoundIsKeptWhileUnrelatedGuardIsOmitted() { } @Test - void aliasedArgumentKeepsTheVariableItCopiesInBinderOrder() { + void aliasedArgumentKeepsTheVariableItCopiesAfterIt() { RefinementError error = verify("ErrorCounterexampleAliasedArgument.java"); - assertAssignments(error, assignment("configured", "-1"), assignment("#timeout", "-1")); + assertAssignments(error, assignment("#timeout", "-1"), assignment("configured", "-1")); } @Test void fieldArgumentKeepsTheField() { RefinementError error = verify("ErrorCounterexampleFieldArgument.java"); - assertAssignments(error, assignment("this#testSuite.ErrorCounterexampleFieldArgument.timeout", "-1"), - assignment("#timeout", "-1")); + assertAssignments(error, assignment("#timeout", "-1"), + assignment("this#testSuite.ErrorCounterexampleFieldArgument.timeout", "-1")); } @Test @@ -140,13 +140,13 @@ void knownArgumentIsOmittedWhileTheOtherArgumentIsKept() { @Test void pathConditionLinkedToTheArgumentIsKeptWhileUnlinkedOneIsOmitted() { RefinementError error = verify("ErrorCounterexampleLinkedPathCondition.java"); - assertAssignments(error, assignment("port", "0"), assignment("#timeout", "-1")); + assertAssignments(error, assignment("#timeout", "-1"), assignment("port", "0")); } @Test void returnKeepsItsSourceWhileUnrelatedPathConditionIsOmitted() { RefinementError error = verify("ErrorCounterexampleReturnPath.java"); - assertAssignments(error, assignment("configured", "-1"), assignment("#ret", "-1")); + assertAssignments(error, assignment("#ret", "-1"), assignment("configured", "-1")); } @Test @@ -163,11 +163,53 @@ void ghostOfArgumentFoundKnowsNothingAboutIsKept() { } @Test - void ghostValueFoundAlreadyStatesIsOmitted() { + void ghostValueFoundAlreadyStatesIsOmittedSoThePathConditionIsShown() { RefinementError error = verify("ErrorCounterexampleKnownGhost.java"); + assertAssignments(error, assignment("port", "0")); + } + + @Test + void combinedGuardShowsOnlyTheArgument() { + RefinementError error = verify("ErrorCounterexampleCombinedGuard.java"); + assertAssignments(error, assignment("timeout", "-1")); + } + + @Test + void mixedGuardShowsOnlyTheArgument() { + RefinementError error = verify("ErrorCounterexampleMixedGuard.java"); + assertAssignments(error, assignment("timeout", "-1")); + } + + @Test + void guardRelatingTheArgumentToAnotherVariableKeepsItAfterTheArgument() { + RefinementError error = verify("ErrorCounterexampleGuardRelatesArguments.java"); + assertAssignments(error, assignment("timeout", "-1"), assignment("retries", "0")); + } + + @Test + void returnedConstantShowsThePathConditionThatLedToIt() { + RefinementError error = verify("ErrorCounterexampleReturnConstant.java"); + assertAssignments(error, assignment("port", "-1")); + } + + @Test + void enumValueFoundAlreadyStatesIsOmitted() { + RefinementError error = verify("ErrorCounterexampleKnownEnum.java"); assertTrue(error.getCounterexample().isEmpty()); } + @Test + void arrayArgumentShowsItsLengthAndNotTheArray() { + RefinementError error = verify("ErrorCounterexampleArrayArgument.java"); + assertAssignments(error, assignment("length(a)", "0")); + } + + @Test + void indexIntoLocalArrayShowsTheIndexAndNotTheArray() { + RefinementError error = verify("ErrorCounterexampleArrayIndex.java"); + assertAssignments(error, assignment("k", "-1")); + } + private static RefinementError verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index e86a91212..fc88bbe70 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -32,14 +32,14 @@ void omitsFoundConjunctsUnlinkedToExpected() { RefinementError error = error("x > y", vc("∀a:int. a > 0", "∀x:int. x == a", "∀b:int. b < 0", "∀y:int. true", "true"), "a=1", "b=-1", "x=1", "y=5"); - assertEquals(List.of(pair("y", "5"), pair("a", "1"), pair("x", "1")), error.getCounterexample().assignments()); + assertEquals(List.of(pair("y", "5"), pair("x", "1"), pair("a", "1")), error.getCounterexample().assignments()); } @Test void keepsFoundConjunctsLinkedThroughAnEqualityChain() { RefinementError error = error("c >= 0", vc("∀a:int. a < 0", "∀b:int. b == a", "∀c:int. c == b", "true"), "c=-1", "b=-1", "a=-1"); - assertEquals(List.of(pair("a", "-1"), pair("c", "-1")), error.getCounterexample().assignments()); + assertEquals(List.of(pair("c", "-1"), pair("a", "-1")), error.getCounterexample().assignments()); } @Test @@ -47,7 +47,7 @@ void omitsUnmentionedPathBinderAndListsGeneratedNamesLast() { RefinementError error = error("t >= 0", vc("∀#fresh_1:int. true", "∀port:int. true", "∀#fresh_2:boolean. port > 0", "∀t:int. t == #fresh_1 + port", "true"), "#fresh_2=false", "t=-1", "#fresh_1=-2", "port=1"); - assertEquals(List.of(pair("port", "1"), pair("t", "-1"), pair("#fresh_1", "-2")), + assertEquals(List.of(pair("t", "-1"), pair("port", "1"), pair("#fresh_1", "-2")), error.getCounterexample().assignments()); } @@ -67,12 +67,66 @@ void keepsGhostApplicationsOfExpectedAndFormatsTheirArguments() { } @Test - void hasNoCounterexampleWhenOnlyUnrelatedValuesRemain() { + void fallsBackToThePathConditionWhenFoundStatesEveryLinkedValue() { RefinementError error = error("x > 1", vc("∀x:int. x == 1", "∀port:int. port > 0", "true"), "x=1", "port=1"); + assertEquals(List.of(pair("port", "1")), error.getCounterexample().assignments()); + } + + @Test + void hasNoCounterexampleWhenFoundStatesEveryValue() { + RefinementError error = error("x > 1", vc("∀x:int. x == 1", "true"), "x=1"); assertTrue(error.getCounterexample().isEmpty()); assertNull(error.getCounterexampleStr()); } + @Test + void splitsNegatedDisjunctionsSoEachGuardLinksOnlyItsOwnVariables() { + RefinementError error = error("t >= 0", + vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", + "∀#fresh_1:boolean. !(port < 0 || retries < 0 || t > 100)", "true"), + "port=0", "retries=0", "t=-1"); + assertEquals(List.of(pair("t", "-1")), error.getCounterexample().assignments()); + } + + @Test + void splitsNestedConjunctionsAndDoubleNegations() { + RefinementError error = error("t >= 0", + vc("∀port:int. true", "∀retries:int. true", "∀backoff:int. true", "∀t:int. true", + "∀#fresh_1:boolean. !(port < 0 || !!(retries > 3 && backoff > 1) || t > 100)", "true"), + "port=0", "retries=0", "backoff=0", "t=-1"); + assertEquals(List.of(pair("t", "-1")), error.getCounterexample().assignments()); + } + + @Test + void keepsAGuardThatRelatesExpectedToAnotherVariable() { + RefinementError error = error("t >= 0", vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", + "∀#fresh_1:boolean. !(port < 0 || retries > t)", "true"), "port=0", "retries=-2", "t=-1"); + assertEquals(List.of(pair("t", "-1"), pair("retries", "-2")), error.getCounterexample().assignments()); + } + + @Test + void omitsEnumValuesFoundAlreadyStates() { + RefinementError error = error("f == Format.PNG && n > 0", vc("∀f:int. f == Format.JPG", "∀n:int. true", "true"), + "f=JPG", "n=0"); + assertEquals(List.of(pair("n", "0")), error.getCounterexample().assignments()); + } + + @Test + void omitsGhostValuesWithSeveralArgumentsFoundAlreadyStates() { + RefinementError error = error("at(#l_1, #i_2) > 0 && #i_2 > 0", vc("∀#i_2:int. at(#l_1, #i_2) == 0", "true"), + "at(#l_1, #i_2)=0", "#i_2=0"); + assertEquals(List.of(pair("#i_2", "0")), error.getCounterexample().assignments()); + assertEquals("Counterexample: i² == 0", error.getCounterexampleStr()); + } + + @Test + void keepsGhostValuesWithSeveralArgumentsFoundSaysNothingAbout() { + RefinementError error = error("at(#l_1, #i_2) > 0", vc("∀#i_2:int. #i_2 > 0", "true"), "at(#l_1, #i_2)=0", + "#i_2=1"); + assertEquals(List.of(pair("at(#l_1, #i_2)", "0"), pair("#i_2", "1")), error.getCounterexample().assignments()); + assertEquals("Counterexample: at(l¹, i²) == 0 && i² == 1", error.getCounterexampleStr()); + } + private static RefinementError error(String expected, VCImplication found, String... assignments) { Counterexample counterexample = new Counterexample( Arrays.stream(assignments).map(a -> a.split("=")).map(parts -> pair(parts[0], parts[1])).toList()); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java index e832502a8..f04d2c81d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java @@ -13,13 +13,13 @@ void formatsVariables() { assertEquals("#fresh¹²", VariableFormatter.format("#fresh_12")); assertEquals("#ret³", VariableFormatter.format("#ret_3")); assertEquals("this#Class", VariableFormatter.format("this#Class")); - } - - @Test - void formatsGhostApplicationArguments() { + // ghost applications assertEquals("size(s²)", VariableFormatter.format("size(#s_2)")); assertEquals("size(bag)", VariableFormatter.format("size(bag)")); assertEquals("at(list³, #fresh¹²)", VariableFormatter.format("at(#list_3, #fresh_12)")); assertEquals("size(this)", VariableFormatter.format("size(this)")); + assertEquals("f(g(a¹, b²), c³)", VariableFormatter.format("f(g(#a_1, #b_2), #c_3)")); + assertEquals("f(g(h(a¹)), b)", VariableFormatter.format("f(g(h(#a_1)),b)")); + assertEquals("size()", VariableFormatter.format("size()")); } } From b9d7e9b7b21ac69c130744787b48628ea359fd9a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 12:37:00 +0000 Subject: [PATCH 3/3] Show no counterexample when found fixes every value expected depends on The fallback to the other terms found shows could point at an unrelated path condition (port == 1 for take(value) with value == 0 already in found). Only terms linked to expected are now kept, so when found states all of them the counterexample is empty, as for a literal argument. Co-Authored-By: Claude Opus 5.5 --- ...rorCounterexampleKnownAliasedArgument.java | 15 +++++++++ ...rorCounterexampleKnownGuardedArgument.java | 14 ++++++++ ...unterexampleKnownTwiceGuardedArgument.java | 15 +++++++++ .../ErrorCounterexampleReturnFromPath.java | 13 ++++++++ .../diagnostics/errors/RefinementError.java | 14 +++----- .../api/tests/TestCounterexamples.java | 32 ++++++++++++++++--- .../RefinementErrorCounterexampleTest.java | 11 +++++-- 7 files changed, 99 insertions(+), 15 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownAliasedArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGuardedArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownTwiceGuardedArgument.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnFromPath.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownAliasedArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownAliasedArgument.java new file mode 100644 index 000000000..cde569d8f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownAliasedArgument.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleKnownAliasedArgument { + + static void take(@Refinement("_ > 1") int value) {} + + static void probe(int port) { + int base = 0; + int value = base; + if (port > 0) + take(value); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGuardedArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGuardedArgument.java new file mode 100644 index 000000000..44cf6a668 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownGuardedArgument.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleKnownGuardedArgument { + + static void take(@Refinement("_ > 1") int value) {} + + static void probe(int port) { + int value = 0; + if (port > 0) + take(value); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownTwiceGuardedArgument.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownTwiceGuardedArgument.java new file mode 100644 index 000000000..43a320f4f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleKnownTwiceGuardedArgument.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleKnownTwiceGuardedArgument { + + static void take(@Refinement("_ > 1") int value) {} + + static void probe(int port, int retries) { + int value = 0; + if (port > 0) + if (retries < 3) + take(value); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnFromPath.java b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnFromPath.java new file mode 100644 index 000000000..0b218ccfc --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCounterexampleReturnFromPath.java @@ -0,0 +1,13 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorCounterexampleReturnFromPath { + + @Refinement("_ > 10") + static int ten(int port) { + if (port < 0) + return port + 1; // Expect: Refinement Error + return 11; + } +} 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 183e8d03e..47ef1630e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -89,9 +89,9 @@ public VCSimplificationResult getFound() { } // Keeps the counterexample assignments to the terms of expected and of the found facts linked to them, except - // values found already states, or to every term found shows when that leaves nothing. The terms of expected come - // first, those found says nothing about before the rest, then the linked terms in the order of the VC binders, with - // generated names last + // values found already states, so there is none when found fixes every value expected depends on. The terms of + // expected come first, those found says nothing about before the rest, then the linked terms in the order of the + // VC binders, with generated names last private Counterexample filterCounterexample(Counterexample counterexample) { if (counterexample == null) return new Counterexample(List.of()); @@ -102,12 +102,8 @@ private Counterexample filterCounterexample(Counterexample counterexample) { List expectedTerms = termsOf(getExpected().getExpression()); Set linkedTerms = expectedTerms.isEmpty() ? new HashSet<>(foundTerms) : linkedTerms(facts, expectedTerms); - List> unknown = counterexample.assignments().stream().filter(a -> !isKnown(a, facts)) - .toList(); - List> assignments = unknown.stream().filter(a -> linkedTerms.contains(a.first())).toList(); - // e.g. a return value found states, where the path condition that led to it is what is left to show - if (assignments.isEmpty()) - assignments = unknown.stream().filter(a -> foundTerms.contains(a.first())).toList(); + List> assignments = counterexample.assignments().stream() + .filter(a -> linkedTerms.contains(a.first())).filter(a -> !isKnown(a, facts)).toList(); List order = new ArrayList<>(originalBinders()); order.addAll(foundTerms); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 6e6befa16..6c6e5568c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -163,9 +163,9 @@ void ghostOfArgumentFoundKnowsNothingAboutIsKept() { } @Test - void ghostValueFoundAlreadyStatesIsOmittedSoThePathConditionIsShown() { + void ghostValueFoundAlreadyStatesIsOmittedWithTheUnrelatedPathCondition() { RefinementError error = verify("ErrorCounterexampleKnownGhost.java"); - assertAssignments(error, assignment("port", "0")); + assertTrue(error.getCounterexample().isEmpty()); } @Test @@ -187,9 +187,33 @@ void guardRelatingTheArgumentToAnotherVariableKeepsItAfterTheArgument() { } @Test - void returnedConstantShowsThePathConditionThatLedToIt() { + void returnedConstantFoundAlreadyStatesHasNoCounterexample() { RefinementError error = verify("ErrorCounterexampleReturnConstant.java"); - assertAssignments(error, assignment("port", "-1")); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void returnComputedFromThePathConditionShowsBoth() { + RefinementError error = verify("ErrorCounterexampleReturnFromPath.java"); + assertAssignments(error, assignment("#ret", "0"), assignment("port", "-1")); + } + + @Test + void argumentFoundAlreadyStatesHasNoCounterexampleUnderAGuard() { + RefinementError error = verify("ErrorCounterexampleKnownGuardedArgument.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void argumentFoundAlreadyStatesHasNoCounterexampleUnderTwoGuards() { + RefinementError error = verify("ErrorCounterexampleKnownTwiceGuardedArgument.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void argumentKnownThroughAnAliasHasNoCounterexampleUnderAGuard() { + RefinementError error = verify("ErrorCounterexampleKnownAliasedArgument.java"); + assertTrue(error.getCounterexample().isEmpty()); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index fc88bbe70..5beb4df9e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -67,9 +67,16 @@ void keepsGhostApplicationsOfExpectedAndFormatsTheirArguments() { } @Test - void fallsBackToThePathConditionWhenFoundStatesEveryLinkedValue() { + void omitsThePathConditionWhenFoundStatesEveryLinkedValue() { RefinementError error = error("x > 1", vc("∀x:int. x == 1", "∀port:int. port > 0", "true"), "x=1", "port=1"); - assertEquals(List.of(pair("port", "1")), error.getCounterexample().assignments()); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void keepsAPathConditionTheExpectedValueIsComputedFrom() { + RefinementError error = error("#ret_1 > 10", + vc("∀port:int. port < 0", "∀#ret_1:int. #ret_1 == port + 1", "true"), "#ret_1=0", "port=-1"); + assertEquals(List.of(pair("#ret_1", "0"), pair("port", "-1")), error.getCounterexample().assignments()); } @Test