Merge branch 'main' into issue-1162-toolchain

.github/workflows/kani.yml

@@ -105,6 +105,7 @@ jobs:
         run: |
           docker run -w /tmp/kani/tests/cargo-kani/simple-lib  kani-latest  cargo kani
           docker run -w /tmp/kani/tests/cargo-kani/simple-visualize  kani-latest  cargo kani
+          docker run -w /tmp/kani/tests/cargo-kani/build-rs-works  kani-latest  cargo kani
 
       # We can't run macos in a container, so we can only test locally.
       # Hopefully any dependency issues won't be unique to macos.
@@ -115,6 +116,7 @@ jobs:
           cargo-kani setup --use-local-bundle ./kani-latest-x86_64-apple-darwin.tar.gz
           (cd tests/cargo-kani/simple-lib && cargo kani)
           (cd tests/cargo-kani/simple-visualize && cargo kani)
+          (cd tests/cargo-kani/build-rs-works && cargo kani)
 
       - name: Upload artifact
         uses: actions/upload-artifact@v3

Cargo.lock

@@ -361,6 +361,7 @@ dependencies = [
  "bitflags",
  "clap",
  "cprover_bindings",
+ "home",
  "kani_metadata",
  "kani_queries",
  "libc",
@@ -381,7 +382,6 @@ dependencies = [
  "anyhow",
  "clap",
  "glob",
- "home",
  "kani_metadata",
  "serde",
  "serde_json",

docs/src/install-guide.md

@@ -17,7 +17,7 @@ Currently, only two platforms are supported:
 
 The following must already be installed:
 
-* **Python version 3.6 or greater.**
+* **Python version 3.8 or greater** and the package installer pip.
 * Rust installed via `rustup`
 * `ctags` is required for Kani's `--visualize` option to work correctly.
 

kani-compiler/Cargo.toml

@@ -12,6 +12,7 @@ atty = "0.2.14"
 bitflags = { version = "1.0", optional = true }
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = "2.33.0"
+home = "0.5"
 kani_queries = {path = "kani_queries"}
 kani_metadata = { path = "../kani_metadata", optional = true }
 libc = { version = "0.2", optional = true }

kani-compiler/src/main.rs

@@ -139,25 +139,13 @@ fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
     if let Some(extra_flags) = args.values_of_os(parser::RUSTC_OPTIONS) {
         extra_flags.for_each(|arg| rustc_args.push(convert_arg(arg)));
     }
-    let sysroot = sysroot_path(args.value_of(parser::SYSROOT)).expect(
-        "[Error] Invalid sysroot. Rebuild Kani or provide the path to rust sysroot using --sysroot option",
-    );
+    let sysroot = sysroot_path(args.value_of(parser::SYSROOT));
     rustc_args.push(String::from("--sysroot"));
     rustc_args.push(convert_arg(sysroot.as_os_str()));
     tracing::debug!(?rustc_args, "Compile");
     rustc_args
 }
 
-/// Try to generate the rustup toolchain path.
-fn toolchain_path(home: Option<String>, toolchain: Option<String>) -> Option<PathBuf> {
-    match (home, toolchain) {
-        (Some(home), Some(toolchain)) => {
-            Some([home, String::from("toolchains"), toolchain].iter().collect::<PathBuf>())
-        }
-        _ => None,
-    }
-}
-
 /// Convert an argument from OsStr to String.
 /// If conversion fails, panic with a custom message.
 fn convert_arg(arg: &OsStr) -> String {
@@ -166,28 +154,42 @@ fn convert_arg(arg: &OsStr) -> String {
         .to_string()
 }
 
-/// Get the sysroot, following the order bellow:
-/// - "--sysroot" command line argument
-/// - compile-time environment
-///    - $SYSROOT
-///    - $RUSTUP_HOME/toolchains/$RUSTUP_TOOLCHAIN
+/// Get the sysroot, for our specific version of Rust nightly.
+///
+/// Rust normally finds its sysroot by looking at where itself (the `rustc`
+/// executable) is located. This will fail for us because we're `kani-compiler`
+/// and not located under the rust sysroot.
 ///
-/// We currently don't support:
-/// - runtime environment
-///    - $SYSROOT
-///    - $RUSTUP_HOME/toolchains/$RUSTUP_TOOLCHAIN
-/// - rustc --sysroot
+/// We do know the actual name of the toolchain we need, however.
+/// So if we don't have `--sysroot`, then we look for our toolchain
+/// in the usual place for rustup.
 ///
-/// since we rely on specific nightly version of rustc which may not be compatible with the workspace rustc.
-fn sysroot_path(sysroot_arg: Option<&str>) -> Option<PathBuf> {
-    let path = sysroot_arg
-        .map(PathBuf::from)
-        .or_else(|| std::option_env!("SYSROOT").map(PathBuf::from))
-        .or_else(|| {
-            let home = std::option_env!("RUSTUP_HOME");
-            let toolchain = std::option_env!("RUSTUP_TOOLCHAIN");
-            toolchain_path(home.map(String::from), toolchain.map(String::from))
-        });
+/// We previously used to pass `--sysroot` in `KANIFLAGS` from `kani-driver`,
+/// but this failed to have effect when building a `build.rs` file.
+/// This wasn't used anywhere but passing down here, so we've just migrated
+/// the code to find the sysroot path directly into this function.
+fn sysroot_path(sysroot_arg: Option<&str>) -> PathBuf {
+    // rustup sets some environment variables during build, but this is not clearly documented.
+    // https://github.com/rust-lang/rustup/blob/master/src/toolchain.rs (search for RUSTUP_HOME)
+    // We're using RUSTUP_TOOLCHAIN here, which is going to be set by our `rust-toolchain.toml` file.
+    // This is a *compile-time* constant, not a dynamic lookup at runtime, so this is reliable.
+    let toolchain = env!("RUSTUP_TOOLCHAIN");
+
+    let path = if let Some(s) = sysroot_arg {
+        PathBuf::from(s)
+    } else {
+        // We use the home crate to do a *runtime* determination of where rustup toolchains live
+        let rustup = home::rustup_home().expect("Couldn't find RUSTUP_HOME");
+        rustup.join("toolchains").join(toolchain)
+    };
+    // If we ever have a problem with the above not being good enough, we can consider a third heuristic
+    // for finding our sysroot: readlink() on `../toolchain` from the location of our executable.
+    // At time of writing this would only work for release, not development, however, so I'm not going
+    // with this option yet. It would eliminate the need for the `home` crate however.
+
+    if !path.exists() {
+        panic!("Couldn't find Kani Rust toolchain {}. Tried: {}", toolchain, path.display());
+    }
     tracing::debug!(?path, ?sysroot_arg, "Sysroot path.");
     path
 }

kani-driver/Cargo.toml

@@ -19,7 +19,6 @@ structopt = "0.3"
 clap = "2.34"
 glob = "0.3"
 toml = "0.5"
-home = "0.5"
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml

kani-driver/src/call_single_file.rs

@@ -96,8 +96,6 @@ impl KaniSession {
     pub fn kani_rustc_flags(&self) -> Vec<OsString> {
         let mut flags = vec![OsString::from("--goto-c")];
 
-        flags.push("--sysroot".into());
-        flags.push((&self.rust_toolchain).into());
         if let Some(rlib) = &self.kani_rlib {
             flags.push("--kani-lib".into());
             flags.push(rlib.into());

kani-driver/src/session.rs

@@ -23,8 +23,6 @@ pub struct KaniSession {
     /// The location we found 'cbmc_json_parser.py'
     pub cbmc_json_parser_py: PathBuf,
 
-    /// The location we found the specific Rust toolchain we require
-    pub rust_toolchain: PathBuf,
     /// The location we found our pre-built libraries
     pub kani_rlib: Option<PathBuf>,
 
@@ -52,7 +50,6 @@ impl KaniSession {
             kani_lib_c: install.kani_lib_c()?,
             kani_c_stubs: install.kani_c_stubs()?,
             cbmc_json_parser_py: install.cbmc_json_parser_py()?,
-            rust_toolchain: install.rust_toolchain()?,
             kani_rlib: install.kani_rlib()?,
             temporaries: RefCell::new(vec![]),
         })
@@ -201,21 +198,6 @@ impl InstallType {
         self.base_path_with("scripts/cbmc_json_parser.py")
     }
 
-    pub fn rust_toolchain(&self) -> Result<PathBuf> {
-        // rustup sets some environment variables during build, but this is not clearly documented.
-        // https://github.com/rust-lang/rustup/blob/master/src/toolchain.rs (search for RUSTUP_HOME)
-        // We're using RUSTUP_TOOLCHAIN here, which is going to be set by our `rust-toolchain.toml` file.
-        // This is a compile-time constant, not a dynamic lookup at runtime, so this is reliable.
-        let toolchain = env!("RUSTUP_TOOLCHAIN");
-        // We use the home crate to do a *runtime* determination of where rustup toolchains live
-        let path = home::rustup_home()?.join("toolchains").join(toolchain);
-        if path.as_path().exists() {
-            Ok(path)
-        } else {
-            bail!("Unable to find rust toolchain {}. Looked for {}", toolchain, path.display());
-        }
-    }
-
     pub fn kani_rlib(&self) -> Result<Option<PathBuf>> {
         match self {
             Self::DevRepo(_repo) => {

src/lib.rs

@@ -152,7 +152,7 @@ fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
 
     // TODO: this is a repetition of versions from elsewhere
     Command::new("python3")
-        .args(&["-m", "pip", "install", "cbmc-viewer==2.11", "--target"])
+        .args(&["-m", "pip", "install", "cbmc-viewer==3.2", "--target"])
         .arg(&pyroot)
         .run()?;
     Command::new("python3")

tests/cargo-kani/build-rs-works/Cargo.toml

@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "build-rs-works"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tests/cargo-kani/build-rs-works/build.rs

@@ -0,0 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    println!("cargo:rustc-env=SET_IN_BUILD_RS=Y");
+}

tests/cargo-kani/build-rs-works/src/lib.rs

@@ -0,0 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn check() {
+    assert!(env!("SET_IN_BUILD_RS") == "Y");
+}