Replace struct impl of Invariant by Arbitrary (rust-lang#1401)

We have recently realized that implementing Invariant of Option, Result
and array has a limitation. This is not sufficient to generate arbitrary
values of types that only implements Arbitrary.

Thus, implement Arbitrary instead.

Author: celinval

library/kani/src/arbitrary.rs

@@ -20,3 +20,38 @@ where
         value
     }
 }
+
+impl<T, const N: usize> Arbitrary for [T; N]
+where
+    T: Arbitrary,
+{
+    fn any() -> Self {
+        // The "correct way" would be to MaybeUninit but there is performance penalty.
+        let mut data: [T; N] = unsafe { crate::any_raw() };
+
+        for elem in &mut data[..] {
+            *elem = T::any();
+        }
+
+        data
+    }
+}
+
+impl<T> Arbitrary for Option<T>
+where
+    T: Arbitrary,
+{
+    fn any() -> Self {
+        if bool::any() { Some(T::any()) } else { None }
+    }
+}
+
+impl<T, E> Arbitrary for Result<T, E>
+where
+    T: Arbitrary,
+    E: Arbitrary,
+{
+    fn any() -> Self {
+        if bool::any() { Ok(T::any()) } else { Err(E::any()) }
+    }
+}

library/kani/src/invariant.rs

@@ -71,39 +71,6 @@ unsafe impl Invariant for char {
     }
 }
 
-unsafe impl<T: Invariant, const N: usize> Invariant for [T; N] {
-    fn is_valid(&self) -> bool {
-        self.iter().all(|e| e.is_valid())
-    }
-}
-
-unsafe impl<T> Invariant for Option<T>
-where
-    T: Invariant,
-{
-    #[inline(always)]
-    fn is_valid(&self) -> bool {
-        if let Some(v) = self { v.is_valid() } else { matches!(*self, None) }
-    }
-}
-
-unsafe impl<T, E> Invariant for Result<T, E>
-where
-    T: Invariant,
-    E: Invariant,
-{
-    #[inline(always)]
-    fn is_valid(&self) -> bool {
-        if let Ok(v) = self {
-            v.is_valid()
-        } else if let Err(e) = self {
-            e.is_valid()
-        } else {
-            false
-        }
-    }
-}
-
 macro_rules! nonzero_invariant {
     ( $type: ty ) => {
         unsafe impl Invariant for $type {

tests/kani/Arbitrary/arbitrary_structs.rs

@@ -0,0 +1,108 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that users can use any Option, Result and array if they implement Arbitrary or Invariant.
+#![cfg_attr(kani, feature(min_specialization))]
+
+extern crate kani;
+use kani::Arbitrary;
+use kani::Invariant;
+
+trait PercentTrait {
+    fn val(&self) -> u8;
+    fn ok(&self) -> bool;
+}
+
+macro_rules! percent_type {
+    ( $type: tt ) => {
+        struct $type {
+            inner: u8,
+        }
+        impl PercentTrait for $type {
+            fn val(&self) -> u8 {
+                self.inner
+            }
+
+            fn ok(&self) -> bool {
+                self.inner <= 100
+            }
+        }
+    };
+}
+
+percent_type!(Percent);
+percent_type!(PercentInvariant);
+percent_type!(PercentArbitrary);
+
+unsafe impl Invariant for PercentInvariant {
+    fn is_valid(&self) -> bool {
+        self.ok()
+    }
+}
+
+impl Arbitrary for PercentArbitrary {
+    fn any() -> Self {
+        let val = kani::any();
+        kani::assume(val <= 100);
+        PercentArbitrary { inner: val }
+    }
+}
+
+unsafe impl Invariant for Percent {
+    fn is_valid(&self) -> bool {
+        self.ok()
+    }
+}
+
+impl Arbitrary for Percent {
+    fn any() -> Self {
+        let val = kani::any();
+        kani::assume(val <= 100);
+        Percent { inner: val }
+    }
+}
+
+fn check<T: PercentTrait + Arbitrary>() {
+    let var = Option::<T>::any();
+    match var {
+        None => assert!(T::any().ok()),
+        Some(p) => assert!(p.ok()),
+    }
+}
+
+fn check_result<T: PercentTrait + Arbitrary>() {
+    let var = Result::<T, ()>::any();
+    match var {
+        Err(_) => assert!(T::any().ok()),
+        Ok(p) => assert!(p.ok()),
+    }
+}
+
+fn check_array<T: PercentTrait + Arbitrary>() {
+    let var: [T; 10] = kani::any();
+    assert!(var.iter().all(|e| e.ok()));
+}
+
+#[kani::proof]
+#[kani::unwind(12)]
+fn check_invariant() {
+    check::<PercentInvariant>();
+    check_result::<PercentInvariant>();
+    check_array::<PercentInvariant>();
+}
+
+#[kani::proof]
+#[kani::unwind(12)]
+fn check_arbitrary() {
+    check::<PercentArbitrary>();
+    check_result::<PercentArbitrary>();
+    check_array::<PercentArbitrary>();
+}
+
+#[kani::proof]
+#[kani::unwind(12)]
+fn check_both() {
+    check::<Percent>();
+    check_result::<Percent>();
+    check_array::<Percent>();
+}

tests/kani/FunctionAbstractions/mem_replace.rs

@@ -17,7 +17,7 @@ unsafe impl kani::Invariant for Pair {
     }
 }
 
-fn test<T: kani::Invariant + std::cmp::PartialEq + Clone>() {
+fn test<T: kani::Arbitrary + std::cmp::PartialEq + Clone>() {
     let mut var1 = kani::any::<T>();
     let var2 = kani::any::<T>();
     let old_var1 = var1.clone();

tests/kani/FunctionAbstractions/mem_swap.rs

@@ -17,7 +17,7 @@ unsafe impl kani::Invariant for Pair {
     }
 }
 
-fn test<T: kani::Invariant + std::cmp::PartialEq + Clone>() {
+fn test<T: kani::Arbitrary + std::cmp::PartialEq + Clone>() {
     let mut var1 = kani::any::<T>();
     let mut var2 = kani::any::<T>();
     let old_var1 = var1.clone();