Pack spread varargs arguments into one array argument (#349)

Arguments were matched one-to-one with the method parameters, so a call
to a varargs method with more arguments than parameters indexed past the
parameter list and crashed (`Index 1 out of bounds for length 1`), and a
call with zero or one spread argument was checked against the varargs
parameter as if that argument were the array itself.

When a call passes its trailing arguments individually (the argument
count differs from the parameter count, or the last argument is not a
subtype of the array type and not null), the varargs parameter is now
bound to a fresh array instance whose only refinement is its length
(the number of spread arguments). Refinements on the varargs parameter
are checked against that array; the individual elements are not checked
against anything. Passing an explicit array keeps the one-to-one
mapping. Parameter checking now iterates over the mapped parameters
instead of the arguments.

Fixes #349

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

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

@@ -0,0 +1,35 @@
+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;
+    }
+
+    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;
+        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/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-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();