Include Kissat in the Kani bundle (rust-lang#2087)

Author: zhassan-aws

.github/actions/setup/action.yml

@@ -25,6 +25,10 @@ runs:
         run: ./scripts/setup/${{ inputs.os }}/install_viewer.sh
         shell: bash
 
+      - name: Install Kissat
+        run: ./scripts/setup/install_kissat.sh
+        shell: bash
+
       - name: Install Rust toolchain
         run: ./scripts/setup/install_rustup.sh
         shell: bash

.github/workflows/kani.yml

@@ -156,6 +156,7 @@ jobs:
             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 -w /tmp/kani/tests/cargo-kani/simple-kissat  $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:

docs/src/build-from-source.md

@@ -13,6 +13,7 @@ In general, the following dependencies are required to build Kani from source.
 1. Cargo installed via [rustup](https://rustup.rs/)
 2. [CBMC](https://github.com/diffblue/cbmc) (latest release)
 3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (latest release)
+4. [Kissat](https://github.com/arminbiere/kissat) (Release 3.0.0)
 
 Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.
 
@@ -30,6 +31,7 @@ git submodule update --init
 ./scripts/setup/ubuntu/install_deps.sh
 ./scripts/setup/ubuntu/install_cbmc.sh
 ./scripts/setup/ubuntu/install_viewer.sh
+./scripts/setup/install_kissat.sh
 # If you haven't already (or from https://rustup.rs/):
 ./scripts/setup/install_rustup.sh
 source $HOME/.cargo/env
@@ -47,6 +49,7 @@ git submodule update --init
 ./scripts/setup/macos/install_deps.sh
 ./scripts/setup/macos/install_cbmc.sh
 ./scripts/setup/macos/install_viewer.sh
+./scripts/setup/install_kissat.sh
 # If you haven't already (or from https://rustup.rs/):
 ./scripts/setup/install_rustup.sh
 source $HOME/.cargo/env

kani-dependencies

@@ -1,3 +1,4 @@
 CBMC_VERSION="5.75.0"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.8"
+KISSAT_VERSION="3.0.0"

scripts/check_kissat_version.sh

@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Check if kissat has the minimum required version specified in the
+# `kani_dependencies` file under kani's root folder
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+KANI_DIR=$SCRIPT_DIR/..
+source "${KANI_DIR}/kani-dependencies"
+
+if [ -z "${KISSAT_VERSION:-}" ]; then
+  echo "$0: ERROR: KISSAT_VERSION is not set"
+  return 1
+fi
+cmd="kissat --version"
+if kissat_version=$($cmd); then
+  # Perform a lexicographic comparison of the version
+  if [[ $kissat_version < $KISSAT_VERSION ]]; then
+    echo "ERROR: Kissat version is $kissat_version. Expected at least $KISSAT_VERSION."
+    return 1
+  fi
+else
+  echo "ERROR: Couldn't run command '$cmd'"
+  return 1
+fi

scripts/kani-regression.sh

@@ -24,6 +24,7 @@ export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
 # Required dependencies
 check-cbmc-version.py --major 5 --minor 75
 check-cbmc-viewer-version.py --major 3 --minor 5
+check_kissat_version.sh
 
 # Formatting check
 ${SCRIPT_DIR}/kani-fmt.sh --check

scripts/setup/install_kissat.sh

@@ -0,0 +1,42 @@
+#!/bin/bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+# Source kani-dependencies to get KISSAT_VERSION
+source kani-dependencies
+
+if [ -z "${KISSAT_VERSION:-}" ]; then
+  echo "$0: Error: KISSAT_VERSION is not specified"
+  exit 1
+fi
+
+# Check if the correct Kissat version is already installed
+if command -v kissat > /dev/null; then
+  if kissat_version=$(kissat --version); then
+    if [[ $kissat_version == $KISSAT_VERSION ]]; then
+      # Already installed
+      exit 0
+    else
+      echo "Warning: Overriding Kissat version ${kissat_version} with ${KISSAT_VERSION}"
+    fi
+  fi
+fi
+
+# Kissat release
+FILE="rel-${KISSAT_VERSION}.tar.gz"
+URL="https://github.com/arminbiere/kissat/archive/refs/tags/$FILE"
+
+set -x
+
+wget -O "$FILE" "$URL"
+tar -xvzf $FILE
+DIR_NAME="kissat-rel-${KISSAT_VERSION}"
+cd $DIR_NAME
+./configure && make kissat && sudo install build/kissat /usr/local/bin
+cd -
+
+# Clean up on success
+rm $FILE
+rm -rf $DIR_NAME

tests/cargo-kani/simple-kissat/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "simple-kissat"
+version = "0.1.0"
+edition = "2021"
+description = "Tests that Kani can be invoked with Kissat"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+
+[kani.flags]
+enable-unstable = true
+cbmc-args = ["--external-sat-solver", "kissat" ]

tests/cargo-kani/simple-kissat/expected

@@ -0,0 +1,2 @@
+Solving with External SAT solver
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/simple-kissat/src/main.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that concatenating two nondet arrays into a vector
+//! preserves the values
+
+#[kani::proof]
+fn check_concat() {
+    let arr1: [i32; 2] = kani::any();
+    let arr2: [i32; 3] = kani::any();
+    let mut v = Vec::new();
+    v.extend_from_slice(&arr1);
+    v.extend_from_slice(&arr2);
+    assert_eq!(v[0], arr1[0]);
+    assert_eq!(v[1], arr1[1]);
+    assert_eq!(v[2], arr2[0]);
+    assert_eq!(v[3], arr2[1]);
+    assert_eq!(v[4], arr2[2]);
+}
+
+fn main() {}

tools/build-kani/src/main.rs

@@ -40,6 +40,7 @@ fn main() -> Result<()> {
 
             bundle_kani(dir)?;
             bundle_cbmc(dir)?;
+            bundle_kissat(dir)?;
             // cbmc-viewer isn't bundled, it's pip install'd on first-time setup
 
             create_release_bundle(dir, &bundle_name)?;
@@ -140,6 +141,17 @@ fn bundle_cbmc(dir: &Path) -> Result<()> {
     Ok(())
 }
 
+/// Copy Kissat binary into `dir`
+fn bundle_kissat(dir: &Path) -> Result<()> {
+    // Assumes `kissat` exists in PATH (similar to `bundle_cbmc`)
+    let bin = dir.join("bin");
+
+    // We use these directly
+    cp(&which::which("kissat")?, &bin)?;
+
+    Ok(())
+}
+
 /// Create the release tarball from `./dir` named `bundle`.
 /// This should include all files as `dir/<path>` in the tarball.
 /// e.g. `kani-1.0/bin/kani-compiler` not just `bin/kani-compiler`.