Merge branch 'main' into chores-170-target

.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();

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<T: ?Sized> NonNull<T> {
     /// [`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<T: ?Sized> NonNull<T> {
     /// [`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<T: ?Sized> NonNull<T> {
     #[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<T>)
     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);
+        }
+    }
 }

scripts/run-kani.sh

@@ -3,17 +3,19 @@
 set -e
 
 usage() {
-    echo "Usage: $0 [options] [-p <path>] [--kani-args <command arguments>]"
+    echo "Usage: $0 [options] [-p <path>] [--run <verify-std|list>] [--kani-args <command arguments>]"
     echo "Options:"
     echo "  -h, --help         Show this help message"
     echo "  -p, --path <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 <verify-std|list>  Optional: Specify whether to run 'verify-std' or 'list' command. Defaults to 'verify-std' if not specified."
     echo "  --kani-args  <command arguments to kani>  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
 }
 
 # 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