Skip to content

Commit

Permalink
Apply format changes to our repository
Browse files Browse the repository at this point in the history
  • Loading branch information
celinval committed Dec 4, 2024
1 parent 16a9a86 commit a56634c
Show file tree
Hide file tree
Showing 23 changed files with 383 additions and 273 deletions.
26 changes: 13 additions & 13 deletions library/core/src/alloc/layout.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,20 @@
// collections, resulting in having to optimize down excess IR multiple times.
// Your performance intuition is useless. Run perf.

use safety::{ensures, Invariant, requires};
use safety::{Invariant, ensures, requires};

#[cfg(kani)]
use crate::cmp;
use crate::error::Error;
use crate::intrinsics::{unchecked_add, unchecked_mul, unchecked_sub};
use crate::mem::SizedTypeProperties;
use crate::ptr::{Alignment, NonNull};
use crate::{assert_unsafe_precondition, fmt, mem};

#[cfg(kani)]
use crate::kani;
#[cfg(kani)]
use crate::cmp;

use crate::mem::SizedTypeProperties;
use crate::ptr::{Alignment, NonNull};
// Used only for contract verification.
#[allow(unused_imports)]
use crate::ub_checks::Invariant;
use crate::{assert_unsafe_precondition, fmt, mem};

// While this function is used in one place and its implementation
// could be inlined, the previous attempts to do so made rustc
Expand Down Expand Up @@ -624,14 +623,15 @@ impl fmt::Display for LayoutError {
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;

impl kani::Arbitrary for Layout {
fn any() -> Self {
let align = kani::any::<Alignment>();
let size = kani::any_where(|s: &usize| *s <= isize::MAX as usize - (align.as_usize() - 1));
let size =
kani::any_where(|s: &usize| *s <= isize::MAX as usize - (align.as_usize() - 1));
unsafe { Layout { size, align } }
}
}
Expand Down Expand Up @@ -684,8 +684,8 @@ mod verify {
pub fn check_for_value_i32() {
let x = kani::any::<i32>();
let _ = Layout::for_value::<i32>(&x);
let array : [i32; 2] = [1, 2];
let _ = Layout::for_value::<[i32]>(&array[1 .. 1]);
let array: [i32; 2] = [1, 2];
let _ = Layout::for_value::<[i32]>(&array[1..1]);
let trait_ref: &dyn core::fmt::Debug = &x;
let _ = Layout::for_value::<dyn core::fmt::Debug>(trait_ref);
// TODO: the case of an extern type as unsized tail is not yet covered
Expand Down Expand Up @@ -724,7 +724,7 @@ mod verify {
pub fn check_padding_needed_for() {
let layout = kani::any::<Layout>();
let a2 = kani::any::<usize>();
if(a2.is_power_of_two() && a2 <= layout.align()) {
if (a2.is_power_of_two() && a2 <= layout.align()) {
let _ = layout.padding_needed_for(a2);
}
}
Expand Down
9 changes: 5 additions & 4 deletions library/core/src/ascii/ascii_char.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
//! helps with clarity as we're also referring to `char` intentionally in here.
use safety::{ensures, requires};
use crate::mem::transmute;
use crate::{assert_unsafe_precondition, fmt};

#[cfg(kani)]
use crate::kani;
use crate::mem::transmute;
use crate::{assert_unsafe_precondition, fmt};

/// One of the 128 Unicode characters from U+0000 through U+007F,
/// often known as the [ASCII] subset.
Expand Down Expand Up @@ -623,11 +623,12 @@ impl fmt::Debug for AsciiChar {
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;
use AsciiChar;

use super::*;

#[kani::proof_for_contract(AsciiChar::from_u8)]
fn check_from_u8() {
let b: u8 = kani::any();
Expand Down
10 changes: 5 additions & 5 deletions library/core/src/char/convert.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
//! Character conversions.
use safety::{requires, ensures};
use safety::{ensures, requires};

use crate::char::TryFromCharError;
use crate::error::Error;
use crate::fmt;
#[cfg(kani)]
use crate::kani;
use crate::mem::transmute;
use crate::str::FromStr;
use crate::ub_checks::assert_unsafe_precondition;

#[cfg(kani)]
use crate::kani;

/// Converts a `u32` to a `char`. See [`char::from_u32`].
#[must_use]
#[inline]
Expand Down Expand Up @@ -298,7 +298,7 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option<char> {
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;

Expand Down
12 changes: 6 additions & 6 deletions library/core/src/char/methods.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,13 @@
use super::*;
use crate::intrinsics::const_eval_select;
#[cfg(kani)]
use crate::kani;
use crate::slice;
use crate::str::from_utf8_unchecked_mut;
use crate::unicode::printable::is_printable;
use crate::unicode::{self, conversions};

#[cfg(kani)]
use crate::kani;

impl char {
/// The lowest valid code point a `char` can have, `'\0'`.
///
Expand Down Expand Up @@ -1857,19 +1856,20 @@ pub const fn encode_utf16_raw(mut code: u32, dst: &mut [u16]) -> &mut [u16] {
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;
use safety::ensures;

use super::*;

#[ensures(|result| c.is_ascii() == (result.is_some() && (result.unwrap() as u8 as char == *c)))]
fn as_ascii_clone(c: &char) -> Option<ascii::Char> {
c.as_ascii()
}

#[kani::proof_for_contract(as_ascii_clone)]
fn check_as_ascii_ascii_char() {
let ascii: char = kani::any_where(|c : &char| c.is_ascii());
let ascii: char = kani::any_where(|c: &char| c.is_ascii());
as_ascii_clone(&ascii);
}

Expand Down
22 changes: 10 additions & 12 deletions library/core/src/ffi/c_str.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,15 +4,13 @@ use crate::cmp::Ordering;
use crate::error::Error;
use crate::ffi::c_char;
use crate::iter::FusedIterator;
#[cfg(kani)]
use crate::kani;
use crate::marker::PhantomData;
use crate::ptr::NonNull;
use crate::slice::memchr;
use crate::{fmt, intrinsics, ops, slice, str};

use crate::ub_checks::Invariant;

#[cfg(kani)]
use crate::kani;
use crate::{fmt, intrinsics, ops, slice, str};

// FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link
// depends on where the item is being documented. however, since this is libcore, we can't
Expand Down Expand Up @@ -224,7 +222,7 @@ impl Invariant for &CStr {
let bytes: &[c_char] = &self.inner;
let len = bytes.len();

!bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0)
!bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len - 1].contains(&0)
}
}

Expand Down Expand Up @@ -859,7 +857,7 @@ impl FusedIterator for Bytes<'_> {}
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;

// Helper function
fn arbitrary_cstr(slice: &[u8]) -> &CStr {
let result = CStr::from_bytes_until_nul(&slice);
Expand All @@ -884,17 +882,17 @@ mod verify {
assert!(c_str.is_safe());
}
}

// pub const fn count_bytes(&self) -> usize
#[kani::proof]
#[kani::unwind(32)]
fn check_count_bytes() {
const MAX_SIZE: usize = 32;
let mut bytes: [u8; MAX_SIZE] = kani::any();

// Non-deterministically generate a length within the valid range [0, MAX_SIZE]
let mut len: usize = kani::any_where(|&x| x < MAX_SIZE);

// If a null byte exists before the generated length
// adjust len to its position
if let Some(pos) = bytes[..len].iter().position(|&x| x == 0) {
Expand All @@ -903,7 +901,7 @@ mod verify {
// If no null byte, insert one at the chosen length
bytes[len] = 0;
}

let c_str = CStr::from_bytes_until_nul(&bytes).unwrap();
// Verify that count_bytes matches the adjusted length
assert_eq!(c_str.count_bytes(), len);
Expand Down Expand Up @@ -941,4 +939,4 @@ mod verify {
assert_eq!(bytes, &slice[..end_idx]);
assert!(c_str.is_safe());
}
}
}
9 changes: 5 additions & 4 deletions library/core/src/intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,12 +65,12 @@
#![allow(missing_docs)]

use safety::requires;
use crate::marker::{DiscriminantKind, Tuple};
use crate::mem::SizedTypeProperties;
use crate::{ptr, ub_checks};

#[cfg(kani)]
use crate::kani;
use crate::marker::{DiscriminantKind, Tuple};
use crate::mem::SizedTypeProperties;
use crate::{ptr, ub_checks};

pub mod mir;
pub mod simd;
Expand Down Expand Up @@ -3757,9 +3757,10 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use core::{cmp, fmt};

use super::*;
use crate::kani;

Expand Down
7 changes: 3 additions & 4 deletions library/core/src/mem/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,10 @@
#![stable(feature = "rust1", since = "1.0.0")]

use crate::alloc::Layout;
use crate::marker::DiscriminantKind;
use crate::{clone, cmp, fmt, hash, intrinsics, ptr};

#[cfg(kani)]
use crate::kani;
use crate::marker::DiscriminantKind;
use crate::{clone, cmp, fmt, hash, intrinsics, ptr};

mod manually_drop;
#[stable(feature = "manually_drop", since = "1.20.0")]
Expand Down Expand Up @@ -1372,7 +1371,7 @@ pub macro offset_of($Container:ty, $($fields:expr)+ $(,)?) {
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;
use crate::kani;
Expand Down
2 changes: 1 addition & 1 deletion library/core/src/num/int_macros.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1301,7 +1301,7 @@ macro_rules! int_impl {
#[cfg_attr(bootstrap, rustc_const_unstable(feature = "unchecked_shifts", issue = "85122"))]
#[inline(always)]
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
#[requires(rhs < <$ActualT>::BITS)]
#[requires(rhs < <$ActualT>::BITS)]
pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
assert_unsafe_precondition!(
check_language_ub,
Expand Down
Loading

0 comments on commit a56634c

Please sign in to comment.