Add CI test for --use-local-toolchain

.github/workflows/check-setup.yml

@@ -0,0 +1,191 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Job to check if the setup flow and associated flags are working as expected
+#
+# This will run everytime there's a change to main
+name: Check Setup
+on:
+  pull_request:
+  push:
+    branches:
+      - 'main'
+
+jobs:
+  build_bundle_macos:
+    name: BuildBundle-MacOs
+    runs-on: macos-13
+    permissions:
+      contents: write
+    outputs:
+      version: ${{ steps.bundle.outputs.version }}
+      bundle: ${{ steps.bundle.outputs.bundle }}
+      package: ${{ steps.bundle.outputs.package }}
+      crate_version: ${{ steps.bundle.outputs.crate_version }}
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: macos-13
+
+      - name: Build bundle
+        id: bundle
+        uses: ./.github/actions/build-bundle
+        with:
+          os: macos-13
+          arch: x86_64-apple-darwin
+
+  build_bundle_linux:
+    name: BuildBundle-Linux
+    runs-on: ubuntu-20.04
+    outputs:
+      # The bundle version (latest or the version to be released)
+      version: ${{ steps.bundle.outputs.version }}
+      bundle: ${{ steps.bundle.outputs.bundle }}
+      package: ${{ steps.bundle.outputs.package }}
+      crate_version: ${{ steps.bundle.outputs.crate_version }}
+    container:
+      # Build using ubuntu 18 due to compatibility issues with older OS.
+      image: ubuntu:18.04
+      volumes:
+        - /usr/local:/mnt/host-local
+    steps:
+
+      - name: Free up docker disk space
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          rm -r /mnt/host-local/lib/android /mnt/host-local/.ghcup
+          df -h
+
+      # This is required before checkout because the container does not
+      # have Git installed, so cannot run checkout action.
+      # The checkout action requires Git >=2.18 and python 3.7, so use the Git maintainers' PPA.
+      # and the "deadsnakes" PPA, as the default version of python on ubuntu 22.04 is Python 3.10
+      - name: Install system dependencies
+        run: |
+          apt-get update
+          apt-get install -y software-properties-common apt-utils
+          add-apt-repository ppa:git-core/ppa
+          add-apt-repository ppa:deadsnakes/ppa
+          apt-get update
+          apt-get install -y \
+            build-essential bash-completion curl lsb-release sudo g++ gcc flex \
+            bison make patch git python3.7 python3.7-dev python3.7-distutils
+          update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1
+          curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py
+          python3 get-pip.py --force-reinstall
+          rm get-pip.py
+
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-18.04
+
+      - name: Build bundle
+        id: bundle
+        uses: ./.github/actions/build-bundle
+        with:
+          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: Checkout Kani under "kani"
+        uses: actions/checkout@v4
+        with:
+          path: kani
+
+      - name: Setup Kani Dependencies
+        uses: ./kani/.github/actions/setup
+        with:
+          os: ${{ matrix.os }}
+          kani_dir: 'kani'
+
+      - name: Build Kani
+        run: cargo install --locked --path ./kani
+
+      - name: Download bundle
+        uses: actions/download-artifact@v3
+        with:
+          name: ${{ matrix.prev_job.bundle }}
+
+      - 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: |
+          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: Run cargo-kani tests
+        run: |
+          for dir in function multiple-harnesses verbose; do
+            >&2 echo "Running test $dir"
+            pushd ./tests/cargo-ui/$dir
+            cargo kani
+            popd
+          done
+
+      - name: Check --help and --version
+        run: |
+          cargo kani --help && cargo kani --version
+
+      - name: Run standalone kani test
+        run: |
+          >&2 echo "Running test on file $dir"
+          pushd ./tests/kani/$dir
+          kani bool_ref.rs
+          popd

src/setup.rs

@@ -145,18 +145,33 @@ pub(crate) fn get_rust_toolchain_version(kani_dir: &Path) -> Result<String> {
 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);
 
     // 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 build_toolchain_path = kani_dir.join("toolchain");
+        let bundle_toolchain_rustc_version = get_rustc_version(build_toolchain_path.into())?;
+        let custom_toolchain_rustc_version = get_rustc_version(local_toolchain_path.clone())?;
+
+        if bundle_toolchain_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,
+                bundle_toolchain_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 +204,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(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}");