Check calls on a constructor call whose constructor has refined parameters (#407)

Follow-up to #361 (typestate calls made directly on a constructor call).

## Problem
A call made directly on `new T(args)` fails when the constructor
`T(args)` has refined parameters:

```java
Socket socket = new ServerSocket(8080).accept();
```
```
Argument Mismatch Error: Argument '#<init>_398' and its respective parameter of ghost
'java.net.ServerSocket.state1' types are incompatible: expected ServerSocket, got void
```

With refined parameters, the constructor call goes through
`applyReturnRefinement`, which sets the call's `TARGET` metadata to the
constructor's return-value instance (`#<init>_N`, typed `void`).
`prepareInvocationTarget` checked `TARGET` before the constructor-call
case, so it used that instance as the receiver. Constructors without
refined parameters (`new ServerSocket().accept()`) were not affected.

## Fix
- `prepareInvocationTarget` handles a constructor-call target before
falling back to `TARGET` metadata.
- The fresh receiver is stored under a new `Keys.RECEIVER` key on the
constructor call and reused when the same invocation is prepared again
(the target is prepared both for the parameter checks and for the state
change), so it is created once.

## Tests
- `CorrectConstructorReceiverRefinedArgument`: `new
Listener(8080).accept()` where `Listener(int)` has a refined parameter
and lands in `bound`. It failed before this change.
- `ErrorConstructorReceiverRefinedArgument`: the same constructor
followed by a call that needs `unbound` is reported.
- `mvn test`: 414 tests, 0 failures.

Found on a real fixed bug (a static page server whose fix was `new
ServerSocket(port).accept()`). We also checked 53 exercises built from
real OSS bugs: the results are identical to main's.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

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

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"unbound", "bound"})
+class CorrectRefinedArgListener {
+    @StateRefinement(to = "unbound(this)")
+    public CorrectRefinedArgListener() {}
+
+    @StateRefinement(to = "bound(this)")
+    public CorrectRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {}
+
+    @StateRefinement(from = "bound(this)")
+    public void accept() {}
+}
+
+public class CorrectConstructorReceiverRefinedArgument {
+    static void chained() {
+        new CorrectRefinedArgListener(8080).accept();
+    }
+}

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

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"unbound", "bound"})
+class ErrorRefinedArgListener {
+    @StateRefinement(to = "unbound(this)")
+    public ErrorRefinedArgListener() {}
+
+    @StateRefinement(to = "bound(this)")
+    public ErrorRefinedArgListener(@Refinement("0 <= _ && _ <= 65535") int port) {}
+
+    @StateRefinement(from = "unbound(this)", to = "bound(this)")
+    public void bind() {}
+}
+
+public class ErrorConstructorReceiverRefinedArgument {
+    static void chained() {
+        new ErrorRefinedArgListener(8080).bind(); // Expect: State Refinement Error
+    }
+}

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

@@ -744,24 +744,29 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             }
 
             return name;
-        } else if (target2.getMetadata(Keys.TARGET) != null) {
-            // invocation is in
-            // who did put the metadata here then?
-            VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
-            Optional<Variable> v = target2Vi.getParent();
-            invocation.putMetadata(Keys.TARGET, target2Vi);
-            return v.map(Refined::getName).orElse(target2Vi.getName());
+        } else if (target2 instanceof CtConstructorCall<?> newCall
+                && newCall.getMetadata(Keys.RECEIVER)instanceof RefinedVariable receiver) {
+            // `new T(args).method()` already prepared: reuse its receiver instead of creating another one
+            invocation.putMetadata(Keys.TARGET, receiver);
+            return receiver.getName();
         } else if (target2 instanceof CtConstructorCall<?> newCall
                 && newCall.getMetadata(Keys.REFINEMENT)instanceof Predicate state) {
-            // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives
+            // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives. Must come
+            // before the TARGET case: a constructor with refined parameters puts its (void) return value in TARGET
             String name = String.format(Formats.FRESH, tc.getContext().getCounter());
             CtTypeReference<?> type = newCall.getType();
             RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type,
                     state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall);
             receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
             newCall.putMetadata(Keys.TARGET, receiver);
+            newCall.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();
+            invocation.putMetadata(Keys.TARGET, target2Vi);
+            return v.map(Refined::getName).orElse(target2Vi.getName());
         }
         return null;
     }

liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java

@@ -4,6 +4,7 @@ public final class Keys {
     public static final String REFINEMENT = "refinement";
     public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check";
     public static final String TARGET = "target";
+    public static final String RECEIVER = "receiver";
     public static final String RETURN_VAR_NAME = "return_var_name";
     public static final String THIS = "this";
     public static final String WILDCARD = "_";