Treat results of methods without refinements as unconstrained in operations

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<String> list) {
+        for (int i = 0; i < list.size(); i++) {
+            System.out.println(list.get(i));
+        }
+    }
+
+    public void boxedResult(List<Integer> list) {
+        if (list.get(0) > 3) {
+            @Refinement("_ > 0")
+            int y = 1;
+        }
+    }
+
+    public void booleanResultInConjunction(Map<String, Integer> 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;
+        }
+    }
+}

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();
+    }
+}

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<Integer> list) {
+        if (list.get(0) > 3) {
+        } else {
+            @Refinement("_ > 0")
+            int y = -1; // Expect: Refinement Error
+        }
+    }
+
+    public void booleanResultInConjunction(Map<String, Integer> 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
+        }
+    }
+}

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
+    }
+}

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
+    }
+}

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);
     }
 
     /**