Hacktoberfest 2026:维护者为十月标记出来的 issue,仍然开放、适合新手。 浏览 Hacktoberfest issue

[TS] Model Float64Array(length) construction instead of an unresolved receiver

未关闭
#604 0 条评论 0 个 reaction 已指派 0 人 在 GitHub 查看

维护者通常 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,通用步骤见我们的新手贡献指南。

从这里开始

  1. 先读完整个 Issue,再读项目的贡献指南。
  2. 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
  3. Fork 仓库,在一个分支上完成修改。
  4. 提交 Pull Request,并在描述里引用这个 Issue 编号。

UnitTestBot/usvm 的其他 Issue

查看 UnitTestBot/usvm 的全部 Issue

相似的 Issue

更多 Kotlin Issue

把新 issue 发到你的邮箱

精选适合新手参与的 GitHub issue 摘要。