Skip to content

Commit 269448e

Browse files
committed
Squashed 'library/' changes from a2cf636..3e6b1c26cd5
3e6b1c26cd5 Merge commit 'cee9f0879743983a0924f94d37e0abd6d464bb4f' into sync-2024-07-20 496b81c004b Merge commit 'dd0d2657eb2c8466bbd9fa6ea4bf2b094565c680' into sync-2024-07-17 e3a5cb88602 Merge commit 'dd0d2657eb2c8466bbd9fa6ea4bf2b094565c680' into sync-2024-07-17 2f83451ef02 Reapply repository changes to library files 7b3d8ba5d15 Reapply repository changes to library files c0a2240a2e7 Move contracts back to library/contracts 9d2c65282fd Move contracts back to library/contracts 586d10f1860 Merge commit '0cd155fda0d5b0b3ba666cd9df978d380f6c7067' as 'library' 9cab9f2bf44 Merge commit '0cd155fda0d5b0b3ba666cd9df978d380f6c7067' as 'library' 47a29de Delete library folder so we can recreate subtree eea60ef Record library patch and delete library/ af85a10 Move contracts out of library for now fd1c9c2 Add contracts for Layout and Alignment (#33) 5d8ee62 Add permissions needed to modify PR (#34) bbfbb19 Add PR approval check for specific directories (#31) 5f2798e Add a challenge for `linked_list` (#30) 5a7327e Propose a new challenge about pointer arithmetic ops (#23) c7dd281 Add committee application guideline and committee TOML file (#32) df109da Add tracking issue for challenges template (#27) 52bea58 Remove copyright strings (#24) e15993a Fix challenge numbers and move to challenges/ dir (#22) ebb5c7f Add copyright file (#13) df8da5a Add a few more contract and harness examples (#18) 5b70960 Run CI checks on all PRs against to main (#20) a7c6d00 refined core transmutation challenge. (#11) 614eb77 Add simple ensures, requires, safety predicates (#15) 3a164b0 Add Challenge 2: Verify the memory safery of core intrinsics using raw pointers (#14) 8931064 Add Kani usage and verify-std section to verification book (#12) 5a369ec Add initial challenge template (#10) b8464d4 Add Rust tests and Kani workflow (#9) 6f793b3 Update text and book ec8c25c Fix text 4a6eb06 Add disclaimer, and fix links (#5) dc3222b Fix the book script (#8) c9653b7 Add copyright check file (#7) 05dca8f Add contest book (#6) 838f888 Adding std library as a subtree 6efb19b Merge commit '2faab3154fb126423ccf8e56c10577a3cd3f9457' as 'library' 2faab31 Squashed 'library/' content from commit f461edda8cb 104c14e Update README.md (#3) 7c30a94 Add README.md file (#2) f24a233 Create initial commit with the license files git-subtree-dir: library git-subtree-split: 3e6b1c26cd58a676a339261c5e190fa29b903833
1 parent dd0d265 commit 269448e

File tree

13 files changed

+267
-1
lines changed

13 files changed

+267
-1
lines changed

contracts/safety/Cargo.toml

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
[package]
2+
name = "safety"
3+
version = "0.1.0"
4+
edition = "2021"
5+
license = "MIT OR Apache-2.0"
6+
7+
[lib]
8+
proc-macro = true
9+
10+
[dependencies]
11+
proc-macro2 = "1.0"
12+
proc-macro-error = "1.0.4"
13+
quote = "1.0.20"
14+
syn = { version = "2.0.18", features = ["full"] }

contracts/safety/build.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
fn main() {
2+
// We add the configurations here to be checked.
3+
println!("cargo:rustc-check-cfg=cfg(kani_host)");
4+
}

contracts/safety/src/kani.rs

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
use proc_macro::{TokenStream};
2+
use quote::{quote, format_ident};
3+
use syn::{ItemFn, parse_macro_input};
4+
5+
pub(crate) fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
6+
rewrite_attr(attr, item, "requires")
7+
}
8+
9+
pub(crate) fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
10+
rewrite_attr(attr, item, "ensures")
11+
}
12+
13+
fn rewrite_attr(attr: TokenStream, item: TokenStream, name: &str) -> TokenStream {
14+
let args = proc_macro2::TokenStream::from(attr);
15+
let fn_item = parse_macro_input!(item as ItemFn);
16+
let attribute = format_ident!("{}", name);
17+
quote!(
18+
#[kani_core::#attribute(#args)]
19+
#fn_item
20+
).into()
21+
}

contracts/safety/src/lib.rs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
//! Implement a few placeholders for contract attributes until they get implemented upstream.
2+
//! Each tool should implement their own version in a separate module of this crate.
3+
4+
use proc_macro::TokenStream;
5+
use proc_macro_error::proc_macro_error;
6+
7+
#[cfg(kani_host)]
8+
#[path = "kani.rs"]
9+
mod tool;
10+
11+
#[cfg(not(kani_host))]
12+
#[path = "runtime.rs"]
13+
mod tool;
14+
15+
#[proc_macro_error]
16+
#[proc_macro_attribute]
17+
pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
18+
tool::requires(attr, item)
19+
}
20+
21+
#[proc_macro_error]
22+
#[proc_macro_attribute]
23+
pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
24+
tool::ensures(attr, item)
25+
}

contracts/safety/src/runtime.rs

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
use proc_macro::TokenStream;
2+
3+
/// For now, runtime requires is a no-op.
4+
///
5+
/// TODO: At runtime the `requires` should become an assert unsafe precondition.
6+
pub(crate) fn requires(_attr: TokenStream, item: TokenStream) -> TokenStream {
7+
item
8+
}
9+
10+
/// For now, runtime requires is a no-op.
11+
///
12+
/// TODO: At runtime the `ensures` should become an assert as well.
13+
pub(crate) fn ensures(_attr: TokenStream, item: TokenStream) -> TokenStream {
14+
item
15+
}

core/Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,9 @@ name = "corebenches"
2424
path = "benches/lib.rs"
2525
test = true
2626

27+
[dependencies]
28+
safety = {path = "../contracts/safety" }
29+
2730
[dev-dependencies]
2831
rand = { version = "0.8.5", default-features = false }
2932
rand_xorshift = { version = "0.3.0", default-features = false }

core/src/alloc/layout.rs

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,16 @@
44
// collections, resulting in having to optimize down excess IR multiple times.
55
// Your performance intuition is useless. Run perf.
66

7+
use safety::requires;
78
use crate::cmp;
89
use crate::error::Error;
910
use crate::fmt;
1011
use crate::mem;
1112
use crate::ptr::{Alignment, NonNull};
1213

14+
#[cfg(kani)]
15+
use crate::kani;
16+
1317
// While this function is used in one place and its implementation
1418
// could be inlined, the previous attempts to do so made rustc
1519
// slower:
@@ -117,6 +121,7 @@ impl Layout {
117121
#[must_use]
118122
#[inline]
119123
#[rustc_allow_const_fn_unstable(ptr_alignment_type)]
124+
#[requires(Layout::from_size_align(size, align).is_ok())]
120125
pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
121126
// SAFETY: the caller is required to uphold the preconditions.
122127
unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -492,3 +497,21 @@ impl fmt::Display for LayoutError {
492497
f.write_str("invalid parameters to Layout::from_size_align")
493498
}
494499
}
500+
501+
#[cfg(kani)]
502+
#[unstable(feature="kani", issue="none")]
503+
mod verify {
504+
use super::*;
505+
506+
#[kani::proof_for_contract(Layout::from_size_align_unchecked)]
507+
pub fn check_from_size_align_unchecked() {
508+
let s = kani::any::<usize>();
509+
let a = kani::any::<usize>();
510+
511+
unsafe {
512+
let layout = Layout::from_size_align_unchecked(s, a);
513+
assert_eq!(layout.size(), s);
514+
assert_eq!(layout.align(), a);
515+
}
516+
}
517+
}

core/src/intrinsics.rs

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,11 +63,15 @@
6363
)]
6464
#![allow(missing_docs)]
6565

66+
use safety::requires;
6667
use crate::marker::DiscriminantKind;
6768
use crate::marker::Tuple;
6869
use crate::ptr;
6970
use crate::ub_checks;
7071

72+
#[cfg(kani)]
73+
use crate::kani;
74+
7175
pub mod mir;
7276
pub mod simd;
7377

@@ -2708,6 +2712,12 @@ pub const fn is_val_statically_known<T: Copy>(_arg: T) -> bool {
27082712
#[rustc_intrinsic]
27092713
// This has fallback `const fn` MIR, so shouldn't need stability, see #122652
27102714
#[rustc_const_unstable(feature = "const_typed_swap", issue = "none")]
2715+
#[cfg_attr(kani, kani::modifies(x))]
2716+
#[cfg_attr(kani, kani::modifies(y))]
2717+
#[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
2718+
#[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
2719+
#[requires(x.addr() != y.addr() || core::mem::size_of::<T>() == 0)]
2720+
#[requires((x.addr() >= y.addr() + core::mem::size_of::<T>()) || (y.addr() >= x.addr() + core::mem::size_of::<T>()))]
27112721
pub const unsafe fn typed_swap<T>(x: *mut T, y: *mut T) {
27122722
// SAFETY: The caller provided single non-overlapping items behind
27132723
// pointers, so swapping them with `count: 1` is fine.
@@ -3154,3 +3164,37 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
31543164

31553165
const_eval_select((ptr, align), compiletime, runtime);
31563166
}
3167+
3168+
#[cfg(kani)]
3169+
#[unstable(feature="kani", issue="none")]
3170+
mod verify {
3171+
use core::{cmp, fmt};
3172+
use super::*;
3173+
use crate::kani;
3174+
3175+
#[kani::proof_for_contract(typed_swap)]
3176+
pub fn check_typed_swap_u8() {
3177+
check_swap::<u8>()
3178+
}
3179+
3180+
#[kani::proof_for_contract(typed_swap)]
3181+
pub fn check_typed_swap_char() {
3182+
check_swap::<char>()
3183+
}
3184+
3185+
#[kani::proof_for_contract(typed_swap)]
3186+
pub fn check_typed_swap_non_zero() {
3187+
check_swap::<core::num::NonZeroI32>()
3188+
}
3189+
3190+
pub fn check_swap<T: kani::Arbitrary + Copy + cmp::PartialEq + fmt::Debug>() {
3191+
let mut x = kani::any::<T>();
3192+
let old_x = x;
3193+
let mut y = kani::any::<T>();
3194+
let old_y = y;
3195+
3196+
unsafe { typed_swap(&mut x, &mut y) };
3197+
assert_eq!(y, old_x);
3198+
assert_eq!(x, old_y);
3199+
}
3200+
}

core/src/lib.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -424,6 +424,9 @@ mod unit;
424424
#[stable(feature = "core_primitive", since = "1.43.0")]
425425
pub mod primitive;
426426

427+
#[cfg(kani)]
428+
kani_core::kani_lib!(core);
429+
427430
// Pull in the `core_arch` crate directly into core. The contents of
428431
// `core_arch` are in a different repository: rust-lang/stdarch.
429432
//

core/src/mem/mod.rs

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,9 @@ use crate::intrinsics;
1313
use crate::marker::DiscriminantKind;
1414
use crate::ptr;
1515

16+
#[cfg(kani)]
17+
use crate::kani;
18+
1619
mod manually_drop;
1720
#[stable(feature = "manually_drop", since = "1.20.0")]
1821
pub use manually_drop::ManuallyDrop;
@@ -725,6 +728,8 @@ pub unsafe fn uninitialized<T>() -> T {
725728
#[stable(feature = "rust1", since = "1.0.0")]
726729
#[rustc_const_unstable(feature = "const_swap", issue = "83163")]
727730
#[rustc_diagnostic_item = "mem_swap"]
731+
#[cfg_attr(kani, crate::kani::modifies(x))]
732+
#[cfg_attr(kani, crate::kani::modifies(y))]
728733
pub const fn swap<T>(x: &mut T, y: &mut T) {
729734
// SAFETY: `&mut` guarantees these are typed readable and writable
730735
// as well as non-overlapping.
@@ -1359,3 +1364,38 @@ pub macro offset_of($Container:ty, $($fields:expr)+ $(,)?) {
13591364
// The `{}` is for better error messages
13601365
{builtin # offset_of($Container, $($fields)+)}
13611366
}
1367+
1368+
#[cfg(kani)]
1369+
#[unstable(feature="kani", issue="none")]
1370+
mod verify {
1371+
use super::*;
1372+
use crate::kani;
1373+
1374+
/// Use this type to ensure that mem swap does not drop the value.
1375+
#[derive(kani::Arbitrary)]
1376+
struct CannotDrop<T: kani::Arbitrary> {
1377+
inner: T,
1378+
}
1379+
1380+
impl<T: kani::Arbitrary> Drop for CannotDrop<T> {
1381+
fn drop(&mut self) {
1382+
unreachable!("Cannot drop")
1383+
}
1384+
}
1385+
1386+
#[kani::proof_for_contract(swap)]
1387+
pub fn check_swap_primitive() {
1388+
let mut x: u8 = kani::any();
1389+
let mut y: u8 = kani::any();
1390+
swap(&mut x, &mut y)
1391+
}
1392+
1393+
#[kani::proof_for_contract(swap)]
1394+
pub fn check_swap_adt_no_drop() {
1395+
let mut x: CannotDrop<char> = kani::any();
1396+
let mut y: CannotDrop<char> = kani::any();
1397+
swap(&mut x, &mut y);
1398+
forget(x);
1399+
forget(y);
1400+
}
1401+
}

0 commit comments

Comments
 (0)