From 107daa7c36fdf2341ac972fd7bfba39f26ff786b Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Mon, 8 Jul 2024 17:02:54 -0400 Subject: [PATCH 1/6] CI: Allow use of `node16` for release jobs (#3322) actions/checkout@v3 is causing trouble in the `BuildBundle-Linux` workflow as described in #3321 . This PR sets `ACTIONS_ALLOW_USE_UNSECURE_NODE_VERSION: true` to continue using `node16` so we don't find issues with `node20` dependencies in `ubuntu-18.04` jobs. This is the option recommended in this GitHub post: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/ Resolves #3321 --- .github/workflows/release.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index f7fbf32cc3eb..2097a9e8f5f3 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -16,6 +16,7 @@ on: env: RUST_BACKTRACE: 1 + ACTIONS_ALLOW_USE_UNSECURE_NODE_VERSION: true jobs: build_bundle_macos: From 53b702d90c8db2df5666ecb3cc1584ba77b7e585 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 8 Jul 2024 23:40:41 +0200 Subject: [PATCH 2/6] Auto-upload macOS ARM binaries to draft release (#3320) In #3266 a job to build macOS ARM binaries was added, but the artifacts weren't yet propagated to the release. This PR adds this missing step. --- .github/workflows/release.yml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 2097a9e8f5f3..9fb35033d2d1 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -323,7 +323,7 @@ jobs: if: ${{ github.event_name == 'push' && startsWith(github.ref, 'refs/tags/kani-') }} name: Release runs-on: ubuntu-20.04 - needs: [build_bundle_macos, build_bundle_linux, test_bundle, test_alt_platform] + needs: [build_bundle_macos, build_bundle_macos_aarch64, build_bundle_linux, test_bundle, test_alt_platform] permissions: contents: write outputs: @@ -355,6 +355,11 @@ jobs: with: name: ${{ needs.build_bundle_macos.outputs.bundle }} + - name: Download MacOS ARM bundle + uses: actions/download-artifact@v3 + with: + name: ${{ needs.build_bundle_macos_aarch64.outputs.bundle }} + - name: Download Linux bundle uses: actions/download-artifact@v3 with: @@ -368,7 +373,7 @@ jobs: with: name: kani-${{ env.TAG_VERSION }} tag: kani-${{ env.TAG_VERSION }} - artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }}" + artifacts: "${{ needs.build_bundle_linux.outputs.bundle }},${{ needs.build_bundle_macos.outputs.bundle }},${{ needs.build_bundle_macos_aarch64.outputs.bundle }}" body: | Kani Rust verifier release bundle version ${{ env.TAG_VERSION }}. draft: true From 34820bd8473b80f99c7863cb9f8780ad464a2687 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 9 Jul 2024 09:27:07 -0400 Subject: [PATCH 3/6] Bump tests/perf/s2n-quic from `37335c1` to `cd20ac1` (#3330) --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 37335c196fb5..cd20ac16f5e4 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 37335c196fb5755dcbe2532e5a3820e46906d5ea +Subproject commit cd20ac16f5e4477238164074d2ed5b94ca8ba4fd From 923346c5cedd1a96619fc49dec385bd5c1c9a8db Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Tue, 9 Jul 2024 09:03:16 -0700 Subject: [PATCH 4/6] Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked (#3332) This PR introduces layout checks for types to instrument mutable pointer casts. If two types have incompatible padding (e.g. a padding byte in one is a data byte in the other or vice-versa), an "unsupported check" assertion is inserted. This overapproximates for soundness, since the casts do not cause UB themselves, but an alternative solution involves tracking every MIR place, which is costly. Resolves #3324 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../transform/check_uninit/uninit_visitor.rs | 70 +++++++++++++++++-- .../uninit/access-padding-via-cast/expected | 2 +- .../expected/uninit/delayed-ub/delayed-ub.rs | 14 ++++ tests/expected/uninit/delayed-ub/expected | 5 ++ 4 files changed, 83 insertions(+), 8 deletions(-) create mode 100644 tests/expected/uninit/delayed-ub/delayed-ub.rs create mode 100644 tests/expected/uninit/delayed-ub/expected diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs index 19b13c6ab8b6..0614724be6bf 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs @@ -12,9 +12,11 @@ use stable_mir::mir::{ NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }; -use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, TyKind, UintTy}; +use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, Ty, TyKind, UintTy}; use strum_macros::AsRefStr; +use super::{PointeeInfo, PointeeLayout}; + /// Memory initialization operations: set or get memory initialization state for a given pointer. #[derive(AsRefStr, Clone, Debug)] pub enum MemoryInitOp { @@ -540,13 +542,34 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { - if let Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), _, ty) = rvalue { - if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { - if pointee_ty.kind().is_trait() { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), - }); + if let Rvalue::Cast(cast_kind, operand, ty) = rvalue { + match cast_kind { + CastKind::PointerCoercion(PointerCoercion::Unsize) => { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), + }); + } + } } + CastKind::PtrToPtr => { + let operand_ty = operand.ty(&self.locals).unwrap(); + if let ( + RigidTy::RawPtr(from_ty, Mutability::Mut), + RigidTy::RawPtr(to_ty, Mutability::Mut), + ) = (operand_ty.kind().rigid().unwrap(), ty.kind().rigid().unwrap()) + { + if !tys_layout_compatible(from_ty, to_ty) { + // If casting from a mutable pointer to a mutable pointer with + // different layouts, delayed UB could occur. + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.".to_string(), + }); + } + } + } + _ => {} } }; self.super_rvalue(rvalue, location); @@ -711,3 +734,36 @@ fn try_resolve_instance(locals: &[LocalDecl], func: &Operand) -> Result bool { + // Retrieve layouts to assess compatibility. + let from_ty_info = PointeeInfo::from_ty(*from_ty); + let to_ty_info = PointeeInfo::from_ty(*to_ty); + if let (Ok(from_ty_info), Ok(to_ty_info)) = (from_ty_info, to_ty_info) { + let from_ty_layout = match from_ty_info.layout() { + PointeeLayout::Sized { layout } => layout, + PointeeLayout::Slice { element_layout } => element_layout, + PointeeLayout::TraitObject => return false, + }; + let to_ty_layout = match to_ty_info.layout() { + PointeeLayout::Sized { layout } => layout, + PointeeLayout::Slice { element_layout } => element_layout, + PointeeLayout::TraitObject => return false, + }; + // Ensure `to_ty_layout` does not have a larger size. + if to_ty_layout.len() <= from_ty_layout.len() { + // Check data and padding bytes pair-wise. + if from_ty_layout.iter().zip(to_ty_layout.iter()).all( + |(from_ty_layout_byte, to_ty_layout_byte)| { + // Make sure all data and padding bytes match. + from_ty_layout_byte == to_ty_layout_byte + }, + ) { + return true; + } + } + }; + false +} diff --git a/tests/expected/uninit/access-padding-via-cast/expected b/tests/expected/uninit/access-padding-via-cast/expected index 12c5c0a4a439..e02883b26cdf 100644 --- a/tests/expected/uninit/access-padding-via-cast/expected +++ b/tests/expected/uninit/access-padding-via-cast/expected @@ -1,4 +1,4 @@ -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut [u8; 4]` +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. VERIFICATION:- FAILED diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs new file mode 100644 index 000000000000..bfed0a1f39a1 --- /dev/null +++ b/tests/expected/uninit/delayed-ub/delayed-ub.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z ghost-state -Z uninit-checks + +/// Checks that Kani rejects mutable pointer casts between types of different padding. +#[kani::proof] +fn invalid_value() { + unsafe { + let mut value: u128 = 0; + let ptr = &mut value as *mut _ as *mut (u8, u32, u64); + *ptr = (4, 4, 4); // This assignment itself does not cause UB... + let c: u128 = value; // ...but this reads a padding value! + } +} diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected new file mode 100644 index 000000000000..e02883b26cdf --- /dev/null +++ b/tests/expected/uninit/delayed-ub/expected @@ -0,0 +1,5 @@ +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + +VERIFICATION:- FAILED + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. \ No newline at end of file From 3b4042ca701c4ae232263748e97a80511873c80c Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 9 Jul 2024 19:08:35 +0000 Subject: [PATCH 5/6] Automatic cargo update to 2024-07-08 (#3329) Dependency upgrade resulting from `cargo update`. --- Cargo.lock | 74 +++++++++++++++++++++++++++--------------------------- 1 file changed, 37 insertions(+), 37 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index cf47e75b0562..fd76b5e75b43 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -169,7 +169,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.68", + "syn 2.0.69", ] [[package]] @@ -482,7 +482,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.68", + "syn 2.0.69", ] [[package]] @@ -909,29 +909,29 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.203" +version = "1.0.204" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7253ab4de971e72fb7be983802300c30b5a7f0c2e56fab8abfc6a214307c0094" +checksum = "bc76f558e0cbb2a839d37354c575f1dc3fdc6546b5be373ba43d95f231bf7c12" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.203" +version = "1.0.204" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba" +checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222" dependencies = [ "proc-macro2", "quote", - "syn 2.0.68", + "syn 2.0.69", ] [[package]] name = "serde_json" -version = "1.0.119" +version = "1.0.120" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e8eddb61f0697cc3989c5d64b452f5488e2b8a60fd7d5076a3045076ffef8cb0" +checksum = "4e0d21c9a8cae1235ad58a00c11cb40d4b1e5c784f1ef2c537876ed6ffd8b7c5" dependencies = [ "itoa", "ryu", @@ -1030,7 +1030,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.68", + "syn 2.0.69", ] [[package]] @@ -1045,9 +1045,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.68" +version = "2.0.69" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "901fa70d88b9d6c98022e23b4136f9f3e54e4662c3bc1bd1d84a42a9a0f0c1e9" +checksum = "201fcda3845c23e8212cd466bfebf0bd20694490fc0356ae8e428e0824a915a6" dependencies = [ "proc-macro2", "quote", @@ -1083,7 +1083,7 @@ checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533" dependencies = [ "proc-macro2", "quote", - "syn 2.0.68", + "syn 2.0.69", ] [[package]] @@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.68", + "syn 2.0.69", ] [[package]] @@ -1320,9 +1320,9 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb" +checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ "windows_aarch64_gnullvm", "windows_aarch64_msvc", @@ -1336,51 +1336,51 @@ dependencies = [ [[package]] name = "windows_aarch64_gnullvm" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263" +checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" [[package]] name = "windows_aarch64_msvc" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6" +checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" [[package]] name = "windows_i686_gnu" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670" +checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" [[package]] name = "windows_i686_gnullvm" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9" +checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" [[package]] name = "windows_i686_msvc" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf" +checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" [[package]] name = "windows_x86_64_gnu" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9" +checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" [[package]] name = "windows_x86_64_gnullvm" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596" +checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" [[package]] name = "windows_x86_64_msvc" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0" +checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" @@ -1399,20 +1399,20 @@ checksum = "d135d17ab770252ad95e9a872d365cf3090e3be864a34ab46f48555993efc904" [[package]] name = "zerocopy" -version = "0.7.34" +version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae87e3fcd617500e5d106f0380cf7b77f3c6092aae37191433159dda23cfb087" +checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" dependencies = [ "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.7.34" +version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b" +checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.68", + "syn 2.0.69", ] From 068f63cc32ab638b039ef29e1fb061559efe14d6 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 12 Jul 2024 09:01:32 -0700 Subject: [PATCH 6/6] Improve performance and language support of memory initialization checks (#3313) This is a follow-up PR for #3264, a part of the larger work towards #3300. This PR introduces: - Use of demonic non-determinism (prophecy variables) to improve memory initialization checks performance; - Instead of keeping track of memory initialization of each possibly uninitialized byte pointed to by some pointer, one is chosen non-deterministically; - Tests for proper memory initialization checks injection for compiler intrinsics; - Separate functions for checking memory initialization of slice chunks. 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .../codegen_cprover_gotoc/codegen/contract.rs | 2 +- .../codegen_cprover_gotoc/overrides/hooks.rs | 36 +++ .../src/kani_middle/transform/body.rs | 21 +- .../kani_middle/transform/check_uninit/mod.rs | 161 ++++++++-- .../transform/check_uninit/uninit_visitor.rs | 169 +++++----- .../kani_middle/transform/kani_intrinsics.rs | 6 +- .../src/kani_middle/transform/mod.rs | 8 +- kani-driver/src/call_single_file.rs | 5 +- library/kani/src/lib.rs | 24 ++ library/kani/src/mem.rs | 18 +- library/kani/src/mem_init.rs | 288 +++++++++++++----- library/kani_core/src/lib.rs | 24 ++ library/kani_core/src/mem.rs | 19 +- .../access-padding-uninit.rs | 2 +- .../access-padding-via-cast.rs | 2 +- .../uninit/alloc-to-slice/alloc-to-slice.rs | 4 +- tests/expected/uninit/atomic/atomic.rs | 31 ++ tests/expected/uninit/atomic/expected | 13 + tests/expected/uninit/intrinsics/expected | 70 +++++ .../expected/uninit/intrinsics/intrinsics.rs | 127 ++++++++ .../vec-read-bad-len/vec-read-bad-len.rs | 2 +- .../vec-read-semi-init/vec-read-semi-init.rs | 2 +- .../uninit/vec-read-uninit/vec-read-uninit.rs | 2 +- .../access-padding-enum-diverging-variants.rs | 2 +- .../access-padding-enum-multiple-variants.rs | 2 +- .../access-padding-enum-single-field.rs | 2 +- .../access-padding-enum-single-variant.rs | 2 +- tests/kani/Uninit/access-padding-init.rs | 15 + tests/kani/Uninit/alloc-to-slice.rs | 19 ++ tests/kani/Uninit/alloc-zeroed-to-slice.rs | 22 ++ tests/kani/Uninit/atomic.rs | 66 ++++ .../Uninit/struct-padding-and-arr-init.rs | 21 ++ tests/kani/Uninit/vec-read-init.rs | 11 + tests/perf/uninit/Cargo.toml | 14 - tests/perf/uninit/expected | 1 - tests/perf/uninit/src/lib.rs | 68 ----- tests/std-checks/core/slice.expected | 2 +- tests/std-checks/core/src/slice.rs | 20 +- 38 files changed, 1013 insertions(+), 290 deletions(-) create mode 100644 tests/expected/uninit/atomic/atomic.rs create mode 100644 tests/expected/uninit/atomic/expected create mode 100644 tests/expected/uninit/intrinsics/expected create mode 100644 tests/expected/uninit/intrinsics/intrinsics.rs create mode 100644 tests/kani/Uninit/access-padding-init.rs create mode 100644 tests/kani/Uninit/alloc-to-slice.rs create mode 100644 tests/kani/Uninit/alloc-zeroed-to-slice.rs create mode 100644 tests/kani/Uninit/atomic.rs create mode 100644 tests/kani/Uninit/struct-padding-and-arr-init.rs create mode 100644 tests/kani/Uninit/vec-read-init.rs delete mode 100644 tests/perf/uninit/Cargo.toml delete mode 100644 tests/perf/uninit/expected delete mode 100644 tests/perf/uninit/src/lib.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index d35015aa040d..c7e7d5b817bd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -122,7 +122,7 @@ impl<'tcx> GotocCtx<'tcx> { .tcx .all_diagnostic_items(()) .name_to_id - .get(&rustc_span::symbol::Symbol::intern("KaniMemInitShadowMem")) + .get(&rustc_span::symbol::Symbol::intern("KaniMemoryInitializationState")) .map(|attr_id| { self.tcx .symbol_name(rustc_middle::ty::Instance::mono(self.tcx, *attr_id)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index fc245fc6f4c9..c0df279932f6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -143,6 +143,41 @@ impl GotocHook for Assert { } } +struct Check; +impl GotocHook for Check { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniCheck") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let cond = fargs.remove(0).cast_to(Type::bool()); + let msg = fargs.remove(0); + let msg = gcx.extract_const_message(&msg).unwrap(); + let target = target.unwrap(); + let caller_loc = gcx.codegen_caller_span_stable(span); + + let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); + + Stmt::block( + vec![ + reach_stmt, + gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } +} + struct Nondet; impl GotocHook for Nondet { @@ -510,6 +545,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(Panic), Rc::new(Assume), Rc::new(Assert), + Rc::new(Check), Rc::new(Cover), Rc::new(Nondet), Rc::new(IsAllocated), diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 22895bd8d20d..d82dda80cc05 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -387,12 +387,13 @@ pub enum CheckType { } impl CheckType { - /// This will create the type of check that is available in the current crate. + /// This will create the type of check that is available in the current crate, attempting to + /// create a check that generates an assertion following by an assumption of the same assertion. /// /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return /// [CheckType::Panic]. - pub fn new(tcx: TyCtxt) -> CheckType { + pub fn new_assert_assume(tcx: TyCtxt) -> CheckType { if let Some(instance) = find_instance(tcx, "KaniAssert") { CheckType::Assert(instance) } else if find_instance(tcx, "panic_str").is_some() { @@ -401,6 +402,22 @@ impl CheckType { CheckType::NoCore } } + + /// This will create the type of check that is available in the current crate, attempting to + /// create a check that generates an assertion, without assuming the condition afterwards. + /// + /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will + /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return + /// [CheckType::Panic]. + pub fn new_assert(tcx: TyCtxt) -> CheckType { + if let Some(instance) = find_instance(tcx, "KaniCheck") { + CheckType::Assert(instance) + } else if find_instance(tcx, "panic_str").is_some() { + CheckType::Panic + } else { + CheckType::NoCore + } + } } /// We store the index of an instruction to avoid borrow checker issues and unnecessary copies. diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 6665ab697287..e1b265751fd5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -29,8 +29,17 @@ mod uninit_visitor; pub use ty_layout::{PointeeInfo, PointeeLayout}; use uninit_visitor::{CheckUninitVisitor, InitRelevantInstruction, MemoryInitOp}; -const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = - &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"]; +// Function bodies of those functions will not be instrumented as not to cause infinite recursion. +const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] = &[ + "KaniIsPtrInitialized", + "KaniSetPtrInitialized", + "KaniIsSliceChunkPtrInitialized", + "KaniSetSliceChunkPtrInitialized", + "KaniIsSlicePtrInitialized", + "KaniSetSlicePtrInitialized", + "KaniIsStrPtrInitialized", + "KaniSetStrPtrInitialized", +]; /// Instrument the code with checks for uninitialized memory. #[derive(Debug)] @@ -59,8 +68,8 @@ impl TransformPass for UninitPass { fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "transform"); - // Need to break infinite recursion when shadow memory checks are inserted, - // so the internal function responsible for shadow memory checks are skipped. + // Need to break infinite recursion when memory initialization checks are inserted, so the + // internal functions responsible for memory initialization are skipped. if tcx .get_diagnostic_name(rustc_internal::internal(tcx, instance.def.def_id())) .map(|diagnostic_name| { @@ -74,6 +83,11 @@ impl TransformPass for UninitPass { let mut new_body = MutableBody::from(body); let orig_len = new_body.blocks().len(); + // Inject a call to set-up memory initialization state if the function is a harness. + if is_harness(instance, tcx) { + inject_memory_init_setup(&mut new_body, tcx, &mut self.mem_init_fn_cache); + } + // Set of basic block indices for which analyzing first statement should be skipped. // // This is necessary because some checks are inserted before the source instruction, which, in @@ -159,10 +173,12 @@ impl UninitPass { }; match operation { - MemoryInitOp::Check { .. } => { + MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Check { .. } => { self.build_get_and_check(tcx, body, source, operation, pointee_ty_info, skip_first) } - MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => { + MemoryInitOp::SetSliceChunk { .. } + | MemoryInitOp::Set { .. } + | MemoryInitOp::SetRef { .. } => { self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first) } MemoryInitOp::Unsupported { .. } => { @@ -171,8 +187,8 @@ impl UninitPass { } } - /// Inject a load from shadow memory tracking memory initialization and an assertion that all - /// non-padding bytes are initialized. + /// Inject a load from memory initialization state and an assertion that all non-padding bytes + /// are initialized. fn build_get_and_check( &mut self, tcx: TyCtxt, @@ -189,18 +205,34 @@ impl UninitPass { let ptr_operand = operation.mk_operand(body, source); match pointee_info.layout() { PointeeLayout::Sized { layout } => { + let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); + // Depending on whether accessing the known number of elements in the slice, need to + // pass is as an argument. + let (diagnostic, args) = match &operation { + MemoryInitOp::Check { .. } => { + let diagnostic = "KaniIsPtrInitialized"; + let args = vec![ptr_operand.clone(), layout_operand]; + (diagnostic, args) + } + MemoryInitOp::CheckSliceChunk { .. } => { + let diagnostic = "KaniIsSliceChunkPtrInitialized"; + let args = + vec![ptr_operand.clone(), layout_operand, operation.expect_count()]; + (diagnostic, args) + } + _ => unreachable!(), + }; let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, "KaniIsPtrInitialized", &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); collect_skipped(&operation, body, skip_first); body.add_call( &is_ptr_initialized_instance, source, operation.position(), - vec![ptr_operand.clone(), layout_operand, operation.expect_count()], + args, ret_place.clone(), ); } @@ -252,8 +284,8 @@ impl UninitPass { ) } - /// Inject a store into shadow memory tracking memory initialization to initialize or - /// deinitialize all non-padding bytes. + /// Inject a store into memory initialization state to initialize or deinitialize all + /// non-padding bytes. fn build_set( &mut self, tcx: TyCtxt, @@ -272,27 +304,50 @@ impl UninitPass { match pointee_info.layout() { PointeeLayout::Sized { layout } => { + let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); + // Depending on whether writing to the known number of elements in the slice, need to + // pass is as an argument. + let (diagnostic, args) = match &operation { + MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => { + let diagnostic = "KaniSetPtrInitialized"; + let args = vec![ + ptr_operand, + layout_operand, + Operand::Constant(ConstOperand { + span: source.span(body.blocks()), + user_ty: None, + const_: MirConst::from_bool(value), + }), + ]; + (diagnostic, args) + } + MemoryInitOp::SetSliceChunk { .. } => { + let diagnostic = "KaniSetSliceChunkPtrInitialized"; + let args = vec![ + ptr_operand, + layout_operand, + operation.expect_count(), + Operand::Constant(ConstOperand { + span: source.span(body.blocks()), + user_ty: None, + const_: MirConst::from_bool(value), + }), + ]; + (diagnostic, args) + } + _ => unreachable!(), + }; let set_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, "KaniSetPtrInitialized", &mut self.mem_init_fn_cache), + get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), layout.len(), *pointee_info.ty(), ); - let layout_operand = mk_layout_operand(body, source, operation.position(), &layout); collect_skipped(&operation, body, skip_first); body.add_call( &set_ptr_initialized_instance, source, operation.position(), - vec![ - ptr_operand, - layout_operand, - operation.expect_count(), - Operand::Constant(ConstOperand { - span: source.span(body.blocks()), - user_ty: None, - const_: MirConst::from_bool(value), - }), - ], + args, ret_place, ); } @@ -426,3 +481,59 @@ pub fn resolve_mem_init_fn(fn_def: FnDef, layout_size: usize, associated_type: T ) .unwrap() } + +/// Checks if the instance is a harness -- an entry point of Kani analysis. +fn is_harness(instance: Instance, tcx: TyCtxt) -> bool { + let harness_identifiers = [ + vec![ + rustc_span::symbol::Symbol::intern("kanitool"), + rustc_span::symbol::Symbol::intern("proof_for_contract"), + ], + vec![ + rustc_span::symbol::Symbol::intern("kanitool"), + rustc_span::symbol::Symbol::intern("proof"), + ], + ]; + harness_identifiers.iter().any(|attr_path| { + tcx.has_attrs_with_path(rustc_internal::internal(tcx, instance.def.def_id()), attr_path) + }) +} + +/// Inject an initial call to set-up memory initialization tracking. +fn inject_memory_init_setup( + new_body: &mut MutableBody, + tcx: TyCtxt, + mem_init_fn_cache: &mut HashMap<&'static str, FnDef>, +) { + // First statement or terminator in the harness. + let mut source = if !new_body.blocks()[0].statements.is_empty() { + SourceInstruction::Statement { idx: 0, bb: 0 } + } else { + SourceInstruction::Terminator { bb: 0 } + }; + + // Dummy return place. + let ret_place = Place { + local: new_body.new_local( + Ty::new_tuple(&[]), + source.span(new_body.blocks()), + Mutability::Not, + ), + projection: vec![], + }; + + // Resolve the instance and inject a call to set-up the memory initialization state. + let memory_initialization_init = Instance::resolve( + get_mem_init_fn_def(tcx, "KaniInitializeMemoryInitializationState", mem_init_fn_cache), + &GenericArgs(vec![]), + ) + .unwrap(); + + new_body.add_call( + &memory_initialization_init, + &mut source, + InsertPosition::Before, + vec![], + ret_place, + ); +} diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs index 0614724be6bf..f68869e6681d 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs @@ -8,11 +8,11 @@ use stable_mir::mir::alloc::GlobalAlloc; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::visit::{Location, PlaceContext}; use stable_mir::mir::{ - BasicBlockIdx, CastKind, ConstOperand, LocalDecl, MirVisitor, Mutability, - NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, - StatementKind, Terminator, TerminatorKind, + BasicBlockIdx, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand, + Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, + TerminatorKind, }; -use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, Ty, TyKind, UintTy}; +use stable_mir::ty::{ConstantKind, RigidTy, Ty, TyKind}; use strum_macros::AsRefStr; use super::{PointeeInfo, PointeeLayout}; @@ -20,15 +20,21 @@ use super::{PointeeInfo, PointeeLayout}; /// Memory initialization operations: set or get memory initialization state for a given pointer. #[derive(AsRefStr, Clone, Debug)] pub enum MemoryInitOp { + /// Check memory initialization of data bytes in a memory region starting from the pointer + /// `operand` and of length `sizeof(operand)` bytes. + Check { operand: Operand }, + /// Set memory initialization state of data bytes in a memory region starting from the pointer + /// `operand` and of length `sizeof(operand)` bytes. + Set { operand: Operand, value: bool, position: InsertPosition }, /// Check memory initialization of data bytes in a memory region starting from the pointer /// `operand` and of length `count * sizeof(operand)` bytes. - Check { operand: Operand, count: Operand }, + CheckSliceChunk { operand: Operand, count: Operand }, /// Set memory initialization state of data bytes in a memory region starting from the pointer /// `operand` and of length `count * sizeof(operand)` bytes. - Set { operand: Operand, count: Operand, value: bool, position: InsertPosition }, + SetSliceChunk { operand: Operand, count: Operand, value: bool, position: InsertPosition }, /// Set memory initialization of data bytes in a memory region starting from the reference to - /// `operand` and of length `count * sizeof(operand)` bytes. - SetRef { operand: Operand, count: Operand, value: bool, position: InsertPosition }, + /// `operand` and of length `sizeof(operand)` bytes. + SetRef { operand: Operand, value: bool, position: InsertPosition }, /// Unsupported memory initialization operation. Unsupported { reason: String }, } @@ -39,9 +45,10 @@ impl MemoryInitOp { /// `MemoryInitOp::SetRef`. pub fn mk_operand(&self, body: &mut MutableBody, source: &mut SourceInstruction) -> Operand { match self { - MemoryInitOp::Check { operand, .. } | MemoryInitOp::Set { operand, .. } => { - operand.clone() - } + MemoryInitOp::Check { operand, .. } + | MemoryInitOp::Set { operand, .. } + | MemoryInitOp::CheckSliceChunk { operand, .. } + | MemoryInitOp::SetSliceChunk { operand, .. } => operand.clone(), MemoryInitOp::SetRef { operand, .. } => Operand::Copy(Place { local: { let place = match operand { @@ -62,24 +69,34 @@ impl MemoryInitOp { pub fn expect_count(&self) -> Operand { match self { - MemoryInitOp::Check { count, .. } - | MemoryInitOp::Set { count, .. } - | MemoryInitOp::SetRef { count, .. } => count.clone(), - MemoryInitOp::Unsupported { .. } => unreachable!(), + MemoryInitOp::CheckSliceChunk { count, .. } + | MemoryInitOp::SetSliceChunk { count, .. } => count.clone(), + MemoryInitOp::Check { .. } + | MemoryInitOp::Set { .. } + | MemoryInitOp::SetRef { .. } + | MemoryInitOp::Unsupported { .. } => unreachable!(), } } pub fn expect_value(&self) -> bool { match self { - MemoryInitOp::Set { value, .. } | MemoryInitOp::SetRef { value, .. } => *value, - MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => unreachable!(), + MemoryInitOp::Set { value, .. } + | MemoryInitOp::SetSliceChunk { value, .. } + | MemoryInitOp::SetRef { value, .. } => *value, + MemoryInitOp::Check { .. } + | MemoryInitOp::CheckSliceChunk { .. } + | MemoryInitOp::Unsupported { .. } => unreachable!(), } } pub fn position(&self) -> InsertPosition { match self { - MemoryInitOp::Set { position, .. } | MemoryInitOp::SetRef { position, .. } => *position, - MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => InsertPosition::Before, + MemoryInitOp::Set { position, .. } + | MemoryInitOp::SetSliceChunk { position, .. } + | MemoryInitOp::SetRef { position, .. } => *position, + MemoryInitOp::Check { .. } + | MemoryInitOp::CheckSliceChunk { .. } + | MemoryInitOp::Unsupported { .. } => InsertPosition::Before, } } } @@ -158,12 +175,12 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { self.super_statement(stmt, location); // Source is a *const T and it must be initialized. - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: copy.src.clone(), count: copy.count.clone(), }); // Destimation is a *mut T so it gets initialized. - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: copy.dst.clone(), count: copy.count.clone(), value: true, @@ -188,7 +205,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { { self.push_target(MemoryInitOp::Check { operand: Operand::Copy(place_to_add_projections.clone()), - count: mk_const_operand(1, location.span()), }); }; } @@ -197,7 +213,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if place_without_deref.ty(&self.locals).unwrap().kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place_without_deref), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::After, }); @@ -208,7 +223,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if let Rvalue::AddressOf(..) = rvalue { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::After, }); @@ -219,7 +233,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { self.super_statement(stmt, location); self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), value: false, position: InsertPosition::After, }); @@ -263,8 +276,14 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { /* Intrinsics that can be safely skipped */ } name if name.starts_with("atomic") => { - let num_args = - if name.starts_with("atomic_cxchg") { 3 } else { 2 }; + let num_args = match name { + // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments. + name if name.starts_with("atomic_cxchg") => 3, + // All `atomic_load` intrinsics take `src` as an argument. + name if name.starts_with("atomic_load") => 1, + // All other `atomic` intrinsics take `dst, src` as arguments. + _ => 2, + }; assert_eq!( args.len(), num_args, @@ -276,7 +295,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Check { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), }); } "compare_bytes" => { @@ -293,11 +311,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { args[1].ty(self.locals).unwrap().kind(), TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) )); - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[0].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[1].clone(), count: args[2].clone(), }); @@ -318,11 +336,11 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { args[1].ty(self.locals).unwrap().kind(), TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) )); - self.push_target(MemoryInitOp::Check { + self.push_target(MemoryInitOp::CheckSliceChunk { operand: args[0].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: args[1].clone(), count: args[2].clone(), value: true, @@ -345,29 +363,12 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Check { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), }); self.push_target(MemoryInitOp::Check { operand: args[1].clone(), - count: mk_const_operand(1, location.span()), }); } - "unaligned_volatile_load" => { - assert_eq!( - args.len(), - 1, - "Unexpected number of arguments for `unaligned_volatile_load`" - ); - assert!(matches!( - args[0].ty(self.locals).unwrap().kind(), - TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) - )); - self.push_target(MemoryInitOp::Check { - operand: args[0].clone(), - count: mk_const_operand(1, location.span()), - }); - } - "volatile_load" => { + "volatile_load" | "unaligned_volatile_load" => { assert_eq!( args.len(), 1, @@ -379,7 +380,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Check { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), }); } "volatile_store" => { @@ -394,7 +394,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { )); self.push_target(MemoryInitOp::Set { operand: args[0].clone(), - count: mk_const_operand(1, location.span()), value: true, position: InsertPosition::After, }); @@ -409,7 +408,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { args[0].ty(self.locals).unwrap().kind(), TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) )); - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: args[0].clone(), count: args[2].clone(), value: true, @@ -432,7 +431,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } "alloc::alloc::__rust_alloc_zeroed" => { /* Memory is initialized here, need to update shadow memory. */ - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: Operand::Copy(destination.clone()), count: args[0].clone(), value: true, @@ -441,7 +440,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } "alloc::alloc::__rust_dealloc" => { /* Memory is uninitialized here, need to update shadow memory. */ - self.push_target(MemoryInitOp::Set { + self.push_target(MemoryInitOp::SetSliceChunk { operand: args[0].clone(), count: args[1].clone(), value: false, @@ -458,18 +457,30 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { TerminatorKind::Drop { place, .. } => { self.super_terminator(term, location); let place_ty = place.ty(&self.locals).unwrap(); - // When drop is codegen'ed, a reference is taken to the place which is later implicitly coerced to a pointer. - // Hence, we need to bless this pointer as initialized. - self.push_target(MemoryInitOp::SetRef { - operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), - value: true, - position: InsertPosition::Before, - }); + + // When drop is codegen'ed for types that could define their own dropping + // behavior, a reference is taken to the place which is later implicitly coerced + // to a pointer. Hence, we need to bless this pointer as initialized. + match place + .ty(&self.locals) + .unwrap() + .kind() + .rigid() + .expect("should be working with monomorphized code") + { + RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { + self.push_target(MemoryInitOp::SetRef { + operand: Operand::Copy(place.clone()), + value: true, + position: InsertPosition::Before, + }); + } + _ => {} + } + if place_ty.kind().is_raw_ptr() { self.push_target(MemoryInitOp::Set { operand: Operand::Copy(place.clone()), - count: mk_const_operand(1, location.span()), value: false, position: InsertPosition::After, }); @@ -497,7 +508,6 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if ptr_ty.kind().is_raw_ptr() { self.push_target(MemoryInitOp::Check { operand: Operand::Copy(intermediate_place.clone()), - count: mk_const_operand(1, location.span()), }); } } @@ -528,12 +538,14 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { if let ConstantKind::Allocated(allocation) = constant.const_.kind() { for (_, prov) in &allocation.provenance.ptrs { if let GlobalAlloc::Static(_) = GlobalAlloc::from(prov.0) { - self.push_target(MemoryInitOp::Set { - operand: Operand::Constant(constant.clone()), - count: mk_const_operand(1, location.span()), - value: true, - position: InsertPosition::Before, - }); + if constant.ty().kind().is_raw_ptr() { + // If a static is a raw pointer, need to mark it as initialized. + self.push_target(MemoryInitOp::Set { + operand: Operand::Constant(constant.clone()), + value: true, + position: InsertPosition::Before, + }); + } }; } } @@ -679,6 +691,12 @@ fn can_skip_intrinsic(intrinsic_name: &str) -> bool { /* SIMD operations */ true } + name if name.starts_with("atomic_fence") + || name.starts_with("atomic_singlethreadfence") => + { + /* Atomic fences */ + true + } "copy_nonoverlapping" => unreachable!( "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" ), @@ -705,15 +723,6 @@ fn can_skip_intrinsic(intrinsic_name: &str) -> bool { } } -/// Create a constant operand with a given value and span. -fn mk_const_operand(value: usize, span: Span) -> Operand { - Operand::Constant(ConstOperand { - span, - user_ty: None, - const_: MirConst::try_from_uint(value as u128, UintTy::Usize).unwrap(), - }) -} - /// Try removing a topmost deref projection from a place if it exists, returning a place without it. fn try_remove_topmost_deref(place: &Place) -> Option { let mut new_place = place.clone(); diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index ea7bf8625228..c4534bf11b4d 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -216,11 +216,7 @@ impl IntrinsicGeneratorPass { &is_ptr_initialized_instance, &mut terminator, InsertPosition::Before, - vec![ - Operand::Copy(Place::from(1)), - layout_operand, - Operand::Copy(Place::from(2)), - ], + vec![Operand::Copy(Place::from(1)), layout_operand], Place::from(ret_var), ); } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 56ab0be493c4..26a95978fcaf 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -60,7 +60,7 @@ impl BodyTransformation { inst_passes: vec![], cache: Default::default(), }; - let check_type = CheckType::new(tcx); + let check_type = CheckType::new_assert_assume(tcx); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); // This has to come after stubs since we want this to replace the stubbed body. @@ -73,7 +73,11 @@ impl BodyTransformation { // generated code for future instrumentation passes. transformer.add_pass( queries, - UninitPass { check_type: check_type.clone(), mem_init_fn_cache: HashMap::new() }, + UninitPass { + // Since this uses demonic non-determinism under the hood, should not assume the assertion. + check_type: CheckType::new_assert(tcx), + mem_init_fn_cache: HashMap::new(), + }, ); transformer.add_pass( queries, diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 7cbe150427e9..411dabb5270e 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -140,7 +140,10 @@ impl KaniSession { } if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) { - flags.push("--ub-check=uninit".into()) + // Automatically enable shadow memory, since the version of uninitialized memory checks + // without non-determinism depends on it. + flags.push("-Z ghost-state".into()); + flags.push("--ub-check=uninit".into()); } if self.args.ignore_locals_lifetime { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 6eab2a331811..7487cc26b186 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -123,6 +123,30 @@ pub const fn assert(cond: bool, msg: &'static str) { assert!(cond, "{}", msg); } +/// Creates an assertion of the specified condition, but does not assume it afterwards. +/// +/// # Example: +/// +/// ```rust +/// let x: bool = kani::any(); +/// let y = !x; +/// kani::check(x || y, "ORing a boolean variable with its negation must be true") +/// ``` +#[cfg(not(feature = "concrete_playback"))] +#[inline(never)] +#[rustc_diagnostic_item = "KaniCheck"] +pub const fn check(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; +} + +#[cfg(feature = "concrete_playback")] +#[inline(never)] +#[rustc_diagnostic_item = "KaniCheck"] +pub const fn check(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); +} + /// Creates a cover property with the specified condition and message. /// /// # Example: diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 0b390e74288d..f861f6b2ba25 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -118,9 +118,11 @@ where ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); + // Need to assert `is_initialized` because non-determinism is used under the hood, so it does + // not make sense to use it inside assumption context. metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -148,7 +150,11 @@ where ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); - is_inbounds(&metadata, thin_ptr) && is_initialized(ptr, 1) && unsafe { has_valid_value(ptr) } + // Need to assert `is_initialized` because non-determinism is used under the hood, so it does + // not make sense to use it inside assumption context. + is_inbounds(&metadata, thin_ptr) + && assert_is_initialized(ptr) + && unsafe { has_valid_value(ptr) } } /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. @@ -294,10 +300,16 @@ unsafe fn has_valid_value(_ptr: *const T) -> bool { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] -pub fn is_initialized(_ptr: *const T, _len: usize) -> bool { +pub fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() } +/// A helper to assert `is_initialized` to use it as a part of other predicates. +fn assert_is_initialized(ptr: *const T) -> bool { + crate::check(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); + true +} + /// Get the object ID of the given pointer. #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index 37832ea32604..a09e515d7e17 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -1,20 +1,23 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module uses shadow memory API to track memory initialization of raw pointers. +//! This module provides instrumentation for tracking memory initialization of raw pointers. //! //! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to -//! by raw pointers could be either initialized or uninitialized. Compiler automatically inserts -//! calls to `is_xxx_initialized` and `set_xxx_initialized` at appropriate locations to get or set -//! the initialization status of the memory pointed to. Padding bytes are always considered -//! uninitialized: type layout is determined at compile time and statically injected into the -//! program (see `Layout`). +//! by raw pointers could be either initialized or uninitialized. Padding bytes are always +//! considered uninitialized when read as data bytes. Each type has a type layout to specify which +//! bytes are considered to be data and which -- padding. This is determined at compile time and +//! statically injected into the program (see `Layout`). +//! +//! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at +//! appropriate locations to get or set the initialization status of the memory pointed to. +//! +//! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, +//! so calls to `is_xxx_initialized` should be only used in assertion contexts. // Definitions in this module are not meant to be visible to the end user, only the compiler. #![allow(dead_code)] -use crate::shadow::ShadowMem; - /// Bytewise mask, representing which bytes of a type are data and which are padding. /// For example, for a type like this: /// ``` @@ -25,98 +28,243 @@ use crate::shadow::ShadowMem; /// } /// ``` /// the layout would be [true, true, true, false]; -type Layout = [bool; N]; - -/// Global shadow memory object for tracking memory initialization. -#[rustc_diagnostic_item = "KaniMemInitShadowMem"] -static mut MEM_INIT_SHADOW_MEM: ShadowMem = ShadowMem::new(false); - -/// Get initialization state of `len` items laid out according to the `layout` starting at address `ptr`. -#[rustc_diagnostic_item = "KaniIsUnitPtrInitialized"] -fn is_unit_ptr_initialized(ptr: *const (), layout: Layout, len: usize) -> bool { - let mut count: usize = 0; - while count < len { - let mut offset: usize = 0; - while offset < N { - unsafe { - if layout[offset] - && !MEM_INIT_SHADOW_MEM.get((ptr as *const u8).add(count * N + offset)) - { - return false; - } - offset += 1; - } +type Layout = [bool; LAYOUT_SIZE]; + +/// Currently tracked non-deterministically chosen memory initialization state. +struct MemoryInitializationState { + pub tracked_object_id: usize, + pub tracked_offset: usize, + pub value: bool, +} + +impl MemoryInitializationState { + /// This is a dummy initialization function -- the values will be eventually overwritten by a + /// call to `initialize_memory_initialization_state`. + pub const fn new() -> Self { + Self { tracked_object_id: 0, tracked_offset: 0, value: false } + } + + /// Return currently tracked memory initialization state if `ptr` points to the currently + /// tracked object and the tracked offset lies within `LAYOUT_SIZE` bytes of `ptr`. Return + /// `true` otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn get( + &mut self, + ptr: *const u8, + layout: Layout, + ) -> bool { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + LAYOUT_SIZE + { + !layout[(self.tracked_offset - offset) % LAYOUT_SIZE] || self.value + } else { + true } - count += 1; } - true -} -/// Set initialization state to `value` for `len` items laid out according to the `layout` starting at address `ptr`. -#[rustc_diagnostic_item = "KaniSetUnitPtrInitialized"] -fn set_unit_ptr_initialized( - ptr: *const (), - layout: Layout, - len: usize, - value: bool, -) { - let mut count: usize = 0; - while count < len { - let mut offset: usize = 0; - while offset < N { - unsafe { - MEM_INIT_SHADOW_MEM - .set((ptr as *const u8).add(count * N + offset), value && layout[offset]); - } - offset += 1; + /// Set currently tracked memory initialization state if `ptr` points to the currently tracked + /// object and the tracked offset lies within `LAYOUT_SIZE` bytes of `ptr`. Do nothing + /// otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn set( + &mut self, + ptr: *const u8, + layout: Layout, + value: bool, + ) { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + LAYOUT_SIZE + { + self.value = layout[(self.tracked_offset - offset) % LAYOUT_SIZE] && value; + } + } + + /// Return currently tracked memory initialization state if `ptr` points to the currently + /// tracked object and the tracked offset lies within `LAYOUT_SIZE * num_elts` bytes of `ptr`. + /// Return `true` otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn get_slice( + &mut self, + ptr: *const u8, + layout: Layout, + num_elts: usize, + ) -> bool { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + num_elts * LAYOUT_SIZE + { + !layout[(self.tracked_offset - offset) % LAYOUT_SIZE] || self.value + } else { + true + } + } + + /// Set currently tracked memory initialization state if `ptr` points to the currently tracked + /// object and the tracked offset lies within `LAYOUT_SIZE * num_elts` bytes of `ptr`. Do + /// nothing otherwise. + /// + /// Such definition is necessary since both tracked object and tracked offset are chosen + /// non-deterministically. + pub fn set_slice( + &mut self, + ptr: *const u8, + layout: Layout, + num_elts: usize, + value: bool, + ) { + let obj = crate::mem::pointer_object(ptr); + let offset = crate::mem::pointer_offset(ptr); + if self.tracked_object_id == obj + && self.tracked_offset >= offset + && self.tracked_offset < offset + num_elts * LAYOUT_SIZE + { + self.value = layout[(self.tracked_offset - offset) % LAYOUT_SIZE] && value; } - count += 1; } } -/// Get initialization state of `len` items laid out according to the `layout` starting at address `ptr`. +/// Global object for tracking memory initialization state. +#[rustc_diagnostic_item = "KaniMemoryInitializationState"] +static mut MEM_INIT_STATE: MemoryInitializationState = MemoryInitializationState::new(); + +/// Set tracked object and tracked offset to a non-deterministic value. +#[rustc_diagnostic_item = "KaniInitializeMemoryInitializationState"] +fn initialize_memory_initialization_state() { + unsafe { + MEM_INIT_STATE.tracked_object_id = crate::any(); + MEM_INIT_STATE.tracked_offset = crate::any(); + MEM_INIT_STATE.value = false; + } +} + +/// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniIsPtrInitialized"] -fn is_ptr_initialized(ptr: *const T, layout: Layout, len: usize) -> bool { +fn is_ptr_initialized( + ptr: *const T, + layout: Layout, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } let (ptr, _) = ptr.to_raw_parts(); - is_unit_ptr_initialized(ptr, layout, len) + unsafe { MEM_INIT_STATE.get(ptr as *const u8, layout) } } -/// Set initialization state to `value` for `len` items laid out according to the `layout` starting at address `ptr`. +/// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniSetPtrInitialized"] -fn set_ptr_initialized( +fn set_ptr_initialized( + ptr: *const T, + layout: Layout, + value: bool, +) { + if LAYOUT_SIZE == 0 { + return; + } + let (ptr, _) = ptr.to_raw_parts(); + unsafe { + MEM_INIT_STATE.set(ptr as *const u8, layout, value); + } +} + +/// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[rustc_diagnostic_item = "KaniIsSliceChunkPtrInitialized"] +fn is_slice_chunk_ptr_initialized( + ptr: *const T, + layout: Layout, + num_elts: usize, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } + let (ptr, _) = ptr.to_raw_parts(); + unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) } +} + +/// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[rustc_diagnostic_item = "KaniSetSliceChunkPtrInitialized"] +fn set_slice_chunk_ptr_initialized( ptr: *const T, - layout: Layout, - len: usize, + layout: Layout, + num_elts: usize, value: bool, ) { + if LAYOUT_SIZE == 0 { + return; + } let (ptr, _) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, len, value); + unsafe { + MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); + } } /// Get initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniIsSlicePtrInitialized"] -fn is_slice_ptr_initialized(ptr: *const [T], layout: Layout) -> bool { - let (ptr, len) = ptr.to_raw_parts(); - is_unit_ptr_initialized(ptr, layout, len) +fn is_slice_ptr_initialized( + ptr: *const [T], + layout: Layout, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) } } /// Set initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`. #[rustc_diagnostic_item = "KaniSetSlicePtrInitialized"] -fn set_slice_ptr_initialized(ptr: *const [T], layout: Layout, value: bool) { - let (ptr, len) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, len, value); +fn set_slice_ptr_initialized( + ptr: *const [T], + layout: Layout, + value: bool, +) { + if LAYOUT_SIZE == 0 { + return; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { + MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); + } } /// Get initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr`. #[rustc_diagnostic_item = "KaniIsStrPtrInitialized"] -fn is_str_ptr_initialized(ptr: *const str, layout: Layout) -> bool { - let (ptr, len) = ptr.to_raw_parts(); - is_unit_ptr_initialized(ptr, layout, len) +fn is_str_ptr_initialized( + ptr: *const str, + layout: Layout, +) -> bool { + if LAYOUT_SIZE == 0 { + return true; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { MEM_INIT_STATE.get_slice(ptr as *const u8, layout, num_elts) } } /// Set initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`. #[rustc_diagnostic_item = "KaniSetStrPtrInitialized"] -fn set_str_ptr_initialized(ptr: *const str, layout: Layout, value: bool) { - let (ptr, len) = ptr.to_raw_parts(); - set_unit_ptr_initialized(ptr, layout, len, value); +fn set_str_ptr_initialized( + ptr: *const str, + layout: Layout, + value: bool, +) { + if LAYOUT_SIZE == 0 { + return; + } + let (ptr, num_elts) = ptr.to_raw_parts(); + unsafe { + MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); + } } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 143fbb7ef825..68a8e79658f1 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -124,6 +124,30 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } + /// Creates an assertion of the specified condition and message, but does not assume it afterwards. + /// + /// # Example: + /// + /// ```rust + /// let x: bool = kani::any(); + /// let y = !x; + /// kani::check(x || y, "ORing a boolean variable with its negation must be true") + /// ``` + #[cfg(not(feature = "concrete_playback"))] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + pub const fn check(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; + } + + #[cfg(feature = "concrete_playback")] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + pub const fn check(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); + } + /// Creates a cover property with the specified condition and message. /// /// # Example: diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 3b10856765a5..bcf4cd2248a6 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -123,9 +123,11 @@ macro_rules! kani_mem { ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); + // Need to assert `is_initialized` because non-determinism is used under the hood, so it + // does not make sense to use it inside assumption context. metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -154,8 +156,10 @@ macro_rules! kani_mem { ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); + // Need to assert `is_initialized` because non-determinism is used under the hood, so it + // does not make sense to use it inside assumption context. is_inbounds(&metadata, thin_ptr) - && is_initialized(ptr, 1) + && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -302,10 +306,19 @@ macro_rules! kani_mem { /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[rustc_diagnostic_item = "KaniIsInitialized"] #[inline(never)] - pub fn is_initialized(_ptr: *const T, _len: usize) -> bool { + pub fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() } + /// A helper to assert `is_initialized` to use it as a part of other predicates. + fn assert_is_initialized(ptr: *const T) -> bool { + super::check( + is_initialized(ptr), + "Undefined Behavior: Reading from an uninitialized pointer", + ); + true + } + /// Get the object ID of the given pointer. #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs index d6e735e219ad..8e65b95aefa2 100644 --- a/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr::addr_of; diff --git a/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs index b73bebc827bc..1604625fc54c 100644 --- a/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs +++ b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; #[repr(C)] diff --git a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs index 3c4420f5791f..318f234c31be 100644 --- a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs +++ b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks -use std::alloc::{alloc, dealloc, Layout}; +use std::alloc::{alloc, Layout}; use std::slice::from_raw_parts; /// Checks that Kani catches an attempt to form a slice from uninitialized memory. diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs new file mode 100644 index 000000000000..63c85af41a3f --- /dev/null +++ b/tests/expected/uninit/atomic/atomic.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +#![feature(core_intrinsics)] + +use std::alloc::{alloc, Layout}; +use std::sync::atomic::{AtomicU8, Ordering}; + +// Checks if memory initialization checks correctly fail when uninitialized memory is passed to +// atomic intrinsics. +#[kani::proof] +fn local_atomic_uninit() { + // Get a pointer to an uninitialized value + let layout = Layout::from_size_align(16, 8).unwrap(); + let ptr: *mut u8 = unsafe { alloc(layout) }; + // Try accessing `ptr` via atomic intrinsics, should be UB in each case. + unsafe { + match kani::any() { + 0 => { + std::intrinsics::atomic_store_relaxed(ptr, 1); + } + 1 => { + std::intrinsics::atomic_load_relaxed(ptr as *const u8); + } + _ => { + std::intrinsics::atomic_cxchg_relaxed_relaxed(ptr, 1, 1); + } + }; + } +} diff --git a/tests/expected/uninit/atomic/expected b/tests/expected/uninit/atomic/expected new file mode 100644 index 000000000000..c7d9593f22a7 --- /dev/null +++ b/tests/expected/uninit/atomic/expected @@ -0,0 +1,13 @@ +SUMMARY: + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +VERIFICATION:- FAILED + +Summary:\ +Verification failed for - local_atomic_uninit\ +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected new file mode 100644 index 000000000000..ffa98b6f1140 --- /dev/null +++ b/tests/expected/uninit/intrinsics/expected @@ -0,0 +1,70 @@ +Checking harness check_typed_swap_safe... + +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + +VERIFICATION:- FAILED + +Checking harness check_typed_swap... + +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8` + +VERIFICATION:- FAILED + +Checking harness check_volatile_store_and_load_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_volatile_load... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Checking harness check_write_bytes_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_compare_bytes_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_compare_bytes... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Checking harness check_copy_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Checking harness check_copy_nonoverlapping_safe... + +VERIFICATION:- SUCCESSFUL + +Checking harness check_copy_nonoverlapping... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +VERIFICATION:- FAILED + +Summary: +Verification failed for - check_typed_swap_safe +Verification failed for - check_typed_swap +Verification failed for - check_volatile_load +Verification failed for - check_compare_bytes +Verification failed for - check_copy +Verification failed for - check_copy_nonoverlapping +Complete - 5 successfully verified harnesses, 6 failures, 11 total. diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs new file mode 100644 index 000000000000..aa8a89b7b959 --- /dev/null +++ b/tests/expected/uninit/intrinsics/intrinsics.rs @@ -0,0 +1,127 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks +//! Checks that Kani supports memory initialization checks via intrinsics. + +#![feature(core_intrinsics)] + +use std::alloc::{alloc, alloc_zeroed, Layout}; +use std::intrinsics::*; + +#[kani::proof] +fn check_copy_nonoverlapping() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc(layout); + copy_nonoverlapping(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + } +} + +#[kani::proof] +fn check_copy_nonoverlapping_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc_zeroed(layout); + let dst: *mut u8 = alloc(layout); + // `src` is initialized here, `dst` is uninitialized, but it is fine since we are writing into it. + copy_nonoverlapping(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_copy() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc(layout); + copy(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + } +} + +#[kani::proof] +fn check_copy_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc_zeroed(layout); + let dst: *mut u8 = alloc(layout); + // `src` is initialized here, `dst` is uninitialized, but it is fine since we are writing into it. + copy(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_compare_bytes() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc(layout); + let right: *mut u8 = alloc(layout); + // ~ERROR: Accessing `left` and `right` here, both of which are uninitialized. + compare_bytes(left as *const u8, right as *const u8, 2); + } +} + +#[kani::proof] +fn check_compare_bytes_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc_zeroed(layout); + let right: *mut u8 = alloc_zeroed(layout); + // Both `left` and `right` are initialized here. + compare_bytes(left as *const u8, right as *const u8, 2); + } +} + +#[kani::proof] +fn check_write_bytes_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc(layout); + let right: *mut u8 = alloc(layout); + write_bytes(left, 0, 2); + write_bytes(right, 0, 2); + // Both `left` and `right` are initialized here. + compare_bytes(left as *const u8, right as *const u8, 2); + } +} + +#[kani::proof] +fn check_volatile_load() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + volatile_load(src as *const u8); // ~ERROR: Accessing `src` here, which is uninitialized. + } +} + +#[kani::proof] +fn check_volatile_store_and_load_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + volatile_store(src, 0); + volatile_load(src as *const u8); // `src` is initialized here. + } +} + +#[kani::proof] +fn check_typed_swap() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc(layout); + let right: *mut u8 = alloc(layout); + // ~ERROR: Accessing `left` and `right` here, both of which are uninitialized. + typed_swap(left, right); + } +} + +#[kani::proof] +fn check_typed_swap_safe() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let left: *mut u8 = alloc_zeroed(layout); + let right: *mut u8 = alloc_zeroed(layout); + // Both `left` and `right` are initialized here. + typed_swap(left, right); + } +} diff --git a/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs index 9778bb11a277..f5cae82c5350 100644 --- a/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs +++ b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ops::Index; diff --git a/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs index 4330f5f53023..2e007cabaced 100644 --- a/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs +++ b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks /// Checks that Kani catches an attempt to read uninitialized memory from a semi-initialized vector. #[kani::proof] diff --git a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs index c322b4d33bb2..e6daf80cd5e3 100644 --- a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs +++ b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks /// Checks that Kani catches an attempt to read uninitialized memory from an uninitialized vector. #[kani::proof] diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs index 7feb493a5b3f..fae491c40622 100644 --- a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs +++ b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs index fb8fae06ca59..dd6942252cb2 100644 --- a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs +++ b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/kani/Uninit/access-padding-enum-single-field.rs index c283b603f705..63f7f6043905 100644 --- a/tests/kani/Uninit/access-padding-enum-single-field.rs +++ b/tests/kani/Uninit/access-padding-enum-single-field.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/kani/Uninit/access-padding-enum-single-variant.rs index f33cfe7ce6fb..bb87d36d26c8 100644 --- a/tests/kani/Uninit/access-padding-enum-single-variant.rs +++ b/tests/kani/Uninit/access-padding-enum-single-variant.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z ghost-state -Z uninit-checks +// kani-flags: -Z uninit-checks use std::ptr; use std::ptr::addr_of; diff --git a/tests/kani/Uninit/access-padding-init.rs b/tests/kani/Uninit/access-padding-init.rs new file mode 100644 index 000000000000..7523622a6106 --- /dev/null +++ b/tests/kani/Uninit/access-padding-init.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::ptr::addr_of; + +#[repr(C)] +struct S(u32, u8); + +#[kani::proof] +fn access_padding_init() { + let s = S(0, 0); + let ptr: *const u8 = addr_of!(s) as *const u8; + let data = unsafe { *(ptr.add(3)) }; // Accessing data bytes is valid. +} diff --git a/tests/kani/Uninit/alloc-to-slice.rs b/tests/kani/Uninit/alloc-to-slice.rs new file mode 100644 index 000000000000..863d3b40b390 --- /dev/null +++ b/tests/kani/Uninit/alloc-to-slice.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::alloc::{alloc, Layout}; + +#[kani::proof] +fn alloc_to_slice() { + let layout = Layout::from_size_align(32, 8).unwrap(); + unsafe { + let ptr = alloc(layout); + *ptr = 0x41; + *ptr.add(1) = 0x42; + *ptr.add(2) = 0x43; + *ptr.add(3) = 0x44; + *ptr.add(16) = 0x00; + let val = *(ptr.add(2)); // Accessing previously initialized byte is valid. + } +} diff --git a/tests/kani/Uninit/alloc-zeroed-to-slice.rs b/tests/kani/Uninit/alloc-zeroed-to-slice.rs new file mode 100644 index 000000000000..d00ca4c6abff --- /dev/null +++ b/tests/kani/Uninit/alloc-zeroed-to-slice.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::alloc::{alloc_zeroed, Layout}; +use std::slice::from_raw_parts; + +#[kani::proof] +fn alloc_zeroed_to_slice() { + let layout = Layout::from_size_align(32, 8).unwrap(); + unsafe { + // This returns initialized memory, so any further accesses are valid. + let ptr = alloc_zeroed(layout); + *ptr = 0x41; + *ptr.add(1) = 0x42; + *ptr.add(2) = 0x43; + *ptr.add(3) = 0x44; + *ptr.add(16) = 0x00; + let slice1 = from_raw_parts(ptr, 16); + let slice2 = from_raw_parts(ptr.add(16), 16); + } +} diff --git a/tests/kani/Uninit/atomic.rs b/tests/kani/Uninit/atomic.rs new file mode 100644 index 000000000000..376f365d408c --- /dev/null +++ b/tests/kani/Uninit/atomic.rs @@ -0,0 +1,66 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::sync::atomic::{AtomicUsize, Ordering}; + +fn any_ordering() -> Ordering { + match kani::any() { + 0 => Ordering::Relaxed, + 1 => Ordering::Release, + 2 => Ordering::Acquire, + 3 => Ordering::AcqRel, + _ => Ordering::SeqCst, + } +} + +fn store_ordering() -> Ordering { + match kani::any() { + 0 => Ordering::Relaxed, + 1 => Ordering::Release, + _ => Ordering::SeqCst, + } +} + +fn load_ordering() -> Ordering { + match kani::any() { + 0 => Ordering::Relaxed, + 1 => Ordering::Acquire, + _ => Ordering::SeqCst, + } +} + +static GLOBAL_ATOMIC: AtomicUsize = AtomicUsize::new(0); + +// Checks if memory initialization checks work with atomics defined in the global scope. +#[kani::proof] +fn global_atomic() { + let old_value = GLOBAL_ATOMIC.fetch_add(1, any_ordering()); +} + +// Checks if memory initialization checks work with atomics. +#[kani::proof] +fn local_atomic() { + // Get a pointer to an allocated value + let ptr: *mut usize = Box::into_raw(Box::new(0)); + + // Create an atomic from the allocated value + let atomic = unsafe { AtomicUsize::from_ptr(ptr) }; + + // Use `atomic` for atomic operations + atomic.store(1, store_ordering()); + let old_val = atomic.load(load_ordering()); + let old_val = atomic.swap(2, any_ordering()); + + // Deallocate the value + unsafe { drop(Box::from_raw(ptr)) } +} + +// Checks if memory initialization checks work with compare-and-swap atomics. +#[kani::proof] +fn compare_exchange_atomic() { + // Create an atomic. + let some_var = AtomicUsize::new(5); + // Perform a `compare-and-swap` operation. + some_var.compare_exchange(5, 10, any_ordering(), load_ordering()); +} diff --git a/tests/kani/Uninit/struct-padding-and-arr-init.rs b/tests/kani/Uninit/struct-padding-and-arr-init.rs new file mode 100644 index 000000000000..c67b1177bfa3 --- /dev/null +++ b/tests/kani/Uninit/struct-padding-and-arr-init.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::ptr::addr_of_mut; + +#[repr(C)] +struct S(u32, u8); + +#[kani::proof] +fn struct_padding_and_arr_init() { + unsafe { + let mut s = S(0, 0); + let sptr = addr_of_mut!(s); + let sptr2 = sptr as *mut [u8; 4]; + *sptr2 = [0; 4]; + *sptr = S(0, 0); + // Both S(u32, u8) and [u8; 4] have the same layout, so the memory is initialized. + let val = *sptr2; + } +} diff --git a/tests/kani/Uninit/vec-read-init.rs b/tests/kani/Uninit/vec-read-init.rs new file mode 100644 index 000000000000..78812c59830e --- /dev/null +++ b/tests/kani/Uninit/vec-read-init.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +#[kani::proof] +fn vec_read_init() { + let mut v: Vec = Vec::with_capacity(10); + unsafe { *v.as_mut_ptr().add(5) = 0x42 }; + let def = unsafe { *v.as_ptr().add(5) }; // Accessing previously initialized byte is valid. + let x = def + 1; +} diff --git a/tests/perf/uninit/Cargo.toml b/tests/perf/uninit/Cargo.toml deleted file mode 100644 index 9f44cb3fe103..000000000000 --- a/tests/perf/uninit/Cargo.toml +++ /dev/null @@ -1,14 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "uninit" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] - -[package.metadata.kani] -unstable = { ghost-state = true, uninit-checks = true } diff --git a/tests/perf/uninit/expected b/tests/perf/uninit/expected deleted file mode 100644 index f7b4fd303a77..000000000000 --- a/tests/perf/uninit/expected +++ /dev/null @@ -1 +0,0 @@ -Complete - 5 successfully verified harnesses, 0 failures, 5 total. \ No newline at end of file diff --git a/tests/perf/uninit/src/lib.rs b/tests/perf/uninit/src/lib.rs deleted file mode 100644 index 86b101c0e5d8..000000000000 --- a/tests/perf/uninit/src/lib.rs +++ /dev/null @@ -1,68 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::alloc::{alloc, alloc_zeroed, Layout}; -use std::ptr; -use std::ptr::addr_of; -use std::slice::from_raw_parts; - -#[repr(C)] -struct S(u32, u8); - -#[kani::proof] -fn access_padding_init() { - let s = S(0, 0); - let ptr: *const u8 = addr_of!(s) as *const u8; - let data = unsafe { *(ptr.add(3)) }; // Accessing data bytes is valid. -} - -#[kani::proof] -fn alloc_to_slice() { - let layout = Layout::from_size_align(32, 8).unwrap(); - unsafe { - let ptr = alloc(layout); - *ptr = 0x41; - *ptr.add(1) = 0x42; - *ptr.add(2) = 0x43; - *ptr.add(3) = 0x44; - *ptr.add(16) = 0x00; - let val = *(ptr.add(2)); // Accessing previously initialized byte is valid. - } -} - -#[kani::proof] -fn alloc_zeroed_to_slice() { - let layout = Layout::from_size_align(32, 8).unwrap(); - unsafe { - // This returns initialized memory, so any further accesses are valid. - let ptr = alloc_zeroed(layout); - *ptr = 0x41; - *ptr.add(1) = 0x42; - *ptr.add(2) = 0x43; - *ptr.add(3) = 0x44; - *ptr.add(16) = 0x00; - let slice1 = from_raw_parts(ptr, 16); - let slice2 = from_raw_parts(ptr.add(16), 16); - } -} - -#[kani::proof] -fn struct_padding_and_arr_init() { - unsafe { - let mut s = S(0, 0); - let sptr = ptr::addr_of_mut!(s); - let sptr2 = sptr as *mut [u8; 4]; - *sptr2 = [0; 4]; - *sptr = S(0, 0); - // Both S(u32, u8) and [u8; 4] have the same layout, so the memory is initialized. - let val = *sptr2; - } -} - -#[kani::proof] -fn vec_read_init() { - let mut v: Vec = Vec::with_capacity(10); - unsafe { *v.as_mut_ptr().add(5) = 0x42 }; - let def = unsafe { *v.as_ptr().add(5) }; // Accessing previously initialized byte is valid. - let x = def + 1; -} diff --git a/tests/std-checks/core/slice.expected b/tests/std-checks/core/slice.expected index 01a90d50b557..4426ff6c02cd 100644 --- a/tests/std-checks/core/slice.expected +++ b/tests/std-checks/core/slice.expected @@ -1 +1 @@ -Complete - 1 successfully verified harnesses, 0 failures, 1 total. +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/std-checks/core/src/slice.rs b/tests/std-checks/core/src/slice.rs index 044f4bd38586..fe627f21a5ae 100644 --- a/tests/std-checks/core/src/slice.rs +++ b/tests/std-checks/core/src/slice.rs @@ -1,25 +1,30 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +extern crate kani; + /// Create wrapper functions to standard library functions that contains their contract. pub mod contracts { use kani::{mem::*, requires}; #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))] - #[requires(is_initialized(data, len))] pub unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] { std::slice::from_raw_parts(data, len) } + + #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))] + pub unsafe fn from_raw_parts_mut<'a, T>(data: *mut T, len: usize) -> &'a mut [T] { + std::slice::from_raw_parts_mut(data, len) + } } #[cfg(kani)] mod verify { use super::*; - const MAX_LEN: usize = 2; + const MAX_LEN: usize = isize::MAX as usize; #[kani::proof_for_contract(contracts::from_raw_parts)] - #[kani::unwind(25)] pub fn check_from_raw_parts_primitive() { let len: usize = kani::any(); kani::assume(len < MAX_LEN); @@ -27,4 +32,13 @@ mod verify { let arr = vec![0u8; len]; let _slice = unsafe { contracts::from_raw_parts(arr.as_ptr(), len) }; } + + #[kani::proof_for_contract(contracts::from_raw_parts_mut)] + pub fn check_from_raw_parts_mut_primitive() { + let len: usize = kani::any(); + kani::assume(len < MAX_LEN); + + let mut arr = vec![0u8; len]; + let _slice = unsafe { contracts::from_raw_parts_mut(arr.as_mut_ptr(), len) }; + } }