From 15a8e65778de43886813a211f859f088c50a0b82 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 12 Dec 2024 23:45:09 +0100 Subject: [PATCH 1/7] Add review guidelines (#226) Extends committee membership information with guidance on what is expected of committee members. 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: Carolyn Zech --- doc/src/general-rules.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/doc/src/general-rules.md b/doc/src/general-rules.md index b56ddc7e7d778..b5cc9604e4b35 100644 --- a/doc/src/general-rules.md +++ b/doc/src/general-rules.md @@ -92,3 +92,21 @@ members = [ + "rahulku" ] ``` + +Committee members are expected to contribute by reviewing pull requests (all +pull requests review approvals from at least two committee members before they +can be merged). +Reviews of solutions towards challenges should consider at least the following aspects: + +1. Does the pull request implement a solution that respects/meets the success + criteria of the challenge? +2. Do the contracts and harnesses incorporate the safety conditions stated in + the documentation (from comments in the code and the + [standard library documentation](https://doc.rust-lang.org/std/index.html))? + Note that we currently focus on safety verification. Pre- and post-conditions + towards functional correctness are acceptable as long as they do not + negatively impact verification of safety, such as over-constraining input + values or causing excessive verification run time. +3. Is the contributed code of adequate quality, idiomatic, and stands a chance + to be accepted into the standard library (to the best of the committee + member's knowledge)? From b0fdecf3f4b8c1fc103c65c7d3b31f7bb612ab76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kalle=20Ahlstr=C3=B6m?= <71292737+kahlstrm@users.noreply.github.com> Date: Fri, 13 Dec 2024 08:39:40 +0200 Subject: [PATCH 2/7] Fix intrinsics challenge typo in summary (#228) This PR fixes a minor typo in `SUMMARY.md` I noticed while browsing through the site. 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/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 3f99b7ffc8985..35377852d0d15 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -14,7 +14,7 @@ - [Challenges](./challenges.md) - [1: Verify core transmuting methods](./challenges/0001-core-transmutation.md) - - [2: Verify the memory safery of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md) + - [2: Verify the memory safety of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md) - [3: Verifying Raw Pointer Arithmetic Operations](./challenges/0003-pointer-arithmentic.md) - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md) From 928c07ec7699f45ee857ba4b3e6b03a8228c7b8a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Dec 2024 19:04:25 +0100 Subject: [PATCH 3/7] Remove non-endorsement note (#227) We now have the foundation's endorsement for this work. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- README.md | 3 ++- doc/src/general-rules.md | 2 -- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 2417adde4e446..8ba51232cb91f 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,8 @@ The goal is to have a verified [Rust standard library](https://doc.rust-lang.org 2. Creating new techniques to perform scalable verification 3. Apply techniques to verify previously unverified parts of the standard library. -For that we are launching a contest that includes a series of challenges that focus on verifying +For that we are launching a [contest supported by the Rust Foundation](https://foundation.rust-lang.org/news/rust-foundation-collaborates-with-aws-initiative-to-verify-rust-standard-libraries/) +that includes a series of challenges that focus on verifying memory safety and a subset of undefined behaviors in the Rust standard library. Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its successful completion. diff --git a/doc/src/general-rules.md b/doc/src/general-rules.md index b5cc9604e4b35..0b884d996ba24 100644 --- a/doc/src/general-rules.md +++ b/doc/src/general-rules.md @@ -6,8 +6,6 @@ and we kept a copy of the Rust standard library inside the `library/` folder that shall be used as the verification target for all our challenges. We will periodically update the `library/` folder to track newer versions of the [official Rust standard library](https://github.com/rust-lang/rust/). -**NOTE:** This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation. - **Challenges:** Each individual verification effort will have a tracking issue where contributors can add comments and ask clarification questions. You can find the list of [open challenges here](https://github.com/model-checking/verify-rust-std/labels/Challenge). From 866a1951cebe0aca2072202b58911d78a6e6d688 Mon Sep 17 00:00:00 2001 From: Samuel Thomas Date: Wed, 18 Dec 2024 08:30:30 -0600 Subject: [PATCH 4/7] add challenge for safety of primitive conversions (#217) 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: Cole Vick Co-authored-by: Michael Tautschnig Co-authored-by: Carolyn Zech --- doc/src/SUMMARY.md | 2 +- doc/src/challenges/0014-convert-num.md | 150 +++++++++++++++++++++++++ 2 files changed, 151 insertions(+), 1 deletion(-) create mode 100644 doc/src/challenges/0014-convert-num.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 35377852d0d15..e6b2a9c78e598 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -26,4 +26,4 @@ - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) - [12: Safety of `NonZero`](./challenges/0012-nonzero.md) - [13: Safety of `CStr`](./challenges/0013-cstr.md) - + - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md) diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md new file mode 100644 index 0000000000000..e6dc78666718d --- /dev/null +++ b/doc/src/challenges/0014-convert-num.md @@ -0,0 +1,150 @@ +# Challenge 14: Safety of Primitive Conversions + +- **Status:** Open +- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220 +- **Start date:** 2024/12/15 +- **End date:** 2025/2/28 +- **Prize:** *TBD* + +------------------- + +## Goal + +Verify the safety of number conversions in `core::convert::num`. + +There are two conversions that use unsafe code: conversion from NonZero integer to NonZero integer and conversion from floating point number to integer. All conversions use macros to implement traits for primitive types in bulk. You will need to add contracts into the macros so that contracts are generated for each implementation. As the conversions are all macro generated, it is probably a good idea to write your own macro for generating the harnesses. + +### Success Criteria + +#### NonZero Conversions +Write a type invariant for `core::num::NonZero`, then write harnesses for all `nonzero` conversions. + +Write proof contracts for each NonZero primitive conversion, listed in full below. These conversions are implemented through two macros: `impl_nonzero_int_from_nonzero_int!` and `impl_nonzero_int_try_from_nonzero_int!`. + +For each invocation of `impl_nonzero_int_from_nonzero_int!`, prove that the conversion it implements does not cause undefined behavior nor panic. For example, for `impl_nonzero_int_from_nonzero_int!(u8 => u16);`, prove that calling `NonZero::from(small: NonZero)` does not cause undefined behavior nor panic for an arbitrary `small` that satisfies the `NonZero` type invariant. + +For each invocation of `impl_nonzero_int_try_from_nonzero_int!`, prove that the conversion it implements does not cause undefined behavior. For example, for `impl_nonzero_int_try_from_nonzero_int!(u16 => u8);`, prove that calling `NonZero::try_from(value: NonZero)` does not cause undefined behavior for an arbitrary `value` that satisfies the `NonZero` type invariant. Additionally, prove that if the `value` does not fit into the target type (e.g., `value` is too large to fit into a `NonZero`) that the function panics. + +non-zero unsigned integer -> non-zero unsigned integer +- `impl_nonzero_int_from_nonzero_int!(u8 => u16);` +- `impl_nonzero_int_from_nonzero_int!(u8 => u32);` +- `impl_nonzero_int_from_nonzero_int!(u8 => u64);` +- `impl_nonzero_int_from_nonzero_int!(u8 => u128);` +- `impl_nonzero_int_from_nonzero_int!(u8 => usize);` +- `impl_nonzero_int_from_nonzero_int!(u16 => u32);` +- `impl_nonzero_int_from_nonzero_int!(u16 => u64);` +- `impl_nonzero_int_from_nonzero_int!(u16 => u128);` +- `impl_nonzero_int_from_nonzero_int!(u16 => usize);` +- `impl_nonzero_int_from_nonzero_int!(u32 => u64);` +- `impl_nonzero_int_from_nonzero_int!(u32 => u128);` +- `impl_nonzero_int_from_nonzero_int!(u64 => u128);` + +non-zero signed integer -> non-zero signed integer +- `impl_nonzero_int_from_nonzero_int!(i8 => i16);` +- `impl_nonzero_int_from_nonzero_int!(i8 => i32);` +- `impl_nonzero_int_from_nonzero_int!(i8 => i64);` +- `impl_nonzero_int_from_nonzero_int!(i8 => i128);` +- `impl_nonzero_int_from_nonzero_int!(i8 => isize);` +- `impl_nonzero_int_from_nonzero_int!(i16 => i32);` +- `impl_nonzero_int_from_nonzero_int!(i16 => i64);` +- `impl_nonzero_int_from_nonzero_int!(i16 => i128);` +- `impl_nonzero_int_from_nonzero_int!(i16 => isize);` +- `impl_nonzero_int_from_nonzero_int!(i32 => i64);` +- `impl_nonzero_int_from_nonzero_int!(i32 => i128);` +- `impl_nonzero_int_from_nonzero_int!(i64 => i128);` + +non-zero unsigned -> non-zero signed integer +- `impl_nonzero_int_from_nonzero_int!(u8 => i16);` +- `impl_nonzero_int_from_nonzero_int!(u8 => i32);` +- `impl_nonzero_int_from_nonzero_int!(u8 => i64);` +- `impl_nonzero_int_from_nonzero_int!(u8 => i128);` +- `impl_nonzero_int_from_nonzero_int!(u8 => isize);` +- `impl_nonzero_int_from_nonzero_int!(u16 => i32);` +- `impl_nonzero_int_from_nonzero_int!(u16 => i64);` +- `impl_nonzero_int_from_nonzero_int!(u16 => i128);` +- `impl_nonzero_int_from_nonzero_int!(u32 => i64);` +- `impl_nonzero_int_from_nonzero_int!(u32 => i128);` +- `impl_nonzero_int_from_nonzero_int!(u64 => i128);` + +There are also the fallible versions. Remember to cover both the panicking and non-panicking cases. + +unsigned non-zero integer -> unsigned non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(u16 => u8);` +- `impl_nonzero_int_try_from_nonzero_int!(u32 => u8, u16, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(u64 => u8, u16, u32, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(u128 => u8, u16, u32, u64, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(usize => u8, u16, u32, u64, u128);` + +signed non-zero integer -> signed non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(i16 => i8);` +- `impl_nonzero_int_try_from_nonzero_int!(i32 => i8, i16, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(i64 => i8, i16, i32, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(i128 => i8, i16, i32, i64, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(isize => i8, i16, i32, i64, i128);` + +unsigned non-zero integer -> signed non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(u8 => i8);` +- `impl_nonzero_int_try_from_nonzero_int!(u16 => i8, i16, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(u32 => i8, i16, i32, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(u64 => i8, i16, i32, i64, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(u128 => i8, i16, i32, i64, i128, isize);` +- `impl_nonzero_int_try_from_nonzero_int!(usize => i8, i16, i32, i64, i128, isize);` + +signed non-zero integer -> unsigned non-zero integer +- `impl_nonzero_int_try_from_nonzero_int!(i8 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i16 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i32 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i64 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize);` +- `impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);` + + +#### Safety for Float to Int + +```rust +macro_rules! impl_float_to_int { + ($Float:ty => $($Int:ty),+) => { + #[unstable(feature = "convert_float_to_int", issue = "67057")] + impl private::Sealed for $Float {} + $( + #[unstable(feature = "convert_float_to_int", issue = "67057")] + impl FloatToInt<$Int> for $Float { + #[inline] + unsafe fn to_int_unchecked(self) -> $Int { + // SAFETY: the safety contract must be upheld by the caller. + unsafe { crate::intrinsics::float_to_int_unchecked(self) } + } + } + )+ + } +} +``` + +The safety constraints referenced in the comments are that the input value must: +- Not be NaN +- Not be infinite +- Be representable in the return type Int, after truncating off its fractional part + +These constraints are given in the [documentation](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). + +The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) LLVM instructions, which may be useful for reference. +Prove safety for each of the following conversions: + +- `impl_float_to_int!(f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` +- `impl_float_to_int!(f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` +- `impl_float_to_int!(f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` +- `impl_float_to_int!(f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)` + +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. From 67e2f1ce059818f369c441c9ef6285381403e489 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 19 Dec 2024 13:51:20 -0500 Subject: [PATCH 5/7] Parallelize & Partition Verification (#229) Shard Kani verification workflow across multiple runners by: 1. Running `kani list --format json`, which outputs a JSON file like this: ```json { "kani-version": "0.56.0", "file-version": "0.1", "standard-harnesses": { "src/lib.rs": [ "proof3", "verify::proof2" ], "src/test.rs": [ "test::proof4", "test::proof5" ] }, "contract-harnesses": { "src/lib.rs": [ "proof" ] }, "contracts": [ { "function": "bar", "file": "src/lib.rs", "harnesses": [ "proof" ] } ], "totals": { "standard-harnesses": 4, "contract-harnesses": 1, "functions-under-contract": 1 } } ``` 2. Extracting the harnesses inside `"standard-harnesses"` and `"contract-harnesses"` into an array called `ALL_HARNESSES` and the length of that array into `HARNESS_COUNT`. (So in this example, `ALL_HARNESSES = [proof3, verify::proof2, test::proof4, test::proof5, proof]` and `HARNESS_COUNT=5`). 3. Dividing the harnesses evenly between four workers. For example, if worker 1's harnesses are `proof3` and `verify::proof2`, then we call `kani verify-std --harness proof3 --harness verify::proof2 --exact`. The `--exact` makes Kani look for the exact harness name. This is important so that we don't match on partial patterns, e.g., if there is a harness called "foo" and a harness called "foo_bar", passing `--harness foo` without `--exact` would match against both harnesses, and then `foo_bar` would run twice. 4. Also parallelize verification within a single runner by passing `-j` to Kani. I chose four workers somewhat arbitrarily--it makes each worker take about 45 minutes to an hour to finish. I thought it was good to have a balance between too few workers (which still makes us wait a while) and too many workers (which makes you look through more logs to find where a given harness is being verified). But happy to play with this number if people have opinions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/workflows/kani.yml | 20 +++++-- scripts/run-kani.sh | 104 +++++++++++++++++++++++++++++++------ 2 files changed, 106 insertions(+), 18 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 89d9096ec3289..90463ec8574c6 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -17,16 +17,25 @@ defaults: jobs: check-kani-on-std: - name: Verify std library + name: Verify std library (partition ${{ matrix.partition }}) runs-on: ${{ matrix.os }} strategy: matrix: os: [ubuntu-latest, macos-latest] + partition: [1, 2, 3, 4] include: - os: ubuntu-latest base: ubuntu - os: macos-latest base: macos + fail-fast: false + + env: + # Define the index of this particular worker [1-WORKER_TOTAL] + WORKER_INDEX: ${{ matrix.partition }} + # Total number of workers running this step + WORKER_TOTAL: 4 + steps: # Step 1: Check out the repository - name: Checkout Repository @@ -34,8 +43,13 @@ jobs: with: path: head submodules: true - - # Step 2: Run Kani on the std library (default configuration) + + # Step 2: Install jq + - name: Install jq + if: matrix.os == 'ubuntu-latest' + run: sudo apt-get install -y jq + + # Step 3: Run Kani on the std library (default configuration) - name: Run Kani Verification run: head/scripts/run-kani.sh --path ${{github.workspace}}/head diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 652680bd7eb78..72aa8ef176056 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -77,6 +77,22 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE} REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL} BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME} +# Unstable arguments to pass to Kani +unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts" + +# Variables used for parallel harness verification +# When we say "parallel," we mean two dimensions of parallelization: +# 1. Sharding verification across multiple workers. The Kani workflow that calls this script defines WORKER_INDEX and WORKER_TOTAL for this purpose: +# we shard verification across WORKER_TOTAL workers, where each worker has a unique WORKER_INDEX that it uses to derive its share of ALL_HARNESSES to verify. +# 2. Within a single worker, we parallelize verification between multiple cores by invoking kani with -j. + +# Array of all of the harnesses in the repository, set in get_harnesses() +declare -a ALL_HARNESSES +# Length of ALL_HARNESSES, set in get_harnesses() +declare -i HARNESS_COUNT +# `kani list` JSON FILE_VERSION that the parallel verification command expects +EXPECTED_JSON_FILE_VERSION="0.1" + # Function to read commit ID from TOML file read_commit_from_toml() { local file="$1" @@ -151,10 +167,50 @@ get_kani_path() { echo "$(realpath "$build_dir/scripts/kani")" } -run_kani_command() { +# Run kani list with JSON format and process with jq to extract harness names and total number of harnesses. +# Note: The code to extract ALL_HARNESSES is dependent on `kani list --format json` FILE_VERSION 0.1. +# (The FILE_VERSION variable is defined in Kani in the list module's output code, current path kani-driver/src/list/output.rs) +# If FILE_VERSION changes, first update the ALL_HARNESSES extraction logic to work with the new format, if necessary, +# then update EXPECTED_JSON_FILE_VERSION. +get_harnesses() { local kani_path="$1" - shift - "$kani_path" "$@" + "$kani_path" list -Z list $unstable_args ./library --std --format json + local json_file_version=$(jq -r '.["file-version"]' "$WORK_DIR/kani-list.json") + if [[ $json_file_version != $EXPECTED_JSON_FILE_VERSION ]]; then + echo "Error: The JSON file-version in kani-list.json does not equal $EXPECTED_JSON_FILE_VERSION" + exit 1 + fi + # Extract the harnesses inside "standard-harnesses" and "contract-harnesses" + # into an array called ALL_HARNESSES and the length of that array into HARNESS_COUNT + ALL_HARNESSES=($(jq -r ' + ([.["standard-harnesses"] | to_entries | .[] | .value[]] + + [.["contract-harnesses"] | to_entries | .[] | .value[]]) | + .[] + ' $WORK_DIR/kani-list.json)) + HARNESS_COUNT=${#ALL_HARNESSES[@]} +} + +# Given an array of harness names, run verification for those harnesses +run_verification_subset() { + local kani_path="$1" + local harnesses=("${@:2}") # All arguments after kani_path are harness names + + # Build the --harness arguments + local harness_args="" + for harness in "${harnesses[@]}"; do + harness_args="$harness_args --harness $harness" + done + + echo "Running verification for harnesses:" + printf '%s\n' "${harnesses[@]}" + "$kani_path" verify-std -Z unstable-options ./library \ + $unstable_args \ + $harness_args --exact \ + -j \ + --output-format=terse \ + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 } # Check if binary exists and is up to date @@ -176,7 +232,6 @@ check_binary_exists() { return 1 } - main() { local build_dir="$WORK_DIR/kani_build" @@ -209,19 +264,38 @@ main() { "$kani_path" --version 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 \ - -Z float-lib \ - -Z c-ffi \ - $command_args \ - --enable-unstable \ - --cbmc-args --object-bits 12 + if [[ -n "$WORKER_INDEX" && -n "$WORKER_TOTAL" ]]; then + echo "Running as parallel worker $WORKER_INDEX of $WORKER_TOTAL" + get_harnesses "$kani_path" + + echo "All harnesses:" + printf '%s\n' "${ALL_HARNESSES[@]}" + echo "Total number of harnesses: $HARNESS_COUNT" + + # Calculate this worker's portion (add WORKER_TOTAL - 1 to force ceiling division) + chunk_size=$(( (HARNESS_COUNT + WORKER_TOTAL - 1) / WORKER_TOTAL )) + echo "Number of harnesses this worker will run: $chunk_size" + + start_idx=$(( (WORKER_INDEX - 1) * chunk_size )) + echo "Start index into ALL_HARNESSES is $start_idx" + + # Extract this worker's harnesses + worker_harnesses=("${ALL_HARNESSES[@]:$start_idx:$chunk_size}") + + # Run verification for this subset + run_verification_subset "$kani_path" "${worker_harnesses[@]}" + else + # Run verification for all harnesses (not in parallel) + echo "Running Kani verify-std command..." + "$kani_path" verify-std -Z unstable-options ./library \ + $unstable_args + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 + fi elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." - "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format markdown + "$kani_path" list -Z list $unstable_args ./library --std --format markdown fi } From 5da586f715dba2dcd175d9863bfa5d383c9b0bf1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 19 Dec 2024 15:37:17 -0500 Subject: [PATCH 6/7] Improve `u16::carrying_mul` harness performance (#230) This harness takes between 22-25 minutes in CI. Change the harnesses's macro to use kissat solver instead, which brings verification time down to ~7 seconds. As an aside, I noticed this problem because the partition 1 runner in #229 is taking ~55 minutes, where the other partitions are taking ~30 minutes. This harness accounts for almost the entire difference. One nice consequence of partitioning verification is that it will make performance issues like this more noticeable. 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/num/mod.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index cea05a55a7cda..a561eb3f9375b 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1759,6 +1759,7 @@ mod verify { ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => { $( #[kani::proof] + #[kani::solver(kissat)] pub fn $harness_name() { let lhs: $type = kani::any::<$type>(); let rhs: $type = kani::any::<$type>(); From 1a38674ad6753e3a78e0181d1fe613f3b25ebacd Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Sat, 21 Dec 2024 18:31:53 -0800 Subject: [PATCH 7/7] Add missing line separator (#232) Fix a typo introduced in #229 that prevents `kani-args` from getting passed to the `kani` command. This was discovered by @tengjiang (see https://github.com/model-checking/verify-rust-std/discussions/231). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- scripts/run-kani.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 72aa8ef176056..63df2886d0d71 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -288,7 +288,7 @@ main() { # Run verification for all harnesses (not in parallel) echo "Running Kani verify-std command..." "$kani_path" verify-std -Z unstable-options ./library \ - $unstable_args + $unstable_args \ $command_args \ --enable-unstable \ --cbmc-args --object-bits 12