Merge remote-tracking branch 'upstream/main' into clean-comment

Author: giltho

.cargo/config.toml

@@ -1,11 +1,35 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+# Command aliases
+[alias]
+# Build kani with development configuration.
+build-dev = "run -p build-kani -- build-dev"
+# Build kani release bundle.
+bundle = "run -p build-kani -- bundle"
+
+# Constants used by different processes.
+# These constants should be evaluated during compilation via `env!()`.
+[env]
+# Path to the repository root.
+KANI_REPO_ROOT={value = "", relative = true}
+# Path to the sysroot build. This folder will contain a bin/ and a lib/ folder.
+KANI_SYSROOT ={value = "target/kani", relative = true}
+# Target for building Kani's libraries. Their configuration is different than the binary build, so we must use
+# something different than regular `target/`.
+KANI_BUILD_LIBS ={value = "target/build-libs", relative = true}
+# Build Kani library without `build-std`.
+KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true}
+
 [target.'cfg(all())']
 rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
 
     # Purposefully disabled lints
     "-Aclippy::expect_fun_call",
     "-Aclippy::or_fun_call",
     "-Aclippy::new_without_default",
+
+    # New lints that we are not compliant yet
+    "-Aclippy::needless-borrow",
+    "-Aclippy::bool-to-int-with-if",
 ]

.github/ISSUE_TEMPLATE/bug_report.md

@@ -1,8 +1,12 @@
 ---
 name: Bug Report
 about: Create a bug report for Kani
-labels: bug
+title: ''
+labels: "[C] Bug"
+assignees: ''
+
 ---
+
 <!--
 If this is a security issue, please report it following the
 [security reporting procedure](https://github.com/model-checking/kani/security/policy).

.github/ISSUE_TEMPLATE/dev-improvement.md

@@ -0,0 +1,13 @@
+---
+name: Dev Improvement
+about: 'Internal issues that track improvements that don''t affect Kani users. E.g.:
+  CI, refactoring.'
+title: ''
+labels: "[C] Internal"
+assignees: ''
+
+---
+
+**Proposed change:**
+
+**Motivation:**

.github/ISSUE_TEMPLATE/feature_request.md

@@ -1,8 +1,12 @@
 ---
 name: Feature Request
-about: Create a feature request for Kani
-labels: 
+about: Request a new feature or improvement for Kani
+title: ''
+labels: "[C] Feature / Enhancement"
+assignees: ''
+
 ---
+
 <!--
 If this is a security issue, please report it following the
 [security reporting procedure](https://github.com/model-checking/kani/security/policy).

.github/actions/setup/action.yml

@@ -17,7 +17,7 @@ runs:
         shell: bash
 
       - name: Install cbmc-viewer
-        run: ./scripts/setup/install_viewer.sh
+        run: ./scripts/setup/${{ inputs.os }}/install_viewer.sh
         shell: bash
 
       - name: Install Rust toolchain

.github/workflows/audit.yml

@@ -5,7 +5,12 @@
 # 2. Checks Rust-Sec registry for security advisories.
 
 name: Cargo Audit
-on: [pull_request]
+on:
+  pull_request:
+  push:
+    # Run on changes to branches but not tags.
+    branches:
+      - '**'
 
 jobs:
   audit:

.github/workflows/format-check.yml

@@ -1,7 +1,13 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 name: Kani Format Check
-on: pull_request
+on:
+  pull_request:
+  push:
+    # Not just any push, as that includes tags.
+    # We don't want to re-trigger this workflow when tagging an existing commit.
+    branches:
+      - '**'
 
 jobs:
   format-check:
@@ -13,7 +19,9 @@ jobs:
       - name: Execute copyright check
         run: ./scripts/ci/run-copyright-check.sh
 
+      # Ignore failures here for now until we can pindown a version.
       - name: Check C code formatting
+        continue-on-error: true
         run: ./scripts/run-clang-format.sh -d
 
       - name: Check Python code formatting

.github/workflows/kani.yml

@@ -28,7 +28,7 @@ jobs:
           os: ${{ matrix.os }}
 
       - name: Build Kani
-        run: cargo build
+        run: cargo build-dev
 
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
@@ -47,7 +47,7 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani
-        run: cargo build
+        run: cargo build-dev
 
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
@@ -64,7 +64,7 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani using release mode
-        run: cargo build --release
+        run: cargo build-dev -- --release
 
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
@@ -83,7 +83,7 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani
-        run: cargo build
+        run: cargo build-dev
 
       - name: Install book runner dependencies
         run: ./scripts/setup/install_bookrunner_deps.sh
@@ -133,7 +133,7 @@ jobs:
 
       - name: Build release bundle
         run: |
-          cargo run -p make-kani-release -- latest
+          cargo bundle -- latest
           cargo package -p kani-verifier
 
       - name: Build container test
@@ -154,6 +154,8 @@ jobs:
             docker run -w /tmp/kani/tests/cargo-kani/build-rs-works  $tag  cargo kani
             docker run $tag  cargo-kani setup --use-local-bundle ./${{ matrix.artifact }}
           done
+          # While the above test OS issues, now try testing with nightly as default:
+          docker run -w /tmp/kani/tests/cargo-kani/simple-lib  kani-20-04  bash -c "rustup default nightly && cargo kani"
 
       # We can't run macos in a container, so we can only test locally.
       # Hopefully any dependency issues won't be unique to macos.

.github/workflows/release.yml

@@ -36,11 +36,6 @@ jobs:
             echo "Git tag ${{env.TAG_VERSION}} did not match crate version ${{env.CRATE_VERSION}}"
             exit 1
           fi
-          # Check the action script's tag.
-          if ! grep -F "image: docker://ghcr.io/model-checking/kani-ubuntu-20.04:${{ env.TAG_VERSION }}" action.yml; then
-            echo "Git tag ${{env.TAG_VERSION}} did not match version in action.yml"
-            exit 1;
-          fi
 
       - name: Create release
         id: create_release
@@ -80,7 +75,7 @@ jobs:
 
       - name: Build release bundle
         run: |
-          cargo run -p make-kani-release -- ${{ needs.Release.outputs.version }}
+          cargo bundle
 
       - name: Upload artifact
         uses: actions/upload-release-asset@v1
@@ -113,7 +108,7 @@ jobs:
 
       - name: 'Build release bundle'
         run: |
-          cargo run -p make-kani-release -- ${{ needs.Release.outputs.version }}
+          cargo bundle
           cargo package -p kani-verifier
 
       - name: 'Login to GitHub Container Registry'

.github/workflows/slow-tests.yml

@@ -24,7 +24,7 @@ jobs:
           os: ${{ matrix.os }}
 
       - name: Build Kani
-        run: cargo build
+        run: cargo build-dev
 
       - name: Run Kani's slow tests
         run: ./scripts/kani-slow-tests.sh