From 1ac3ef74a0665fa6cd7d333ee3802f2130af7b2d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 20 Oct 2025 15:20:09 +0100 Subject: [PATCH] Fix Refined Method Overloading MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Márcio Caetano <153174341+rodrigomilisse@users.noreply.github.com> --- .../DummySemaphoreRefinements.java | 12 ++++++++++++ .../TestMethodOverloadCorrect.java | 10 ++++++++++ .../general_checkers/MethodsFunctionsChecker.java | 10 ++++++---- .../general_checkers/OperationsChecker.java | 5 +++-- 4 files changed, 31 insertions(+), 6 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/DummySemaphoreRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/TestMethodOverloadCorrect.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/DummySemaphoreRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/DummySemaphoreRefinements.java new file mode 100644 index 00000000..bd6c2fda --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/DummySemaphoreRefinements.java @@ -0,0 +1,12 @@ +package testSuite.classes.method_overload_correct; + +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_correct/TestMethodOverloadCorrect.java b/liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/TestMethodOverloadCorrect.java new file mode 100644 index 00000000..821af4fb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/TestMethodOverloadCorrect.java @@ -0,0 +1,10 @@ +package testSuite.classes.method_overload_correct; + +import java.util.concurrent.Semaphore; + +public class TestMethodOverloadCorrect { + 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/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 8b1806fd..51158e5d 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 @@ -191,7 +191,7 @@ public void getReturnRefinements(CtReturn ret) { return; if (method.getParent() instanceof CtClass) { RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), - ((CtClass) method.getParent()).getQualifiedName()); + ((CtClass) method.getParent()).getQualifiedName(), method.getParameters().size()); List lv = fi.getArguments(); for (Variable v : lv) { @@ -229,7 +229,8 @@ public void getInvocationRefinements(CtInvocation invocation) { } else if (method.getParent() instanceof CtClass) { String ctype = ((CtClass) method.getParent()).getQualifiedName(); - RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype); + int argSize = invocation.getArguments().size(); + RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, argSize); if (f != null) { // inside rtc.context checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), method.getSimpleName(), ctype); @@ -264,13 +265,14 @@ private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation String ctype = (ctref != null) ? ctref.toString() : null; String name = ctr.getSimpleName(); // missing - if (rtc.getContext().getFunction(name, ctype) != null) { // inside rtc.context + int argSize = invocation.getArguments().size(); + 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 (rtc.getContext().getFunction(completeName, ctype) != null) { + if (rtc.getContext().getFunction(completeName, ctype, argSize) != null) { checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName, ctype); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 3f31da92..94c6a830 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -249,7 +249,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // Get function refinements with non_used variables String met = ((CtClass) method.getParent()).getQualifiedName(); // TODO check - RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met); + RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size()); Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!! // Substitute _ by the variable that we send String newName = String.format(rtc.freshFormat, rtc.getContext().getCounter()); @@ -275,7 +275,8 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB int i = c.indexOf("<"); String typeNotParametrized = (i > 0) ? c.substring(0, i) : c; String methodInClassName = typeNotParametrized + "." + simpleName; - RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized); + RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized, + inv.getArguments().size()); Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!! // Substitute _ by the variable that we send