Repository navigation
[TS] Support push invocation in InstanceCallExpr resolution #300
Description
Resolution (2026-10-14)
Audited against usvm main at 19866c959d.
Array.push executes a bounded source model with runtime-kind-preserving storage; zero through three arguments, new length and mutation are covered. Larger arities remain explicit residual cases. Implementation: usvm #443, usvm #448, usvm #449.
Validation: All 7 TsArrayMutationEtsIrModelTest regressions passed.
Original report and acceptance context, retained for traceability
Current implementation is
// TODO write tests
if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) {
return scope.calcOnState {
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
val lengthLValue = mkArrayLengthLValue(
resolvedInstance,
EtsArrayType(EtsUnknownType, dimensions = 1)
)
val length = memory.read(lengthLValue)
val newLength = mkBvAddExpr(length, 1.toBv())
memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null
// TODO check sorts compatibility
val newIndexLValue = mkArrayIndexLValue(
resolvedArg.sort,
resolvedInstance,
length,
EtsArrayType(EtsUnknownType, dimensions = 1)
)
memory.write(newIndexLValue, resolvedArg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr)
newLength
}
}
We need to check it and fix if required
Metadata
Metadata
Assignees
Labels
No labels
Activity