Merge branch 'main' into chores-update-rewards

.github/pull_requests.toml

@@ -15,5 +15,6 @@ members = [
     "carolynzech",
     "robdockins",
     "HuStmpHrrr",
-    "Eh2406"
+    "Eh2406",
+    "jswrenn"
 ]

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

doc/src/challenges/0005-linked-list.md

@@ -24,7 +24,7 @@ The memory safety of the following public functions that iterating over the inte
 
 | Function | Location |
 |---------|---------|
-|clearn | alloc::collections::linked_list |
+|clear| alloc::collections::linked_list |
 |contains| alloc::collections::linked_list |
 |split_off| alloc::collections::linked_list |
 |remove| alloc::collections::linked_list |

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
@@ -80,15 +92,26 @@ read_commit_from_toml() {
     echo "$commit"
 }
 
-clone_kani_repo() {
+setup_kani_repo() {
     local repo_url="$1"
     local directory="$2"
     local branch="$3"
     local commit="$4"
-    git clone "$repo_url" "$directory"
-    pushd "$directory"
-    git checkout "$commit"
-    popd
+
+    if [[ ! -d "${directory}" ]]; then
+        mkdir -p "${directory}"
+        pushd "${directory}" > /dev/null
+
+        git init . >& /dev/null
+        git remote add origin "${repo_url}" >& /dev/null
+    else
+        pushd "${directory}" > /dev/null
+    fi
+
+    git fetch --depth 1 origin "$commit" --quiet
+    git checkout "$commit" --quiet
+    git submodule update --init --recursive --depth 1 --quiet
+    popd > /dev/null
 }
 
 get_current_commit() {
@@ -103,17 +126,22 @@ get_current_commit() {
 build_kani() {
     local directory="$1"
     pushd "$directory"
-    os_name=$(uname -s)
-
-    if [[ "$os_name" == "Linux" ]]; then
-        ./scripts/setup/ubuntu/install_deps.sh
-    elif [[ "$os_name" == "Darwin" ]]; then
-        ./scripts/setup/macos/install_deps.sh
+    source "kani-dependencies"
+    # Check if installed versions are correct.
+    if ./scripts/check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} && ./scripts/check_kissat_version.sh; then
+        echo "Dependencies are up-to-date"
     else
-        echo "Unknown operating system"
+        os_name=$(uname -s)
+
+        if [[ "$os_name" == "Linux" ]]; then
+            ./scripts/setup/ubuntu/install_deps.sh
+        elif [[ "$os_name" == "Darwin" ]]; then
+            ./scripts/setup/macos/install_deps.sh
+        else
+            echo "Unknown operating system"
+        fi
     fi
 
-    git submodule update --init --recursive
     cargo build-dev --release
     popd
 }
@@ -135,19 +163,22 @@ check_binary_exists() {
     local expected_commit="$2"
     local kani_path=$(get_kani_path "$build_dir")
 
-    if [[ -f "$kani_path" ]]; then
+    if [[ -d "${build_dir}" ]]; then
         local current_commit=$(get_current_commit "$build_dir")
         if [[ "$current_commit" = "$expected_commit" ]]; then
             return 0
+        else
+            echo "Kani repository is out of date. Rebuilding..."
         fi
+    else
+        echo "Kani repository not found. Creating..."
     fi
     return 1
 }
 
 
 main() {
     local build_dir="$WORK_DIR/kani_build"
-    local temp_dir_target=$(mktemp -d)
 
     echo "Using TOML file: $TOML_FILE"
     echo "Using repository URL: $REPO_URL"
@@ -161,12 +192,8 @@ main() {
     else
         echo "Building Kani from commit: $commit"
 
-        # Remove old build directory if it exists
-        rm -rf "$build_dir"
-        mkdir -p "$build_dir"
-
         # Clone repository and checkout specific commit
-        clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
+        setup_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
 
         # Build project
         build_kani "$build_dir"
@@ -181,16 +208,21 @@ 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 \
+            -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
 
-cleanup()
-{
-  rm -rf "$temp_dir_target"
-}
-
-trap cleanup EXIT