Skip to content

Commit beffa81

Browse files
CatarinaGamboaCatarinaGamboa
committed
add logic for method overload with different types
1 parent 5430ba1 commit beffa81

File tree

7 files changed

+157
-17
lines changed

7 files changed

+157
-17
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;
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;
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 null;
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: 60 additions & 17 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,16 @@ 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);
67+
if (f == null)
68+
f = rtc.getContext().getFunction(exe.getSimpleName(), exe.getDeclaringType().getQualifiedName(),
69+
ctConstructorCall.getArguments().size());
6570
if (f != null) {
6671
Map<String, String> map = checkInvocationRefinements(ctConstructorCall,
6772
ctConstructorCall.getArguments(), ctConstructorCall.getTarget(), f.getName(),
68-
f.getTargetClass());
73+
f.getTargetClass(), paramTypes);
6974
AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall);
7075
}
7176
}
@@ -220,11 +225,13 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) throws LJEr
220225

221226
} else if (method.getParent() instanceof CtClass) {
222227
String ctype = ((CtClass<?>) method.getParent()).getQualifiedName();
223-
int argSize = invocation.getArguments().size();
224-
RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, argSize);
228+
List<CtTypeReference<?>> paramTypes = invocation.getExecutable().getParameters();
229+
RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, paramTypes);
230+
if (f == null)
231+
f = rtc.getContext().getFunction(method.getSimpleName(), ctype, invocation.getArguments().size());
225232
if (f != null) { // inside rtc.context
226233
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
227-
method.getSimpleName(), ctype);
234+
method.getSimpleName(), ctype, paramTypes);
228235
}
229236
}
230237
}
@@ -236,6 +243,16 @@ public RefinedFunction getRefinementFunction(String methodName, String className
236243
return f;
237244
}
238245

246+
public RefinedFunction getRefinementFunction(String methodName, String className,
247+
List<CtTypeReference<?>> paramTypes) {
248+
RefinedFunction f = rtc.getContext().getFunction(methodName, className, paramTypes);
249+
if (f == null)
250+
f = rtc.getContext().getFunction(String.format("%s.%s", className, methodName), className, paramTypes);
251+
if (f == null)
252+
f = getRefinementFunction(methodName, className, paramTypes.size());
253+
return f;
254+
}
255+
239256
private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?> invocation) throws LJError {
240257
CtTypeReference<?> ctref = ctr.getDeclaringType();
241258
if (ctref == null) {
@@ -247,38 +264,62 @@ private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?>
247264

248265
String name = ctr.getSimpleName(); // missing
249266
int argSize = invocation.getArguments().size();
267+
List<CtTypeReference<?>> paramTypes = ctr.getParameters();
250268
String qualifiedSignature = null;
251269
if (ctype != null) {
252270
qualifiedSignature = String.format("%s.%s", ctype, ctr.getSignature());
253-
if (rtc.getContext().getFunction(qualifiedSignature, ctype, argSize) != null) {
271+
RefinedFunction f = rtc.getContext().getFunction(qualifiedSignature, ctype, paramTypes);
272+
if (f == null)
273+
f = rtc.getContext().getFunction(qualifiedSignature, ctype, argSize);
274+
if (f != null) {
254275
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
255-
qualifiedSignature, ctype);
276+
qualifiedSignature, ctype, paramTypes);
256277
return;
257278
}
258279
}
259280
String signature = ctr.getSignature();
260-
if (rtc.getContext().getFunction(signature, ctype, argSize) != null) {
261-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype);
281+
RefinedFunction f = rtc.getContext().getFunction(signature, ctype, paramTypes);
282+
if (f == null)
283+
f = rtc.getContext().getFunction(signature, ctype, argSize);
284+
if (f != null) {
285+
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype,
286+
paramTypes);
262287
return;
263288
}
264-
if (rtc.getContext().getFunction(name, ctype, argSize) != null) { // inside rtc.context
265-
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype);
289+
f = rtc.getContext().getFunction(name, ctype, paramTypes);
290+
if (f == null)
291+
f = rtc.getContext().getFunction(name, ctype, argSize);
292+
if (f != null) { // inside rtc.context
293+
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype,
294+
paramTypes);
266295
return;
267296
}
268297
if (qualifiedSignature != null) {
269298
String completeName = String.format("%s.%s", ctype, name);
270-
if (rtc.getContext().getFunction(completeName, ctype, argSize) != null) {
299+
f = rtc.getContext().getFunction(completeName, ctype, paramTypes);
300+
if (f == null)
301+
f = rtc.getContext().getFunction(completeName, ctype, argSize);
302+
if (f != null) {
271303
checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName,
272-
ctype);
304+
ctype, paramTypes);
273305
}
274306
}
275307
}
276308

277309
private Map<String, String> checkInvocationRefinements(CtElement invocation, List<CtExpression<?>> arguments,
278310
CtExpression<?> target, String methodName, String className) throws LJError {
311+
return checkInvocationRefinements(invocation, arguments, target, methodName, className, null);
312+
}
313+
314+
private Map<String, String> checkInvocationRefinements(CtElement invocation, List<CtExpression<?>> arguments,
315+
CtExpression<?> target, String methodName, String className, List<CtTypeReference<?>> paramTypes)
316+
throws LJError {
279317
// -- Part 1: Check if the invocation is possible
280-
int si = arguments.size();
281-
RefinedFunction f = rtc.getContext().getFunction(methodName, className, si);
318+
RefinedFunction f = null;
319+
if (paramTypes != null)
320+
f = rtc.getContext().getFunction(methodName, className, paramTypes);
321+
if (f == null)
322+
f = rtc.getContext().getFunction(methodName, className, arguments.size());
282323
if (f == null)
283324
return new HashMap<>();
284325
Map<String, String> map = mapInvocation(arguments, f);
@@ -407,8 +448,10 @@ public void loadFunctionInfo(CtExecutable<?> method) {
407448
className = ((CtInterface<?>) method.getParent()).getQualifiedName();
408449
}
409450
if (className != null) {
410-
RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className,
411-
method.getParameters().size());
451+
List<CtTypeReference<?>> paramTypes = new ArrayList<>();
452+
for (CtParameter<?> p : method.getParameters())
453+
paramTypes.add(p.getType());
454+
RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className, paramTypes);
412455
if (fi != null) {
413456
List<Variable> lv = fi.getArguments();
414457
for (Variable v : lv)

0 commit comments

Comments
 (0)