Repository navigation
[TS] Support multiple arguments in Array.unshift #438
Description
Resolution (2026-10-14)
Audited against usvm main at 19866c959d.
The bounded Array.unshift source model supports zero through three arguments in source order and preserves known sparse slots/aliases. Larger arities remain explicit residual cases. Implementation: usvm #449, usvm #477.
Validation: All 7 TsArrayMutationEtsIrModelTest regressions passed; #477 contains the sparse and zero/multiple-argument source/Node regressions.
Original report and acceptance context, retained for traceability
Problem
The Array.unshift approximation requires exactly one argument and has an explicit vararg TODO.
Minimal TypeScript example
export function prepend(): number[] {
const values = [3];
values.unshift(1, 2);
return values;
}Expected behavior
prepend() returns [1, 2, 3] and unshift returns the new length 3. Evaluate arguments left to right and preserve their order after shifting existing elements.
Current source evidence
Checked against USVM main 53dce8f3bca2713642c783ba8308a6a360a9e516. This exact snippet is a proposed regression from source audit; it has not yet been run as a new end-to-end test. #368 audits the existing call approximations but does not implement these individual fixes.
Acceptance criteria
- A focused test checks the symbolic outcome without reporting an approximation as exact semantics.
- The supported case agrees with concrete TypeScript/Node.js replay.
- Unsupported operand or environment cases remain explicit.
Activity