Merge branch 'main' into issue-1233-ptr-oob

model-checking · Dec 11, 2024 · cd21766 · cd21766
2 parents fa0d1ec + db1c5fe
commit cd21766
Show file tree

Hide file tree

Showing 25 changed files with 85 additions and 93 deletions.
diff --git 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, macos-14]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04, macos-14]
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -97,7 +97,7 @@ jobs:
     needs: [build_bundle_macos, build_bundle_linux]
     strategy:
       matrix:
-        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04]
         include:
         - os: macos-13
           rust_target: x86_64-apple-darwin
@@ -108,6 +108,9 @@ jobs:
         - os: ubuntu-22.04
           rust_target: x86_64-unknown-linux-gnu
           prev_job: ${{ needs.build_bundle_linux.outputs }}
+        - os: ubuntu-24.04
+          rust_target: x86_64-unknown-linux-gnu
+          prev_job: ${{ needs.build_bundle_linux.outputs }}
     runs-on: ${{ matrix.os }}
     steps:
       - name: Download bundle
@@ -197,7 +200,7 @@ jobs:
     needs: [build_bundle_macos, build_bundle_linux]
     strategy:
       matrix:
-        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04, ubuntu-24.04]
         include:
           # Stores the output of the previous job conditional to the OS
           - prev_job: ${{ needs.build_bundle_linux.outputs }}

diff --git a/Cargo.lock b/Cargo.lock
@@ -90,9 +90,9 @@ dependencies = [
 
 [[package]]
 name = "anyhow"
-version = "1.0.93"
+version = "1.0.94"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4c95c10ba0b00a02636238b814946408b1322d5ac4760326e6fb8ec956d85775"
+checksum = "c1fd03a028ef38ba2276dce7e33fcd6369c158a1bca17946c4b1b701891c1ff7"
 
 [[package]]
 name = "arrayvec"
@@ -225,9 +225,9 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.2.2"
+version = "1.2.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f34d93e62b03caf570cccc334cbc6c2fceca82f39211051345108adcba3eebdc"
+checksum = "27f657647bcff5394bf56c7317665bbf790a137a50eaaa5c6bfbb9e27a518f2d"
 dependencies = [
  "shlex",
 ]
@@ -278,19 +278,19 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.5.21"
+version = "4.5.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fb3b4b9e5a7c7514dfa52869339ee98b3156b0bfb4e8a77c4ff4babb64b1604f"
+checksum = "3135e7ec2ef7b10c6ed8950f0f792ed96ee093fa088608f1c76e569722700c84"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.21"
+version = "4.5.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b17a95aa67cc7b5ebd32aa5370189aa0d79069ef1c64ce893bd30fb24bff20ec"
+checksum = "30582fc632330df2bd26877bde0c1f4470d57c582bbc070376afcd04d8cb4838"
 dependencies = [
  "anstream",
  "anstyle",
@@ -312,9 +312,9 @@ dependencies = [
 
 [[package]]
 name = "clap_lex"
-version = "0.7.3"
+version = "0.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "afb84c814227b90d6895e01398aee0d8033c00e7466aca416fb6a8e0eb19d8a7"
+checksum = "f46ad14479a25103f283c0f10005961cf086d8dc42205bb44c46ac563475dca6"
 
 [[package]]
 name = "colorchoice"
@@ -577,9 +577,9 @@ dependencies = [
 
 [[package]]
 name = "fastrand"
-version = "2.2.0"
+version = "2.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "486f806e73c5707928240ddc295403b1b93c96a02038563881c4a2fd84b81ac4"
+checksum = "37909eebbb50d72f9059c3b6d82c0463f2ff062c9e95845c43a6c9c0355411be"
 
 [[package]]
 name = "fixedbitset"
@@ -1397,15 +1397,15 @@ dependencies = [
 
 [[package]]
 name = "rustix"
-version = "0.38.41"
+version = "0.38.42"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d7f649912bc1495e167a6edee79151c84b1bad49748cb4f1f1167f459f6224f6"
+checksum = "f93dc38ecbab2eb790ff964bb77fa94faf256fd3e73285fd7ba0903b76bedb85"
 dependencies = [
  "bitflags",
  "errno",
  "libc",
  "linux-raw-sys",
- "windows-sys 0.52.0",
+ "windows-sys 0.59.0",
 ]
 
 [[package]]
@@ -1710,9 +1710,9 @@ dependencies = [
 
 [[package]]
 name = "time"
-version = "0.3.36"
+version = "0.3.37"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
+checksum = "35e7868883861bd0e56d9ac6efcaaca0d6d5d82a2a7ec8209ff492c07cf37b21"
 dependencies = [
  "deranged",
  "itoa",
@@ -1733,9 +1733,9 @@ checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
 
 [[package]]
 name = "time-macros"
-version = "0.2.18"
+version = "0.2.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf"
+checksum = "2834e6017e3e5e4b9834939793b282bc03b37a3336245fa820e35e233e2a85de"
 dependencies = [
  "num-conv",
  "time-core",
@@ -1752,9 +1752,9 @@ dependencies = [
 
 [[package]]
 name = "tokio"
-version = "1.41.1"
+version = "1.42.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "22cfb5bee7a6a52939ca9224d6ac897bb669134078daa8735560897f69de4d33"
+checksum = "5cec9b21b0450273377fc97bd4c33a8acffc8c996c987a7c5b319a0083707551"
 dependencies = [
  "backtrace",
  "bytes",

diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md
@@ -18,7 +18,7 @@ Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##
 
 ### Install dependencies on Ubuntu
 
-Support is available for Ubuntu 18.04, 20.04 and 22.04.
+Support is available for Ubuntu 20.04, 22.04, and 24.04.
 The simplest way to install dependencies (especially if you're using a fresh VM)
 is following our CI scripts:
 

diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
@@ -27,6 +27,7 @@ use clap::Parser;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_driver::{Callbacks, Compilation, RunCompiler};
 use rustc_interface::Config;
+use rustc_middle::ty::TyCtxt;
 use rustc_session::config::ErrorOutputType;
 use rustc_smir::rustc_internal;
 use rustc_span::ErrorGuaranteed;
@@ -124,17 +125,15 @@ impl Callbacks for KaniCompiler {
     }
 
     /// After analysis, we check the crate items for Kani API misuse or configuration issues.
-    fn after_analysis<'tcx>(
+    fn after_analysis(
         &mut self,
         _compiler: &rustc_interface::interface::Compiler,
-        rustc_queries: &'tcx rustc_interface::Queries<'tcx>,
+        tcx: TyCtxt<'_>,
     ) -> Compilation {
-        rustc_queries.global_ctxt().unwrap().enter(|tcx| {
-            rustc_internal::run(tcx, || {
-                check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm);
-            })
-            .unwrap()
-        });
+        rustc_internal::run(tcx, || {
+            check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm);
+        })
+        .unwrap();
         Compilation::Continue
     }
 }
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -673,12 +673,12 @@ fn expect_key_string_value(
     attr: &Attribute,
 ) -> Result<rustc_span::Symbol, ErrorGuaranteed> {
     let span = attr.span;
-    let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else {
+    let AttrArgs::Eq { eq_span: _, value } = &attr.get_normal_item().args else {
         return Err(sess
             .dcx()
             .span_err(span, "Expected attribute of the form #[attr = \"value\"]"));
     };
-    let maybe_str = match it {
+    let maybe_str = match value {
         AttrArgsEq::Ast(expr) => {
             if let ExprKind::Lit(tok) = expr.kind {
                 match LitKind::from_token_lit(tok) {

diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
@@ -76,7 +76,7 @@ impl Project {
         trace!(?harness.goto_file, ?expected_path, ?typ, "get_harness_artifact");
         self.artifacts.iter().find(|artifact| {
             artifact.has_type(typ)
-                && expected_path.as_ref().map_or(true, |goto_file| *goto_file == artifact.path)
+                && expected_path.as_ref().is_none_or(|goto_file| *goto_file == artifact.path)
         })
     }
 

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-11-28"
+channel = "nightly-2024-12-09"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/scripts/ci/Dockerfile.bundle-release-20-04 b/scripts/ci/Dockerfile.bundle-release-20-04
@@ -17,7 +17,7 @@ COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
 # directory. Rustup is purged for space.
 
 RUN apt-get update && \
-    apt-get install -y python3 python3-pip curl ctags && \
+    apt-get install -y curl && \
     curl -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain none && \
     (cd kani-verifier/; cargo) && \
     rustup default $(rustup toolchain list | awk '{ print $1 }') && \

diff --git a/scripts/ci/Dockerfile.bundle-test-al2 b/scripts/ci/Dockerfile.bundle-test-al2
@@ -4,7 +4,7 @@
 # Note: this file is intended only for testing the kani release bundle
 
 FROM amazonlinux:2
-RUN yum install -y gcc python3 python3-pip curl ctags tar gzip && \
+RUN yum install -y gcc curl tar gzip && \
     curl -sSf https://sh.rustup.rs | sh -s -- -y
 ENV PATH="/root/.cargo/bin:${PATH}"
 

diff --git a/scripts/ci/Dockerfile.bundle-test-nixos b/scripts/ci/Dockerfile.bundle-test-nixos
@@ -10,12 +10,9 @@ RUN echo $' \n\
 with import <nixpkgs> {}; \n\
 mkShell { \n\
   packages = [ \n\
-    ctags \n\
     curl \n\
     gcc \n\
     patchelf \n\
-    python310 \n\
-    python310Packages.pip \n\
     rustup \n\
   ]; \n\
 }' >> ./default.nix

diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04
@@ -7,7 +7,7 @@ FROM ubuntu:20.04
 ENV DEBIAN_FRONTEND=noninteractive \
     DEBCONF_NONINTERACTIVE_SEEN=true
 RUN apt-get update && \
-    apt-get install -y python3 python3-pip curl ctags && \
+    apt-get install -y curl && \
     curl -sSf https://sh.rustup.rs | sh -s -- -y
 ENV PATH="/root/.cargo/bin:${PATH}"
 

diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt
@@ -9,7 +9,7 @@ ENV DEBIAN_FRONTEND=noninteractive \
     DEBCONF_NONINTERACTIVE_SEEN=true \
     KANI_HOME="/tmp"
 RUN apt-get update && \
-    apt-get install -y python3 python3-pip curl ctags && \
+    apt-get install -y curl && \
     curl -sSf https://sh.rustup.rs | sh -s -- -y
 ENV PATH="/root/.cargo/bin:${PATH}"
 

diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04
@@ -7,7 +7,7 @@ FROM ubuntu:22.04
 ENV DEBIAN_FRONTEND=noninteractive \
     DEBCONF_NONINTERACTIVE_SEEN=true
 RUN apt-get update && \
-    apt-get install -y python3 python3-pip curl universal-ctags && \
+    apt-get install -y curl && \
     curl -sSf https://sh.rustup.rs | sh -s -- -y
 ENV PATH="/root/.cargo/bin:${PATH}"
 

diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04
@@ -0,0 +1,20 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Note: this file is intended only for testing the kani release bundle
+
+FROM ubuntu:24.04
+ENV DEBIAN_FRONTEND=noninteractive \
+    DEBCONF_NONINTERACTIVE_SEEN=true
+RUN apt-get update && \
+    apt-get install -y curl && \
+    curl -sSf https://sh.rustup.rs | sh -s -- -y
+ENV PATH="/root/.cargo/bin:${PATH}"
+
+WORKDIR /tmp/kani
+COPY ./tests ./tests
+COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./
+# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
+COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
+RUN cargo install --path ./kani-verifier
+RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh
@@ -14,7 +14,6 @@ DEPS=(
   gcc10-c++
   git
   openssl-devel
-  python3-pip
   wget
 )
 
@@ -24,9 +23,6 @@ sudo yum -y update
 sudo yum -y groupinstall "Development Tools"
 sudo yum -y install "${DEPS[@]}"
 
-# Add Python package dependencies
-python3 -m pip install autopep8
-
 # Get the directory containing this script
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 

diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh
@@ -14,9 +14,6 @@ brew update
 brew install python@3 || true
 brew link --overwrite python@3
 
-# Install dependencies via `brew`
-brew install universal-ctags wget jq
-
 # Get the directory containing this script
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 

diff --git a/scripts/setup/ubuntu-18.04 → scripts/setup/ubuntu-24.04 b/scripts/setup/ubuntu-18.04 → scripts/setup/ubuntu-24.04
diff --git a/scripts/setup/ubuntu/install_cbmc.sh b/scripts/setup/ubuntu/install_cbmc.sh
@@ -15,7 +15,7 @@ fi
 UBUNTU_VERSION=$(lsb_release -rs)
 MAJOR=${UBUNTU_VERSION%.*}
 
-if [[ "${MAJOR}" -gt "18" ]] && [[ $(dpkg --print-architecture) = "amd64" ]]
+if [[ "${MAJOR}" -ge "20" ]] && [[ $(dpkg --print-architecture) = "amd64" ]]
 then
   FILE="ubuntu-${UBUNTU_VERSION}-cbmc-${CBMC_VERSION}-Linux.deb"
   URL="https://github.com/diffblue/cbmc/releases/download/cbmc-${CBMC_VERSION}/$FILE"
@@ -29,7 +29,7 @@ then
   exit 0
 fi
 
-# There are no binaries for 18.04 or for non-x86_64, so build from source
+# There are no binaries for Ubuntu before 20.04 or for non-x86_64, so build from source
 
 WORK_DIR=$(mktemp -d)
 git clone \