diff --git a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/Test.java new file mode 100644 index 00000000..76be7caf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/Test.java @@ -0,0 +1,16 @@ +package testSuite.classes.overload_constructors_correct; + +public class Test{ + void test3(){ + Throwable t = new Throwable("Example"); + t.initCause(null); + t.getCause(); + } + + void test4(){ + Throwable originT = new Throwable(); + Throwable t = new Throwable(originT); + t.getCause(); + } + +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/ThrowableRefinements.java new file mode 100644 index 00000000..df0e4260 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/ThrowableRefinements.java @@ -0,0 +1,20 @@ +package testSuite.classes.overload_constructors_correct; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"start", "hasMessage", "hasCause"}) +@ExternalRefinementsFor("java.lang.Throwable") +public interface ThrowableRefinements { + + // ##### Constructors ####### + @StateRefinement(to="hasMessage(this)") + public void Throwable(String message); + + @StateRefinement(to="hasCause(this)") + public void Throwable(Throwable cause); + + @StateRefinement(from="!hasCause(this)", to="hasCause(this)") + public Throwable initCause(Throwable cause); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected new file mode 100644 index 00000000..49d2a05a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected @@ -0,0 +1 @@ +State Refinement Error diff --git a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java new file mode 100644 index 00000000..407c23a3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java @@ -0,0 +1,17 @@ +package testSuite.classes.overload_constructors_error; + +public class Test{ + void test3(){ + Throwable t = new Throwable("Example"); + t.initCause(null); + t.getCause(); + } + + void test4(){ + Throwable originT = new Throwable(); + Throwable t = new Throwable(originT); + t.initCause(null);// should be an error but its not + t.getCause(); + } + +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/ThrowableRefinements.java new file mode 100644 index 00000000..77c6bc69 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/ThrowableRefinements.java @@ -0,0 +1,20 @@ +package testSuite.classes.overload_constructors_error; + +import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.ExternalRefinementsFor; + +@StateSet({"start", "hasMessage", "hasCause"}) +@ExternalRefinementsFor("java.lang.Throwable") +public interface ThrowableRefinements { + + // ##### Constructors ####### + @StateRefinement(to="hasMessage(this)") + public void Throwable(String message); + + @StateRefinement(to="hasCause(this)") + public void Throwable(Throwable cause); + + @StateRefinement(from="!hasCause(this)", to="hasCause(this)") + public Throwable initCause(Throwable cause); +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 23176dfd..7979fcc0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -300,6 +300,29 @@ public RefinedFunction getFunction(String name, String target, int size) { return null; } + public RefinedFunction getFunction(String name, String target, List> paramTypes) { + for (RefinedFunction fi : ctxFunctions) { + if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target) + && argumentTypesMatch(fi.getArguments(), paramTypes)) + return fi; + } + return getFunction(name, target, paramTypes.size()); + } + + private boolean argumentTypesMatch(List args, List> paramTypes) { + if (args.size() != paramTypes.size()) + return false; + for (int i = 0; i < args.size(); i++) { + CtTypeReference argType = args.get(i).getType(); + CtTypeReference paramType = paramTypes.get(i); + if (argType == null || paramType == null) + return false; + if (!argType.getQualifiedName().equals(paramType.getQualifiedName())) + return false; + } + return true; + } + public List getAllMethodsWithNameSize(String name, int size) { List l = new ArrayList<>(); for (RefinedFunction fi : ctxFunctions) { 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 af16bf92..12628ab9 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 @@ -1,5 +1,6 @@ package liquidjava.processor.refinement_checker.general_checkers; +import java.util.ArrayList; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -60,12 +61,13 @@ public void getConstructorRefinements(CtConstructor c) throws LJError { public void getConstructorInvocationRefinements(CtConstructorCall ctConstructorCall) throws LJError { CtExecutableReference exe = ctConstructorCall.getExecutable(); if (exe != null) { + List> paramTypes = exe.getParameters(); RefinedFunction f = rtc.getContext().getFunction(exe.getSimpleName(), - exe.getDeclaringType().getQualifiedName(), ctConstructorCall.getArguments().size()); + exe.getDeclaringType().getQualifiedName(), paramTypes); if (f != null) { Map map = checkInvocationRefinements(ctConstructorCall, ctConstructorCall.getArguments(), ctConstructorCall.getTarget(), f.getName(), - f.getTargetClass()); + f.getTargetClass(), paramTypes); AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall); } } @@ -220,22 +222,15 @@ public void getInvocationRefinements(CtInvocation invocation) throws LJEr } else if (method.getParent() instanceof CtClass) { String ctype = ((CtClass) method.getParent()).getQualifiedName(); - int argSize = invocation.getArguments().size(); - RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, argSize); + List> paramTypes = invocation.getExecutable().getParameters(); + RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, paramTypes); if (f != null) { // inside rtc.context checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), - method.getSimpleName(), ctype); + method.getSimpleName(), ctype, paramTypes); } } } - 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), className, size); - return f; - } - private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation invocation) throws LJError { CtTypeReference ctref = ctr.getDeclaringType(); if (ctref == null) { @@ -246,39 +241,47 @@ private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation String ctype = (ctref != null) ? ctref.toString() : null; String name = ctr.getSimpleName(); // missing - int argSize = invocation.getArguments().size(); + List> paramTypes = ctr.getParameters(); String qualifiedSignature = null; if (ctype != null) { qualifiedSignature = String.format("%s.%s", ctype, ctr.getSignature()); - if (rtc.getContext().getFunction(qualifiedSignature, ctype, argSize) != null) { + RefinedFunction f = rtc.getContext().getFunction(qualifiedSignature, ctype, paramTypes); + if (f != null) { checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), - qualifiedSignature, ctype); + qualifiedSignature, ctype, paramTypes); return; } } String signature = ctr.getSignature(); - if (rtc.getContext().getFunction(signature, ctype, argSize) != null) { - checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype); + RefinedFunction f = rtc.getContext().getFunction(signature, ctype, paramTypes); + if (f != null) { + checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), signature, ctype, + paramTypes); return; } - if (rtc.getContext().getFunction(name, ctype, argSize) != null) { // inside rtc.context - checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype); + f = rtc.getContext().getFunction(name, ctype, paramTypes); + if (f != null) { // inside rtc.context + checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype, + paramTypes); return; } if (qualifiedSignature != null) { String completeName = String.format("%s.%s", ctype, name); - if (rtc.getContext().getFunction(completeName, ctype, argSize) != null) { + f = rtc.getContext().getFunction(completeName, ctype, paramTypes); + if (f != null) { checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName, - ctype); + ctype, paramTypes); } } } private Map checkInvocationRefinements(CtElement invocation, List> arguments, - CtExpression target, String methodName, String className) throws LJError { + CtExpression target, String methodName, String className, List> paramTypes) + throws LJError { // -- Part 1: Check if the invocation is possible - int si = arguments.size(); - RefinedFunction f = rtc.getContext().getFunction(methodName, className, si); + RefinedFunction f = null; + if (paramTypes != null) + f = rtc.getContext().getFunction(methodName, className, paramTypes); if (f == null) return new HashMap<>(); Map map = mapInvocation(arguments, f); @@ -407,8 +410,10 @@ public void loadFunctionInfo(CtExecutable method) { className = ((CtInterface) method.getParent()).getQualifiedName(); } if (className != null) { - RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className, - method.getParameters().size()); + List> paramTypes = new ArrayList<>(); + for (CtParameter p : method.getParameters()) + paramTypes.add(p.getType()); + RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), className, paramTypes); if (fi != null) { List lv = fi.getArguments(); for (Variable v : lv)