From ca725a73c81ee72c4b6c800bfdb71d5642d3a0c7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Jan 2025 22:57:55 +0100 Subject: [PATCH 1/9] Fix challenge 15 (SIMD) link and title (#240) The move from 14 to 15 wasn't entirely complete. 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 +- doc/src/challenges/0015-intrinsics-simd.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 01f9459dd5944..8073d12bf1f66 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -26,4 +26,4 @@ - [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) - - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0014-intrinsics-simd.md) + - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md) diff --git a/doc/src/challenges/0015-intrinsics-simd.md b/doc/src/challenges/0015-intrinsics-simd.md index fc97ff1840e54..1fa995f85a90a 100644 --- a/doc/src/challenges/0015-intrinsics-simd.md +++ b/doc/src/challenges/0015-intrinsics-simd.md @@ -1,4 +1,4 @@ -# Challenge 14: Contracts and Tests for SIMD Intrinsics +# Challenge 15: Contracts and Tests for SIMD Intrinsics - **Status:** Open - **Reward:** From 01e49769cfe20db89e4eeee9c0cbcbc5681bff3e Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 27 Jan 2025 17:48:45 +0000 Subject: [PATCH 2/9] Update Kani Metrics (#241) This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. --------- Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro --- scripts/kani-std-analysis/metrics-data.json | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json index 75a71c0301483..9113075d9e401 100644 --- a/scripts/kani-std-analysis/metrics-data.json +++ b/scripts/kani-std-analysis/metrics-data.json @@ -12,6 +12,19 @@ "safe_fns_under_contract": 77, "verified_safe_fns_under_contract": 77, "total_functions_under_contract": 224 + }, + { + "date": "2025-01-26", + "total_unsafe_fns": 6987, + "total_safe_abstractions": 1704, + "total_safe_fns": 14666, + "unsafe_fns_under_contract": 144, + "verified_unsafe_fns_under_contract": 132, + "safe_abstractions_under_contract": 41, + "verified_safe_abstractions_under_contract": 41, + "safe_fns_under_contract": 77, + "verified_safe_fns_under_contract": 77, + "total_functions_under_contract": 224 } ] -} \ No newline at end of file +} From 566cd1371c3b0bbd3da001ab591bb65524b1c10d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Wed, 29 Jan 2025 20:46:57 +0000 Subject: [PATCH 3/9] Goto-transcoder action (#236) Resolves #108 This PR enables the use of goto-transcoder for the following contracts: ``` core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_mul_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_mul_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shl_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shl_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shr_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_shr_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_sub_i8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_sub_u8.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_add_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_mul_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_mul_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shl_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_shr_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_i64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u16.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u32.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify25checked_unchecked_sub_u64.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_add_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_add_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shl_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shl_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shr_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_shr_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_sub_i128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify26checked_unchecked_sub_u128.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_add_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_add_usize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shl_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shl_usize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shr_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_shr_usize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_sub_isize.out core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify27checked_unchecked_sub_usize.out ``` The version of ESBMC used contains the following solvers: - Boolector (default) - Z3 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/goto-transcoder.yml | 37 ++++++++++++ .gitignore | 2 + doc/src/tools.md | 1 + doc/src/tools/goto-transcoder.md | 85 +++++++++++++++++++++++++++ scripts/run-goto-transcoder.sh | 52 ++++++++++++++++ 5 files changed, 177 insertions(+) create mode 100644 .github/workflows/goto-transcoder.yml create mode 100644 doc/src/tools/goto-transcoder.md create mode 100755 scripts/run-goto-transcoder.sh diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml new file mode 100644 index 0000000000000..7272f2d657a0f --- /dev/null +++ b/.github/workflows/goto-transcoder.yml @@ -0,0 +1,37 @@ +# This workflow executes the supported contracts in goto-transcoder + +name: Run GOTO Transcoder (ESBMC) +on: + workflow_dispatch: + merge_group: + pull_request: + branches: [ main ] + push: + paths: + - 'library/**' + - '.github/workflows/goto-transcoder.yml' + - 'scripts/run-kani.sh' + - 'scripts/run-goto-transcoder.sh' + +defaults: + run: + shell: bash + +jobs: + verify-rust-std: + name: Verify contracts with goto-transcoder + runs-on: ubuntu-latest + steps: + # Step 1: Check out the repository + - name: Checkout Repository + uses: actions/checkout@v4 + with: + submodules: true + + # Step 2: Generate contracts programs + - name: Generate contracts + run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts + + # Step 3: Run goto-transcoder + - name: Run goto-transcoder + run: ./scripts/run-goto-transcoder.sh kani/contracts checked_unchecked.*.out diff --git a/.gitignore b/.gitignore index a3cdde9bde1ac..4bafa69269a57 100644 --- a/.gitignore +++ b/.gitignore @@ -48,6 +48,8 @@ package-lock.json ## Kani *.out +## GOTO-Transcoder +goto-transcoder # Added by cargo # # already existing elements were commented out diff --git a/doc/src/tools.md b/doc/src/tools.md index 0eaba7c40d4d8..cb5ebababb1ee 100644 --- a/doc/src/tools.md +++ b/doc/src/tools.md @@ -12,6 +12,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section. | Tool | CI Status | |---------------------|-------| | Kani Rust Verifier | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml) | + | GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml) | diff --git a/doc/src/tools/goto-transcoder.md b/doc/src/tools/goto-transcoder.md new file mode 100644 index 0000000000000..7ddfdf59a5d96 --- /dev/null +++ b/doc/src/tools/goto-transcoder.md @@ -0,0 +1,85 @@ +# GOTO-Transcoder (ESBMC) + +The [goto-transcoder](https://github.com/rafaelsamenezes/goto-transcoder) is an initiative to add a compatibility layer between GOTO programs generated from CPROVER tools (e.g., CBMC and goto-instrument). Specifically, it adds a compatibility layer between Kani and [ESBMC](https://github.com/esbmc/esbmc). ESBMC has a few differences to CBMC, including: +- CBMC focuses on SAT-based encodings of unrolled programs, while ESBMC targets SMT-based encodings. The SMT support of ESBMC includes sending the full formula or using incremental-SMT. +- CBMC's concurrency support is an entirely symbolic encoding of a concurrent program in one SAT formula, while ESBMC explores each interleaving individually using context-bounded verification. +- ESBMC implements incremental-BMC and k-induction strategies. + + +To install the tool, you may just download the source code and build it with `cargo build`. +For ESBMC, we recommend using [this release](https://github.com/esbmc/esbmc/releases/tag/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241). + +Additionally, we also depend on Kani to generate the GOTO files. You can find more information about how to install in [the installation section of the Kani book](https://model-checking.github.io/kani/install-guide.html). + +# Steps to Use the Tool + +For these steps let's verify a Rust hello world, we will assume that you have Kani available in your system. We will start with +the Hello World from the [Kani tutorial](https://model-checking.github.io/kani/kani-tutorial.html): + +```rust +// File: test.rs +#[kani::proof] +fn main() { + assert!(1 == 2); +} +``` + +## Use Kani to generate the CBMC GOTO program + +Invoke Kani and ask it to keep the intermediate files: `kani test.rs --keep-temps`. This generates a `.out` file that is in the GBF +format. We can double-check this by invoking it with CBMC: `cbmc *test4main.out --show-goto-functions`: + +``` +[...] +main /* _RNvCshu9GRFEWjwO_4test4main */ + // 12 file test.rs line 3 column 10 function main + DECL _RNvCshu9GRFEWjwO_4test4main::1::var_0 : struct tag-Unit + // 13 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 9 function main + DECL _RNvCshu9GRFEWjwO_4test4main::1::var_1 : struct tag-Unit + // 14 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 22 function main + DECL _RNvCshu9GRFEWjwO_4test4main::1::var_2 : c_bool[8] +[...] +``` + +## Convert the CBMC goto into ESBMC goto + +1. Clone goto-transcoder: `git clone https://github.com/rafaelsamenezes/goto-transcoder.git` +2. Convert to the ESBMC file: `cargo run cbmc2esbmc .out .goto` + +``` +Running: goto-transcoder file.cbmc.out _RNvCshu9GRFEWjwO_4test4main file.esbmc.goto +[2024-10-09T13:07:20Z INFO gototranscoder] Converting CBMC input into ESBMC +[2024-10-09T13:07:20Z INFO gototranscoder] Done +``` + +This will generate the `file.esbmc.goto`, which can be used as the ESBMC input. + +## Invoke ESBMC + +1. Invoke ESBMC with the program: `esbmc --binary file.esbmc.goto`. + +``` +Solving with solver Z3 v4.13.0 +Runtime decision procedure: 0.001s +Building error trace + +[Counterexample] + + +State 1 file test.rs line 4 column 5 function main thread 0 +---------------------------------------------------- +Violated property: + file test.rs line 4 column 5 function main + KANI_CHECK_ID_test.cbacc14fa409fc10::test_0 + 0 + + +VERIFICATION FAILED +``` + + +## Using GOTO-Transcoder to verify the Rust Standard Library + +1. Follow the same procedure for Kani to add new properties. +2. Run Kani with the following extra args: `--keep-temps --only-codegen`. +3. You can then run each contract individually. diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh new file mode 100755 index 0000000000000..a29dfbd34b492 --- /dev/null +++ b/scripts/run-goto-transcoder.sh @@ -0,0 +1,52 @@ +#!/bin/bash + +set -e + +############## +# PARAMETERS # +############## +contract_folder=$1/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps +supported_regex=$2 +unsupported_regex=neg + +goto_transcoder_git=https://github.com/rafaelsamenezes/goto-transcoder +esbmc_url=https://github.com/esbmc/esbmc/releases/download/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241/esbmc-linux.zip + +########## +# SCRIPT # +########## + +echo "Checking contracts with goto-transcoder" + +if [ ! -d "goto-transcoder" ]; then + echo "goto-transcoder not found. Downloading..." + git clone $goto_transcoder_git + cd goto-transcoder + wget $esbmc_url + unzip esbmc-linux.zip + chmod +x ./linux-release/bin/esbmc + cd .. +fi + +ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > ./goto-transcoder/_contracts.txt + +cd goto-transcoder +while IFS= read -r line; do + # I expect each line to be similar to 'core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out' + # The entrypoint of the contract would be _RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8 + # So we use awk to extract this name. + contract=`echo "$line" | awk '{match($0, /(_RNv.*).out/, arr); print arr[1]}'` + echo "Processing: $contract" + if [[ -z "$contract" ]]; then + continue + fi + if echo "$contract" | grep -q "$unsupported_regex"; then + continue + fi + echo "Running: goto-transcoder $contract $contract_folder/$line $contract.esbmc.goto" + cargo run cbmc2esbmc $contract ../$contract_folder/$line $contract.esbmc.goto + ./linux-release/bin/esbmc --binary $contract.esbmc.goto +done < "_contracts.txt" + +rm "_contracts.txt" +cd .. From 5699f3ca2b71f52e482bd21ceac46f0e53934ff4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Tue, 4 Feb 2025 21:40:06 +0000 Subject: [PATCH 4/9] Add goto-transcoder.md into summary (#243) The goto-transcoder is not appearing in the book pages. This should fix it. --- doc/src/SUMMARY.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 8073d12bf1f66..86b93dea01dba 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -8,6 +8,7 @@ - [Verification Tools](./tools.md) - [Kani](./tools/kani.md) + - [GOTO Transcoder](./tools/goto-transcoder.md) --- From db8e5a729bb434eca9c93dd4f8b34279af506740 Mon Sep 17 00:00:00 2001 From: Alex Le Blanc <83725365+AlexLB99@users.noreply.github.com> Date: Tue, 4 Feb 2025 17:12:17 -0500 Subject: [PATCH 5/9] transmute_unchecked contracts and harnesses (#185) This is a draft pull request towards solving #19. ## Changes - Added wrappers for `transmute_unchecked()` - Annotated these wrappers with contracts - Wrote harnesses that verify these wrappers Note: the reason we write wrappers for `transmute_unchecked()` and we annotate those wrappers is that function contracts do not appear to be currently supported for compiler intrinsics (as discussed in [#3345](https://github.com/model-checking/kani/issues/3345)). Also, rather than using a single wrapper for `transmute_unchecked()`, we write several with different constraints on the input (since leaving the function parameters completely generic severely restricts what we can do in the contracts, e.g., testing for equality). This is not intended to be a complete solution for verifying `transmute_unchecked()`, but instead a proof of concept to see how aligned this is with the expected solution. Any feedback would be greatly appreciated -- thank you! 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: AlexLB99 --- library/core/src/intrinsics/mod.rs | 100 +++++++++++++++++++++++++++++ 1 file changed, 100 insertions(+) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 29ef19daaf679..4063cdadca8cc 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4642,6 +4642,106 @@ mod verify { let dst = if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) }; unsafe { copy_nonoverlapping(src, dst, kani::any()) } } + + //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does + //not currently support contracts (https://github.com/model-checking/kani/issues/3345) + #[requires(crate::mem::size_of::() == crate::mem::size_of::())] //T and U have same size (transmute_unchecked does not guarantee this) + #[requires(ub_checks::can_dereference(&input as *const T as *const U))] //output can be deref'd as value of type U + #[allow(dead_code)] + unsafe fn transmute_unchecked_wrapper(input: T) -> U { + unsafe { transmute_unchecked(input) } + } + + //generates harness that transmutes arbitrary values of input type to output type + //use when you expect all resulting bit patterns of output type to be valid + macro_rules! transmute_unchecked_should_succeed { + ($harness:ident, $src:ty, $dst:ty) => { + #[kani::proof_for_contract(transmute_unchecked_wrapper)] + fn $harness() { + let src: $src = kani::any(); + let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; + } + }; + } + + //generates harness that transmutes arbitrary values of input type to output type + //use when you expect some resulting bit patterns of output type to be invalid + macro_rules! transmute_unchecked_should_fail { + ($harness:ident, $src:ty, $dst:ty) => { + #[kani::proof] + #[kani::stub_verified(transmute_unchecked_wrapper)] + #[kani::should_panic] + fn $harness() { + let src: $src = kani::any(); + let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; + } + }; + } + + //transmute between the 4-byte numerical types + transmute_unchecked_should_succeed!(transmute_unchecked_i32_to_u32, i32, u32); + transmute_unchecked_should_succeed!(transmute_unchecked_u32_to_i32, u32, i32); + transmute_unchecked_should_succeed!(transmute_unchecked_i32_to_f32, i32, f32); + transmute_unchecked_should_succeed!(transmute_unchecked_f32_to_i32, f32, i32); + transmute_unchecked_should_succeed!(transmute_unchecked_u32_to_f32, u32, f32); + transmute_unchecked_should_succeed!(transmute_unchecked_f32_to_u32, f32, u32); + //transmute between the 8-byte numerical types + transmute_unchecked_should_succeed!(transmute_unchecked_i64_to_u64, i64, u64); + transmute_unchecked_should_succeed!(transmute_unchecked_u64_to_i64, u64, i64); + transmute_unchecked_should_succeed!(transmute_unchecked_i64_to_f64, i64, f64); + transmute_unchecked_should_succeed!(transmute_unchecked_f64_to_i64, f64, i64); + transmute_unchecked_should_succeed!(transmute_unchecked_u64_to_f64, u64, f64); + transmute_unchecked_should_succeed!(transmute_unchecked_f64_to_u64, f64, u64); + //transmute between arrays of bytes and numerical types + transmute_unchecked_should_succeed!(transmute_unchecked_arr_to_u32, [u8; 4], u32); + transmute_unchecked_should_succeed!(transmute_unchecked_u32_to_arr, u32, [u8; 4]); + transmute_unchecked_should_succeed!(transmute_unchecked_arr_to_u64, [u8; 8], u64); + transmute_unchecked_should_succeed!(transmute_unchecked_u64_to_arr, u64, [u8; 8]); + //transmute to type with potentially invalid bit patterns + transmute_unchecked_should_fail!(transmute_unchecked_u8_to_bool, u8, bool); + transmute_unchecked_should_fail!(transmute_unchecked_u32_to_char, u32, char); + + //tests that transmute works correctly when transmuting something with zero size + #[kani::proof_for_contract(transmute_unchecked_wrapper)] + fn transmute_zero_size() { + let empty_arr: [u8;0] = []; + let unit_val: () = unsafe { transmute_unchecked_wrapper(empty_arr) }; + assert!(unit_val == ()); + } + + //generates harness that transmutes arbitrary values two ways + //i.e. (src -> dest) then (dest -> src) + //We then check that the output is equal to the input + //This tests that transmute does not mutate the bit patterns + //Note: this would not catch reversible mutations + //e.g., deterministically flipping a bit + macro_rules! transmute_unchecked_two_ways { + ($harness:ident, $src:ty, $dst:ty) => { + #[kani::proof_for_contract(transmute_unchecked_wrapper)] + fn $harness() { + let src: $src = kani::any(); + let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; + let src2: $src = unsafe { transmute_unchecked_wrapper(dst) }; + assert_eq!(src,src2); + } + }; + } + + //transmute 2-ways between the 4-byte numerical types + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i32_to_u32, i32, u32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u32_to_i32, u32, i32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i32_to_f32, i32, f32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u32_to_f32, u32, f32); + //transmute 2-ways between the 8-byte numerical types + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i64_to_u64, i64, u64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u64_to_i64, u64, i64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i64_to_f64, i64, f64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u64_to_f64, u64, f64); + //transmute 2-ways between arrays of bytes and numerical types + transmute_unchecked_two_ways!(transmute_unchecked_2ways_arr_to_u32, [u8; 4], u32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u32_to_arr, u32, [u8; 4]); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_arr_to_u64, [u8; 8], u64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u64_to_arr, u64, [u8; 8]); // FIXME: Enable this harness once is fixed. // Harness triggers a spurious failure when writing 0 bytes to an invalid memory location, From a2c90fd955b2bb41ace3f20879cef0ef8bbe3b3a Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Wed, 5 Feb 2025 00:27:31 +0000 Subject: [PATCH 6/9] Update Kani Metrics (#244) This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com> Co-authored-by: Carolyn Zech --- scripts/kani-std-analysis/metrics-data.json | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json index 9113075d9e401..faae5ae14baf1 100644 --- a/scripts/kani-std-analysis/metrics-data.json +++ b/scripts/kani-std-analysis/metrics-data.json @@ -25,6 +25,19 @@ "safe_fns_under_contract": 77, "verified_safe_fns_under_contract": 77, "total_functions_under_contract": 224 + }, + { + "date": "2025-02-02", + "total_unsafe_fns": 6987, + "total_safe_abstractions": 1704, + "total_safe_fns": 14666, + "unsafe_fns_under_contract": 144, + "verified_unsafe_fns_under_contract": 132, + "safe_abstractions_under_contract": 41, + "verified_safe_abstractions_under_contract": 41, + "safe_fns_under_contract": 77, + "verified_safe_fns_under_contract": 77, + "total_functions_under_contract": 224 } ] -} +} \ No newline at end of file From e2146fa08efabf089bab45eb6eb54926d64d32a9 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 10 Feb 2025 13:52:01 -0500 Subject: [PATCH 7/9] Update Kani Metrics (#245) This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com> --- scripts/kani-std-analysis/metrics-data.json | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json index faae5ae14baf1..d1180922a842f 100644 --- a/scripts/kani-std-analysis/metrics-data.json +++ b/scripts/kani-std-analysis/metrics-data.json @@ -38,6 +38,19 @@ "safe_fns_under_contract": 77, "verified_safe_fns_under_contract": 77, "total_functions_under_contract": 224 + }, + { + "date": "2025-02-09", + "total_unsafe_fns": 6987, + "total_safe_abstractions": 1704, + "total_safe_fns": 14666, + "unsafe_fns_under_contract": 144, + "verified_unsafe_fns_under_contract": 132, + "safe_abstractions_under_contract": 41, + "verified_safe_abstractions_under_contract": 41, + "safe_fns_under_contract": 77, + "verified_safe_fns_under_contract": 77, + "total_functions_under_contract": 225 } ] } \ No newline at end of file From ff0b5bfe953a90dff3a5c5ef77871562b4a0dc63 Mon Sep 17 00:00:00 2001 From: "Shoyu Vanilla (Flint)" Date: Wed, 12 Feb 2025 04:38:58 +0900 Subject: [PATCH 8/9] Add harnesses for safety of primitive conversions (#233) Towards #220 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/convert/num.rs | 337 ++++++++++++++++++++++++++++++++ 1 file changed, 337 insertions(+) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 0246d0627cafe..38200a73b775f 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -1,4 +1,10 @@ +use safety::requires; + +#[cfg(kani)] +use crate::kani; use crate::num::TryFromIntError; +#[allow(unused_imports)] +use crate::ub_checks::float_to_int_in_range; mod private { /// This trait being unreachable from outside the crate @@ -25,6 +31,9 @@ macro_rules! impl_float_to_int { #[unstable(feature = "convert_float_to_int", issue = "67057")] impl FloatToInt<$Int> for $Float { #[inline] + #[requires( + self.is_finite() && float_to_int_in_range::<$Float, $Int>(self) + )] 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) } @@ -540,3 +549,331 @@ 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); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Generate harnesses for `NonZero::::from(NonZero)`. + macro_rules! generate_nonzero_int_from_nonzero_int_harness { + ($Small:ty => $Large:ty, $harness:ident) => { + #[kani::proof] + pub fn $harness() { + let x: NonZero<$Small> = kani::any(); + let _ = NonZero::<$Large>::from(x); + } + }; + } + + // This bundles the calls to `generate_nonzero_int_from_nonzero_int_harness` + // macro into segregated namespaces for better organization and usability. + macro_rules! generate_nonzero_int_from_nonzero_int_harnesses { + ($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => { + mod $ns { + use super::*; + + $( + mod $Large { + use super::*; + + generate_nonzero_int_from_nonzero_int_harness!( + $Small => $Large, + check_nonzero_int_from_nonzero_int + ); + } + )+ + } + }; + } + + // non-zero unsigned integer -> non-zero integer, infallible + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u8, + u8 => u16, u32, u64, u128, usize, i16, i32, i64, i128, isize, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u16, + u16 => u32, u64, u128, usize, i32, i64, i128, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u32, + u32 => u64, u128, i64, i128, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u64, + u64 => u128, i128, + ); + + // non-zero signed integer -> non-zero signed integer, infallible + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i8, + i8 => i16, i32, i64, i128, isize, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i16, + i16 => i32, i64, i128, isize, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i32, + i32 => i64, i128, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i64, + i64 => i128, + ); + + // Generates harnesses for `NonZero::::try_from(NonZero)`. + // Since the function may be fallible or infallible depending on `source` and `target`, + // this macro supports generating both cases. + macro_rules! generate_nonzero_int_try_from_nonzero_int_harness { + // Passing two identities - one for pass and one for panic - generates harnesses + // for fallible cases. + ($source:ty => $target:ty, $harness_pass:ident, $harness_panic:ident $(,)?) => { + #[kani::proof] + pub fn $harness_pass() { + let x_inner: $source = kani::any_where(|&v| { + (v > 0 && (v as u128) <= (<$target>::MAX as u128)) + || (v < 0 && (v as i128) >= (<$target>::MIN as i128)) + }); + let x = NonZero::new(x_inner).unwrap(); + let _ = NonZero::<$target>::try_from(x).unwrap(); + } + + #[kani::proof] + #[kani::should_panic] + pub fn $harness_panic() { + let x_inner: $source = kani::any_where(|&v| { + (v > 0 && (v as u128) > (<$target>::MAX as u128)) + || (v < 0 && (v as i128) < (<$target>::MIN as i128)) + || (v == 0) + }); + let x = NonZero::new(x_inner).unwrap(); + let _ = NonZero::<$target>::try_from(x).unwrap(); + } + }; + // Passing a single identity generates harnesses for infallible cases. + ($source:ty => $target:ty, $harness_infallible:ident $(,)?) => { + #[kani::proof] + pub fn $harness_infallible() { + let x: NonZero<$source> = kani::any(); + let _ = NonZero::<$target>::try_from(x).unwrap(); + } + }; + } + + // This bundles the calls to `generate_nonzero_int_try_from_nonzero_int_harness` + // macro into segregated namespaces for better organization and usability. + // Conversions from the source type to the target types inside the first pair + // of square brackets are fallible, while those to the second pairs are + // infallible. + macro_rules! generate_nonzero_int_try_from_nonzero_int_harnesses { + ($ns:ident, $source:ty => ([$($target:tt),* $(,)?], [$($infallible:tt),* $(,)?] $(,)?)) => { + mod $ns { + use super::*; + + $( + mod $target { + use super::*; + + generate_nonzero_int_try_from_nonzero_int_harness!( + $source => $target, + check_nonzero_int_try_from_nonzero_int, + check_nonzero_int_try_from_nonzero_int_should_panic, + ); + } + )* + $( + mod $infallible { + use super::*; + + generate_nonzero_int_try_from_nonzero_int_harness!( + $source => $infallible, + check_nonzero_int_try_from_nonzero_int_infallible, + ); + } + )* + } + }; + } + + // unsigned non-zero integer -> non-zero integer fallible + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u16, + u16 => ( + [u8, i8, i16], + [isize], + ) + ); + + #[cfg(target_pointer_width = "16")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u16, + u16 => ( + [u8, i8, i16, isize], + [], + ) + ); + + #[cfg(target_pointer_width = "64")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u32, + u32 => ( + [u8, u16, i8, i16, i32], + [usize, isize], + ) + ); + + #[cfg(target_pointer_width = "32")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u32, + u32 => ( + [u8, u16, i8, i16, i32, isize], + [usize], + ) + ); + + #[cfg(target_pointer_width = "16")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u32, + u32 => ( + [u8, u16, usize, i8, i16, i32, isize], + [], + ) + ); + + #[cfg(target_pointer_width = "64")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u64, + u64 => ( + [u8, u16, u32, i8, i16, i32, i64, isize], + [usize], + ) + ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u64, + u64 => ( + [u8, u16, u32, usize, i8, i16, i32, i64, isize], + [], + ) + ); + + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u128, + u128 => ( + [u8, u16, u32, u64, usize, i8, i16, i32, i64, i128, isize], + [], + ) + ); + + // signed non-zero integer -> non-zero integer fallible + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i8, + i8 => ( + [u8, u16, u32, u64, u128, usize], + [], + ) + ); + + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i16, + i16 => ( + [u8, u16, u32, u64, u128, usize, i8], + [], + ) + ); + + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i32, + i32 => ( + [u8, u16, u32, u64, u128, usize, i8, i16], + [isize], + ) + ); + + #[cfg(target_pointer_width = "16")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i32, + i32 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, isize], + [], + ) + ); + + #[cfg(target_pointer_width = "64")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i64, + i64 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, i32], + [isize], + ) + ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i64, + i64 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, i32, isize], + [], + ) + ); + + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i128, + i128 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, isize], + [], + ) + ); + + // Generate harnesses for `>::to_int_unchecked(self)`. + macro_rules! generate_float_to_int_harness { + ($Float:ty => $Int:ty, $harness:ident) => { + #[kani::proof_for_contract(<$Float>::to_int_unchecked)] + pub fn $harness() { + let x: $Float = kani::any(); + let _: $Int = unsafe { x.to_int_unchecked() }; + } + }; + } + + // This bundles the calls to `generate_float_to_int_harness` macro into segregated + // namespaces for better organization and usability. + macro_rules! generate_float_to_int_harnesses { + ($ns:ident, $(($Float:tt => $($Int:tt),+ $(,)?)),+ $(,)?) => { + mod $ns { + use super::*; + + $( + mod $Float { + use super::*; + + $( + mod $Int { + use super::*; + + generate_float_to_int_harness!( + $Float => $Int, + check_float_to_int_unchecked + ); + } + )+ + } + )+ + } + }; + } + + // float -> integer unchecked + generate_float_to_int_harnesses!( + check_f16_to_int_unchecked, + (f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + (f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + (f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + (f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + ); +} From 10424a1677b53b6d6fcb83a570f6e3c44c848c4a Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 17 Feb 2025 20:11:58 +0000 Subject: [PATCH 9/9] Update Kani Metrics (#246) This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com> --- scripts/kani-std-analysis/metrics-data.json | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json index d1180922a842f..be1695d367d94 100644 --- a/scripts/kani-std-analysis/metrics-data.json +++ b/scripts/kani-std-analysis/metrics-data.json @@ -51,6 +51,19 @@ "safe_fns_under_contract": 77, "verified_safe_fns_under_contract": 77, "total_functions_under_contract": 225 + }, + { + "date": "2025-02-16", + "total_unsafe_fns": 6987, + "total_safe_abstractions": 1704, + "total_safe_fns": 14666, + "unsafe_fns_under_contract": 192, + "verified_unsafe_fns_under_contract": 132, + "safe_abstractions_under_contract": 41, + "verified_safe_abstractions_under_contract": 41, + "safe_fns_under_contract": 77, + "verified_safe_fns_under_contract": 77, + "total_functions_under_contract": 273 } ] } \ No newline at end of file