Implement Arbitrary for PhantomData and PhantomPinned (rust-lang#2225)

Co-authored-by: Celina G. Val <[email protected]>

Author: zhassan-aws

library/kani/src/arbitrary.rs

@@ -3,7 +3,10 @@
 
 //! This module introduces the Arbitrary trait as well as implementation for primitive types and
 //! other std containers.
-use std::num::*;
+use std::{
+    marker::{PhantomData, PhantomPinned},
+    num::*,
+};
 
 /// This trait should be used to generate symbolic variables that represent any valid value of
 /// its type.
@@ -120,3 +123,15 @@ where
         if bool::any() { Ok(T::any()) } else { Err(E::any()) }
     }
 }
+
+impl<T: ?Sized> Arbitrary for std::marker::PhantomData<T> {
+    fn any() -> Self {
+        PhantomData
+    }
+}
+
+impl Arbitrary for std::marker::PhantomPinned {
+    fn any() -> Self {
+        PhantomPinned
+    }
+}

tests/ui/derive-arbitrary/phantom_data/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/ui/derive-arbitrary/phantom_data/test.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that Kani can automatically derive `Arbitrary` on a struct that has
+//! `std::marker::PhantomData`
+
+#[derive(kani::Arbitrary)]
+struct Foo<T> {
+    x: i32,
+    _f: std::marker::PhantomData<T>,
+}
+
+impl<T> Foo<T> {
+    fn new(v: i32) -> Self {
+        Self { x: v, _f: std::marker::PhantomData }
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let f: Foo<u16> = Foo::new(x);
+    assert_eq!(f.x, x);
+}

tests/ui/derive-arbitrary/phantom_pinned/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/ui/derive-arbitrary/phantom_pinned/test.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that Kani can automatically derive `Arbitrary` on a struct that has
+//! `std::marker::PhantomPinned`
+
+#[derive(kani::Arbitrary)]
+struct Foo {
+    x: i32,
+    _f: std::marker::PhantomPinned,
+}
+
+impl Foo {
+    fn new(v: i32) -> Self {
+        Self { x: v, _f: std::marker::PhantomPinned }
+    }
+}
+
+#[kani::proof]
+fn check_arbitrary_phantom_pinned() {
+    let x = kani::any();
+    let f: Foo = Foo::new(x);
+    assert_eq!(f.x, x);
+}