Skip to content

Commit 430fc53

Browse files
authored
Move logic to find rustup toolchain from -driver to -compiler. (rust-lang#1187)
1 parent e2b7304 commit 430fc53

File tree

10 files changed

+60
-55
lines changed

10 files changed

+60
-55
lines changed

.github/workflows/kani.yml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,7 @@ jobs:
105105
run: |
106106
docker run -w /tmp/kani/tests/cargo-kani/simple-lib kani-latest cargo kani
107107
docker run -w /tmp/kani/tests/cargo-kani/simple-visualize kani-latest cargo kani
108+
docker run -w /tmp/kani/tests/cargo-kani/build-rs-works kani-latest cargo kani
108109
109110
# We can't run macos in a container, so we can only test locally.
110111
# Hopefully any dependency issues won't be unique to macos.
@@ -115,6 +116,7 @@ jobs:
115116
cargo-kani setup --use-local-bundle ./kani-latest-x86_64-apple-darwin.tar.gz
116117
(cd tests/cargo-kani/simple-lib && cargo kani)
117118
(cd tests/cargo-kani/simple-visualize && cargo kani)
119+
(cd tests/cargo-kani/build-rs-works && cargo kani)
118120
119121
- name: Upload artifact
120122
uses: actions/upload-artifact@v3

Cargo.lock

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -361,6 +361,7 @@ dependencies = [
361361
"bitflags",
362362
"clap",
363363
"cprover_bindings",
364+
"home",
364365
"kani_metadata",
365366
"kani_queries",
366367
"libc",
@@ -381,7 +382,6 @@ dependencies = [
381382
"anyhow",
382383
"clap",
383384
"glob",
384-
"home",
385385
"kani_metadata",
386386
"serde",
387387
"serde_json",

kani-compiler/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ atty = "0.2.14"
1212
bitflags = { version = "1.0", optional = true }
1313
cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
1414
clap = "2.33.0"
15+
home = "0.5"
1516
kani_queries = {path = "kani_queries"}
1617
kani_metadata = { path = "../kani_metadata", optional = true }
1718
libc = { version = "0.2", optional = true }

kani-compiler/src/main.rs

Lines changed: 35 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -139,25 +139,13 @@ fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
139139
if let Some(extra_flags) = args.values_of_os(parser::RUSTC_OPTIONS) {
140140
extra_flags.for_each(|arg| rustc_args.push(convert_arg(arg)));
141141
}
142-
let sysroot = sysroot_path(args.value_of(parser::SYSROOT)).expect(
143-
"[Error] Invalid sysroot. Rebuild Kani or provide the path to rust sysroot using --sysroot option",
144-
);
142+
let sysroot = sysroot_path(args.value_of(parser::SYSROOT));
145143
rustc_args.push(String::from("--sysroot"));
146144
rustc_args.push(convert_arg(sysroot.as_os_str()));
147145
tracing::debug!(?rustc_args, "Compile");
148146
rustc_args
149147
}
150148

151-
/// Try to generate the rustup toolchain path.
152-
fn toolchain_path(home: Option<String>, toolchain: Option<String>) -> Option<PathBuf> {
153-
match (home, toolchain) {
154-
(Some(home), Some(toolchain)) => {
155-
Some([home, String::from("toolchains"), toolchain].iter().collect::<PathBuf>())
156-
}
157-
_ => None,
158-
}
159-
}
160-
161149
/// Convert an argument from OsStr to String.
162150
/// If conversion fails, panic with a custom message.
163151
fn convert_arg(arg: &OsStr) -> String {
@@ -166,28 +154,42 @@ fn convert_arg(arg: &OsStr) -> String {
166154
.to_string()
167155
}
168156

169-
/// Get the sysroot, following the order bellow:
170-
/// - "--sysroot" command line argument
171-
/// - compile-time environment
172-
/// - $SYSROOT
173-
/// - $RUSTUP_HOME/toolchains/$RUSTUP_TOOLCHAIN
157+
/// Get the sysroot, for our specific version of Rust nightly.
158+
///
159+
/// Rust normally finds its sysroot by looking at where itself (the `rustc`
160+
/// executable) is located. This will fail for us because we're `kani-compiler`
161+
/// and not located under the rust sysroot.
174162
///
175-
/// We currently don't support:
176-
/// - runtime environment
177-
/// - $SYSROOT
178-
/// - $RUSTUP_HOME/toolchains/$RUSTUP_TOOLCHAIN
179-
/// - rustc --sysroot
163+
/// We do know the actual name of the toolchain we need, however.
164+
/// So if we don't have `--sysroot`, then we look for our toolchain
165+
/// in the usual place for rustup.
180166
///
181-
/// since we rely on specific nightly version of rustc which may not be compatible with the workspace rustc.
182-
fn sysroot_path(sysroot_arg: Option<&str>) -> Option<PathBuf> {
183-
let path = sysroot_arg
184-
.map(PathBuf::from)
185-
.or_else(|| std::option_env!("SYSROOT").map(PathBuf::from))
186-
.or_else(|| {
187-
let home = std::option_env!("RUSTUP_HOME");
188-
let toolchain = std::option_env!("RUSTUP_TOOLCHAIN");
189-
toolchain_path(home.map(String::from), toolchain.map(String::from))
190-
});
167+
/// We previously used to pass `--sysroot` in `KANIFLAGS` from `kani-driver`,
168+
/// but this failed to have effect when building a `build.rs` file.
169+
/// This wasn't used anywhere but passing down here, so we've just migrated
170+
/// the code to find the sysroot path directly into this function.
171+
fn sysroot_path(sysroot_arg: Option<&str>) -> PathBuf {
172+
// rustup sets some environment variables during build, but this is not clearly documented.
173+
// https://github.com/rust-lang/rustup/blob/master/src/toolchain.rs (search for RUSTUP_HOME)
174+
// We're using RUSTUP_TOOLCHAIN here, which is going to be set by our `rust-toolchain.toml` file.
175+
// This is a *compile-time* constant, not a dynamic lookup at runtime, so this is reliable.
176+
let toolchain = env!("RUSTUP_TOOLCHAIN");
177+
178+
let path = if let Some(s) = sysroot_arg {
179+
PathBuf::from(s)
180+
} else {
181+
// We use the home crate to do a *runtime* determination of where rustup toolchains live
182+
let rustup = home::rustup_home().expect("Couldn't find RUSTUP_HOME");
183+
rustup.join("toolchains").join(toolchain)
184+
};
185+
// If we ever have a problem with the above not being good enough, we can consider a third heuristic
186+
// for finding our sysroot: readlink() on `../toolchain` from the location of our executable.
187+
// At time of writing this would only work for release, not development, however, so I'm not going
188+
// with this option yet. It would eliminate the need for the `home` crate however.
189+
190+
if !path.exists() {
191+
panic!("Couldn't find Kani Rust toolchain {}. Tried: {}", toolchain, path.display());
192+
}
191193
tracing::debug!(?path, ?sysroot_arg, "Sysroot path.");
192194
path
193195
}

kani-driver/Cargo.toml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@ structopt = "0.3"
1919
clap = "2.34"
2020
glob = "0.3"
2121
toml = "0.5"
22-
home = "0.5"
2322

2423
# A good set of suggested dependencies can be found in rustup:
2524
# https://github.com/rust-lang/rustup/blob/master/Cargo.toml

kani-driver/src/call_single_file.rs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -96,8 +96,6 @@ impl KaniSession {
9696
pub fn kani_rustc_flags(&self) -> Vec<OsString> {
9797
let mut flags = vec![OsString::from("--goto-c")];
9898

99-
flags.push("--sysroot".into());
100-
flags.push((&self.rust_toolchain).into());
10199
if let Some(rlib) = &self.kani_rlib {
102100
flags.push("--kani-lib".into());
103101
flags.push(rlib.into());

kani-driver/src/session.rs

Lines changed: 0 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ pub struct KaniSession {
2323
/// The location we found 'cbmc_json_parser.py'
2424
pub cbmc_json_parser_py: PathBuf,
2525

26-
/// The location we found the specific Rust toolchain we require
27-
pub rust_toolchain: PathBuf,
2826
/// The location we found our pre-built libraries
2927
pub kani_rlib: Option<PathBuf>,
3028

@@ -52,7 +50,6 @@ impl KaniSession {
5250
kani_lib_c: install.kani_lib_c()?,
5351
kani_c_stubs: install.kani_c_stubs()?,
5452
cbmc_json_parser_py: install.cbmc_json_parser_py()?,
55-
rust_toolchain: install.rust_toolchain()?,
5653
kani_rlib: install.kani_rlib()?,
5754
temporaries: RefCell::new(vec![]),
5855
})
@@ -201,21 +198,6 @@ impl InstallType {
201198
self.base_path_with("scripts/cbmc_json_parser.py")
202199
}
203200

204-
pub fn rust_toolchain(&self) -> Result<PathBuf> {
205-
// rustup sets some environment variables during build, but this is not clearly documented.
206-
// https://github.com/rust-lang/rustup/blob/master/src/toolchain.rs (search for RUSTUP_HOME)
207-
// We're using RUSTUP_TOOLCHAIN here, which is going to be set by our `rust-toolchain.toml` file.
208-
// This is a compile-time constant, not a dynamic lookup at runtime, so this is reliable.
209-
let toolchain = env!("RUSTUP_TOOLCHAIN");
210-
// We use the home crate to do a *runtime* determination of where rustup toolchains live
211-
let path = home::rustup_home()?.join("toolchains").join(toolchain);
212-
if path.as_path().exists() {
213-
Ok(path)
214-
} else {
215-
bail!("Unable to find rust toolchain {}. Looked for {}", toolchain, path.display());
216-
}
217-
}
218-
219201
pub fn kani_rlib(&self) -> Result<Option<PathBuf>> {
220202
match self {
221203
Self::DevRepo(_repo) => {
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
[package]
4+
name = "build-rs-works"
5+
version = "0.1.0"
6+
edition = "2021"
7+
8+
[dependencies]
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
fn main() {
5+
println!("cargo:rustc-env=SET_IN_BUILD_RS=Y");
6+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
#[kani::proof]
5+
fn check() {
6+
assert!(env!("SET_IN_BUILD_RS") == "Y");
7+
}

0 commit comments

Comments
 (0)