From 4db111ff2649581be7c304b24736ac4b0dbe1e95 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 23:31:37 -0500 Subject: [PATCH 1/2] `kani list` Workflow (#146) Adds a workflow that runs `kani list` on the standard library and posts the results in a comment on the pull request. This workflow runs iff a pull request is merged, so that we have one comment at the end of a PR with the most up-to-date list results. (I considered other approaches, like running it on opening the PR or with every commit, but decided having one single comment with the final changes was best for brevity/clarity). See this [test PR](https://github.com/carolynzech/verify-rust-std/pull/10) on my fork as a demo of how it would work. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val --- .github/workflows/kani.yml | 14 ++++++++++++++ scripts/run-kani.sh | 33 ++++++++++++++++++++++++++++----- 2 files changed, 42 insertions(+), 5 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 6dec32c1620ec..b3c8aa3882066 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -65,3 +65,17 @@ jobs: - name: Test Kani script (In Repo Directory) working-directory: ${{github.workspace}}/head run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse + + # Step 4: Run list on the std library and add output to job summary + - name: Run Kani List + run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head + + - name: Add Kani List output to job summary + uses: actions/github-script@v6 + with: + script: | + const fs = require('fs'); + const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8'); + await core.summary + .addRaw(kaniOutput) + .write(); \ No newline at end of file diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 1c62a05969e34..e8f0dc42193d6 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -3,10 +3,11 @@ set -e usage() { - echo "Usage: $0 [options] [-p ] [--kani-args ]" + echo "Usage: $0 [options] [-p ] [--run ] [--kani-args ]" echo "Options:" echo " -h, --help Show this help message" echo " -p, --path Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory." + echo " --run Optional: Specify whether to run 'verify-std' or 'list' command. Defaults to 'verify-std' if not specified." echo " --kani-args Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument." exit 1 } @@ -14,6 +15,7 @@ usage() { # Initialize variables command_args="" path="" +run_command="verify-std" # Parse command line arguments # TODO: Improve parsing with getopts @@ -31,13 +33,23 @@ while [[ $# -gt 0 ]]; do usage fi ;; + --run) + if [[ -n $2 && ($2 == "verify-std" || $2 == "list") ]]; then + run_command=$2 + shift 2 + else + echo "Error: Invalid run command. Must be 'verify-std' or 'list'." + usage + fi + ;; --kani-args) shift command_args="$@" break ;; *) - break + echo "Error: Unknown option $1" + usage ;; esac done @@ -181,9 +193,20 @@ main() { echo "Running Kani command..." "$kani_path" --version - echo "Running Kani verify-std command..." - - "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12 + if [[ "$run_command" == "verify-std" ]]; then + echo "Running Kani verify-std command..." + "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" \ + -Z function-contracts \ + -Z mem-predicates \ + -Z loop-contracts \ + --output-format=terse \ + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 + elif [[ "$run_command" == "list" ]]; then + echo "Running Kani list command..." + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates ./library --std > $path/kani_list.txt + fi } main From 8f5512db864f3c568766b7f5b90d83a31320445c Mon Sep 17 00:00:00 2001 From: Daniel Tu <135958699+danielhumanmod@users.noreply.github.com> Date: Wed, 20 Nov 2024 09:15:54 -0800 Subject: [PATCH 2/2] Contracts & Harnesses for `swap`, `replace`, and `drop_in_place` (#144) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit # Description This PR introduces function contracts and proof harness for the NonNull pointer in the Rust core library. Specifically, it verifies three new APIs—`swap`, `replace`, and `drop_in_place` with Kani. These changes enhance the functionality of memory operations for NonNull pointers. # Change Overview Covered APIs: 1. NonNull::swap: Swaps the values at two mutable locations of the same type 2. NonNull::replace: Replaces the pointer's value, returning the old value 3. NonNull::drop_in_place: Executes the destructor (if any) of the pointed-to value Resolves #53 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/ptr/non_null.rs | 63 +++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index e6f5bff9eca60..4834c8009ec44 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -10,7 +10,6 @@ use crate::ub_checks::assert_unsafe_precondition; use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; - #[cfg(kani)] use crate::kani; #[cfg(kani)] @@ -1060,6 +1059,8 @@ impl NonNull { /// [`ptr::drop_in_place`]: crate::ptr::drop_in_place() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure self is aligned, initialized, and valid for read + #[requires(ub_checks::can_write(self.as_ptr() as *mut()))] // Ensure self is valid for write pub unsafe fn drop_in_place(self) { // SAFETY: the caller must uphold the safety contract for `drop_in_place`. unsafe { ptr::drop_in_place(self.as_ptr()) } @@ -1151,6 +1152,9 @@ impl NonNull { /// [`ptr::replace`]: crate::ptr::replace() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] + #[cfg_attr(kani, kani::modifies(self.as_ptr()))] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is aligned, initialized, and valid for read + #[requires(ub_checks::can_write(self.as_ptr()))] // Ensure self is valid for write pub unsafe fn replace(self, src: T) -> T where T: Sized, @@ -1169,6 +1173,9 @@ impl NonNull { #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_swap", issue = "83163")] + #[cfg_attr(kani, kani::modifies(self.as_ptr(), with.as_ptr()))] + #[requires(ub_checks::can_dereference(self.as_ptr()) && ub_checks::can_write(self.as_ptr()))] + #[requires(ub_checks::can_dereference(with.as_ptr()) && ub_checks::can_write(with.as_ptr()))] pub const unsafe fn swap(self, with: NonNull) where T: Sized, @@ -2118,4 +2125,58 @@ mod verify { let _ = ptr.get_unchecked_mut(lower..upper); } } + + #[kani::proof_for_contract(NonNull::replace)] + pub fn non_null_check_replace() { + let mut x: i32 = kani::any(); + let mut y: i32 = kani::any(); + + let origin_ptr = NonNull::new(&mut x as *mut i32).unwrap(); + unsafe { + let captured_original = ptr::read(origin_ptr.as_ptr()); + let replaced = origin_ptr.replace(y); + let after_replace = ptr::read(origin_ptr.as_ptr()); + + assert_eq!(captured_original, replaced); + assert_eq!(after_replace, y) + } + } + + #[kani::proof_for_contract(NonNull::drop_in_place)] + pub fn non_null_check_drop_in_place() { + struct Droppable { + value: i32, + } + + impl Drop for Droppable { + fn drop(&mut self) { + } + } + + let mut droppable = Droppable { value: kani::any() }; + let ptr = NonNull::new(&mut droppable as *mut Droppable).unwrap(); + unsafe { + ptr.drop_in_place(); + } + } + + #[kani::proof_for_contract(NonNull::swap)] + pub fn non_null_check_swap() { + let mut a: i32 = kani::any(); + let mut b: i32 = kani::any(); + + let ptr_a = NonNull::new(&mut a as *mut i32).unwrap(); + let ptr_b = NonNull::new(&mut b as *mut i32).unwrap(); + + unsafe { + let old_a = ptr::read(ptr_a.as_ptr()); + let old_b = ptr::read(ptr_b.as_ptr()); + ptr_a.swap(ptr_b); + // Verify that the values have been swapped. + let new_a = ptr::read(ptr_a.as_ptr()); + let new_b = ptr::read(ptr_b.as_ptr()); + assert_eq!(old_a, new_b); + assert_eq!(old_b, new_a); + } + } }