From 3a967e316ab90736da81b75789dca9763a306f1e Mon Sep 17 00:00:00 2001 From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com> Date: Thu, 17 Oct 2024 06:29:26 -0700 Subject: [PATCH 1/6] Contracts & Harnesses for `wrapping_shl` (#112) Towards #59 ### Changes * Added contracts for `wrapping_shl` (located in `library/core/src/num/int_macros.rs` and `uint_macros.rs`) * Added a macro for generating wrapping_{shl, shr} harnesses * Added harnesses for `wrapping_shl` of each integer type * `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`, `u128`, `usize` --- 12 harnesses in total. ### Revalidation 1. Per the discussion in #59, we have to **build and run Kani from `feature/verify-rust-std` branch**. 2. To revalidate the verification results, run the following command. `` can be either `num::verify` to run all harnesses or `num::verify::` (e.g. `checked_wrapping_shl_i8`) to run a specific harness. ``` kani verify-std "path/to/library" \ --harness \ -Z unstable-options \ -Z function-contracts \ -Z mem-predicates ``` All harnesses should pass the default checks (1251 checks where 1 unreachable). ``` SUMMARY: ** 0 of 1251 failed (1 unreachable) VERIFICATION:- SUCCESSFUL Verification Time: 2.4682913s Complete - 1 successfully verified harnesses, 0 failures, 1 total. ``` Example of the unreachable check: ``` Check 123: num::::wrapping_shl.assertion.1 - Status: UNREACHABLE - Description: "attempt to subtract with overflow" - Location: library/core/src/num/int_macros.rs:2172:42 in function num::::wrapping_shl ``` ### Questions 1. Should we add `requires` (and `ensures`) for `wrapping_shl` given that `unchecked_shl` already has a `requires`? 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/int_macros.rs | 1 + library/core/src/num/mod.rs | 38 +++++++++++++++++++++++++++++ library/core/src/num/uint_macros.rs | 1 + 3 files changed, 40 insertions(+) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index c84087172974a..03e1eb0bc5dab 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -2160,6 +2160,7 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] pub const fn wrapping_shl(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift // out of bounds diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 91c1ccb708613..f84b769bee976 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1687,6 +1687,19 @@ mod verify { } } + // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}` + macro_rules! generate_wrapping_shift_harness { + ($type:ty, $method:ident, $harness_name:ident) => { + #[kani::proof_for_contract($type::$method)] + pub fn $harness_name() { + let num1: $type = kani::any::<$type>(); + let num2: u32 = kani::any::(); + + let _ = num1.$method(num2); + } + } + } + // `unchecked_add` proofs // // Target types: @@ -1905,4 +1918,29 @@ mod verify { widening_mul_u64_large, u64::MAX - 10u64, u64::MAX, widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64 ); + + // `wrapping_shl` proofs + // + // Target types: + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total + // + // Target contracts: + // #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] + // + // Target function: + // pub const fn wrapping_shl(self, rhs: u32) -> Self + // + // This function performs an panic-free bitwise left shift operation. + generate_wrapping_shift_harness!(i8, wrapping_shl, checked_wrapping_shl_i8); + generate_wrapping_shift_harness!(i16, wrapping_shl, checked_wrapping_shl_i16); + generate_wrapping_shift_harness!(i32, wrapping_shl, checked_wrapping_shl_i32); + generate_wrapping_shift_harness!(i64, wrapping_shl, checked_wrapping_shl_i64); + generate_wrapping_shift_harness!(i128, wrapping_shl, checked_wrapping_shl_i128); + generate_wrapping_shift_harness!(isize, wrapping_shl, checked_wrapping_shl_isize); + generate_wrapping_shift_harness!(u8, wrapping_shl, checked_wrapping_shl_u8); + generate_wrapping_shift_harness!(u16, wrapping_shl, checked_wrapping_shl_u16); + generate_wrapping_shift_harness!(u32, wrapping_shl, checked_wrapping_shl_u32); + generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64); + generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128); + generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 0576e087935bb..67b8768dea1d0 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2138,6 +2138,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] pub const fn wrapping_shl(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift // out of bounds From a636c052abbcff26ac8f07a16c623ef7cd6fa5b1 Mon Sep 17 00:00:00 2001 From: MWDZ <101102544+MWDZ@users.noreply.github.com> Date: Mon, 21 Oct 2024 18:14:25 -0700 Subject: [PATCH 2/6] Contracts & Harnesses for wrapping_shr (#123) Towards https://github.com/model-checking/verify-rust-std/issues/59 Changes Added contracts for wrapping_shr (located in library/core/src/num/int_macros.rs and uint_macros.rs) Added harnesses for wrapping_shr of each integer type i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize --- 12 harnesses in total. Revalidation Per the discussion in https://github.com/model-checking/verify-rust-std/issues/59, we have to build and run Kani from feature/verify-rust-std branch. To revalidate the verification results, run the following command. can be either num::verify to run all harnesses or num::verify:: (e.g. checked_wrapping_shl_i8) to run a specific harness. ``` kani verify-std "path/to/library" \ --harness \ -Z unstable-options \ -Z function-contracts \ -Z mem-predicates ``` All harnesses should pass the default checks (1251 checks where 1 unreachable). ``` SUMMARY: ** 0 of 161 failed (1 unreachable) VERIFICATION:- SUCCESSFUL Verification Time: 0.32086188s Complete - 12 successfully verified harnesses, 0 failures, 12 total. ``` Example of the unreachable check: ``` Check 9: num::::wrapping_shr.assertion.1 - Status: UNREACHABLE - Description: "attempt to subtract with overflow" - Location: library/core/src/num/int_macros.rs:2199:42 in function num::::wrapping_shr ``` --------- Co-authored-by: Yenyun035 --- library/core/src/num/int_macros.rs | 1 + library/core/src/num/mod.rs | 24 ++++++++++++++++++++++++ library/core/src/num/uint_macros.rs | 1 + 3 files changed, 26 insertions(+) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 03e1eb0bc5dab..4ff7f97542d93 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -2191,6 +2191,7 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))] pub const fn wrapping_shr(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift // out of bounds diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index f84b769bee976..b123d998a8466 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1943,4 +1943,28 @@ mod verify { generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64); generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128); generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize); + + // `wrapping_shr` proofs + // + // Target types: + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total + // + // Target contracts: + // #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))] + // Target function: + // pub const fn wrapping_shr(self, rhs: u32) -> Self { + // + // This function performs an panic-free bitwise right shift operation. + generate_wrapping_shift_harness!(i8, wrapping_shr, checked_wrapping_shr_i8); + generate_wrapping_shift_harness!(i16, wrapping_shr, checked_wrapping_shr_i16); + generate_wrapping_shift_harness!(i32, wrapping_shr, checked_wrapping_shr_i32); + generate_wrapping_shift_harness!(i64, wrapping_shr, checked_wrapping_shr_i64); + generate_wrapping_shift_harness!(i128, wrapping_shr, checked_wrapping_shr_i128); + generate_wrapping_shift_harness!(isize, wrapping_shr, checked_wrapping_shr_isize); + generate_wrapping_shift_harness!(u8, wrapping_shr, checked_wrapping_shr_u8); + generate_wrapping_shift_harness!(u16, wrapping_shr, checked_wrapping_shr_u16); + generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32); + generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64); + generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); + generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 67b8768dea1d0..3220be1d86f30 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2172,6 +2172,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))] pub const fn wrapping_shr(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift // out of bounds From 0a8ba7bc4ccfc54aeaf786498fa49c5631df95e1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 22 Oct 2024 16:26:53 -0400 Subject: [PATCH 3/6] Fix tool template link in README (#132) --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c3c9712cb2669..41cf22c3a7c7a 100644 --- a/README.md +++ b/README.md @@ -47,4 +47,4 @@ See [the Rust repository](https://github.com/rust-lang/rust) for details. ## Introducing a New Tool -Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool. +Please use the [template available in this repository](./doc/src/tool_template.md) to introduce a new verification tool. From 38d490cd67a585a6e9834f30a235f6c0a3613b33 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 22 Oct 2024 22:30:48 +0100 Subject: [PATCH 4/6] Add safety dependency to alloc and std crates (#121) Just as previously done for core: this will enable future use of `safety::{ensures,requires}` in those crates. --- library/alloc/Cargo.toml | 1 + library/alloc/src/lib.rs | 1 + library/std/Cargo.toml | 1 + library/std/src/lib.rs | 1 + 4 files changed, 4 insertions(+) diff --git a/library/alloc/Cargo.toml b/library/alloc/Cargo.toml index 1bd4434d4f7e9..7911be6579f4e 100644 --- a/library/alloc/Cargo.toml +++ b/library/alloc/Cargo.toml @@ -11,6 +11,7 @@ edition = "2021" [dependencies] core = { path = "../core" } compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] } +safety = { path = "../contracts/safety" } [dev-dependencies] rand = { version = "0.8.5", default-features = false, features = ["alloc"] } diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 7aaa4e73df72c..d28c5a29df2b9 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -91,6 +91,7 @@ // // Library features: // tidy-alphabetical-start +#![cfg_attr(kani, feature(kani))] #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))] #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))] #![feature(alloc_layout_extra)] diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index e20fe9feff114..2d75324261318 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -26,6 +26,7 @@ hashbrown = { version = "0.14", default-features = false, features = [ std_detect = { path = "../stdarch/crates/std_detect", default-features = false, features = [ 'rustc-dep-of-std', ] } +safety = { path = "../contracts/safety" } # Dependencies of the `backtrace` crate rustc-demangle = { version = "0.1.24", features = ['rustc-dep-of-std'] } diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 60969af3e8541..3121ee8be8722 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -269,6 +269,7 @@ #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))] #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))] #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))] +#![cfg_attr(kani, feature(kani))] // // Language features: // tidy-alphabetical-start From 61f68cf35fac0dc992d53f6c36a38ddeaf0aa4d0 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Wed, 23 Oct 2024 18:15:26 -0400 Subject: [PATCH 5/6] Add script to automate build & running kani (#78) 1. Adds a one-click command to pull, build and run kani 2. Adds a toml file to store the commit info about the HEAD of `kani/features/verify-std` 3. Checks for caching to prevent re-pulling, and building already compatible kani binary 4. Modifies CI to re-use this script instead of the previous script 5. Add `--kani-args` to pass arguments to kani command. `-p` sets the working directory. 6. Adds a CI job to test the entrypoint workflow itself. 7. Default output-format to terse #### Extras Cleans up some print statements in the `run_update_with_checks` script. ## Call-out 1. This does not allow command configuration, so it essentially all proofs in the library by default, which CAN get expensive. I can very easily add a harness filter to ensure that we can process only relevent harnesses. 2. Need to change documentation to use this command instead of using kani directly as is currently suggested. 3. Need to consider move to python, argument parsing with bash is a bad experience. 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: Michael Tautschnig --- .github/workflows/kani.yml | 45 ++++++-- .gitignore | 1 + scripts/check_kani.sh | 55 ---------- scripts/run-kani.sh | 196 ++++++++++++++++++++++++++++++++++ tool_config/kani-version.toml | 5 + 5 files changed, 239 insertions(+), 63 deletions(-) delete mode 100644 scripts/check_kani.sh create mode 100755 scripts/run-kani.sh create mode 100644 tool_config/kani-version.toml diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index da0928998976c..6dec32c1620ec 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -1,6 +1,5 @@ -# This workflow is responsible for verifying the standard library with Kani. - name: Kani + on: workflow_dispatch: pull_request: @@ -9,18 +8,18 @@ on: paths: - 'library/**' - '.github/workflows/kani.yml' - - 'scripts/check_kani.sh' + - 'scripts/run-kani.sh' defaults: run: shell: bash jobs: - build: + check-kani-on-std: + name: Verify std library runs-on: ${{ matrix.os }} strategy: matrix: - # Kani does not support windows. os: [ubuntu-latest, macos-latest] include: - os: ubuntu-latest @@ -28,11 +27,41 @@ jobs: - os: macos-latest base: macos steps: - - name: Checkout Library + # Step 1: Check out the repository + - name: Checkout Repository uses: actions/checkout@v4 with: path: head submodules: true - - name: Run Kani Script - run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head + # Step 2: Run Kani on the std library (default configuration) + - name: Run Kani Verification + run: head/scripts/run-kani.sh --path ${{github.workspace}}/head + + test-kani-script: + name: Test Kani script + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + include: + - os: ubuntu-latest + base: ubuntu + - os: macos-latest + base: macos + steps: + # Step 1: Check out the repository + - name: Checkout Repository + uses: actions/checkout@v4 + with: + path: head + submodules: true + + # Step 2: Test Kani verification script with specific arguments + - name: Test Kani script (Custom Args) + run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse + + # Step 3: Test Kani verification script in the repository directory + - 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 diff --git a/.gitignore b/.gitignore index 41f6d2a5e3c36..5bfc180d4d58e 100644 --- a/.gitignore +++ b/.gitignore @@ -19,6 +19,7 @@ Session.vim ## Build /book/ /build/ +/kani_build/ /target library/target *.rlib diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh deleted file mode 100644 index c93499cb7a398..0000000000000 --- a/scripts/check_kani.sh +++ /dev/null @@ -1,55 +0,0 @@ -#!/bin/bash - -set -e - -# Set the working directories -VERIFY_RUST_STD_DIR="$1" -KANI_DIR=$(mktemp -d) - -RUNNER_TEMP=$(mktemp -d) - -# Get the OS name -os_name=$(uname -s) - -# Checkout your local repository -echo "Checking out local repository..." -echo -cd "$VERIFY_RUST_STD_DIR" - -# Checkout the Kani repository -echo "Checking out Kani repository..." -echo -git clone --depth 1 -b features/verify-rust-std https://github.com/model-checking/kani.git "$KANI_DIR" - -# Check the OS and -# Setup dependencies for Kani -echo "Setting up dependencies for Kani..." -echo -cd "$KANI_DIR" -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 - -# Build Kani -echo "Building Kani..." -echo -cargo build-dev --release -# echo "$(pwd)/scripts" >> $PATH - -# Run tests -echo "Running tests..." -echo -cd "$VERIFY_RUST_STD_DIR" -$KANI_DIR/scripts/kani verify-std -Z unstable-options $VERIFY_RUST_STD_DIR/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates - -echo "Tests completed." -echo - -# Clean up the Kani directory (optional) -rm -rf "$KANI_DIR" -rm -rf "$RUNNER_TEMP" -# rm -rf "$VERIFY_RUST_STD_DIR" diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh new file mode 100755 index 0000000000000..8ce27dac5d207 --- /dev/null +++ b/scripts/run-kani.sh @@ -0,0 +1,196 @@ +#!/bin/bash + +set -e + +usage() { + echo "Usage: $0 [options] [-p ] [--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 " --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 +} + +# Initialize variables +command_args="" +path="" + +# Parse command line arguments +# TODO: Improve parsing with getopts +while [[ $# -gt 0 ]]; do + case $1 in + -h|--help) + usage + ;; + -p|--path) + if [[ -n $2 ]]; then + path=$2 + shift 2 + else + echo "Error: Path argument is missing" + usage + fi + ;; + --kani-args) + shift + command_args="$@" + break + ;; + *) + break + ;; + esac +done + +# Set working directory +if [[ -n "$path" ]]; then + if [[ ! -d "$path" ]]; then + echo "Error: Specified directory does not exist." + usage + fi + WORK_DIR=$(realpath "$path") +else + WORK_DIR=$(pwd) +fi + +cd "$WORK_DIR" + +# Default values +DEFAULT_TOML_FILE="tool_config/kani-version.toml" +DEFAULT_REPO_URL="https://github.com/model-checking/kani.git" +DEFAULT_BRANCH_NAME="features/verify-rust-std" + +# Use environment variables if set, otherwise use defaults +TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE} +REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL} +BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME} + +# Function to read commit ID from TOML file +read_commit_from_toml() { + local file="$1" + if [[ ! -f "$file" ]]; then + echo "Error: TOML file not found: $file" >&2 + exit 1 + fi + local commit=$(grep '^commit *=' "$file" | sed 's/^commit *= *"\(.*\)"/\1/') + if [[ -z "$commit" ]]; then + echo "Error: 'commit' field not found in TOML file" >&2 + exit 1 + fi + echo "$commit" +} + +clone_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 +} + +get_current_commit() { + local directory="$1" + if [ -d "$directory/.git" ]; then + git -C "$directory" rev-parse HEAD + else + echo "" + fi +} + +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 + else + echo "Unknown operating system" + fi + + git submodule update --init --recursive + cargo build-dev --release + popd +} + +get_kani_path() { + local build_dir="$1" + echo "$(realpath "$build_dir/scripts/kani")" +} + +run_kani_command() { + local kani_path="$1" + shift + "$kani_path" "$@" +} + +# Check if binary exists and is up to date +check_binary_exists() { + local build_dir="$1" + local expected_commit="$2" + local kani_path=$(get_kani_path "$build_dir") + + if [[ -f "$kani_path" ]]; then + local current_commit=$(get_current_commit "$build_dir") + if [[ "$current_commit" = "$expected_commit" ]]; then + return 0 + fi + 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" + + # Read commit ID from TOML file + commit=$(read_commit_from_toml "$TOML_FILE") + + # Check if binary already exists and is up to date + if check_binary_exists "$build_dir" "$commit"; then + echo "Kani binary is up to date. Skipping build." + 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" + + # Build project + build_kani "$build_dir" + + echo "Kani build completed successfully!" + fi + + # Get the path to the Kani executable + kani_path=$(get_kani_path "$build_dir") + echo "Kani executable path: $kani_path" + + 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 --output-format=terse $command_args +} + +main + +cleanup() +{ + rm -rf "$temp_dir_target" +} + +trap cleanup EXIT diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml new file mode 100644 index 0000000000000..59b19da6a5958 --- /dev/null +++ b/tool_config/kani-version.toml @@ -0,0 +1,5 @@ +# This version should be updated whenever there is a change that makes this version of kani +# incomaptible with the verify-std repo. + +[kani] +commit = "5f8f513d297827cfdce4c48065e51973ba563068" From c4a1f45edbe3987fc8c9513c6d424039d6ef8e86 Mon Sep 17 00:00:00 2001 From: Lanfei Ma <99311320+lanfeima@users.noreply.github.com> Date: Fri, 25 Oct 2024 17:46:41 -0700 Subject: [PATCH 6/6] Harnesses for carrying_mul (#114) ## Towards: Issue #59 ### Parent branch: main --- ### Changes - Added macros for generating `carrying_mul` harnesses - Added harnesses for `carrying_mul` for the following integer types: - `u8`, `u16`, `u32`, `u64` --------- Co-authored-by: yew005 Co-authored-by: MWDZ Co-authored-by: Yenyun035 Co-authored-by: Rajath Co-authored-by: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com> --- library/core/src/num/mod.rs | 84 +++++++++++++++++++++++++++++++++++-- 1 file changed, 80 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index b123d998a8466..d039ffb7056f6 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1657,6 +1657,51 @@ mod verify { } } } + + /// A macro to generate Kani proof harnesses for the `carrying_mul` method, + /// + /// The macro creates multiple harnesses for different ranges of input values, + /// allowing testing of both small and large inputs. + /// + /// # Parameters: + /// - `$type`: The integer type (e.g., u8, u16) for which the `carrying_mul` function is being tested. + /// - `$wide_type`: A wider type to simulate the multiplication (e.g., u16 for u8, u32 for u16). + /// - `$harness_name`: The name of the Kani harness to be generated. + /// - `$min`: The minimum value for the range of inputs for `lhs`, `rhs`, and `carry_in`. + /// - `$max`: The maximum value for the range of inputs for `lhs`, `rhs`, and `carry_in`. + macro_rules! generate_carrying_mul_intervals { + ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => { + $( + #[kani::proof] + pub fn $harness_name() { + let lhs: $type = kani::any::<$type>(); + let rhs: $type = kani::any::<$type>(); + let carry_in: $type = kani::any::<$type>(); + + kani::assume(lhs >= $min && lhs <= $max); + kani::assume(rhs >= $min && rhs <= $max); + kani::assume(carry_in >= $min && carry_in <= $max); + + // Perform the carrying multiplication + let (result, carry_out) = lhs.carrying_mul(rhs, carry_in); + + // Manually compute the expected result and carry using wider type + let wide_result = (lhs as $wide_type) + .wrapping_mul(rhs as $wide_type) + .wrapping_add(carry_in as $wide_type); + + let expected_result = wide_result as $type; + let expected_carry = (wide_result >> <$type>::BITS) as $type; + + // Assert the result and carry are correct + assert_eq!(result, expected_result); + assert_eq!(carry_out, expected_carry); + } + )+ + } + } + + // Part 2 : Nested unsafe functions Generation Macros --> https://github.com/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md @@ -1741,7 +1786,7 @@ mod verify { generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128); generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize); - // unchecked_mul proofs + // `unchecked_mul` proofs // // Target types: // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total, with different interval checks for each. @@ -1892,8 +1937,37 @@ mod verify { generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128); generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize); + + // Part_2 `carrying_mul` proofs + // + // ====================== u8 Harnesses ====================== + /// Kani proof harness for `carrying_mul` on `u8` type with full range of values. + generate_carrying_mul_intervals!(u8, u16, + carrying_mul_u8_full_range, 0u8, u8::MAX + ); + + // ====================== u16 Harnesses ====================== + /// Kani proof harness for `carrying_mul` on `u16` type with full range of values. + generate_carrying_mul_intervals!(u16, u32, + carrying_mul_u16_full_range, 0u16, u16::MAX + ); + + // ====================== u32 Harnesses ====================== + generate_carrying_mul_intervals!(u32, u64, + carrying_mul_u32_small, 0u32, 10u32, + carrying_mul_u32_large, u32::MAX - 10u32, u32::MAX, + carrying_mul_u32_mid_edge, (u32::MAX / 2) - 10u32, (u32::MAX / 2) + 10u32 + ); + + // ====================== u64 Harnesses ====================== + generate_carrying_mul_intervals!(u64, u128, + carrying_mul_u64_small, 0u64, 10u64, + carrying_mul_u64_large, u64::MAX - 10u64, u64::MAX, + carrying_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64 + ); + - // Part 2 : Proof harnesses + // Part_2 `widening_mul` proofs // ====================== u8 Harnesses ====================== generate_widening_mul_intervals!(u8, u16, widening_mul_u8, 0u8, u8::MAX); @@ -1919,7 +1993,7 @@ mod verify { widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64 ); - // `wrapping_shl` proofs + // Part_2 `wrapping_shl` proofs // // Target types: // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total @@ -1944,7 +2018,7 @@ mod verify { generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128); generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize); - // `wrapping_shr` proofs + // Part_2 `wrapping_shr` proofs // // Target types: // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total @@ -1967,4 +2041,6 @@ mod verify { generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64); generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); + } +