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/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. 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/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index c84087172974a..4ff7f97542d93 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 @@ -2190,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 91c1ccb708613..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 @@ -1687,6 +1732,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: @@ -1728,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. @@ -1879,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); @@ -1905,4 +1992,55 @@ mod verify { widening_mul_u64_large, u64::MAX - 10u64, u64::MAX, widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64 ); + + // 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 + // + // 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); + + // 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 + // + // 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 0576e087935bb..3220be1d86f30 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 @@ -2171,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 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 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"