compiletest: start cargo-kani tests from a clean target directory#4614
Open
tautschnig wants to merge 2 commits into
Open
compiletest: start cargo-kani tests from a clean target directory#4614tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
Conversation
The cargo-kani test runner reuses a persistent --target-dir (`output_base_dir()/target`) across regression runs. compiletest re-runs a cargo-kani test whenever its inputs change (the stamp is derived from `kani-compiler` and the library/compiler/driver source trees), and the test then reuses whatever is left in that target directory. If the directory is in a stale or partially-built state -- e.g. left over from a regression run that was interrupted or OOM-killed mid-build, or built by an older kani-compiler -- cargo can treat a path-dependency crate as up to date while its compiled artifact is missing or incompatible. The dependent crate then fails to build with errors such as `error[E0463]: can't find crate for ...`, which do not match the test's expected output. This deterministically affected the multi-crate path-dependency tests (e.g. stubbing-do-not-resolve, stubbing-double-extern-path) and would recur on every kani rebuild until the build directory was wiped by hand. Remove the per-test target directory before invoking `cargo kani` so each run starts from a clean, reproducible state. This adds no meaningful cost: a test is only re-run when its inputs changed, in which case cargo would rebuild these crates anyway. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Ensures compiletest’s cargo-kani-based regression tests run from a clean, reproducible Cargo target directory to avoid failures caused by stale/partially-built artifacts lingering across reruns.
Changes:
- Deletes the per-test
output_base_dir()/targetdirectory before invokingcargo kani. - Adds detailed rationale explaining why persistent target dirs can cause spurious build failures (e.g., E0463).
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+286
to
+288
| let target_dir = self.output_base_dir().join("target"); | ||
| let _ = fs::remove_dir_all(&target_dir); | ||
| cargo.arg("kani").arg("--target-dir").arg(&target_dir).current_dir(parent_dir); |
Comment on lines
+272
to
+286
| // Start each run from a clean target directory. The target directory is | ||
| // persistent across regression runs and is reused whenever the test is | ||
| // re-run (e.g., after `kani-compiler` or the libraries change, which | ||
| // invalidates the test stamp). A target directory left in a stale or | ||
| // partially-built state -- for instance from a regression run that was | ||
| // interrupted or OOM-killed mid-build -- can make cargo treat a | ||
| // path-dependency crate as up-to-date while its compiled artifact is | ||
| // missing, producing spurious `can't find crate` (E0463) errors that | ||
| // don't match the expected output. This mostly affects multi-crate | ||
| // tests (those with path dependencies). Removing the directory first | ||
| // guarantees a clean, reproducible build regardless of any leftover | ||
| // state. This adds no meaningful cost: the test is only ever re-run | ||
| // when its inputs changed, in which case cargo would rebuild these | ||
| // crates anyway. | ||
| let target_dir = self.output_base_dir().join("target"); |
…age mode Address review feedback on PR model-checking#4614: - Don't silently ignore `fs::remove_dir_all` errors. A missing directory (first run) is fine, but any other failure (permissions, a held lock, ...) would leave the stale state in place and reintroduce the very non-determinism this guards against, so fail the test loudly instead. - Apply the same cleanup to the `cargo-coverage` mode (`run_cargo_coverage_test`), which reuses the same persistent `output_base_dir()/target` and is susceptible to the same stale-build failures. The logic is now shared via a `clean_cargo_target_dir` helper used by both runners. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The cargo-kani test runner reuses a persistent --target-dir (
output_base_dir()/target) across regression runs. compiletest re-runs a cargo-kani test whenever its inputs change (the stamp is derived fromkani-compilerand the library/compiler/driver source trees), and the test then reuses whatever is left in that target directory.If the directory is in a stale or partially-built state -- e.g. left over from a regression run that was interrupted or OOM-killed mid-build, or built by an older kani-compiler -- cargo can treat a path-dependency crate as up to date while its compiled artifact is missing or incompatible. The dependent crate then fails to build with errors such as
error[E0463]: can't find crate for ..., which do not match the test's expected output. This deterministically affected the multi-crate path-dependency tests (e.g. stubbing-do-not-resolve, stubbing-double-extern-path) and would recur on every kani rebuild until the build directory was wiped by hand.Remove the per-test target directory before invoking
cargo kaniso each run starts from a clean, reproducible state. This adds no meaningful cost: a test is only re-run when its inputs changed, in which case cargo would rebuild these crates anyway.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.