Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

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

Đang mở
  • Có gì không ổn?
#555 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Maintainer thường phản hồi trong vòng 1 ngày

@CaelmBleidd đang làm issue này rồi.

Từ ngày 16/10/2026.

  • #608 của @CaelmBleidd — đang mở

Đánh giá

Độ khó
4/5
Thời gian dự kiến
3-5 ngày
Mức phù hợp với người mới
38/100
Loại issue
Tính năng
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
kotlin, typescript
Lĩnh vực
testing, tooling

Hướng nghiên cứu

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.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.

Ngôn ngữ chính
Kotlin
Star
33
Fork
27
Merge trung bình
3 ngày 21 giờ
Pull request đã merge (30 ngày)
88

Chuẩn bị môi trường

Dự án này không cung cấp dev container, Dockerfile hay hướng dẫn đóng góp, nên bạn cần tự thiết lập môi trường: hãy bắt đầu từ README và xem hướng dẫn đóng góp lần đầu của chúng tôi để biết các bước chung.

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của UnitTestBot/usvm

Tất cả issue của UnitTestBot/usvm

Issue tương tự

Thêm issue về Kotlin

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.