Requested feature: Compilation can take more time than the actual verification.
Use case: Users verifying harnesses where the potential reachable set of instructions is high despite the low harness coverage.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Test case:
Cargo.toml:
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
[package]
name = "performance"
version = "0.1.0"
edition = "2021"
[dependencies]
anyhow = "1"
src/lib.rs
celinval@truffles:/tmp/assess/proof-works$ cat src/lib.rs
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
use anyhow::*;
#[kani::proof]
fn proof_using_anyhow() {
let _ = Ok(()).context("words");
}
Running cargo kani takes about 35s to compile but around 6s to actually verify the code. Using the code from #1972
$ cargo kani --verbose 2>&1 | /bin/grep -e "Finished"
INFO kani_compiler::codegen_cprover_gotoc::compiler_interface Finished reachability analysis in 0.000000266s
INFO kani_compiler::codegen_cprover_gotoc::compiler_interface Finished reachability analysis in 0.18315084s
INFO kani_compiler::codegen_cprover_gotoc::compiler_interface Finished codegen in 6.1482673s
INFO kani_compiler::codegen_cprover_gotoc::compiler_interface Finished symtab2gb in 26.552908s
Finished dev [unoptimized + debuginfo] target(s) in 35.06s
Finished cargo in 35.10514s
Finished goto-cc in 4.792684s
Finished goto-cc in 4.5120525s
Finished goto-instrument in 5.182001s
Finished goto-instrument in 5.2142944s
Finished goto-instrument in 4.422661s
Finished run_cmbc in 6.745211s
edit: Running with release version of Kani, the compilation time drops considerably and it's dominated by the call to symtab2gb.
Requested feature: Compilation can take more time than the actual verification.
Use case: Users verifying harnesses where the potential reachable set of instructions is high despite the low harness coverage.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Test case:
Cargo.toml:
src/lib.rs
Running
cargo kanitakes about 35s to compile but around 6s to actually verify the code. Using the code from #1972edit: Running with release version of Kani, the compilation time drops considerably and it's dominated by the call to
symtab2gb.