Skip to content

Commit

Permalink
attempt 1
Browse files Browse the repository at this point in the history
  • Loading branch information
carolynzech committed Feb 20, 2025
1 parent 87bbc0d commit 477ad90
Show file tree
Hide file tree
Showing 16 changed files with 141 additions and 220 deletions.
4 changes: 2 additions & 2 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
[submodule "library/stdarch"]
[submodule "stdarch"]
path = library/stdarch
url = https://github.com/rust-lang/stdarch.git
shallow = true
[submodule "library/backtrace"]
[submodule "backtrace"]
path = library/backtrace
url = https://github.com/rust-lang/backtrace-rs.git
shallow = true
90 changes: 90 additions & 0 deletions library/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

6 changes: 1 addition & 5 deletions library/alloc/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,8 @@ edition = "2021"

[dependencies]
core = { path = "../core" }
<<<<<<< HEAD
compiler_builtins = { version = "=0.1.138", features = ['rustc-dep-of-std'] }
safety = { path = "../contracts/safety" }
=======
compiler_builtins = { version = "=0.1.145", features = ['rustc-dep-of-std'] }
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
safety = { path = "../contracts/safety" }

[dev-dependencies]
rand = { version = "0.8.5", default-features = false, features = ["alloc"] }
Expand Down
5 changes: 0 additions & 5 deletions library/alloc/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -92,12 +92,7 @@
//
// Library features:
// tidy-alphabetical-start
<<<<<<< HEAD
#![cfg_attr(kani, feature(kani))]
#![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
#![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
=======
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
#![cfg_attr(test, feature(str_as_str))]
#![feature(alloc_layout_extra)]
#![feature(allocator_api)]
Expand Down
16 changes: 0 additions & 16 deletions library/core/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -15,25 +15,9 @@ edition = "2021"
test = false
bench = false

<<<<<<< HEAD
[[test]]
name = "coretests"
path = "tests/lib.rs"

[[bench]]
name = "corebenches"
path = "benches/lib.rs"
test = true

[dependencies]
safety = {path = "../contracts/safety" }

[dev-dependencies]
rand = { version = "0.8.5", default-features = false }
rand_xorshift = { version = "0.3.0", default-features = false }

=======
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
[features]
# Make panics and failed asserts immediately abort without formatting any message
panic_immediate_abort = []
Expand Down
22 changes: 8 additions & 14 deletions library/core/src/intrinsics/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4003,22 +4003,16 @@ pub const fn is_val_statically_known<T: Copy>(_arg: T) -> bool {
#[rustc_nounwind]
#[inline]
#[rustc_intrinsic]
<<<<<<< HEAD
// Const-unstable because `swap_nonoverlapping` is const-unstable.
#[rustc_const_unstable(feature = "const_typed_swap", issue = "none")]
#[rustc_intrinsic_const_stable_indirect]
#[rustc_allow_const_fn_unstable(const_swap_nonoverlapping)] // this is anyway not called since CTFE implements the intrinsic
#[cfg_attr(kani, kani::modifies(x))]
#[cfg_attr(kani, kani::modifies(y))]
#[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
#[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
#[requires(x.addr() != y.addr() || core::mem::size_of::<T>() == 0)]
#[requires(ub_checks::maybe_is_nonoverlapping(x as *const (), y as *const (), size_of::<T>(), 1))]
#[ensures(|_| ub_checks::can_dereference(x) && ub_checks::can_dereference(y))]
pub const unsafe fn typed_swap<T>(x: *mut T, y: *mut T) {
=======
#[rustc_intrinsic_const_stable_indirect]
#[rustc_allow_const_fn_unstable(const_swap_nonoverlapping)] // this is anyway not called since CTFE implements the intrinsic
pub const unsafe fn typed_swap_nonoverlapping<T>(x: *mut T, y: *mut T) {
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
// SAFETY: The caller provided single non-overlapping items behind
// pointers, so swapping them with `count: 1` is fine.
unsafe { ptr::swap_nonoverlapping(x, y, 1) };
Expand Down Expand Up @@ -4954,19 +4948,19 @@ mod verify {
use core::mem::MaybeUninit;
use kani::{AllocationStatus, Arbitrary, ArbitraryPointer, PointerGenerator};

#[kani::proof_for_contract(typed_swap)]
#[kani::proof_for_contract(typed_swap_nonoverlapping)]
pub fn check_typed_swap_u8() {
run_with_arbitrary_ptrs::<u8>(|x, y| unsafe { typed_swap(x, y) });
run_with_arbitrary_ptrs::<u8>(|x, y| unsafe { typed_swap_nonoverlapping(x, y) });
}

#[kani::proof_for_contract(typed_swap)]
#[kani::proof_for_contract(typed_swap_nonoverlapping)]
pub fn check_typed_swap_char() {
run_with_arbitrary_ptrs::<char>(|x, y| unsafe { typed_swap(x, y) });
run_with_arbitrary_ptrs::<char>(|x, y| unsafe { typed_swap_nonoverlapping(x, y) });
}

#[kani::proof_for_contract(typed_swap)]
#[kani::proof_for_contract(typed_swap_nonoverlapping)]
pub fn check_typed_swap_non_zero() {
run_with_arbitrary_ptrs::<core::num::NonZeroI32>(|x, y| unsafe { typed_swap(x, y) });
run_with_arbitrary_ptrs::<core::num::NonZeroI32>(|x, y| unsafe { typed_swap_nonoverlapping(x, y) });
}

#[kani::proof_for_contract(copy)]
Expand Down
8 changes: 0 additions & 8 deletions library/core/src/num/int_macros.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2136,11 +2136,7 @@ macro_rules! int_impl {
#[must_use = "this returns the result of the operation, \
without modifying the original"]
#[inline(always)]
<<<<<<< HEAD
#[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
=======
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
pub const fn wrapping_shl(self, rhs: u32) -> Self {
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
// out of bounds
Expand Down Expand Up @@ -2170,11 +2166,7 @@ macro_rules! int_impl {
#[must_use = "this returns the result of the operation, \
without modifying the original"]
#[inline(always)]
<<<<<<< HEAD
#[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
=======
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
pub const fn wrapping_shr(self, rhs: u32) -> Self {
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
// out of bounds
Expand Down
68 changes: 2 additions & 66 deletions library/core/src/num/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1604,68 +1604,8 @@ macro_rules! from_str_int_impl {
)*}
}

<<<<<<< HEAD
from_str_radix! { unsigned u8 u16 u32 u64 u128 }
from_str_radix! { signed i8 i16 i32 i64 i128 }

// Re-use the relevant implementation of from_str_radix for isize and usize to avoid outputting two
// identical functions.
macro_rules! from_str_radix_size_impl {
($($signedness:ident $t:ident $size:ty),*) => {$(
impl $size {
/// Converts a string slice in a given base to an integer.
///
/// The string is expected to be an optional
#[doc = sign_dependent_expr!{
$signedness ?
if signed {
" `+` or `-` "
}
if unsigned {
" `+` "
}
}]
/// sign followed by only digits. Leading and trailing non-digit characters (including
/// whitespace) represent an error. Underscores (which are accepted in rust literals)
/// also represent an error.
///
/// Digits are a subset of these characters, depending on `radix`:
/// * `0-9`
/// * `a-z`
/// * `A-Z`
///
/// # Panics
///
/// This function panics if `radix` is not in the range from 2 to 36.
///
/// # Examples
///
/// Basic usage:
/// ```
#[doc = concat!("assert_eq!(", stringify!($size), "::from_str_radix(\"A\", 16), Ok(10));")]
/// ```
/// Trailing space returns error:
/// ```
#[doc = concat!("assert!(", stringify!($size), "::from_str_radix(\"1 \", 10).is_err());")]
/// ```
#[stable(feature = "rust1", since = "1.0.0")]
#[rustc_const_stable(feature = "const_int_from_str", since = "1.82.0")]
#[inline]
pub const fn from_str_radix(src: &str, radix: u32) -> Result<$size, ParseIntError> {
match <$t>::from_str_radix(src, radix) {
Ok(x) => Ok(x as $size),
Err(e) => Err(e),
}
}
})*}
}

#[cfg(target_pointer_width = "16")]
from_str_radix_size_impl! { signed i16 isize, unsigned u16 usize }
#[cfg(target_pointer_width = "32")]
from_str_radix_size_impl! { signed i32 isize, unsigned u32 usize }
#[cfg(target_pointer_width = "64")]
from_str_radix_size_impl! { signed i64 isize, unsigned u64 usize }
from_str_int_impl! { signed isize i8 i16 i32 i64 i128 }
from_str_int_impl! { unsigned usize u8 u16 u32 u64 u128 }

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
Expand Down Expand Up @@ -2376,7 +2316,3 @@ mod verify {
checked_f128_to_int_unchecked_usize
);
}
=======
from_str_int_impl! { signed isize i8 i16 i32 i64 i128 }
from_str_int_impl! { unsigned usize u8 u16 u32 u64 u128 }
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
8 changes: 0 additions & 8 deletions library/core/src/num/uint_macros.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2238,11 +2238,7 @@ macro_rules! uint_impl {
#[must_use = "this returns the result of the operation, \
without modifying the original"]
#[inline(always)]
<<<<<<< HEAD
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
#[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
=======
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
pub const fn wrapping_shl(self, rhs: u32) -> Self {
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
// out of bounds
Expand Down Expand Up @@ -2275,11 +2271,7 @@ macro_rules! uint_impl {
#[must_use = "this returns the result of the operation, \
without modifying the original"]
#[inline(always)]
<<<<<<< HEAD
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
#[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
=======
>>>>>>> 6a0734179ff38467ed3169324d8f7ab4b07796ef
pub const fn wrapping_shr(self, rhs: u32) -> Self {
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
// out of bounds
Expand Down
Loading

0 comments on commit 477ad90

Please sign in to comment.