diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index c7444754e53b9..1c8011bbe6de7 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -117,8 +117,10 @@ jobs: - name: Build container test if: ${{ matrix.os == 'ubuntu-18.04' }} run: | - docker build -t kani-20-04 -f scripts/ci/Dockerfile.bundle-test-20-04 . - docker build -t kani-18-04 -f scripts/ci/Dockerfile.bundle-test-18-04 . + docker build -t kani-20-04 -f scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 . + docker build -t kani-18-04 -f scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 . + # this one does its tests automatically, for reasons documented in the file: + docker build -t kani-nixos -f scripts/ci/Dockerfile.bundle-test-nixos . - name: Run installed tests if: ${{ matrix.os == 'ubuntu-18.04' }} diff --git a/scripts/ci/Dockerfile.bundle-test-al2 b/scripts/ci/Dockerfile.bundle-test-al2 new file mode 100644 index 0000000000000..ffd8244355ee6 --- /dev/null +++ b/scripts/ci/Dockerfile.bundle-test-al2 @@ -0,0 +1,19 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# 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 && \ + 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 +RUN cargo install kani-verifier +RUN cargo-kani setup diff --git a/scripts/ci/Dockerfile.bundle-test-nixos b/scripts/ci/Dockerfile.bundle-test-nixos new file mode 100644 index 0000000000000..90b4ec721da73 --- /dev/null +++ b/scripts/ci/Dockerfile.bundle-test-nixos @@ -0,0 +1,44 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Note: this file is intended only for testing the kani release bundle + +FROM nixos/nix +RUN nix-channel --update +WORKDIR /tmp/kani +RUN echo $' \n\ +with import {}; \n\ +mkShell { \n\ + packages = [ \n\ + ctags \n\ + curl \n\ + gcc \n\ + patchelf \n\ + python310 \n\ + python310Packages.pip \n\ + rustup \n\ + ]; \n\ +}' >> ./default.nix +# we need to switch to nix-shell to get proper support for e.g. pip +SHELL ["nix-shell", "--command"] +ENTRYPOINT ["nix-shell"] +RUN rustup toolchain add stable +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 + +# Temporary hack: nix-shell causes problems when trying to run these with 'docker run' +# like we do for other tests, so we've imported these into the dockerfile for now +# until everything can be replaced with 'self-test': +# https://github.com/model-checking/kani/issues/1246 +RUN cargo kani --version +RUN (cd /tmp/kani/tests/cargo-kani/simple-lib && cargo kani) +RUN (cd /tmp/kani/tests/cargo-kani/simple-visualize && cargo kani) +RUN (cd /tmp/kani/tests/cargo-kani/build-rs-works && cargo kani) +RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz diff --git a/scripts/ci/Dockerfile.bundle-test-18-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 similarity index 100% rename from scripts/ci/Dockerfile.bundle-test-18-04 rename to scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 diff --git a/scripts/ci/Dockerfile.bundle-test-20-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 similarity index 100% rename from scripts/ci/Dockerfile.bundle-test-20-04 rename to scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 new file mode 100644 index 0000000000000..6f10fc394495a --- /dev/null +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-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:22.04 +ENV DEBIAN_FRONTEND=noninteractive \ + DEBCONF_NONINTERACTIVE_SEEN=true +RUN apt-get update && \ + apt-get install -y python3 python3-pip curl universal-ctags && \ + 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/src/os_hacks.rs b/src/os_hacks.rs index 6451ad67449c3..096a4d3a47793 100644 --- a/src/os_hacks.rs +++ b/src/os_hacks.rs @@ -9,7 +9,8 @@ use std::ffi::OsString; use std::path::Path; use std::process::Command; -use anyhow::Result; +use anyhow::{bail, Context, Result}; +use os_info::Info; use crate::cmd::AutoRun; @@ -45,3 +46,78 @@ pub fn setup_python_deps_on_ubuntu_18_04(pyroot: &Path, pkg_versions: &[&str]) - Ok(()) } + +/// This is the final step of setup, where we look for OSes that require additional setup steps +/// beyond the usual ones that we have done already. +pub fn setup_os_hacks(kani_dir: &Path, os: &Info) -> Result<()> { + match os.os_type() { + os_info::Type::NixOS => setup_nixos_patchelf(kani_dir), + os_info::Type::Linux => { + // NixOs containers are detected as Unknown Linux, so use a fallback hack: + if std::env::var_os("NIX_CC").is_some() && Path::new("/etc/nix").exists() { + return setup_nixos_patchelf(kani_dir); + } + Ok(()) + } + _ => Ok(()), + } +} + +/// On NixOS, the dynamic linker does not live at the standard path, and so our downloaded +/// pre-built binaries need patching. +/// In addition, the C++ standard library (needed by the CBMC binaries we ship) also does not +/// have a standard path, and so we need to inject an rpath into those binaries to get them +/// to successfully link at runtime. +fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> { + // Encode our assumption that we're working on x86 here, because when we add ARM + // support, we need to look for a different path. + assert!(env!("TARGET") == "x86_64-unknown-linux-gnu"); + if Path::new("/lib64/ld-linux-x86-64.so.2").exists() { + // if the expected path exists, I guess things are fine? + return Ok(()); + } + + println!("[NixOS detected] Applying 'patchelf' to downloaded binaries"); + + // Find the correct dynamic linker: + // `interp=$(cat $NIX_CC/nix-support/dynamic-linker)` + let nix_cc = std::env::var_os("NIX_CC") + .context("On NixOS but 'NIX_CC` environment variable not set, couldn't apply patchelf.")?; + let path = Path::new(&nix_cc).join("nix-support/dynamic-linker"); + let interp_raw = std::fs::read_to_string(path) + .context("Couldn't read $NIX_CC/nix-support/dynamic-linker")?; + let interp = interp_raw.trim(); + + // Find the correct path to link C++ stdlib: + // `rpath=$(nix-instantiate --eval -E "(import {}).stdenv.cc.cc.lib.outPath")/lib` + let rpath_output = Command::new("nix-instantiate") + .args(&["--eval", "-E", "(import {}).stdenv.cc.cc.lib.outPath"]) + .output()?; + if !rpath_output.status.success() { + bail!("Failed to find C++ standard library with `nix-instantiate`"); + } + let rpath_raw = std::str::from_utf8(&rpath_output.stdout)?; + // The output is in quotes, remove them: + let rpath_prefix = rpath_raw.trim().trim_matches('"'); + let rpath = format!("{}/lib", rpath_prefix); + + let patch_interp = |file: &Path| -> Result<()> { + Command::new("patchelf").args(&["--set-interpreter", interp]).arg(file).run() + }; + let patch_rpath = |file: &Path| -> Result<()> { + Command::new("patchelf").args(&["--set-rpath", &rpath]).arg(file).run() + }; + + let bin = kani_dir.join("bin"); + + for filename in &["kani-compiler", "kani-driver"] { + patch_interp(&bin.join(filename))?; + } + for filename in &["cbmc", "goto-analyzer", "goto-cc", "goto-instrument", "symtab2gb"] { + let file = bin.join(filename); + patch_interp(&file)?; + patch_rpath(&file)?; + } + + Ok(()) +} diff --git a/src/setup.rs b/src/setup.rs index 474f3df0a689e..8d72509f10dc2 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -11,6 +11,7 @@ use std::process::Command; use anyhow::{bail, Context, Result}; use crate::cmd::AutoRun; +use crate::os_hacks; /// Comes from our Cargo.toml manifest file. Must correspond to our release verion. const VERSION: &str = env!("CARGO_PKG_VERSION"); @@ -48,6 +49,8 @@ pub fn setup(use_local_bundle: Option) -> Result<()> { setup_build_kani_prelude(&kani_dir, toolchain_version)?; + os_hacks::setup_os_hacks(&kani_dir, &os)?; + println!("[6/6] Successfully completed Kani first-time setup."); Ok(()) @@ -114,7 +117,7 @@ fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> { if os.os_type() == os_info::Type::Ubuntu && *os.version() == os_info::Version::Semantic(18, 4, 0) { - crate::os_hacks::setup_python_deps_on_ubuntu_18_04(&pyroot, pkg_versions)?; + os_hacks::setup_python_deps_on_ubuntu_18_04(&pyroot, pkg_versions)?; return Ok(()); }