From 8e8ed29cdf11da271829f1c4eae5a1d37f3aac63 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Wed, 30 Sep 2026 21:57:59 +0100 Subject: [PATCH 1/2] Treat results of methods without refinements as unconstrained in operations Fixes the crash when an invocation of a method with no refinements is an operand of a binary operation (#300). Co-Authored-By: Claude Opus 5.5 --- .../CorrectUnknownMethodInComparison.java | 23 +++++++++++++++++++ .../ErrorUnknownMethodInOperation.java | 12 ++++++++++ .../general_checkers/OperationsChecker.java | 14 +++++++++++ 3 files changed, 49 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java new file mode 100644 index 00000000..905d8f91 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java @@ -0,0 +1,23 @@ +package testSuite; + +import java.util.List; + +// Results of methods without refinements can be used in operations (issue #300) +@SuppressWarnings("unused") +public class CorrectUnknownMethodInComparison { + public void lengthInComparison(String s) { + if (s.length() < 3) { + System.out.println("short"); + } + } + + public void equalsInDisjunction(String s) { + boolean known = s.equals("a") || s.equals("b"); + } + + public void sizeInLoopBound(List list) { + for (int i = 0; i < list.size(); i++) { + System.out.println(list.get(i)); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java new file mode 100644 index 00000000..177dab74 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java @@ -0,0 +1,12 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// Results of methods without refinements carry no information (issue #300) +@SuppressWarnings("unused") +public class ErrorUnknownMethodInOperation { + public void lengthPlusOne(String s) { + @Refinement("_ > 0") + int x = s.length() + 1; // Expect: Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index b07a06c6..1c244119 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -253,6 +253,8 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // Get function refinements with non_used variables String met = ((CtClass) method.getParent()).getQualifiedName(); // TODO check RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size()); + if (fi == null) + return getUnconstrainedInvocationVariable(inv); Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! // Substitute _ by the variable that we send @@ -265,6 +267,16 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // TODO Maybe add cases } + /** + * Creates a fresh variable with no information (refinement true) to represent the result of an invocation of a + * method without refinements + */ + private Predicate getUnconstrainedInvocationVariable(CtInvocation inv) { + String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + rtc.getContext().addVarToContext(newName, inv.getType(), new Predicate(), inv); + return new Predicate(newName, inv); + } + private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) throws LJError { CtExpression t = inv.getTarget(); @@ -279,6 +291,8 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) thr String methodInClassName = typeNotParametrized + "." + simpleName; RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized, inv.getArguments().size()); + if (fi == null) + return getUnconstrainedInvocationVariable(inv); Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! // Substitute _ by the variable that we send From b7ad615333c6f2453bf2349294d23221f0caecb1 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Wed, 30 Sep 2026 23:30:05 +0100 Subject: [PATCH 2/2] Handle unknown invocations on non-variable targets and interface methods Invocations whose target is not a variable (chained or static calls such as s.trim().length() or Math.max(a, b)) used as operands now also get an unconstrained fresh variable instead of `true`, which crashed Z3 with a BoolExpr/ArithExpr cast. Methods declared in interfaces no longer crash with a ClassCastException when looking up the declaring type. Add negative tests mirroring the positive ones, including branch conditions over unknown method results and typestate preservation. Co-Authored-By: Claude Opus 5.5 --- .../CorrectUnknownMethodInComparison.java | 59 ++++++++++++- ...CorrectUnknownMethodInComparisonState.java | 26 ++++++ .../ErrorUnknownMethodInComparison.java | 85 +++++++++++++++++++ .../ErrorUnknownMethodInComparisonState.java | 27 ++++++ .../general_checkers/OperationsChecker.java | 6 +- 5 files changed, 199 insertions(+), 4 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparisonState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparison.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparisonState.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java index 905d8f91..4338abdb 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java @@ -1,13 +1,28 @@ package testSuite; import java.util.List; +import java.util.Map; + +import liquidjava.specification.Refinement; // Results of methods without refinements can be used in operations (issue #300) @SuppressWarnings("unused") public class CorrectUnknownMethodInComparison { + interface Shape { + int area(); + } + + int helper() { + return 1; + } + public void lengthInComparison(String s) { if (s.length() < 3) { - System.out.println("short"); + @Refinement("_ > 0") + int y = 1; + } else { + @Refinement("_ > 0") + int z = 1; } } @@ -20,4 +35,46 @@ public void sizeInLoopBound(List list) { System.out.println(list.get(i)); } } + + public void boxedResult(List list) { + if (list.get(0) > 3) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void booleanResultInConjunction(Map map, String k, int n) { + if (map.containsKey(k) && n > 0) { + @Refinement("_ > 0") + int y = n; + } + } + + public void staticCall(int a, int b) { + if (Math.max(a, b) > 0) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void chainedCall(String s) { + if (s.trim().length() > 0) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void implicitThisCall() { + if (helper() > 0) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void interfaceMethod(Shape shape) { + if (shape.area() > 0) { + @Refinement("_ > 0") + int y = 1; + } + } } diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparisonState.java b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparisonState.java new file mode 100644 index 00000000..5733c9d1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparisonState.java @@ -0,0 +1,26 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Calling a method without refinements in a condition keeps the object's state (issue #300) +@StateSet({"open", "closed"}) +public class CorrectUnknownMethodInComparisonState { + @StateRefinement(to = "open(this)") + public CorrectUnknownMethodInComparisonState() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public int count() { + return 0; + } + + public static void main(String[] args) { + CorrectUnknownMethodInComparisonState r = new CorrectUnknownMethodInComparisonState(); + if (r.count() > 0) { + System.out.println("non-empty"); + } + r.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparison.java new file mode 100644 index 00000000..9fe0d440 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparison.java @@ -0,0 +1,85 @@ +package testSuite; + +import java.util.List; +import java.util.Map; + +import liquidjava.specification.Refinement; + +// Results of methods without refinements are unconstrained, so no branch is dead (issue #300) +@SuppressWarnings("unused") +public class ErrorUnknownMethodInComparison { + interface Shape { + int area(); + } + + int helper() { + return 1; + } + + public void thenBranch(String s) { + if (s.length() < 3) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void elseBranch(String s) { + if (s.length() < 3) { + } else { + @Refinement("_ > 0") + int z = -1; // Expect: Refinement Error + } + } + + public void equalsInDisjunction(String s) { + if (s.equals("a") || s.equals("b")) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void boxedResult(List list) { + if (list.get(0) > 3) { + } else { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void booleanResultInConjunction(Map map, String k, int n) { + if (map.containsKey(k) && n > 0) { + @Refinement("_ > 0") + int y = n - 1; // Expect: Refinement Error + } + } + + public void staticCall(int a, int b) { + if (Math.max(a, b) > 0) { + } else { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void chainedCall(String s) { + if (s.trim().length() > 0) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void implicitThisCall() { + if (helper() > 0) { + } else { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void interfaceMethod(Shape shape) { + if (shape.area() > 0) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparisonState.java b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparisonState.java new file mode 100644 index 00000000..0689f40a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparisonState.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Calling a method without refinements in a condition keeps the object's state (issue #300) +@StateSet({"open", "closed"}) +public class ErrorUnknownMethodInComparisonState { + @StateRefinement(to = "open(this)") + public ErrorUnknownMethodInComparisonState() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public int count() { + return 0; + } + + public static void main(String[] args) { + ErrorUnknownMethodInComparisonState r = new ErrorUnknownMethodInComparisonState(); + r.close(); + if (r.count() > 0) { + System.out.println("non-empty"); + } + r.close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 1c244119..35264189 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -37,9 +37,9 @@ import spoon.reflect.code.CtVariableWrite; import spoon.reflect.code.UnaryOperatorKind; import spoon.reflect.declaration.CtAnnotation; -import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtType; import spoon.reflect.declaration.ParentNotInitializedException; import spoon.reflect.reference.CtVariableReference; import spoon.support.reflect.code.CtIfImpl; @@ -251,7 +251,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab return getOperationRefinementFromExternalLib(inv); // Get function refinements with non_used variables - String met = ((CtClass) method.getParent()).getQualifiedName(); // TODO check + String met = method.getParent(CtType.class).getQualifiedName(); // TODO check RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size()); if (fi == null) return getUnconstrainedInvocationVariable(inv); @@ -310,7 +310,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) thr rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); return new Predicate(newName, inv); // Return variable that represents the invocation } - return new Predicate(); + return getUnconstrainedInvocationVariable(inv); } /**