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
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions