Add support for Ubuntu 18.04 to installer

.github/workflows/kani.yml

@@ -75,11 +75,11 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-10.15, ubuntu-20.04]
+        os: [macos-10.15, ubuntu-18.04]
         include:
           - os: macos-10.15
             artifact: kani-latest-x86_64-apple-darwin.tar.gz
-          - os: ubuntu-20.04
+          - os: ubuntu-18.04
             artifact: kani-latest-x86_64-unknown-linux-gnu.tar.gz
     steps:
       - name: Checkout Kani
@@ -96,26 +96,29 @@ jobs:
           cargo package -p kani-verifier
 
       - name: Build container test
-        if: ${{ matrix.os == 'ubuntu-20.04' }}
+        if: ${{ matrix.os == 'ubuntu-18.04' }}
         run: |
-          docker build -t kani-latest -f scripts/ci/Dockerfile.release-bundle-test .
+          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 .
 
       - name: Run installed tests
-        if: ${{ matrix.os == 'ubuntu-20.04' }}
+        if: ${{ matrix.os == 'ubuntu-18.04' }}
         run: |
-          docker run kani-latest  cargo kani --version
-          docker run -w /tmp/kani/tests/cargo-kani/simple-lib  kani-latest  cargo kani
-          docker run -w /tmp/kani/tests/cargo-kani/simple-visualize  kani-latest  cargo kani
-          docker run -w /tmp/kani/tests/cargo-kani/build-rs-works  kani-latest  cargo kani
-          docker run kani-latest  cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
+          for tag in kani-20-04 kani-18-04; do
+            docker run $tag  cargo kani --version
+            docker run -w /tmp/kani/tests/cargo-kani/simple-lib  $tag  cargo kani
+            docker run -w /tmp/kani/tests/cargo-kani/simple-visualize  $tag  cargo kani
+            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
 
       # We can't run macos in a container, so we can only test locally.
       # Hopefully any dependency issues won't be unique to macos.
       - name: Local install test
         if: ${{ matrix.os == 'macos-10.15' }}
         run: |
           cargo install --path ./target/package/kani-verifier-*[^e]
-          cargo-kani setup --use-local-bundle ./kani-latest-x86_64-apple-darwin.tar.gz
+          cargo-kani setup --use-local-bundle ./${{ matrix.artifact }}
           (cd tests/cargo-kani/simple-lib && cargo kani)
           (cd tests/cargo-kani/simple-visualize && cargo kani)
           (cd tests/cargo-kani/build-rs-works && cargo kani)

Cargo.lock

@@ -395,6 +395,7 @@ version = "0.2.0"
 dependencies = [
  "anyhow",
  "home",
+ "os_info",
 ]
 
 [[package]]
@@ -637,6 +638,16 @@ version = "1.10.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "87f3e037eac156d1775da914196f0f37741a274155e34a0b7e427c35d2a2ecb9"
 
+[[package]]
+name = "os_info"
+version = "3.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0eca3ecae1481e12c3d9379ec541b238a16f0b75c9a409942daa8ec20dbfdb62"
+dependencies = [
+ "log",
+ "winapi",
+]
+
 [[package]]
 name = "parking_lot"
 version = "0.12.0"

Cargo.toml

@@ -19,6 +19,7 @@ include = ["/src", "/build.rs", "/rust-toolchain.toml", "/LICENSE-*", "/README.m
 [dependencies]
 anyhow = "1"
 home = "0.5"
+os_info = { version = "3", default-features = false }
 
 [[bin]]
 name = "kani"

scripts/ci/Dockerfile.bundle-test-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:18.04
+ENV DEBIAN_FRONTEND=noninteractive \
+    DEBCONF_NONINTERACTIVE_SEEN=true
+RUN apt-get update && \
+    apt-get install -y python3 python3-pip curl 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

src/lib.rs

@@ -15,6 +15,7 @@
 #![warn(clippy::all, clippy::cargo)]
 
 mod cmd;
+mod os_hacks;
 mod setup;
 
 use std::env;

src/os_hacks.rs

@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! In order to avoid introducing a large amount of OS-specific workarounds into the main
+//! "flow" of code in setup.rs, this module contains all functions that implement os-specific
+//! workarounds.
+
+use std::ffi::OsString;
+use std::path::Path;
+use std::process::Command;
+
+use anyhow::Result;
+
+use crate::cmd::AutoRun;
+
+/// See [`crate::setup::setup_python_deps`]
+pub fn setup_python_deps_on_ubuntu_18_04(pyroot: &Path, pkg_versions: &[&str]) -> Result<()> {
+    println!("Applying a workaround for 18.04...");
+    // https://github.com/pypa/pip/issues/3826
+    // Ubuntu 18.04 has a patched-to-be-broken version of pip that just straight-up makes `--target` not work.
+    // Worse still, there is no apparent way to replicate the correct behavior cleanly.
+
+    // This is a really awful hack to simulate getting the same result. I can find no other solution.
+    // Example failed approach: `--system --target pyroot` fails to create a `pyroot/bin` with binaries.
+
+    // Step 1: use `--system --prefix pyroot`. This disables the broken behavior, and creates `bin` but...
+    Command::new("python3")
+        .args(&["-m", "pip", "install", "--system", "--prefix"])
+        .arg(&pyroot)
+        .args(pkg_versions)
+        .run()?;
+
+    // Step 2: move `pyroot/lib/python3.6/site-packages/*` up to `pyroot`
+    // This seems to successfully replicate the behavior of `--target`
+    // "mv" is not idempotent however so we need to do "cp -r"
+    let mut mv_cmd = OsString::new();
+    mv_cmd.push("cp -r ");
+    mv_cmd.push(pyroot.as_os_str());
+    mv_cmd.push("/lib/python*/site-packages/* ");
+    mv_cmd.push(pyroot.as_os_str());
+    Command::new("bash").arg("-c").arg(mv_cmd).run()?;
+
+    Ok(())
+}

src/setup.rs

@@ -33,6 +33,7 @@ pub fn appears_setup() -> bool {
 /// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION`
 pub fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
     let kani_dir = kani_dir();
+    let os = os_info::get();
 
     println!("[0/6] Running Kani first-time setup...");
 
@@ -43,7 +44,7 @@ pub fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
 
     let toolchain_version = setup_rust_toolchain(&kani_dir)?;
 
-    setup_python_deps(&kani_dir)?;
+    setup_python_deps(&kani_dir, &os)?;
 
     setup_build_kani_prelude(&kani_dir, toolchain_version)?;
 
@@ -103,15 +104,26 @@ fn setup_rust_toolchain(kani_dir: &Path) -> Result<String> {
 }
 
 /// Install into the pyroot the python dependencies we need
-fn setup_python_deps(kani_dir: &Path) -> Result<()> {
+fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> {
     println!("[4/6] Installing Kani python dependencies...");
     let pyroot = kani_dir.join("pyroot");
 
     // TODO: this is a repetition of versions from kani/scripts/setup/$OS/install_deps.sh
+    let pkg_versions = &["cbmc-viewer==3.2", "colorama==0.4.3"];
+
+    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)?;
+        return Ok(());
+    }
+
     Command::new("python3")
-        .args(&["-m", "pip", "install", "cbmc-viewer==3.2", "colorama==0.4.3", "--target"])
+        .args(&["-m", "pip", "install", "--target"])
         .arg(&pyroot)
+        .args(pkg_versions)
         .run()?;
+
     Ok(())
 }