Add support for installing on NixOS (rust-lang#1298)

* Also added dockerfiles for AL2, Ubuntu 22.04. Not in CI yet.

Author: tedinski

Diff for: .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 for: 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 for: 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 <nixpkgs> {}; \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 for: scripts/ci/Dockerfile.bundle-test-18-04 renamed to scripts/ci/Dockerfile.bundle-test-ubuntu-18-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 for: scripts/ci/Dockerfile.bundle-test-20-04 renamed to scripts/ci/Dockerfile.bundle-test-ubuntu-20-04

@@ -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 <nixpkgs> {}).stdenv.cc.cc.lib.outPath")/lib`
+    let rpath_output = Command::new("nix-instantiate")
+        .args(&["--eval", "-E", "(import <nixpkgs> {}).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 for: scripts/ci/Dockerfile.bundle-test-ubuntu-22-04

@@ -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<OsString>) -> 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(());
     }