Check Method Signatures in External Refinements

liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java

@@ -12,5 +12,5 @@ public interface ErrorExtRefNonExistentMethod<E> {
     public void ArrayList();
 
     @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
-    public void adddd(E e);
+    public boolean adddd(E e);
 }

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<E> {
+
+    @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);
+}

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<E> {
+
+    @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);
+}

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<E> {
+
+    @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
+}

liquidjava-example/src/main/java/testSuite/classes/arraylist_correct/ArrayListRefinements.java

@@ -12,7 +12,7 @@ public interface ArrayListRefinements<E> {
     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();

liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java

@@ -11,7 +11,7 @@ public interface StackRefinements<E> {
 	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();

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);

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 <R> void visitCtMethod(CtMethod<R> 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;
     }