Support .length on array expressions and spread varargs calls

liquidjava-example/src/main/java/testSuite/CorrectLengthOfArrayExpression.java

@@ -0,0 +1,36 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectLengthOfArrayExpression {
+
+    int[] values = new int[3];
+
+    int[] values() {
+        return values;
+    }
+
+    static double sum(double[][] grid) {
+        double total = 0;
+        for (int i = 0; i < grid.length; i++) {
+            for (int j = 0; j < grid[i].length; j++) {
+                total += grid[i][j];
+            }
+        }
+        return total;
+    }
+
+    static int sizes(CorrectLengthOfArrayExpression o) {
+        return o.values().length + o.values.length;
+    }
+
+    int ownSize() {
+        return values.length + this.values.length;
+    }
+
+    static int firstRow(@Refinement("length(grid) > 0") int[][] grid) {
+        @Refinement("_ > 0")
+        int rows = grid.length;
+        return rows + grid[0].length;
+    }
+}

liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java

@@ -0,0 +1,42 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectVarargsCall {
+
+    static int count(String... names) {
+        return names.length;
+    }
+
+    static int first(@Refinement("length(xs) > 0") int... xs) {
+        return xs[0];
+    }
+
+    static int pick(@Refinement("k >= 0") int k, int... xs) {
+        return k;
+    }
+
+    @Refinement("_ == 7")
+    static int seven(int... xs) {
+        return 7;
+    }
+
+    CorrectVarargsCall(@Refinement("length(xs) > 1") int... xs) {
+    }
+
+    public static void main(String[] args) {
+        int a = count();
+        int b = count("a");
+        int c = count("a", "b", "c");
+        int d = count(new String[] { "x" });
+        int e = count(args);
+        int f = first(1, 2);
+        int g = first(5);
+        int h = pick(0);
+        int i = pick(1, 2, 3);
+        int j = count("a", "b") + 1;
+        @Refinement("_ == 8")
+        int k = seven(1, 2) + 1;
+        new CorrectVarargsCall(1, 2);
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorEmptyVarargsCall.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorEmptyVarargsCall {
+
+    static int first(@Refinement("length(xs) > 0") int... xs) {
+        return xs[0];
+    }
+
+    public static void main(String[] args) {
+        int a = first(); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorLengthOfArrayExpression.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorLengthOfArrayExpression {
+
+    static int nonNegative(@Refinement("_ >= 0") int x) {
+        return x;
+    }
+
+    static int rowSize(int[][] grid, int i) {
+        return nonNegative(grid[i].length - 10); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java

@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorVarargsCall {
+
+    static int pick(@Refinement("k >= 0") int k, int... xs) {
+        return k;
+    }
+
+    public static void main(String[] args) {
+        int i = pick(-1, 2, 3); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorVarargsLoopState.java

@@ -0,0 +1,27 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "marked"})
+public class ErrorVarargsLoopState {
+    @StateRefinement(to = "open(this)")
+    ErrorVarargsLoopState() {}
+
+    @StateRefinement(to = "marked(this)")
+    void mark(int... tags) {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    // The loop may run zero times, leaving b open, even when mark spreads its varargs.
+    static void mayBeEmpty(int n) {
+        ErrorVarargsLoopState b = new ErrorVarargsLoopState();
+        int k = 0;
+        while (k < n) {
+            b.mark(1, 2);
+            k++;
+        }
+        b.reset(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -332,9 +332,14 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
                     Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
 
         } else if (fieldRead.getVariable().getSimpleName().equals("length")) {
-            String targetName = fieldRead.getTarget().toString();
-            fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
-                    BuiltinFunctionPredicate.length(targetName, fieldRead)));
+            // only a local variable or parameter can be named in a refinement; the length of any other array
+            // expression (e.g. grid[i], o.arr() or this.arr) is left unconstrained
+            CtExpression<?> target = fieldRead.getTarget();
+            Predicate lengthRefinement = new Predicate();
+            if (target instanceof CtVariableRead<?> && !(target instanceof CtFieldRead<?>))
+                lengthRefinement = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
+                        BuiltinFunctionPredicate.length(target.toString(), fieldRead));
+            fieldRead.putMetadata(Keys.REFINEMENT, lengthRefinement);
         } else if (fieldRead.getVariable().getDeclaringType().getDeclaration() instanceof CtEnum) {
             // only enums declared in the analyzed sources can be translated to SMT
             String target = fieldRead.getVariable().getDeclaringType().getSimpleName();
@@ -672,7 +677,7 @@ private void havocChangedIn(CtLoop loop) {
         Set<String> names = new LinkedHashSet<>();
         for (CtAbstractInvocation<?> call : calls) {
             if (call instanceof CtInvocation<?> inv
-                    && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size())
+                    && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), Utils.declaredArity(inv))
                             .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) {
                 if (inv.getTarget()instanceof CtVariableAccess<?> target)
                     changed.add(target);

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

@@ -20,10 +20,12 @@
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
+import spoon.reflect.code.CtAbstractInvocation;
 import spoon.reflect.code.CtConstructorCall;
 import spoon.reflect.code.CtExpression;
 import spoon.reflect.code.CtFieldRead;
 import spoon.reflect.code.CtInvocation;
+import spoon.reflect.code.CtLiteral;
 import spoon.reflect.code.CtReturn;
 import spoon.reflect.code.CtVariableRead;
 import spoon.reflect.declaration.CtClass;
@@ -332,7 +334,7 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
             f = rtc.getContext().getFunction(methodName, className, paramTypes);
         if (f == null)
             return new HashMap<>();
-        Map<String, String> map = mapInvocation(arguments, f);
+        Map<String, String> map = mapInvocation(invocation, arguments, f);
 
         String returnViName = prepareReturnInstance(invocation, f);
 
@@ -351,7 +353,7 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
             return map;
         }
 
-        checkParameters(invocation, arguments, f, map);
+        checkParameters(invocation, f, map);
 
         if (target != null)
             AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
@@ -412,10 +414,18 @@ private void applyReturnRefinement(CtElement invocation, RefinedFunction f, Map<
         invocation.putMetadata(Keys.REFINEMENT, methodRef);
     }
 
-    private Map<String, String> mapInvocation(List<CtExpression<?>> arguments, RefinedFunction f) {
+    private Map<String, String> mapInvocation(CtElement invocation, List<CtExpression<?>> arguments,
+            RefinedFunction f) {
         Map<String, String> mapInvocation = new HashMap<>();
         List<Variable> functionParams = f.getArguments();
-        for (int i = 0; i < arguments.size(); i++) {
+        int mapped = arguments.size();
+        if (spreadsVarargs(invocation, arguments, functionParams.size())) {
+            // the trailing arguments are packed into a new array, which is what the varargs parameter refers to
+            mapped = functionParams.size() - 1;
+            Variable varargs = functionParams.get(mapped);
+            mapInvocation.put(varargs.getName(), createVarargsArray(invocation, varargs, arguments.size() - mapped));
+        }
+        for (int i = 0; i < mapped; i++) {
             Variable fArg = functionParams.get(i);
             CtExpression<?> iArg = arguments.get(i);
             String invStr;
@@ -433,6 +443,36 @@ private Map<String, String> mapInvocation(List<CtExpression<?>> arguments, Refin
         return mapInvocation;
     }
 
+    /**
+     * Whether a call to a varargs method passes its trailing arguments individually (zero, one or several of them)
+     * instead of passing an array as the varargs parameter.
+     */
+    private boolean spreadsVarargs(CtElement invocation, List<CtExpression<?>> arguments, int paramCount) {
+        if (paramCount == 0 || !(invocation instanceof CtAbstractInvocation<?> inv))
+            return false;
+        CtExecutable<?> method = inv.getExecutable().getExecutableDeclaration();
+        if (method == null || method.getParameters().size() != paramCount)
+            return false;
+        CtParameter<?> last = method.getParameters().get(paramCount - 1);
+        if (!last.isVarArgs())
+            return false;
+        if (arguments.size() != paramCount)
+            return true;
+        CtExpression<?> lastArg = arguments.get(paramCount - 1);
+        if (lastArg instanceof CtLiteral<?> lit && lit.getValue() == null)
+            return false; // a null array
+        CtTypeReference<?> argType = lastArg.getType();
+        return argType == null || !argType.isSubtypeOf(last.getType());
+    }
+
+    private String createVarargsArray(CtElement invocation, Variable fArg, int length) {
+        String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter());
+        Predicate lengthRef = Predicate.createEquals(Predicate.createInvocation("length", Predicate.createVar(nVar)),
+                Predicate.createLit(String.valueOf(length), Types.INT));
+        rtc.getContext().addInstanceToContext(nVar, fArg.getType(), lengthRef, invocation);
+        return nVar;
+    }
+
     private String createVariableRepresentingArgument(CtExpression<?> iArg, Variable fArg) {
         Predicate met = (Predicate) iArg.getMetadata(Keys.REFINEMENT);
         if (met == null)
@@ -444,11 +484,10 @@ private String createVariableRepresentingArgument(CtExpression<?> iArg, Variable
         return nVar;
     }
 
-    private void checkParameters(CtElement invocation, List<CtExpression<?>> arguments, RefinedFunction f,
-            Map<String, String> map) throws LJError {
-        List<Variable> functionParams = f.getArguments();
-        for (int i = 0; i < arguments.size(); i++) {
-            Variable fArg = functionParams.get(i);
+    private void checkParameters(CtElement invocation, RefinedFunction f, Map<String, String> map) throws LJError {
+        for (Variable fArg : f.getArguments()) {
+            if (!map.containsKey(fArg.getName()))
+                continue;
             Predicate c = fArg.getMainRefinement();
             c = c.substituteVariable(fArg.getName(), map.get(fArg.getName()));
             List<String> vars = c.getVariableNames();

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

@@ -275,7 +275,8 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
 
             // Get function refinements with non_used variables
             String met = method.getParent(CtType.class).getQualifiedName(); // TODO check
-            RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size());
+            RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met,
+                    method.getParameters().size());
             if (fi == null)
                 return getUnconstrainedInvocationVariable(inv);
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!
@@ -313,7 +314,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
             String typeNotParametrized = (i > 0) ? c.substring(0, i) : c;
             String methodInClassName = typeNotParametrized + "." + simpleName;
             RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized,
-                    inv.getArguments().size());
+                    Utils.declaredArity(inv));
             if (fi == null)
                 return getUnconstrainedInvocationVariable(inv);
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

@@ -8,6 +8,7 @@
 import java.util.stream.Stream;
 
 import liquidjava.utils.constants.Types;
+import spoon.reflect.code.CtAbstractInvocation;
 import spoon.reflect.code.CtBlock;
 import spoon.reflect.code.CtFor;
 import spoon.reflect.code.CtForEach;
@@ -18,6 +19,7 @@
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtConstructor;
 import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.CtExecutable;
 import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtFieldReference;
@@ -56,6 +58,15 @@ public static String qualifyFieldName(CtFieldReference<?> field) {
         return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName();
     }
 
+    /**
+     * Number of parameters the invoked method declares, which differs from the number of arguments when a call spreads
+     * its varargs
+     */
+    public static int declaredArity(CtAbstractInvocation<?> invocation) {
+        CtExecutable<?> method = invocation.getExecutable().getExecutableDeclaration();
+        return method != null ? method.getParameters().size() : invocation.getExecutable().getParameters().size();
+    }
+
     public static String getFile(CtElement element) {
         SourcePosition pos = element.getPosition();
         if (pos == null || pos.getFile() == null)