[TS] Model Float64Array(length) construction instead of an unresolved receiver
维护者通常 1 天内回复
还没有人认领这个 Issue。
评估
- 难度
- 4/5
- 预计耗时
- 3-5 天
- 新手友好度
- 43/100
- Issue 类型
- 功能
- 描述清晰度
- 描述清楚
- 活跃度
- 活跃
- 技术栈
- kotlin, typescript
调研方向
Read the typed-array call modeling and receiver resolution paths, then add a source-level regression for Float64Array(length). Replay the unchanged Adder from d3-array src/fsum.js through the public campaign-file entry point and check that construction is modeled with receiver identity and zero initialization. Record any remaining indexed read or write limitation explicitly; preserve the original class and oracle.
由索引模型根据 Issue 内容生成。
描述
Current delivery (2026-10-17)
The Float64Array allocation fix is not implemented. This issue remains open, and the unchanged Adder construction is still a semantic support boundary.
Published #608 at 0e418f5800ffe86b9963965203ffab158d4e357a is open, not merged, with all 7 CI checks green. It fixes the diagnostic transport described in the original report: actual stop/fresh-return events retain the callee, failureReason, statement, and original source location in public property-search and auxiliary-search diagnostics. Its 33 focused tests and three Detekt tasks pass, including JSON round trips for a stopped Float64Array constructor and Array.slice. Successful model application is not mislabeled as a limitation.
That change adds no typed-array allocation, receiver identity, zero initialization, or indexed access semantics. In particular, retaining Float64Array::constructor / RECEIVER_CLASS_NOT_FOUND explains the rejection but does not make the Adder property executable symbolically. #573 concerns ordinary-array sparse indexed growth; #578/#595 concern member identity and accessor safety. None completes #604.
The required next implementation remains the bounded Float64Array(length) constructor model and unchanged-Adder replay stated below, followed by honest reporting of any next indexed-access boundary. Keep the original class and oracle unchanged. The original report's generic-only structured diagnostic describes the pre-#608 baseline, while its allocation acceptance remains current.
Original report and acceptance (retained verbatim)
The PBT class-corpus development check reaches an unsupported call while constructing the unchanged Adder class from d3-array. This prevents symbolic execution before add or valueOf runs.
The source is pinned to d3-array be0ae0d2b36ab91b833294ad2cfc5d5905acbd0f / src/fsum.js. Its constructor contains:
constructor() {
this._partials = new Float64Array(32);
this._n = 0;
}
Copy that complete source module unchanged to Subject.ts, and run this property with a dense six-element array of bounded integers:
import { Adder } from './Subject';
export function check(values: number[]): boolean {
const subject = new Adder();
let expected = 0;
for (const value of values) {
subject.add(value);
expected += value;
}
const first = subject.valueOf();
const second = subject.valueOf();
return first === expected && second === first;
}
Observed through the public campaign-file entry point in SYMBOLIC_ONLY, SEQUENTIAL, and COVERAGE_FEEDBACK:
TsUnknownCallModelDispatcher - Stopping path for unknown call
Float64Array::constructor(): Float64Array
at EtsStmtLocation(method=Adder::constructor(): Adder, index=4):
reason=RECEIVER_CLASS_NOT_FOUND
All three symbolic results are UNSUPPORTED with no completed symbolic inputs. The structured result currently reports usvm.execution.unsupported / The symbolic engine encountered an unsupported property call; the concrete receiver and location are present in stderr. This is an operation in the original subject class, rather than an unsupported reference oracle in the experiment wrapper.
Native Node.js v22.23.1 passes the same original-class property, including [1,2,3,4,5,6] (both reads return 21) and [1000000,-1000000,2,3,4,5] (both reads return 14). The class declaration was compared byte-for-byte against the pinned archive. No replacement with an ordinary Array was made.
The observed assembly is 115135772215cc3cb569dab3dfe0fbab0b141584: public #597 plus the exact sparse-array fix #573, accessor fix #595 at 371a4659321831999ecacb4835c90785b0a23af6, and helper changes #599/#601. Java is Zulu 11.0.32.1. The calibration used seed 37, a 30-second total allocation, six integers in [-1000000,1000000], and the original property above. The failure occurs during construction and is independent of the random input values.
Expected scope: recognize Float64Array(length) as a supported bounded typed-array allocation, with the appropriate receiver identity and zero initialization. Add a source-level regression for the constructor, then re-run the unchanged Adder reproduction. Any separately unsupported indexed-read/write behavior should remain explicit rather than being approximated as an ordinary JavaScript array or hidden by a source rewrite.
This blocks one genuine-class candidate in #356/#357/#405. It does not establish a defect in d3-array. The unsupported candidate remains in the corpus inventory.
- 主要语言
- Kotlin
- 星标
- 33
- 派生
- 27
- 平均合并
- 3 天 21 小时
- 30 天内合并 PR
- 88
环境准备
这个项目没有提供开发容器、Dockerfile 或贡献指南,环境需要你自己搭建:先看它的 README,通用步骤见我们的新手贡献指南。
从这里开始
- 先读完整个 Issue,再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库,在一个分支上完成修改。
- 提交 Pull Request,并在描述里引用这个 Issue 编号。
UnitTestBot/usvm 的其他 Issue
-
[TS PBT] Save campaign-file artifacts before stdout publication可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭
难度 2/5 1-3 小时 新手友好度 74/100
UnitTestBot/usvm#612 ·
维护者通常 1 天内回复
-
[TS PBT] Preserve class verification after expected PBT budget expiry可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭
难度 5/5 一周以上 新手友好度 18/100
UnitTestBot/usvm#618 ·
维护者通常 1 天内回复
-
难度 4/5 3-5 天 新手友好度 25/100
UnitTestBot/usvm#613 ·
维护者通常 1 天内回复
-
难度 5/5 一周以上 新手友好度 25/100
UnitTestBot/usvm#592 ·
维护者通常 1 天内回复
-
[TS] Invoke declared class getters during property reads可能已有人在做 关联的 PR 仍在进行中或已合并。 未关闭
难度 4/5 3-5 天 新手友好度 15/100
UnitTestBot/usvm#577 · 1 条评论 ·
维护者通常 1 天内回复
相似的 Issue
-
submit-adaption submit-adaption-pre
难度 1/5 1 小时以内 新手友好度 76/100
BetterAndroid/android-notification-icon-project#783 · 1 条评论 ·
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 68/100
-
coding size:s skill:kotlin-core sub-issue
难度 2/5 1-3 小时 新手友好度 76/100
SKaiNET-developers/SKaiNET#1421 ·
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 65/100
leonlatsch/Photok#809 ·
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 84/100
维护者通常 1 天内回复