Skip to content

Commit 344205a

Browse files
committed
Update Kani version & fix conflicts
1 parent b6a29a4 commit 344205a

File tree

16 files changed

+69
-247
lines changed

16 files changed

+69
-247
lines changed

library/alloc/Cargo.toml

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,8 @@ edition = "2021"
1010

1111
[dependencies]
1212
core = { path = "../core" }
13-
<<<<<<< HEAD
14-
compiler_builtins = { version = "=0.1.138", features = ['rustc-dep-of-std'] }
15-
safety = { path = "../contracts/safety" }
16-
=======
1713
compiler_builtins = { version = "=0.1.145", features = ['rustc-dep-of-std'] }
18-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
14+
safety = { path = "../contracts/safety" }
1915

2016
[dev-dependencies]
2117
rand = { version = "0.8.5", default-features = false, features = ["alloc"] }

library/alloc/src/lib.rs

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -92,12 +92,7 @@
9292
//
9393
// Library features:
9494
// tidy-alphabetical-start
95-
<<<<<<< HEAD
9695
#![cfg_attr(kani, feature(kani))]
97-
#![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
98-
#![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
99-
=======
100-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
10196
#![cfg_attr(test, feature(str_as_str))]
10297
#![feature(alloc_layout_extra)]
10398
#![feature(allocator_api)]

library/core/Cargo.toml

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -15,25 +15,9 @@ edition = "2021"
1515
test = false
1616
bench = false
1717

18-
<<<<<<< HEAD
19-
[[test]]
20-
name = "coretests"
21-
path = "tests/lib.rs"
22-
23-
[[bench]]
24-
name = "corebenches"
25-
path = "benches/lib.rs"
26-
test = true
27-
2818
[dependencies]
2919
safety = {path = "../contracts/safety" }
3020

31-
[dev-dependencies]
32-
rand = { version = "0.8.5", default-features = false }
33-
rand_xorshift = { version = "0.3.0", default-features = false }
34-
35-
=======
36-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
3721
[features]
3822
# Make panics and failed asserts immediately abort without formatting any message
3923
panic_immediate_abort = []

library/core/src/intrinsics/mod.rs

Lines changed: 27 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -64,13 +64,13 @@
6464
)]
6565
#![allow(missing_docs)]
6666

67-
use crate::marker::{DiscriminantKind, Tuple};
68-
use crate::mem::SizedTypeProperties;
69-
use crate::{ptr, ub_checks};
7067
use safety::{ensures, requires};
7168

7269
#[cfg(kani)]
7370
use crate::kani;
71+
use crate::marker::{DiscriminantKind, Tuple};
72+
use crate::mem::SizedTypeProperties;
73+
use crate::{ptr, ub_checks};
7474

7575
pub mod fallback;
7676
pub mod mir;
@@ -4003,22 +4003,16 @@ pub const fn is_val_statically_known<T: Copy>(_arg: T) -> bool {
40034003
#[rustc_nounwind]
40044004
#[inline]
40054005
#[rustc_intrinsic]
4006-
<<<<<<< HEAD
4007-
// Const-unstable because `swap_nonoverlapping` is const-unstable.
4008-
#[rustc_const_unstable(feature = "const_typed_swap", issue = "none")]
4006+
#[rustc_intrinsic_const_stable_indirect]
4007+
#[rustc_allow_const_fn_unstable(const_swap_nonoverlapping)] // this is anyway not called since CTFE implements the intrinsic
40094008
#[cfg_attr(kani, kani::modifies(x))]
40104009
#[cfg_attr(kani, kani::modifies(y))]
40114010
#[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
40124011
#[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
40134012
#[requires(x.addr() != y.addr() || core::mem::size_of::<T>() == 0)]
40144013
#[requires(ub_checks::maybe_is_nonoverlapping(x as *const (), y as *const (), size_of::<T>(), 1))]
40154014
#[ensures(|_| ub_checks::can_dereference(x) && ub_checks::can_dereference(y))]
4016-
pub const unsafe fn typed_swap<T>(x: *mut T, y: *mut T) {
4017-
=======
4018-
#[rustc_intrinsic_const_stable_indirect]
4019-
#[rustc_allow_const_fn_unstable(const_swap_nonoverlapping)] // this is anyway not called since CTFE implements the intrinsic
40204015
pub const unsafe fn typed_swap_nonoverlapping<T>(x: *mut T, y: *mut T) {
4021-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
40224016
// SAFETY: The caller provided single non-overlapping items behind
40234017
// pointers, so swapping them with `count: 1` is fine.
40244018
unsafe { ptr::swap_nonoverlapping(x, y, 1) };
@@ -4949,24 +4943,28 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
49494943
#[cfg(kani)]
49504944
#[unstable(feature = "kani", issue = "none")]
49514945
mod verify {
4952-
use super::*;
4953-
use crate::kani;
49544946
use core::mem::MaybeUninit;
4947+
49554948
use kani::{AllocationStatus, Arbitrary, ArbitraryPointer, PointerGenerator};
49564949

4957-
#[kani::proof_for_contract(typed_swap)]
4950+
use super::*;
4951+
use crate::kani;
4952+
4953+
#[kani::proof_for_contract(typed_swap_nonoverlapping)]
49584954
pub fn check_typed_swap_u8() {
4959-
run_with_arbitrary_ptrs::<u8>(|x, y| unsafe { typed_swap(x, y) });
4955+
run_with_arbitrary_ptrs::<u8>(|x, y| unsafe { typed_swap_nonoverlapping(x, y) });
49604956
}
49614957

4962-
#[kani::proof_for_contract(typed_swap)]
4958+
#[kani::proof_for_contract(typed_swap_nonoverlapping)]
49634959
pub fn check_typed_swap_char() {
4964-
run_with_arbitrary_ptrs::<char>(|x, y| unsafe { typed_swap(x, y) });
4960+
run_with_arbitrary_ptrs::<char>(|x, y| unsafe { typed_swap_nonoverlapping(x, y) });
49654961
}
49664962

4967-
#[kani::proof_for_contract(typed_swap)]
4963+
#[kani::proof_for_contract(typed_swap_nonoverlapping)]
49684964
pub fn check_typed_swap_non_zero() {
4969-
run_with_arbitrary_ptrs::<core::num::NonZeroI32>(|x, y| unsafe { typed_swap(x, y) });
4965+
run_with_arbitrary_ptrs::<core::num::NonZeroI32>(|x, y| unsafe {
4966+
typed_swap_nonoverlapping(x, y)
4967+
});
49704968
}
49714969

49724970
#[kani::proof_for_contract(copy)]
@@ -4981,7 +4979,7 @@ mod verify {
49814979
// `copy_nonoverlapping`.
49824980
// Kani contract checking would fail due to existing restriction on calls to
49834981
// the function under verification.
4984-
let gen_any_ptr = |buf: &mut [MaybeUninit<char>; 100]| -> *mut char {
4982+
let gen_any_ptr = |buf: &mut [MaybeUninit<char>; 100]| -> *mut char {
49854983
let base = buf.as_mut_ptr() as *mut u8;
49864984
base.wrapping_add(kani::any_where(|offset: &usize| *offset < 400)) as *mut char
49874985
};
@@ -4996,13 +4994,13 @@ mod verify {
49964994
let dst = if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) };
49974995
unsafe { copy_nonoverlapping(src, dst, kani::any()) }
49984996
}
4999-
5000-
//We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does
4997+
4998+
//We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does
50014999
//not currently support contracts (https://github.com/model-checking/kani/issues/3345)
50025000
#[requires(crate::mem::size_of::<T>() == crate::mem::size_of::<U>())] //T and U have same size (transmute_unchecked does not guarantee this)
50035001
#[requires(ub_checks::can_dereference(&input as *const T as *const U))] //output can be deref'd as value of type U
50045002
#[allow(dead_code)]
5005-
unsafe fn transmute_unchecked_wrapper<T,U>(input: T) -> U {
5003+
unsafe fn transmute_unchecked_wrapper<T, U>(input: T) -> U {
50065004
unsafe { transmute_unchecked(input) }
50075005
}
50085006

@@ -5058,7 +5056,7 @@ mod verify {
50585056
//tests that transmute works correctly when transmuting something with zero size
50595057
#[kani::proof_for_contract(transmute_unchecked_wrapper)]
50605058
fn transmute_zero_size() {
5061-
let empty_arr: [u8;0] = [];
5059+
let empty_arr: [u8; 0] = [];
50625060
let unit_val: () = unsafe { transmute_unchecked_wrapper(empty_arr) };
50635061
assert!(unit_val == ());
50645062
}
@@ -5076,7 +5074,7 @@ mod verify {
50765074
let src: $src = kani::any();
50775075
let dst: $dst = unsafe { transmute_unchecked_wrapper(src) };
50785076
let src2: $src = unsafe { transmute_unchecked_wrapper(dst) };
5079-
assert_eq!(src,src2);
5077+
assert_eq!(src, src2);
50805078
}
50815079
};
50825080
}
@@ -5104,28 +5102,17 @@ mod verify {
51045102
#[kani::proof_for_contract(write_bytes)]
51055103
fn check_write_bytes() {
51065104
let mut generator = PointerGenerator::<100>::new();
5107-
let ArbitraryPointer {
5108-
ptr,
5109-
status,
5110-
..
5111-
} = generator.any_alloc_status::<char>();
5105+
let ArbitraryPointer { ptr, status, .. } = generator.any_alloc_status::<char>();
51125106
kani::assume(supported_status(status));
51135107
unsafe { write_bytes(ptr, kani::any(), kani::any()) };
51145108
}
51155109

51165110
fn run_with_arbitrary_ptrs<T: Arbitrary>(harness: impl Fn(*mut T, *mut T)) {
51175111
let mut generator1 = PointerGenerator::<100>::new();
51185112
let mut generator2 = PointerGenerator::<100>::new();
5119-
let ArbitraryPointer {
5120-
ptr: src,
5121-
status: src_status,
5122-
..
5123-
} = generator1.any_alloc_status::<T>();
5124-
let ArbitraryPointer {
5125-
ptr: dst,
5126-
status: dst_status,
5127-
..
5128-
} = if kani::any() {
5113+
let ArbitraryPointer { ptr: src, status: src_status, .. } =
5114+
generator1.any_alloc_status::<T>();
5115+
let ArbitraryPointer { ptr: dst, status: dst_status, .. } = if kani::any() {
51295116
generator1.any_alloc_status::<T>()
51305117
} else {
51315118
generator2.any_alloc_status::<T>()

library/core/src/num/int_macros.rs

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2136,11 +2136,7 @@ macro_rules! int_impl {
21362136
#[must_use = "this returns the result of the operation, \
21372137
without modifying the original"]
21382138
#[inline(always)]
2139-
<<<<<<< HEAD
21402139
#[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
2141-
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
2142-
=======
2143-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
21442140
pub const fn wrapping_shl(self, rhs: u32) -> Self {
21452141
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
21462142
// out of bounds
@@ -2170,11 +2166,7 @@ macro_rules! int_impl {
21702166
#[must_use = "this returns the result of the operation, \
21712167
without modifying the original"]
21722168
#[inline(always)]
2173-
<<<<<<< HEAD
21742169
#[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
2175-
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
2176-
=======
2177-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
21782170
pub const fn wrapping_shr(self, rhs: u32) -> Self {
21792171
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
21802172
// out of bounds

library/core/src/num/mod.rs

Lines changed: 2 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -1604,68 +1604,8 @@ macro_rules! from_str_int_impl {
16041604
)*}
16051605
}
16061606

1607-
<<<<<<< HEAD
1608-
from_str_radix! { unsigned u8 u16 u32 u64 u128 }
1609-
from_str_radix! { signed i8 i16 i32 i64 i128 }
1610-
1611-
// Re-use the relevant implementation of from_str_radix for isize and usize to avoid outputting two
1612-
// identical functions.
1613-
macro_rules! from_str_radix_size_impl {
1614-
($($signedness:ident $t:ident $size:ty),*) => {$(
1615-
impl $size {
1616-
/// Converts a string slice in a given base to an integer.
1617-
///
1618-
/// The string is expected to be an optional
1619-
#[doc = sign_dependent_expr!{
1620-
$signedness ?
1621-
if signed {
1622-
" `+` or `-` "
1623-
}
1624-
if unsigned {
1625-
" `+` "
1626-
}
1627-
}]
1628-
/// sign followed by only digits. Leading and trailing non-digit characters (including
1629-
/// whitespace) represent an error. Underscores (which are accepted in rust literals)
1630-
/// also represent an error.
1631-
///
1632-
/// Digits are a subset of these characters, depending on `radix`:
1633-
/// * `0-9`
1634-
/// * `a-z`
1635-
/// * `A-Z`
1636-
///
1637-
/// # Panics
1638-
///
1639-
/// This function panics if `radix` is not in the range from 2 to 36.
1640-
///
1641-
/// # Examples
1642-
///
1643-
/// Basic usage:
1644-
/// ```
1645-
#[doc = concat!("assert_eq!(", stringify!($size), "::from_str_radix(\"A\", 16), Ok(10));")]
1646-
/// ```
1647-
/// Trailing space returns error:
1648-
/// ```
1649-
#[doc = concat!("assert!(", stringify!($size), "::from_str_radix(\"1 \", 10).is_err());")]
1650-
/// ```
1651-
#[stable(feature = "rust1", since = "1.0.0")]
1652-
#[rustc_const_stable(feature = "const_int_from_str", since = "1.82.0")]
1653-
#[inline]
1654-
pub const fn from_str_radix(src: &str, radix: u32) -> Result<$size, ParseIntError> {
1655-
match <$t>::from_str_radix(src, radix) {
1656-
Ok(x) => Ok(x as $size),
1657-
Err(e) => Err(e),
1658-
}
1659-
}
1660-
})*}
1661-
}
1662-
1663-
#[cfg(target_pointer_width = "16")]
1664-
from_str_radix_size_impl! { signed i16 isize, unsigned u16 usize }
1665-
#[cfg(target_pointer_width = "32")]
1666-
from_str_radix_size_impl! { signed i32 isize, unsigned u32 usize }
1667-
#[cfg(target_pointer_width = "64")]
1668-
from_str_radix_size_impl! { signed i64 isize, unsigned u64 usize }
1607+
from_str_int_impl! { signed isize i8 i16 i32 i64 i128 }
1608+
from_str_int_impl! { unsigned usize u8 u16 u32 u64 u128 }
16691609

16701610
#[cfg(kani)]
16711611
#[unstable(feature = "kani", issue = "none")]
@@ -2376,7 +2316,3 @@ mod verify {
23762316
checked_f128_to_int_unchecked_usize
23772317
);
23782318
}
2379-
=======
2380-
from_str_int_impl! { signed isize i8 i16 i32 i64 i128 }
2381-
from_str_int_impl! { unsigned usize u8 u16 u32 u64 u128 }
2382-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534

library/core/src/num/uint_macros.rs

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2238,11 +2238,7 @@ macro_rules! uint_impl {
22382238
#[must_use = "this returns the result of the operation, \
22392239
without modifying the original"]
22402240
#[inline(always)]
2241-
<<<<<<< HEAD
2242-
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
22432241
#[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
2244-
=======
2245-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
22462242
pub const fn wrapping_shl(self, rhs: u32) -> Self {
22472243
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
22482244
// out of bounds
@@ -2275,11 +2271,7 @@ macro_rules! uint_impl {
22752271
#[must_use = "this returns the result of the operation, \
22762272
without modifying the original"]
22772273
#[inline(always)]
2278-
<<<<<<< HEAD
2279-
#[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_shifts))]
22802274
#[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
2281-
=======
2282-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
22832275
pub const fn wrapping_shr(self, rhs: u32) -> Self {
22842276
// SAFETY: the masking by the bitsize of the type ensures that we do not shift
22852277
// out of bounds

library/core/src/ptr/alignment.rs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -49,12 +49,9 @@ impl Alignment {
4949
/// but in an `Alignment` instead of a `usize`.
5050
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
5151
#[inline]
52-
<<<<<<< HEAD
52+
#[must_use]
5353
#[requires(mem::align_of::<T>().is_power_of_two())]
5454
#[ensures(|result| result.as_usize().is_power_of_two())]
55-
=======
56-
#[must_use]
57-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
5855
pub const fn of<T>() -> Self {
5956
// This can't actually panic since type alignment is always a power of two.
6057
const { Alignment::new(mem::align_of::<T>()).unwrap() }

library/core/src/ptr/mod.rs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -395,12 +395,9 @@
395395
#![allow(clippy::not_unsafe_ptr_arg_deref)]
396396

397397
use crate::cmp::Ordering;
398-
<<<<<<< HEAD
398+
use crate::intrinsics::const_eval_select;
399399
#[cfg(kani)]
400400
use crate::kani;
401-
=======
402-
use crate::intrinsics::const_eval_select;
403-
>>>>>>> 9c1e515a1356d2d232f1823051c3dc7bd948b534
404401
use crate::marker::FnPtr;
405402
use crate::mem::{self, MaybeUninit, SizedTypeProperties};
406403
use crate::{fmt, hash, intrinsics, ub_checks};

0 commit comments

Comments
 (0)