Add preconditions for disjoint_bitor (#347)

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

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <[email protected]>

Author: tautschnig

.github/workflows/kani.yml

@@ -78,9 +78,15 @@ jobs:
       # possible functions as that may take a lot longer than expected. Instead,
       # explicitly list all functions (or prefixes thereof) the proofs of which
       # are known to pass.
+      # Notes:
+      # - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
+      #   as whitespace is not supported, cf.
+      #   https://github.com/model-checking/kani/issues/4046
       - 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::__default_lib_allocator:: \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \

library/core/src/intrinsics/fallback.rs

@@ -7,6 +7,11 @@
 )]
 #![allow(missing_docs)]
 
+use safety::requires;
+
+#[cfg(kani)]
+use crate::kani;
+
 #[const_trait]
 #[rustc_const_unstable(feature = "core_intrinsics_fallbacks", issue = "none")]
 pub trait CarryingMulAdd: Copy + 'static {
@@ -132,6 +137,7 @@ macro_rules! impl_disjoint_bitor {
         impl const DisjointBitOr for $t {
             #[cfg_attr(miri, track_caller)]
             #[inline]
+            #[requires((self & other) == zero!($t))]
             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,