Skip to content

Derive the cargo output directory from cargo's reported artifacts - #4766

Merged
feliperodri merged 1 commit into
model-checking:mainfrom
feliperodri:fix-cargo-target-layout
Aug 27, 2026
Merged

Derive the cargo output directory from cargo's reported artifacts#4766
feliperodri merged 1 commit into
model-checking:mainfrom
feliperodri:fix-cargo-target-layout

Conversation

@feliperodri

Copy link
Copy Markdown
Member

Description

cargo_build hardcoded the compiler output directory as target/kani/<triple>/debug/deps, and cargo_project then canonicalized it. That layout is cargo's to choose, and cargo 1.99 changes it: artifacts no longer share debug/deps — each package gets its own debug/build/PKG/HASH/out/ — so debug/deps is never created and the canonicalize fails:

error: No such file or directory (os error 2)

Artifact discovery was already layout-agnostic: map_kani_artifact derives every path from the filenames that cargo reports. The hardcoded directory was the only thing tying the driver to the old layout.

This PR:

  • Derives CargoOutputs::outdir from the discovered artifacts instead of assuming a path.
  • Drops the canonicalize in cargo_project. An artifact path is canonical already (Artifact::try_new canonicalizes), and the no-artifacts fallback names a directory cargo had no reason to create — canonicalizing it turns a benign case into a hard error.
  • Makes two tests layout-agnostic: check-output searches the target directory for its --gen-c output, and cargo_playback_opts asserts only the file name of the executable whose path cargo itself reports.

Note that with cargo 1.99 a multi-package build no longer has a single output directory. outdir names one of them; it feeds only the output_dir field of the -Z unstable-options JSON frontend, and previously named a directory that under 1.99 does not exist at all. The doc comment says so explicitly.

The layout change, confirmed locally on nightly-2026-08-01 (cargo 1.99.0-nightly):

# cargo 1.97
target/kani/<triple>/debug/deps/<pkg>-<hash>.kani-metadata.json

# cargo 1.99 -- one directory per package, no debug/deps at all
target/kani/<triple>/debug/build/<pkg>/<hash>/out/<pkg>-<hash>.kani-metadata.json

Why this is a standalone PR

This unblocks the toolchain upgrade chain. It has no dependency on any toolchain bump and is behaviour-preserving on the current toolchain, so it can land on its own. The intended order is #4760 (2026-06-01) → #4764 (2026-07-01) → this PR → the 2026-08-01 bump, which is blocked on it.

Testing

On the current toolchain (nightly-2026-05-01, cargo 1.97 — old layout):

  • cargo-kani: 71 passed, 0 failed
  • script-based-pre: 70 passed, 2 failed — both failures (cargo_autoharness_filter, cargo_autoharness_slices) reproduce on unmodified main and are unrelated to this change
  • cargo test -p kani-driver: 93 passed
  • ./scripts/kani-fmt.sh --check, cargo clippy --workspace --tests -- -D warnings, RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings: clean

Cherry-picked onto the local 2026-08-01 branch (cargo 1.99 — new layout), which is where the bug bites:

Suite Before After
cargo-kani 68 failed 71 passed, 0 failed
script-based-pre 11 failed 68 passed, 0 failed
  • Was this change tested? Yes
  • Is this a breaking change? No

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

`cargo_build` hardcoded the compiler output directory as
`target/kani/<triple>/debug/deps`, and `cargo_project` then canonicalized
it -- so any layout that does not match becomes
`error: No such file or directory (os error 2)`.

That layout is cargo's to choose, and cargo 1.99 changes it: artifacts no
longer share `debug/deps`, each package getting its own
`debug/build/PKG/HASH/out/` instead. Artifact discovery was already
layout-agnostic (`map_kani_artifact` derives every path from the
`filenames` cargo reports), so the hardcoded directory was the only thing
tying the driver to the old layout.

Derive it from the discovered artifacts instead, and drop the
canonicalization: an artifact path is canonical already, and the
no-artifacts fallback names a directory cargo had no reason to create.

Two tests hardcoded the same layout and are now layout-agnostic:
`check-output` searches the target directory for its `--gen-c` output, and
`cargo_playback_opts` asserts only the file name of the executable whose
path cargo reports.
@feliperodri
feliperodri requested review from a team as code owners August 26, 2026 23:11
@github-actions github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 26, 2026
@feliperodri
feliperodri enabled auto-merge August 27, 2026 00:55
@feliperodri
feliperodri added this pull request to the merge queue Aug 27, 2026
Merged via the queue into model-checking:main with commit a505b41 Aug 27, 2026
33 checks passed
@feliperodri
feliperodri deleted the fix-cargo-target-layout branch August 27, 2026 18:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants