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 +} 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/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(); 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..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 @@ -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; @@ -18,8 +21,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; @@ -78,11 +81,38 @@ public void visitCtMethod(CtMethod method) { if (errorEmitter.foundError()) return; - if (!methodExists(method)) { - ErrorHandler.printCustomError(method, - "Could not find method '" + method.getSignature() + "' in class '" + 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)) { + String matchingNames = targetType.getMethods().stream() + .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("\nAvailable overloads:\n "); + sb.append(matchingNames); + } + ErrorHandler.printCustomError(method, sb.toString(), errorEmitter); + return; + } } + MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); try { mfc.getMethodRefinements(method, prefix); @@ -138,17 +168,42 @@ private boolean classExists(String className) { return factory.Type().createReference(className).getTypeDeclaration() != null; } - private boolean methodExists(CtMethod method) { - CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration(); + 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())); + } + + 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) { + 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; }