Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

[TS PBT] Search for property violations with USVM

オープン
  • 何か問題がありますか？
#352 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

メンテナーはふだん 1 日以内に返信

まだ誰も着手していません。

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
35/100
issue の種類
機能追加
明瞭さ
おおむね明確
活発さ
活発
技術スタック
kotlin, typescript
領域
compilers, testing-qa

調査の方向性

Start with dependencies #351 and #384, then trace the existing target and machine execution APIs and the JsConcreteValue extraction path. Review the focused examples and relevant tests for holding, false, throwing, precondition, and multi-call relational predicates. Done means scoped candidate artifacts and tests distinguish termination and capability outcomes without confirming candidates.

索引モデルが issue の本文から書いたものです。

説明

Delivery boundary in the full #345 roadmap

Preserve the original-predicate violation search in PR #387 as this issue's scope. #398 adds assertion/intermediate/hypothesis targets, #399 selects them, and #355 integrates feedback. #401 and #402 own richer relational/sequence support; this issue does not acquire all their acceptance gates. Searching an original user property remains a mandatory baseline in every feedback comparison.

Part of #345. Depends on #351 and #384.

Goal

Use USVM to search for inputs violating the original TypeScript predicate under the shared declared domain and precondition.

Scope

  • Execute the mapped predicate with #351 inputs and a supported pure precondition following #384.
  • A false predicate result or any escaping predicate exception, including an assertion failure, is a candidate violation. Expected exceptions are caught inside the predicate. A non-boolean result is a property-definition error.
  • Support a relational predicate making multiple ordinary calls within one invocation. This does not require a general stateful-testing framework or persistent state between samples.
  • Use the existing target and machine execution APIs.
  • Extract supported candidate inputs once using JsConcreteValue, preserving ordered inputs and the supported alias/value semantics. #353 consumes this representation rather than implementing a second extraction layer.
  • Keep reached-target information independent from extraction failure and run termination. A reached state with unrepresentable inputs remains visible but is not a confirmed counterexample.
  • Distinguish no violation found within this search, timeout, unsupported execution, property-definition error, engine failure and input-resolution failure.
  • Async or otherwise unsupported predicates remain concrete-only where a backend can run them.

Definition of Done

  • Focused examples cover a holding predicate, false predicate, throwing predicate, precondition rejection/error and a multi-call relational property.
  • Candidate artifacts retain property ID, inputs when available, reached target, termination status and capability limitations.
  • No unsupported/opaque execution or timeout is reported as a proved property.
  • Every candidate remains unconfirmed until #353 replays it in the original runtime.
  • No duplicate capability model, exception framework, value codec or generic target framework is introduced.
  • Deliver the existing scoped implementation with relevant tests.

Concrete replay, shrinking and search hints are outside this issue.

主要言語
Kotlin
スター
33
フォーク
27
平均マージ
3日 8時間
マージ済み PR（30日）
7

環境構築

このプロジェクトには開発コンテナ、Dockerfile、コントリビューションガイドがありません。まず README を読み、一般的な手順ははじめてのコントリビューションガイドを参照してください。

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

UnitTestBot/usvm のほかの issue

UnitTestBot/usvm の issue をすべて見る

似ている issue

Kotlin の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。