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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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-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-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..47ef1630e 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; @@ -8,11 +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; @@ -77,20 +88,130 @@ 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 facts linked to them, except + // 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()); - 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 facts = factsOf(foundExpression); + List foundTerms = termsOf(foundExpression); + List expectedTerms = termsOf(getExpected().getExpression()); + Set linkedTerms = expectedTerms.isEmpty() ? new HashSet<>(foundTerms) + : linkedTerms(facts, expectedTerms); 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(); + .filter(a -> linkedTerms.contains(a.first())).filter(a -> !isKnown(a, facts)).toList(); - return new Counterexample(assignments); + List order = new ArrayList<>(originalBinders()); + order.addAll(foundTerms); + order.addAll(expectedTerms); + return new Counterexample(assignments.stream() + .sorted(Comparator + .> comparingInt(a -> relevance(a.first(), expectedTerms, foundTerms)) + .thenComparingInt(a -> order.indexOf(a.first()))) + .toList()); + } + + // 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 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 = facts.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; + } + + // 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(); + while (original.getOrigin() != null) + original = original.getOrigin(); + return original.getBinders(); + } + + // 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 + 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) { + 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(", ")); + return Utils.getSimpleName(invocation.getName()) + "(" + args + ")"; + } + 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 0a9422932..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 @@ -14,6 +14,9 @@ public static String format(String name) { if (name == null) return null; + if (isApplication(name)) + return formatApplication(name); + Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); if (!matcher.matches()) return name; @@ -43,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 9d45cde00..6c6e5568c 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,171 @@ 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 + 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 aliasedArgumentKeepsTheVariableItCopiesAfterIt() { + RefinementError error = verify("ErrorCounterexampleAliasedArgument.java"); + assertAssignments(error, assignment("#timeout", "-1"), assignment("configured", "-1")); + } + + @Test + void fieldArgumentKeepsTheField() { + RefinementError error = verify("ErrorCounterexampleFieldArgument.java"); + assertAssignments(error, assignment("#timeout", "-1"), + assignment("this#testSuite.ErrorCounterexampleFieldArgument.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("#timeout", "-1"), assignment("port", "0")); + } + + @Test + void returnKeepsItsSourceWhileUnrelatedPathConditionIsOmitted() { + RefinementError error = verify("ErrorCounterexampleReturnPath.java"); + assertAssignments(error, assignment("#ret", "-1"), assignment("configured", "-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 ghostValueFoundAlreadyStatesIsOmittedWithTheUnrelatedPathCondition() { + RefinementError error = verify("ErrorCounterexampleKnownGhost.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + + @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 returnedConstantFoundAlreadyStatesHasNoCounterexample() { + RefinementError error = verify("ErrorCounterexampleReturnConstant.java"); + 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 + 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) { 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..5beb4df9e --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -0,0 +1,147 @@ +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("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("c", "-1"), pair("a", "-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("t", "-1"), pair("port", "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 omitsThePathConditionWhenFoundStatesEveryLinkedValue() { + RefinementError error = error("x > 1", vc("∀x:int. x == 1", "∀port:int. port > 0", "true"), "x=1", "port=1"); + 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 + 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()); + 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..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,5 +13,13 @@ void formatsVariables() { assertEquals("#fresh¹²", VariableFormatter.format("#fresh_12")); assertEquals("#ret³", VariableFormatter.format("#ret_3")); assertEquals("this#Class", VariableFormatter.format("this#Class")); + // 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()")); } }