diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index bd3e145e1bce..04ac4d20280b 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -101,6 +101,106 @@ jobs: os: linux arch: x86_64-unknown-linux-gnu + test-use-local-toolchain: + name: TestLocalToolchain + needs: [build_bundle_macos, build_bundle_linux] + strategy: + matrix: + os: [macos-13, ubuntu-20.04, ubuntu-22.04] + include: + - os: macos-13 + rust_target: x86_64-apple-darwin + prev_job: ${{ needs.build_bundle_macos.outputs }} + - os: ubuntu-20.04 + rust_target: x86_64-unknown-linux-gnu + prev_job: ${{ needs.build_bundle_linux.outputs }} + - os: ubuntu-22.04 + rust_target: x86_64-unknown-linux-gnu + prev_job: ${{ needs.build_bundle_linux.outputs }} + runs-on: ${{ matrix.os }} + steps: + - name: Download bundle + uses: actions/download-artifact@v3 + with: + name: ${{ matrix.prev_job.bundle }} + + - name: Download kani-verifier crate + uses: actions/download-artifact@v3 + with: + name: ${{ matrix.prev_job.package }} + + - name: Check download + run: | + ls -lh . + + - name: Get toolchain version used to setup kani + run: | + tar zxvf ${{ matrix.prev_job.bundle }} + DATE=$(cat ./kani-latest/rust-toolchain-version | cut -d'-' -f2,3,4) + echo "Nightly date: $DATE" + echo "DATE=$DATE" >> $GITHUB_ENV + + - name: Install Kani from path + run: | + tar zxvf ${{ matrix.prev_job.package }} + cargo install --locked --path kani-verifier-${{ matrix.prev_job.crate_version }} + + - name: Create a custom toolchain directory + run: mkdir -p ${{ github.workspace }}/../custom_toolchain + + - name: Fetch the nightly tarball + run: | + echo "Downloading Rust toolchain from rust server." + curl --proto '=https' --tlsv1.2 -O https://static.rust-lang.org/dist/$DATE/rust-nightly-${{ matrix.rust_target }}.tar.gz + tar -xzf rust-nightly-${{ matrix.rust_target }}.tar.gz + ./rust-nightly-${{ matrix.rust_target }}/install.sh --prefix=${{ github.workspace }}/../custom_toolchain + + - name: Ensure installation is correct + run: | + cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }} --use-local-toolchain ${{ github.workspace }}/../custom_toolchain/ + + - name: Ensure that the rustup toolchain is not present + run: | + if [ ! -e "~/.rustup/toolchains/" ]; then + echo "Default toolchain file does not exist. Proceeding with running tests." + else + echo "::error::Default toolchain exists despite not installing." + exit 1 + fi + + - name: Checkout tests + uses: actions/checkout@v4 + + - name: Move rust-toolchain file to outside kani + run: | + mkdir -p ${{ github.workspace }}/../post-setup-tests + cp -r tests/cargo-ui ${{ github.workspace }}/../post-setup-tests + cp -r tests/kani/Assert ${{ github.workspace }}/../post-setup-tests + ls ${{ github.workspace }}/../post-setup-tests + + - name: Run cargo-kani tests after moving + run: | + for dir in function multiple-harnesses verbose; do + >&2 echo "Running test $dir" + pushd ${{ github.workspace }}/../post-setup-tests/cargo-ui/$dir + cargo kani + popd + done + + - name: Check --help and --version + run: | + >&2 echo "Running cargo kani --help and --version" + pushd ${{ github.workspace }}/../post-setup-tests/Assert + cargo kani --help && cargo kani --version + popd + + - name: Run standalone kani test + run: | + >&2 echo "Running test on file bool_ref" + pushd ${{ github.workspace }}/../post-setup-tests/Assert + kani bool_ref.rs + popd + test_bundle: name: TestBundle needs: [build_bundle_macos, build_bundle_linux] diff --git a/src/setup.rs b/src/setup.rs index 050a8e166334..730679f06c10 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -141,22 +141,42 @@ pub(crate) fn get_rust_toolchain_version(kani_dir: &Path) -> Result { .context("Reading release bundle rust-toolchain-version") } +pub(crate) fn get_rustc_version_from_build(kani_dir: &Path) -> Result { + std::fs::read_to_string(kani_dir.join("rustc-version")) + .context("Reading release bundle rustc-version") +} + /// Install the Rust toolchain version we require fn setup_rust_toolchain(kani_dir: &Path, use_local_toolchain: Option) -> Result { // Currently this means we require the bundle to have been unpacked first! let toolchain_version = get_rust_toolchain_version(kani_dir)?; - println!("[3/5] Installing rust toolchain version: {}", &toolchain_version); + let rustc_version = get_rustc_version_from_build(kani_dir)?.trim().to_string(); // Symlink to a local toolchain if the user explicitly requests if let Some(local_toolchain_path) = use_local_toolchain { let toolchain_path = Path::new(&local_toolchain_path); - // TODO: match the version against which kani was built - // Issue: https://github.com/model-checking/kani/issues/3060 - symlink_rust_toolchain(toolchain_path, kani_dir)?; - return Ok(toolchain_version); + + let custom_toolchain_rustc_version = + get_rustc_version_from_local_toolchain(local_toolchain_path.clone())?; + + if rustc_version == custom_toolchain_rustc_version { + symlink_rust_toolchain(toolchain_path, kani_dir)?; + println!( + "[3/5] Installing rust toolchain from path provided: {}", + &toolchain_path.to_string_lossy() + ); + return Ok(toolchain_version); + } else { + bail!( + "The toolchain with rustc {:?} being used to setup is not the same as the one Kani used in its release bundle {:?}. Try to setup with the same version as the bundle.", + custom_toolchain_rustc_version, + rustc_version, + ); + } } // This is the default behaviour when no explicit path to a toolchain is mentioned + println!("[3/5] Installing rust toolchain version: {}", &toolchain_version); Command::new("rustup").args(["toolchain", "install", &toolchain_version]).run()?; let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); symlink_rust_toolchain(&toolchain, kani_dir)?; @@ -189,6 +209,27 @@ fn download_filename() -> String { format!("kani-{VERSION}-{TARGET}.tar.gz") } +/// Get the version of rustc that is being used to setup kani by the user +fn get_rustc_version_from_local_toolchain(path: OsString) -> Result { + let path = Path::new(&path); + let rustc_path = path.join("bin").join("rustc"); + + let output = Command::new(rustc_path).arg("--version").output(); + + match output { + Ok(output) => { + if output.status.success() { + Ok(String::from_utf8(output.stdout).map(|s| s.trim().to_string())?) + } else { + bail!( + "Could not parse rustc version string. Toolchain installation likely invalid. " + ); + } + } + Err(_) => bail!("Could not get rustc version. Toolchain installation likely invalid"), + } +} + /// The download URL for this version of Kani fn download_url() -> String { let tag: &str = &format!("kani-{VERSION}"); diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index b94e951fe178..f65d52e03fd1 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -97,8 +97,9 @@ fn bundle_kani(dir: &Path) -> Result<()> { cp_dir(&kani_sysroot_lib(), dir)?; cp_dir(&kani_playback_lib().parent().unwrap(), dir)?; - // 5. Record the exact toolchain we use + // 5. Record the exact toolchain and rustc version we use std::fs::write(dir.join("rust-toolchain-version"), env!("RUSTUP_TOOLCHAIN"))?; + std::fs::write(dir.join("rustc-version"), get_rustc_version()?)?; // 6. Include a licensing note cp(Path::new("tools/build-kani/license-notes.txt"), dir)?; @@ -181,6 +182,13 @@ fn cp(src: &Path, dst: &Path) -> Result<()> { Ok(()) } +/// Record version of rustc being used to build Kani +fn get_rustc_version() -> Result { + let output = Command::new("rustc").arg("--version").output(); + let rustc_version = String::from_utf8(output.unwrap().stdout)?; + Ok(rustc_version) +} + /// Copy files from `src` to `dst` that respect the given pattern. pub fn cp_files

(src: &Path, dst: &Path, predicate: P) -> Result<()> where