Merge remote-tracking branch 'origin/main' into issue-2998-ub-rfc

Conflicts: - rfc/src/SUMMARY.md
model-checking · Jun 28, 2024 · 5185c04 · 5185c04
2 parents aef9cb8 + 5a6a5f3
commit 5185c04
Show file tree

Hide file tree

Showing 561 changed files with 10,432 additions and 10,312 deletions.
diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml
@@ -55,12 +55,6 @@ jobs:
           os: ubuntu-20.04
           kani_dir: new
 
-      - name: Build Kani (new variant)
-        run: pushd new && cargo build-dev
-
-      - name: Build Kani (old variant)
-        run: pushd old && cargo build-dev
-
       - name: Copy benchmarks from new to old
         run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
 

diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml
@@ -32,10 +32,6 @@ jobs:
           os: ${{ matrix.os }}
           kani_dir: 'kani'
 
-      - name: Build Kani
-        working-directory: ./kani
-        run: cargo build-dev
-
       - name: Checkout CBMC under "cbmc"
         uses: actions/checkout@v4
         with:

diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml
@@ -30,7 +30,7 @@ jobs:
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
-          grep ^CBMC_VERSION kani-dependencies >> $GITHUB_ENV
+          grep ^CBMC_VERSION kani-dependencies | sed 's/"//g' >> $GITHUB_ENV
           CBMC_LATEST=$(gh -R diffblue/cbmc release list | grep Latest | awk '{print $1}' | cut -f2 -d-)
           echo "CBMC_LATEST=$CBMC_LATEST" >> $GITHUB_ENV
           # check whether the version has changed at all
@@ -47,8 +47,8 @@ jobs:
           elif ! git ls-remote --exit-code origin cbmc-$CBMC_LATEST ; then
             CBMC_LATEST_MAJOR=$(echo $CBMC_LATEST | cut -f1 -d.)
             CBMC_LATEST_MINOR=$(echo $CBMC_LATEST | cut -f2 -d.)
-            sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_MAJOR\"/" kani-dependencies
-            sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_MINOR\"/" kani-dependencies
+            sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_LATEST_MAJOR\"/" kani-dependencies
+            sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_LATEST_MINOR\"/" kani-dependencies
             sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies
             git diff
             if ! ./scripts/kani-regression.sh ; then
@@ -79,7 +79,7 @@ jobs:
           token: ${{ github.token }}
           title: 'CBMC upgrade to ${{ env.CBMC_LATEST }} failed'
           body: >
-            Updating CBMC from ${{ evn.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
+            Updating CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
 
             The failed automated run
             [can be found here.](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }})
diff --git a/.github/workflows/kani-m1.yml b/.github/workflows/kani-m1.yml
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04, macos-14]
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
@@ -27,9 +27,6 @@ jobs:
         with:
           os: ${{ matrix.os }}
 
-      - name: Build Kani
-        run: cargo build-dev
-
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
@@ -88,47 +85,19 @@ jobs:
         with:
           os: ubuntu-20.04
 
-      - name: Build Kani using release mode
-        run: cargo build-dev -- --release
-
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
         env:
           RUST_TEST_THREADS: 1
 
-  bookrunner:
+  documentation:
     runs-on: ubuntu-20.04
     permissions:
       contents: write
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
 
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        run: cargo build-dev
-
-      - name: Install book runner dependencies
-        run: ./scripts/setup/install_bookrunner_deps.sh
-
-      - name: Generate book runner report
-        run: cargo run -p bookrunner
-        env:
-          DOC_RUST_LANG_ORG_CHANNEL: nightly
-
-      - name: Print book runner text results
-        run: cat build/output/latest/html/bookrunner.txt
-
-      - name: Print book runner failures grouped by stage
-        run: python3 scripts/ci/bookrunner_failures_by_stage.py build/output/latest/html/index.html
-
-      - name: Detect unexpected book runner failures
-        run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt
-
       - name: Install book dependencies
         run: ./scripts/setup/ubuntu/install_doc_deps.sh
 

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -44,6 +44,32 @@ jobs:
           os: macos-13
           arch: x86_64-apple-darwin
 
+  build_bundle_macos_aarch64:
+    name: BuildBundle-MacOs-ARM
+    runs-on: macos-14
+    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-14
+
+      - name: Build bundle
+        id: bundle
+        uses: ./.github/actions/build-bundle
+        with:
+          os: macos-14
+          arch: aarch64-apple-darwin
+
   build_bundle_linux:
     name: BuildBundle-Linux
     runs-on: ubuntu-20.04
@@ -82,7 +108,7 @@ jobs:
             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
+          curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py
           python3 get-pip.py --force-reinstall
           rm get-pip.py
 
@@ -101,6 +127,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-${{ matrix.prev_job.version }}/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 supported-lib-types/rlib 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]
@@ -284,7 +410,7 @@ jobs:
           OWNER: '${{ github.repository_owner }}'
 
       - name: Build and push
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           file: scripts/ci/Dockerfile.bundle-release-20-04

diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml
@@ -30,42 +30,11 @@ jobs:
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
-          current_toolchain_date=$(grep ^channel rust-toolchain.toml | sed 's/.*nightly-\(.*\)"/\1/')
-          echo "current_toolchain_date=$current_toolchain_date" >> $GITHUB_ENV
-          current_toolchain_epoch=$(date --date $current_toolchain_date +%s)
-          next_toolchain_date=$(date --date "@$(($current_toolchain_epoch + 86400))" +%Y-%m-%d)
-          echo "next_toolchain_date=$next_toolchain_date" >> $GITHUB_ENV
-          if gh issue list -S \
-              "Toolchain upgrade to nightly-$next_toolchain_date failed" \
-              --json number,title | grep title ; then
-            echo "next_step=none" >> $GITHUB_ENV
-          elif ! git ls-remote --exit-code origin toolchain-$next_toolchain_date ; then
-            echo "next_step=create_pr" >> $GITHUB_ENV
-            sed -i "/^channel/ s/$current_toolchain_date/$next_toolchain_date/" rust-toolchain.toml
-            git diff
-            git clone --filter=tree:0 https://github.com/rust-lang/rust rust.git
-            cd rust.git
-            current_toolchain_hash=$(curl https://static.rust-lang.org/dist/$current_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
-            echo "current_toolchain_hash=$current_toolchain_hash" >> $GITHUB_ENV
-            next_toolchain_hash=$(curl https://static.rust-lang.org/dist/$next_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
-            echo "next_toolchain_hash=$next_toolchain_hash" >> $GITHUB_ENV
-            EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64)
-            echo "git_log<<$EOF" >> $GITHUB_ENV
-            git log --oneline $current_toolchain_hash..$next_toolchain_hash | \
-              sed 's#^#https://github.com/rust-lang/rust/commit/#' >> $GITHUB_ENV
-            echo "$EOF" >> $GITHUB_ENV
-            cd ..
-            rm -rf rust.git
-            if ! cargo build-dev ; then
-              echo "next_step=create_issue" >> $GITHUB_ENV
-            else
-              if ! ./scripts/kani-regression.sh ; then
-                echo "next_step=create_issue" >> $GITHUB_ENV
-              fi
-            fi
-          else
-            echo "next_step=none" >> $GITHUB_ENV
-          fi
+          source scripts/toolchain_update.sh
+
+      - name: Clean untracked files
+        run: git clean -f
+
       - name: Create Pull Request
         if: ${{ env.next_step == 'create_pr' }}
         uses: peter-evans/create-pull-request@v6

diff --git a/.gitignore b/.gitignore
@@ -48,6 +48,10 @@ no_llvm_build
 /tmp/
 # Created by default with `src/ci/docker/run.sh`
 /obj/
+# Created by kani-compiler
+*.rlib
+*.rmeta
+*.mir
 
 ## Temporary files
 *~
@@ -74,10 +78,8 @@ package-lock.json
 tests/rustdoc-gui/src/**.lock
 
 # Before adding new lines, see the comment at the top.
-/.litani_cache_dir
 /.ninja_deps
 /.ninja_log
-/tests/bookrunner
 *Cargo.lock
 tests/kani-dependency-test/diamond-dependency/build
 tests/kani-multicrate/type-mismatch/mismatch/target

diff --git a/.gitmodules b/.gitmodules
@@ -1,12 +1,3 @@
-[submodule "src/doc/nomicon"]
-	path = tools/bookrunner/rust-doc/nomicon
-	url = https://github.com/rust-lang/nomicon.git
-[submodule "src/doc/reference"]
-	path = tools/bookrunner/rust-doc/reference
-	url = https://github.com/rust-lang/reference.git
-[submodule "src/doc/rust-by-example"]
-	path = tools/bookrunner/rust-doc/rust-by-example
-	url = https://github.com/rust-lang/rust-by-example.git
 [submodule "firecracker"]
 	path = firecracker
 	url = https://github.com/firecracker-microvm/firecracker.git