Add tests for issues related to std linking (#1801)

Add tests for #564, #208 and #87.

Unfortunately, it looks like there are still issues with with how we are
encoding panic threads and dynamic objects which are causing two of the
test cases to fail.

tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs

@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// This test takes too long with all the std symbols. Use --legacy-linker for now.
-// kani-flags: --legacy-linker
+// The original harness takes too long so we introduced a simplified version to run in CI.
+// kani-flags: --harness simplified
 
 //! 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
+//! We added a simplified version of the original harness from:
+//! <https://github.com/model-checking/kani/issues/426>
 
 use std::sync::Arc;
 use std::sync::Mutex;
@@ -37,9 +38,17 @@ impl Subscriber for DummySubscriber {
     }
 }
 
+#[kani::proof]
+#[kani::unwind(2)]
+fn simplified() {
+    let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
+    let data = s.lock().unwrap();
+    assert!(data.get() == 0);
+}
+
 #[kani::proof]
 #[kani::unwind(1)]
-fn main() {
+fn original() {
     let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
     let mut data = s.lock().unwrap();
     data.increment();

tests/kani/StdLink/fixme_panic_hook.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test was created to cover panic hook handling by Kani.
+//! Tracking issue: <https://github.com/model-checking/kani/issues/208>
+use std::panic;
+
+#[kani::proof]
+#[kani::unwind(2)]
+fn custom_hook() {
+    panic::set_hook(Box::new(|_| {
+        assert!(false);
+    }));
+
+    let _ = panic::take_hook();
+
+    panic!("Normal panic");
+}

tests/kani/StdLink/overlapping_traits.rs

@@ -0,0 +1,50 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+//! This test is to check how Kani handle some std functions. The original issue was:
+//! <https://github.com/model-checking/kani/issues/564>
+//! This code was extracted from Rust by Example book.
+trait UsernameWidget {
+    // Get the selected username out of this widget
+    fn get(&self) -> String;
+}
+
+trait AgeWidget {
+    // Get the selected age out of this widget
+    fn get(&self) -> u8;
+}
+
+// A form with both a UsernameWidget and an AgeWidget
+struct Form {
+    username: String,
+    age: u8,
+}
+
+impl UsernameWidget for Form {
+    fn get(&self) -> String {
+        self.username.clone()
+    }
+}
+
+impl AgeWidget for Form {
+    fn get(&self) -> u8 {
+        self.age
+    }
+}
+
+#[kani::proof]
+pub fn main() {
+    let form = Form { username: "rustacean".to_owned(), age: 28 };
+
+    // If you uncomment this line, you'll get an error saying
+    // "multiple `get` found". Because, after all, there are multiple methods
+    // named `get`.
+    // println!("{}", form.get());
+
+    let username = <Form as UsernameWidget>::get(&form);
+    assert_eq!("rustacean".to_owned(), username);
+    let age = <Form as AgeWidget>::get(&form);
+    assert_eq!(28, age);
+}