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/SUMMARY.md b/doc/src/SUMMARY.md index 01f9459dd5944..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) --- @@ -26,4 +27,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:** 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/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), + ); +} 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, diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json index 75a71c0301483..be1695d367d94 100644 --- a/scripts/kani-std-analysis/metrics-data.json +++ b/scripts/kani-std-analysis/metrics-data.json @@ -12,6 +12,58 @@ "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 + }, + { + "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 + }, + { + "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 + }, + { + "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 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 ..