Logic for method overload with different types

liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/Test.java

@@ -0,0 +1,16 @@
+package testSuite.classes.overload_constructors_correct;
+
+public class Test{
+    void test3(){
+        Throwable t = new Throwable("Example");
+        t.initCause(null);
+        t.getCause();
+    }
+
+    void test4(){
+        Throwable originT = new Throwable();
+        Throwable t = new Throwable(originT); 
+        t.getCause();
+    }
+
+}

liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/ThrowableRefinements.java

@@ -0,0 +1,20 @@
+package testSuite.classes.overload_constructors_correct;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.ExternalRefinementsFor;
+
+@StateSet({"start", "hasMessage", "hasCause"})
+@ExternalRefinementsFor("java.lang.Throwable")
+public interface ThrowableRefinements {
+
+    // ##### Constructors #######
+    @StateRefinement(to="hasMessage(this)")
+    public void Throwable(String message);
+
+    @StateRefinement(to="hasCause(this)")
+    public void Throwable(Throwable cause);
+
+    @StateRefinement(from="!hasCause(this)", to="hasCause(this)")
+    public Throwable initCause(Throwable cause);
+}

liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected

@@ -0,0 +1 @@
+State Refinement Error

liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java

@@ -0,0 +1,17 @@
+package testSuite.classes.overload_constructors_error;
+
+public class Test{
+    void test3(){
+        Throwable t = new Throwable("Example");
+        t.initCause(null);
+        t.getCause();
+    }
+
+    void test4(){
+        Throwable originT = new Throwable();
+        Throwable t = new Throwable(originT); 
+        t.initCause(null);// should be an error but its not
+        t.getCause();
+    }
+
+}

liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/ThrowableRefinements.java

@@ -0,0 +1,20 @@
+package testSuite.classes.overload_constructors_error;
+
+import liquidjava.specification.StateSet;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.ExternalRefinementsFor;
+
+@StateSet({"start", "hasMessage", "hasCause"})
+@ExternalRefinementsFor("java.lang.Throwable")
+public interface ThrowableRefinements {
+
+    // ##### Constructors #######
+    @StateRefinement(to="hasMessage(this)")
+    public void Throwable(String message);
+
+    @StateRefinement(to="hasCause(this)")
+    public void Throwable(Throwable cause);
+
+    @StateRefinement(from="!hasCause(this)", to="hasCause(this)")
+    public Throwable initCause(Throwable cause);
+}

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

@@ -300,6 +300,29 @@ public RefinedFunction getFunction(String name, String target, int size) {
         return null;
     }
 
+    public RefinedFunction getFunction(String name, String target, List<CtTypeReference<?>> paramTypes) {
+        for (RefinedFunction fi : ctxFunctions) {
+            if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target)
+                    && argumentTypesMatch(fi.getArguments(), paramTypes))
+                return fi;
+        }
+        return null;
+    }
+
+    private boolean argumentTypesMatch(List<Variable> args, List<CtTypeReference<?>> paramTypes) {
+        if (args.size() != paramTypes.size())
+            return false;
+        for (int i = 0; i < args.size(); i++) {
+            CtTypeReference<?> argType = args.get(i).getType();
+            CtTypeReference<?> paramType = paramTypes.get(i);
+            if (argType == null || paramType == null)
+                return false;
+            if (!argType.getQualifiedName().equals(paramType.getQualifiedName()))
+                return false;
+        }
+        return true;
+    }
+
     public List<RefinedFunction> getAllMethodsWithNameSize(String name, int size) {
         List<RefinedFunction> l = new ArrayList<>();
         for (RefinedFunction fi : ctxFunctions) {

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

@@ -1,5 +1,6 @@
 package liquidjava.processor.refinement_checker.general_checkers;
 
+import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
@@ -60,12 +61,16 @@ public void getConstructorRefinements(CtConstructor<?> c) throws LJError {
     public void getConstructorInvocationRefinements(CtConstructorCall<?> ctConstructorCall) throws LJError {
         CtExecutableReference<?> exe = ctConstructorCall.getExecutable();
         if (exe != null) {
+            List<CtTypeReference<?>> paramTypes = exe.getParameters();
             RefinedFunction f = rtc.getContext().getFunction(exe.getSimpleName(),
-                    exe.getDeclaringType().getQualifiedName(), ctConstructorCall.getArguments().size());
+                    exe.getDeclaringType().getQualifiedName(), paramTypes);
+            if (f == null)
+                f = rtc.getContext().getFunction(exe.getSimpleName(), exe.getDeclaringType().getQualifiedName(),
+                        ctConstructorCall.getArguments().size());
             if (f != null) {
                 Map<String, String> map = checkInvocationRefinements(ctConstructorCall,
                         ctConstructorCall.getArguments(), ctConstructorCall.getTarget(), f.getName(),
-                        f.getTargetClass());
+                        f.getTargetClass(), paramTypes);
                 AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall);
             }
         }
@@ -220,11 +225,13 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJEr
 
         } else if (method.getParent() instanceof CtClass) {
             String ctype = ((CtClass<?>) method.getParent()).getQualifiedName();
-            int argSize = invocation.getArguments().size();
-            RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, argSize);
+            List<CtTypeReference<?>> paramTypes = invocation.getExecutable().getParameters();
+            RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, paramTypes);
+            if (f == null)
+                f = rtc.getContext().getFunction(method.getSimpleName(), ctype, invocation.getArguments().size());
             if (f != null) { // inside rtc.context
                 checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
-                        method.getSimpleName(), ctype);
+                        method.getSimpleName(), ctype, paramTypes);
             }
         }
     }
@@ -236,6 +243,16 @@ public RefinedFunction getRefinementFunction(String methodName, String className
         return f;
     }
 
+    public RefinedFunction getRefinementFunction(String methodName, String className,
+            List<CtTypeReference<?>> paramTypes) {
+        RefinedFunction f = rtc.getContext().getFunction(methodName, className, paramTypes);
+        if (f == null)
+            f = rtc.getContext().getFunction(String.format("%s.%s", className, methodName), className, paramTypes);
+        if (f == null)
+            f = getRefinementFunction(methodName, className, paramTypes.size());
+        return f;
+    }
+
     private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?> invocation) throws LJError {
         CtTypeReference<?> ctref = ctr.getDeclaringType();
         if (ctref == null) {
@@ -247,38 +264,62 @@ private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?>
 
         String name = ctr.getSimpleName(); // missing
         int argSize = invocation.getArguments().size();
+        List<CtTypeReference<?>> paramTypes = ctr.getParameters();
         String qualifiedSignature = null;
         if (ctype != null) {
             qualifiedSignature = String.format("%s.%s", ctype, ctr.getSignature());
-            if (rtc.getContext().getFunction(qualifiedSignature, ctype, argSize) != null) {
+            RefinedFunction f = rtc.getContext().getFunction(qualifiedSignature, ctype, paramTypes);
+            if (f == null)
+                f = rtc.getContext().getFunction(qualifiedSignature, ctype, argSize);
+            if (f != null) {
                 checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
-                        qualifiedSignature, ctype);
+                        qualifiedSignature, ctype, paramTypes);
                 return;
             }
         }
         String signature = ctr.getSignature();
-        if (rtc.getContext().getFunction(signature, ctype, argSize) != null) {
-            checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype);
+        RefinedFunction f = rtc.getContext().getFunction(signature, ctype, paramTypes);
+        if (f == null)
+            f = rtc.getContext().getFunction(signature, ctype, argSize);
+        if (f != null) {
+            checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype,
+                    paramTypes);
             return;
         }
-        if (rtc.getContext().getFunction(name, ctype, argSize) != null) { // inside rtc.context
-            checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype);
+        f = rtc.getContext().getFunction(name, ctype, paramTypes);
+        if (f == null)
+            f = rtc.getContext().getFunction(name, ctype, argSize);
+        if (f != null) { // inside rtc.context
+            checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype,
+                    paramTypes);
             return;
         }
         if (qualifiedSignature != null) {
             String completeName = String.format("%s.%s", ctype, name);
-            if (rtc.getContext().getFunction(completeName, ctype, argSize) != null) {
+            f = rtc.getContext().getFunction(completeName, ctype, paramTypes);
+            if (f == null)
+                f = rtc.getContext().getFunction(completeName, ctype, argSize);
+            if (f != null) {
                 checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName,
-                        ctype);
+                        ctype, paramTypes);
             }
         }
     }
 
     private Map<String, String> checkInvocationRefinements(CtElement invocation, List<CtExpression<?>> arguments,
             CtExpression<?> target, String methodName, String className) throws LJError {
+        return checkInvocationRefinements(invocation, arguments, target, methodName, className, null);
+    }
+
+    private Map<String, String> checkInvocationRefinements(CtElement invocation, List<CtExpression<?>> arguments,
+            CtExpression<?> target, String methodName, String className, List<CtTypeReference<?>> paramTypes)
+            throws LJError {
         // -- Part 1: Check if the invocation is possible
-        int si = arguments.size();
-        RefinedFunction f = rtc.getContext().getFunction(methodName, className, si);
+        RefinedFunction f = null;
+        if (paramTypes != null)
+            f = rtc.getContext().getFunction(methodName, className, paramTypes);
+        if (f == null)
+            f = rtc.getContext().getFunction(methodName, className, arguments.size());
         if (f == null)
             return new HashMap<>();
         Map<String, String> map = mapInvocation(arguments, f);
@@ -407,8 +448,10 @@ public void loadFunctionInfo(CtExecutable<?> method) {
             className = ((CtInterface<?>) method.getParent()).getQualifiedName();
         }
         if (className != null) {
-            RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className,
-                    method.getParameters().size());
+            List<CtTypeReference<?>> paramTypes = new ArrayList<>();
+            for (CtParameter<?> p : method.getParameters())
+                paramTypes.add(p.getType());
+            RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className, paramTypes);
             if (fi != null) {
                 List<Variable> lv = fi.getArguments();
                 for (Variable v : lv)