From 61f80dfe627978225d0bf7472336ac99812c14dc Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 4 Nov 2025 13:47:46 +0000 Subject: [PATCH] Add Signature to Refined Function (Codex) --- .../DummySemaphoreRefinements.java | 12 +++++++ .../TestMethodOverloadEror.java | 10 ++++++ .../processor/context/RefinedFunction.java | 21 +++++++++-- .../MethodsFunctionsChecker.java | 36 ++++++++++++++++--- 4 files changed, 72 insertions(+), 7 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/method_overload_error/DummySemaphoreRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/method_overload_error/TestMethodOverloadEror.java 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 new file mode 100644 index 00000000..c056dec9 --- /dev/null +++ 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; +} \ No newline at end of file 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 new file mode 100644 index 00000000..b977c1b0 --- /dev/null +++ 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); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java index 7b70f473..807f4682 100644 --- 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 argRefinements; private String targetClass; private List 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 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/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 84bf9672..4c35c931 100644 --- 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 void getMethodRefinements(CtMethod 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 void getMethodRefinements(CtMethod 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 void getInvocationRefinements(CtInvocation 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 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 map = mapInvocation(arguments, f); if (target != null) {