Merge branch 'main' into diagnostics

rcosta358 · web-flow · commit 64bec447be69 · 2025-11-05T16:56:08.000Z
diff --git 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<E> {
     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
@@ -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);
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java 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<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);
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java 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<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
+}
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
@@ -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();
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
@@ -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();
diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/DummySemaphoreRefinements.java b/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;
+}
diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java b/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);
+	}
+}
diff --git 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/context/RefinedFunction.java b/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;
     }
 }
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
@@ -19,8 +19,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,11 +79,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);
@@ -139,17 +166,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;
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/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) {

Original file line number	Diff line number	Diff line change
`@@ -12,5 +12,5 @@ public interface ErrorExtRefNonExistentMethod<E> {`
`12`	`12`	`public void ArrayList();`
`13`	`13`
`14`	`14`	`@StateRefinement(to = "size(this) == (size(old(this)) + 1)")`
`15`		`- public void adddd(E e);`
	`15`	`+ public boolean adddd(E e);`
`16`	`16`	`}`