From db88e5fa8ca870344f5c0de9e8654a27ec17a3fe Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 Jan 2025 10:49:21 +0000 Subject: [PATCH 1/6] Enable GitHub Linux/Arm runners in CI GitHub made Linux Arm 64-bit runners available: https://github.blog/changelog/2025-01-16-linux-arm64-hosted-runners-now-available-for-free-in-public-repositories-public-preview/. Run regression tests on those and build release packages. --- .github/workflows/kani.yml | 2 +- .github/workflows/release.yml | 46 ++++++++++++++++++++++++++++++----- 2 files changed, 41 insertions(+), 7 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index ad2fe757dc17..76e3e1ef8de1 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -18,7 +18,7 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04, macos-14] + os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04, macos-14, ubuntu-24.04-arm] steps: - name: Checkout Kani uses: actions/checkout@v4 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 1db596441f58..27a95b2206fd 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -92,12 +92,36 @@ jobs: os: linux arch: x86_64-unknown-linux-gnu + build_bundle_linux_arm: + name: BuildBundle-Linux-Arm + runs-on: ubuntu-24.04-arm + 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: ubuntu-24.04-arm + + - name: Build bundle + id: bundle + uses: ./.github/actions/build-bundle + with: + os: linux + arch: aarch64-unknown-linux-gnu + test-use-local-toolchain: name: TestLocalToolchain - needs: [build_bundle_macos, build_bundle_linux] + needs: [build_bundle_macos, build_bundle_linux, build_bundle_linux_arm] strategy: matrix: - os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04] + os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04, ubuntu-24.04-arm] include: - os: macos-13 rust_target: x86_64-apple-darwin @@ -111,6 +135,9 @@ jobs: - os: ubuntu-24.04 rust_target: x86_64-unknown-linux-gnu prev_job: ${{ needs.build_bundle_linux.outputs }} + - os: ubuntu-24.04-arm + rust_target: aarch64-unknown-linux-gnu + prev_job: ${{ needs.build_bundle_linux_arm.outputs }} runs-on: ${{ matrix.os }} steps: - name: Download bundle @@ -197,15 +224,17 @@ jobs: test_bundle: name: TestBundle - needs: [build_bundle_macos, build_bundle_linux] + needs: [build_bundle_macos, build_bundle_linux, build_bundle_linux_arm] strategy: matrix: - os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04] + os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04, ubuntu-24.04-arm] include: # Stores the output of the previous job conditional to the OS - prev_job: ${{ needs.build_bundle_linux.outputs }} - os: macos-13 prev_job: ${{ needs.build_bundle_macos.outputs }} + - os: ubuntu-24.04-arm + prev_job: ${{ needs.build_bundle_linux_arm.outputs }} runs-on: ${{ matrix.os }} steps: - name: Download bundle @@ -245,7 +274,7 @@ jobs: if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }} name: Release runs-on: ubuntu-20.04 - needs: [build_bundle_macos, build_bundle_macos_aarch64, build_bundle_linux, test_bundle] + needs: [build_bundle_macos, build_bundle_macos_aarch64, build_bundle_linux, build_bundle_linux_arm, test_bundle] outputs: version: ${{ steps.versioning.outputs.version }} upload_url: ${{ steps.create_release.outputs.upload_url }} @@ -285,6 +314,11 @@ jobs: with: name: ${{ needs.build_bundle_linux.outputs.bundle }} + - name: Download Linux Arm bundle + uses: actions/download-artifact@v4 + with: + name: ${{ needs.build_bundle_linux_arm.outputs.bundle }} + - name: Create release id: create_release uses: ncipollo/release-action@v1.15.0 @@ -293,7 +327,7 @@ jobs: with: name: kani-${{ env.TAG_VERSION }} tag: kani-${{ env.TAG_VERSION }} - artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }},${{ needs.build_bundle_macos_aarch64.outputs.bundle }}" + artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_linux_arm.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }},${{ needs.build_bundle_macos_aarch64.outputs.bundle }}" body: | Kani Rust verifier release bundle version ${{ env.TAG_VERSION }}. draft: true From 2ca4a316fdc2a437aba4a622f485b160000c8b32 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 Jan 2025 11:10:32 +0000 Subject: [PATCH 2/6] setup symlink --- scripts/setup/ubuntu-24.04-arm | 1 + 1 file changed, 1 insertion(+) create mode 120000 scripts/setup/ubuntu-24.04-arm diff --git a/scripts/setup/ubuntu-24.04-arm b/scripts/setup/ubuntu-24.04-arm new file mode 120000 index 000000000000..7d13753d73e8 --- /dev/null +++ b/scripts/setup/ubuntu-24.04-arm @@ -0,0 +1 @@ +ubuntu \ No newline at end of file From 757c788071fd1f9915ed07c8715d0369100509da Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 25 Jun 2025 19:01:34 +0000 Subject: [PATCH 3/6] Update CBMC dependency to 6.7.0 Kani now uses CBMC's latest release. Notably, this includes necessary fixes to improve Kani's quantifier support as well as full aarch64/Linux support, and better constant propagation (which, in turn, required adjusting the `unsupported_num_objects` test so that object creation done in a loop does not get sliced from the formula). Resolves: #4020 --- kani-dependencies | 4 ++-- .../loop-contract/struct_projection.expected | 6 +----- .../shadow/unsupported_num_objects/test.rs | 19 ++++++++++++------- ...om_raw_part_fixme.rs => from_raw_parts.rs} | 2 -- 4 files changed, 15 insertions(+), 16 deletions(-) rename tests/kani/Quantifiers/{from_raw_part_fixme.rs => from_raw_parts.rs} (94%) diff --git a/kani-dependencies b/kani-dependencies index b3667d086efa..4c91cc7b8db7 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,5 +1,5 @@ CBMC_MAJOR="6" -CBMC_MINOR="6" -CBMC_VERSION="6.6.0" +CBMC_MINOR="7" +CBMC_VERSION="6.7.0" KISSAT_VERSION="4.0.1" diff --git a/tests/expected/loop-contract/struct_projection.expected b/tests/expected/loop-contract/struct_projection.expected index e398784ef656..cb57de9f6a56 100644 --- a/tests/expected/loop-contract/struct_projection.expected +++ b/tests/expected/loop-contract/struct_projection.expected @@ -1,8 +1,4 @@ -struct_projection.loop_invariant_step.1\ - - Status: SUCCESS\ - - Description: "Check invariant after step for loop struct_projection.0" - -struct_projection.loop_invariant_step.2\ +struct_projection.loop_invariant_step.\ - Status: SUCCESS\ - Description: "Check invariant after step for loop struct_projection.0" diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index bb9233afc648..f7efb80312d7 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -10,17 +10,22 @@ static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(fals fn check_max_objects() { let mut i = 0; // A dummy loop that creates `N`` objects. - // After the loop, CBMC's object ID counter should be at `N` + 2: + // After the loop, CBMC's object ID counter should be at `N` + 3: // - `N` created in the loop + // - the NULL pointer whose object ID is 0, and - // - the object ID for `i` + // - objects for i, have_42 + let mut have_42 = false; while i < N { - let x: Box = Box::new(i); + let x: Box = Box::new(kani::any()); + if *x == 42 { + have_42 = true; + } i += 1; } - // create a new object whose ID is `N` + 2 - let x = 42; + // create a new object whose ID is `N` + 4 + let x: i32 = have_42 as i32; + assert_eq!(x, have_42 as i32); // the following call to `set` would fail if the object ID for `x` exceeds // the maximum allowed by Kani's shadow memory model unsafe { @@ -30,10 +35,10 @@ fn check_max_objects() { #[kani::proof] fn check_max_objects_pass() { - check_max_objects::<510>(); + check_max_objects::<1019>(); } #[kani::proof] fn check_max_objects_fail() { - check_max_objects::<511>(); + check_max_objects::<1020>(); } diff --git a/tests/kani/Quantifiers/from_raw_part_fixme.rs b/tests/kani/Quantifiers/from_raw_parts.rs similarity index 94% rename from tests/kani/Quantifiers/from_raw_part_fixme.rs rename to tests/kani/Quantifiers/from_raw_parts.rs index 88a711e963d1..4010554a3745 100644 --- a/tests/kani/Quantifiers/from_raw_part_fixme.rs +++ b/tests/kani/Quantifiers/from_raw_parts.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z quantifiers -//! FIXME: - use std::mem; #[kani::proof] From 2de1f4311239d7f678046b5bc2dfc92c0fe5a6af Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Jun 2025 21:11:13 +0000 Subject: [PATCH 4/6] Need to use arch+OS throughout --- .github/actions/build-bundle/action.yml | 14 ++++++-------- .github/workflows/release.yml | 12 ++++-------- 2 files changed, 10 insertions(+), 16 deletions(-) diff --git a/.github/actions/build-bundle/action.yml b/.github/actions/build-bundle/action.yml index 5a06efb4105c..84d60d77a7df 100644 --- a/.github/actions/build-bundle/action.yml +++ b/.github/actions/build-bundle/action.yml @@ -1,12 +1,10 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT name: Build bundle -description: "Build the Kani bundle for the current architecture and OS. The inputs must match the worker architecture." +description: "Build the Kani bundle for the current platform. The inputs must match the worker architecture." inputs: - arch: - description: "Current architecture tuple" - os: - description: "Current operating system" + platform: + description: "Current platform tuple" outputs: version: description: "The bundle version (latest or =crate_version)" @@ -55,14 +53,14 @@ runs: shell: bash run: | cargo bundle -- ${{ env.VERSION }} - echo "BUNDLE=kani-${{ env.VERSION }}-${{ inputs.arch }}.tar.gz" >> $GITHUB_ENV + echo "BUNDLE=kani-${{ env.VERSION }}-${{ inputs.platform }}.tar.gz" >> $GITHUB_ENV - name: Build package shell: bash run: | cargo package -p kani-verifier - mv target/package/kani-verifier-${{ env.CRATE_VERSION }}.crate ${{ inputs.os }}-kani-verifier.crate - echo "PKG=${{ inputs.os }}-kani-verifier.crate" >> $GITHUB_ENV + mv target/package/kani-verifier-${{ env.CRATE_VERSION }}.crate ${{ inputs.platform }}-kani-verifier.crate + echo "PKG=${{ inputs.platform }}-kani-verifier.crate" >> $GITHUB_ENV - name: Upload bundle uses: actions/upload-artifact@v4 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 37b15dcc14ad..a8ace3d55a33 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -41,8 +41,7 @@ jobs: id: bundle uses: ./.github/actions/build-bundle with: - os: macos-13 - arch: x86_64-apple-darwin + platform: x86_64-apple-darwin build_bundle_macos_aarch64: name: BuildBundle-MacOs-ARM @@ -65,8 +64,7 @@ jobs: id: bundle uses: ./.github/actions/build-bundle with: - os: macos-14 - arch: aarch64-apple-darwin + platform: aarch64-apple-darwin build_bundle_linux: name: BuildBundle-Linux @@ -89,8 +87,7 @@ jobs: id: bundle uses: ./.github/actions/build-bundle with: - os: linux - arch: x86_64-unknown-linux-gnu + platform: x86_64-unknown-linux-gnu build_bundle_linux_arm: name: BuildBundle-Linux-Arm @@ -113,8 +110,7 @@ jobs: id: bundle uses: ./.github/actions/build-bundle with: - os: linux - arch: aarch64-unknown-linux-gnu + platform: aarch64-unknown-linux-gnu test-use-local-toolchain: name: TestLocalToolchain From d17ceacec79726abcdb5e67e83f2c4b7748224f5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Jul 2025 10:17:22 +0000 Subject: [PATCH 5/6] Consistently use x86_64/aarch64 suffix --- .github/workflows/release.yml | 51 +++++++++++++++++++---------------- 1 file changed, 28 insertions(+), 23 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 3049a9c2bea9..ec9e842690ef 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -20,8 +20,8 @@ env: ACTIONS_ALLOW_USE_UNSECURE_NODE_VERSION: true jobs: - build_bundle_macos: - name: BuildBundle-MacOs + build_bundle_macos_x86_64: + name: BuildBundle-MacOs-x86_64 runs-on: macos-13 outputs: version: ${{ steps.bundle.outputs.version }} @@ -44,7 +44,7 @@ jobs: platform: x86_64-apple-darwin build_bundle_macos_aarch64: - name: BuildBundle-MacOs-ARM + name: BuildBundle-MacOs-aarch64 runs-on: macos-14 outputs: version: ${{ steps.bundle.outputs.version }} @@ -66,8 +66,8 @@ jobs: with: platform: aarch64-apple-darwin - build_bundle_linux: - name: BuildBundle-Linux + build_bundle_linux_x86_64: + name: BuildBundle-Linux-x86_64 runs-on: ubuntu-22.04 outputs: version: ${{ steps.bundle.outputs.version }} @@ -89,8 +89,8 @@ jobs: with: platform: x86_64-unknown-linux-gnu - build_bundle_linux_arm: - name: BuildBundle-Linux-Arm + build_bundle_linux_aarch64: + name: BuildBundle-Linux-aarch64 runs-on: ubuntu-24.04-arm outputs: version: ${{ steps.bundle.outputs.version }} @@ -114,23 +114,26 @@ jobs: test-use-local-toolchain: name: TestLocalToolchain - needs: [build_bundle_macos, build_bundle_linux, build_bundle_linux_arm] + needs: [build_bundle_macos_x86_64, build_bundle_macos_aarch64, build_bundle_linux, build_bundle_linux_arm] strategy: matrix: - os: [macos-13, ubuntu-22.04, ubuntu-24.04, ubuntu-24.04-arm] + os: [macos-13, macos-14, ubuntu-22.04, ubuntu-24.04, ubuntu-24.04-arm] include: - os: macos-13 rust_target: x86_64-apple-darwin - prev_job: ${{ needs.build_bundle_macos.outputs }} + prev_job: ${{ needs.build_bundle_macos_x86_64.outputs }} + - os: macos-14 + rust_target: aarch64-apple-darwin + prev_job: ${{ needs.build_bundle_macos_aarch64.outputs }} - os: ubuntu-22.04 rust_target: x86_64-unknown-linux-gnu - prev_job: ${{ needs.build_bundle_linux.outputs }} + prev_job: ${{ needs.build_bundle_linux_x86_64.outputs }} - os: ubuntu-24.04 rust_target: x86_64-unknown-linux-gnu - prev_job: ${{ needs.build_bundle_linux.outputs }} + prev_job: ${{ needs.build_bundle_linux_x86_64.outputs }} - os: ubuntu-24.04-arm rust_target: aarch64-unknown-linux-gnu - prev_job: ${{ needs.build_bundle_linux_arm.outputs }} + prev_job: ${{ needs.build_bundle_linux_aarch64.outputs }} runs-on: ${{ matrix.os }} steps: - name: Download bundle @@ -217,17 +220,19 @@ jobs: test_bundle: name: TestBundle - needs: [build_bundle_macos, build_bundle_linux, build_bundle_linux_arm] + needs: [build_bundle_macos_x86_64, build_bundle_macos_aarch64, build_bundle_linux_x86_64, build_bundle_linux_aarch64] strategy: matrix: - os: [macos-13, ubuntu-22.04, ubuntu-24.04, ubuntu-24.04-arm] + os: [macos-13, macos-14, ubuntu-22.04, ubuntu-24.04, ubuntu-24.04-arm] include: # Stores the output of the previous job conditional to the OS - - prev_job: ${{ needs.build_bundle_linux.outputs }} + - prev_job: ${{ needs.build_bundle_linux_x86_64.outputs }} - os: macos-13 - prev_job: ${{ needs.build_bundle_macos.outputs }} + prev_job: ${{ needs.build_bundle_macos_x86_64.outputs }} + - os: macos-14 + prev_job: ${{ needs.build_bundle_macos_aarch64.outputs }} - os: ubuntu-24.04-arm - prev_job: ${{ needs.build_bundle_linux_arm.outputs }} + prev_job: ${{ needs.build_bundle_linux_aarch64.outputs }} runs-on: ${{ matrix.os }} steps: - name: Download bundle @@ -267,7 +272,7 @@ jobs: if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }} name: Release runs-on: ubuntu-24.04 - needs: [build_bundle_macos, build_bundle_macos_aarch64, build_bundle_linux, build_bundle_linux_arm, test_bundle] + needs: [build_bundle_macos_x86_64, build_bundle_macos_aarch64, build_bundle_linux_x86_64, build_bundle_linux_aarch64, test_bundle] outputs: version: ${{ steps.versioning.outputs.version }} upload_url: ${{ steps.create_release.outputs.upload_url }} @@ -295,7 +300,7 @@ jobs: - name: Download MacOS bundle uses: actions/download-artifact@v4 with: - name: ${{ needs.build_bundle_macos.outputs.bundle }} + name: ${{ needs.build_bundle_macos_x86_64.outputs.bundle }} - name: Download MacOS ARM bundle uses: actions/download-artifact@v4 @@ -305,12 +310,12 @@ jobs: - name: Download Linux bundle uses: actions/download-artifact@v4 with: - name: ${{ needs.build_bundle_linux.outputs.bundle }} + name: ${{ needs.build_bundle_linux_x86_64.outputs.bundle }} - name: Download Linux Arm bundle uses: actions/download-artifact@v4 with: - name: ${{ needs.build_bundle_linux_arm.outputs.bundle }} + name: ${{ needs.build_bundle_linux_aarch64.outputs.bundle }} - name: Create release id: create_release @@ -320,7 +325,7 @@ jobs: with: name: kani-${{ env.TAG_VERSION }} tag: kani-${{ env.TAG_VERSION }} - artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_linux_arm.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }},${{ needs.build_bundle_macos_aarch64.outputs.bundle }}" + artifacts: "${{ needs.build_bundle_linux_x86_64.outputs.bundle }},${{ needs.build_bundle_linux_aarch64.outputs.bundle }},${{ needs.build_bundle_macos_x86_64.outputs.bundle }},${{ needs.build_bundle_macos_aarch64.outputs.bundle }}" body: | Kani Rust verifier release bundle version ${{ env.TAG_VERSION }}. draft: true From 2494e4fac8d969fa590bc3d84e5850053ba12c51 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Jul 2025 20:21:25 +0000 Subject: [PATCH 6/6] Fix cvc5 arm --- scripts/setup/ubuntu/install_deps.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh index 5e5cbc660ff7..9499d383a85e 100755 --- a/scripts/setup/ubuntu/install_deps.sh +++ b/scripts/setup/ubuntu/install_deps.sh @@ -31,7 +31,7 @@ sudo apt-get --yes update sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}" -ARCH=$(uname -m) +ARCH=$(uname -m | sed 's/aarch64/arm64/') curl -L --remote-name https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.0/cvc5-Linux-${ARCH}-static.zip sudo unzip -o -j -d /usr/local/bin cvc5-Linux-${ARCH}-static.zip cvc5-Linux-${ARCH}-static/bin/cvc5 rm cvc5-Linux-${ARCH}-static.zip