Skip to content

Commit fc43543

Browse files
celinvalcelinval
authored
Enable MIR Linker by default and adjust tests (rust-lang#1785)
 - intrinsics: Use legacy linker for some of them because of not so friendly messages. - performance: A few test are taking too long because of the new symbols being included in the analysis. Keep legacy linker for now. - fixme: Enable a few fixme tests and tests that were marked as verify-fail due to missing symbols. These run fine now with the linker.
1 parent 91e2596 commit fc43543

File tree

22 files changed

+88
-158
lines changed

22 files changed

+88
-158
lines changed

‎docs/src/tutorial/loops-unwinding/check_initialize_prefix.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
FAILURE\
2-
unwinding assertion loop 2
2+
unwinding assertion loop
33
VERIFICATION:- FAILED

‎kani-driver/src/args.rs

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -136,11 +136,20 @@ pub struct KaniArgs {
136136
/// Kani will only compile the crate. No verification will be performed
137137
#[structopt(long, hidden_short_help(true))]
138138
pub only_codegen: bool,
139-
/// Enables experimental MIR Linker. This option will affect how Kani prunes the code to be
140-
/// analyzed. Please report any missing function issue found here:
141-
/// <https://github.com/model-checking/kani/issues/new/choose>
142-
#[structopt(long, hidden = true, requires("enable-unstable"))]
139+
140+
/// Disable the new MIR Linker. Using this option may result in missing symbols from the
141+
/// `std` library. See <https://github.com/model-checking/kani/issues/1213> for more details.
142+
#[structopt(long, hidden = true)]
143+
pub legacy_linker: bool,
144+
145+
/// Enable the new MIR Linker. This is already the default option and it will be removed once
146+
/// the linker is stable.
147+
/// The MIR Linker affects how Kani prunes the code to be analyzed. It also fixes previous
148+
/// issues with missing `std` function definitions.
149+
/// See <https://model-checking.github.io/kani/rfc/rfcs/0001-mir-linker.html> for more details.
150+
#[structopt(long, conflicts_with("legacy_linker"), hidden = true)]
143151
pub mir_linker: bool,
152+
144153
/// Compiles Kani harnesses in all features of all packages selected on the command-line.
145154
#[structopt(long)]
146155
pub all_features: bool,

‎kani-driver/src/call_cargo.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ impl KaniSession {
6262

6363
// Arguments that will only be passed to the target package.
6464
let mut pkg_args: Vec<OsString> = vec![];
65-
if self.args.mir_linker {
65+
if !self.args.legacy_linker {
6666
// Only provide reachability flag to the target package.
6767
pkg_args.push("--".into());
6868
if self.args.function.is_some() {

‎kani-driver/src/call_single_file.rs

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -48,14 +48,12 @@ impl KaniSession {
4848
}
4949

5050
let mut kani_args = self.kani_specific_flags();
51-
if self.args.mir_linker {
52-
if self.args.function.is_some() {
53-
kani_args.push("--reachability=pub_fns".into());
54-
} else {
55-
kani_args.push("--reachability=harnesses".into());
56-
}
57-
} else {
51+
if self.args.legacy_linker {
5852
kani_args.push("--reachability=legacy".into());
53+
} else if self.args.function.is_some() {
54+
kani_args.push("--reachability=pub_fns".into());
55+
} else {
56+
kani_args.push("--reachability=harnesses".into());
5957
}
6058

6159
let mut rustc_args = self.kani_rustc_flags();

‎scripts/codegen-firecracker.sh

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,9 @@ cd $KANI_DIR/firecracker/src/devices/src/virtio/
2626
# Disable warnings until https://github.com/model-checking/kani/issues/573 is fixed
2727
export RUSTC_LOG=error
2828
export RUST_BACKTRACE=1
29-
# Kani cannot locate Cargo.toml correctly: https://github.com/model-checking/kani/issues/717
30-
cargo kani --only-codegen
29+
# Use the legacy linker for now since we want to maximize the code that we are compiling from firecracker.
30+
# The MIR Linker will by default only collect code relevant to proof harnesses, however, firecracker has none.
31+
cargo kani --only-codegen --legacy-linker
3132

3233
echo
3334
echo "Finished Firecracker codegen regression successfully..."

‎tests/cargo-ui/dry-run/expected

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
KANIFLAGS="--goto-c --log-level=warn --assertion-reach-checks --reachability=legacy -C symbol-mangling-version=v0" RUSTC=
1+
KANIFLAGS="--goto-c
2+
RUSTC=
23
RUSTFLAGS="--kani-flags" cargo rustc
34
goto-cc
45
goto-cc

‎tests/expected/drop/expected

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,6 @@
11
Status: UNDETERMINED\
22
Description: "assertion failed: self.w_id == 0"\
3-
in function <Wrapper<DummyImpl> as std::ops::Drop>::drop
4-
5-
Status: UNDETERMINED\
6-
Description: "assertion failed: self.id == 1"\
7-
in function <DummyImpl as std::ops::Drop>::drop
3+
in function <Wrapper<dyn DummyTrait> as std::ops::Drop>::drop
84

95
Status: FAILURE\
106
Description: "drop unsized struct for Wrapper<dyn DummyTrait> is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/1072"

‎tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,14 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
4-
// Checks that `copy_nonoverlapping` triggers an overflow failure if the `count`
5-
// argument can overflow a `usize`
3+
// kani-flags: --legacy-linker
4+
//! Checks that `copy_nonoverlapping` triggers an overflow failure if the `count`
5+
//! argument can overflow a `usize`
6+
//!
7+
//! When enabling "--mir-linker", the error we currently get is:
8+
//! > Failed checks: Called `Option::unwrap()` on a `None` value
9+
//! This happens because of std debug checks. The `is_nonoverlapping` check has a
10+
//! `checked_mul().unwrap()` that fails in the overflow scenario.
11+
//! See <https://github.com/model-checking/kani/issues/1740> for more details.
612
#[kani::proof]
713
fn test_copy_nonoverlapping_unaligned() {
814
let arr: [i32; 3] = [0, 1, 0];

‎tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,11 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
4+
// kani-flags: --legacy-linker
5+
//! The MIR linker errors are not quite user friendly. For more details, see
6+
//! <https://github.com/model-checking/kani/issues/1740>
7+
//! Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
8+
59
#[kani::proof]
610
fn test_copy_nonoverlapping_unaligned() {
711
let arr: [i32; 3] = [0, 1, 0];

‎tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// Checks that `copy_nonoverlapping` fails when `src` is not aligned.
4+
// kani-flags: --legacy-linker
5+
//! The MIR linker errors are not quite user friendly. For more details, see
6+
//! <https://github.com/model-checking/kani/issues/1740>
7+
//! Checks that `copy_nonoverlapping` fails when `src` is not aligned.
58
#[kani::proof]
69
fn test_copy_nonoverlapping_unaligned() {
710
let arr: [i32; 3] = [0, 1, 0];

‎tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// Checks that `copy` fails when `dst` is not aligned.
4+
// kani-flags: --legacy-linker
5+
//! The MIR linker errors are not quite user friendly. For more details, see
6+
//! <https://github.com/model-checking/kani/issues/1740>
7+
//! Checks that `copy` fails when `dst` is not aligned.
58
#[kani::proof]
69
fn test_copy_unaligned() {
710
let arr: [i32; 3] = [0, 1, 0];

‎tests/expected/intrinsics/copy/copy-unaligned-src/main.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// Checks that `copy` fails when `src` is not aligned.
4+
// kani-flags: --legacy-linker
5+
//! The MIR linker errors are not quite user friendly. For more details, see
6+
//! <https://github.com/model-checking/kani/issues/1740>
7+
//! Checks that `copy` fails when `src` is not aligned.
58
#[kani::proof]
69
fn test_copy_unaligned() {
710
let arr: [i32; 3] = [0, 1, 0];

‎tests/expected/intrinsics/write_bytes/unaligned/main.rs

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// Checks that `write_bytes` fails when `dst` is not aligned.
5-
6-
// This test is a modified version of the example in
7-
// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
4+
// kani-flags: --legacy-linker
5+
//! The MIR linker errors are not quite user friendly. For more details, see
6+
//! <https://github.com/model-checking/kani/issues/1740>
7+
//! Checks that `write_bytes` fails when `dst` is not aligned.
8+
//! This test is a modified version of the example in
9+
//! https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
810
use std::intrinsics::write_bytes;
911

1012
#[kani::proof]

‎tests/kani/FatPointers/boxslice2.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
// kani-verify-fail
43

54
// Casts boxed array to boxed slice (example taken from rust documentation)
65
use std::str;

‎tests/kani/Iterator/flat_map_count_fixme.rs

Lines changed: 0 additions & 16 deletions
This file was deleted.

‎tests/kani/Refs/main.rs

Lines changed: 4 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -1,66 +1,10 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
// running with a unwind of 1 passes; running with unwind of two gets stuck in post-processing
4-
// from arg_parser.rs in firecracker/src/utils/src
5-
6-
// warning: ignoring typecast
7-
// * type: struct_tag
8-
// * identifier: tag-std::alloc::Global
9-
// 0: struct
10-
// * type: struct_tag
11-
// * identifier: tag-std::mem::ManuallyDrop<std::vec::Vec<&()>>
12-
// 0: struct
13-
// * type: struct_tag
14-
// * identifier: tag-std::vec::Vec<&()>
15-
// 0: struct
16-
// * type: struct_tag
17-
// * identifier: tag-alloc::raw_vec::RawVec<&()>
18-
// 0: struct
19-
// * type: struct_tag
20-
// * identifier: tag-std::alloc::Global
21-
// 1: struct
22-
// * type: struct_tag
23-
// * identifier: tag-std::ptr::Unique<&()>
24-
// 0: struct
25-
// * type: struct_tag
26-
// * identifier: tag-std::marker::PhantomData<&()>
27-
// 1: constant
28-
// * type: pointer
29-
// * width: 64
30-
// 0: pointer
31-
// * width: 64
32-
// 0: struct_tag
33-
// * identifier: tag-Unit
34-
// * value: 8
35-
// 2: constant
36-
// * type: unsignedbv
37-
// * #source_location:
38-
// * file: <built-in-additions>
39-
// * line: 1
40-
// * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
41-
// * width: 64
42-
// * #typedef: __CPROVER_size_t
43-
// * #c_type: unsigned_long_int
44-
// * #source_location:
45-
// * file: <built-in-additions>
46-
// * line: 16
47-
// * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
48-
// * value: 0
49-
// 1: constant
50-
// * type: unsignedbv
51-
// * #source_location:
52-
// * file: <built-in-additions>
53-
// * line: 1
54-
// * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
55-
// * width: 64
56-
// * #typedef: __CPROVER_size_t
57-
// * #c_type: unsigned_long_int
58-
// * #source_location:
59-
// * file: <built-in-additions>
60-
// * line: 16
61-
// * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
62-
// * value: 0
3+
// This test takes too long with all the std symbols. Use --legacy-linker for now.
4+
// kani-flags: --legacy-linker
635

6+
//! This harness was based on firecracker argument parsing code from arg_parser.rs in
7+
//! firecracker/src/utils/src. It used to get stuck in post-processing with unwind of two or more.
648
use std::collections::BTreeMap;
659

6610
pub struct ArgParser<'a> {

‎tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs

Lines changed: 7 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,12 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
// This is a regression test for size_and_align_of_dst computing the
4-
// size and alignment of a dynamically-sized type like
5-
// Arc<Mutex<dyn Subscriber>>.
3+
// This test takes too long with all the std symbols. Use --legacy-linker for now.
4+
// kani-flags: --legacy-linker
65

7-
// https://github.com/model-checking/kani/issues/426
8-
// Current Kani-time compiler panic in implementing drop_in_place:
9-
10-
// thread 'rustc' panicked at 'Function call does not type check:
11-
// "func":"Expr"{
12-
// "value":"Symbol"{
13-
// "identifier":"_RINvNtCsgWci0eQkB8o_4core3ptr13drop_in_placeNtNtNtCs1HAdiQHUxxm_3std10sys_common5mutex12MovableMutexECsb7rQPrKk64Y_4main"
14-
// },
15-
// "typ":"Code"{
16-
// "parameters":[
17-
// "Parameter"{
18-
// "typ":"Pointer"{
19-
// "typ":"StructTag(""tag-std::sys_common::mutex::MovableMutex"")"
20-
// },
21-
// }
22-
// ],
23-
// "return_type":"StructTag(""tag-Unit"")"
24-
// },
25-
// }"args":[
26-
// "Expr"{
27-
// "value":"Symbol"{
28-
// "identifier":"_RINvNtCsgWci0eQkB8o_4core3ptr13drop_in_placeINtNtNtCs1HAdiQHUxxm_3std4sync5mutex5MutexDNtCsb7rQPrKk64Y_4main10SubscriberEL_EEB1p_::1::var_1"
29-
// },
30-
// "typ":"StructTag(""tag-dyn Subscriber"")",
31-
// }
32-
// ]"', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:532:9"
6+
//! This is a regression test for size_and_align_of_dst computing the
7+
//! size and alignment of a dynamically-sized type like
8+
//! Arc<Mutex<dyn Subscriber>>.
9+
//! https://github.com/model-checking/kani/issues/426
3310
3411
use std::sync::Arc;
3512
use std::sync::Mutex;
@@ -61,6 +38,7 @@ impl Subscriber for DummySubscriber {
6138
}
6239

6340
#[kani::proof]
41+
#[kani::unwind(1)]
6442
fn main() {
6543
let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
6644
let mut data = s.lock().unwrap();

‎tests/kani/Slice/pathbuf.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
// kani-verify-fail
43

54
use std::fs;
65
use std::path::PathBuf;
76
#[kani::proof]
7+
#[kani::unwind(3)]
88
fn main() {
99
let buf = PathBuf::new();
10-
let _x = fs::remove_dir_all(buf);
10+
let _x = fs::remove_file(buf);
1111
}

‎tests/kani/Strings/parse.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//! This test is to check how Kani handle some std functions, such as parse.
5+
//! This test used to trigger a missing function before the MIR Linker.
6+
7+
#[kani::proof]
8+
#[kani::unwind(3)]
9+
pub fn main() {
10+
let strings = vec!["tofu", "93"];
11+
let numbers: Vec<_> = strings.into_iter().filter_map(|s| s.parse::<i32>().ok()).collect();
12+
assert_eq!(numbers.len(), 1);
13+
assert_eq!(numbers[0], 93);
14+
}

‎tests/ui/missing-function/replaced-description/main.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// Checks if the description for undefined functions has been updated to
5-
// "Function with missing definition is unreachable"
4+
// kani-flags: --legacy-linker
5+
//! Checks if the description for undefined functions has been updated to
6+
//! "Function with missing definition is unreachable"
67
78
#[kani::proof]
89
fn main() {

‎tests/ui/missing-function/rust-by-example-description/expected

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎tests/ui/missing-function/rust-by-example-description/main.rs

Lines changed: 0 additions & 13 deletions
This file was deleted.

0 commit comments

Comments
 (0)