Skip to content

Commit 035225c

Browse files
celinvalzhassan-aws
celinval
and
zhassan-aws
authored
Enable build cache in cargo kani (rust-lang#2232)
This change re-enable the build cache in Kani. For that, we also added a new dummy option that includes Kani's version, which will ensure that the cache gets refreshed when the user upgrades Kani. We also enabled an option to force rebuild: `--force-build` Co-authored-by: Zyad Hassan <[email protected]>
1 parent 9ad7eeb commit 035225c

File tree

22 files changed

+388
-10
lines changed

22 files changed

+388
-10
lines changed

‎Cargo.toml

+1
Original file line numberDiff line numberDiff line change
@@ -66,4 +66,5 @@ exclude = [
6666
"tests/cargo-ui",
6767
"tests/slow",
6868
"tests/assess-scan-test-scaffold",
69+
"tests/script-based-pre",
6970
]

‎kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

+4
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,10 @@ impl CodegenBackend for GotocCodegenBackend {
8181
provide::provide_extern(providers);
8282
}
8383

84+
fn print_version(&self) {
85+
println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION"));
86+
}
87+
8488
fn codegen_crate(
8589
&self,
8690
tcx: TyCtxt,

‎kani-compiler/src/parser.rs

+6-6
Original file line numberDiff line numberDiff line change
@@ -46,12 +46,6 @@ pub const ENABLE_STUBBING: &str = "enable-stubbing";
4646
/// Configure command options for the Kani compiler.
4747
pub fn parser() -> Command {
4848
let app = command!()
49-
.arg(
50-
Arg::new("kani-compiler-version")
51-
.short('?')
52-
.action(ArgAction::Version)
53-
.help("Gets `kani-compiler` version."),
54-
)
5549
.arg(
5650
Arg::new(KANI_LIB)
5751
.long(KANI_LIB)
@@ -137,6 +131,12 @@ pub fn parser() -> Command {
137131
.help("Instruct the compiler to perform stubbing.")
138132
.requires(HARNESS)
139133
.action(ArgAction::SetTrue),
134+
)
135+
.arg(
136+
Arg::new("check-version")
137+
.long("check-version")
138+
.action(ArgAction::Set)
139+
.help("Pass the kani version to the compiler to ensure cache coherence."),
140140
);
141141
#[cfg(feature = "unsound_experiments")]
142142
let app = crate::unsound_experiments::arg_parser::add_unsound_experiments_to_parser(app);

‎kani-driver/src/args.rs

+4
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,10 @@ pub struct KaniArgs {
113113
#[arg(long)]
114114
pub target_dir: Option<PathBuf>,
115115

116+
/// Force Kani to rebuild all packages before the verification.
117+
#[arg(long)]
118+
pub force_build: bool,
119+
116120
/// Toggle between different styles of output
117121
#[arg(long, default_value = "regular", ignore_case = true, value_enum)]
118122
pub output_format: OutputFormat,

‎kani-driver/src/call_cargo.rs

+1-3
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,7 @@ impl KaniSession {
5151
.join("kani");
5252
let outdir = target_dir.join(build_target).join("debug/deps");
5353

54-
// Clean directory before building since we are unable to handle cache today.
55-
// TODO: https://github.com/model-checking/kani/issues/1736
56-
if target_dir.exists() {
54+
if self.args.force_build && target_dir.exists() {
5755
fs::remove_dir_all(&target_dir)?;
5856
}
5957

‎kani-driver/src/call_single_file.rs

+9-1
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ impl KaniSession {
6666

6767
/// These arguments are arguments passed to kani-compiler that are `kani` compiler specific.
6868
pub fn kani_compiler_flags(&self) -> Vec<String> {
69-
let mut flags = vec![];
69+
let mut flags = vec![check_version()];
7070

7171
if self.args.debug {
7272
flags.push("--log-level=debug".into());
@@ -187,3 +187,11 @@ impl KaniSession {
187187
pub fn to_rustc_arg(kani_args: Vec<String>) -> String {
188188
format!(r#"-Cllvm-args={}"#, kani_args.join(" "))
189189
}
190+
191+
/// Function that returns a `--check-version` argument to be added to the compiler flags.
192+
/// This is really just used to force the compiler to recompile everything from scratch when a user
193+
/// upgrades Kani. Cargo currently ignores the codegen backend version.
194+
/// See <https://github.com/model-checking/kani/issues/2140> for more context.
195+
fn check_version() -> String {
196+
format!("--check-version={}", env!("CARGO_PKG_VERSION"))
197+
}

‎tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml

+13
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,16 @@ description = "Test that Kani correctly handle supported crate types"
1010
name = "lib"
1111
crate-type = ["lib", "rlib"]
1212
path = "../src/lib.rs"
13+
14+
[package.metadata.kani.flags]
15+
# This test doesn't work with the cache due to naming conflict caused by
16+
# declaring ["lib", "rlib"] which is in fact redundant.
17+
# See https://github.com/rust-lang/cargo/issues/6313 for more details.
18+
#
19+
# This still works for a fresh build and it only prints a warning. Thus, we
20+
# force rebuild for now.
21+
#
22+
# Note that support for this case is deprecated. AFAIK, there is no plan to fix
23+
# cargo build cache for cases like this. Until then, we might as well check that
24+
# our support level matches cargo's.
25+
force-build = true

‎tests/script-based-pre/build-cache-bin/bin/Cargo.toml

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
[package]
4+
name = "bin"
5+
version = "0.1.0"
6+
edition = "2021"

‎tests/script-based-pre/build-cache-bin/bin/src/lib.rs

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
#[kani::proof]
4+
fn cover_bool() {
5+
match kani::any() {
6+
true => kani::cover!(true, "true"),
7+
false => kani::cover!(true, "false"),
8+
}
9+
}
10+
11+
#[kani::proof]
12+
fn cover_option() {
13+
match kani::any() {
14+
Some(true) => kani::cover!(true, "true"),
15+
Some(false) => kani::cover!(true, "false"),
16+
None => kani::cover!(true, "none"),
17+
}
18+
}

‎tests/script-based-pre/build-cache-bin/cache_works.expected

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
Initial compilation
2+
target/initial.log:Compiled 1 crates
3+
target/initial.log:No harness verified
4+
Re-execute the same command
5+
target/same.log:Compiled 0 crates
6+
target/same.log:No harness verified
7+
Run with new arg that affects kani-driver workflow only
8+
target/driver_opt.log:Compiled 0 crates
9+
target/driver_opt.log:Checking harness cover_option...
10+
target/driver_opt.log:Checking harness cover_bool...
11+
target/driver_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
12+
Run with a new argument that affects compilation
13+
target/disable_checks.log:Compiled 1 crates
14+
target/disable_checks.log:Checking harness cover_option...
15+
target/disable_checks.log:Checking harness cover_bool...
16+
target/disable_checks.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
17+
Run with new dependency
18+
target/new_dep.log:Compiled 2 crates
19+
target/new_dep.log:Checking harness cover_option...
20+
target/new_dep.log:Checking harness cover_bool...
21+
target/new_dep.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.

‎tests/script-based-pre/build-cache-bin/cache_works.sh

+71
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
#!/usr/bin/env bash
2+
# Copyright Kani Contributors
3+
# SPDX-License-Identifier: Apache-2.0 OR MIT
4+
5+
# Checks situations where running kani multiple times will work as expected when
6+
# the target crate is binary.
7+
#
8+
# The following checks should not trigger recompilation.
9+
# - Exact same input being invoked a second time.
10+
# - Different options that do not affect the compilation, only the Kani workt flow.
11+
# While the following should recompile the target.
12+
# - Pass a new argument that affects compilation
13+
# - Add a dependency
14+
set -e
15+
set -u
16+
17+
ORIG=bin
18+
OUT_DIR=target
19+
MANIFEST=${OUT_DIR}/${ORIG}/Cargo.toml
20+
21+
# Expects two arguments: "kani arguments" "output_file"
22+
function check_kani {
23+
local args=$1
24+
local log_file="${OUT_DIR}/$2"
25+
# Run kani with the given arguments
26+
if [ -z "${args}" ]
27+
then
28+
cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
29+
2>&1 | tee "${log_file}"
30+
else
31+
cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
32+
"${args}" 2>&1 | tee "${log_file}"
33+
fi
34+
35+
# Print information about the generated log file.
36+
# Check for occurrences of "Compiling" messages in the log files
37+
local compiled=$(grep -c "Compiling" ${log_file})
38+
echo "${log_file}:Compiled ${compiled} crates"
39+
40+
# Check which harnesses were verified
41+
grep "Checking harness" -H ${log_file} || echo "${log_file}:No harness verified"
42+
43+
# Check the verification summary
44+
grep "successfully verified harnesses" -H ${log_file} || true
45+
}
46+
47+
# Ensure output folder is clean
48+
rm -rf ${OUT_DIR}
49+
mkdir -p ${OUT_DIR}
50+
# Move the original source to the output folder since it will be modified
51+
cp -r ${ORIG} ${OUT_DIR}
52+
53+
echo "Initial compilation"
54+
check_kani --only-codegen initial.log
55+
56+
echo "Re-execute the same command"
57+
check_kani --only-codegen same.log
58+
59+
echo "Run with new arg that affects kani-driver workflow only"
60+
check_kani "" driver_opt.log
61+
62+
echo "Run with a new argument that affects compilation"
63+
check_kani --no-assertion-reach-checks disable_checks.log
64+
65+
echo "Run with new dependency"
66+
cargo new --lib ${OUT_DIR}/new_dep
67+
cargo add new_dep --manifest-path ${MANIFEST} --path ${OUT_DIR}/new_dep
68+
check_kani --no-assertion-reach-checks new_dep.log
69+
70+
# Try to leave a clean output folder at the end
71+
rm -rf ${OUT_DIR}

‎tests/script-based-pre/build-cache-bin/config.yml

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
script: cache_works.sh
4+
expected: cache_works.expected

‎tests/script-based-pre/build-cache-dirty/config.yml

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
script: rebuild.sh
4+
expected: rebuild.expected

‎tests/script-based-pre/build-cache-dirty/rebuild.expected

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
Initial compilation
2+
omplete - 2 successfully verified harnesses, 0 failures, 2 total.
3+
target/initial.log:Compiled 2 crates
4+
target/initial.log:Checking harness check_u8_i16...
5+
target/initial.log:Checking harness check_u8_u32...
6+
target/initial.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
7+
Run with a new argument that affects compilation
8+
target/enable_checks.log:Compiled 2 crates
9+
target/enable_checks.log:Checking harness check_u8_i16...
10+
target/enable_checks.log:Checking harness check_u8_u32...
11+
target/enable_checks.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
12+
Run after change to the source code
13+
target/changed_src.log:Compiled 1 crates
14+
target/changed_src.log:Checking harness noop_check...
15+
target/changed_src.log:Checking harness check_u8_i16...
16+
target/changed_src.log:Checking harness check_u8_u32...
17+
target/changed_src.log:Complete - 3 successfully verified harnesses, 0 failures, 3 total.
18+
Run with new dependency
19+
target/new_dep.log:Compiled 2 crates
20+
target/new_dep.log:Checking harness noop_check...
21+
target/new_dep.log:Checking harness check_u8_i16...
22+
target/new_dep.log:Checking harness check_u8_u32...
23+
target/new_dep.log:Complete - 3 successfully verified harnesses, 0 failures, 3 total.

‎tests/script-based-pre/build-cache-dirty/rebuild.sh

+68
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
#!/usr/bin/env bash
2+
# Copyright Kani Contributors
3+
# SPDX-License-Identifier: Apache-2.0 OR MIT
4+
5+
# Checks situations where running kani multiple times should trigger a new build
6+
# The cases we cover here are:
7+
# - Pass a new argument that affects compilation
8+
# - Change the source code
9+
# - Add a dependency
10+
# Note: This should run in the folder where the script is.
11+
12+
OUT_DIR=target
13+
MANIFEST=${OUT_DIR}/target_lib/Cargo.toml
14+
LIB_SRC=${OUT_DIR}/target_lib/src/lib.rs
15+
16+
# Expects two arguments: "kani arguments" "output_file"
17+
function check_kani {
18+
local args=$1
19+
local log_file="${OUT_DIR}/$2"
20+
# Run kani with the given arguments
21+
if [ -z "${args}" ]
22+
then
23+
cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
24+
2>&1 | tee "${log_file}"
25+
else
26+
cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
27+
"${args}" 2>&1 | tee "${log_file}"
28+
fi
29+
30+
# Print information about the generated log file.
31+
# Check for occurrences of "Compiling" messages in the log files
32+
local compiled=$(grep -c "Compiling" ${log_file})
33+
echo "${log_file}:Compiled ${compiled} crates"
34+
35+
# Check which harnesses were verified
36+
grep "Checking harness" -H ${log_file} || echo "${log_file}:No harness verified"
37+
38+
# Check the verification summary
39+
grep "successfully verified harnesses" -H ${log_file} || true
40+
}
41+
42+
# Ensure output folder is clean
43+
rm -rf ${OUT_DIR}
44+
mkdir -p ${OUT_DIR}
45+
46+
# Copy the project so we don't make changes to the source code
47+
cp -r target_lib ${OUT_DIR}
48+
49+
echo "Initial compilation"
50+
check_kani --no-assertion-reach-checks initial.log
51+
52+
echo "Run with a new argument that affects compilation"
53+
check_kani "" enable_checks.log
54+
55+
echo "Run after change to the source code"
56+
echo '
57+
#[kani::proof]
58+
fn noop_check() {}
59+
' >> ${LIB_SRC}
60+
check_kani "" changed_src.log
61+
62+
echo "Run with new dependency"
63+
cargo new --lib ${OUT_DIR}/new_dep
64+
cargo add new_dep --manifest-path ${MANIFEST} --path ${OUT_DIR}/new_dep
65+
check_kani "" new_dep.log
66+
67+
# Try to leave a clean output folder at the end
68+
rm -rf ${OUT_DIR}

‎tests/script-based-pre/build-cache-dirty/target_lib/Cargo.toml

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
[package]
4+
name = "target_lib"
5+
version = "0.1.0"
6+
edition = "2021"
7+
8+
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
9+
10+
[dependencies]
11+
either = "1.8"

‎tests/script-based-pre/build-cache-dirty/target_lib/src/lib.rs

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//! We don't use any of our dependencies to keep the test fast
4+
5+
#[kani::proof]
6+
fn check_u8_u32() {
7+
let before: u8 = kani::any();
8+
let temp = before as u32;
9+
let after: u8 = temp.try_into().unwrap();
10+
assert_eq!(after, before);
11+
}
12+
13+
#[kani::proof]
14+
fn check_u8_i16() {
15+
let before: u8 = kani::any();
16+
let temp = before as i16;
17+
let after: u8 = temp.try_into().unwrap();
18+
assert_eq!(after, before);
19+
}

‎tests/script-based-pre/build-cache-fresh/cache_works.expected

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
Initial compilation
2+
target/initial.log:Compiled 1 crates
3+
target/initial.log:No harness verified
4+
Re-execute the same command
5+
target/same.log:Compiled 0 crates
6+
target/same.log:No harness verified
7+
Run with new arg that affects kani-driver workflow only
8+
target/driver_opt.log:Compiled 0 crates
9+
target/driver_opt.log:Checking harness cover_option...
10+
target/driver_opt.log:Checking harness cover_bool...
11+
target/driver_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
12+
Run with a new cbmc option
13+
target/cbmc_opt.log:Compiled 0 crates
14+
target/cbmc_opt.log:Checking harness cover_option...
15+
target/cbmc_opt.log:Checking harness cover_bool...
16+
target/cbmc_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.

0 commit comments

Comments
 (0)