Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Run format check in our CI and fix repo format #205

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 2 additions & 4 deletions .github/workflows/rustc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ defaults:
shell: bash

jobs:
build:
upstream_test:
runs-on: ${{ matrix.os }}
strategy:
matrix:
Expand All @@ -27,8 +27,6 @@ jobs:
steps:
- name: Checkout Library
uses: actions/checkout@v4
with:
path: head

- name: Run rustc script
run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head
run: ./scripts/check_rustc.sh
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