-
Notifications
You must be signed in to change notification settings - Fork 5
Open
Description
Problem
Integration tests currently take 2h 37m (example run), which is too long for PR iteration.
Root Cause: Redundant Test Executions
Analysis of the test suite reveals significant overlap:
| Test | Backend | Count | Wall Time | Purpose |
|---|---|---|---|---|
test_exec_smir[*-haskell] |
Haskell | 35 | ~70 min | Concrete execution + snapshot |
test_exec_smir[*-llvm] |
LLVM | 35 | ~55 min | Same, different backend |
test_prove_termination |
Haskell | 19 | ~25 min | Prove termination (same 19 programs as exec_smir depth=None subset) |
test_prove_rs |
Haskell | 49 | long tail | Symbolic verification |
Key redundancies:
exec_smirruns every test twice (LLVM + Haskell) — both verify the same snapshot outputprove_terminationtests the exact same 19 programs already covered byexec_smir[*-haskell]- 9 out of 10 overlapping
.rsfiles betweenprove-rs/andexec-smir/are byte-identical duplicates
Proposed Phased Approach
Phase 1: Remove redundant test runs (small PR, ~80 min savings)
exec_smir: keep Haskell only, remove LLVM parametrization- Haskell is the backend used for proving — bugs here have higher impact
- Removing LLVM saves ~35 tests
- Remove
test_prove_terminationentirelyexec_smir[*-haskell]already runs these 19 programs through the Haskell backendprove_rsalready covers symbolic verification
Expected result: ~2h37m → ~1h20m
Phase 2: Consolidate Rust test programs (structural refactor)
- Merge
prove-rs/,exec-smir/,run-rs/source files into a singleprograms/directory - Remove 9 duplicated
.rsfiles - Test logic references the unified directory
Phase 3: Declarative test configuration
- Introduce a config file (e.g.,
test-config.toml) mapping each program to its test modes (prove,run-haskell,parse-only) - Single test function reads config and dispatches accordingly
More: Consolidate redundant tests
Data
134 unique Rust programs across 4 directories:
prove-rs/: 84.rs+ 1.jsonexec-smir/: 39.rsrun-rs/: 34.rs(only used for smir-parse stability, not integration tests)run-smir-random/: 2.rs
File overlaps: prove-rs ∩ exec-smir = 10 (9 identical), prove-rs ∩ run-rs = 13
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels