diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java new file mode 100644 index 00000000..4338abdb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparison.java @@ -0,0 +1,80 @@ +package testSuite; + +import java.util.List; +import java.util.Map; + +import liquidjava.specification.Refinement; + +// Results of methods without refinements can be used in operations (issue #300) +@SuppressWarnings("unused") +public class CorrectUnknownMethodInComparison { + interface Shape { + int area(); + } + + int helper() { + return 1; + } + + public void lengthInComparison(String s) { + if (s.length() < 3) { + @Refinement("_ > 0") + int y = 1; + } else { + @Refinement("_ > 0") + int z = 1; + } + } + + public void equalsInDisjunction(String s) { + boolean known = s.equals("a") || s.equals("b"); + } + + public void sizeInLoopBound(List list) { + for (int i = 0; i < list.size(); i++) { + System.out.println(list.get(i)); + } + } + + public void boxedResult(List list) { + if (list.get(0) > 3) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void booleanResultInConjunction(Map map, String k, int n) { + if (map.containsKey(k) && n > 0) { + @Refinement("_ > 0") + int y = n; + } + } + + public void staticCall(int a, int b) { + if (Math.max(a, b) > 0) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void chainedCall(String s) { + if (s.trim().length() > 0) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void implicitThisCall() { + if (helper() > 0) { + @Refinement("_ > 0") + int y = 1; + } + } + + public void interfaceMethod(Shape shape) { + if (shape.area() > 0) { + @Refinement("_ > 0") + int y = 1; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparisonState.java b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparisonState.java new file mode 100644 index 00000000..5733c9d1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnknownMethodInComparisonState.java @@ -0,0 +1,26 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Calling a method without refinements in a condition keeps the object's state (issue #300) +@StateSet({"open", "closed"}) +public class CorrectUnknownMethodInComparisonState { + @StateRefinement(to = "open(this)") + public CorrectUnknownMethodInComparisonState() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public int count() { + return 0; + } + + public static void main(String[] args) { + CorrectUnknownMethodInComparisonState r = new CorrectUnknownMethodInComparisonState(); + if (r.count() > 0) { + System.out.println("non-empty"); + } + r.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparison.java new file mode 100644 index 00000000..9fe0d440 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparison.java @@ -0,0 +1,85 @@ +package testSuite; + +import java.util.List; +import java.util.Map; + +import liquidjava.specification.Refinement; + +// Results of methods without refinements are unconstrained, so no branch is dead (issue #300) +@SuppressWarnings("unused") +public class ErrorUnknownMethodInComparison { + interface Shape { + int area(); + } + + int helper() { + return 1; + } + + public void thenBranch(String s) { + if (s.length() < 3) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void elseBranch(String s) { + if (s.length() < 3) { + } else { + @Refinement("_ > 0") + int z = -1; // Expect: Refinement Error + } + } + + public void equalsInDisjunction(String s) { + if (s.equals("a") || s.equals("b")) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void boxedResult(List list) { + if (list.get(0) > 3) { + } else { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void booleanResultInConjunction(Map map, String k, int n) { + if (map.containsKey(k) && n > 0) { + @Refinement("_ > 0") + int y = n - 1; // Expect: Refinement Error + } + } + + public void staticCall(int a, int b) { + if (Math.max(a, b) > 0) { + } else { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void chainedCall(String s) { + if (s.trim().length() > 0) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void implicitThisCall() { + if (helper() > 0) { + } else { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } + + public void interfaceMethod(Shape shape) { + if (shape.area() > 0) { + @Refinement("_ > 0") + int y = -1; // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparisonState.java b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparisonState.java new file mode 100644 index 00000000..0689f40a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInComparisonState.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Calling a method without refinements in a condition keeps the object's state (issue #300) +@StateSet({"open", "closed"}) +public class ErrorUnknownMethodInComparisonState { + @StateRefinement(to = "open(this)") + public ErrorUnknownMethodInComparisonState() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public int count() { + return 0; + } + + public static void main(String[] args) { + ErrorUnknownMethodInComparisonState r = new ErrorUnknownMethodInComparisonState(); + r.close(); + if (r.count() > 0) { + System.out.println("non-empty"); + } + r.close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java new file mode 100644 index 00000000..177dab74 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java @@ -0,0 +1,12 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// Results of methods without refinements carry no information (issue #300) +@SuppressWarnings("unused") +public class ErrorUnknownMethodInOperation { + public void lengthPlusOne(String s) { + @Refinement("_ > 0") + int x = s.length() + 1; // Expect: Refinement Error + } +} 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 b07a06c6..35264189 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 @@ -37,9 +37,9 @@ import spoon.reflect.code.CtVariableWrite; import spoon.reflect.code.UnaryOperatorKind; import spoon.reflect.declaration.CtAnnotation; -import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtType; import spoon.reflect.declaration.ParentNotInitializedException; import spoon.reflect.reference.CtVariableReference; import spoon.support.reflect.code.CtIfImpl; @@ -251,8 +251,10 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab return getOperationRefinementFromExternalLib(inv); // Get function refinements with non_used variables - String met = ((CtClass) method.getParent()).getQualifiedName(); // TODO check + String met = method.getParent(CtType.class).getQualifiedName(); // TODO check RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size()); + if (fi == null) + return getUnconstrainedInvocationVariable(inv); Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! // Substitute _ by the variable that we send @@ -265,6 +267,16 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // TODO Maybe add cases } + /** + * Creates a fresh variable with no information (refinement true) to represent the result of an invocation of a + * method without refinements + */ + private Predicate getUnconstrainedInvocationVariable(CtInvocation inv) { + String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + rtc.getContext().addVarToContext(newName, inv.getType(), new Predicate(), inv); + return new Predicate(newName, inv); + } + private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) throws LJError { CtExpression t = inv.getTarget(); @@ -279,6 +291,8 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) thr String methodInClassName = typeNotParametrized + "." + simpleName; RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized, inv.getArguments().size()); + if (fi == null) + return getUnconstrainedInvocationVariable(inv); Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! // Substitute _ by the variable that we send @@ -296,7 +310,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) thr rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); return new Predicate(newName, inv); // Return variable that represents the invocation } - return new Predicate(); + return getUnconstrainedInvocationVariable(inv); } /**