Skip to content

Commit 848eeb5

Browse files
CatarinaGamboaCopilotrcosta358
authored
Logic for method overload with different types (#172)
* add logic for method overload with different types * Update liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/ThrowableRefinements.java Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> * Update liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> * Reviewed Changes --------- Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> Co-authored-by: Ricardo Costa <rcosta.ms358@gmail.com>
1 parent 5430ba1 commit 848eeb5

File tree

7 files changed

+128
-26
lines changed

7 files changed

+128
-26
lines changed

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
package testSuite.classes.overload_constructors_correct;
2+
3+
public class Test{
4+
void test3(){
5+
Throwable t = new Throwable("Example");
6+
t.initCause(null);
7+
t.getCause();
8+
}
9+
10+
void test4(){
11+
Throwable originT = new Throwable();
12+
Throwable t = new Throwable(originT);
13+
t.getCause();
14+
}
15+
16+
}

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
package testSuite.classes.overload_constructors_correct;
2+
3+
import liquidjava.specification.StateSet;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
7+
@StateSet({"start", "hasMessage", "hasCause"})
8+
@ExternalRefinementsFor("java.lang.Throwable")
9+
public interface ThrowableRefinements {
10+
11+
// ##### Constructors #######
12+
@StateRefinement(to="hasMessage(this)")
13+
public void Throwable(String message);
14+
15+
@StateRefinement(to="hasCause(this)")
16+
public void Throwable(Throwable cause);
17+
18+
@StateRefinement(from="!hasCause(this)", to="hasCause(this)")
19+
public Throwable initCause(Throwable cause);
20+
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
State Refinement Error

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite.classes.overload_constructors_error;
2+
3+
public class Test{
4+
void test3(){
5+
Throwable t = new Throwable("Example");
6+
t.initCause(null);
7+
t.getCause();
8+
}
9+
10+
void test4(){
11+
Throwable originT = new Throwable();
12+
Throwable t = new Throwable(originT);
13+
t.initCause(null);// should be an error but its not
14+
t.getCause();
15+
}
16+
17+
}

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
package testSuite.classes.overload_constructors_error;
2+
3+
import liquidjava.specification.StateSet;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
7+
@StateSet({"start", "hasMessage", "hasCause"})
8+
@ExternalRefinementsFor("java.lang.Throwable")
9+
public interface ThrowableRefinements {
10+
11+
// ##### Constructors #######
12+
@StateRefinement(to="hasMessage(this)")
13+
public void Throwable(String message);
14+
15+
@StateRefinement(to="hasCause(this)")
16+
public void Throwable(Throwable cause);
17+
18+
@StateRefinement(from="!hasCause(this)", to="hasCause(this)")
19+
public Throwable initCause(Throwable cause);
20+
}

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -300,6 +300,29 @@ public RefinedFunction getFunction(String name, String target, int size) {
300300
return null;
301301
}
302302

303+
public RefinedFunction getFunction(String name, String target, List<CtTypeReference<?>> paramTypes) {
304+
for (RefinedFunction fi : ctxFunctions) {
305+
if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target)
306+
&& argumentTypesMatch(fi.getArguments(), paramTypes))
307+
return fi;
308+
}
309+
return getFunction(name, target, paramTypes.size());
310+
}
311+
312+
private boolean argumentTypesMatch(List<Variable> args, List<CtTypeReference<?>> paramTypes) {
313+
if (args.size() != paramTypes.size())
314+
return false;
315+
for (int i = 0; i < args.size(); i++) {
316+
CtTypeReference<?> argType = args.get(i).getType();
317+
CtTypeReference<?> paramType = paramTypes.get(i);
318+
if (argType == null || paramType == null)
319+
return false;
320+
if (!argType.getQualifiedName().equals(paramType.getQualifiedName()))
321+
return false;
322+
}
323+
return true;
324+
}
325+
303326
public List<RefinedFunction> getAllMethodsWithNameSize(String name, int size) {
304327
List<RefinedFunction> l = new ArrayList<>();
305328
for (RefinedFunction fi : ctxFunctions) {

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

Lines changed: 31 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package liquidjava.processor.refinement_checker.general_checkers;
22

3+
import java.util.ArrayList;
34
import java.util.HashMap;
45
import java.util.List;
56
import java.util.Map;
@@ -60,12 +61,13 @@ public void getConstructorRefinements(CtConstructor<?> c) throws LJError {
6061
public void getConstructorInvocationRefinements(CtConstructorCall<?> ctConstructorCall) throws LJError {
6162
CtExecutableReference<?> exe = ctConstructorCall.getExecutable();
6263
if (exe != null) {
64+
List<CtTypeReference<?>> paramTypes = exe.getParameters();
6365
RefinedFunction f = rtc.getContext().getFunction(exe.getSimpleName(),
64-
exe.getDeclaringType().getQualifiedName(), ctConstructorCall.getArguments().size());
66+
exe.getDeclaringType().getQualifiedName(), paramTypes);
6567
if (f != null) {
6668
Map<String, String> map = checkInvocationRefinements(ctConstructorCall,
6769
ctConstructorCall.getArguments(), ctConstructorCall.getTarget(), f.getName(),
68-
f.getTargetClass());
70+
f.getTargetClass(), paramTypes);
6971
AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall);
7072
}
7173
}
@@ -220,22 +222,15 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJEr
220222

221223
} else if (method.getParent() instanceof CtClass) {
222224
String ctype = ((CtClass<?>) method.getParent()).getQualifiedName();
223-
int argSize = invocation.getArguments().size();
224-
RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, argSize);
225+
List<CtTypeReference<?>> paramTypes = invocation.getExecutable().getParameters();
226+
RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, paramTypes);
225227
if (f != null) { // inside rtc.context
226228
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
227-
method.getSimpleName(), ctype);
229+
method.getSimpleName(), ctype, paramTypes);
228230
}
229231
}
230232
}
231233

232-
public RefinedFunction getRefinementFunction(String methodName, String className, int size) {
233-
RefinedFunction f = rtc.getContext().getFunction(methodName, className, size);
234-
if (f == null)
235-
f = rtc.getContext().getFunction(String.format("%s.%s", className, methodName), className, size);
236-
return f;
237-
}
238-
239234
private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?> invocation) throws LJError {
240235
CtTypeReference<?> ctref = ctr.getDeclaringType();
241236
if (ctref == null) {
@@ -246,39 +241,47 @@ private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?>
246241
String ctype = (ctref != null) ? ctref.toString() : null;
247242

248243
String name = ctr.getSimpleName(); // missing
249-
int argSize = invocation.getArguments().size();
244+
List<CtTypeReference<?>> paramTypes = ctr.getParameters();
250245
String qualifiedSignature = null;
251246
if (ctype != null) {
252247
qualifiedSignature = String.format("%s.%s", ctype, ctr.getSignature());
253-
if (rtc.getContext().getFunction(qualifiedSignature, ctype, argSize) != null) {
248+
RefinedFunction f = rtc.getContext().getFunction(qualifiedSignature, ctype, paramTypes);
249+
if (f != null) {
254250
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
255-
qualifiedSignature, ctype);
251+
qualifiedSignature, ctype, paramTypes);
256252
return;
257253
}
258254
}
259255
String signature = ctr.getSignature();
260-
if (rtc.getContext().getFunction(signature, ctype, argSize) != null) {
261-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype);
256+
RefinedFunction f = rtc.getContext().getFunction(signature, ctype, paramTypes);
257+
if (f != null) {
258+
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype,
259+
paramTypes);
262260
return;
263261
}
264-
if (rtc.getContext().getFunction(name, ctype, argSize) != null) { // inside rtc.context
265-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype);
262+
f = rtc.getContext().getFunction(name, ctype, paramTypes);
263+
if (f != null) { // inside rtc.context
264+
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype,
265+
paramTypes);
266266
return;
267267
}
268268
if (qualifiedSignature != null) {
269269
String completeName = String.format("%s.%s", ctype, name);
270-
if (rtc.getContext().getFunction(completeName, ctype, argSize) != null) {
270+
f = rtc.getContext().getFunction(completeName, ctype, paramTypes);
271+
if (f != null) {
271272
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName,
272-
ctype);
273+
ctype, paramTypes);
273274
}
274275
}
275276
}
276277

277278
private Map<String, String> checkInvocationRefinements(CtElement invocation, List<CtExpression<?>> arguments,
278-
CtExpression<?> target, String methodName, String className) throws LJError {
279+
CtExpression<?> target, String methodName, String className, List<CtTypeReference<?>> paramTypes)
280+
throws LJError {
279281
// -- Part 1: Check if the invocation is possible
280-
int si = arguments.size();
281-
RefinedFunction f = rtc.getContext().getFunction(methodName, className, si);
282+
RefinedFunction f = null;
283+
if (paramTypes != null)
284+
f = rtc.getContext().getFunction(methodName, className, paramTypes);
282285
if (f == null)
283286
return new HashMap<>();
284287
Map<String, String> map = mapInvocation(arguments, f);
@@ -407,8 +410,10 @@ public void loadFunctionInfo(CtExecutable<?> method) {
407410
className = ((CtInterface<?>) method.getParent()).getQualifiedName();
408411
}
409412
if (className != null) {
410-
RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className,
411-
method.getParameters().size());
413+
List<CtTypeReference<?>> paramTypes = new ArrayList<>();
414+
for (CtParameter<?> p : method.getParameters())
415+
paramTypes.add(p.getType());
416+
RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), className, paramTypes);
412417
if (fi != null) {
413418
List<Variable> lv = fi.getArguments();
414419
for (Variable v : lv)

0 commit comments

Comments
 (0)