Support bitwuzla, cvc5, z3 as solver attribute values (#4218)

Adds support for solver attribute values `bitwuzla`, `cvc5`, and `z3` to
make CBMC use the corresponding SMT solver.

Use Z3 for selected tests when running regression tests with the
following rationale: The tests loop_assigns_for_vec.rs and
assert-postconditions.rs previously required more than 8 GB of memory on
Ubuntu/x86 and solved in 1:15 minutes and 25 seconds, respectively. When
using Z3 as back-end solver, they complete in 35 and 2 seconds (2.5 GB
and 150 MB), respectively.

Use CVC5 for the test from issue #4226.

We are not testing Bitwuzla support in CI at this point (though it has
been confirmed to work locally), because Bitwuzla only releases binaries
for some of our CI platforms, and we cannot even build Bitwuzla from
source on Ubuntu 22.04 (meson is too old).

Resolves: #3277
Resolves: #4226

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

docs/src/build-from-source.md

@@ -13,6 +13,8 @@ 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. [Kissat](https://github.com/arminbiere/kissat) (Release 4.0.1)
+3. [Z3](https://github.com/Z3Prover/z3)
+4. [cvc5](https://github.com/cvc5/cvc5)
 
 Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.
 

docs/src/reference/attributes.md

@@ -206,6 +206,9 @@ At present, `<solver>` can be one of:
  - `minisat`: [MiniSat](http://minisat.se/).
  - `cadical` (default): [CaDiCaL](https://github.com/arminbiere/cadical).
  - `kissat`: [kissat](https://github.com/arminbiere/kissat).
+ - `z3`: [Z3](https://github.com/Z3Prover/z3/).
+ - `bitwuzla`: [Bitwuzla](https://github.com/bitwuzla/bitwuzla).
+ - `cvc5`: [cvc5](https://github.com/cvc5/cvc5).
  - `bin="<SAT_SOLVER_BINARY>"`: A custom solver binary, `"<SAT_SOLVER_BINARY>"`, that must be in path.
 
 ### Example

kani-driver/src/call_cbmc.rs

@@ -279,10 +279,16 @@ impl KaniSession {
         };
 
         match solver {
+            CbmcSolver::Bitwuzla => {
+                args.push("--bitwuzla".into());
+            }
             CbmcSolver::Cadical => {
                 args.push("--sat-solver".into());
                 args.push("cadical".into());
             }
+            CbmcSolver::Cvc5 => {
+                args.push("--cvc5".into());
+            }
             CbmcSolver::Kissat => {
                 args.push("--external-sat-solver".into());
                 args.push("kissat".into());
@@ -291,6 +297,9 @@ impl KaniSession {
                 // Minisat is currently CBMC's default solver, so no need to
                 // pass any arguments
             }
+            CbmcSolver::Z3 => {
+                args.push("--z3".into());
+            }
             CbmcSolver::Binary(solver_binary) => {
                 // Check if the specified binary exists in path
                 if which::which(solver_binary).is_err() {

kani_metadata/src/cbmc_solver.rs

@@ -10,15 +10,24 @@ use strum_macros::{AsRefStr, EnumString, VariantNames};
 #[derive(Debug, Clone, AsRefStr, EnumString, VariantNames, PartialEq, Eq, Serialize, Deserialize)]
 #[strum(serialize_all = "snake_case")]
 pub enum CbmcSolver {
+    /// Bitwuzla SMT solver
+    Bitwuzla,
+
     /// CaDiCaL which is available in CBMC as of version 5.77.0
     Cadical,
 
+    /// cvc5 SMT solver
+    Cvc5,
+
     /// The kissat solver that is included in the Kani bundle
     Kissat,
 
     /// MiniSAT (CBMC's default solver)
     Minisat,
 
+    /// Z3 SMT solver
+    Z3,
+
     /// A solver binary variant whose argument gets passed to
     /// `--external-sat-solver`. The specified binary must exist in path.
     #[strum(disabled, serialize = "bin=<SAT_SOLVER_BINARY>")]

scripts/setup/macos/install_deps.sh

@@ -14,6 +14,14 @@ brew update
 brew install python@3 || true
 brew link --overwrite python@3
 
+# Install SMT solvers being used in regression tests
+brew install z3
+ARCH=$(uname -m)
+curl -L --remote-name https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.0/cvc5-macOS-${ARCH}-static.zip
+sudo unzip -o -j -d /usr/local/bin cvc5-macOS-${ARCH}-static.zip cvc5-macOS-${ARCH}-static/bin/cvc5
+rm cvc5-macOS-${ARCH}-static.zip
+cvc5 --version
+
 # Get the directory containing this script
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 

scripts/setup/ubuntu/install_deps.sh

@@ -16,6 +16,7 @@ DEPS=(
   gpg-agent
   make
   patch
+  z3
   zlib1g
   zlib1g-dev
 )
@@ -30,6 +31,12 @@ sudo apt-get --yes update
 
 sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}"
 
+ARCH=$(uname -m)
+curl -L --remote-name https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.0/cvc5-Linux-${ARCH}-static.zip
+sudo unzip -o -j -d /usr/local/bin cvc5-Linux-${ARCH}-static.zip cvc5-Linux-${ARCH}-static/bin/cvc5
+rm cvc5-Linux-${ARCH}-static.zip
+cvc5 --version
+
 # Get the directory containing this script
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 

tests/expected/function-contract/as-assertions/assert-postconditions.rs

@@ -23,6 +23,7 @@ fn add_one(add_one_ptr: &mut u32) {
 }
 
 #[kani::proof_for_contract(add_three)]
+#[kani::solver(z3)]
 fn prove_add_three() {
     let mut i = kani::any();
     add_three(&mut i);

tests/expected/loop-contract/loop_assigns_for_vec.rs

@@ -12,6 +12,7 @@ use std::ptr;
 use std::ptr::slice_from_raw_parts;
 
 #[kani::proof]
+#[kani::solver(z3)]
 fn main() {
     let mut i = 0;
     let a: [u8; 3] = kani::any();

tests/kani/Quantifiers/arbitrary_range.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
+
+// See https://github.com/model-checking/kani/issues/4226
+
+#[kani::proof]
+#[kani::solver(cvc5)]
+fn main() {
+    const N: usize = 100;
+    let a: [i32; N] = kani::any();
+    let i = kani::any();
+    kani::assume(i < N - 1);
+    kani::assume(kani::forall!(|j in (1, i)| a[j] < 10));
+    kani::assume(a[i] < 10);
+    assert!(kani::forall!(|j in (1, i+1)| a[j] < 10));
+}
+
+#[kani::proof]
+fn bounded() {
+    const N: usize = 100;
+    let a: [i32; N] = kani::any();
+    let i = 20;
+    kani::assume(i < N - 1);
+    kani::assume(kani::forall!(|j in (1, i)| a[j] < 10));
+    kani::assume(a[i] < 10);
+    assert!(kani::forall!(|j in (1, i+1)| a[j] < 10));
+}