Soundness: reassigning a parameter changes the state recorded from its earlier use (new HashMap<>(n); n = 5) #439

Impact: a real violation passes verification (missed error).

Description

A parameter has no variable instance until it is first assigned, so a use of it before then refers to the raw name. In mapInvocation (MethodsFunctionsChecker.java:431, ovi.map(Refined::getName).orElse(vr.toString())) the constructor's state cap(this) == initialCapacity becomes cap(r) == n, and a later n = 5 changes what n means, so cap(r) == 5 is assumed. Plain reads use the same fallback (RefinementTypeChecker.getPutVariableMetadata, RefinementTypeChecker.java:912), so int m = n; n = 5; also gives m == 5 (second example). Giving each parameter an initial instance would avoid it.

Minimal reproducer (two files)

import liquidjava.specification.*;

@ExternalRefinementsFor("java.util.HashMap")
@Ghost("int cap")
public interface HashMapRefinements<K, V> {
    @StateRefinement(to = "cap(this) == initialCapacity")
    void HashMap(int initialCapacity);

    @StateRefinement(from = "cap(this) == 5")
    V get(Object k);
}

import java.util.HashMap;

public class Repro {
    static void f(int n) {
        HashMap<String, String> r = new HashMap<>(n);
        n = 5;
        r.get("k");   // cap(r) is the old n, not 5
    }
}

Expected

A State Refinement Error at r.get("k").

Actual

Correct! Passed Verification.

Control: without n = 5

State Refinement Error: found cap(r⁸) == n but expected cap(r⁸) == 5

The same happens with a class specified in the file (new Box(n) with to = "cap(this) == c") and with a method's to (b.set(n)). It does not happen when the argument is a local declared with an initializer (int m = 3; new Box(m); m = 5; is reported).

Without a constructor

import liquidjava.specification.Refinement;

public class Repro {
    static void f(int n) {
        int m = n;
        n = 5;
        @Refinement("_ == 5") int k = m;   // m is the old n
    }
}

Correct! Passed Verification.

Reproduced on main at 1a506fe (liquidjava-verifier 0.0.36).

Context

Found while reviewing #433.

🤖 Generated with Claude Code