Merge branch 'main' into kk-gen-docs

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,35 +1,11 @@
-
-### Description of changes: 
-
-Describe Kani's current behavior and how your code changes that behavior. If there are no issues this PR is resolving, explain why this change is necessary.
-
-### Resolved issues:
+> Please ensure your PR description includes the following:
+> 1. A description of how your changes improve Kani.
+> 2. Some context on the problem you are solving.
+> 3. A list of issues that are resolved by this PR.
+> 4. If you had to perform any manual test, please describe them.
+>
+> **Make sure you remove this list from the final PR description.**
 
 Resolves #ISSUE-NUMBER
 
-### Related RFC:
-
-<!--
-Link to the Tracking RFC issue if this work implements part of an RFC.
--->
-Optional #ISSUE-NUMBER.
-
-### Call-outs:
-
-<!-- 
-Address any potentially confusing code. Is there code added that needs to be cleaned up later? Is there code that is missing because it’s still in development? 
--->
-
-### Testing:
-
-* How is this change tested?
-
-* Is this a refactor change?
-
-### Checklist
-- [ ] Each commit message has a non-empty body, explaining why the change was made
-- [ ] Methods or procedures are documented
-- [ ] Regression or unit tests are included, or existing tests cover the modified code
-- [ ] My PR is restricted to a single feature or bugfix
-
 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

.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
@@ -12,12 +13,24 @@ inputs:
 runs:
  using: composite
  steps:
- - name: Install dependencies
- run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
+ - name: Remove unnecessary software to free up disk space
+ if: contains(fromJSON('["ubuntu-20.04","ubuntu-22.04"]'), inputs.os)
  shell: bash
+ run: |
+ # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+ df -h
+ sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+ df -h
 
  - name: Install Rust toolchain
- run: cd ${{ inputs.kani_dir }} && ./scripts/setup/install_rustup.sh
+ run: |
+ cd ${{ inputs.kani_dir }}
+ ./scripts/setup/install_rustup.sh
+ echo "$HOME/.cargo/bin" >> $GITHUB_PATH
+ shell: bash
+
+ - name: Install dependencies
+ run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
  shell: bash
 
  - name: Update submodules

.github/dependabot.yml

@@ -0,0 +1,21 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/configuration-options-for-the-dependabot.yml-file
+
+version: 2
+updates:
+ - package-ecosystem: "github-actions"
+ directory: "/"
+ schedule:
+ interval: "weekly"
+
+ - package-ecosystem: "cargo"
+ directory: "/"
+ schedule:
+ interval: "weekly"
+ groups:
+ cargo:
+ update-types:
+ - "minor"
+ - "patch"

.github/labeler.yml

@@ -0,0 +1,13 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# Configuration for auto-labeling PRs
+#
+# Note that we enable dot, so "**" matches all files in a folder
+
+Z-BenchCI:
+- any:
+ - changed-files:
+ - any-glob-to-any-file: ['kani-compiler/**', 'kani-driver/src/call-*', 'cprover_bindings/**', 'library/**']
+ - any-glob-to-any-file: ['rust-toolchain.toml', 'Cargo.lock']
+ - any-glob-to-any-file: ['kani-dependencies']

.github/workflows/audit.yml

@@ -16,7 +16,7 @@ jobs:
  audit:
  runs-on: ubuntu-latest
  steps:
- - uses: actions/checkout@v3
+ - uses: actions/checkout@v4
  - uses: EmbarkStudios/cargo-deny-action@v1
  with:
  arguments: --all-features --workspace

.github/workflows/bench.yml

@@ -0,0 +1,86 @@
+# 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'
+ workflow_call:
+
+jobs:
+ perf-benchcomp:
+ runs-on: ubuntu-20.04
+ steps:
+ - name: Save push event HEAD and HEAD~ to environment variables
+ if: ${{ github.event_name == 'push' }}
+ run: |
+ echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
+ echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"
+
+ - name: Save pull request HEAD and base to environment variables
+ 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"
+
+ - name: Check out Kani (old variant)
+ uses: actions/checkout@v4
+ with:
+ path: ./old
+ ref: ${{ env.OLD_REF }}
+ fetch-depth: 2
+
+ - name: Check out Kani (new variant)
+ uses: actions/checkout@v4
+ with:
+ path: ./new
+ ref: ${{ env.NEW_REF }}
+ fetch-depth: 1
+
+ - name: Set up Kani Dependencies (old variant)
+ uses: ./old/.github/actions/setup
+ with:
+ os: ubuntu-20.04
+ kani_dir: old
+
+ - name: Set up Kani Dependencies (new variant)
+ uses: ./new/.github/actions/setup
+ with:
+ 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/
+
+ - name: Run benchcomp
+ run: |
+ new/tools/benchcomp/bin/benchcomp \
+ --config new/tools/benchcomp/configs/perf-regression.yaml \
+ run
+ new/tools/benchcomp/bin/benchcomp \
+ --config new/tools/benchcomp/configs/perf-regression.yaml \
+ collate
+
+ - name: Perf Regression Results Table
+ run: |
+ new/tools/benchcomp/bin/benchcomp \
+ --config new/tools/benchcomp/configs/perf-regression.yaml \
+ visualize --only dump_markdown_results_table >> "$GITHUB_STEP_SUMMARY"
+
+ - name: Run other visualizations
+ run: |
+ new/tools/benchcomp/bin/benchcomp \
+ --config new/tools/benchcomp/configs/perf-regression.yaml \
+ visualize --except dump_markdown_results_table

.github/workflows/cbmc-latest.yml

@@ -19,10 +19,10 @@ 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
+ uses: actions/checkout@v4
  with:
  path: kani
 
@@ -37,7 +37,7 @@ jobs:
  run: cargo build-dev
 
  - name: Checkout CBMC under "cbmc"
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  repository: diffblue/cbmc
  path: cbmc
@@ -58,7 +58,7 @@ jobs:
  runs-on: ubuntu-20.04
  steps:
  - name: Checkout Kani under "kani"
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: kani
 
@@ -73,7 +73,7 @@ jobs:
  run: cargo build-dev -- --release
 
  - name: Checkout CBMC under "cbmc"
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  repository: diffblue/cbmc
  path: cbmc