Skip to content

Incrementally integrate external Rust test suites into mir-semantics CI #964

@Stevengre

Description

@Stevengre

Context

PR #962 (jh/test_coverage_20260225_master_pr) explored adding external test coverage infrastructure — coverage matrix, fetch scripts, batch runner, report tooling, and test harnesses for 5 external suites — all at once. That approach is too large for a single PR. We will add tests incrementally instead.

External test suites evaluated

Suite Source
miri-pass rust-lang/miri tests/pass/
miri-fail rust-lang/miri tests/fail/
ui-run-pass rust-lang/rust tests/ui/ (run-pass)
kani model-checking/kani tests/kani/
rustlantis cbeuw/rustlantis (generated programs)

TODO

  • Import stable-mir-json UI tests as mir-semantics tests
  • Add passing miri-pass tests to prove-rs suite
  • Add passing miri-fail tests to prove-rs suite
  • Add passing ui-run-pass tests to prove-rs suite
  • Add passing kani tests to prove-rs suite
  • Investigate rustlantis generated programs for potential test coverage

Workflow

For each test being added:

  1. Verify stable-mir-json can compile the Rust file and produce valid SMIR JSON
  2. Add the test to mir-semantics prove-rs / integration tests
  3. Keep PRs small — a handful of tests from one suite per PR

Reference

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions