From 4db111ff2649581be7c304b24736ac4b0dbe1e95 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 23:31:37 -0500 Subject: [PATCH 1/5] `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/5] 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); + } + } } From 971befd78b5e59456280724e8c67bf1a3b43c42b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 20 Nov 2024 11:43:45 -0800 Subject: [PATCH 3/5] Improve run-kani script to use default target (#172) Use default target folder instead of using a temporary folder. Users are still able to customize the folder using Kani argument. Avoid needless updates when Kani dependencies are already up-to-date. Fixes #170 --- scripts/run-kani.sh | 63 ++++++++++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 27 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index e8f0dc42193d6..e32bb22c23f56 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -92,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() { @@ -115,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 } @@ -147,11 +163,15 @@ 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 } @@ -159,7 +179,6 @@ check_binary_exists() { 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" @@ -173,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" @@ -195,7 +210,7 @@ main() { 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" \ + "$kani_path" verify-std -Z unstable-options ./library \ -Z function-contracts \ -Z mem-predicates \ -Z loop-contracts \ @@ -211,9 +226,3 @@ main() { main -cleanup() -{ - rm -rf "$temp_dir_target" -} - -trap cleanup EXIT From a8dd9753fb7d02f9e023083bb5642f804dcb671b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 20 Nov 2024 15:02:19 -0500 Subject: [PATCH 4/5] Add @jswrenn to reviewers list (#175) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/pull_requests.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index d5d88e0b9fca5..a83cebe76609e 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -15,5 +15,6 @@ members = [ "carolynzech", "robdockins", "HuStmpHrrr", - "Eh2406" + "Eh2406", + "jswrenn" ] From 406b1c196a08c69444351721a41bc73922f48c9b Mon Sep 17 00:00:00 2001 From: Bhuwan Pandit Date: Fri, 22 Nov 2024 15:27:06 +0000 Subject: [PATCH 5/5] docs(0005): typo fix in the challenge docs (#178) This PR, just fixes a typo for a function name in the challenge docs. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- doc/src/challenges/0005-linked-list.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index a5c931712025a..0215bbd029714 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -23,7 +23,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 |