Enable MIR Linker by default and adjust tests (#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.

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

@@ -1,3 +1,3 @@
 FAILURE\
-unwinding assertion loop 2
+unwinding assertion loop
 VERIFICATION:- FAILED

kani-driver/src/args.rs

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

kani-driver/src/call_cargo.rs

@@ -62,7 +62,7 @@ impl KaniSession {
 
         // Arguments that will only be passed to the target package.
         let mut pkg_args: Vec<OsString> = vec![];
-        if self.args.mir_linker {
+        if !self.args.legacy_linker {
             // Only provide reachability flag to the target package.
             pkg_args.push("--".into());
             if self.args.function.is_some() {

kani-driver/src/call_single_file.rs

@@ -48,14 +48,12 @@ impl KaniSession {
         }
 
         let mut kani_args = self.kani_specific_flags();
-        if self.args.mir_linker {
-            if self.args.function.is_some() {
-                kani_args.push("--reachability=pub_fns".into());
-            } else {
-                kani_args.push("--reachability=harnesses".into());
-            }
-        } else {
+        if self.args.legacy_linker {
             kani_args.push("--reachability=legacy".into());
+        } else if self.args.function.is_some() {
+            kani_args.push("--reachability=pub_fns".into());
+        } else {
+            kani_args.push("--reachability=harnesses".into());
         }
 
         let mut rustc_args = self.kani_rustc_flags();

scripts/codegen-firecracker.sh

@@ -26,8 +26,9 @@ cd $KANI_DIR/firecracker/src/devices/src/virtio/
 # Disable warnings until https://github.com/model-checking/kani/issues/573 is fixed
 export RUSTC_LOG=error
 export RUST_BACKTRACE=1
-# Kani cannot locate Cargo.toml correctly: https://github.com/model-checking/kani/issues/717
-cargo kani --only-codegen
+# Use the legacy linker for now since we want to maximize the code that we are compiling from firecracker.
+# The MIR Linker will by default only collect code relevant to proof harnesses, however, firecracker has none.
+cargo kani --only-codegen --legacy-linker
 
 echo
 echo "Finished Firecracker codegen regression successfully..."

tests/cargo-ui/dry-run/expected

@@ -1,4 +1,5 @@
-KANIFLAGS="--goto-c --log-level=warn --assertion-reach-checks --reachability=legacy -C symbol-mangling-version=v0" RUSTC=
+KANIFLAGS="--goto-c
+RUSTC=
 RUSTFLAGS="--kani-flags" cargo rustc
 goto-cc 
 goto-cc

tests/expected/drop/expected

@@ -1,10 +1,6 @@
 Status: UNDETERMINED\
 Description: "assertion failed: self.w_id == 0"\
-in function <Wrapper<DummyImpl> as std::ops::Drop>::drop
-
-Status: UNDETERMINED\
-Description: "assertion failed: self.id == 1"\
-in function <DummyImpl as std::ops::Drop>::drop
+in function <Wrapper<dyn DummyTrait> as std::ops::Drop>::drop
 
 Status: FAILURE\
 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

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

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

@@ -1,7 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
+// kani-flags: --legacy-linker
+//! The MIR linker errors are not quite user friendly. For more details, see
+//! <https://github.com/model-checking/kani/issues/1740>
+//! Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
+
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

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

@@ -1,7 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks that `copy_nonoverlapping` fails when `src` is not aligned.
+// kani-flags: --legacy-linker
+//! The MIR linker errors are not quite user friendly. For more details, see
+//! <https://github.com/model-checking/kani/issues/1740>
+//! Checks that `copy_nonoverlapping` fails when `src` is not aligned.
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

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

@@ -1,7 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks that `copy` fails when `dst` is not aligned.
+// kani-flags: --legacy-linker
+//! The MIR linker errors are not quite user friendly. For more details, see
+//! <https://github.com/model-checking/kani/issues/1740>
+//! Checks that `copy` fails when `dst` is not aligned.
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

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

@@ -1,7 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks that `copy` fails when `src` is not aligned.
+// kani-flags: --legacy-linker
+//! The MIR linker errors are not quite user friendly. For more details, see
+//! <https://github.com/model-checking/kani/issues/1740>
+//! Checks that `copy` fails when `src` is not aligned.
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

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

@@ -1,10 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks that `write_bytes` fails when `dst` is not aligned.
-
-// This test is a modified version of the example in
-// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+// kani-flags: --legacy-linker
+//! The MIR linker errors are not quite user friendly. For more details, see
+//! <https://github.com/model-checking/kani/issues/1740>
+//! Checks that `write_bytes` fails when `dst` is not aligned.
+//! This test is a modified version of the example in
+//! https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
 use std::intrinsics::write_bytes;
 
 #[kani::proof]

tests/kani/FatPointers/boxslice2.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
 // Casts boxed array to boxed slice (example taken from rust documentation)
 use std::str;

tests/kani/Refs/main.rs

@@ -1,66 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// running with a unwind of 1 passes; running with unwind of two gets stuck in post-processing
-// from arg_parser.rs in firecracker/src/utils/src
-
-// warning: ignoring typecast
-//   * type: struct_tag
-//       * identifier: tag-std::alloc::Global
-//   0: struct
-//       * type: struct_tag
-//           * identifier: tag-std::mem::ManuallyDrop<std::vec::Vec<&()>>
-//       0: struct
-//           * type: struct_tag
-//               * identifier: tag-std::vec::Vec<&()>
-//           0: struct
-//               * type: struct_tag
-//                   * identifier: tag-alloc::raw_vec::RawVec<&()>
-//               0: struct
-//                   * type: struct_tag
-//                       * identifier: tag-std::alloc::Global
-//               1: struct
-//                   * type: struct_tag
-//                       * identifier: tag-std::ptr::Unique<&()>
-//                   0: struct
-//                       * type: struct_tag
-//                           * identifier: tag-std::marker::PhantomData<&()>
-//                   1: constant
-//                       * type: pointer
-//                           * width: 64
-//                           0: pointer
-//                               * width: 64
-//                               0: struct_tag
-//                                   * identifier: tag-Unit
-//                       * value: 8
-//               2: constant
-//                   * type: unsignedbv
-//                       * #source_location:
-//                         * file: <built-in-additions>
-//                         * line: 1
-//                         * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
-//                       * width: 64
-//                       * #typedef: __CPROVER_size_t
-//                       * #c_type: unsigned_long_int
-//                   * #source_location:
-//                     * file: <built-in-additions>
-//                     * line: 16
-//                     * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
-//                   * value: 0
-//           1: constant
-//               * type: unsignedbv
-//                   * #source_location:
-//                     * file: <built-in-additions>
-//                     * line: 1
-//                     * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
-//                   * width: 64
-//                   * #typedef: __CPROVER_size_t
-//                   * #c_type: unsigned_long_int
-//               * #source_location:
-//                 * file: <built-in-additions>
-//                 * line: 16
-//                 * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
-//               * value: 0
+// This test takes too long with all the std symbols. Use --legacy-linker for now.
+// kani-flags: --legacy-linker
 
+//! This harness was based on firecracker argument parsing code from arg_parser.rs in
+//! firecracker/src/utils/src. It used to get stuck in post-processing with unwind of two or more.
 use std::collections::BTreeMap;
 
 pub struct ArgParser<'a> {

tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs

@@ -1,35 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// This is a regression test for size_and_align_of_dst computing the
-// size and alignment of a dynamically-sized type like
-// Arc<Mutex<dyn Subscriber>>.
+// This test takes too long with all the std symbols. Use --legacy-linker for now.
+// kani-flags: --legacy-linker
 
-// https://github.com/model-checking/kani/issues/426
-// Current Kani-time compiler panic in implementing drop_in_place:
-
-// thread 'rustc' panicked at 'Function call does not type check:
-// "func":"Expr"{
-//     "value":"Symbol"{
-//        "identifier":"_RINvNtCsgWci0eQkB8o_4core3ptr13drop_in_placeNtNtNtCs1HAdiQHUxxm_3std10sys_common5mutex12MovableMutexECsb7rQPrKk64Y_4main"
-//     },
-//     "typ":"Code"{
-//        "parameters":[
-//           "Parameter"{
-//              "typ":"Pointer"{
-//                 "typ":"StructTag(""tag-std::sys_common::mutex::MovableMutex"")"
-//              },
-//           }
-//        ],
-//        "return_type":"StructTag(""tag-Unit"")"
-//     },
-//  }"args":[
-//     "Expr"{
-//        "value":"Symbol"{
-//           "identifier":"_RINvNtCsgWci0eQkB8o_4core3ptr13drop_in_placeINtNtNtCs1HAdiQHUxxm_3std4sync5mutex5MutexDNtCsb7rQPrKk64Y_4main10SubscriberEL_EEB1p_::1::var_1"
-//        },
-//        "typ":"StructTag(""tag-dyn Subscriber"")",
-//     }
-//  ]"', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:532:9"
+//! This is a regression test for size_and_align_of_dst computing the
+//! size and alignment of a dynamically-sized type like
+//! Arc<Mutex<dyn Subscriber>>.
+//! https://github.com/model-checking/kani/issues/426
 
 use std::sync::Arc;
 use std::sync::Mutex;
@@ -61,6 +38,7 @@ impl Subscriber for DummySubscriber {
 }
 
 #[kani::proof]
+#[kani::unwind(1)]
 fn main() {
     let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
     let mut data = s.lock().unwrap();

tests/kani/Slice/pathbuf.rs

@@ -1,11 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
 use std::fs;
 use std::path::PathBuf;
 #[kani::proof]
+#[kani::unwind(3)]
 fn main() {
     let buf = PathBuf::new();
-    let _x = fs::remove_dir_all(buf);
+    let _x = fs::remove_file(buf);
 }

tests/kani/Strings/parse.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test is to check how Kani handle some std functions, such as parse.
+//! This test used to trigger a missing function before the MIR Linker.
+
+#[kani::proof]
+#[kani::unwind(3)]
+pub fn main() {
+    let strings = vec!["tofu", "93"];
+    let numbers: Vec<_> = strings.into_iter().filter_map(|s| s.parse::<i32>().ok()).collect();
+    assert_eq!(numbers.len(), 1);
+    assert_eq!(numbers[0], 93);
+}

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

@@ -1,8 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks if the description for undefined functions has been updated to
-// "Function with missing definition is unreachable"
+// kani-flags: --legacy-linker
+//! Checks if the description for undefined functions has been updated to
+//! "Function with missing definition is unreachable"
 
 #[kani::proof]
 fn main() {