From 614eb77f86d158da5dcbe7f63c2d80dbea7824aa Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Jun 2024 20:48:17 -0700 Subject: [PATCH] Add simple ensures, requires, safety predicates (#15) I also added one proof-of-concept harness to ensure Kani can verify it. --- .github/workflows/kani.yml | 13 ++++++- .github/workflows/rustc.yml | 3 ++ .gitignore | 1 + library/contracts/safety/Cargo.toml | 17 +++++++++ library/contracts/safety/build.rs | 4 +++ library/contracts/safety/src/kani.rs | 21 +++++++++++ library/contracts/safety/src/lib.rs | 25 +++++++++++++ library/contracts/safety/src/runtime.rs | 15 ++++++++ library/core/Cargo.toml | 3 ++ library/core/src/lib.rs | 3 ++ library/core/src/ptr/mod.rs | 21 +++++++++++ library/core/src/ub_checks.rs | 48 +++++++++++++++++++++++++ 12 files changed, 173 insertions(+), 1 deletion(-) create mode 100644 library/contracts/safety/Cargo.toml create mode 100644 library/contracts/safety/build.rs create mode 100644 library/contracts/safety/src/kani.rs create mode 100644 library/contracts/safety/src/lib.rs create mode 100644 library/contracts/safety/src/runtime.rs diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 03365bd9cdbf1..2b950b3e097b8 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -26,6 +26,11 @@ jobs: matrix: # Kani does not support windows. os: [ubuntu-latest, macos-latest] + include: + - os: ubuntu-latest + base: ubuntu + - os: macos-latest + base: macos steps: - name: Checkout Library uses: actions/checkout@v4 @@ -41,6 +46,11 @@ jobs: path: kani ref: features/verify-rust-std + - name: Setup Dependencies + working-directory: kani + run: | + ./scripts/setup/${{ matrix.base }}/install_deps.sh + - name: Build `Kani` working-directory: kani run: | @@ -52,5 +62,6 @@ jobs: env: RUST_BACKTRACE: 1 run: | - kani verify-std -Z unstable-options ./library --target-dir "target" + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -Z mem-predicates -Z ptr-to-ref-cast-checks diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml index 2b8eb1a56dec8..c971d223ff331 100644 --- a/.github/workflows/rustc.yml +++ b/.github/workflows/rustc.yml @@ -61,6 +61,9 @@ jobs: - name: Run tests working-directory: upstream + env: + # Avoid error due to unexpected `cfg`. + RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))" run: | ./configure --set=llvm.download-ci-llvm=true ./x test --stage 0 library/std diff --git a/.gitignore b/.gitignore index fa490af4c013e..f9fe675ebbe11 100644 --- a/.gitignore +++ b/.gitignore @@ -26,6 +26,7 @@ Session.vim *.rlib *.rmeta *.mir +Cargo.lock ## Temporary files *~ diff --git a/library/contracts/safety/Cargo.toml b/library/contracts/safety/Cargo.toml new file mode 100644 index 0000000000000..e51487e7266e9 --- /dev/null +++ b/library/contracts/safety/Cargo.toml @@ -0,0 +1,17 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "safety" +version = "0.1.0" +edition = "2021" +license = "MIT OR Apache-2.0" + +[lib] +proc-macro = true + +[dependencies] +proc-macro2 = "1.0" +proc-macro-error = "1.0.4" +quote = "1.0.20" +syn = { version = "2.0.18", features = ["full"] } diff --git a/library/contracts/safety/build.rs b/library/contracts/safety/build.rs new file mode 100644 index 0000000000000..e74a4c9e57d6e --- /dev/null +++ b/library/contracts/safety/build.rs @@ -0,0 +1,4 @@ +fn main() { + // We add the configurations here to be checked. + println!("cargo:rustc-check-cfg=cfg(kani_host)"); +} diff --git a/library/contracts/safety/src/kani.rs b/library/contracts/safety/src/kani.rs new file mode 100644 index 0000000000000..a8b4ab360dc8e --- /dev/null +++ b/library/contracts/safety/src/kani.rs @@ -0,0 +1,21 @@ +use proc_macro::{TokenStream}; +use quote::{quote, format_ident}; +use syn::{ItemFn, parse_macro_input}; + +pub(crate) fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + rewrite_attr(attr, item, "requires") +} + +pub(crate) fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + rewrite_attr(attr, item, "ensures") +} + +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); + let attribute = format_ident!("{}", name); + quote!( + #[kani_core::#attribute(#args)] + #fn_item + ).into() +} diff --git a/library/contracts/safety/src/lib.rs b/library/contracts/safety/src/lib.rs new file mode 100644 index 0000000000000..9fe852a622de3 --- /dev/null +++ b/library/contracts/safety/src/lib.rs @@ -0,0 +1,25 @@ +//! Implement a few placeholders for contract attributes until they get implemented upstream. +//! Each tool should implement their own version in a separate module of this crate. + +use proc_macro::TokenStream; +use proc_macro_error::proc_macro_error; + +#[cfg(kani_host)] +#[path = "kani.rs"] +mod tool; + +#[cfg(not(kani_host))] +#[path = "runtime.rs"] +mod tool; + +#[proc_macro_error] +#[proc_macro_attribute] +pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + tool::requires(attr, item) +} + +#[proc_macro_error] +#[proc_macro_attribute] +pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + tool::ensures(attr, item) +} diff --git a/library/contracts/safety/src/runtime.rs b/library/contracts/safety/src/runtime.rs new file mode 100644 index 0000000000000..78e8b1dc354d2 --- /dev/null +++ b/library/contracts/safety/src/runtime.rs @@ -0,0 +1,15 @@ +use proc_macro::TokenStream; + +/// For now, runtime requires is a no-op. +/// +/// TODO: At runtime the `requires` should become an assert unsafe precondition. +pub(crate) fn requires(_attr: TokenStream, item: TokenStream) -> TokenStream { + item +} + +/// For now, runtime requires 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 +} diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index 0c2642341235b..e9fb39f19966c 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -24,6 +24,9 @@ name = "corebenches" path = "benches/lib.rs" test = true +[dependencies] +safety = {path = "../contracts/safety" } + [dev-dependencies] rand = { version = "0.8.5", default-features = false } rand_xorshift = { version = "0.3.0", default-features = false } diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 206d1ab885291..7626d6d4a3cc8 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -431,6 +431,9 @@ mod unit; #[stable(feature = "core_primitive", since = "1.43.0")] pub mod primitive; +#[cfg(kani)] +kani_core::kani_lib!(core); + // Pull in the `core_arch` crate directly into core. The contents of // `core_arch` are in a different repository: rust-lang/stdarch. // diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index d2bbdc84d4dd1..61d101c766f49 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -416,6 +416,8 @@ use crate::marker::FnPtr; use crate::ub_checks; use crate::mem::{self, align_of, size_of, MaybeUninit}; +#[cfg(kani)] +use crate::kani; mod alignment; #[unstable(feature = "ptr_alignment_type", issue = "102070")] @@ -1687,6 +1689,7 @@ pub const unsafe fn write_unaligned(dst: *mut T, src: T) { #[stable(feature = "volatile", since = "1.9.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_diagnostic_item = "ptr_read_volatile"] +#[safety::requires(ub_checks::can_dereference(src))] pub unsafe fn read_volatile(src: *const T) -> T { // SAFETY: the caller must uphold the safety contract for `volatile_load`. unsafe { @@ -1766,6 +1769,7 @@ pub unsafe fn read_volatile(src: *const T) -> T { #[stable(feature = "volatile", since = "1.9.0")] #[rustc_diagnostic_item = "ptr_write_volatile"] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces +#[safety::requires(ub_checks::can_write(dst))] pub unsafe fn write_volatile(dst: *mut T, src: T) { // SAFETY: the caller must uphold the safety contract for `volatile_store`. unsafe { @@ -2290,3 +2294,20 @@ pub macro addr_of($place:expr) { pub macro addr_of_mut($place:expr) { &raw mut $place } + +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +mod verify { + use crate::fmt::Debug; + use super::*; + use crate::kani; + + #[kani::proof_for_contract(read_volatile)] + pub fn check_read_u128() { + let val = kani::any::(); + let ptr = &val as *const _; + let copy = unsafe { read_volatile(ptr) }; + assert_eq!(val, copy); + } +} + diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index 1aa6a288e7082..b864b63c5c661 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -160,3 +160,51 @@ pub(crate) const fn is_nonoverlapping( // This is just for safety checks so we can const_eval_select. const_eval_select((src, dst, size, count), comptime, runtime) } + +pub use predicates::*; + +/// Provide a few predicates to be used in safety contracts. +/// +/// At runtime, they are no-op, and always return true. +#[cfg(not(kani))] +mod predicates { + /// Checks if a pointer can be dereferenced, ensuring: + /// * `src` is valid for reads (see [`crate::ptr`] documentation). + /// * `src` is properly aligned (use `read_unaligned` if not). + /// * `src` points to a properly initialized value of type `T`. + /// + /// [`crate::ptr`]: https://doc.rust-lang.org/std/ptr/index.html + pub fn can_dereference(src: *const T) -> bool { + let _ = src; + true + } + + /// Check if a pointer can be written to: + /// * `dst` must be valid for writes. + /// * `dst` must be properly aligned. Use `write_unaligned` if this is not the + /// case. + pub fn can_write(dst: *mut T) -> bool { + let _ = dst; + true + } + + /// Check if a pointer can be the target of unaligned reads. + /// * `src` must be valid for reads. + /// * `src` must point to a properly initialized value of type `T`. + pub fn can_read_unaligned(src: *const T) -> bool { + let _ = src; + true + } + + /// Check if a pointer can be the target of unaligned writes. + /// * `dst` must be valid for writes. + pub fn can_write_unaligned(dst: *mut T) -> bool { + let _ = dst; + true + } +} + +#[cfg(kani)] +mod predicates { + pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned}; +}