Fix crashes on enum methods, varargs calls and calls on a call result

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

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class CorrectCallResultDoor {
+    @StateRefinement(to = "open(this)")
+    public CorrectCallResultDoor() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+
+    @StateRefinement(to = "closed(this)")
+    public void slam() {}
+}
+
+class CorrectCallResultHolder {
+    private final CorrectCallResultDoor door = new CorrectCallResultDoor();
+
+    CorrectCallResultDoor get() {
+        return door;
+    }
+}
+
+public class CorrectCallResultReceiver {
+    static void use(CorrectCallResultHolder holder) {
+        holder.get().slam();
+    }
+}

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

@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+enum CorrectEnumWithMethodAction {
+    UNDO, REDO;
+
+    String getText() {
+        return name();
+    }
+}
+
+public class CorrectEnumWithMethod {
+    static String describe(CorrectEnumWithMethodAction action) {
+        @Refinement("_ > 0")
+        int width = 1;
+        return action.getText() + width;
+    }
+}

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

@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+class CorrectVarargsLogger {
+    void debug(@Refinement("_ >= 0") int level, String format, Object... args) {}
+}
+
+public class CorrectVarargsCall {
+    static void log(CorrectVarargsLogger logger, Object a, Object b) {
+        logger.debug(1, "{} and {}", a, b);
+        logger.debug(2, "nothing");
+        logger.debug(3, "{}", new Object[] {a});
+    }
+}

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

@@ -0,0 +1,27 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class ErrorCallResultDoor {
+    @StateRefinement(to = "open(this)")
+    public ErrorCallResultDoor() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+class ErrorCallResultHolder {
+    private final ErrorCallResultDoor door = new ErrorCallResultDoor();
+
+    ErrorCallResultDoor get() {
+        return door;
+    }
+}
+
+public class ErrorCallResultReceiver {
+    static void use(ErrorCallResultHolder holder) {
+        holder.get().close(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+class ErrorVarargsLogger {
+    void debug(@Refinement("_ >= 0") int level, String format, Object... args) {}
+}
+
+public class ErrorVarargsCall {
+    static void log(ErrorVarargsLogger logger, Object a, Object b) {
+        logger.debug(-1, "{} and {}", a, b); // Expect: Refinement Error
+    }
+}

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

@@ -21,6 +21,7 @@
 import spoon.reflect.declaration.CtRecord;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtField;
+import spoon.reflect.declaration.CtEnum;
 import spoon.reflect.declaration.CtInterface;
 import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.declaration.CtParameter;
@@ -46,6 +47,11 @@ public void visitCtRecord(CtRecord ctRecord) {
         // records are user code, like classes: external specs are only read from interfaces
     }
 
+    @Override
+    public <T extends Enum<?>> void visitCtEnum(CtEnum<T> ctEnum) {
+        // enums are user code too; their methods have no external target
+    }
+
     @Override
     public <T> void visitCtInterface(CtInterface<T> intrface) {
         Optional<CtAnnotation<?>> externalRef = getExternalRefinement(intrface);

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

@@ -419,7 +419,7 @@ private void applyReturnRefinement(CtElement invocation, RefinedFunction f, Map<
     private Map<String, String> mapInvocation(List<CtExpression<?>> arguments, RefinedFunction f) {
         Map<String, String> mapInvocation = new HashMap<>();
         List<Variable> functionParams = f.getArguments();
-        for (int i = 0; i < arguments.size(); i++) {
+        for (int i = 0; i < matchedArguments(arguments, functionParams); i++) {
             Variable fArg = functionParams.get(i);
             CtExpression<?> iArg = arguments.get(i);
             String invStr;
@@ -437,6 +437,16 @@ private Map<String, String> mapInvocation(List<CtExpression<?>> arguments, Refin
         return mapInvocation;
     }
 
+    /**
+     * The number of arguments bound one to one to parameters. A varargs call can pass more (or fewer) arguments than
+     * there are parameters; the ones collected into the varargs array are left out.
+     */
+    private static int matchedArguments(List<CtExpression<?>> arguments, List<Variable> params) {
+        if (arguments.size() == params.size())
+            return arguments.size();
+        return Math.min(arguments.size(), Math.max(params.size() - 1, 0));
+    }
+
     private String createVariableRepresentingArgument(CtExpression<?> iArg, Variable fArg) {
         Predicate met = (Predicate) iArg.getMetadata(Keys.REFINEMENT);
         if (met == null)
@@ -451,7 +461,7 @@ private String createVariableRepresentingArgument(CtExpression<?> iArg, Variable
     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++) {
+        for (int i = 0; i < matchedArguments(arguments, functionParams); i++) {
             Variable fArg = functionParams.get(i);
             Predicate c = fArg.getMainRefinement();
             c = c.substituteVariable(fArg.getName(), map.get(fArg.getName()));

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -848,6 +848,21 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             newCall.putMetadata(Keys.RECEIVER, receiver);
             invocation.putMetadata(Keys.TARGET, receiver);
             return name;
+        } else if (target2 instanceof CtInvocation<?> call
+                && call.getMetadata(Keys.RECEIVER)instanceof RefinedVariable receiver) {
+            invocation.putMetadata(Keys.TARGET, receiver);
+            return receiver.getName();
+        } else if (target2 instanceof CtInvocation<?> call && call.getMetadata(Keys.TARGET) != null
+                && !isReturnValue(call)) {
+            // `a.get().method()` where get() has no return refinement: the call's TARGET is its own receiver (a), not
+            // the value it returns, so the receiver is a fresh value of the call's type, in a state not known here
+            String name = String.format(Formats.FRESH, tc.getContext().getCounter());
+            CtTypeReference<?> type = call.getType();
+            RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type, new Predicate(), call);
+            receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
+            call.putMetadata(Keys.RECEIVER, receiver);
+            invocation.putMetadata(Keys.TARGET, receiver);
+            return name;
         } else if (target2.getMetadata(Keys.TARGET) != null) {
             VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
             Optional<Variable> v = target2Vi.getParent();
@@ -857,6 +872,12 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
         return null;
     }
 
+    /** Whether a call's TARGET metadata is the value it returns (set when its return refinement is applied). */
+    private static boolean isReturnValue(CtInvocation<?> call) {
+        return call.getMetadata(Keys.TARGET)instanceof VariableInstance vi
+                && vi.getName().equals(call.getMetadata(Keys.RETURN_VAR_NAME));
+    }
+
     static VariableInstance getTarget(CtElement invocation) {
         if (invocation.getMetadata(Keys.TARGET) != null) {
             return (VariableInstance) invocation.getMetadata(Keys.TARGET);