Change default solver to CaDiCal (rust-lang#2654)

By default, Kani will now run CBMC with CaDiCaL, since this solver has outperformed Minisat in most of our benchmarks. User's should still be able to select Minisat (or a different solver) either by using `#[solver]` harness attribute or by passing `--solver=<SOLVER>` command line option.

Co-authored-by: Zyad Hassan <[email protected]>

Author: celinval

.github/workflows/kani.yml

@@ -93,6 +93,8 @@ jobs:
 
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
+        env:
+          RUST_TEST_THREADS: 1
 
   bookrunner:
     runs-on: ubuntu-20.04

CHANGELOG.md

@@ -4,6 +4,18 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.34.0]
+
+### Breaking Changes
+* Change default solver to CaDiCaL by @celinval in https://github.com/model-checking/kani/pull/2557
+By default, Kani will now run CBMC with CaDiCaL, since this solver has outperformed Minisat in most of our benchmarks.
+User's should still be able to select Minisat (or a different solver) either by using `#[solver]` harness attribute,
+or by passing `--solver=<SOLVER>` command line option.
+
+## What's Changed
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.33.0...kani-0.34.0
+
 ## [0.33.0]
 
 ## What's Changed

docs/src/reference/attributes.md

@@ -203,8 +203,8 @@ VERIFICATION:- SUCCESSFUL
 This may change the verification time required to verify a harness.
 
 At present, `<solver>` can be one of:
- - `minisat` (default): [MiniSat](http://minisat.se/).
- - `cadical`: [CaDiCaL](https://github.com/arminbiere/cadical).
+ - `minisat`: [MiniSat](http://minisat.se/).
+ - `cadical` (default): [CaDiCaL](https://github.com/arminbiere/cadical).
  - `kissat`: [kissat](https://github.com/arminbiere/kissat).
  - `bin="<SAT_SOLVER_BINARY>"`: A custom solver binary, `"<SAT_SOLVER_BINARY>"`, that must be in path.
 
@@ -226,6 +226,11 @@ fn check() {
 
 Changing the solver may result in different verification times depending on the harness.
 
+Note that the default solver may vary depending on Kani's version.
+We highly recommend users to annotate their harnesses if the choice of solver
+has a major impact on performance, even if the solver used is the current
+default one.
+
 ## `#[kani::stub(<original>, <replacement>)]`
 
 **Replaces the function/method with name <original> with the function/method with name <replacement> during compilation**

kani-driver/src/args/mod.rs

@@ -208,6 +208,7 @@ pub struct VerificationArgs {
     #[arg(long, requires("harnesses"))]
     pub unwind: Option<u32>,
     /// Specify the CBMC solver to use. Overrides the harness `solver` attribute.
+    /// If no solver is specified (with --solver or harness attribute), Kani will use CaDiCaL.
     #[arg(long, value_parser = CbmcSolverValueParser::new(CbmcSolver::VARIANTS))]
     pub solver: Option<CbmcSolver>,
     /// Pass through directly to CBMC; must be the last flag.

kani-driver/src/call_cbmc.rs

@@ -16,6 +16,10 @@ use crate::cbmc_output_parser::{
 use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
 use crate::session::KaniSession;
 
+/// We will use Cadical by default since it performed better than MiniSAT in our analysis.
+/// Note: Kissat was marginally better, but it is an external solver which could be more unstable.
+static DEFAULT_SOLVER: CbmcSolver = CbmcSolver::Cadical;
+
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub enum VerificationStatus {
     Success,
@@ -206,8 +210,7 @@ impl KaniSession {
         } else if let Some(solver) = harness_solver {
             solver
         } else {
-            // Nothing to do
-            return Ok(());
+            &DEFAULT_SOLVER
         };
 
         match solver {

tests/ui/concrete-playback/message-order/expected

@@ -6,8 +6,8 @@ Concrete playback unit test for `dummy`:
 #[test]
 fn kani_concrete_playback_dummy
     let concrete_vals: Vec<Vec<u8>> = vec![
-        // 32778
-        vec![10, 128, 0, 0],
+        // 10
+        vec![10, 0, 0, 0],
     ];
     kani::concrete_playback_run(concrete_vals, dummy);
 }

tests/ui/concrete-playback/message-order/main.rs

@@ -5,5 +5,5 @@
 
 #[kani::proof]
 fn dummy() {
-    kani::cover!(kani::any::<u32>() != 10);
+    kani::cover!(kani::any::<u32>() == 10);
 }