Warn when the CBMC on PATH does not match the pinned version - #4723
Open
ivmat wants to merge 1 commit into
Open
Conversation
…sion
`kani-dependencies` pins the CBMC version, but that pin was only enforced at setup/CI time by
`install_deps.sh` / `kani-regression.sh`. At runtime `kani-driver` used whatever `cbmc` it resolved
from `PATH` with no check, so a locally installed, unpinned CBMC could silently diverge from the pin
while every log claimed the pinned toolchain was in use.
`kani-driver` now resolves the CBMC version actually on `PATH` via `cbmc --version`, compares it
against the pin, and warns naming both versions when they differ. The pin is embedded at compile time
with `include_str!("../../kani-dependencies")` rather than read from the install root at runtime:
release bundles do not ship `kani-dependencies`, so a runtime read would silently disable the check
for exactly the users least able to audit their own toolchain. Embedding also removes the
dev-repo/release asymmetry entirely, and rustc tracks the included file as a build dependency, so
editing the pin still triggers a rebuild.
`--version` is handled explicitly rather than by clap's generated flag (`disable_version_flag`), so
that `kani --version` and `cargo kani --version` actually perform this check. Previously clap
intercepted the flag and exited before the driver ran, which would have made "check `--version`
before a campaign" useless advice. The explicit path preserves clap's conventional first line
(`kani <version>` / `cargo-kani <version>`) so scripts that parse it -- including the two
script-based version regression tests -- keep working, and appends the CBMC lines after it.
For `cargo kani`, the flag is detected by scanning the raw arguments before any project
configuration is merged, so `--version` cannot be broken by a malformed `Cargo.toml` -- matching the
robustness of clap's built-in, whose version action previously fired inside
`cargo_locate_project`'s early parse, before any TOML was read. The scan matches whole arguments
only and stops at `--` or `--cbmc-args` (everything beyond those belongs to CBMC, not Kani); a
post-parse fallback catches spellings the scan cannot see, such as `-V` clustered with other short
flags. Known residual: a clustered `-V` combined with a malformed `Cargo.toml` reports the TOML
error instead of the version -- loudly, not silently.
The check is deliberately not emitted under `--quiet` during verification, preserving the
zero-output contract asserted by `tests/script-based-pre/check-quiet/check-quiet.sh`; `--version`
is an explicit one-shot query, not verification output, so it reports regardless.
Note for reviewers: `tools/build-kani` bundles whichever `cbmc` is on the builder's `PATH`
(`which::which("cbmc")`), which is the build-time analogue of the same problem. That is left as a
follow-up to keep this change focused; with this check in place a mismatched bundle now at least
reports itself at runtime.
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.
Description
kani-dependenciespins a CBMC version, but the pin is only enforced at setup/CI time (install_deps.sh,kani-regression.sh). At runtimekani-driveruses whatevercbmcresolves fromPATHwith no check, so a locally installed CBMC can silently diverge from the pin while the user believes the pinned toolchain is in use. On a machine with several CBMC versions installed this is easy to hit and invisible when it happens — results get attributed to a toolchain that never ran.This PR makes
kani-driverresolvecbmc --versionfromPATH, compare it against the pin, and warn naming both versions when they differ. Design points:include_str!ofkani-dependencies) rather than read at runtime: release bundles don't ship that file, so a runtime read would silently disable the check for exactly the users least able to audit their toolchain. rustc tracks the included file, so editing the pin still rebuilds.--versionis handled explicitly (disable_version_flag) sokani --version/cargo kani --versionactually run the check — clap's built-in flag exits during parsing, before any driver code runs. The first output line stayskani <version>/cargo-kani <version>, so scripts that parse it keep working; the CBMC lines are appended after it.cargo kani, the version flag is detected on the raw arguments before project configuration is merged, so--versioncannot be broken by a malformedCargo.toml(matching the robustness of clap's built-in, whose version action previously fired insidecargo_locate_project's early parse). The scan matches whole arguments only and stops at--or--cbmc-args; a post-parse fallback catches spellings the scan cannot see, such as-Vclustered with other short flags. Known residual: a clustered-Vcombined with a malformedCargo.tomlreports the TOML error instead of the version — loudly, not silently.--quietduring verification (preserving the zero-output contract incheck-quiet.sh), but--versionas an explicit query always reports.tools/build-kanibundling whichevercbmcis on the builder'sPATHis the build-time analogue of the same problem; left as a follow-up to keep this focused. With this check, a mismatched bundle at least reports itself at runtime.Manual testing
Unit tests cover the version parse/compare and the raw
--versionscan. Verified live both ways — a matching CBMC 6.10.0 is silent, a mismatched 6.8.0 fires naming both versions. Both script-based version regression tests (kani-version-flag-version,cargo-kani-version-flag-version) pass.cargo kani --versionverified to work from a directory whoseCargo.tomlis malformed, and a--versionafter--cbmc-argsis forwarded to CBMC, not intercepted.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.