diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 9d445fc7dc10c..ca25c36bf449a 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -19,6 +19,7 @@ - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md) - [6: Safety of `NonNull`](./challenges/0006-nonnull.md) + - [7: Safety of Methods for Atomic Types and `ReentrantLock`](./challenges/0007-atomic-types.md) - [8: Contracts for SmallSort](./challenges/0008-smallsort.md) - [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) - [10: Memory safety of String](./challenges/0010-string.md) diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md new file mode 100644 index 0000000000000..69bff582f7751 --- /dev/null +++ b/doc/src/challenges/0007-atomic-types.md @@ -0,0 +1,128 @@ +# Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics + +- **Status:** Open +- **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83) +- **Start date:** *2024-10-30* +- **End date:** *2024-12-10* + +------------------- + +## Goal + +[`core::sync::atomic`](https://doc.rust-lang.org/std/sync/atomic/index.html) provides methods that operate on atomic types. +For example, `AtomicBool::store(&self, val: bool, order: Ordering)` stores `val` in the atomic boolean referenced by `self` according to the specified [atomic memory ordering](https://doc.rust-lang.org/std/sync/atomic/enum.Ordering.html). + +The goal of this challenge is to verify that these methods are safe.[^1] + +### Success Criteria + +#### Part 1: Unsafe Methods + +First, verify that the unsafe `from_ptr` methods are safe, given that their safety preconditions are met. + +Write safety contracts for each of the `from_ptr` methods: + +- `AtomicBool::from_ptr` +- `AtomicPtr::from_ptr` +- `AtomicI8::from_ptr` +- `AtomicU8::from_ptr` +- `AtomicI16::from_ptr` +- `AtomicU16::from_ptr` +- `AtomicI32::from_ptr` +- `AtomicU32::from_ptr` +- `AtomicI64::from_ptr` +- `AtomicU64::from_ptr` +- `AtomicI128::from_ptr` +- `AtomicU128::from_ptr` + +Specifically, encode the conditions about `ptr`'s alignment and validity (marked `#Safety` in the methods' documentation) as preconditions. +Then, verify that the methods are safe for all possible values for the type that `ptr` points to, given that `ptr` satisfies those preconditions. + +For example, `AtomicI8::from_ptr` is defined as: +```rust +/// `ptr` must be [valid] ... (comment continues; omitted for brevity) +pub const unsafe fn from_ptr<'a>(ptr: *mut i8) -> &'a AtomicI8 { + // SAFETY: guaranteed by the caller + unsafe { &*ptr.cast() } +} +``` + +To verify this method, first encode the safety comments (e.g., about pointer validity) as preconditions, then verify the absence of undefined behavior for all possible `i8` values. + +For the `AtomicPtr` case only, we do not require that you verify safety for all possible types. +Concretely, below is the type signature for `AtomicPtr::from_ptr`: + +```rust +pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr +``` + +The type pointed to is a `*mut T`. +Verify that for any arbitrary value for this `*mut T` (i.e., any arbitrary memory address), the method is safe. +However, you need not verify the method for all possible instantiations of `T`. +It suffices to verify this method for `T` of byte sizes 0, 1, 2, 4, and at least one non-power of two. + +#### Part 2: Safe Abstractions + +The atomic types expose safe abstractions for atomic operations. +In this part, you will work toward verifying that these abstractions are indeed safe by writing and verifying safety contracts for the unsafe code in their bodies. + +For example, `AtomicBool::store` is the (public) safe method that atomically updates the boolean's value. +This method invokes the unsafe function `atomic_store`, which in turn calls `intrinsics::atomic_store_relaxed`, `intrinsics::atomic_store_release`, or `intrinsics::atomic_store_seqcst`, depending on the provided ordering. + +Write and verify safety contracts for the unsafe functions: + +- `atomic_store` +- `atomic_load` +- `atomic_swap` +- `atomic_add` +- `atomic_sub` +- `atomic_compare_exchange` +- `atomic_compare_exchange_weak` +- `atomic_and` +- `atomic_nand` +- `atomic_or` +- `atomic_xor` +- `atomic_max` +- `atomic_umax` +- `atomic_umin` + +Then, for each of the safe abstractions that invoke the unsafe functions listed above, write contracts that ensure that they are not invoked with `order`s that would cause panics. + +For example, `atomic_store` panics if invoked with `Acquire` or `AcqRel` ordering. +In this case, you would write contracts on the safe `store` methods that enforce that they are not called with either of those `order`s. + +#### Part 3: Atomic Intrinsics + +Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in `core::intrinsics`): + +| Operations | Functions | +|-----------------------|-------------| +| Store | `atomic_store_relaxed`, `atomic_store_release`, `atomic_store_seqcst` | +| Load | `atomic_load_relaxed`, `atomic_load_acquire`, `atomic_load_seqcst` | +| Swap | `atomic_xchg_relaxed`, `atomic_xchg_acquire`, `atomic_xchg_release`, `atomic_xchg_acqrel`, `atomic_xchg_seqcst` | +| Add | `atomic_xadd_relaxed`, `atomic_xadd_acquire`, `atomic_xadd_release`, `atomic_xadd_acqrel`, `atomic_xadd_seqcst` | +| Sub | `atomic_xsub_relaxed`, `atomic_xsub_acquire`, `atomic_xsub_release`, `atomic_xsub_acqrel`, `atomic_xsub_seqcst` | +| Compare Exchange | `atomic_cxchg_relaxed_relaxed`, `atomic_cxchg_relaxed_acquire`, `atomic_cxchg_relaxed_seqcst`, `atomic_cxchg_acquire_relaxed`, `atomic_cxchg_acquire_acquire`, `atomic_cxchg_acquire_seqcst`, `atomic_cxchg_release_relaxed`, `atomic_cxchg_release_acquire`, `atomic_cxchg_release_seqcst`, `atomic_cxchg_acqrel_relaxed`, `atomic_cxchg_acqrel_acquire`, `atomic_cxchg_acqrel_seqcst`, `atomic_cxchg_seqcst_relaxed`, `atomic_cxchg_seqcst_acquire`, `atomic_cxchg_seqcst_seqcst` | +| Compare Exchange Weak | `atomic_cxchgweak_relaxed_relaxed`, `atomic_cxchgweak_relaxed_acquire`, `atomic_cxchgweak_relaxed_seqcst`, `atomic_cxchgweak_acquire_relaxed`, `atomic_cxchgweak_acquire_acquire`, `atomic_cxchgweak_acquire_seqcst`, `atomic_cxchgweak_release_relaxed`, `atomic_cxchgweak_release_acquire`, `atomic_cxchgweak_release_seqcst`, `atomic_cxchgweak_acqrel_relaxed`, `atomic_cxchgweak_acqrel_acquire`, `atomic_cxchgweak_acqrel_seqcst`, `atomic_cxchgweak_seqcst_relaxed`, `atomic_cxchgweak_seqcst_acquire`, `atomic_cxchgweak_seqcst_seqcst` | +| And | `atomic_and_relaxed`, `atomic_and_acquire`, `atomic_and_release`, `atomic_and_acqrel`, `atomic_and_seqcst` | +| Nand | `atomic_nand_relaxed`, `atomic_nand_acquire`, `atomic_nand_release`, `atomic_nand_acqrel`, `atomic_nand_seqcst` | +| Or | `atomic_or_seqcst`, `atomic_or_acquire`, `atomic_or_release`, `atomic_or_acqrel`, `atomic_or_relaxed` | +| Xor | `atomic_xor_seqcst`, `atomic_xor_acquire`, `atomic_xor_release`, `atomic_xor_acqrel`, `atomic_xor_relaxed` | +| Max | `atomic_max_relaxed`, `atomic_max_acquire`, `atomic_max_release`, `atomic_max_acqrel`, `atomic_max_seqcst` | +| Min | `atomic_min_relaxed`, `atomic_min_acquire`, `atomic_min_release`, `atomic_min_acqrel`, `atomic_min_seqcst` | +| Umax | `atomic_umax_relaxed`, `atomic_umax_acquire`, `atomic_umax_release`, `atomic_umax_acqrel`, `atomic_umax_seqcst` | +| Umin | `atomic_umin_relaxed`, `atomic_umin_acquire`, `atomic_umin_release`, `atomic_umin_acqrel`, `atomic_umin_seqcst` | + +## List of UBs + +In addition to any safety properties mentioned in the API documentation, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Data races. +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Invoking undefined behavior via compiler intrinsics. +* Producing an invalid value. + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) in addition to the ones listed above. + +[^1]: Throughout this challenge, when we say "safe", it is identical to saying "does not exhibit undefined behavior". \ No newline at end of file diff --git a/doc/src/general-rules.md b/doc/src/general-rules.md index 4f419decbdf6b..79c940230dea0 100644 --- a/doc/src/general-rules.md +++ b/doc/src/general-rules.md @@ -5,7 +5,9 @@ **Verification Target:** [Our repository](https://github.com/model-checking/verify-rust-std) is a fork of the original Rust repository, and we kept a copy of the Rust standard library inside the `library/` folder that shall be used as the verification target for all our challenges. We will periodically update the `library/` folder to track newer versions of the [official Rust standard library](https://github.com/rust-lang/rust/). -NOTE: This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation. + +**NOTE:** This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation. + **Challenges:** Each individual verification effort will have a tracking issue where contributors can add comments and ask clarification questions. You can find the list of [open challenges here](https://github.com/model-checking/verify-rust-std/labels/Challenge). diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 9cfd198e9bc8e..d1066b8d9076d 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -59,7 +59,8 @@ Create a local copy of the [model-checking fork](https://github.com/model-checki `assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `modifies`, `requires` and `ensures`) directly. -For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. This is just for the purpose of getting started, so you can insert in any existing file in the core library if you have other preferences. +For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. +This is just for the purpose of getting started, so you can insert it in a different (existing) file in the core library instead. ``` rust #[cfg(kani)] @@ -84,22 +85,24 @@ pub mod verify { } ``` -### Step 2 - Run the Kani verify-std subcommand +### Step 2 - Run the Kani script on the std library -To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started. -Run the following command in your local terminal (Replace "/path/to/library" and "/path/to/target" with your local paths) from the verify repository root: +To aid the Rust Standard Library verification effort, Kani provides a script out of the box to help you get started. +Run the following command in your local terminal from the verify repository root: ``` -kani verify-std -Z unstable-options "/path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z mem-predicates +./scripts/run-kani.sh --path . ``` -The command `kani verify-std` is a sub-command of the `kani`. This specific sub-command is used to verify the Rust Standard Library with the following arguments. +To pass kani arguments such as `--harness`, you can run the script with `--kani-args` and continue passing in all the necessary arguments: -- `"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script. For example, `./library` or `/home/ubuntu/verify-rust-std/library` -- `--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files. For example, `/tmp` or `/tmp/verify-std` +``` +./scripts/run-kani.sh --path . --kani-args --harness alloc::layout::verify::check_array_i32 --output-format=terse +``` + +The script `run-kani` installs the right version of Kani for you, builds it and then finally runs the verify-std sub-command of the `kani` with some default flags. -Apart from these, you can use your regular `kani-args` such as `-Z function-contracts`, `-Z stubbing` and `-Z mem-predicates` depending on your verification needs. If you run into a Kani error that says `Use of unstable feature`, add the corresponding feature with `-Z` to the command line. -For more details on Kani's features, refer to [the features section in the Kani Book](https://model-checking.github.io/kani/reference/attributes.html) +**NOTE:** This script may crash due to linking issues. If the script fails with an error message related to linking, link the new CBMC version, delete the `./kani_build` directory and re-run. ### Step 3 - Check verification result @@ -122,7 +125,7 @@ You can specify a specific harness to be verified using the `--harness` flag. For example, in your local copy of the verify repo, run the following command. ``` -kani verify-std --harness harness_introduction -Z unstable-options "./library" --target-dir "/tmp" -Z function-contracts -Z mem-predicates +./scripts/run-kani.sh --kani-args --harness harness_introduction ``` This gives you the verification result for just `harness_introduction` from the aforementioned blob. @@ -144,13 +147,16 @@ Verification Time: 0.01885804s Complete - 1 successfully verified harnesses, 0 failures, 1 total. ``` -Now you can write proof harnesses to verify specific functions in the library. -The current convention is to keep proofs in the same module file of the verification target. -To run Kani for an individual proof, use `--harness [harness_function_name]`. -Note that Kani will batch run all proofs in the library folder if you do not supply the `--harness` flag. -If Kani returns the error `no harnesses matched the harness filter`, you can give the full name of the harness. -For example, to run the proof harness named `check_new` in `library/core/src/ptr/unique.rs`, use -`--harness ptr::unique::verify::check_new`. To run all proofs in `unique.rs`, use `--harness ptr::unique::verify`. +Now you can write proof harnesses to verify specific functions in the library. +The current convention is to keep proofs in the same module file of the verification target. + +To run Kani for an individual proof, use `--harness [harness_function_name]`. +Note that Kani will batch run all proofs in the library folder if you do not supply the `--harness` flag. + +If Kani returns the error `no harnesses matched the harness filter`, you can give the full name of the harness. +For example, to run the proof harness named `check_new` in `library/core/src/ptr/unique.rs`, use +`--harness ptr::unique::verify::check_new`. To run all proofs in `unique.rs`, use `--harness ptr::unique::verify`. + To find the full name of a harness, check the Kani output and find the line starting with `Checking harness [harness full name]`. ## More details diff --git a/library/contracts/safety/src/kani.rs b/library/contracts/safety/src/kani.rs index a8b4ab360dc8e..0f36ed2d68530 100644 --- a/library/contracts/safety/src/kani.rs +++ b/library/contracts/safety/src/kani.rs @@ -1,6 +1,6 @@ -use proc_macro::{TokenStream}; -use quote::{quote, format_ident}; -use syn::{ItemFn, parse_macro_input}; +use proc_macro::TokenStream; +use quote::{format_ident, quote}; +use syn::{parse_macro_input, ItemFn, Stmt}; pub(crate) fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { rewrite_attr(attr, item, "requires") @@ -10,6 +10,21 @@ pub(crate) fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { rewrite_attr(attr, item, "ensures") } +pub(crate) fn loop_invariant(attr: TokenStream, stmt: TokenStream) -> TokenStream { + rewrite_stmt_attr(attr, stmt, "loop_invariant") +} + +fn rewrite_stmt_attr(attr: TokenStream, stmt_stream: TokenStream, name: &str) -> TokenStream { + let args = proc_macro2::TokenStream::from(attr); + let stmt = parse_macro_input!(stmt_stream as Stmt); + let attribute = format_ident!("{}", name); + quote!( + #[kani_core::#attribute(#args)] + #stmt + ) + .into() +} + fn rewrite_attr(attr: TokenStream, item: TokenStream, name: &str) -> TokenStream { let args = proc_macro2::TokenStream::from(attr); let fn_item = parse_macro_input!(item as ItemFn); @@ -17,5 +32,6 @@ fn rewrite_attr(attr: TokenStream, item: TokenStream, name: &str) -> TokenStream quote!( #[kani_core::#attribute(#args)] #fn_item - ).into() + ) + .into() } diff --git a/library/contracts/safety/src/lib.rs b/library/contracts/safety/src/lib.rs index 9fe852a622de3..eba2e91b44e85 100644 --- a/library/contracts/safety/src/lib.rs +++ b/library/contracts/safety/src/lib.rs @@ -3,6 +3,11 @@ use proc_macro::TokenStream; use proc_macro_error::proc_macro_error; +use quote::{format_ident, quote, quote_spanned}; +use syn::{ + parse_macro_input, parse_quote, spanned::Spanned, Data, DataEnum, DeriveInput, Fields, + GenericParam, Generics, Ident, Index, ItemStruct, +}; #[cfg(kani_host)] #[path = "kani.rs"] @@ -12,6 +17,135 @@ mod tool; #[path = "runtime.rs"] mod tool; +/// Expands the `#[invariant(...)]` attribute macro. +/// The macro expands to an implementation of the `is_safe` method for the `Invariant` trait. +/// This attribute is only supported for structs. +/// +/// # Example +/// +/// ```ignore +/// #[invariant(self.width == self.height)] +/// struct Square { +/// width: u32, +/// height: u32, +/// } +/// ``` +/// +/// expands to: +/// ```ignore +/// impl core::ub_checks::Invariant for Square { +/// fn is_safe(&self) -> bool { +/// self.width == self.height +/// } +/// } +/// ``` +/// For more information on the Invariant trait, see its documentation in core::ub_checks. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn invariant(attr: TokenStream, item: TokenStream) -> TokenStream { + let safe_body = proc_macro2::TokenStream::from(attr); + let item = parse_macro_input!(item as ItemStruct); + let item_name = &item.ident; + let (impl_generics, ty_generics, where_clause) = item.generics.split_for_impl(); + + let expanded = quote! { + #item + #[unstable(feature="invariant", issue="none")] + impl #impl_generics core::ub_checks::Invariant for #item_name #ty_generics #where_clause { + fn is_safe(&self) -> bool { + #safe_body + } + } + }; + + proc_macro::TokenStream::from(expanded) +} + +/// Expands the derive macro for the Invariant trait. +/// The macro expands to an implementation of the `is_safe` method for the `Invariant` trait. +/// This macro is only supported for structs and enums. +/// +/// # Example +/// +/// ```ignore +/// #[derive(Invariant)] +/// struct Square { +/// width: u32, +/// height: u32, +/// } +/// ``` +/// +/// expands to: +/// ```ignore +/// impl core::ub_checks::Invariant for Square { +/// fn is_safe(&self) -> bool { +/// self.width.is_safe() && self.height.is_safe() +/// } +/// } +/// ``` +/// For enums, the body of `is_safe` matches on the variant and calls `is_safe` on its fields, +/// # Example +/// +/// ```ignore +/// #[derive(Invariant)] +/// enum MyEnum { +/// OptionOne(u32, u32), +/// OptionTwo(Square), +/// OptionThree +/// } +/// ``` +/// +/// expands to: +/// ```ignore +/// impl core::ub_checks::Invariant for MyEnum { +/// fn is_safe(&self) -> bool { +/// match self { +/// MyEnum::OptionOne(field1, field2) => field1.is_safe() && field2.is_safe(), +/// MyEnum::OptionTwo(field1) => field1.is_safe(), +/// MyEnum::OptionThree => true, +/// } +/// } +/// } +/// ``` +/// For more information on the Invariant trait, see its documentation in core::ub_checks. +#[proc_macro_error] +#[proc_macro_derive(Invariant)] +pub fn derive_invariant(item: TokenStream) -> TokenStream { + let derive_item = parse_macro_input!(item as DeriveInput); + let item_name = &derive_item.ident; + let safe_body = match derive_item.data { + Data::Struct(struct_data) => { + safe_body(&struct_data.fields) + }, + Data::Enum(enum_data) => { + let variant_checks = variant_checks(enum_data, item_name); + + quote! { + match self { + #(#variant_checks),* + } + } + }, + Data::Union(..) => unimplemented!("Attempted to derive Invariant on a union; Invariant can only be derived for structs and enums."), + }; + + // Add a bound `T: Invariant` to every type parameter T. + let generics = add_trait_bound_invariant(derive_item.generics); + // Generate an expression to sum up the heap size of each field. + let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); + + let expanded = quote! { + // The generated implementation. + #[unstable(feature="invariant", issue="none")] + impl #impl_generics core::ub_checks::Invariant for #item_name #ty_generics #where_clause { + fn is_safe(&self) -> bool { + #safe_body + } + } + }; + proc_macro::TokenStream::from(expanded) +} + #[proc_macro_error] #[proc_macro_attribute] pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { @@ -23,3 +157,102 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { tool::ensures(attr, item) } + +#[proc_macro_error] +#[proc_macro_attribute] +pub fn loop_invariant(attr: TokenStream, stmt_stream: TokenStream) -> TokenStream { + tool::loop_invariant(attr, stmt_stream) +} + +/// Add a bound `T: Invariant` to every type parameter T. +fn add_trait_bound_invariant(mut generics: Generics) -> Generics { + generics.params.iter_mut().for_each(|param| { + if let GenericParam::Type(type_param) = param { + type_param + .bounds + .push(parse_quote!(core::ub_checks::Invariant)); + } + }); + generics +} + +/// Generate safety checks for each variant of an enum +fn variant_checks(enum_data: DataEnum, item_name: &Ident) -> Vec { + enum_data + .variants + .iter() + .map(|variant| { + let variant_name = &variant.ident; + match &variant.fields { + Fields::Unnamed(fields) => { + let field_names: Vec<_> = fields + .unnamed + .iter() + .enumerate() + .map(|(i, _)| format_ident!("field{}", i + 1)) + .collect(); + + let field_checks: Vec<_> = field_names + .iter() + .map(|field_name| { + quote! { #field_name.is_safe() } + }) + .collect(); + + quote! { + #item_name::#variant_name(#(#field_names),*) => #(#field_checks)&&* + } + } + Fields::Unit => { + quote! { + #item_name::#variant_name => true + } + } + Fields::Named(_) => unreachable!("Enums do not have named fields"), + } + }) + .collect() +} + +/// Generate the body for the `is_safe` method. +/// For each field of the type, enforce that it is safe. +fn safe_body(fields: &Fields) -> proc_macro2::TokenStream { + match fields { + Fields::Named(ref fields) => { + let field_safe_calls: Vec = fields + .named + .iter() + .map(|field| { + let name = &field.ident; + quote_spanned! {field.span()=> + self.#name.is_safe() + } + }) + .collect(); + if !field_safe_calls.is_empty() { + quote! { #( #field_safe_calls )&&* } + } else { + quote! { true } + } + } + Fields::Unnamed(ref fields) => { + let field_safe_calls: Vec = fields + .unnamed + .iter() + .enumerate() + .map(|(idx, field)| { + let field_idx = Index::from(idx); + quote_spanned! {field.span()=> + self.#field_idx.is_safe() + } + }) + .collect(); + if !field_safe_calls.is_empty() { + quote! { #( #field_safe_calls )&&* } + } else { + quote! { true } + } + } + Fields::Unit => quote! { true }, + } +} diff --git a/library/contracts/safety/src/runtime.rs b/library/contracts/safety/src/runtime.rs index 78e8b1dc354d2..3d1cb1d96c90e 100644 --- a/library/contracts/safety/src/runtime.rs +++ b/library/contracts/safety/src/runtime.rs @@ -7,9 +7,16 @@ pub(crate) fn requires(_attr: TokenStream, item: TokenStream) -> TokenStream { item } -/// For now, runtime requires is a no-op. +/// For now, runtime ensures is a no-op. /// /// TODO: At runtime the `ensures` should become an assert as well. pub(crate) fn ensures(_attr: TokenStream, item: TokenStream) -> TokenStream { item } + +/// For now, runtime loop_invariant is a no-op. +/// +/// TODO: At runtime the `loop_invariant` should become an assert as well. +pub(crate) fn loop_invariant(_attr: TokenStream, stmt_stream: TokenStream) -> TokenStream { + stmt_stream +} diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index 666c5be7c29b5..44b909a0adb50 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -4,7 +4,7 @@ // collections, resulting in having to optimize down excess IR multiple times. // Your performance intuition is useless. Run perf. -use safety::{ensures, requires}; +use safety::{ensures, Invariant, requires}; use crate::error::Error; use crate::ptr::{Alignment, NonNull}; use crate::{assert_unsafe_precondition, cmp, fmt, mem}; @@ -12,6 +12,10 @@ use crate::{assert_unsafe_precondition, cmp, fmt, mem}; #[cfg(kani)] use crate::kani; +// Used only for contract verification. +#[allow(unused_imports)] +use crate::ub_checks::Invariant; + // While this function is used in one place and its implementation // could be inlined, the previous attempts to do so made rustc // slower: @@ -39,6 +43,7 @@ const fn size_align() -> (usize, usize) { #[stable(feature = "alloc_layout", since = "1.28.0")] #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] #[lang = "alloc_layout"] +#[derive(Invariant)] pub struct Layout { // size of the requested block of memory, measured in bytes. size: usize, @@ -132,6 +137,7 @@ impl Layout { #[inline] #[rustc_allow_const_fn_unstable(ptr_alignment_type)] #[requires(Layout::from_size_align(size, align).is_ok())] + #[ensures(|result| result.is_safe())] #[ensures(|result| result.size() == size)] #[ensures(|result| result.align() == align)] pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self { diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index fd1b4f9a45d54..af6129480ff73 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -1,4 +1,4 @@ -use safety::{ensures, requires}; +use safety::{ensures, invariant, requires}; use crate::num::NonZero; use crate::ub_checks::assert_unsafe_precondition; use crate::{cmp, fmt, hash, mem, num}; @@ -6,6 +6,9 @@ use crate::{cmp, fmt, hash, mem, num}; #[cfg(kani)] use crate::kani; +#[cfg(kani)] +use crate::ub_checks::Invariant; + /// A type storing a `usize` which is a power of two, and thus /// represents a possible alignment in the Rust abstract machine. /// @@ -14,6 +17,7 @@ use crate::kani; #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[derive(Copy, Clone, PartialEq, Eq)] #[repr(transparent)] +#[invariant(self.as_usize().is_power_of_two())] pub struct Alignment(AlignmentEnum); // Alignment is `repr(usize)`, but via extra steps. @@ -256,6 +260,7 @@ impl Default for Alignment { #[cfg(target_pointer_width = "16")] #[derive(Copy, Clone, PartialEq, Eq)] #[repr(u16)] +#[cfg_attr(kani, derive(kani::Arbitrary))] enum AlignmentEnum { _Align1Shl0 = 1 << 0, _Align1Shl1 = 1 << 1, @@ -278,6 +283,7 @@ enum AlignmentEnum { #[cfg(target_pointer_width = "32")] #[derive(Copy, Clone, PartialEq, Eq)] #[repr(u32)] +#[cfg_attr(kani, derive(kani::Arbitrary))] enum AlignmentEnum { _Align1Shl0 = 1 << 0, _Align1Shl1 = 1 << 1, @@ -316,6 +322,7 @@ enum AlignmentEnum { #[cfg(target_pointer_width = "64")] #[derive(Copy, Clone, PartialEq, Eq)] #[repr(u64)] +#[cfg_attr(kani, derive(kani::Arbitrary))] enum AlignmentEnum { _Align1Shl0 = 1 << 0, _Align1Shl1 = 1 << 1, @@ -390,8 +397,9 @@ mod verify { impl kani::Arbitrary for Alignment { fn any() -> Self { - let align = kani::any_where(|a: &usize| a.is_power_of_two()); - unsafe { mem::transmute::(align) } + let obj = Self { 0: kani::any() }; + kani::assume(obj.is_safe()); + obj } } diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index f5713fafb7c72..3bd47bbdc85ab 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -209,3 +209,58 @@ mod predicates { mod predicates { pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned}; } + +/// This trait should be used to specify and check type safety invariants for a +/// type. For type invariants, we refer to the definitions in the Rust's Unsafe +/// Code Guidelines Reference: +/// +/// +/// In summary, the reference distinguishes two kinds of type invariants: +/// - *Validity invariant*: An invariant that all data must uphold any time +/// it's accessed or copied in a typed manner. This invariant is exploited by +/// the compiler to perform optimizations. +/// - *Safety invariant*: An invariant that safe code may assume all data to +/// uphold. This invariant can be temporarily violated by unsafe code, but +/// must always be upheld when interfacing with unknown safe code. +/// +/// Therefore, validity invariants must be upheld at all times, while safety +/// invariants only need to be upheld at the boundaries to safe code. +pub trait Invariant { + /// Specify the type's safety invariants + fn is_safe(&self) -> bool; +} + +/// Any value is considered safe for the type +macro_rules! trivial_invariant { + ( $type: ty ) => { + impl Invariant for $type { + #[inline(always)] + fn is_safe(&self) -> bool { + true + } + } + }; +} + +trivial_invariant!(u8); +trivial_invariant!(u16); +trivial_invariant!(u32); +trivial_invariant!(u64); +trivial_invariant!(u128); +trivial_invariant!(usize); + +trivial_invariant!(i8); +trivial_invariant!(i16); +trivial_invariant!(i32); +trivial_invariant!(i64); +trivial_invariant!(i128); +trivial_invariant!(isize); + +trivial_invariant!(()); +trivial_invariant!(bool); +trivial_invariant!(char); + +trivial_invariant!(f16); +trivial_invariant!(f32); +trivial_invariant!(f64); +trivial_invariant!(f128); diff --git a/library/core/src/unicode/mod.rs b/library/core/src/unicode/mod.rs index 6066aa9921607..5ee17570bbc42 100644 --- a/library/core/src/unicode/mod.rs +++ b/library/core/src/unicode/mod.rs @@ -31,3 +31,21 @@ mod unicode_data; /// [Unicode 11.0 or later, Section 3.1 Versions of the Unicode Standard](https://www.unicode.org/versions/Unicode11.0.0/ch03.pdf#page=4). #[stable(feature = "unicode_version", since = "1.45.0")] pub const UNICODE_VERSION: (u8, u8, u8) = unicode_data::UNICODE_VERSION; + +#[cfg(kani)] +mod verify { + use super::conversions::{to_upper, to_lower}; + use crate::kani; + + /// Checks that `to_upper` does not trigger UB or panics for all valid characters. + #[kani::proof] + fn check_to_upper_safety() { + let _ = to_upper(kani::any()); + } + + /// Checks that `to_lower` does not trigger UB or panics for all valid characters. + #[kani::proof] + fn check_to_lower_safety() { + let _ = to_lower(kani::any()); + } +} diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml index 59b19da6a5958..5c0b4c857b6b0 100644 --- a/tool_config/kani-version.toml +++ b/tool_config/kani-version.toml @@ -1,5 +1,5 @@ # This version should be updated whenever there is a change that makes this version of kani -# incomaptible with the verify-std repo. +# incompatible with the verify-std repo. [kani] commit = "5f8f513d297827cfdce4c48065e51973ba563068"