Fix Refined Method Overloading (#77)

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/method_overload_error/DummySemaphoreRefinements.java

@@ -0,0 +1,12 @@
+package testSuite.classes.method_overload_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+
+@ExternalRefinementsFor("java.util.concurrent.Semaphore")
+public interface DummySemaphoreRefinements {
+
+	public abstract void acquire();
+
+	public abstract void acquire(@Refinement("_ >= 0") int permits) throws InterruptedException;
+}

liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java

@@ -0,0 +1,10 @@
+package testSuite.classes.method_overload_error;
+
+import java.util.concurrent.Semaphore;
+
+public class TestMethodOverloadEror {
+	public static void main(String[] args) throws InterruptedException {
+		Semaphore sem = new Semaphore(1);
+		sem.acquire(-1);
+	}
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java

@@ -12,6 +12,7 @@ public class RefinedFunction extends Refined {
     private List<Variable> argRefinements;
     private String targetClass;
     private List<ObjectState> stateChange;
+    private String signature;
 
     public RefinedFunction() {
         argRefinements = new ArrayList<>();
@@ -47,6 +48,14 @@ public String getTargetClass() {
         return targetClass;
     }
 
+    public void setSignature(String signature) {
+        this.signature = signature;
+    }
+
+    public String getSignature() {
+        return signature;
+    }
+
     public Predicate getRenamedRefinements(Context c, CtElement element) {
         return getRenamedRefinements(getAllRefinements(), c, element);
     }
@@ -132,8 +141,8 @@ public List<Predicate> getToStates() {
 
     @Override
     public String toString() {
-        return "Function [name=" + super.getName() + ", argRefinements=" + argRefinements + ", refReturn="
-                + super.getRefinement() + ", targetClass=" + targetClass + "]";
+        return "Function [name=" + super.getName() + ", signature=" + signature + ", argRefinements=" + argRefinements
+                + ", refReturn=" + super.getRefinement() + ", targetClass=" + targetClass + "]";
     }
 
     @Override
@@ -142,6 +151,7 @@ public int hashCode() {
         int result = super.hashCode();
         result = prime * result + ((argRefinements == null) ? 0 : argRefinements.hashCode());
         result = prime * result + ((targetClass == null) ? 0 : targetClass.hashCode());
+        result = prime * result + ((signature == null) ? 0 : signature.hashCode());
         return result;
     }
 
@@ -157,13 +167,18 @@ public boolean equals(Object obj) {
         if (argRefinements == null) {
             if (other.argRefinements != null)
                 return false;
-        } else if (argRefinements.size() != other.argRefinements.size())
+        } else if (!argRefinements.equals(other.argRefinements))
             return false;
         if (targetClass == null) {
             if (other.targetClass != null)
                 return false;
         } else if (!targetClass.equals(other.targetClass))
             return false;
+        if (signature == null) {
+            if (other.signature != null)
+                return false;
+        } else if (!signature.equals(other.signature))
+            return false;
         return true;
     }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -51,6 +51,12 @@ public void getConstructorRefinements(CtConstructor<?> c) throws ParsingExceptio
         f.setType(c.getType());
         handleFunctionRefinements(f, c, c.getParameters());
         f.setRefReturn(new Predicate());
+        CtTypeReference<?> declaring = c.getDeclaringType() != null ? c.getDeclaringType().getReference() : null;
+        if (declaring != null) {
+            f.setSignature(String.format("%s.%s", declaring.getQualifiedName(), c.getSignature()));
+        } else {
+            f.setSignature(c.getSignature());
+        }
         if (c.getParent() instanceof CtClass) {
             CtClass<?> klass = (CtClass<?>) c.getParent();
             f.setClass(klass.getQualifiedName());
@@ -89,6 +95,11 @@ public <R> void getMethodRefinements(CtMethod<R> method) throws ParsingException
             CtInterface<?> inter = (CtInterface<?>) method.getParent();
             f.setClass(inter.getQualifiedName());
         }
+        String owner = f.getTargetClass();
+        if (owner != null)
+            f.setSignature(String.format("%s.%s", owner, method.getSignature()));
+        else
+            f.setSignature(method.getSignature());
         rtc.getContext().addFunctionToContext(f);
 
         auxGetMethodRefinements(method, f);
@@ -113,6 +124,7 @@ public <R> void getMethodRefinements(CtMethod<R> method, String prefix) throws P
         f.setType(method.getType());
         f.setRefReturn(new Predicate());
         f.setClass(prefix);
+        f.setSignature(String.format("%s.%s", prefix, method.getSignature()));
         rtc.getContext().addFunctionToContext(f);
         auxGetMethodRefinements(method, f);
 
@@ -251,7 +263,7 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) {
     public RefinedFunction getRefinementFunction(String methodName, String className, int size) {
         RefinedFunction f = rtc.getContext().getFunction(methodName, className, size);
         if (f == null)
-            f = rtc.getContext().getFunction(String.format("%s.%s", className, methodName), methodName, size);
+            f = rtc.getContext().getFunction(String.format("%s.%s", className, methodName), className, size);
         return f;
     }
 
@@ -266,12 +278,26 @@ private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?>
 
         String name = ctr.getSimpleName(); // missing
         int argSize = invocation.getArguments().size();
+        String qualifiedSignature = null;
+        if (ctype != null) {
+            qualifiedSignature = String.format("%s.%s", ctype, ctr.getSignature());
+            if (rtc.getContext().getFunction(qualifiedSignature, ctype, argSize) != null) {
+                checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
+                        qualifiedSignature, ctype);
+                return;
+            }
+        }
+        String signature = ctr.getSignature();
+        if (rtc.getContext().getFunction(signature, ctype, argSize) != null) {
+            checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype);
+            return;
+        }
         if (rtc.getContext().getFunction(name, ctype, argSize) != null) { // inside rtc.context
             checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype);
             return;
-        } else {
-            String prefix = ctype;
-            String completeName = String.format("%s.%s", prefix, name);
+        }
+        if (qualifiedSignature != null) {
+            String completeName = String.format("%s.%s", ctype, name);
             if (rtc.getContext().getFunction(completeName, ctype, argSize) != null) {
                 checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName,
                         ctype);
@@ -284,6 +310,8 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
         // -- Part 1: Check if the invocation is possible
         int si = arguments.size();
         RefinedFunction f = rtc.getContext().getFunction(methodName, className, si);
+        if (f == null)
+            return new HashMap<>();
         Map<String, String> map = mapInvocation(arguments, f);
 
         if (target != null) {