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/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); + } + } } diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 3b009bfff22ac..e32bb22c23f56 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 @@ -196,9 +208,20 @@ main() { echo "Running Kani command..." "$kani_path" --version - echo "Running Kani verify-std command..." - - "$kani_path" verify-std -Z unstable-options ./library -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 \ + -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