Add CI test for --use-local-toolchain

.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]

src/setup.rs

@@ -141,22 +141,42 @@ pub(crate) fn get_rust_toolchain_version(kani_dir: &Path) -> Result<String> {
         .context("Reading release bundle rust-toolchain-version")
 }
 
+pub(crate) fn get_rustc_version_from_build(kani_dir: &Path) -> Result<String> {
+    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<OsString>) -> Result<String> {
     // 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<String> {
+    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}");

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<String> {
+    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<P>(src: &Path, dst: &Path, predicate: P) -> Result<()>
 where