Hacktoberfest 2026：維護者為十月標記出來的 issue，仍然開放、適合新手。 瀏覽 Hacktoberfest issue

[TS PBT] Preserve runtime limitation reasons in property-search results

未關閉
  • 哪裡不對？
#555 0 則留言 0 個 reaction 已指派 0 人 在 GitHub 檢視

維護者通常 1 天內回覆

@CaelmBleidd 已經在處理了。

開始於 2026年10月16日。

  • #608 來自 @CaelmBleidd —— 未關閉

評估

難度
4/5
預估耗時
3-5 天
新手友好度
38/100
Issue 類型
功能
描述清晰度
基本清楚
活躍度
活躍
技術堆疊
kotlin, typescript
領域
testing, tooling

研究方向

Start with TsInterpreterObserver and the existing onRuntimeFeatureLimitation event to see what statement, reason and detail it already carries. Then trace how the PBT search result and its artifact are built, and check whether the limitation is dropped there. Done when a property whose only path is excluded by ARRAY_INDEX_GROWTH reports that reason, a mixed supported/excluded property keeps both, and the result round-trips through DSL/campaign serialization. The issue depends on #345 and #388, so confirm scope with maintainers first.

由索引模型根據 Issue 內容生成。

描述

Part of the two-phase PBT -> USVM plan in #345, agreed on 2026-10-16.

Problem

The fixed-input PGOrbit investigation observed an ARRAY_INDEX_GROWTH event from TsInterpreterObserver, while the analysis result contained EXHAUSTED, no terminal states, no unsupported paths and unsupportedCall=false. The PBT search result therefore loses the reason that execution was incomplete.

The existing onRuntimeFeatureLimitation event already carries the statement, stable reason and detail. Calls consumers retain this signal; the PBT consumer should reuse it.

Required change

  • Retain bounded, deduplicated runtime-limitation diagnostics in the existing PBT result/artifact path.
  • Preserve the original source statement and reason, including array bounds and other supported model limitations.
  • Distinguish exhausted supported search from paths excluded by a model limitation. Keep reached candidates, timeout, solver UNKNOWN and ordinary property outcomes independently visible.
  • Use existing observer/result mechanisms. No generic telemetry system or new search session is required.

Acceptance

  • A property whose only symbolic path exceeds the supported array capacity reports its actual stable runtime limitation reason rather than an unexplained no-finding result. Historical ARRAY_INDEX_GROWTH evidence remains preserved below.
  • A property with both supported and excluded paths retains supported results and reports the limitation.
  • The result survives normal DSL/campaign serialization, with the original program and oracle unchanged.

This issue reports the limitation; implementing sparse growth remains #388. Public end-to-end regressions and their current supported/excluded fixture boundary are recorded in the delivery status below.

Delivery status (2026-10-17)

The PBT observer/result delivery preserves bounded, deduplicated runtime limitation reasons in #560; #608 adds stopped/fresh unknown-call residual reasons, callee and source through the existing observer contract. Successfully applied models are not limitations. Ordinary and auxiliary public campaign round trips retain diagnostics. #608 passed 33 focused tests, strict Detekt and common-assembly checks; it remains an open PR.

The original sparse-growth event above is historical. #573 separately supplies bounded sparse growth under #388, so index 9 is no longer an excluded-path fixture in the current assembly. Index 1001 still truthfully reports usvm.runtime.array-length-capacity. This reporting does not add Float64Array, arbitrary computed initialization or private/helper closures.

The completed class pilot also preserves a different incompleteness boundary: some symbolic results have NO_VIOLATION_REACHED with no runtime limitation while original native verification leaves inputs unchecked; other runner processes are externally killed or fail artifact handling. These are not evidence of language unsupport or complete no-finding coverage. #354 and #357 retain their exact deadline/publication/native-check dispositions separately; no new speculative model limitation was invented from empty stdout.

主要語言
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 摘要。