Merge branch 'main' into synthesizer-args

.github/actions/build-bundle/action.yml

@@ -0,0 +1,92 @@
+# 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."
+inputs:
+  arch:
+    description: "Current architecture tuple"
+  os:
+    description: "Current operating system"
+outputs:
+  version:
+    description: "The bundle version (latest or =crate_version)"
+    value: ${{ steps.set_output.outputs.version }}
+  crate_version:
+    description: "The current crate version"
+    value: ${{ steps.set_output.outputs.crate_version }}
+  bundle:
+    description: "The bundle file name"
+    value: ${{ steps.set_output.outputs.bundle }}
+  package:
+    description: "The package file name"
+    value: ${{ steps.set_output.outputs.package }}
+runs:
+  using: composite
+  steps:
+    - name: Export crate version
+      shell: bash
+      run: |
+        echo "CRATE_VERSION=$(cargo pkgid | cut -d@ -f2)" >> $GITHUB_ENV
+
+    - name: Export tag version
+      shell: bash
+      if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }}
+      run: |
+        # GITHUB_REF is refs/tags/kani-0.1.0
+        echo "VERSION=$(echo ${{ github.ref }} | cut -d "-" -f 2)" >> $GITHUB_ENV
+
+    - name: Check Version
+      shell: bash
+      if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }}
+      run: |
+        # Validate git tag & Cargo.toml are in sync on version number
+        if [[ ${{ env.CRATE_VERSION }} != ${{ env.VERSION }} ]]; then
+          echo "Git tag ${{env.VERSION}} did not match crate version ${{env.CRATE_VERSION}}"
+          exit 1
+        fi
+
+    - name: Export latest version
+      shell: bash
+      if: ${{ !startsWith(github.ref, 'refs/tags/kani-') }}
+      run: |
+        echo "VERSION=latest" >> $GITHUB_ENV
+
+    - name: Build bundle
+      shell: bash
+      run: |
+        cargo bundle -- ${{ env.VERSION }}
+        echo "BUNDLE=kani-${{ env.VERSION }}-${{ inputs.arch }}.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
+
+    - name: Upload bundle
+      uses: actions/upload-artifact@v3
+      with:
+        name: ${{ env.BUNDLE }}
+        path: ${{ env.BUNDLE }}
+        if-no-files-found: error
+        # Aggressively short retention: we don't really need these
+        retention-days: 3
+
+    - name: Upload kani-verifier pkg
+      uses: actions/upload-artifact@v3
+      with:
+        name: ${{ env.PKG }}
+        path: ${{ env.PKG }}
+        if-no-files-found: error
+        # Aggressively short retention: we don't really need these
+        retention-days: 3
+
+    - name: Export output
+      shell: bash
+      id: set_output
+      run: |
+        echo "version=${{ env.VERSION }}" >> ${GITHUB_OUTPUT}
+        echo "crate_version=${{ env.CRATE_VERSION }}" >> ${GITHUB_OUTPUT}
+        echo "bundle=${{ env.BUNDLE }}" >> ${GITHUB_OUTPUT}
+        echo "package=${{ env.PKG }}" >> ${GITHUB_OUTPUT}

.github/actions/setup/action.yml

@@ -1,6 +1,7 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 name: Setup Kani Dependencies
+description: "Setup the machine to run Kani. Install rustup, dependencies and sync submodules."
 inputs:
   os:
     description: In which Operating System is this running
@@ -21,12 +22,15 @@ runs:
           sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
           df -h
 
-      - name: Install dependencies
-        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
+      - name: Install Rust toolchain
+        run: |
+          cd ${{ inputs.kani_dir }}
+          ./scripts/setup/install_rustup.sh
+          echo "$HOME/.cargo/bin" >> $GITHUB_PATH
         shell: bash
 
-      - name: Install Rust toolchain
-        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/install_rustup.sh
+      - name: Install dependencies
+        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
         shell: bash
 
       - name: Update submodules

.github/workflows/bench.yml

@@ -1,21 +1,20 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Run performance benchmarks comparing two different Kani versions.
+# This workflow takes much longer than other workflows, so we don't run it by default.
+# This workflow will run when:
+#  - Changes are pushed to 'main'.
+#  - Triggered by another workflow
 name: Kani Performance Benchmarks
 on:
   push:
     branches:
       - 'main'
-  pull_request:
-    types:
-      - labeled
+  workflow_call:
 
 jobs:
   perf-benchcomp:
-    if: ${{ github.event_name == 'push' 
-      || (github.event_name == 'pull_request' 
-         && github.event.action == 'labeled'
-         && github.event.label.name == 'Z-BenchCI')
-      }}
     runs-on: ubuntu-20.04
     steps:
       - name: Save push event HEAD and HEAD~ to environment variables
@@ -25,7 +24,7 @@ jobs:
           echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"
 
       - name: Save pull request HEAD and base to environment variables
-        if: ${{ github.event_name == 'pull_request' }}
+        if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }}
         run: |
           echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
           echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"

.github/workflows/cbmc-latest.yml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-11, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani under "kani"
         uses: actions/checkout@v3

.github/workflows/extra_jobs.yml

@@ -0,0 +1,49 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Workflow that execute jobs based on the files that were changed or some label configuration.
+#
+# The first job in this workflow will auto label the PR, while the following jobs will conditionally
+# run according to the auto-label result.
+#
+# This workflow runs on `pull_request_target` because the labeler needs extra write permission.
+# Thus, we keep this job minimal, and the only actions used are from the same verified publisher.
+#
+# Other jobs should not require extra permissions, so be careful when adding new jobs to not propagate write
+# permissions.
+#
+# Note that this also means that the workflow version run is the one currently in `main`,
+# not the one from the PR. This is only relevant if a PR is changing this workflow.
+#
+# See <https://github.com/actions/labeler/issues/121> for more details.
+
+name: Kani Extra
+on: pull_request_target
+
+jobs:
+  # Keep this job minimal since it requires extra permission
+  auto-label:
+    name: Auto Label
+    permissions:
+      contents: read
+      pull-requests: write
+    outputs:
+      all-labels: ${{ steps.labeler.outputs.all-labels }}
+      new-labels: ${{ steps.labeler.outputs.new-labels }}
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout Kani
+      uses: actions/checkout@v3
+
+    - name: Label PR
+      id: labeler
+      uses: actions/labeler@v4
+      with:
+        dot: true
+
+  verification-bench:
+    name: Verification Benchmarks
+    needs: auto-label
+    permissions: {}
+    if: contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI')
+    uses: ./.github/workflows/bench.yml

.github/workflows/kani-m1.yml

@@ -0,0 +1,30 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Run the regression job on Apple M1 only on commits to `main`
+name: Kani CI M1
+on:
+  push:
+    branches:
+      - 'main'
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  regression:
+    runs-on: macos-13-xlarge
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: macos-13-xlarge
+
+      - name: Build Kani
+        run: cargo build-dev
+
+      - name: Execute Kani regression
+        run: ./scripts/kani-regression.sh

.github/workflows/kani.yml

@@ -17,7 +17,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-11, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v3
@@ -144,123 +144,3 @@ jobs:
           branch: gh-pages
           folder: docs/book/
           single-commit: true
-
-  releasebundle-macos:
-    runs-on: ${{ matrix.os }}
-    strategy:
-      matrix:
-        os: [macos-11]
-        include:
-          - os: macos-11
-            artifact: kani-latest-x86_64-apple-darwin.tar.gz
-    steps:
-      - name: Checkout Kani
-        uses: actions/checkout@v3
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ${{ matrix.os }}
-
-      - name: Build release bundle
-        run: |
-          cargo bundle -- latest
-          cargo package -p kani-verifier
-
-      # We can't run macos in a container, so we can only test locally.
-      # Hopefully any dependency issues won't be unique to macos.
-      - name: Local install test
-        if: ${{ matrix.os == 'macos-11' }}
-        run: |
-          cargo install --path ./target/package/kani-verifier-*[^e]
-          cargo-kani setup --use-local-bundle ./${{ matrix.artifact }}
-          (cd tests/cargo-kani/simple-lib && cargo kani)
-          (cd tests/cargo-kani/simple-visualize && cargo kani)
-          (cd tests/cargo-kani/build-rs-works && cargo kani)
-
-      - name: Upload artifact
-        uses: actions/upload-artifact@v3
-        with:
-          name: ${{ matrix.artifact }}
-          path: ${{ matrix.artifact }}
-          if-no-files-found: error
-          # Aggressively short retention: we don't really need these
-          retention-days: 3
-
-  releasebundle-ubuntu:
-    runs-on: ubuntu-20.04
-    container:
-      image: ubuntu:18.04
-      volumes:
-        - /usr/local:/mnt/host-local
-    steps:
-      - name: Remove unnecessary software to free up 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, so use the Git maintainers' PPA.
-      - name: Install system dependencies
-        run: |
-          apt-get update
-          apt-get install -y software-properties-common apt-utils
-          add-apt-repository ppa:git-core/ppa
-          apt-get update
-          apt-get install -y \
-            build-essential bash-completion curl lsb-release sudo g++ gcc flex \
-            bison make patch git
-          curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL \
-            https://get.docker.com -o /tmp/install-docker.sh
-          bash /tmp/install-docker.sh
-
-      - name: Checkout Kani
-        uses: actions/checkout@v3
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-18.04
-
-      - name: Build release bundle
-        run: |
-          PATH=/github/home/.cargo/bin:$PATH cargo bundle -- latest
-          PATH=/github/home/.cargo/bin:$PATH cargo package -p kani-verifier
-
-      # -v flag: Use docker socket from host as we're running docker-in-docker
-      - name: Build container test
-        run: |
-          for tag in 20-04 20-04-alt 18-04; do
-            >&2 echo "Building test container for ${tag}"
-            docker build -t kani-$tag -f scripts/ci/Dockerfile.bundle-test-ubuntu-$tag .
-          done
-
-      - name: Run installed tests
-        run: |
-          for tag in kani-20-04 kani-20-04-alt kani-18-04; do
-            for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
-              >&2 echo "Tag $tag: running test $dir"
-              docker run -v /var/run/docker.sock:/var/run/docker.sock \
-                -w /tmp/kani/tests/cargo-kani/$dir $tag cargo kani
-            done
-            docker run -v /var/run/docker.sock:/var/run/docker.sock \
-              $tag cargo-kani setup \
-                --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
-          done
-
-          # While the above test OS issues, now try testing with nightly as
-          # default:
-          docker run -v /var/run/docker.sock:/var/run/docker.sock \
-            -w /tmp/kani/tests/cargo-kani/simple-lib kani-20-04  \
-            bash -c "rustup default nightly && cargo kani"
-
-      - name: Upload artifact
-        uses: actions/upload-artifact@v3
-        with:
-          name: kani-latest-x86_64-unknown-linux-gnu.tar.gz
-          path: kani-latest-x86_64-unknown-linux-gnu.tar.gz
-          if-no-files-found: error
-          # Aggressively short retention: we don't really need these
-          retention-days: 3