Add preconditions for disjoint_bitor

Uses the verbatim SAFETY comment as precondition to avoid spurious proof
failures.

Author: tautschnig

.github/workflows/kani.yml

@@ -81,6 +81,8 @@ jobs:
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern ">::disjoint_bitor" \
+            --include-pattern ">::unchecked_disjoint_bitor" \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \

library/core/src/intrinsics/fallback.rs

@@ -1,3 +1,8 @@
+use safety::requires;
+
+#[cfg(kani)]
+use crate::kani;
+
 #![unstable(
     feature = "core_intrinsics_fallbacks",
     reason = "The fallbacks will never be stable, as they exist only to be called \
@@ -132,6 +137,7 @@ macro_rules! impl_disjoint_bitor {
         impl const DisjointBitOr for $t {
             #[cfg_attr(miri, track_caller)]
             #[inline]
+            #[requires((self & other) == 0)]
             unsafe fn disjoint_bitor(self, other: Self) -> Self {
                 // Note that the assume here is required for UB detection in Miri!
 

library/core/src/num/uint_macros.rs

@@ -1265,6 +1265,7 @@ macro_rules! uint_impl {
         #[unstable(feature = "disjoint_bitor", issue = "135758")]
         #[rustc_const_unstable(feature = "disjoint_bitor", issue = "135758")]
         #[inline]
+        #[requires((self & other) == 0)]
         pub const unsafe fn unchecked_disjoint_bitor(self, other: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,