From 290450d9132c2727888de01142eec170e8f379b0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 4 Nov 2025 11:33:05 +0000 Subject: [PATCH 1/6] Check Method Signatures in External Refinements --- .../ArrayListRefinements.java | 2 +- .../correctInvocation/MathRefinements.java | 10 ++-- .../ExternalRefinementTypeChecker.java | 52 +++++++++++++++---- 3 files changed, 48 insertions(+), 16 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java index fc094999..260a8297 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java @@ -12,7 +12,7 @@ public interface ArrayListRefinements { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public void add(E e); + public boolean add(E e); // @Refinement("size(_) == size(this)") // public Object clone(); diff --git a/liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java b/liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java index 95577d65..b2798a66 100644 --- a/liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/math/correctInvocation/MathRefinements.java @@ -16,13 +16,13 @@ public interface MathRefinements { public int abs(int arg0); @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(long arg0); + public long abs(long arg0); @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(float arg0); + public float abs(float arg0); @Refinement("(arg0 > 0)?( _ == arg0):(_ == -arg0)") - public int abs(double arg0); + public double abs(double arg0); @Refinement(" _ == a+b") public int addExact(int a, int b); @@ -43,13 +43,13 @@ public interface MathRefinements { public int decrementExact(int a); @Refinement("_ == (a-1)") - public int decrementExact(long a); + public long decrementExact(long a); @Refinement("_ == (a+1)") public int incrementExact(int a); @Refinement("_ == (a+1)") - public int incrementExact(long a); + public long incrementExact(long a); @Refinement("(a > b)? (_ == a):(_ == b)") public int max(int a, int b); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index ae41e0d6..7af0f33b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -18,8 +18,8 @@ import spoon.reflect.declaration.CtField; import spoon.reflect.declaration.CtInterface; import spoon.reflect.declaration.CtMethod; +import spoon.reflect.declaration.CtParameter; import spoon.reflect.declaration.CtType; -import spoon.reflect.declaration.CtTypeParameter; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; @@ -79,8 +79,8 @@ public void visitCtMethod(CtMethod method) { return; if (!methodExists(method)) { - ErrorHandler.printCustomError(method, - "Could not find method '" + method.getSignature() + "' in class '" + prefix + "'", errorEmitter); + ErrorHandler.printCustomError(method, String.format("Could not find method '%s %s' in class '%s'", + method.getType().getSimpleName(), method.getSignature(), prefix), errorEmitter); return; } MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); @@ -140,15 +140,47 @@ private boolean classExists(String className) { private boolean methodExists(CtMethod method) { CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration(); + if (targetType == null) + return false; + + String methodName = method.getSimpleName(); + boolean isConstructor = methodName.equals(targetType.getSimpleName()); + + if (isConstructor && targetType instanceof CtClass) { + // find constructor with matching signature + CtClass targetClass = (CtClass) targetType; + return targetClass.getConstructors().stream() + .anyMatch(c -> parametersMatch(c.getParameters(), method.getParameters())); + } else { + // find method with matching signature + return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(methodName)) + .anyMatch(m -> parametersMatch(m.getParameters(), method.getParameters()) + && typesMatch(m.getType(), method.getType())); + } + } + + private boolean typesMatch(CtTypeReference type1, CtTypeReference type2) { + if (type1 == null && type2 == null) + return true; + + if (type1 == null || type2 == null) + return false; + + return type1.getQualifiedName().equals(type2.getQualifiedName()); + } + + private boolean parametersMatch(List targetParams, List refinementParams) { + if (targetParams.size() != refinementParams.size()) + return false; - // find a method with matching name and parameter count - boolean methodFound = targetType.getMethods().stream() - .anyMatch(m -> m.getSimpleName().equals(method.getSimpleName()) - && m.getParameters().size() == method.getParameters().size()); + for (int i = 0; i < targetParams.size(); i++) { + CtParameter targetParam = (CtParameter) targetParams.get(i); + CtParameter refinementParam = (CtParameter) refinementParams.get(i); + if (targetParam == null || refinementParam == null) + return false; - if (!methodFound) { - // check if constructor method - return method.getSimpleName().equals(targetType.getSimpleName()); + if (!typesMatch(targetParam.getType(), refinementParam.getType())) + return false; } return true; } From 23d1ffde41250e6eb318fa57118f673c9dfc7867 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 4 Nov 2025 11:39:02 +0000 Subject: [PATCH 2/6] Add Tests --- .../testSuite/ErrorExtRefNonExistentMethod.java | 2 +- .../testSuite/ErrorExtRefWrongConstructor.java | 16 ++++++++++++++++ .../testSuite/ErrorExtRefWrongParameterType.java | 16 ++++++++++++++++ .../java/testSuite/ErrorExtRefWrongRetType.java | 16 ++++++++++++++++ 4 files changed, 49 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java index ac3db0d0..78b1c8c9 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java @@ -12,5 +12,5 @@ public interface ErrorExtRefNonExistentMethod { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public void adddd(E e); + public boolean adddd(E e); } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java b/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java new file mode 100644 index 00000000..636d3adb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.RefinementPredicate; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +public interface ErrorExtRefWrongConstructor { + + @RefinementPredicate("int size(ArrayList l)") + @StateRefinement(to = "size(this) == 0") + public void ArrayList(String wrongParameter); + + @StateRefinement(to = "size(this) == (size(old(this)) + 1)") + public boolean add(E e); +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java b/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java new file mode 100644 index 00000000..da2135c5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.RefinementPredicate; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +public interface ErrorExtRefWrongParameterType { + + @RefinementPredicate("int size(ArrayList l)") + @StateRefinement(to = "size(this) == 0") + public void ArrayList(); + + @StateRefinement(to = "size(this) == (size(old(this)) + 1)") + public boolean add(int wrongParameter); +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java b/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java new file mode 100644 index 00000000..48509080 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.RefinementPredicate; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +public interface ErrorExtRefWrongRetType { + + @RefinementPredicate("int size(ArrayList l)") + @StateRefinement(to = "size(this) == 0") + public void ArrayList(); + + @StateRefinement(to = "size(this) == (size(old(this)) + 1)") + public int add(E e); // wrong return type +} From 702fe1708d651c20ea210fbee2ab7b1e827b61f2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 4 Nov 2025 11:44:32 +0000 Subject: [PATCH 3/6] Separate Method and Constructor Existence Checks --- .../ExternalRefinementTypeChecker.java | 50 +++++++++++-------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 7af0f33b..9bcc0043 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -78,11 +78,26 @@ public void visitCtMethod(CtMethod method) { if (errorEmitter.foundError()) return; - if (!methodExists(method)) { - ErrorHandler.printCustomError(method, String.format("Could not find method '%s %s' in class '%s'", - method.getType().getSimpleName(), method.getSignature(), prefix), errorEmitter); + CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration(); + if (targetType == null || !(targetType instanceof CtClass)) return; + + boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName()); + if (isConstructor) { + if (!constructorExists(targetType, method)) { + ErrorHandler.printCustomError(method, + String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix), + errorEmitter); + return; + } + } else { + if (!methodExists(targetType, method)) { + ErrorHandler.printCustomError(method, String.format("Could not find method '%s %s' for '%s'", + method.getType().getSimpleName(), method.getSignature(), prefix), errorEmitter); + return; + } } + MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); try { mfc.getMethodRefinements(method, prefix); @@ -138,25 +153,18 @@ private boolean classExists(String className) { return factory.Type().createReference(className).getTypeDeclaration() != null; } - private boolean methodExists(CtMethod method) { - CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration(); - if (targetType == null) - return false; - - String methodName = method.getSimpleName(); - boolean isConstructor = methodName.equals(targetType.getSimpleName()); + private boolean methodExists(CtType targetType, CtMethod method) { + // find method with matching signature + return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName())) + .anyMatch(m -> parametersMatch(m.getParameters(), method.getParameters()) + && typesMatch(m.getType(), method.getType())); + } - if (isConstructor && targetType instanceof CtClass) { - // find constructor with matching signature - CtClass targetClass = (CtClass) targetType; - return targetClass.getConstructors().stream() - .anyMatch(c -> parametersMatch(c.getParameters(), method.getParameters())); - } else { - // find method with matching signature - return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(methodName)) - .anyMatch(m -> parametersMatch(m.getParameters(), method.getParameters()) - && typesMatch(m.getType(), method.getType())); - } + private boolean constructorExists(CtType targetType, CtMethod method) { + // find constructor with matching signature + CtClass targetClass = (CtClass) targetType; + return targetClass.getConstructors().stream() + .anyMatch(c -> parametersMatch(c.getParameters(), method.getParameters())); } private boolean typesMatch(CtTypeReference type1, CtTypeReference type2) { From d81f0ecaa262af234803614dd74453d90ce78686 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 4 Nov 2025 11:54:09 +0000 Subject: [PATCH 4/6] Improve Error Message For Missing Method --- .../ExternalRefinementTypeChecker.java | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 9bcc0043..49ad4c58 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -3,6 +3,9 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; +import java.util.stream.Collectors; +import java.util.stream.Stream; + import liquidjava.errors.ErrorEmitter; import liquidjava.errors.ErrorHandler; import liquidjava.processor.context.Context; @@ -92,8 +95,19 @@ public void visitCtMethod(CtMethod method) { } } else { if (!methodExists(targetType, method)) { - ErrorHandler.printCustomError(method, String.format("Could not find method '%s %s' for '%s'", - method.getType().getSimpleName(), method.getSignature(), prefix), errorEmitter); + String matchingNames = targetType.getMethods().stream() + .filter(m -> m.getSimpleName().equals(method.getSimpleName())).map(m -> m.getSignature()) + .collect(Collectors.joining("\n\t")); + + StringBuilder sb = new StringBuilder(); + sb.append(String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), + method.getSignature(), prefix)); + + if (!matchingNames.isEmpty()) { + sb.append("\nPossible matches:\n\t"); + sb.append(matchingNames); + } + ErrorHandler.printCustomError(method, sb.toString(), errorEmitter); return; } } From fcceb9edf40fc908ce90155978eb9734d177b625 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 4 Nov 2025 19:44:31 +0000 Subject: [PATCH 5/6] Minor Improvement --- .../refinement_checker/ExternalRefinementTypeChecker.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 49ad4c58..111ee2de 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -96,15 +96,16 @@ public void visitCtMethod(CtMethod method) { } else { if (!methodExists(targetType, method)) { String matchingNames = targetType.getMethods().stream() - .filter(m -> m.getSimpleName().equals(method.getSimpleName())).map(m -> m.getSignature()) - .collect(Collectors.joining("\n\t")); + .filter(m -> m.getSimpleName().equals(method.getSimpleName())) + .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature())) + .collect(Collectors.joining("\n ")); StringBuilder sb = new StringBuilder(); sb.append(String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), method.getSignature(), prefix)); if (!matchingNames.isEmpty()) { - sb.append("\nPossible matches:\n\t"); + sb.append("\nAvailable overloads:\n "); sb.append(matchingNames); } ErrorHandler.printCustomError(method, sb.toString(), errorEmitter); From d15649f7a9f923f90733a97e5dd1cff8f014e890 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 4 Nov 2025 20:17:07 +0000 Subject: [PATCH 6/6] Fix Test --- .../conflicting_ghost_names_correct/StackRefinements.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java index 155d844b..f94b5d02 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java @@ -11,7 +11,7 @@ public interface StackRefinements { public void Stack(); @StateRefinement(to="size(this) == size(old(this)) + 1") - public boolean push(E elem); + public E push(E elem); @StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1") public E pop();