From 326b35ebac9f630239bfb45b8e96eb0aec613eb7 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Fri, 20 Jan 2023 16:24:42 -0800 Subject: [PATCH] Include Kissat in the Kani bundle (#2087) --- .github/actions/setup/action.yml | 4 +++ .github/workflows/kani.yml | 1 + docs/src/build-from-source.md | 3 ++ kani-dependencies | 1 + scripts/check_kissat_version.sh | 26 ++++++++++++++ scripts/kani-regression.sh | 1 + scripts/setup/install_kissat.sh | 42 ++++++++++++++++++++++ tests/cargo-kani/simple-kissat/Cargo.toml | 15 ++++++++ tests/cargo-kani/simple-kissat/expected | 2 ++ tests/cargo-kani/simple-kissat/src/main.rs | 21 +++++++++++ tools/build-kani/src/main.rs | 12 +++++++ 11 files changed, 128 insertions(+) create mode 100755 scripts/check_kissat_version.sh create mode 100755 scripts/setup/install_kissat.sh create mode 100644 tests/cargo-kani/simple-kissat/Cargo.toml create mode 100644 tests/cargo-kani/simple-kissat/expected create mode 100644 tests/cargo-kani/simple-kissat/src/main.rs diff --git a/.github/actions/setup/action.yml b/.github/actions/setup/action.yml index 1786be7c8e71..b2e54b400dad 100644 --- a/.github/actions/setup/action.yml +++ b/.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 diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 1433991a4227..6e145939b74b 100644 --- a/.github/workflows/kani.yml +++ b/.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: diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md index 0b3c2c9c4b6c..7a5ed3a59bd1 100644 --- a/docs/src/build-from-source.md +++ b/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 diff --git a/kani-dependencies b/kani-dependencies index 2df176680c52..44cd15ce74f5 100644 --- a/kani-dependencies +++ b/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" diff --git a/scripts/check_kissat_version.sh b/scripts/check_kissat_version.sh new file mode 100755 index 000000000000..6cd07b940660 --- /dev/null +++ b/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 diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index e7c69505ab3c..a57d651ff3be 100755 --- a/scripts/kani-regression.sh +++ b/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 diff --git a/scripts/setup/install_kissat.sh b/scripts/setup/install_kissat.sh new file mode 100755 index 000000000000..2d28ef4e157c --- /dev/null +++ b/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 diff --git a/tests/cargo-kani/simple-kissat/Cargo.toml b/tests/cargo-kani/simple-kissat/Cargo.toml new file mode 100644 index 000000000000..3bde94c619fb --- /dev/null +++ b/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" ] diff --git a/tests/cargo-kani/simple-kissat/expected b/tests/cargo-kani/simple-kissat/expected new file mode 100644 index 000000000000..9f3b67b8a52a --- /dev/null +++ b/tests/cargo-kani/simple-kissat/expected @@ -0,0 +1,2 @@ +Solving with External SAT solver +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/simple-kissat/src/main.rs b/tests/cargo-kani/simple-kissat/src/main.rs new file mode 100644 index 000000000000..9bb10f867b9f --- /dev/null +++ b/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() {} diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index d2e33893abc5..756aae2a4c43 100644 --- a/tools/build-kani/src/main.rs +++ b/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/` in the tarball. /// e.g. `kani-1.0/bin/kani-compiler` not just `bin/kani-compiler`.