From 2b9838ff68fa9feca9f3937ec735a766f33f017c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 2 Aug 2023 16:37:03 -0700 Subject: [PATCH 1/5] Change default solver to CaDiCal From our analysis, this seems to be a much better option than MiniSat. --- kani-driver/src/args/mod.rs | 1 + kani-driver/src/call_cbmc.rs | 7 +++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 626f2d81be93..a30ecef77ffd 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -208,6 +208,7 @@ pub struct VerificationArgs { #[arg(long, requires("harnesses"))] pub unwind: Option, /// 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, /// Pass through directly to CBMC; must be the last flag. diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index cd87e13782e9..37f66a9f38ad 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/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 { From 5ea6dedd317da1a9338cd46afcbf184a0459f574 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 2 Aug 2023 16:49:48 -0700 Subject: [PATCH 2/5] Fix test and update doc --- docs/src/reference/attributes.md | 9 +++++++-- tests/ui/concrete-playback/message-order/expected | 4 ++-- tests/ui/concrete-playback/message-order/main.rs | 2 +- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md index bb7823eb8116..bd8b80cbbdaa 100644 --- a/docs/src/reference/attributes.md +++ b/docs/src/reference/attributes.md @@ -203,8 +203,8 @@ VERIFICATION:- SUCCESSFUL This may change the verification time required to verify a harness. At present, `` 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=""`: A custom 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(, )]` **Replaces the function/method with name with the function/method with name during compilation** diff --git a/tests/ui/concrete-playback/message-order/expected b/tests/ui/concrete-playback/message-order/expected index 415584e1f2dc..4fd787d7612b 100644 --- a/tests/ui/concrete-playback/message-order/expected +++ b/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![ - // 32778 - vec![10, 128, 0, 0], + // 10 + vec![10, 0, 0, 0], ]; kani::concrete_playback_run(concrete_vals, dummy); } diff --git a/tests/ui/concrete-playback/message-order/main.rs b/tests/ui/concrete-playback/message-order/main.rs index 81aa4c6886db..a43dc9964cfd 100644 --- a/tests/ui/concrete-playback/message-order/main.rs +++ b/tests/ui/concrete-playback/message-order/main.rs @@ -5,5 +5,5 @@ #[kani::proof] fn dummy() { - kani::cover!(kani::any::() != 10); + kani::cover!(kani::any::() == 10); } From 99e0f49af8c631e6112f48006a55c97b0abb8281 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 3 Aug 2023 10:56:40 -0700 Subject: [PATCH 3/5] Update kani-driver/src/args/mod.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-driver/src/args/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index a30ecef77ffd..867142537cae 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -208,7 +208,7 @@ pub struct VerificationArgs { #[arg(long, requires("harnesses"))] pub unwind: Option, /// 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. + /// 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, /// Pass through directly to CBMC; must be the last flag. From 2598e0de4431dfaaff89b0da375e0e4b61632967 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 4 Aug 2023 11:26:04 -0700 Subject: [PATCH 4/5] Make perf job sequential + document breaking change --- .github/workflows/kani.yml | 2 ++ CHANGELOG.md | 9 +++++++++ 2 files changed, 11 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 436890f505aa..beaebcc32842 100644 --- a/.github/workflows/kani.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index e42d6c05d1a9..6bd041094315 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,15 @@ 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 + +## 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 From f389be906963efdf9ee9b08ba216bdcf21af2ea2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 4 Aug 2023 12:20:06 -0700 Subject: [PATCH 5/5] Update CHANGELOG.md --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6bd041094315..3ccf9a150fc2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,9 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ### 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=` command line option. ## What's Changed