Hacktoberfest 2026: as issues que os mantenedores marcaram para outubro, abertas e boas para iniciantes. Ver issues do Hacktoberfest

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

Aberta
  • Algo errado?
#555 0 comentários 0 reações 0 responsáveis Ver no GitHub

Mantenedores costumam responder em até 1 dia

@CaelmBleidd já está trabalhando nisso.

Desde 16/10/2026.

  • #608 de @CaelmBleidd — aberto

Avaliação

Dificuldade
4/5
Tempo estimado
3-5 dias
Facilidade para iniciantes
38/100
Tipo de issue
Funcionalidade
Clareza
Razoavelmente clara
Status de atividade
Ativa
Stack de tecnologia
kotlin, typescript
Domínio
testing, tooling

Direção de pesquisa

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.

Escrita pelo modelo de indexação a partir do texto da issue.

Descrição

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.

Linguagem predominante
Kotlin
Estrelas
33
Forks
27
Merge médio
3d 21h
PRs com merge (30d)
88

Preparar o ambiente

Este projeto não oferece contêiner de desenvolvimento, Dockerfile nem guia de contribuição, então a configuração fica por sua conta: comece pelo README e veja nosso guia da primeira contribuição para os passos gerais.

Primeiros passos

  1. Leia a issue inteira e depois o guia de contribuição do projeto.
  2. Comente na issue dizendo que vai assumir — evita que duas pessoas façam o mesmo trabalho.
  3. Faça um fork do repositório e trabalhe em uma branch.
  4. Abra um pull request que referencie o número da issue.

Mais de UnitTestBot/usvm

Todas as issues de UnitTestBot/usvm

Issues semelhantes

Mais issues de Kotlin

Receba novas issues na sua caixa de entrada

Um resumo curto de issues do GitHub para quem está começando.