From d25a629bbe25969d0595fde632e7a1903c864c68 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Mon, 24 Jun 2024 21:15:54 -0700
Subject: [PATCH 01/22] Bump tests/perf/s2n-quic from `7495f7b` to `37335c1`
(#3288)
Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`7495f7b` to `37335c1`.
Commits
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
Signed-off-by: dependabot[bot]
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
---
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 7495f7b43c27..37335c196fb5 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit 7495f7b43c271ebf3d467409c43fc3cc864bdcc6
+Subproject commit 37335c196fb5755dcbe2532e5a3820e46906d5ea
From 0274128bc0b9e2f70639ac488a33683eeea33949 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 25 Jun 2024 04:49:01 +0000
Subject: [PATCH 02/22] Automatic toolchain upgrade to nightly-2024-06-23
(#3290)
Update Rust toolchain from nightly-2024-06-22 to nightly-2024-06-23
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
https://github.com/rust-lang/rust/commit/c1b336cb6b491b3be02cd821774f03af4992f413
up to
https://github.com/rust-lang/rust/commit/3cb521a4344f0b556b81c55eec8facddeb1ead83.
The log for this commit range is:
https://github.com/rust-lang/rust/commit/3cb521a434 Auto merge of
#126761 - GuillaumeGomez:unsafe_extern_blocks, r=spastorino
https://github.com/rust-lang/rust/commit/a0f01c3c10 Auto merge of
#126838 - matthiaskrgr:rollup-qkop22o, r=matthiaskrgr
https://github.com/rust-lang/rust/commit/dc9a08f535 Rollup merge of
#126552 - fee1-dead-contrib:rmfx, r=compiler-errors
https://github.com/rust-lang/rust/commit/162120b4fa Rollup merge of
#126318 - Kobzol:bootstrap-perf, r=onur-ozkan
https://github.com/rust-lang/rust/commit/f3ced9d540 Rollup merge of
#126140 - eduardosm:stabilize-fs_try_exists, r=Amanieu
https://github.com/rust-lang/rust/commit/f944afe380 Auto merge of
#116113 - kpreid:arcmut, r=dtolnay
https://github.com/rust-lang/rust/commit/88c3db57e4 Generalize
`{Rc,Arc}::make_mut()` to unsized types.
https://github.com/rust-lang/rust/commit/a9a4830d25 Replace
`WriteCloneIntoRaw` with `CloneToUninit`.
https://github.com/rust-lang/rust/commit/ec201b8650 Add
`core::clone::CloneToUninit`.
https://github.com/rust-lang/rust/commit/81da6a6d40 Make `effects` an
incomplete feature
https://github.com/rust-lang/rust/commit/ac47dbad50 Auto merge of
#126824 - GuillaumeGomez:rollup-sybv8o7, r=GuillaumeGomez
https://github.com/rust-lang/rust/commit/d265538016 Rollup merge of
#126823 - GuillaumeGomez:migrate-run-make-inline-always-many-cgu,
r=Kobzol
https://github.com/rust-lang/rust/commit/25bcc7d130 Rollup merge of
#126731 - Kobzol:bootstrap-cmd-refactor, r=onur-ozkan
https://github.com/rust-lang/rust/commit/399c5cabdd Rollup merge of
#126723 - estebank:dot-dot-dot, r=Nadrieril
https://github.com/rust-lang/rust/commit/3ed2cd74b5 Rollup merge of
#126686 - fmease:dump-preds-n-item-bounds, r=compiler-errors
https://github.com/rust-lang/rust/commit/07e8b3ac01 Rollup merge of
#126555 - beetrees:f16-inline-asm-arm, r=Amanieu
https://github.com/rust-lang/rust/commit/d03d6c0fea Auto merge of
#126750 - scottmcm:less-unlikely, r=jhpratt
https://github.com/rust-lang/rust/commit/e7dfd4a913 Migrate
`run-make/inline-always-many-cgu` to `rmake.rs`
https://github.com/rust-lang/rust/commit/d9962bb4d8 Make `read_dir`
method take a mutable callback
https://github.com/rust-lang/rust/commit/f1b0d54ca9 Auto merge of
#126816 - weihanglo:update-cargo, r=weihanglo
https://github.com/rust-lang/rust/commit/0bd58d8122 Apply review
comments.
https://github.com/rust-lang/rust/commit/250586cb2e Wrap std `Output` in
`CommandOutput`
https://github.com/rust-lang/rust/commit/f0aceed540 Auto merge of
#126817 - workingjubilee:rollup-0rg0k55, r=workingjubilee
https://github.com/rust-lang/rust/commit/38bd7a0fcb Add
`#[rustc_dump_{predicates,item_bounds}]`
https://github.com/rust-lang/rust/commit/1916b3d57f Rollup merge of
#126811 - compiler-errors:tidy-ftl, r=estebank
https://github.com/rust-lang/rust/commit/539090e5cd Rollup merge of
#126809 - estebank:wording-tweak, r=oli-obk
https://github.com/rust-lang/rust/commit/b9ab6c3501 Rollup merge of
#126798 - miguelfrde:master, r=tmandry
https://github.com/rust-lang/rust/commit/9498d5cf2f Rollup merge of
#126787 - Strophox:get-bytes, r=RalfJung
https://github.com/rust-lang/rust/commit/1f9793f1aa Rollup merge of
#126722 - adwinwhite:ptr_fn_abi, r=celinval
https://github.com/rust-lang/rust/commit/84b0922565 Rollup merge of
#126712 - Oneirical:bootest-constestllation, r=jieyouxu
https://github.com/rust-lang/rust/commit/e7956cd994 Rollup merge of
#126530 - beetrees:f16-inline-asm-riscv, r=Amanieu
https://github.com/rust-lang/rust/commit/10e1f5d212 Auto merge of
#124101 - the8472:pidfd-methods, r=cuviper
https://github.com/rust-lang/rust/commit/2c65a24b8c Update cargo
https://github.com/rust-lang/rust/commit/fcae62649e Auto merge of
#126758 - spastorino:avoid-safe-outside-unsafe-blocks, r=compiler-errors
https://github.com/rust-lang/rust/commit/ffd72b1700 Fix remaining cases
https://github.com/rust-lang/rust/commit/ea681ef281 Add a tidy rule to
make sure that diagnostics don't end in periods
https://github.com/rust-lang/rust/commit/8abf149bde to extract a pidfd
we must consume the child
https://github.com/rust-lang/rust/commit/0787c7308c Add PidFd::{kill,
wait, try_wait}
https://github.com/rust-lang/rust/commit/5d5892e966 Remove stray `.`
from error message
https://github.com/rust-lang/rust/commit/d94a40516e
[fuchsia-test-runner] Remove usage of kw_only
https://github.com/rust-lang/rust/commit/771e44ebd3 Add `f16` inline ASM
support for RISC-V
https://github.com/rust-lang/rust/commit/753fb070bb Add `f16` inline ASM
support for 32-bit ARM
https://github.com/rust-lang/rust/commit/22831ed117 Do not allow safe
usafe on static and fn items
https://github.com/rust-lang/rust/commit/a6a83d3d4e bless tests
https://github.com/rust-lang/rust/commit/b512bf6f77 add as_ptr to trait
AllocBytes, fix 2 impls; add pub fn get_bytes_unchecked_raw in
allocation.rs; add pub fn get_alloc_bytes_unchecked_raw[_mut] in
memory.rs
https://github.com/rust-lang/rust/commit/02aaea1803 update intrinsic
const param counting
https://github.com/rust-lang/rust/commit/3b14b756d8 Remove
`feature(effects)` from the standard library
https://github.com/rust-lang/rust/commit/a314f7363a Stop using
`unlikely` in `strict_*` methods
https://github.com/rust-lang/rust/commit/225796a2df Add method to get
`FnAbi` of function pointer
https://github.com/rust-lang/rust/commit/630c3adb14 Add regression test
for `unsafe_extern_blocks`
https://github.com/rust-lang/rust/commit/bb9a3ef90c Implement
`unsafe_extern_blocks` feature in rustdoc
https://github.com/rust-lang/rust/commit/3c0a4bc915 rewrite
crate-name-priority to rmake
https://github.com/rust-lang/rust/commit/bc12972bcd Slightly refactor
the dumping of HIR analysis data
https://github.com/rust-lang/rust/commit/3fe4d134dd Appease `clippy`
https://github.com/rust-lang/rust/commit/c15293407f Remove unused import
https://github.com/rust-lang/rust/commit/5c4318d02c Implement `run_cmd`
in terms of `run_tracked`
https://github.com/rust-lang/rust/commit/0de7b92cc6 Remove
`run_delaying_failure`
https://github.com/rust-lang/rust/commit/e933cfb13c Remove
`run_quiet_delaying_failure`
https://github.com/rust-lang/rust/commit/949e667d3f Remove `run_quiet`
https://github.com/rust-lang/rust/commit/a12f541a18 Implement new
command execution logic
https://github.com/rust-lang/rust/commit/9fd7784b97 Fix `...` in
multline code-skips in suggestions
https://github.com/rust-lang/rust/commit/f22b5afa6a rewrite
error-writing-dependencies to rmake
https://github.com/rust-lang/rust/commit/75ee1d74a9 rewrite
relocation-model to rmake
https://github.com/rust-lang/rust/commit/87d2e61428 Add `x perf` command
for profiling the compiler using `rustc-perf`
https://github.com/rust-lang/rust/commit/fd44aca2aa Copy `rustc-fake`
binary when building the `rustc-perf` tool
https://github.com/rust-lang/rust/commit/9e0b76201b Add `RustcPerf`
bootstrap tool
https://github.com/rust-lang/rust/commit/9ec178df0b Add `cargo_args` to
`ToolBuild`
https://github.com/rust-lang/rust/commit/6a04dfe78c Rename
`std::fs::try_exists` to `std::fs::exists` and stabilize fs_try_exists
Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
---
rust-toolchain.toml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 563b27562580..fb354883739f 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-22"
+channel = "nightly-2024-06-23"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
From 82d79c54b576048bc90dfb3457a49763af0c1a0a Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Mon, 24 Jun 2024 23:30:51 -0700
Subject: [PATCH 03/22] Automatic cargo update to 2024-06-24 (#3286)
Dependency upgrade resulting from `cargo update`.
Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
---
Cargo.lock | 30 +++++++++++++++---------------
1 file changed, 15 insertions(+), 15 deletions(-)
diff --git a/Cargo.lock b/Cargo.lock
index 8de76caa816d..c7a451cc8804 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -169,7 +169,7 @@ dependencies = [
"heck",
"proc-macro2",
"quote",
- "syn 2.0.66",
+ "syn 2.0.68",
]
[[package]]
@@ -482,7 +482,7 @@ dependencies = [
"proc-macro-error",
"proc-macro2",
"quote",
- "syn 2.0.66",
+ "syn 2.0.68",
]
[[package]]
@@ -498,9 +498,9 @@ dependencies = [
[[package]]
name = "lazy_static"
-version = "1.4.0"
+version = "1.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
[[package]]
name = "libc"
@@ -733,9 +733,9 @@ dependencies = [
[[package]]
name = "proc-macro2"
-version = "1.0.85"
+version = "1.0.86"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "22244ce15aa966053a896d1accb3a6e68469b97c7f33f284b99f0d576879fc23"
+checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
dependencies = [
"unicode-ident",
]
@@ -924,7 +924,7 @@ checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba"
dependencies = [
"proc-macro2",
"quote",
- "syn 2.0.66",
+ "syn 2.0.68",
]
[[package]]
@@ -1016,9 +1016,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
[[package]]
name = "strum"
-version = "0.26.2"
+version = "0.26.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5d8cec3501a5194c432b2b7976db6b7d10ec95c253208b45f83f7136aa985e29"
+checksum = "8fec0f0aef304996cf250b31b5a10dee7980c85da9d759361292b8bca5a18f06"
[[package]]
name = "strum_macros"
@@ -1030,7 +1030,7 @@ dependencies = [
"proc-macro2",
"quote",
"rustversion",
- "syn 2.0.66",
+ "syn 2.0.68",
]
[[package]]
@@ -1045,9 +1045,9 @@ dependencies = [
[[package]]
name = "syn"
-version = "2.0.66"
+version = "2.0.68"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5"
+checksum = "901fa70d88b9d6c98022e23b4136f9f3e54e4662c3bc1bd1d84a42a9a0f0c1e9"
dependencies = [
"proc-macro2",
"quote",
@@ -1083,7 +1083,7 @@ checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533"
dependencies = [
"proc-macro2",
"quote",
- "syn 2.0.66",
+ "syn 2.0.68",
]
[[package]]
@@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
dependencies = [
"proc-macro2",
"quote",
- "syn 2.0.66",
+ "syn 2.0.68",
]
[[package]]
@@ -1414,5 +1414,5 @@ checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b"
dependencies = [
"proc-macro2",
"quote",
- "syn 2.0.66",
+ "syn 2.0.68",
]
From d5f8a11bf3f246bb1dc26c024961177958f9c18a Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 25 Jun 2024 14:31:26 +0200
Subject: [PATCH 04/22] Automatic toolchain upgrade to nightly-2024-06-24
(#3291)
Update Rust toolchain from nightly-2024-06-23 to nightly-2024-06-24
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
https://github.com/rust-lang/rust/commit/3cb521a4344f0b556b81c55eec8facddeb1ead83
up to
https://github.com/rust-lang/rust/commit/bcf94dec5ba6838e435902120c0384c360126a26.
---
rust-toolchain.toml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index fb354883739f..d252d446a74c 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-23"
+channel = "nightly-2024-06-24"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
From 1491dd6eaf453efc61e915e0a3d247c2ce03abaf Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 25 Jun 2024 10:28:36 -0700
Subject: [PATCH 05/22] Automatic toolchain upgrade to nightly-2024-06-25
(#3292)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Update Rust toolchain from nightly-2024-06-24 to nightly-2024-06-25
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
https://github.com/rust-lang/rust/commit/bcf94dec5ba6838e435902120c0384c360126a26
up to
https://github.com/rust-lang/rust/commit/6b0f4b5ec3aa707ecaa78230722117324a4ce23c.
The log for this commit range is:
https://github.com/rust-lang/rust/commit/6b0f4b5ec3 Auto merge of
#126914 - compiler-errors:rollup-zx0hchm, r=compiler-errors
https://github.com/rust-lang/rust/commit/16bd6e25e1 Rollup merge of
#126911 - oli-obk:do_not_count_errors, r=compiler-errors
https://github.com/rust-lang/rust/commit/59c258f51f Rollup merge of
#126909 - onur-ozkan:add-kobzol, r=matthiaskrgr
https://github.com/rust-lang/rust/commit/85eb835a14 Rollup merge of
#126904 - GrigorenkoPV:nonzero-fixme, r=joboet
https://github.com/rust-lang/rust/commit/a7721a0373 Rollup merge of
#126899 - GrigorenkoPV:suggest-const-block, r=davidtwco
https://github.com/rust-lang/rust/commit/9ce2a070b3 Rollup merge of
#126682 - Zalathar:coverage-attr, r=lcnr
https://github.com/rust-lang/rust/commit/49bdf460a2 Rollup merge of
#126673 - oli-obk:dont_rely_on_err_reporting, r=compiler-errors
https://github.com/rust-lang/rust/commit/46e43984d1 Rollup merge of
#126413 - matthiaskrgr:crshmsg, r=oli-obk
https://github.com/rust-lang/rust/commit/ed460d2eaa Rollup merge of
#125575 - dingxiangfei2009:derive-smart-ptr, r=davidtwco
https://github.com/rust-lang/rust/commit/c77dc28f87 Rollup merge of
#125082 - kpreid:const-uninit, r=dtolnay
https://github.com/rust-lang/rust/commit/faa28be2f1 Rollup merge of
#124712 - Enselic:deprecate-inline-threshold, r=pnkfelix
https://github.com/rust-lang/rust/commit/00e5f5886a Rollup merge of
#124460 - long-long-float:show-notice-about-enum-with-debug, r=pnkfelix
https://github.com/rust-lang/rust/commit/d8d5732456 Auto merge of
#126784 - scottmcm:smaller-terminator, r=compiler-errors
https://github.com/rust-lang/rust/commit/13fca73f49 Replace
`MaybeUninit::uninit_array()` with array repeat expression.
https://github.com/rust-lang/rust/commit/5a3e2a4e92 Auto merge of
#126523 - joboet:the_great_big_tls_refactor, r=Mark-Simulacrum
https://github.com/rust-lang/rust/commit/45261ff2ec add @kobzol to
bootstrap team for triagebot
https://github.com/rust-lang/rust/commit/84474a25a4 Small fixme in core
now that NonZero is generic
https://github.com/rust-lang/rust/commit/50a02ed789 std: fix wasm builds
https://github.com/rust-lang/rust/commit/8fc6b3de19 Separate the mir
body lifetime from the other lifetimes
https://github.com/rust-lang/rust/commit/1c4d0ced58 Separate the
lifetimes of the `BorrowckInferCtxt` from the other borrowed items
https://github.com/rust-lang/rust/commit/d371d17496 Auto merge of
#126900 - matthiaskrgr:rollup-24ah97b, r=matthiaskrgr
https://github.com/rust-lang/rust/commit/8ffb5f936a compiletest: make
the crash test error message abit more informative
https://github.com/rust-lang/rust/commit/a80ee9159b Rollup merge of
#126882 - estebank:multiline-order, r=WaffleLapkin
https://github.com/rust-lang/rust/commit/8bfde609e2 Rollup merge of
#126414 - ChrisDenton:target-known, r=Nilstrieb
https://github.com/rust-lang/rust/commit/94b9ea417d Rollup merge of
#126213 - zachs18:atomicbool-u8-i8-from-ptr-alignment, r=Nilstrieb
https://github.com/rust-lang/rust/commit/9d24ecc37b Rollup merge of
#125241 - Veykril:tool-rust-analyzer, r=davidtwco
https://github.com/rust-lang/rust/commit/ba5ec1fc5c Suggest inline const
blocks for array initialization
https://github.com/rust-lang/rust/commit/06c072f158 Auto merge of
#126788 - GuillaumeGomez:migrate-rustdoc-tests-syntax, r=fmease,oli-obk
https://github.com/rust-lang/rust/commit/1852141219 coverage: Bless
coverage attribute tests
https://github.com/rust-lang/rust/commit/b7c057c9b2 coverage: Always
error on `#[coverage(..)]` in unexpected places
https://github.com/rust-lang/rust/commit/a000fa8b54 coverage: Tighten
validation of `#[coverage(off)]` and `#[coverage(on)]`
https://github.com/rust-lang/rust/commit/b5dfeba0e1 coverage: Forbid
multiple `#[coverage(..)]` attributes
https://github.com/rust-lang/rust/commit/6909feab8e Allow numbers in
rustdoc tests commands
https://github.com/rust-lang/rust/commit/4e258bb4c3 Fix tidy issue for
rustdoc tests commands
https://github.com/rust-lang/rust/commit/51fedf65ff Remove commands
duplication between `compiletest` and `tests/rustdoc`
https://github.com/rust-lang/rust/commit/1b67035579 Update
`tests/rustdoc` to new test syntax
https://github.com/rust-lang/rust/commit/d3ec92e16e Move `tests/rustdoc`
testsuite to `//@` syntax
https://github.com/rust-lang/rust/commit/2c243d9570 Auto merge of
#126891 - matthiaskrgr:rollup-p6dl1gk, r=matthiaskrgr
https://github.com/rust-lang/rust/commit/b94d2754b5 Rollup merge of
#126888 - compiler-errors:oops-debug-printing, r=dtolnay
https://github.com/rust-lang/rust/commit/9892b3e9fe Rollup merge of
#126854 - devnexen:std_unix_os_fallback_upd, r=Mark-Simulacrum
https://github.com/rust-lang/rust/commit/3108dfaced Rollup merge of
#126849 - workingjubilee:correctly-classify-arm-low-dregs, r=Amanieu
https://github.com/rust-lang/rust/commit/dcace866f0 Rollup merge of
#126845 - rust-lang:cargo_update, r=Mark-Simulacrum
https://github.com/rust-lang/rust/commit/21850f5bd8 Rollup merge of
#126807 - devnexen:copy_file_macos_simpl, r=Mark-Simulacrum
https://github.com/rust-lang/rust/commit/b24e3df0df Rollup merge of
#126754 - compiler-errors:use-rustfmt, r=calebcartwright
https://github.com/rust-lang/rust/commit/ad0531ae0d Rollup merge of
#126455 - surechen:fix_126222, r=estebank
https://github.com/rust-lang/rust/commit/7babf99ea9 Rollup merge of
#126298 - heiher:loongarch64-musl-ci, r=Mark-Simulacrum
https://github.com/rust-lang/rust/commit/9a591ea1ce Rollup merge of
#126177 - carbotaniuman:unsafe_attr_errors, r=jieyouxu
https://github.com/rust-lang/rust/commit/25446c25fc Remove stray println
from rustfmt
https://github.com/rust-lang/rust/commit/d49994b060 Auto merge of
#126023 - amandasystems:you-dropped-this-again, r=nikomatsakis
https://github.com/rust-lang/rust/commit/a23917cfd0 Add hard error and
migration lint for unsafe attrs
https://github.com/rust-lang/rust/commit/284437d434 Special case when a
code line only has multiline span starts
https://github.com/rust-lang/rust/commit/f1be59fa72 SmartPointer
derive-macro
https://github.com/rust-lang/rust/commit/a426d6fdf0 Implement use<>
formatting in rustfmt
https://github.com/rust-lang/rust/commit/16fef40896 Promote
loongarch64-unknown-linux-musl to Tier 2 with host tools
https://github.com/rust-lang/rust/commit/03d73fa6ba ci: Add support for
dist-loongarch64-musl
https://github.com/rust-lang/rust/commit/fc50acae90 fix build
https://github.com/rust-lang/rust/commit/bd9ce3e074
std::unix::os::home_dir: fallback's optimisation.
https://github.com/rust-lang/rust/commit/0d8f734172 compiler: Fix arm32
asm issues by hierarchically sorting reg classes
https://github.com/rust-lang/rust/commit/e8b5ba1111 For [E0308]:
mismatched types, when expr is in an arm's body, not add semicolon ';'
at the end of it.
https://github.com/rust-lang/rust/commit/990535723d cargo update
https://github.com/rust-lang/rust/commit/b28efb11af Save 2 pointers in
`TerminatorKind` (96 → 80 bytes)
https://github.com/rust-lang/rust/commit/65530ba100 std::unix::fs: copy
simplification for apple.
https://github.com/rust-lang/rust/commit/339015920d Add `rust_analyzer`
as a predefined tool
https://github.com/rust-lang/rust/commit/3f2f8438b4 Ensure we don't
accidentally succeed when we want to report an error
https://github.com/rust-lang/rust/commit/32f9b8bf76 std: rename module
for clarity
https://github.com/rust-lang/rust/commit/35f050b8da std: update TLS
module documentation
https://github.com/rust-lang/rust/commit/b2f29edc81 std: use the `c_int`
from `core::ffi` instead of `libc`
https://github.com/rust-lang/rust/commit/d70f071392 std: simplify
`#[cfg]`s for TLS
https://github.com/rust-lang/rust/commit/d630f5da7a Show notice about
"never used" for enum
https://github.com/rust-lang/rust/commit/f3facf1175 std: refactor the
TLS implementation
https://github.com/rust-lang/rust/commit/f5f067bf9d Deprecate no-op
codegen option `-Cinline-threshold=...`
https://github.com/rust-lang/rust/commit/651ff643ae Fix typo in
`-Cno-stack-check` deprecation warning
https://github.com/rust-lang/rust/commit/3af624272a rustc_codegen_ssa:
Remove unused ModuleConfig::inline_threshold
https://github.com/rust-lang/rust/commit/34e6ea1446 Tier 2 std support
must always be known
https://github.com/rust-lang/rust/commit/2d4cb7aa5a Update docs for
AtomicU8/I8.
https://github.com/rust-lang/rust/commit/7885c7b7b2 Update safety docs
for AtomicBool::from_ptr.
https://github.com/rust-lang/rust/commit/7b5b7a7010 Remove confusing
`use_polonius` flag and do less cloning
Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>
---
rust-toolchain.toml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index d252d446a74c..18be92ff77ee 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-24"
+channel = "nightly-2024-06-25"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
From 997c95cc041fac75b7aa0e1b0d2c1eda5453d715 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro"
Date: Thu, 27 Jun 2024 03:16:26 -0400
Subject: [PATCH 06/22] RFC: Quantifiers (#3242)
RFC describing the support for existential and universal quantifiers in
Kani.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---------
Signed-off-by: Felipe R. Monteiro
---
rfc/src/SUMMARY.md | 1 +
rfc/src/rfcs/0010-quantifiers.md | 203 +++++++++++++++++++++++++++++++
2 files changed, 204 insertions(+)
create mode 100644 rfc/src/rfcs/0010-quantifiers.md
diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md
index f8d5dc5639f5..e0b31761ae62 100644
--- a/rfc/src/SUMMARY.md
+++ b/rfc/src/SUMMARY.md
@@ -15,3 +15,4 @@
- [0007-global-conditions](rfcs/0007-global-conditions.md)
- [0008-line-coverage](rfcs/0008-line-coverage.md)
- [0009-function-contracts](rfcs/0009-function-contracts.md)
+- [0010-quantifiers](rfcs/0010-quantifiers.md)
diff --git a/rfc/src/rfcs/0010-quantifiers.md b/rfc/src/rfcs/0010-quantifiers.md
new file mode 100644
index 000000000000..07a5f7548974
--- /dev/null
+++ b/rfc/src/rfcs/0010-quantifiers.md
@@ -0,0 +1,203 @@
+- **Feature Name:** Quantifiers
+- **Feature Request Issue:** [#2546](https://github.com/model-checking/kani/issues/2546) and [#836](https://github.com/model-checking/kani/issues/836)
+- **RFC PR:** [#](https://github.com/model-checking/kani/pull/)
+- **Status:** Unstable
+- **Version:** 1.0
+
+-------------------
+
+## Summary
+
+Quantifiers are logical operators that allow users to express that a property or condition applies to some or all objects within a given domain.
+
+## User Impact
+
+There are two primary quantifiers: the existential quantifier (∃) and the universal quantifier (∀).
+
+1. The existential quantifier (∃): represents the statement "there exists." We use to express that there is at least one object in the domain that satisfies a given condition. For example, "∃x P(x)" means "there exists a value x such that P(x) is true."
+
+2. The universal quantifier (∀): represents the statement "for all" or "for every." We use it to express that a given condition is true for every object in the domain. For example, "∀x P(x)" means "for every value x, P(x) is true."
+
+Rather than exhaustively listing all elements in a domain, quantifiers enable users to make statements about the entire domain at once. This compact representation is crucial when dealing with large or unbounded inputs. Quantifiers also facilitate abstraction and generalization of properties. Instead of specifying properties for specific instances, quantified properties can capture general patterns and behaviors that hold across different objects in a domain. Additionally, by replacing loops in the specification with quantifiers, Kani can encode the properties more efficiently within the specified bounds, making the verification process more manageable and computationally feasible.
+
+This new feature doesn't introduce any breaking changes to users. It will only allow them to write properites using the existential (∃) and universal (∀) quantifiers.
+
+## User Experience
+
+We propose a syntax inspired by ["Pattern Types"](https://github.com/rust-lang/rust/pull/120131). The syntax of existential (i.e., `kani::exists`) and universal (i.e., `kani::forall`) quantifiers are:
+
+```rust
+kani::exists(|: [is ] | )
+kani::forall(|: [is ] | )
+```
+
+If `` is not provided, we assume `` can range over all possible values of the given `` (i.e., syntactic sugar for full range `|: as .. |`). CBMC's SAT backend only supports bounded quantification under **constant** lower and upper bounds (for more details, see the [documentation for quantifiers in CBMC](https://diffblue.github.io/cbmc/contracts-quantifiers.html)). The SMT backend, on the other hand, supports arbitrary Boolean expressions. In any case, `` should not have side effects, as the purpose of quantifiers is to assert a condition over a domain of objects without altering the state.
+
+Consider the following example adapted from the documentation for the [from_raw_parts](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.from_raw_parts) function:
+
+```rust
+use std::ptr;
+use std::mem;
+
+#[kani::proof]
+fn main() {
+ let v = vec![kani::any::(); 100];
+
+ // Prevent running `v`'s destructor so we are in complete control
+ // of the allocation.
+ let mut v = mem::ManuallyDrop::new(v);
+
+ // Pull out the various important pieces of information about `v`
+ let p = v.as_mut_ptr();
+ let len = v.len();
+ let cap = v.capacity();
+
+ unsafe {
+ // Overwrite memory
+ for i in 0..len {
+ *p.add(i) += 1;
+ }
+
+ // Put everything back together into a Vec
+ let rebuilt = Vec::from_raw_parts(p, len, cap);
+ }
+}
+```
+
+Given the `v` vector has non-deterministic values, there are potential arithmetic overflows that might happen in the for loop. So we need to constrain all values of the array. We may also want to check all values of `rebuilt` after the operation. Without quantifiers, we might be tempted to use loops as follows:
+
+```rust
+use std::ptr;
+use std::mem;
+
+#[kani::proof]
+fn main() {
+ let original_v = vec![kani::any::(); 100];
+ let v = original_v.clone();
+ for i in 0..v.len() {
+ kani::assume(v[i] < 5);
+ }
+
+ // Prevent running `v`'s destructor so we are in complete control
+ // of the allocation.
+ let mut v = mem::ManuallyDrop::new(v);
+
+ // Pull out the various important pieces of information about `v`
+ let p = v.as_mut_ptr();
+ let len = v.len();
+ let cap = v.capacity();
+
+ unsafe {
+ // Overwrite memory
+ for i in 0..len {
+ *p.add(i) += 1;
+ }
+
+ // Put everything back together into a Vec
+ let rebuilt = Vec::from_raw_parts(p, len, cap);
+ for i in 0..len {
+ assert_eq!(rebuilt[i], original_v[i]+1);
+ }
+ }
+}
+```
+
+This, however, might unnecessary increase the complexity of the verication process. We can achieve the same effect using quantifiers as shown below.
+
+```rust
+use std::ptr;
+use std::mem;
+
+#[kani::proof]
+fn main() {
+ let original_v = vec![kani::any::(); 3];
+ let v = original_v.clone();
+ kani::assume(kani::forall(|i: usize is ..v.len() | v[i] < 5));
+
+ // Prevent running `v`'s destructor so we are in complete control
+ // of the allocation.
+ let mut v = mem::ManuallyDrop::new(v);
+
+ // Pull out the various important pieces of information about `v`
+ let p = v.as_mut_ptr();
+ let len = v.len();
+ let cap = v.capacity();
+
+ unsafe {
+ // Overwrite memory
+ for i in 0..len {
+ *p.add(i) += 1;
+ }
+
+ // Put everything back together into a Vec
+ let rebuilt = Vec::from_raw_parts(p, len, cap);
+ assert!(kani::forall(|i: usize is ..len | rebuilt[i] == original_v[i]+1));
+ }
+}
+```
+
+The same principle applies if we want to use the existential quantifier.
+
+```rust
+use std::ptr;
+use std::mem;
+
+#[kani::proof]
+fn main() {
+ let original_v = vec![kani::any::(); 3];
+ let v = original_v.clone();
+ kani::assume(kani::forall(|i: usize is ..v.len() | v[i] < 5));
+
+ // Prevent running `v`'s destructor so we are in complete control
+ // of the allocation.
+ let mut v = mem::ManuallyDrop::new(v);
+
+ // Pull out the various important pieces of information about `v`
+ let p = v.as_mut_ptr();
+ let len = v.len();
+ let cap = v.capacity();
+
+ unsafe {
+ // Overwrite memory
+ for i in 0..len {
+ *p.add(i) += 1;
+ if i == 1 {
+ *p.add(i) = 0;
+ }
+ }
+
+ // Put everything back together into a Vec
+ let rebuilt = Vec::from_raw_parts(p, len, cap);
+ assert!(kani::exists(|i: usize is ..len | rebuilt[i] == 0));
+ }
+}
+```
+
+The usage of quantifiers should be valid in any part of the Rust code analysed by Kani.
+
+## Detailed Design
+
+
+
+Kani should have the same support that CBMC has for quantifiers. For more details, see [Quantifiers](https://github.com/diffblue/cbmc/blob/0a69a64e4481473d62496f9975730d24f194884a/doc/cprover-manual/contracts-quantifiers.md).
+
+
+## Open questions
+
+
+- **Function Contracts RFC** - CBMC has support for both `exists` and `forall`, but the
+ code generation is difficult. The most ergonomic and easy way to implement
+ quantifiers on the Rust side is as higher-order functions taking `Fn(T) ->
+ bool`, where `T` is some arbitrary type that can be quantified over. This
+ interface is familiar to developers, but the code generation is tricky, as
+ CBMC level quantifiers only allow certain kinds of expressions. This
+ necessitates a rewrite of the `Fn` closure to a compliant expression.
+ - Which kind of expressions should be accepted as a "compliant expression"?
+
+
+## Future possibilities
+
+
+- CBMC has an SMT backend which allows the use of quantifiers with arbitrary Boolean expressions. Kani must include an option for users to experiment with this backend.
+
+---
From c8746e2e942a137078d3ef7ed458d2a2234337cd Mon Sep 17 00:00:00 2001
From: Matias Scharager
Date: Thu, 27 Jun 2024 13:46:57 -0400
Subject: [PATCH 07/22] Fix operand in fat pointer comparison (#3297)
Fixing a typo that causes potential issues in compilation.
Co-authored-by: Matias Scharager
---
kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 407ff261f6ab..e01ffbe462ba 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -57,7 +57,7 @@ impl<'tcx> GotocCtx<'tcx> {
) -> Expr {
debug!(?op, ?left_op, ?right_op, "codegen_comparison_fat_ptr");
let left_typ = self.operand_ty_stable(left_op);
- let right_typ = self.operand_ty_stable(left_op);
+ let right_typ = self.operand_ty_stable(right_op);
assert_eq!(left_typ, right_typ, "Cannot compare pointers of different types");
assert!(self.is_fat_pointer_stable(left_typ));
From 3adb2620d22d6e3ca654aa0a8c86b4f30da15e00 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig
Date: Thu, 27 Jun 2024 21:04:11 +0200
Subject: [PATCH 08/22] C library: declare malloc (#3296)
In #1812 we removed standard library includes and instead provided
forward declarations of `free`, `calloc`, and `memcpy` -- but seemingly
forgot to include `malloc`, which we also use.
This avoids a warning seen when dialling up `goto-cc` verbosity.
---
library/kani/kani_lib.c | 1 +
1 file changed, 1 insertion(+)
diff --git a/library/kani/kani_lib.c b/library/kani/kani_lib.c
index b077547b10d7..eca17a3abb0e 100644
--- a/library/kani/kani_lib.c
+++ b/library/kani/kani_lib.c
@@ -8,6 +8,7 @@
void free(void *ptr);
void *memcpy(void *dst, const void *src, size_t n);
void *calloc(size_t nmemb, size_t size);
+void *malloc(size_t size);
typedef __CPROVER_bool bool;
From 3b9665fcebe1a3d773996dbd54895ce483c34ea0 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Thu, 27 Jun 2024 14:54:06 -0600
Subject: [PATCH 09/22] Upgrade rust toolchain to 06-26 (#3299)
Related change:
- https://github.com/rust-lang/rust/commit/24e41f1d13
Resolves #3294
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
kani-compiler/src/kani_middle/intrinsics.rs | 2 +-
rust-toolchain.toml | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs
index 82a75a91f1ad..73e42be00e7b 100644
--- a/kani-compiler/src/kani_middle/intrinsics.rs
+++ b/kani-compiler/src/kani_middle/intrinsics.rs
@@ -77,7 +77,7 @@ impl<'tcx> ModelIntrinsics<'tcx> {
let Operand::Constant(fn_def) = func else { unreachable!() };
fn_def.const_ = mirConst::from_value(
ConstValue::ZeroSized,
- tcx.type_of(stub_id).instantiate(tcx, &new_gen_args),
+ tcx.type_of(stub_id).instantiate(tcx, &*new_gen_args),
);
} else {
debug!(?arg_ty, "replace_simd_bitmask failed");
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 18be92ff77ee..e00fa6c1b0e3 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-25"
+channel = "nightly-2024-06-26"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
From 5a6a5f30aac71b6a78cf4242348fd52df34ae0cf Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Fri, 28 Jun 2024 10:07:46 +0200
Subject: [PATCH 10/22] Automatic toolchain upgrade to nightly-2024-06-27
(#3301)
Update Rust toolchain from nightly-2024-06-26 to nightly-2024-06-27
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
https://github.com/rust-lang/rust/commit/fda509e817abeeecb5b76bc1de844f355675c81e
up to
https://github.com/rust-lang/rust/commit/4bc39f028d14c24b04dd17dc425432c6ec354536.
---
rust-toolchain.toml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index e00fa6c1b0e3..c620752b423a 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-26"
+channel = "nightly-2024-06-27"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
From 0994887f481a657c80044a32eea60092499393ed Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Mon, 1 Jul 2024 11:32:21 -0400
Subject: [PATCH 11/22] Automatic cargo update to 2024-07-01 (#3310)
Dependency upgrade resulting from `cargo update`.
---
Cargo.lock | 32 ++++++++++++++++----------------
1 file changed, 16 insertions(+), 16 deletions(-)
diff --git a/Cargo.lock b/Cargo.lock
index c7a451cc8804..89e393db8b46 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -86,9 +86,9 @@ checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0"
[[package]]
name = "bitflags"
-version = "2.5.0"
+version = "2.6.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1"
+checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
[[package]]
name = "build-kani"
@@ -140,9 +140,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
[[package]]
name = "clap"
-version = "4.5.7"
+version = "4.5.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5db83dced34638ad474f39f250d7fea9598bdd239eaced1bdf45d597da0f433f"
+checksum = "84b3edb18336f4df585bc9aa31dd99c036dfa5dc5e9a2939a722a188f3a8970d"
dependencies = [
"clap_builder",
"clap_derive",
@@ -150,9 +150,9 @@ dependencies = [
[[package]]
name = "clap_builder"
-version = "4.5.7"
+version = "4.5.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f7e204572485eb3fbf28f871612191521df159bc3e15a9f5064c66dba3a8c05f"
+checksum = "c1c09dd5ada6c6c78075d6fd0da3f90d8080651e2d6cc8eb2f1aaa4034ced708"
dependencies = [
"anstream",
"anstyle",
@@ -162,9 +162,9 @@ dependencies = [
[[package]]
name = "clap_derive"
-version = "4.5.5"
+version = "4.5.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c780290ccf4fb26629baa7a1081e68ced113f1d3ec302fa5948f1c381ebf06c6"
+checksum = "2bac35c6dafb060fd4d275d9a4ffae97917c13a6327903a8be2153cd964f7085"
dependencies = [
"heck",
"proc-macro2",
@@ -290,9 +290,9 @@ dependencies = [
[[package]]
name = "either"
-version = "1.12.0"
+version = "1.13.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3dca9240753cf90908d7e4aac30f630662b02aebaa1b58a3cadabdb23385b58b"
+checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0"
[[package]]
name = "encode_unicode"
@@ -536,9 +536,9 @@ dependencies = [
[[package]]
name = "log"
-version = "0.4.21"
+version = "0.4.22"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c"
+checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
[[package]]
name = "matchers"
@@ -587,9 +587,9 @@ dependencies = [
[[package]]
name = "num-bigint"
-version = "0.4.5"
+version = "0.4.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c165a9ab64cf766f73521c0dd2cfdff64f488b8f0b3e621face3462d3db536d7"
+checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9"
dependencies = [
"num-integer",
"num-traits",
@@ -929,9 +929,9 @@ dependencies = [
[[package]]
name = "serde_json"
-version = "1.0.117"
+version = "1.0.119"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3"
+checksum = "e8eddb61f0697cc3989c5d64b452f5488e2b8a60fd7d5076a3045076ffef8cb0"
dependencies = [
"itoa",
"ryu",
From 6f0c0b5b97c6861a3113af85c5d94bc17ee3e306 Mon Sep 17 00:00:00 2001
From: Matias Scharager
Date: Mon, 1 Jul 2024 12:39:32 -0400
Subject: [PATCH 12/22] Function Contracts: Closure Type Inference (#3307)
The rust type inference for closures doesn't work in the particular use
case we are using it for ensures clauses. By creating a helper function,
we change the path the rust type inference takes and lets the type of
the closure be identified properly. This means type annotations are no
longer required within ensures clauses.
Resolves #3304
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
library/kani/src/internal.rs | 7 +++++++
.../kani_macros/src/sysroot/contracts/shared.rs | 2 +-
.../simple_ensures_pass_no_annotation.expected | 6 ++++++
.../simple_ensures_pass_no_annotation.rs | 14 ++++++++++++++
.../mutating_ensures_error.expected | 1 +
.../function-contracts/mutating_ensures_error.rs | 12 ++++++++++++
6 files changed, 41 insertions(+), 1 deletion(-)
create mode 100644 tests/expected/function-contract/simple_ensures_pass_no_annotation.expected
create mode 100644 tests/expected/function-contract/simple_ensures_pass_no_annotation.rs
create mode 100644 tests/ui/function-contracts/mutating_ensures_error.expected
create mode 100644 tests/ui/function-contracts/mutating_ensures_error.rs
diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
index a910c333b112..509f2cf51962 100644
--- a/library/kani/src/internal.rs
+++ b/library/kani/src/internal.rs
@@ -90,3 +90,10 @@ pub fn untracked_deref(_: &T) -> T {
#[doc(hidden)]
#[rustc_diagnostic_item = "KaniInitContracts"]
pub fn init_contracts() {}
+
+/// This should only be used within contracts. The intent is to
+/// perform type inference on a closure's argument
+#[doc(hidden)]
+pub fn apply_closure bool>(f: U, x: &T) -> bool {
+ f(x)
+}
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
index 2682c0781661..1ab791d9a117 100644
--- a/library/kani_macros/src/sysroot/contracts/shared.rs
+++ b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -176,7 +176,7 @@ pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) {
.fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect));
let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
- (remembers_stmts, Expr::Verbatim(quote!((#expr)(result))))
+ (remembers_stmts, Expr::Verbatim(quote!(kani::internal::apply_closure(#expr, result))))
}
trait OldTrigger {
diff --git a/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected b/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected
new file mode 100644
index 000000000000..0779b6dc88f8
--- /dev/null
+++ b/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|result| (*result == x) | (*result == y)"\
+in function max
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/simple_ensures_pass_no_annotation.rs b/tests/expected/function-contract/simple_ensures_pass_no_annotation.rs
new file mode 100644
index 000000000000..a3bf30e1c0f7
--- /dev/null
+++ b/tests/expected/function-contract/simple_ensures_pass_no_annotation.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|result| (*result == x) | (*result == y))]
+fn max(x: u32, y: u32) -> u32 {
+ if x > y { x } else { y }
+}
+
+#[kani::proof_for_contract(max)]
+fn max_harness() {
+ let _ = Box::new(9_usize);
+ max(7, 6);
+}
diff --git a/tests/ui/function-contracts/mutating_ensures_error.expected b/tests/ui/function-contracts/mutating_ensures_error.expected
new file mode 100644
index 000000000000..4e9bb3984298
--- /dev/null
+++ b/tests/ui/function-contracts/mutating_ensures_error.expected
@@ -0,0 +1 @@
+cannot assign to `*_x`, as `Fn` closures cannot mutate their captured variables
diff --git a/tests/ui/function-contracts/mutating_ensures_error.rs b/tests/ui/function-contracts/mutating_ensures_error.rs
new file mode 100644
index 000000000000..2fc5f3c8d702
--- /dev/null
+++ b/tests/ui/function-contracts/mutating_ensures_error.rs
@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|_| {*_x += 1; true})]
+fn unit(_x: &mut u32) {}
+
+#[kani::proof_for_contract(id)]
+fn harness() {
+ let mut x = kani::any();
+ unit(&mut x);
+}
From d55f25b81c8fa6a0bed1b7e7f9af3383b397a525 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Mon, 1 Jul 2024 15:14:44 -0400
Subject: [PATCH 13/22] Add support for f16 and f128 for toolchain upgrade to
6/28 (#3306)
Adds support for f16 and f128, i.e
1. adding translation to `irep` .
2. generating arbitrary values for the new types
3. generating basic invariants (checking if safe) for new types
4. Adds sanity testing for arbitrary on the new types.
Resolves #3303
---
cprover_bindings/src/goto_program/expr.rs | 26 +++++++++
cprover_bindings/src/goto_program/typ.rs | 54 ++++++++++++++++++-
cprover_bindings/src/irep/irep_id.rs | 4 ++
cprover_bindings/src/irep/to_irep.rs | 43 +++++++++++++++
cprover_bindings/src/lib.rs | 3 ++
.../codegen_cprover_gotoc/codegen/operand.rs | 6 +++
.../src/codegen_cprover_gotoc/codegen/typ.rs | 7 +--
kani-compiler/src/kani_middle/attributes.rs | 3 +-
kani-compiler/src/main.rs | 2 +
library/kani/src/arbitrary.rs | 4 ++
library/kani/src/invariant.rs | 2 +
library/kani/src/lib.rs | 2 +
library/kani_core/src/arbitrary.rs | 9 ++++
library/kani_core/src/lib.rs | 2 +
rust-toolchain.toml | 2 +-
.../floats/non_standard_floats/expected | 31 +++++++++++
.../floats/non_standard_floats/main.rs | 27 ++++++++++
.../floats/{ => standard_floats}/expected | 2 -
.../floats/{ => standard_floats}/main.rs | 11 ++--
tests/kani/FloatingPoint/main.rs | 6 +++
tests/kani/Invariant/invariant_impls.rs | 7 +++
21 files changed, 240 insertions(+), 13 deletions(-)
create mode 100644 tests/expected/arbitrary/floats/non_standard_floats/expected
create mode 100644 tests/expected/arbitrary/floats/non_standard_floats/main.rs
rename tests/expected/arbitrary/floats/{ => standard_floats}/expected (99%)
rename tests/expected/arbitrary/floats/{ => standard_floats}/main.rs (74%)
diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 75eb18df0abb..16f33115e0ff 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -98,7 +98,11 @@ pub enum ExprValue {
// {}
EmptyUnion,
/// `1.0f`
+ Float16Constant(f16),
+ /// `1.0f`
FloatConstant(f32),
+ /// `Float 128 example`
+ Float128Constant(f128),
/// `function(arguments)`
FunctionCall {
function: Expr,
@@ -581,6 +585,28 @@ impl Expr {
expr!(EmptyUnion, typ)
}
+ /// `3.14f`
+ pub fn float16_constant(c: f16) -> Self {
+ expr!(Float16Constant(c), Type::float16())
+ }
+
+ /// `union {_Float16 f; uint16_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
+ pub fn float16_constant_from_bitpattern(bp: u16) -> Self {
+ let c = f16::from_bits(bp);
+ Self::float16_constant(c)
+ }
+
+ /// `3.14159265358979323846264338327950288L`
+ pub fn float128_constant(c: f128) -> Self {
+ expr!(Float128Constant(c), Type::float128())
+ }
+
+ /// `union {_Float128 f; __uint128_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
+ pub fn float128_constant_from_bitpattern(bp: u128) -> Self {
+ let c = f128::from_bits(bp);
+ Self::float128_constant(c)
+ }
+
/// `1.0f`
pub fn float_constant(c: f32) -> Self {
expr!(FloatConstant(c), Type::float())
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
index da943b26ab19..d0cc8821a447 100644
--- a/cprover_bindings/src/goto_program/typ.rs
+++ b/cprover_bindings/src/goto_program/typ.rs
@@ -41,6 +41,10 @@ pub enum Type {
FlexibleArray { typ: Box },
/// `float`
Float,
+ /// `_Float16`
+ Float16,
+ /// `_Float128`
+ Float128,
/// `struct x {}`
IncompleteStruct { tag: InternedString },
/// `union x {}`
@@ -166,6 +170,8 @@ impl DatatypeComponent {
| Double
| FlexibleArray { .. }
| Float
+ | Float16
+ | Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
@@ -363,6 +369,8 @@ impl Type {
Double => st.machine_model().double_width,
Empty => 0,
FlexibleArray { .. } => 0,
+ Float16 => 16,
+ Float128 => 128,
Float => st.machine_model().float_width,
IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
@@ -532,6 +540,22 @@ impl Type {
}
}
+ pub fn is_float_16(&self) -> bool {
+ let concrete = self.unwrap_typedef();
+ match concrete {
+ Float16 => true,
+ _ => false,
+ }
+ }
+
+ pub fn is_float_128(&self) -> bool {
+ let concrete = self.unwrap_typedef();
+ match concrete {
+ Float128 => true,
+ _ => false,
+ }
+ }
+
pub fn is_float(&self) -> bool {
let concrete = self.unwrap_typedef();
match concrete {
@@ -543,7 +567,7 @@ impl Type {
pub fn is_floating_point(&self) -> bool {
let concrete = self.unwrap_typedef();
match concrete {
- Double | Float => true,
+ Double | Float | Float16 | Float128 => true,
_ => false,
}
}
@@ -577,6 +601,8 @@ impl Type {
| CInteger(_)
| Double
| Float
+ | Float16
+ | Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
@@ -632,6 +658,8 @@ impl Type {
| Double
| Empty
| Float
+ | Float16
+ | Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
@@ -918,6 +946,8 @@ impl Type {
| CInteger(_)
| Double
| Float
+ | Float16
+ | Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
@@ -1042,6 +1072,14 @@ impl Type {
FlexibleArray { typ: Box::new(self) }
}
+ pub fn float16() -> Self {
+ Float16
+ }
+
+ pub fn float128() -> Self {
+ Float128
+ }
+
pub fn float() -> Self {
Float
}
@@ -1275,6 +1313,10 @@ impl Type {
Expr::c_true()
} else if self.is_float() {
Expr::float_constant(1.0)
+ } else if self.is_float_16() {
+ Expr::float16_constant(1.0)
+ } else if self.is_float_128() {
+ Expr::float128_constant(1.0)
} else if self.is_double() {
Expr::double_constant(1.0)
} else {
@@ -1291,6 +1333,10 @@ impl Type {
Expr::c_false()
} else if self.is_float() {
Expr::float_constant(0.0)
+ } else if self.is_float_16() {
+ Expr::float16_constant(0.0)
+ } else if self.is_float_128() {
+ Expr::float128_constant(0.0)
} else if self.is_double() {
Expr::double_constant(0.0)
} else if self.is_pointer() {
@@ -1309,6 +1355,8 @@ impl Type {
| CInteger(_)
| Double
| Float
+ | Float16
+ | Float128
| Integer
| Pointer { .. }
| Signedbv { .. }
@@ -1413,6 +1461,8 @@ impl Type {
Type::Empty => "empty".to_string(),
Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()),
Type::Float => "float".to_string(),
+ Type::Float16 => "float16".to_string(),
+ Type::Float128 => "float128".to_string(),
Type::IncompleteStruct { tag } => tag.to_string(),
Type::IncompleteUnion { tag } => tag.to_string(),
Type::InfiniteArray { typ } => {
@@ -1512,6 +1562,8 @@ mod type_tests {
assert_eq!(type_def.is_unsigned(&mm), src_type.is_unsigned(&mm));
assert_eq!(type_def.is_scalar(), src_type.is_scalar());
assert_eq!(type_def.is_float(), src_type.is_float());
+ assert_eq!(type_def.is_float_16(), src_type.is_float_16());
+ assert_eq!(type_def.is_float_128(), src_type.is_float_128());
assert_eq!(type_def.is_floating_point(), src_type.is_floating_point());
assert_eq!(type_def.width(), src_type.width());
assert_eq!(type_def.can_be_lvalue(), src_type.can_be_lvalue());
diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs
index 119aecb8887c..9d52f4ef32fa 100644
--- a/cprover_bindings/src/irep/irep_id.rs
+++ b/cprover_bindings/src/irep/irep_id.rs
@@ -283,6 +283,8 @@ pub enum IrepId {
Short,
Long,
Float,
+ Float16,
+ Float128,
Double,
Byte,
Boolean,
@@ -1157,6 +1159,8 @@ impl Display for IrepId {
IrepId::Short => "short",
IrepId::Long => "long",
IrepId::Float => "float",
+ IrepId::Float16 => "float16",
+ IrepId::Float128 => "float128",
IrepId::Double => "double",
IrepId::Byte => "byte",
IrepId::Boolean => "boolean",
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index 8716c16d88e0..4b5c86350172 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -254,6 +254,25 @@ impl ToIrep for ExprValue {
)],
}
}
+ ExprValue::Float16Constant(i) => {
+ let c: u16 = i.to_bits();
+ Irep {
+ id: IrepId::Constant,
+ sub: vec![],
+ named_sub: linear_map![(IrepId::Value, Irep::just_bitpattern_id(c, 16, false))],
+ }
+ }
+ ExprValue::Float128Constant(i) => {
+ let c: u128 = i.to_bits();
+ Irep {
+ id: IrepId::Constant,
+ sub: vec![],
+ named_sub: linear_map![(
+ IrepId::Value,
+ Irep::just_bitpattern_id(c, 128, false)
+ )],
+ }
+ }
ExprValue::FunctionCall { function, arguments } => side_effect_irep(
IrepId::FunctionCall,
vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
@@ -695,6 +714,30 @@ impl ToIrep for Type {
(IrepId::CCType, Irep::just_id(IrepId::Float)),
],
},
+ Type::Float16 => Irep {
+ id: IrepId::Floatbv,
+ sub: vec![],
+ // Fraction bits: 10
+ // Exponent width bits: 5
+ // Sign bit: 1
+ named_sub: linear_map![
+ (IrepId::F, Irep::just_int_id(10)),
+ (IrepId::Width, Irep::just_int_id(16)),
+ (IrepId::CCType, Irep::just_id(IrepId::Float16)),
+ ],
+ },
+ Type::Float128 => Irep {
+ id: IrepId::Floatbv,
+ sub: vec![],
+ // Fraction bits: 112
+ // Exponent width bits: 15
+ // Sign bit: 1
+ named_sub: linear_map![
+ (IrepId::F, Irep::just_int_id(112)),
+ (IrepId::Width, Irep::just_int_id(128)),
+ (IrepId::CCType, Irep::just_id(IrepId::Float128)),
+ ],
+ },
Type::IncompleteStruct { tag } => Irep {
id: IrepId::Struct,
sub: vec![],
diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs
index cd87dffd75a6..e77b29a24ca2 100644
--- a/cprover_bindings/src/lib.rs
+++ b/cprover_bindings/src/lib.rs
@@ -29,6 +29,9 @@
//! Speical [irep::Irep::id]s include:
//! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].
+#![feature(f128)]
+#![feature(f16)]
+
mod env;
pub mod goto_program;
pub mod irep;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 7388ca44a5b7..5549edcced25 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -184,12 +184,18 @@ impl<'tcx> GotocCtx<'tcx> {
// Instead, we use integers with the right width to represent the bit pattern.
{
match k {
+ FloatTy::F16 => Some(Expr::float16_constant_from_bitpattern(
+ alloc.read_uint().unwrap() as u16,
+ )),
FloatTy::F32 => Some(Expr::float_constant_from_bitpattern(
alloc.read_uint().unwrap() as u32,
)),
FloatTy::F64 => Some(Expr::double_constant_from_bitpattern(
alloc.read_uint().unwrap() as u64,
)),
+ FloatTy::F128 => {
+ Some(Expr::float128_constant_from_bitpattern(alloc.read_uint().unwrap()))
+ }
}
}
TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _))
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 6d00bda5bce4..6e6547295ff9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -130,6 +130,8 @@ impl<'tcx> GotocCtx<'tcx> {
Type::Empty => todo!(),
Type::FlexibleArray { .. } => todo!(),
Type::Float => write!(out, "f32")?,
+ Type::Float16 => write!(out, "f16")?,
+ Type::Float128 => write!(out, "f128")?,
Type::IncompleteStruct { .. } => todo!(),
Type::IncompleteUnion { .. } => todo!(),
Type::InfiniteArray { .. } => todo!(),
@@ -542,9 +544,8 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Float(k) => match k {
FloatTy::F32 => Type::float(),
FloatTy::F64 => Type::double(),
- // `F16` and `F128` are not yet handled.
- // Tracked here:
- FloatTy::F16 | FloatTy::F128 => unimplemented!(),
+ FloatTy::F16 => Type::float16(),
+ FloatTy::F128 => Type::float128(),
},
ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
ty::Adt(def, subst) => {
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index b7d8feeee886..84ec8d627c59 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -1034,10 +1034,9 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option {
.intersperse("::")
.collect::();
KaniAttributeKind::try_from(ident_str.as_str())
- .map_err(|err| {
+ .inspect_err(|&err| {
debug!(?err, "attr_kind_failed");
tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`"));
- err
})
.ok()
} else {
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index a5cfa347a85e..d2f8cf17e9e7 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -13,6 +13,8 @@
#![feature(more_qualified_paths)]
#![feature(iter_intersperse)]
#![feature(let_chains)]
+#![feature(f128)]
+#![feature(f16)]
extern crate rustc_abi;
extern crate rustc_ast;
extern crate rustc_ast_pretty;
diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index 3f1adc787b79..424ca2485d57 100644
--- a/library/kani/src/arbitrary.rs
+++ b/library/kani/src/arbitrary.rs
@@ -71,6 +71,10 @@ trivial_arbitrary!(isize);
trivial_arbitrary!(f32);
trivial_arbitrary!(f64);
+// Similarly, we do not constraint values for non-standard floating types.
+trivial_arbitrary!(f16);
+trivial_arbitrary!(f128);
+
trivial_arbitrary!(());
impl Arbitrary for bool {
diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs
index f118f94e995c..068cdedc277e 100644
--- a/library/kani/src/invariant.rs
+++ b/library/kani/src/invariant.rs
@@ -96,6 +96,8 @@ trivial_invariant!(isize);
// invariant that checks for NaN, infinite, or subnormal values.
trivial_invariant!(f32);
trivial_invariant!(f64);
+trivial_invariant!(f16);
+trivial_invariant!(f128);
trivial_invariant!(());
trivial_invariant!(bool);
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index acf1e08e0441..0a52a9516398 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -18,6 +18,8 @@
#![allow(internal_features)]
// Required for implementing memory predicates.
#![feature(ptr_metadata)]
+#![feature(f16)]
+#![feature(f128)]
pub mod arbitrary;
#[cfg(feature = "concrete_playback")]
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index d202df4ead1d..a8271ad758cf 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/library/kani_core/src/arbitrary.rs
@@ -88,6 +88,15 @@ macro_rules! generate_arbitrary {
trivial_arbitrary!(i128);
trivial_arbitrary!(isize);
+ // We do not constrain floating points values per type spec. Users must add assumptions to their
+ // verification code if they want to eliminate NaN, infinite, or subnormal.
+ trivial_arbitrary!(f32);
+ trivial_arbitrary!(f64);
+
+ // Similarly, we do not constraint values for non-standard floating types.
+ trivial_arbitrary!(f16);
+ trivial_arbitrary!(f128);
+
nonzero_arbitrary!(NonZeroU8, u8);
nonzero_arbitrary!(NonZeroU16, u16);
nonzero_arbitrary!(NonZeroU32, u32);
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index de808ffaf918..143fbb7ef825 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -17,6 +17,8 @@
#![feature(no_core)]
#![no_core]
+#![feature(f16)]
+#![feature(f128)]
mod arbitrary;
mod mem;
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index c620752b423a..5f02b82a51d2 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-27"
+channel = "nightly-2024-06-28"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/arbitrary/floats/non_standard_floats/expected b/tests/expected/arbitrary/floats/non_standard_floats/expected
new file mode 100644
index 000000000000..26db615201a6
--- /dev/null
+++ b/tests/expected/arbitrary/floats/non_standard_floats/expected
@@ -0,0 +1,31 @@
+Checking harness check_f128...
+
+Status: SATISFIED\
+Description: "This may be true"\
+in function check_f128
+
+Status: SATISFIED\
+Description: "This may also be true"\
+in function check_f128
+
+Status: SATISFIED\
+Description: "NaN should be valid float"\
+in function check_f128
+
+Checking harness check_f16...
+
+Status: SATISFIED\
+Description: "This may be true"\
+in function check_f16
+
+Status: SATISFIED\
+Description: "This may also be true"\
+in function check_f16
+
+Status: SATISFIED\
+Description: "NaN should be valid float"\
+in function check_f16
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/arbitrary/floats/non_standard_floats/main.rs b/tests/expected/arbitrary/floats/non_standard_floats/main.rs
new file mode 100644
index 000000000000..ebea6535b3d5
--- /dev/null
+++ b/tests/expected/arbitrary/floats/non_standard_floats/main.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Ensure that kani::any and kani::any_raw can be used with non-standard floats i.e f16 and f128.
+
+#![feature(f16)]
+#![feature(f128)]
+
+macro_rules! test_non_standard_floats {
+ ( $type: ty ) => {{
+ let v1 = kani::any::<$type>();
+ let v2 = kani::any::<$type>();
+ kani::cover!(v1 == v2, "This may be true");
+ kani::cover!(v1 != v2, "This may also be true");
+ kani::cover!(v1.is_nan(), "NaN should be valid float");
+ }};
+}
+
+#[kani::proof]
+fn check_f16() {
+ test_non_standard_floats!(f16);
+}
+
+#[kani::proof]
+fn check_f128() {
+ test_non_standard_floats!(f128);
+}
diff --git a/tests/expected/arbitrary/floats/expected b/tests/expected/arbitrary/floats/standard_floats/expected
similarity index 99%
rename from tests/expected/arbitrary/floats/expected
rename to tests/expected/arbitrary/floats/standard_floats/expected
index 4bb2fadacd7f..de3b67f28578 100644
--- a/tests/expected/arbitrary/floats/expected
+++ b/tests/expected/arbitrary/floats/standard_floats/expected
@@ -51,10 +51,8 @@ Status: SATISFIED\
Description: "Non-finite numbers are valid float"\
in function check_f32
-
** 6 of 6 cover properties satisfied
-
VERIFICATION:- SUCCESSFUL
Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/arbitrary/floats/main.rs b/tests/expected/arbitrary/floats/standard_floats/main.rs
similarity index 74%
rename from tests/expected/arbitrary/floats/main.rs
rename to tests/expected/arbitrary/floats/standard_floats/main.rs
index 1ad4de3ef3f7..c204643e9ab8 100644
--- a/tests/expected/arbitrary/floats/main.rs
+++ b/tests/expected/arbitrary/floats/standard_floats/main.rs
@@ -1,9 +1,12 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
-// Ensure that kani::any and kani::any_raw can be used with floats.
+// Ensure that kani::any and kani::any_raw can be used with standard floats i.e f32 and f64.
-macro_rules! test {
+#![feature(f16)]
+#![feature(f128)]
+
+macro_rules! test_standard_floats {
( $type: ty ) => {{
let v1 = kani::any::<$type>();
let v2 = kani::any::<$type>();
@@ -18,10 +21,10 @@ macro_rules! test {
#[kani::proof]
fn check_f32() {
- test!(f32);
+ test_standard_floats!(f32);
}
#[kani::proof]
fn check_f64() {
- test!(f64);
+ test_standard_floats!(f64);
}
diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs
index c04bd9b305f8..f8ebccdac02a 100644
--- a/tests/kani/FloatingPoint/main.rs
+++ b/tests/kani/FloatingPoint/main.rs
@@ -1,5 +1,9 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![feature(f16)]
+#![feature(f128)]
+
macro_rules! test_floats {
($ty:ty) => {
let a: $ty = kani::any();
@@ -26,6 +30,8 @@ fn main() {
assert!(1.1 == 1.1 * 1.0);
assert!(1.1 != 1.11 / 1.0);
+ test_floats!(f16);
test_floats!(f32);
test_floats!(f64);
+ test_floats!(f128);
}
diff --git a/tests/kani/Invariant/invariant_impls.rs b/tests/kani/Invariant/invariant_impls.rs
index 4f00f4134956..146c9731370d 100644
--- a/tests/kani/Invariant/invariant_impls.rs
+++ b/tests/kani/Invariant/invariant_impls.rs
@@ -3,6 +3,10 @@
//! Check the `Invariant` implementations that we include in the Kani library
//! with respect to the underlying type invariants.
+
+#![feature(f16)]
+#![feature(f128)]
+
extern crate kani;
use kani::Invariant;
@@ -29,6 +33,9 @@ fn check_safe_impls() {
check_safe_type!(i128);
check_safe_type!(isize);
+ check_safe_type!(f16);
+ check_safe_type!(f128);
+
check_safe_type!(f32);
check_safe_type!(f64);
From 67d6ac9adb2731d6942c26bbe42ab19e54bef3b3 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
<41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 2 Jul 2024 10:56:05 +0200
Subject: [PATCH 14/22] Automatic toolchain upgrade to nightly-2024-06-29
(#3315)
Update Rust toolchain from nightly-2024-06-28 to nightly-2024-06-29
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
https://github.com/rust-lang/rust/commit/9c3bc805dd9cb84019c124b9a50fdff1e62a7ec9
up to
https://github.com/rust-lang/rust/commit/e9e6e2e444c30c23a9c878a88fbc3978c2acad95.
---
rust-toolchain.toml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 5f02b82a51d2..be39f8068af9 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-28"
+channel = "nightly-2024-06-29"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
From 2fb97d28b457bf7eb86086ea44a3c5db23e41e38 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Tue, 2 Jul 2024 05:28:14 -0400
Subject: [PATCH 15/22] Upgrade toolchain to `nightly-2024-07-01` (#3314)
Upgrade toolchain to `nightly-2024-07-01` so we're up to date. No other
changes are required.
---
rust-toolchain.toml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index be39f8068af9..dfe3febbb927 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT
[toolchain]
-channel = "nightly-2024-06-29"
+channel = "nightly-2024-07-01"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
From d926482f7a724770d8f6818f312e8dda7b17738b Mon Sep 17 00:00:00 2001
From: Artem Agvanian
Date: Tue, 2 Jul 2024 12:07:47 -0700
Subject: [PATCH 16/22] Towards Proving Memory Initialization (#3264)
This PR enables automatic memory initialization proofs for raw pointers
in Kani. This is done without any extra instrumentation from the user.
Currently, due to high memory consumption and only partial support of
pointee types for which memory initialization proofs work, this feature
is gated behind `-Z uninit-checks` flag. Note that because it uses
shadow memory under the hood, programs using this feature need to pass
`-Z ghost-state` flag as well.
This PR is a part of working towards #3300.
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: Celina G. Val
---
kani-compiler/src/args.rs | 2 +
.../codegen_cprover_gotoc/codegen/contract.rs | 22 +
.../src/kani_middle/transform/body.rs | 178 ++++-
.../kani_middle/transform/check_uninit/mod.rs | 428 +++++++++++
.../transform/check_uninit/ty_layout.rs | 334 ++++++++
.../transform/check_uninit/uninit_visitor.rs | 713 ++++++++++++++++++
.../src/kani_middle/transform/check_values.rs | 80 +-
.../src/kani_middle/transform/contracts.rs | 2 +-
.../kani_middle/transform/kani_intrinsics.rs | 188 ++++-
.../src/kani_middle/transform/mod.rs | 24 +-
.../src/kani_middle/transform/stubs.rs | 4 +-
kani-driver/src/call_single_file.rs | 4 +
kani_metadata/src/unstable.rs | 2 +
library/kani/src/lib.rs | 1 +
library/kani/src/mem.rs | 10 +-
library/kani/src/mem_init.rs | 122 +++
library/kani_core/src/mem.rs | 12 +-
.../access-padding-uninit.rs | 16 +
.../uninit/access-padding-uninit/expected | 5 +
.../access-padding-via-cast.rs | 20 +
.../uninit/access-padding-via-cast/expected | 5 +
.../uninit/alloc-to-slice/alloc-to-slice.rs | 20 +
tests/expected/uninit/alloc-to-slice/expected | 5 +
.../expected/uninit/vec-read-bad-len/expected | 5 +
.../vec-read-bad-len/vec-read-bad-len.rs | 15 +
.../uninit/vec-read-semi-init/expected | 5 +
.../vec-read-semi-init/vec-read-semi-init.rs | 11 +
.../expected/uninit/vec-read-uninit/expected | 5 +
.../uninit/vec-read-uninit/vec-read-uninit.rs | 10 +
.../access-padding-enum-diverging-variants.rs | 34 +
.../access-padding-enum-multiple-variants.rs | 49 ++
.../access-padding-enum-single-field.rs | 34 +
.../access-padding-enum-single-variant.rs | 32 +
tests/perf/uninit/Cargo.toml | 14 +
tests/perf/uninit/expected | 1 +
tests/perf/uninit/src/lib.rs | 68 ++
tests/std-checks/core/mem.expected | 6 +-
tests/std-checks/core/slice.expected | 1 +
tests/std-checks/core/src/lib.rs | 1 +
tests/std-checks/core/src/mem.rs | 35 +
tests/std-checks/core/src/slice.rs | 30 +
41 files changed, 2500 insertions(+), 53 deletions(-)
create mode 100644 kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
create mode 100644 kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
create mode 100644 kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
create mode 100644 library/kani/src/mem_init.rs
create mode 100644 tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs
create mode 100644 tests/expected/uninit/access-padding-uninit/expected
create mode 100644 tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs
create mode 100644 tests/expected/uninit/access-padding-via-cast/expected
create mode 100644 tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
create mode 100644 tests/expected/uninit/alloc-to-slice/expected
create mode 100644 tests/expected/uninit/vec-read-bad-len/expected
create mode 100644 tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs
create mode 100644 tests/expected/uninit/vec-read-semi-init/expected
create mode 100644 tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs
create mode 100644 tests/expected/uninit/vec-read-uninit/expected
create mode 100644 tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs
create mode 100644 tests/kani/Uninit/access-padding-enum-diverging-variants.rs
create mode 100644 tests/kani/Uninit/access-padding-enum-multiple-variants.rs
create mode 100644 tests/kani/Uninit/access-padding-enum-single-field.rs
create mode 100644 tests/kani/Uninit/access-padding-enum-single-variant.rs
create mode 100644 tests/perf/uninit/Cargo.toml
create mode 100644 tests/perf/uninit/expected
create mode 100644 tests/perf/uninit/src/lib.rs
create mode 100644 tests/std-checks/core/slice.expected
create mode 100644 tests/std-checks/core/src/slice.rs
diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs
index b4d4eb3718d8..e4b7a4435b0f 100644
--- a/kani-compiler/src/args.rs
+++ b/kani-compiler/src/args.rs
@@ -88,4 +88,6 @@ pub enum ExtraChecks {
/// Check pointer validity when casting pointers to references.
/// See https://github.com/model-checking/kani/issues/2975.
PtrToRefCast,
+ /// Check for using uninitialized memory.
+ Uninit,
}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
index 0f27d3f119f7..d35015aa040d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -118,6 +118,27 @@ impl<'tcx> GotocCtx<'tcx> {
.typ
.clone();
+ let shadow_memory_assign = self
+ .tcx
+ .all_diagnostic_items(())
+ .name_to_id
+ .get(&rustc_span::symbol::Symbol::intern("KaniMemInitShadowMem"))
+ .map(|attr_id| {
+ self.tcx
+ .symbol_name(rustc_middle::ty::Instance::mono(self.tcx, *attr_id))
+ .name
+ .to_string()
+ })
+ .and_then(|shadow_memory_table| self.symbol_table.lookup(&shadow_memory_table).cloned())
+ .map(|shadow_memory_symbol| {
+ vec![Lambda::as_contract_for(
+ &goto_annotated_fn_typ,
+ None,
+ shadow_memory_symbol.to_expr(),
+ )]
+ })
+ .unwrap_or_default();
+
let assigns = modified_places
.into_iter()
.map(|local| {
@@ -127,6 +148,7 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(),
)
})
+ .chain(shadow_memory_assign)
.collect();
FunctionContract::new(assigns)
diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index 2bf424a1332d..22895bd8d20d 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -37,6 +37,13 @@ pub struct MutableBody {
span: Span,
}
+/// Denotes whether instrumentation should be inserted before or after the statement.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum InsertPosition {
+ Before,
+ After,
+}
+
impl MutableBody {
/// Get the basic blocks of this builder.
pub fn blocks(&self) -> &[BasicBlock] {
@@ -95,12 +102,13 @@ impl MutableBody {
from: Operand,
pointee_ty: Ty,
mutability: Mutability,
- before: &mut SourceInstruction,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
) -> Local {
assert!(from.ty(self.locals()).unwrap().kind().is_raw_ptr());
let target_ty = Ty::new_ptr(pointee_ty, mutability);
let rvalue = Rvalue::Cast(CastKind::PtrToPtr, from, target_ty);
- self.new_assignment(rvalue, before)
+ self.new_assignment(rvalue, source, position)
}
/// Add a new assignment for the given binary operation.
@@ -111,21 +119,27 @@ impl MutableBody {
bin_op: BinOp,
lhs: Operand,
rhs: Operand,
- before: &mut SourceInstruction,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
) -> Local {
let rvalue = Rvalue::BinaryOp(bin_op, lhs, rhs);
- self.new_assignment(rvalue, before)
+ self.new_assignment(rvalue, source, position)
}
/// Add a new assignment.
///
/// Return local where the result is saved.
- pub fn new_assignment(&mut self, rvalue: Rvalue, before: &mut SourceInstruction) -> Local {
- let span = before.span(&self.blocks);
+ pub fn new_assignment(
+ &mut self,
+ rvalue: Rvalue,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
+ ) -> Local {
+ let span = source.span(&self.blocks);
let ret_ty = rvalue.ty(&self.locals).unwrap();
let result = self.new_local(ret_ty, span, Mutability::Not);
let stmt = Statement { kind: StatementKind::Assign(Place::from(result), rvalue), span };
- self.insert_stmt(stmt, before);
+ self.insert_stmt(stmt, source, position);
result
}
@@ -139,6 +153,7 @@ impl MutableBody {
tcx: TyCtxt,
check_type: &CheckType,
source: &mut SourceInstruction,
+ position: InsertPosition,
value: Local,
msg: &str,
) {
@@ -168,7 +183,7 @@ impl MutableBody {
unwind: UnwindAction::Terminate,
};
let terminator = Terminator { kind, span };
- self.split_bb(source, terminator);
+ self.split_bb(source, position, terminator);
}
CheckType::Panic | CheckType::NoCore => {
tcx.sess
@@ -182,11 +197,55 @@ impl MutableBody {
}
}
- /// Split a basic block right before the source location and use the new terminator
- /// in the basic block that was split.
+ /// Add a new call to the basic block indicated by the given index.
+ ///
+ /// The new call will have the same span as the source instruction, and the basic block
+ /// will be split. The source instruction will be adjusted to point to the first instruction in
+ /// the new basic block.
+ pub fn add_call(
+ &mut self,
+ callee: &Instance,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
+ args: Vec,
+ destination: Place,
+ ) {
+ let new_bb = self.blocks.len();
+ let span = source.span(&self.blocks);
+ let callee_op =
+ Operand::Copy(Place::from(self.new_local(callee.ty(), span, Mutability::Not)));
+ let kind = TerminatorKind::Call {
+ func: callee_op,
+ args,
+ destination,
+ target: Some(new_bb),
+ unwind: UnwindAction::Terminate,
+ };
+ let terminator = Terminator { kind, span };
+ self.split_bb(source, position, terminator);
+ }
+
+ /// Split a basic block and use the new terminator in the basic block that was split.
///
/// The source is updated to point to the same instruction which is now in the new basic block.
- pub fn split_bb(&mut self, source: &mut SourceInstruction, new_term: Terminator) {
+ pub fn split_bb(
+ &mut self,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
+ new_term: Terminator,
+ ) {
+ match position {
+ InsertPosition::Before => {
+ self.split_bb_before(source, new_term);
+ }
+ InsertPosition::After => {
+ self.split_bb_after(source, new_term);
+ }
+ }
+ }
+
+ /// Split a basic block right before the source location.
+ fn split_bb_before(&mut self, source: &mut SourceInstruction, new_term: Terminator) {
let new_bb_idx = self.blocks.len();
let (idx, bb) = match source {
SourceInstruction::Statement { idx, bb } => {
@@ -196,9 +255,9 @@ impl MutableBody {
(orig_idx, orig_bb)
}
SourceInstruction::Terminator { bb } => {
- let orig_bb = *bb;
+ let (orig_idx, orig_bb) = (self.blocks[*bb].statements.len(), *bb);
*bb = new_bb_idx;
- (self.blocks[orig_bb].statements.len(), orig_bb)
+ (orig_idx, orig_bb)
}
};
let old_term = mem::replace(&mut self.blocks[bb].terminator, new_term);
@@ -208,16 +267,95 @@ impl MutableBody {
self.blocks.push(new_bb);
}
- /// Insert statement before the source instruction and update the source as needed.
- pub fn insert_stmt(&mut self, new_stmt: Statement, before: &mut SourceInstruction) {
- match before {
+ /// Split a basic block right after the source location.
+ fn split_bb_after(&mut self, source: &mut SourceInstruction, mut new_term: Terminator) {
+ let new_bb_idx = self.blocks.len();
+ match source {
+ // Split the current block after the statement located at `source`
+ // and move the remaining statements into the new one.
SourceInstruction::Statement { idx, bb } => {
- self.blocks[*bb].statements.insert(*idx, new_stmt);
- *idx += 1;
+ let (orig_idx, orig_bb) = (*idx, *bb);
+ *idx = 0;
+ *bb = new_bb_idx;
+ let old_term = mem::replace(&mut self.blocks[orig_bb].terminator, new_term);
+ let bb_stmts = &mut self.blocks[orig_bb].statements;
+ let remaining = bb_stmts.split_off(orig_idx + 1);
+ let new_bb = BasicBlock { statements: remaining, terminator: old_term };
+ self.blocks.push(new_bb);
}
+ // Make the terminator at `source` point at the new block,
+ // the terminator of which is a simple Goto instruction.
SourceInstruction::Terminator { bb } => {
- // Append statements at the end of the basic block.
- self.blocks[*bb].statements.push(new_stmt);
+ let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
+ // Kani can only instrument function calls like this.
+ match (&mut current_terminator.kind, &mut new_term.kind) {
+ (
+ TerminatorKind::Call { target: Some(target_bb), .. },
+ TerminatorKind::Call { target: Some(new_target_bb), .. },
+ ) => {
+ // Set the new terminator to point where previous terminator pointed.
+ *new_target_bb = *target_bb;
+ // Point the current terminator to the new terminator's basic block.
+ *target_bb = new_bb_idx;
+ // Update the current poisition.
+ *bb = new_bb_idx;
+ self.blocks.push(BasicBlock { statements: vec![], terminator: new_term });
+ }
+ _ => unimplemented!("Kani can only split blocks after calls."),
+ };
+ }
+ };
+ }
+
+ /// Insert statement before or after the source instruction and update the source as needed.
+ pub fn insert_stmt(
+ &mut self,
+ new_stmt: Statement,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
+ ) {
+ match position {
+ InsertPosition::Before => {
+ match source {
+ SourceInstruction::Statement { idx, bb } => {
+ self.blocks[*bb].statements.insert(*idx, new_stmt);
+ *idx += 1;
+ }
+ SourceInstruction::Terminator { bb } => {
+ // Append statements at the end of the basic block.
+ self.blocks[*bb].statements.push(new_stmt);
+ }
+ }
+ }
+ InsertPosition::After => {
+ let new_bb_idx = self.blocks.len();
+ let span = source.span(&self.blocks);
+ match source {
+ SourceInstruction::Statement { idx, bb } => {
+ self.blocks[*bb].statements.insert(*idx + 1, new_stmt);
+ *idx += 1;
+ }
+ SourceInstruction::Terminator { bb } => {
+ // Create a new basic block, as we need to append a statement after the terminator.
+ let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
+ // Kani can only instrument function calls in this way.
+ match &mut current_terminator.kind {
+ TerminatorKind::Call { target: Some(target_bb), .. } => {
+ *source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx };
+ let new_bb = BasicBlock {
+ statements: vec![new_stmt],
+ terminator: Terminator {
+ kind: TerminatorKind::Goto { target: *target_bb },
+ span,
+ },
+ };
+ *target_bb = new_bb_idx;
+ self.blocks.push(new_bb);
+ }
+ _ => unimplemented!("Kani can only insert statements after calls."),
+ };
+ }
+ }
}
}
}
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
new file mode 100644
index 000000000000..6665ab697287
--- /dev/null
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
@@ -0,0 +1,428 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Implement a transformation pass that instruments the code to detect possible UB due to
+//! the accesses to uninitialized memory.
+
+use crate::args::ExtraChecks;
+use crate::kani_middle::find_fn_def;
+use crate::kani_middle::transform::body::{
+ CheckType, InsertPosition, MutableBody, SourceInstruction,
+};
+use crate::kani_middle::transform::{TransformPass, TransformationType};
+use crate::kani_queries::QueryDb;
+use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{AggregateKind, Body, ConstOperand, Mutability, Operand, Place, Rvalue};
+use stable_mir::ty::{
+ FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy,
+};
+use stable_mir::CrateDef;
+use std::collections::{HashMap, HashSet};
+use std::fmt::Debug;
+use tracing::{debug, trace};
+
+mod ty_layout;
+mod uninit_visitor;
+
+pub use ty_layout::{PointeeInfo, PointeeLayout};
+use uninit_visitor::{CheckUninitVisitor, InitRelevantInstruction, MemoryInitOp};
+
+const SKIPPED_DIAGNOSTIC_ITEMS: &[&str] =
+ &["KaniIsUnitPtrInitialized", "KaniSetUnitPtrInitialized"];
+
+/// Instrument the code with checks for uninitialized memory.
+#[derive(Debug)]
+pub struct UninitPass {
+ pub check_type: CheckType,
+ /// Used to cache FnDef lookups of injected memory initialization functions.
+ pub mem_init_fn_cache: HashMap<&'static str, FnDef>,
+}
+
+impl TransformPass for UninitPass {
+ fn transformation_type() -> TransformationType
+ where
+ Self: Sized,
+ {
+ TransformationType::Instrumentation
+ }
+
+ fn is_enabled(&self, query_db: &QueryDb) -> bool
+ where
+ Self: Sized,
+ {
+ let args = query_db.args();
+ args.ub_check.contains(&ExtraChecks::Uninit)
+ }
+
+ 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.
+ if tcx
+ .get_diagnostic_name(rustc_internal::internal(tcx, instance.def.def_id()))
+ .map(|diagnostic_name| {
+ SKIPPED_DIAGNOSTIC_ITEMS.contains(&diagnostic_name.to_ident_string().as_str())
+ })
+ .unwrap_or(false)
+ {
+ return (false, body);
+ }
+
+ let mut new_body = MutableBody::from(body);
+ let orig_len = new_body.blocks().len();
+
+ // 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
+ // turn, gets moved to the next basic block. Hence, we would not need to look at the
+ // instruction again as a part of new basic block. However, if the check is inserted after the
+ // source instruction, we still need to look at the first statement of the new basic block, so
+ // we need to keep track of which basic blocks were created as a part of injecting checks after
+ // the source instruction.
+ let mut skip_first = HashSet::new();
+
+ // Do not cache body.blocks().len() since it will change as we add new checks.
+ let mut bb_idx = 0;
+ while bb_idx < new_body.blocks().len() {
+ if let Some(candidate) =
+ CheckUninitVisitor::find_next(&new_body, bb_idx, skip_first.contains(&bb_idx))
+ {
+ self.build_check_for_instruction(tcx, &mut new_body, candidate, &mut skip_first);
+ bb_idx += 1
+ } else {
+ bb_idx += 1;
+ };
+ }
+ (orig_len != new_body.blocks().len(), new_body.into())
+ }
+}
+
+impl UninitPass {
+ /// Inject memory initialization checks for each operation in an instruction.
+ fn build_check_for_instruction(
+ &mut self,
+ tcx: TyCtxt,
+ body: &mut MutableBody,
+ instruction: InitRelevantInstruction,
+ skip_first: &mut HashSet,
+ ) {
+ debug!(?instruction, "build_check");
+ let mut source = instruction.source;
+ for operation in instruction.before_instruction {
+ self.build_check_for_operation(tcx, body, &mut source, operation, skip_first);
+ }
+ for operation in instruction.after_instruction {
+ self.build_check_for_operation(tcx, body, &mut source, operation, skip_first);
+ }
+ }
+
+ /// Inject memory initialization check for an operation.
+ fn build_check_for_operation(
+ &mut self,
+ tcx: TyCtxt,
+ body: &mut MutableBody,
+ source: &mut SourceInstruction,
+ operation: MemoryInitOp,
+ skip_first: &mut HashSet,
+ ) {
+ if let MemoryInitOp::Unsupported { reason } = &operation {
+ collect_skipped(&operation, body, skip_first);
+ self.unsupported_check(tcx, body, source, operation.position(), reason);
+ return;
+ };
+
+ let pointee_ty_info = {
+ let ptr_operand = operation.mk_operand(body, source);
+ let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap();
+ let pointee_ty = match ptr_operand_ty.kind() {
+ TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty,
+ _ => {
+ unreachable!(
+ "Should only build checks for raw pointers, `{ptr_operand_ty}` encountered."
+ )
+ }
+ };
+ match PointeeInfo::from_ty(pointee_ty) {
+ Ok(type_info) => type_info,
+ Err(_) => {
+ let reason = format!(
+ "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.",
+ );
+ collect_skipped(&operation, body, skip_first);
+ self.unsupported_check(tcx, body, source, operation.position(), &reason);
+ return;
+ }
+ }
+ };
+
+ match operation {
+ MemoryInitOp::Check { .. } => {
+ self.build_get_and_check(tcx, body, source, operation, pointee_ty_info, skip_first)
+ }
+ MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } => {
+ self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first)
+ }
+ MemoryInitOp::Unsupported { .. } => {
+ unreachable!()
+ }
+ }
+ }
+
+ /// Inject a load from shadow memory tracking memory initialization and an assertion that all
+ /// non-padding bytes are initialized.
+ fn build_get_and_check(
+ &mut self,
+ tcx: TyCtxt,
+ body: &mut MutableBody,
+ source: &mut SourceInstruction,
+ operation: MemoryInitOp,
+ pointee_info: PointeeInfo,
+ skip_first: &mut HashSet,
+ ) {
+ let ret_place = Place {
+ local: body.new_local(Ty::bool_ty(), source.span(body.blocks()), Mutability::Not),
+ projection: vec![],
+ };
+ let ptr_operand = operation.mk_operand(body, source);
+ match pointee_info.layout() {
+ PointeeLayout::Sized { layout } => {
+ let is_ptr_initialized_instance = resolve_mem_init_fn(
+ get_mem_init_fn_def(tcx, "KaniIsPtrInitialized", &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()],
+ ret_place.clone(),
+ );
+ }
+ PointeeLayout::Slice { element_layout } => {
+ // Since `str`` is a separate type, need to differentiate between [T] and str.
+ let (slicee_ty, diagnostic) = match pointee_info.ty().kind() {
+ TyKind::RigidTy(RigidTy::Slice(slicee_ty)) => {
+ (slicee_ty, "KaniIsSlicePtrInitialized")
+ }
+ TyKind::RigidTy(RigidTy::Str) => {
+ (Ty::unsigned_ty(UintTy::U8), "KaniIsStrPtrInitialized")
+ }
+ _ => unreachable!(),
+ };
+ let is_ptr_initialized_instance = resolve_mem_init_fn(
+ get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache),
+ element_layout.len(),
+ slicee_ty,
+ );
+ let layout_operand =
+ mk_layout_operand(body, source, operation.position(), &element_layout);
+ collect_skipped(&operation, body, skip_first);
+ body.add_call(
+ &is_ptr_initialized_instance,
+ source,
+ operation.position(),
+ vec![ptr_operand.clone(), layout_operand],
+ ret_place.clone(),
+ );
+ }
+ PointeeLayout::TraitObject => {
+ collect_skipped(&operation, body, skip_first);
+ let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
+ self.unsupported_check(tcx, body, source, operation.position(), reason);
+ return;
+ }
+ };
+
+ // Make sure all non-padding bytes are initialized.
+ collect_skipped(&operation, body, skip_first);
+ let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap();
+ body.add_check(
+ tcx,
+ &self.check_type,
+ source,
+ operation.position(),
+ ret_place.local,
+ &format!("Undefined Behavior: Reading from an uninitialized pointer of type `{ptr_operand_ty}`"),
+ )
+ }
+
+ /// Inject a store into shadow memory tracking memory initialization to initialize or
+ /// deinitialize all non-padding bytes.
+ fn build_set(
+ &mut self,
+ tcx: TyCtxt,
+ body: &mut MutableBody,
+ source: &mut SourceInstruction,
+ operation: MemoryInitOp,
+ pointee_info: PointeeInfo,
+ skip_first: &mut HashSet,
+ ) {
+ let ret_place = Place {
+ local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not),
+ projection: vec![],
+ };
+ let ptr_operand = operation.mk_operand(body, source);
+ let value = operation.expect_value();
+
+ match pointee_info.layout() {
+ PointeeLayout::Sized { layout } => {
+ let set_ptr_initialized_instance = resolve_mem_init_fn(
+ get_mem_init_fn_def(tcx, "KaniSetPtrInitialized", &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),
+ }),
+ ],
+ ret_place,
+ );
+ }
+ PointeeLayout::Slice { element_layout } => {
+ // Since `str`` is a separate type, need to differentiate between [T] and str.
+ let (slicee_ty, diagnostic) = match pointee_info.ty().kind() {
+ TyKind::RigidTy(RigidTy::Slice(slicee_ty)) => {
+ (slicee_ty, "KaniSetSlicePtrInitialized")
+ }
+ TyKind::RigidTy(RigidTy::Str) => {
+ (Ty::unsigned_ty(UintTy::U8), "KaniSetStrPtrInitialized")
+ }
+ _ => unreachable!(),
+ };
+ let set_ptr_initialized_instance = resolve_mem_init_fn(
+ get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache),
+ element_layout.len(),
+ slicee_ty,
+ );
+ let layout_operand =
+ mk_layout_operand(body, source, operation.position(), &element_layout);
+ collect_skipped(&operation, body, skip_first);
+ body.add_call(
+ &set_ptr_initialized_instance,
+ source,
+ operation.position(),
+ vec![
+ ptr_operand,
+ layout_operand,
+ Operand::Constant(ConstOperand {
+ span: source.span(body.blocks()),
+ user_ty: None,
+ const_: MirConst::from_bool(value),
+ }),
+ ],
+ ret_place,
+ );
+ }
+ PointeeLayout::TraitObject => {
+ unreachable!("Cannot change the initialization state of a trait object directly.");
+ }
+ };
+ }
+
+ fn unsupported_check(
+ &self,
+ tcx: TyCtxt,
+ body: &mut MutableBody,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
+ reason: &str,
+ ) {
+ let span = source.span(body.blocks());
+ let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
+ const_: MirConst::from_bool(false),
+ span,
+ user_ty: None,
+ }));
+ let result = body.new_assignment(rvalue, source, position);
+ body.add_check(tcx, &self.check_type, source, position, result, reason);
+ }
+}
+
+/// Create an operand from a bit array that represents a byte mask for a type layout where padding
+/// bytes are marked as `false` and data bytes are marked as `true`.
+///
+/// For example, the layout for:
+/// ```
+/// [repr(C)]
+/// struct {
+/// a: u16,
+/// b: u8
+/// }
+/// ```
+/// will have the following byte mask `[true, true, true, false]`.
+pub fn mk_layout_operand(
+ body: &mut MutableBody,
+ source: &mut SourceInstruction,
+ position: InsertPosition,
+ layout_byte_mask: &[bool],
+) -> Operand {
+ Operand::Move(Place {
+ local: body.new_assignment(
+ Rvalue::Aggregate(
+ AggregateKind::Array(Ty::bool_ty()),
+ layout_byte_mask
+ .iter()
+ .map(|byte| {
+ Operand::Constant(ConstOperand {
+ span: source.span(body.blocks()),
+ user_ty: None,
+ const_: MirConst::from_bool(*byte),
+ })
+ })
+ .collect(),
+ ),
+ source,
+ position,
+ ),
+ projection: vec![],
+ })
+}
+
+/// If injecting a new call to the function before the current statement, need to skip the original
+/// statement when analyzing it as a part of the new basic block.
+fn collect_skipped(operation: &MemoryInitOp, body: &MutableBody, skip_first: &mut HashSet) {
+ if operation.position() == InsertPosition::Before {
+ let new_bb_idx = body.blocks().len();
+ skip_first.insert(new_bb_idx);
+ }
+}
+
+/// Retrieve a function definition by diagnostic string, caching the result.
+pub fn get_mem_init_fn_def(
+ tcx: TyCtxt,
+ diagnostic: &'static str,
+ cache: &mut HashMap<&'static str, FnDef>,
+) -> FnDef {
+ let entry = cache.entry(diagnostic).or_insert_with(|| find_fn_def(tcx, diagnostic).unwrap());
+ *entry
+}
+
+/// Resolves a given memory initialization function with passed type parameters.
+pub fn resolve_mem_init_fn(fn_def: FnDef, layout_size: usize, associated_type: Ty) -> Instance {
+ Instance::resolve(
+ fn_def,
+ &GenericArgs(vec![
+ GenericArgKind::Const(TyConst::try_from_target_usize(layout_size as u64).unwrap()),
+ GenericArgKind::Type(associated_type),
+ ]),
+ )
+ .unwrap()
+}
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
new file mode 100644
index 000000000000..09116230af80
--- /dev/null
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs
@@ -0,0 +1,334 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Utility functions that help calculate type layout.
+
+use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape};
+use stable_mir::target::{MachineInfo, MachineSize};
+use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Ty, TyKind, UintTy};
+use stable_mir::CrateDef;
+
+/// Represents a chunk of data bytes in a data structure.
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+struct DataBytes {
+ /// Offset in bytes.
+ offset: usize,
+ /// Size of this data chunk.
+ size: MachineSize,
+}
+
+/// Bytewise mask, representing which bytes of a type are data and which are padding. Here, `false`
+/// represents padding bytes and `true` represents data bytes.
+type Layout = Vec;
+
+/// Create a byte-wise mask from known chunks of data bytes.
+fn generate_byte_mask(size_in_bytes: usize, data_chunks: Vec) -> Vec {
+ let mut layout_mask = vec![false; size_in_bytes];
+ for data_bytes in data_chunks.iter() {
+ for layout_item in
+ layout_mask.iter_mut().skip(data_bytes.offset).take(data_bytes.size.bytes())
+ {
+ *layout_item = true;
+ }
+ }
+ layout_mask
+}
+
+// Depending on whether the type is statically or dynamically sized,
+// the layout of the element or the layout of the actual type is returned.
+pub enum PointeeLayout {
+ /// Layout of sized objects.
+ Sized { layout: Layout },
+ /// Layout of slices, *const/mut str is included in this case and treated as *const/mut [u8].
+ Slice { element_layout: Layout },
+ /// Trait objects have an arbitrary layout.
+ TraitObject,
+}
+
+pub struct PointeeInfo {
+ pointee_ty: Ty,
+ layout: PointeeLayout,
+}
+
+impl PointeeInfo {
+ pub fn from_ty(ty: Ty) -> Result {
+ match ty.kind() {
+ TyKind::RigidTy(rigid_ty) => match rigid_ty {
+ RigidTy::Str => {
+ let slicee_ty = Ty::unsigned_ty(UintTy::U8);
+ let size_in_bytes = slicee_ty.layout().unwrap().shape().size.bytes();
+ let data_chunks = data_bytes_for_ty(&MachineInfo::target(), slicee_ty, 0)?;
+ let layout = PointeeLayout::Slice {
+ element_layout: generate_byte_mask(size_in_bytes, data_chunks),
+ };
+ Ok(PointeeInfo { pointee_ty: ty, layout })
+ }
+ RigidTy::Slice(slicee_ty) => {
+ let size_in_bytes = slicee_ty.layout().unwrap().shape().size.bytes();
+ let data_chunks = data_bytes_for_ty(&MachineInfo::target(), slicee_ty, 0)?;
+ let layout = PointeeLayout::Slice {
+ element_layout: generate_byte_mask(size_in_bytes, data_chunks),
+ };
+ Ok(PointeeInfo { pointee_ty: ty, layout })
+ }
+ RigidTy::Dynamic(..) => {
+ Ok(PointeeInfo { pointee_ty: ty, layout: PointeeLayout::TraitObject })
+ }
+ _ => {
+ if ty.layout().unwrap().shape().is_sized() {
+ let size_in_bytes = ty.layout().unwrap().shape().size.bytes();
+ let data_chunks = data_bytes_for_ty(&MachineInfo::target(), ty, 0)?;
+ let layout = PointeeLayout::Sized {
+ layout: generate_byte_mask(size_in_bytes, data_chunks),
+ };
+ Ok(PointeeInfo { pointee_ty: ty, layout })
+ } else {
+ Err(format!("Cannot determine type layout for type `{ty}`"))
+ }
+ }
+ },
+ TyKind::Alias(..) | TyKind::Param(..) | TyKind::Bound(..) => {
+ unreachable!("Should only encounter monomorphized types at this point.")
+ }
+ }
+ }
+
+ pub fn ty(&self) -> &Ty {
+ &self.pointee_ty
+ }
+
+ pub fn layout(&self) -> &PointeeLayout {
+ &self.layout
+ }
+}
+
+/// Retrieve a set of data bytes with offsets for a type.
+fn data_bytes_for_ty(
+ machine_info: &MachineInfo,
+ ty: Ty,
+ current_offset: usize,
+) -> Result, String> {
+ let layout = ty.layout().unwrap().shape();
+
+ match layout.fields {
+ FieldsShape::Primitive => Ok(vec![match layout.abi {
+ ValueAbi::Scalar(Scalar::Initialized { value, .. }) => {
+ DataBytes { offset: current_offset, size: value.size(machine_info) }
+ }
+ _ => unreachable!("FieldsShape::Primitive with a different ABI than ValueAbi::Scalar"),
+ }]),
+ FieldsShape::Array { stride, count } if count > 0 => {
+ let TyKind::RigidTy(RigidTy::Array(elem_ty, _)) = ty.kind() else { unreachable!() };
+ let elem_data_bytes = data_bytes_for_ty(machine_info, elem_ty, current_offset)?;
+ let mut result = vec![];
+ if !elem_data_bytes.is_empty() {
+ for idx in 0..count {
+ let idx: usize = idx.try_into().unwrap();
+ let elem_offset = idx * stride.bytes();
+ let mut next_data_bytes = elem_data_bytes
+ .iter()
+ .cloned()
+ .map(|mut req| {
+ req.offset += elem_offset;
+ req
+ })
+ .collect::>();
+ result.append(&mut next_data_bytes)
+ }
+ }
+ Ok(result)
+ }
+ FieldsShape::Arbitrary { ref offsets } => {
+ match ty.kind().rigid().expect(&format!("unexpected type: {ty:?}")) {
+ RigidTy::Adt(def, args) => {
+ match def.kind() {
+ AdtKind::Enum => {
+ // Support basic enumeration forms
+ let ty_variants = def.variants();
+ match layout.variants {
+ VariantsShape::Single { index } => {
+ // Only one variant is reachable. This behaves like a struct.
+ let fields = ty_variants[index.to_index()].fields();
+ let mut fields_data_bytes = vec![];
+ for idx in layout.fields.fields_by_offset_order() {
+ let field_offset = offsets[idx].bytes();
+ let field_ty = fields[idx].ty_with_args(&args);
+ fields_data_bytes.append(&mut data_bytes_for_ty(
+ machine_info,
+ field_ty,
+ field_offset + current_offset,
+ )?);
+ }
+ Ok(fields_data_bytes)
+ }
+ VariantsShape::Multiple {
+ tag_encoding: TagEncoding::Niche { .. },
+ ..
+ } => {
+ Err(format!("Unsupported Enum `{}` check", def.trimmed_name()))?
+ }
+ VariantsShape::Multiple { variants, tag, .. } => {
+ // Retrieve data bytes for the tag.
+ let tag_size = match tag {
+ Scalar::Initialized { value, .. } => {
+ value.size(&machine_info)
+ }
+ Scalar::Union { .. } => {
+ unreachable!("Enum tag should not be a union.")
+ }
+ };
+ // For enums, tag is the only field and should have offset of 0.
+ assert!(offsets.len() == 1 && offsets[0].bytes() == 0);
+ let tag_data_bytes =
+ vec![DataBytes { offset: current_offset, size: tag_size }];
+
+ // Retrieve data bytes for the fields.
+ let mut fields_data_bytes = vec![];
+ // Iterate over all variants for the enum.
+ for (index, variant) in variants.iter().enumerate() {
+ let mut field_data_bytes_for_variant = vec![];
+ let fields = ty_variants[index].fields();
+ // Get offsets of all fields in a variant.
+ let FieldsShape::Arbitrary { offsets: field_offsets } =
+ variant.fields.clone()
+ else {
+ unreachable!()
+ };
+ for field_idx in variant.fields.fields_by_offset_order() {
+ let field_offset = field_offsets[field_idx].bytes();
+ let field_ty = fields[field_idx].ty_with_args(&args);
+ field_data_bytes_for_variant.append(
+ &mut data_bytes_for_ty(
+ machine_info,
+ field_ty,
+ field_offset + current_offset,
+ )?,
+ );
+ }
+ fields_data_bytes.push(field_data_bytes_for_variant);
+ }
+
+ if fields_data_bytes.is_empty() {
+ // If there are no fields, return the tag data bytes.
+ Ok(tag_data_bytes)
+ } else if fields_data_bytes.iter().all(
+ |data_bytes_for_variant| {
+ // Byte layout for variant N.
+ let byte_mask_for_variant = generate_byte_mask(
+ layout.size.bytes(),
+ data_bytes_for_variant.clone(),
+ );
+ // Byte layout for variant 0.
+ let byte_mask_for_first = generate_byte_mask(
+ layout.size.bytes(),
+ fields_data_bytes.first().unwrap().clone(),
+ );
+ byte_mask_for_variant == byte_mask_for_first
+ },
+ ) {
+ // If all fields have the same layout, return fields data
+ // bytes.
+ let mut total_data_bytes = tag_data_bytes;
+ let mut field_data_bytes =
+ fields_data_bytes.first().unwrap().clone();
+ total_data_bytes.append(&mut field_data_bytes);
+ Ok(total_data_bytes)
+ } else {
+ // Struct has multiple padding variants, Kani cannot
+ // differentiate between them.
+ Err(format!(
+ "Unsupported Enum `{}` check",
+ def.trimmed_name()
+ ))
+ }
+ }
+ }
+ }
+ AdtKind::Union => unreachable!(),
+ AdtKind::Struct => {
+ let mut struct_data_bytes = vec![];
+ let fields = def.variants_iter().next().unwrap().fields();
+ for idx in layout.fields.fields_by_offset_order() {
+ let field_offset = offsets[idx].bytes();
+ let field_ty = fields[idx].ty_with_args(&args);
+ struct_data_bytes.append(&mut data_bytes_for_ty(
+ machine_info,
+ field_ty,
+ field_offset + current_offset,
+ )?);
+ }
+ Ok(struct_data_bytes)
+ }
+ }
+ }
+ RigidTy::Pat(base_ty, ..) => {
+ // This is similar to a structure with one field and with niche defined.
+ let mut pat_data_bytes = vec![];
+ pat_data_bytes.append(&mut data_bytes_for_ty(machine_info, *base_ty, 0)?);
+ Ok(pat_data_bytes)
+ }
+ RigidTy::Tuple(tys) => {
+ let mut tuple_data_bytes = vec![];
+ for idx in layout.fields.fields_by_offset_order() {
+ let field_offset = offsets[idx].bytes();
+ let field_ty = tys[idx];
+ tuple_data_bytes.append(&mut data_bytes_for_ty(
+ machine_info,
+ field_ty,
+ field_offset + current_offset,
+ )?);
+ }
+ Ok(tuple_data_bytes)
+ }
+ RigidTy::Bool
+ | RigidTy::Char
+ | RigidTy::Int(_)
+ | RigidTy::Uint(_)
+ | RigidTy::Float(_)
+ | RigidTy::Never => {
+ unreachable!("Expected primitive layout for {ty:?}")
+ }
+ RigidTy::Str | RigidTy::Slice(_) | RigidTy::Array(_, _) => {
+ unreachable!("Expected array layout for {ty:?}")
+ }
+ RigidTy::RawPtr(_, _) | RigidTy::Ref(_, _, _) => Ok(match layout.abi {
+ ValueAbi::Scalar(Scalar::Initialized { value, .. }) => {
+ // Thin pointer, ABI is a single scalar.
+ vec![DataBytes { offset: current_offset, size: value.size(machine_info) }]
+ }
+ ValueAbi::ScalarPair(
+ Scalar::Initialized { value: value_first, .. },
+ Scalar::Initialized { value: value_second, .. },
+ ) => {
+ // Fat pointer, ABI is a scalar pair.
+ let FieldsShape::Arbitrary { offsets } = layout.fields else {
+ unreachable!()
+ };
+ // Since this is a scalar pair, only 2 elements are in the offsets vec.
+ assert!(offsets.len() == 2);
+ vec![
+ DataBytes {
+ offset: current_offset + offsets[0].bytes(),
+ size: value_first.size(machine_info),
+ },
+ DataBytes {
+ offset: current_offset + offsets[1].bytes(),
+ size: value_second.size(machine_info),
+ },
+ ]
+ }
+ _ => unreachable!("RigidTy::RawPtr | RigidTy::Ref with a non-scalar ABI."),
+ }),
+ RigidTy::FnDef(_, _)
+ | RigidTy::FnPtr(_)
+ | RigidTy::Closure(_, _)
+ | RigidTy::Coroutine(_, _, _)
+ | RigidTy::CoroutineWitness(_, _)
+ | RigidTy::Foreign(_)
+ | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")),
+ }
+ }
+ FieldsShape::Union(_) => Err(format!("Unsupported {ty:?}")),
+ FieldsShape::Array { .. } => Ok(vec![]),
+ }
+}
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
new file mode 100644
index 000000000000..19b13c6ab8b6
--- /dev/null
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
@@ -0,0 +1,713 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Visitor that collects all instructions relevant to uninitialized memory access.
+
+use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
+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,
+};
+use stable_mir::ty::{ConstantKind, MirConst, RigidTy, Span, TyKind, UintTy};
+use strum_macros::AsRefStr;
+
+/// 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 `count * sizeof(operand)` bytes.
+ Check { 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 },
+ /// 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 },
+ /// Unsupported memory initialization operation.
+ Unsupported { reason: String },
+}
+
+impl MemoryInitOp {
+ /// Produce an operand for the relevant memory initialization related operation. This is mostly
+ /// required so that the analysis can create a new local to take a reference in
+ /// `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::SetRef { operand, .. } => Operand::Copy(Place {
+ local: {
+ let place = match operand {
+ Operand::Copy(place) | Operand::Move(place) => place,
+ Operand::Constant(_) => unreachable!(),
+ };
+ body.new_assignment(
+ Rvalue::AddressOf(Mutability::Not, place.clone()),
+ source,
+ self.position(),
+ )
+ },
+ projection: vec![],
+ }),
+ MemoryInitOp::Unsupported { .. } => unreachable!(),
+ }
+ }
+
+ pub fn expect_count(&self) -> Operand {
+ match self {
+ MemoryInitOp::Check { count, .. }
+ | MemoryInitOp::Set { count, .. }
+ | MemoryInitOp::SetRef { count, .. } => count.clone(),
+ MemoryInitOp::Unsupported { .. } => unreachable!(),
+ }
+ }
+
+ pub fn expect_value(&self) -> bool {
+ match self {
+ MemoryInitOp::Set { value, .. } | MemoryInitOp::SetRef { value, .. } => *value,
+ MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => unreachable!(),
+ }
+ }
+
+ pub fn position(&self) -> InsertPosition {
+ match self {
+ MemoryInitOp::Set { position, .. } | MemoryInitOp::SetRef { position, .. } => *position,
+ MemoryInitOp::Check { .. } | MemoryInitOp::Unsupported { .. } => InsertPosition::Before,
+ }
+ }
+}
+
+/// Represents an instruction in the source code together with all memory initialization checks/sets
+/// that are connected to the memory used in this instruction and whether they should be inserted
+/// before or after the instruction.
+#[derive(Clone, Debug)]
+pub struct InitRelevantInstruction {
+ /// The instruction that affects the state of the memory.
+ pub source: SourceInstruction,
+ /// All memory-related operations that should happen after the instruction.
+ pub before_instruction: Vec,
+ /// All memory-related operations that should happen after the instruction.
+ pub after_instruction: Vec,
+}
+
+impl InitRelevantInstruction {
+ pub fn push_operation(&mut self, source_op: MemoryInitOp) {
+ match source_op.position() {
+ InsertPosition::Before => self.before_instruction.push(source_op),
+ InsertPosition::After => self.after_instruction.push(source_op),
+ }
+ }
+}
+
+pub struct CheckUninitVisitor<'a> {
+ locals: &'a [LocalDecl],
+ /// Whether we should skip the next instruction, since it might've been instrumented already.
+ /// When we instrument an instruction, we partition the basic block, and the instruction that
+ /// may trigger UB becomes the first instruction of the basic block, which we need to skip
+ /// later.
+ skip_next: bool,
+ /// The instruction being visited at a given point.
+ current: SourceInstruction,
+ /// The target instruction that should be verified.
+ pub target: Option,
+ /// The basic block being visited.
+ bb: BasicBlockIdx,
+}
+
+impl<'a> CheckUninitVisitor<'a> {
+ pub fn find_next(
+ body: &'a MutableBody,
+ bb: BasicBlockIdx,
+ skip_first: bool,
+ ) -> Option {
+ let mut visitor = CheckUninitVisitor {
+ locals: body.locals(),
+ skip_next: skip_first,
+ current: SourceInstruction::Statement { idx: 0, bb },
+ target: None,
+ bb,
+ };
+ visitor.visit_basic_block(&body.blocks()[bb]);
+ visitor.target
+ }
+
+ fn push_target(&mut self, source_op: MemoryInitOp) {
+ let target = self.target.get_or_insert_with(|| InitRelevantInstruction {
+ source: self.current,
+ after_instruction: vec![],
+ before_instruction: vec![],
+ });
+ target.push_operation(source_op);
+ }
+}
+
+impl<'a> MirVisitor for CheckUninitVisitor<'a> {
+ fn visit_statement(&mut self, stmt: &Statement, location: Location) {
+ if self.skip_next {
+ self.skip_next = false;
+ } else if self.target.is_none() {
+ // Leave it as an exhaustive match to be notified when a new kind is added.
+ match &stmt.kind {
+ 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 {
+ operand: copy.src.clone(),
+ count: copy.count.clone(),
+ });
+ // Destimation is a *mut T so it gets initialized.
+ self.push_target(MemoryInitOp::Set {
+ operand: copy.dst.clone(),
+ count: copy.count.clone(),
+ value: true,
+ position: InsertPosition::After,
+ });
+ }
+ StatementKind::Assign(place, rvalue) => {
+ // First check rvalue.
+ self.visit_rvalue(rvalue, location);
+ // Check whether we are assigning into a dereference (*ptr = _).
+ if let Some(place_without_deref) = try_remove_topmost_deref(place) {
+ // First, check that we are not dereferencing extra pointers along the way
+ // (e.g., **ptr = _). If yes, check whether these pointers are initialized.
+ let mut place_to_add_projections =
+ Place { local: place_without_deref.local, projection: vec![] };
+ for projection_elem in place_without_deref.projection.iter() {
+ // If the projection is Deref and the current type is raw pointer, check
+ // if it points to initialized memory.
+ if *projection_elem == ProjectionElem::Deref {
+ if let TyKind::RigidTy(RigidTy::RawPtr(..)) =
+ place_to_add_projections.ty(&self.locals).unwrap().kind()
+ {
+ self.push_target(MemoryInitOp::Check {
+ operand: Operand::Copy(place_to_add_projections.clone()),
+ count: mk_const_operand(1, location.span()),
+ });
+ };
+ }
+ place_to_add_projections.projection.push(projection_elem.clone());
+ }
+ 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,
+ });
+ }
+ }
+ // Check whether Rvalue creates a new initialized pointer previously not captured inside shadow memory.
+ if place.ty(&self.locals).unwrap().kind().is_raw_ptr() {
+ 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,
+ });
+ }
+ }
+ }
+ StatementKind::Deinit(place) => {
+ 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,
+ });
+ }
+ StatementKind::FakeRead(_, _)
+ | StatementKind::SetDiscriminant { .. }
+ | StatementKind::StorageLive(_)
+ | StatementKind::StorageDead(_)
+ | StatementKind::Retag(_, _)
+ | StatementKind::PlaceMention(_)
+ | StatementKind::AscribeUserType { .. }
+ | StatementKind::Coverage(_)
+ | StatementKind::ConstEvalCounter
+ | StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(_))
+ | StatementKind::Nop => self.super_statement(stmt, location),
+ }
+ }
+ let SourceInstruction::Statement { idx, bb } = self.current else { unreachable!() };
+ self.current = SourceInstruction::Statement { idx: idx + 1, bb };
+ }
+
+ fn visit_terminator(&mut self, term: &Terminator, location: Location) {
+ if !(self.skip_next || self.target.is_some()) {
+ self.current = SourceInstruction::Terminator { bb: self.bb };
+ // Leave it as an exhaustive match to be notified when a new kind is added.
+ match &term.kind {
+ TerminatorKind::Call { func, args, destination, .. } => {
+ self.super_terminator(term, location);
+ let instance = match try_resolve_instance(self.locals, func) {
+ Ok(instance) => instance,
+ Err(reason) => {
+ self.super_terminator(term, location);
+ self.push_target(MemoryInitOp::Unsupported { reason });
+ return;
+ }
+ };
+ match instance.kind {
+ InstanceKind::Intrinsic => {
+ match instance.intrinsic_name().unwrap().as_str() {
+ intrinsic_name if can_skip_intrinsic(intrinsic_name) => {
+ /* Intrinsics that can be safely skipped */
+ }
+ name if name.starts_with("atomic") => {
+ let num_args =
+ if name.starts_with("atomic_cxchg") { 3 } else { 2 };
+ assert_eq!(
+ args.len(),
+ num_args,
+ "Unexpected number of arguments for `{name}`"
+ );
+ assert!(matches!(
+ args[0].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(..))
+ ));
+ self.push_target(MemoryInitOp::Check {
+ operand: args[0].clone(),
+ count: mk_const_operand(1, location.span()),
+ });
+ }
+ "compare_bytes" => {
+ assert_eq!(
+ args.len(),
+ 3,
+ "Unexpected number of arguments for `compare_bytes`"
+ );
+ assert!(matches!(
+ args[0].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
+ ));
+ assert!(matches!(
+ args[1].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
+ ));
+ self.push_target(MemoryInitOp::Check {
+ operand: args[0].clone(),
+ count: args[2].clone(),
+ });
+ self.push_target(MemoryInitOp::Check {
+ operand: args[1].clone(),
+ count: args[2].clone(),
+ });
+ }
+ "copy"
+ | "volatile_copy_memory"
+ | "volatile_copy_nonoverlapping_memory" => {
+ assert_eq!(
+ args.len(),
+ 3,
+ "Unexpected number of arguments for `copy`"
+ );
+ assert!(matches!(
+ args[0].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
+ ));
+ assert!(matches!(
+ args[1].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
+ ));
+ self.push_target(MemoryInitOp::Check {
+ operand: args[0].clone(),
+ count: args[2].clone(),
+ });
+ self.push_target(MemoryInitOp::Set {
+ operand: args[1].clone(),
+ count: args[2].clone(),
+ value: true,
+ position: InsertPosition::After,
+ });
+ }
+ "typed_swap" => {
+ assert_eq!(
+ args.len(),
+ 2,
+ "Unexpected number of arguments for `typed_swap`"
+ );
+ assert!(matches!(
+ args[0].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
+ ));
+ assert!(matches!(
+ args[1].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
+ ));
+ 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" => {
+ assert_eq!(
+ args.len(),
+ 1,
+ "Unexpected number of arguments for `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_store" => {
+ assert_eq!(
+ args.len(),
+ 2,
+ "Unexpected number of arguments for `volatile_store`"
+ );
+ assert!(matches!(
+ args[0].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
+ ));
+ self.push_target(MemoryInitOp::Set {
+ operand: args[0].clone(),
+ count: mk_const_operand(1, location.span()),
+ value: true,
+ position: InsertPosition::After,
+ });
+ }
+ "write_bytes" => {
+ assert_eq!(
+ args.len(),
+ 3,
+ "Unexpected number of arguments for `write_bytes`"
+ );
+ assert!(matches!(
+ args[0].ty(self.locals).unwrap().kind(),
+ TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
+ ));
+ self.push_target(MemoryInitOp::Set {
+ operand: args[0].clone(),
+ count: args[2].clone(),
+ value: true,
+ position: InsertPosition::After,
+ })
+ }
+ intrinsic => {
+ self.push_target(MemoryInitOp::Unsupported {
+ reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic}`."),
+ });
+ }
+ }
+ }
+ InstanceKind::Item => {
+ if instance.is_foreign_item() {
+ match instance.name().as_str() {
+ "alloc::alloc::__rust_alloc"
+ | "alloc::alloc::__rust_realloc" => {
+ /* Memory is uninitialized, nothing to do here. */
+ }
+ "alloc::alloc::__rust_alloc_zeroed" => {
+ /* Memory is initialized here, need to update shadow memory. */
+ self.push_target(MemoryInitOp::Set {
+ operand: Operand::Copy(destination.clone()),
+ count: args[0].clone(),
+ value: true,
+ position: InsertPosition::After,
+ });
+ }
+ "alloc::alloc::__rust_dealloc" => {
+ /* Memory is uninitialized here, need to update shadow memory. */
+ self.push_target(MemoryInitOp::Set {
+ operand: args[0].clone(),
+ count: args[1].clone(),
+ value: false,
+ position: InsertPosition::After,
+ });
+ }
+ _ => {}
+ }
+ }
+ }
+ _ => {}
+ }
+ }
+ 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,
+ });
+ 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,
+ });
+ }
+ }
+ TerminatorKind::Goto { .. }
+ | TerminatorKind::SwitchInt { .. }
+ | TerminatorKind::Resume
+ | TerminatorKind::Abort
+ | TerminatorKind::Return
+ | TerminatorKind::Unreachable
+ | TerminatorKind::Assert { .. }
+ | TerminatorKind::InlineAsm { .. } => self.super_terminator(term, location),
+ }
+ }
+ }
+
+ fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) {
+ for (idx, elem) in place.projection.iter().enumerate() {
+ let intermediate_place =
+ Place { local: place.local, projection: place.projection[..idx].to_vec() };
+ match elem {
+ ProjectionElem::Deref => {
+ let ptr_ty = intermediate_place.ty(self.locals).unwrap();
+ 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()),
+ });
+ }
+ }
+ ProjectionElem::Field(idx, target_ty) => {
+ if target_ty.kind().is_union()
+ && (!ptx.is_mutating() || place.projection.len() > idx + 1)
+ {
+ self.push_target(MemoryInitOp::Unsupported {
+ reason: "Kani does not support reasoning about memory initialization of unions.".to_string(),
+ });
+ }
+ }
+ ProjectionElem::Index(_)
+ | ProjectionElem::ConstantIndex { .. }
+ | ProjectionElem::Subslice { .. } => {
+ /* For a slice to be indexed, it should be valid first. */
+ }
+ ProjectionElem::Downcast(_) => {}
+ ProjectionElem::OpaqueCast(_) => {}
+ ProjectionElem::Subtype(_) => {}
+ }
+ }
+ self.super_place(place, ptx, location)
+ }
+
+ fn visit_operand(&mut self, operand: &Operand, location: Location) {
+ if let Operand::Constant(constant) = operand {
+ 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,
+ });
+ };
+ }
+ }
+ }
+ self.super_operand(operand, location);
+ }
+
+ 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(),
+ });
+ }
+ }
+ };
+ self.super_rvalue(rvalue, location);
+ }
+}
+
+/// Determines if the intrinsic has no memory initialization related function and hence can be
+/// safely skipped.
+fn can_skip_intrinsic(intrinsic_name: &str) -> bool {
+ match intrinsic_name {
+ "add_with_overflow"
+ | "arith_offset"
+ | "assert_inhabited"
+ | "assert_mem_uninitialized_valid"
+ | "assert_zero_valid"
+ | "assume"
+ | "bitreverse"
+ | "black_box"
+ | "breakpoint"
+ | "bswap"
+ | "caller_location"
+ | "ceilf32"
+ | "ceilf64"
+ | "copysignf32"
+ | "copysignf64"
+ | "cosf32"
+ | "cosf64"
+ | "ctlz"
+ | "ctlz_nonzero"
+ | "ctpop"
+ | "cttz"
+ | "cttz_nonzero"
+ | "discriminant_value"
+ | "exact_div"
+ | "exp2f32"
+ | "exp2f64"
+ | "expf32"
+ | "expf64"
+ | "fabsf32"
+ | "fabsf64"
+ | "fadd_fast"
+ | "fdiv_fast"
+ | "floorf32"
+ | "floorf64"
+ | "fmaf32"
+ | "fmaf64"
+ | "fmul_fast"
+ | "forget"
+ | "fsub_fast"
+ | "is_val_statically_known"
+ | "likely"
+ | "log10f32"
+ | "log10f64"
+ | "log2f32"
+ | "log2f64"
+ | "logf32"
+ | "logf64"
+ | "maxnumf32"
+ | "maxnumf64"
+ | "min_align_of"
+ | "min_align_of_val"
+ | "minnumf32"
+ | "minnumf64"
+ | "mul_with_overflow"
+ | "nearbyintf32"
+ | "nearbyintf64"
+ | "needs_drop"
+ | "powf32"
+ | "powf64"
+ | "powif32"
+ | "powif64"
+ | "pref_align_of"
+ | "raw_eq"
+ | "rintf32"
+ | "rintf64"
+ | "rotate_left"
+ | "rotate_right"
+ | "roundf32"
+ | "roundf64"
+ | "saturating_add"
+ | "saturating_sub"
+ | "sinf32"
+ | "sinf64"
+ | "sqrtf32"
+ | "sqrtf64"
+ | "sub_with_overflow"
+ | "truncf32"
+ | "truncf64"
+ | "type_id"
+ | "type_name"
+ | "unchecked_div"
+ | "unchecked_rem"
+ | "unlikely"
+ | "vtable_size"
+ | "vtable_align"
+ | "wrapping_add"
+ | "wrapping_mul"
+ | "wrapping_sub" => {
+ /* Intrinsics that do not interact with memory initialization. */
+ true
+ }
+ "ptr_guaranteed_cmp" | "ptr_offset_from" | "ptr_offset_from_unsigned" | "size_of_val" => {
+ /* AFAICS from the documentation, none of those require the pointer arguments to be actually initialized. */
+ true
+ }
+ name if name.starts_with("simd") => {
+ /* SIMD operations */
+ true
+ }
+ "copy_nonoverlapping" => unreachable!(
+ "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
+ ),
+ "offset" => unreachable!(
+ "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
+ ),
+ "unreachable" => unreachable!(
+ "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
+ ),
+ "transmute" | "transmute_copy" | "unchecked_add" | "unchecked_mul" | "unchecked_shl"
+ | "size_of" | "unchecked_shr" | "unchecked_sub" => {
+ unreachable!("Expected intrinsic to be lowered before codegen")
+ }
+ "catch_unwind" => {
+ unimplemented!("")
+ }
+ "retag_box_to_raw" => {
+ unreachable!("This was removed in the latest Rust version.")
+ }
+ _ => {
+ /* Everything else */
+ false
+ }
+ }
+}
+
+/// 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();
+ if let Some(ProjectionElem::Deref) = new_place.projection.pop() {
+ Some(new_place)
+ } else {
+ None
+ }
+}
+
+/// Try retrieving instance for the given function operand.
+fn try_resolve_instance(locals: &[LocalDecl], func: &Operand) -> Result {
+ let ty = func.ty(locals).unwrap();
+ match ty.kind() {
+ TyKind::RigidTy(RigidTy::FnDef(def, args)) => Ok(Instance::resolve(def, &args).unwrap()),
+ _ => Err(format!(
+ "Kani does not support reasoning about memory initialization of arguments to `{ty:?}`."
+ )),
+ }
+}
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index 4ecb16fab023..a7d0f14d270f 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -14,7 +14,9 @@
//! 1. We could merge the invalid values by the offset.
//! 2. We could avoid checking places that have been checked before.
use crate::args::ExtraChecks;
-use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction};
+use crate::kani_middle::transform::body::{
+ CheckType, InsertPosition, MutableBody, SourceInstruction,
+};
use crate::kani_middle::transform::check_values::SourceOp::UnsupportedCheck;
use crate::kani_middle::transform::{TransformPass, TransformationType};
use crate::kani_queries::QueryDb;
@@ -59,7 +61,7 @@ impl TransformPass for ValidValuePass {
/// Transform the function body by inserting checks one-by-one.
/// For every unsafe dereference or a transmute operation, we check all values are valid.
- fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+ fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
trace!(function=?instance.name(), "transform");
let mut new_body = MutableBody::from(body);
let orig_len = new_body.blocks().len();
@@ -83,13 +85,20 @@ impl ValidValuePass {
for operation in instruction.operations {
match operation {
SourceOp::BytesValidity { ranges, target_ty, rvalue } => {
- let value = body.new_assignment(rvalue, &mut source);
+ let value = body.new_assignment(rvalue, &mut source, InsertPosition::Before);
let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value));
for range in ranges {
let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source);
let msg =
format!("Undefined Behavior: Invalid value of type `{target_ty}`",);
- body.add_check(tcx, &self.check_type, &mut source, result, &msg);
+ body.add_check(
+ tcx,
+ &self.check_type,
+ &mut source,
+ InsertPosition::Before,
+ result,
+ &msg,
+ );
}
}
SourceOp::DerefValidity { pointee_ty, rvalue, ranges } => {
@@ -97,7 +106,14 @@ impl ValidValuePass {
let result = build_limits(body, &range, rvalue.clone(), &mut source);
let msg =
format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",);
- body.add_check(tcx, &self.check_type, &mut source, result, &msg);
+ body.add_check(
+ tcx,
+ &self.check_type,
+ &mut source,
+ InsertPosition::Before,
+ result,
+ &msg,
+ );
}
}
SourceOp::UnsupportedCheck { check, ty } => {
@@ -123,8 +139,8 @@ impl ValidValuePass {
span,
user_ty: None,
}));
- let result = body.new_assignment(rvalue, source);
- body.add_check(tcx, &self.check_type, source, result, reason);
+ let result = body.new_assignment(rvalue, source, InsertPosition::Before);
+ body.add_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason);
}
}
@@ -758,30 +774,60 @@ pub fn build_limits(
let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span);
let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span);
let orig_ptr = if req.offset != 0 {
- let start_ptr = move_local(body.new_assignment(rvalue_ptr, source));
+ let start_ptr = move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before));
let byte_ptr = move_local(body.new_cast_ptr(
start_ptr,
Ty::unsigned_ty(UintTy::U8),
Mutability::Not,
source,
+ InsertPosition::Before,
));
let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span);
- let offset = move_local(body.new_assignment(Rvalue::Use(offset_const), source));
- move_local(body.new_binary_op(BinOp::Offset, byte_ptr, offset, source))
+ let offset = move_local(body.new_assignment(
+ Rvalue::Use(offset_const),
+ source,
+ InsertPosition::Before,
+ ));
+ move_local(body.new_binary_op(
+ BinOp::Offset,
+ byte_ptr,
+ offset,
+ source,
+ InsertPosition::Before,
+ ))
} else {
- move_local(body.new_assignment(rvalue_ptr, source))
+ move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before))
};
- let value_ptr =
- body.new_cast_ptr(orig_ptr, Ty::unsigned_ty(primitive_ty), Mutability::Not, source);
+ let value_ptr = body.new_cast_ptr(
+ orig_ptr,
+ Ty::unsigned_ty(primitive_ty),
+ Mutability::Not,
+ source,
+ InsertPosition::Before,
+ );
let value = Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] });
- let start_result = body.new_binary_op(BinOp::Ge, value.clone(), start_const, source);
- let end_result = body.new_binary_op(BinOp::Le, value, end_const, source);
+ let start_result =
+ body.new_binary_op(BinOp::Ge, value.clone(), start_const, source, InsertPosition::Before);
+ let end_result =
+ body.new_binary_op(BinOp::Le, value, end_const, source, InsertPosition::Before);
if req.valid_range.wraps_around() {
// valid >= start || valid <= end
- body.new_binary_op(BinOp::BitOr, move_local(start_result), move_local(end_result), source)
+ body.new_binary_op(
+ BinOp::BitOr,
+ move_local(start_result),
+ move_local(end_result),
+ source,
+ InsertPosition::Before,
+ )
} else {
// valid >= start && valid <= end
- body.new_binary_op(BinOp::BitAnd, move_local(start_result), move_local(end_result), source)
+ body.new_binary_op(
+ BinOp::BitAnd,
+ move_local(start_result),
+ move_local(end_result),
+ source,
+ InsertPosition::Before,
+ )
}
}
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
index f5760bd4d829..eb5266e0a0eb 100644
--- a/kani-compiler/src/kani_middle/transform/contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -47,7 +47,7 @@ impl TransformPass for AnyModifiesPass {
}
/// Transform the function body by replacing it with the stub body.
- fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+ fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
trace!(function=?instance.name(), "AnyModifiesPass::transform");
if instance.def.def_id() == self.kani_any.unwrap().def_id() {
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index 53bbd52086ac..ea7bf8625228 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -7,8 +7,12 @@
//! information; thus, they are implemented as a transformation pass where their body get generated
//! by the transformation.
+use crate::args::{Arguments, ExtraChecks};
use crate::kani_middle::attributes::matches_diagnostic;
-use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction};
+use crate::kani_middle::transform::body::{
+ CheckType, InsertPosition, MutableBody, SourceInstruction,
+};
+use crate::kani_middle::transform::check_uninit::PointeeInfo;
use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_offset};
use crate::kani_middle::transform::{TransformPass, TransformationType};
use crate::kani_queries::QueryDb;
@@ -18,15 +22,24 @@ use stable_mir::mir::{
BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
};
use stable_mir::target::MachineInfo;
-use stable_mir::ty::{MirConst, RigidTy, TyKind};
+use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy};
+use std::collections::HashMap;
use std::fmt::Debug;
use strum_macros::AsRefStr;
use tracing::trace;
+use super::check_uninit::{
+ get_mem_init_fn_def, mk_layout_operand, resolve_mem_init_fn, PointeeLayout,
+};
+
/// Generate the body for a few Kani intrinsics.
#[derive(Debug)]
pub struct IntrinsicGeneratorPass {
pub check_type: CheckType,
+ /// Used to cache FnDef lookups of injected memory initialization functions.
+ pub mem_init_fn_cache: HashMap<&'static str, FnDef>,
+ /// Used to enable intrinsics depending on the flags passed.
+ pub arguments: Arguments,
}
impl TransformPass for IntrinsicGeneratorPass {
@@ -46,10 +59,12 @@ impl TransformPass for IntrinsicGeneratorPass {
/// Transform the function body by inserting checks one-by-one.
/// For every unsafe dereference or a transmute operation, we check all values are valid.
- fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+ fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
trace!(function=?instance.name(), "transform");
if matches_diagnostic(tcx, instance.def, Intrinsics::KaniValidValue.as_ref()) {
(true, self.valid_value_body(tcx, body))
+ } else if matches_diagnostic(tcx, instance.def, Intrinsics::KaniIsInitialized.as_ref()) {
+ (true, self.is_initialized_body(tcx, body))
} else {
(false, body)
}
@@ -86,7 +101,7 @@ impl IntrinsicGeneratorPass {
})),
);
let stmt = Statement { kind: assign, span };
- new_body.insert_stmt(stmt, &mut terminator);
+ new_body.insert_stmt(stmt, &mut terminator, InsertPosition::Before);
let machine_info = MachineInfo::target();
// The first and only argument type.
@@ -110,7 +125,7 @@ impl IntrinsicGeneratorPass {
);
let assign = StatementKind::Assign(Place::from(ret_var), rvalue);
let stmt = Statement { kind: assign, span };
- new_body.insert_stmt(stmt, &mut terminator);
+ new_body.insert_stmt(stmt, &mut terminator, InsertPosition::Before);
}
}
Err(msg) => {
@@ -120,11 +135,169 @@ impl IntrinsicGeneratorPass {
span,
user_ty: None,
}));
- let result = new_body.new_assignment(rvalue, &mut terminator);
+ let result =
+ new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before);
let reason = format!(
"Kani currently doesn't support checking validity of `{target_ty}`. {msg}"
);
- new_body.add_check(tcx, &self.check_type, &mut terminator, result, &reason);
+ new_body.add_check(
+ tcx,
+ &self.check_type,
+ &mut terminator,
+ InsertPosition::Before,
+ result,
+ &reason,
+ );
+ }
+ }
+ new_body.into()
+ }
+
+ /// Generate the body for `is_initialized`, which looks like the following
+ ///
+ /// ```
+ /// pub fn is_initialized(ptr: *const T, len: usize) -> bool {
+ /// let layout = ... // Byte mask representing the layout of T.
+ /// __kani_mem_init_sm_get(ptr, layout, len)
+ /// }
+ /// ```
+ fn is_initialized_body(&mut self, tcx: TyCtxt, body: Body) -> Body {
+ let mut new_body = MutableBody::from(body);
+ new_body.clear_body();
+
+ // Initialize return variable with True.
+ let ret_var = RETURN_LOCAL;
+ let mut terminator = SourceInstruction::Terminator { bb: 0 };
+ let span = new_body.locals()[ret_var].span;
+ let assign = StatementKind::Assign(
+ Place::from(ret_var),
+ Rvalue::Use(Operand::Constant(ConstOperand {
+ span,
+ user_ty: None,
+ const_: MirConst::from_bool(true),
+ })),
+ );
+ let stmt = Statement { kind: assign, span };
+ new_body.insert_stmt(stmt, &mut terminator, InsertPosition::Before);
+
+ if !self.arguments.ub_check.contains(&ExtraChecks::Uninit) {
+ // Short-circut if uninitialized memory checks are not enabled.
+ return new_body.into();
+ }
+
+ // The first argument type.
+ let arg_ty = new_body.locals()[1].ty;
+ let TyKind::RigidTy(RigidTy::RawPtr(target_ty, _)) = arg_ty.kind() else { unreachable!() };
+ let pointee_info = PointeeInfo::from_ty(target_ty);
+ match pointee_info {
+ Ok(pointee_info) => {
+ match pointee_info.layout() {
+ PointeeLayout::Sized { layout } => {
+ if layout.is_empty() {
+ // Encountered a ZST, so we can short-circut here.
+ return new_body.into();
+ }
+ let is_ptr_initialized_instance = resolve_mem_init_fn(
+ get_mem_init_fn_def(
+ tcx,
+ "KaniIsPtrInitialized",
+ &mut self.mem_init_fn_cache,
+ ),
+ layout.len(),
+ *pointee_info.ty(),
+ );
+ let layout_operand = mk_layout_operand(
+ &mut new_body,
+ &mut terminator,
+ InsertPosition::Before,
+ &layout,
+ );
+ new_body.add_call(
+ &is_ptr_initialized_instance,
+ &mut terminator,
+ InsertPosition::Before,
+ vec![
+ Operand::Copy(Place::from(1)),
+ layout_operand,
+ Operand::Copy(Place::from(2)),
+ ],
+ Place::from(ret_var),
+ );
+ }
+ PointeeLayout::Slice { element_layout } => {
+ // Since `str`` is a separate type, need to differentiate between [T] and str.
+ let (slicee_ty, diagnostic) = match pointee_info.ty().kind() {
+ TyKind::RigidTy(RigidTy::Slice(slicee_ty)) => {
+ (slicee_ty, "KaniIsSlicePtrInitialized")
+ }
+ TyKind::RigidTy(RigidTy::Str) => {
+ (Ty::unsigned_ty(UintTy::U8), "KaniIsStrPtrInitialized")
+ }
+ _ => unreachable!(),
+ };
+ let is_ptr_initialized_instance = resolve_mem_init_fn(
+ get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache),
+ element_layout.len(),
+ slicee_ty,
+ );
+ let layout_operand = mk_layout_operand(
+ &mut new_body,
+ &mut terminator,
+ InsertPosition::Before,
+ &element_layout,
+ );
+ new_body.add_call(
+ &is_ptr_initialized_instance,
+ &mut terminator,
+ InsertPosition::Before,
+ vec![Operand::Copy(Place::from(1)), layout_operand],
+ Place::from(ret_var),
+ );
+ }
+ PointeeLayout::TraitObject => {
+ let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
+ const_: MirConst::from_bool(false),
+ span,
+ user_ty: None,
+ }));
+ let result = new_body.new_assignment(
+ rvalue,
+ &mut terminator,
+ InsertPosition::Before,
+ );
+ let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
+
+ new_body.add_check(
+ tcx,
+ &self.check_type,
+ &mut terminator,
+ InsertPosition::Before,
+ result,
+ &reason,
+ );
+ }
+ };
+ }
+ Err(msg) => {
+ // We failed to retrieve the type layout.
+ let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
+ const_: MirConst::from_bool(false),
+ span,
+ user_ty: None,
+ }));
+ let result =
+ new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before);
+ let reason = format!(
+ "Kani currently doesn't support checking memory initialization of `{target_ty}`. {msg}"
+ );
+ new_body.add_check(
+ tcx,
+ &self.check_type,
+ &mut terminator,
+ InsertPosition::Before,
+ result,
+ &reason,
+ );
}
}
new_body.into()
@@ -135,4 +308,5 @@ impl IntrinsicGeneratorPass {
#[strum(serialize_all = "PascalCase")]
enum Intrinsics {
KaniValidValue,
+ KaniIsInitialized,
}
diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
index 8d5c61f55c92..56ab0be493c4 100644
--- a/kani-compiler/src/kani_middle/transform/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -18,6 +18,7 @@
//! case is added.
use crate::kani_middle::codegen_units::CodegenUnit;
use crate::kani_middle::transform::body::CheckType;
+use crate::kani_middle::transform::check_uninit::UninitPass;
use crate::kani_middle::transform::check_values::ValidValuePass;
use crate::kani_middle::transform::contracts::AnyModifiesPass;
use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass;
@@ -30,6 +31,7 @@ use std::collections::HashMap;
use std::fmt::Debug;
pub(crate) mod body;
+mod check_uninit;
mod check_values;
mod contracts;
mod kani_intrinsics;
@@ -64,7 +66,23 @@ impl BodyTransformation {
// This has to come after stubs since we want this to replace the stubbed body.
transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit));
transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() });
- transformer.add_pass(queries, IntrinsicGeneratorPass { check_type });
+ // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by
+ // `UninitPass` does not get unnecessarily instrumented by valid value checks. However, it
+ // would also make sense to check that the values are initialized before checking their
+ // validity. In the future, it would be nice to have a mechanism to skip automatically
+ // generated code for future instrumentation passes.
+ transformer.add_pass(
+ queries,
+ UninitPass { check_type: check_type.clone(), mem_init_fn_cache: HashMap::new() },
+ );
+ transformer.add_pass(
+ queries,
+ IntrinsicGeneratorPass {
+ check_type,
+ mem_init_fn_cache: HashMap::new(),
+ arguments: queries.args().clone(),
+ },
+ );
transformer
}
@@ -79,7 +97,7 @@ impl BodyTransformation {
None => {
let mut body = instance.body().unwrap();
let mut modified = false;
- for pass in self.stub_passes.iter().chain(self.inst_passes.iter()) {
+ for pass in self.stub_passes.iter_mut().chain(self.inst_passes.iter_mut()) {
let result = pass.transform(tcx, body, instance);
modified |= result.0;
body = result.1;
@@ -127,7 +145,7 @@ pub(crate) trait TransformPass: Debug {
Self: Sized;
/// Run a transformation pass in the function body.
- fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body);
+ fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body);
}
/// The transformation result.
diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs
index 4f249afdd45a..3dbd667c3943 100644
--- a/kani-compiler/src/kani_middle/transform/stubs.rs
+++ b/kani-compiler/src/kani_middle/transform/stubs.rs
@@ -43,7 +43,7 @@ impl TransformPass for FnStubPass {
}
/// Transform the function body by replacing it with the stub body.
- fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+ fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
trace!(function=?instance.name(), "transform");
let ty = instance.ty();
if let TyKind::RigidTy(RigidTy::FnDef(fn_def, mut args)) = ty.kind() {
@@ -103,7 +103,7 @@ impl TransformPass for ExternFnStubPass {
///
/// We need to find function calls and function pointers.
/// We should replace this with a visitor once StableMIR includes a mutable one.
- fn transform(&self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+ fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
trace!(function=?instance.name(), "transform");
let mut new_body = MutableBody::from(body);
let changed = false;
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 18ca11b0a30f..7cbe150427e9 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -139,6 +139,10 @@ impl KaniSession {
flags.push("--ub-check=ptr_to_ref_cast".into())
}
+ if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) {
+ flags.push("--ub-check=uninit".into())
+ }
+
if self.args.ignore_locals_lifetime {
flags.push("--ignore-storage-markers".into())
}
diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs
index 9f82e4b02a64..68e4fba28819 100644
--- a/kani_metadata/src/unstable.rs
+++ b/kani_metadata/src/unstable.rs
@@ -91,6 +91,8 @@ pub enum UnstableFeature {
GhostState,
/// Automatically check that pointers are valid when casting them to references.
PtrToRefCastChecks,
+ /// Automatically check that uninitialized memory is not used.
+ UninitChecks,
/// Enable an unstable option or subcommand.
UnstableOptions,
}
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 0a52a9516398..6eab2a331811 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -35,6 +35,7 @@ pub mod vec;
#[doc(hidden)]
pub mod internal;
+mod mem_init;
mod models;
pub use arbitrary::Arbitrary;
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
index c40a1aa696e3..0b390e74288d 100644
--- a/library/kani/src/mem.rs
+++ b/library/kani/src/mem.rs
@@ -120,6 +120,7 @@ where
let (thin_ptr, metadata) = ptr.to_raw_parts();
metadata.is_ptr_aligned(thin_ptr, Internal)
&& is_inbounds(&metadata, thin_ptr)
+ && is_initialized(ptr, 1)
&& unsafe { has_valid_value(ptr) }
}
@@ -147,7 +148,7 @@ where
::Metadata: PtrProperties,
{
let (thin_ptr, metadata) = ptr.to_raw_parts();
- is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) }
+ is_inbounds(&metadata, thin_ptr) && is_initialized(ptr, 1) && unsafe { has_valid_value(ptr) }
}
/// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`.
@@ -290,6 +291,13 @@ unsafe fn has_valid_value(_ptr: *const T) -> bool {
kani_intrinsic()
}
+/// 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 {
+ kani_intrinsic()
+}
+
/// 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
new file mode 100644
index 000000000000..37832ea32604
--- /dev/null
+++ b/library/kani/src/mem_init.rs
@@ -0,0 +1,122 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module uses shadow memory API to track 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`).
+
+// 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:
+/// ```
+/// #[repr(C)]
+/// struct Foo {
+/// a: u16,
+/// b: u8,
+/// }
+/// ```
+/// 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;
+ }
+ }
+ 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;
+ }
+ count += 1;
+ }
+}
+
+/// Get initialization state of `len` 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 {
+ let (ptr, _) = ptr.to_raw_parts();
+ is_unit_ptr_initialized(ptr, layout, len)
+}
+
+/// Set initialization state to `value` for `len` items laid out according to the `layout` starting at address `ptr`.
+#[rustc_diagnostic_item = "KaniSetPtrInitialized"]
+fn set_ptr_initialized(
+ ptr: *const T,
+ layout: Layout,
+ len: usize,
+ value: bool,
+) {
+ let (ptr, _) = ptr.to_raw_parts();
+ set_unit_ptr_initialized(ptr, layout, len, 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)
+}
+
+/// 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);
+}
+
+/// 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)
+}
+
+/// 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);
+}
diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
index 8dd4a27cb03a..3b10856765a5 100644
--- a/library/kani_core/src/mem.rs
+++ b/library/kani_core/src/mem.rs
@@ -125,6 +125,7 @@ macro_rules! kani_mem {
let (thin_ptr, metadata) = ptr.to_raw_parts();
metadata.is_ptr_aligned(thin_ptr, Internal)
&& is_inbounds(&metadata, thin_ptr)
+ && is_initialized(ptr, 1)
&& unsafe { has_valid_value(ptr) }
}
@@ -153,7 +154,9 @@ macro_rules! kani_mem {
::Metadata: PtrProperties,
{
let (thin_ptr, metadata) = ptr.to_raw_parts();
- is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) }
+ is_inbounds(&metadata, thin_ptr)
+ && is_initialized(ptr, 1)
+ && unsafe { has_valid_value(ptr) }
}
/// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`.
@@ -296,6 +299,13 @@ macro_rules! kani_mem {
kani_intrinsic()
}
+ /// 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 {
+ kani_intrinsic()
+ }
+
/// 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
new file mode 100644
index 000000000000..d6e735e219ad
--- /dev/null
+++ b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::ptr::addr_of;
+
+#[repr(C)]
+struct S(u32, u8);
+
+/// Checks that Kani catches an attempt to access padding of a struct using raw pointers.
+#[kani::proof]
+fn check_uninit_padding() {
+ let s = S(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let padding = unsafe { *(ptr.add(5)) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
+}
diff --git a/tests/expected/uninit/access-padding-uninit/expected b/tests/expected/uninit/access-padding-uninit/expected
new file mode 100644
index 000000000000..da8d15b2dbb9
--- /dev/null
+++ b/tests/expected/uninit/access-padding-uninit/expected
@@ -0,0 +1,5 @@
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
\ No newline at end of file
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
new file mode 100644
index 000000000000..b73bebc827bc
--- /dev/null
+++ b/tests/expected/uninit/access-padding-via-cast/access-padding-via-cast.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::ptr;
+#[repr(C)]
+struct S(u8, u16);
+
+/// Checks that Kani catches an attempt to access padding of a struct using casting to different types.
+#[kani::proof]
+fn check_uninit_padding_after_cast() {
+ 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); // should reset the padding
+ let val = *sptr2; // ~ERROR: encountered uninitialized memory
+ }
+}
diff --git a/tests/expected/uninit/access-padding-via-cast/expected b/tests/expected/uninit/access-padding-via-cast/expected
new file mode 100644
index 000000000000..12c5c0a4a439
--- /dev/null
+++ b/tests/expected/uninit/access-padding-via-cast/expected
@@ -0,0 +1,5 @@
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut [u8; 4]`
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
\ No newline at end of file
diff --git a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
new file mode 100644
index 000000000000..3c4420f5791f
--- /dev/null
+++ b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::alloc::{alloc, dealloc, Layout};
+use std::slice::from_raw_parts;
+
+/// Checks that Kani catches an attempt to form a slice from uninitialized memory.
+#[kani::proof]
+fn check_uninit_slice() {
+ let layout = Layout::from_size_align(16, 8).unwrap();
+ unsafe {
+ let ptr = alloc(layout);
+ *ptr = 0x41;
+ *ptr.add(1) = 0x42;
+ *ptr.add(2) = 0x43;
+ *ptr.add(3) = 0x44;
+ let uninit_slice = from_raw_parts(ptr, 16); // ~ERROR: forming a slice from unitialized memory is UB.
+ }
+}
diff --git a/tests/expected/uninit/alloc-to-slice/expected b/tests/expected/uninit/alloc-to-slice/expected
new file mode 100644
index 000000000000..f8347a591edf
--- /dev/null
+++ b/tests/expected/uninit/alloc-to-slice/expected
@@ -0,0 +1,5 @@
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8]`
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
\ No newline at end of file
diff --git a/tests/expected/uninit/vec-read-bad-len/expected b/tests/expected/uninit/vec-read-bad-len/expected
new file mode 100644
index 000000000000..f8347a591edf
--- /dev/null
+++ b/tests/expected/uninit/vec-read-bad-len/expected
@@ -0,0 +1,5 @@
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8]`
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
\ No newline at end of file
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
new file mode 100644
index 000000000000..9778bb11a277
--- /dev/null
+++ b/tests/expected/uninit/vec-read-bad-len/vec-read-bad-len.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::ops::Index;
+
+/// Checks that Kani catches an attempt to read uninitialized memory from a vector with bad length.
+#[kani::proof]
+fn check_vec_read_bad_len() {
+ let mut v: Vec = Vec::with_capacity(10);
+ unsafe {
+ v.set_len(5); // even though length is now 5, vector is still uninitialized
+ }
+ let uninit = v.index(0); // ~ERROR: reading from unitialized memory is UB.
+}
diff --git a/tests/expected/uninit/vec-read-semi-init/expected b/tests/expected/uninit/vec-read-semi-init/expected
new file mode 100644
index 000000000000..da8d15b2dbb9
--- /dev/null
+++ b/tests/expected/uninit/vec-read-semi-init/expected
@@ -0,0 +1,5 @@
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
\ No newline at end of file
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
new file mode 100644
index 000000000000..4330f5f53023
--- /dev/null
+++ b/tests/expected/uninit/vec-read-semi-init/vec-read-semi-init.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+/// Checks that Kani catches an attempt to read uninitialized memory from a semi-initialized vector.
+#[kani::proof]
+fn check_vec_read_semi_init() {
+ let mut v: Vec = Vec::with_capacity(10);
+ unsafe { *v.as_mut_ptr().add(4) = 0x42 };
+ let uninit = unsafe { *v.as_ptr().add(5) }; // ~ERROR: reading from unitialized memory is UB.
+}
diff --git a/tests/expected/uninit/vec-read-uninit/expected b/tests/expected/uninit/vec-read-uninit/expected
new file mode 100644
index 000000000000..da8d15b2dbb9
--- /dev/null
+++ b/tests/expected/uninit/vec-read-uninit/expected
@@ -0,0 +1,5 @@
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
+
+VERIFICATION:- FAILED
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.
\ No newline at end of file
diff --git a/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs
new file mode 100644
index 000000000000..c322b4d33bb2
--- /dev/null
+++ b/tests/expected/uninit/vec-read-uninit/vec-read-uninit.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+/// Checks that Kani catches an attempt to read uninitialized memory from an uninitialized vector.
+#[kani::proof]
+fn check_vec_read_uninit() {
+ let v: Vec = Vec::with_capacity(10);
+ let uninit = unsafe { *v.as_ptr().add(5) }; // ~ERROR: reading from unitialized memory is UB.
+}
diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs
new file mode 100644
index 000000000000..7feb493a5b3f
--- /dev/null
+++ b/tests/kani/Uninit/access-padding-enum-diverging-variants.rs
@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::ptr;
+use std::ptr::addr_of;
+
+/// The layout of this enum is variable, so Kani cannot check memory initialization statically.
+#[repr(C)]
+enum E1 {
+ A(u16, u8),
+ B(u16),
+}
+
+/// The layout of this enum is variable, but both of the arms have the same padding, so Kani should
+/// support that.
+#[repr(C)]
+enum E2 {
+ A(u16),
+ B(u8, u8),
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn access_padding_unsupported() {
+ let s = E1::A(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+}
+
+#[kani::proof]
+fn access_padding_supported() {
+ let s = E2::A(0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+}
diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs
new file mode 100644
index 000000000000..fb8fae06ca59
--- /dev/null
+++ b/tests/kani/Uninit/access-padding-enum-multiple-variants.rs
@@ -0,0 +1,49 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::ptr;
+use std::ptr::addr_of;
+
+/// The layout of this enum is the following (D = data, P = padding):
+/// 0 1 2 3 4 5 6 7
+/// [D, D, D, D, D, D, D, P]
+/// ---------- -------
+/// \_ tag (i32) \_ A|B(u16, u8)
+#[repr(C)]
+enum E {
+ A(u16, u8),
+ B(u16, u8),
+}
+
+#[kani::proof]
+fn access_padding_init_a() {
+ let s = E::A(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_0 = unsafe { *(ptr.add(0)) };
+ let at_4 = unsafe { *(ptr.add(4)) };
+}
+
+#[kani::proof]
+fn access_padding_init_b() {
+ let s = E::A(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_0 = unsafe { *(ptr.add(0)) };
+ let at_4 = unsafe { *(ptr.add(4)) };
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn access_padding_uninit_a() {
+ let s = E::A(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_7 = unsafe { *(ptr.add(7)) };
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn access_padding_uninit_b() {
+ let s = E::A(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_7 = unsafe { *(ptr.add(7)) };
+}
diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/kani/Uninit/access-padding-enum-single-field.rs
new file mode 100644
index 000000000000..c283b603f705
--- /dev/null
+++ b/tests/kani/Uninit/access-padding-enum-single-field.rs
@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::ptr;
+use std::ptr::addr_of;
+
+/// The layout of this enum is the following (D = data, P = padding):
+/// 0 1 2 3 4 5 6 7 8 9 A B C D E F
+/// [D, D, D, D, P, P, P, P, D, D, D, D, D, D, D, D]
+/// ---------- ----------------------
+/// \_ tag (i32) \_ A(u64)
+#[repr(C)]
+enum E {
+ A(u64),
+}
+
+#[kani::proof]
+fn access_padding_init() {
+ let s = E::A(0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_0 = unsafe { *(ptr.add(0)) };
+ let at_3 = unsafe { *(ptr.add(3)) };
+ let at_9 = unsafe { *(ptr.add(9)) };
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn access_padding_uninit() {
+ let s = E::A(0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_4 = unsafe { *(ptr.add(4)) };
+ let at_7 = unsafe { *(ptr.add(7)) };
+}
diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/kani/Uninit/access-padding-enum-single-variant.rs
new file mode 100644
index 000000000000..f33cfe7ce6fb
--- /dev/null
+++ b/tests/kani/Uninit/access-padding-enum-single-variant.rs
@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+use std::ptr;
+use std::ptr::addr_of;
+
+/// The layout of this enum is the following (D = data, P = padding):
+/// 0 1 2 3 4 5 6 7
+/// [D, D, D, D, D, D, D, P]
+/// ---------- -------
+/// \_ tag (i32) \_ A(u16, u8)
+#[repr(C)]
+enum E {
+ A(u16, u8),
+}
+
+#[kani::proof]
+fn access_padding_init() {
+ let s = E::A(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_0 = unsafe { *(ptr.add(0)) };
+ let at_4 = unsafe { *(ptr.add(4)) };
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn access_padding_uninit() {
+ let s = E::A(0, 0);
+ let ptr: *const u8 = addr_of!(s) as *const u8;
+ let at_7 = unsafe { *(ptr.add(7)) };
+}
diff --git a/tests/perf/uninit/Cargo.toml b/tests/perf/uninit/Cargo.toml
new file mode 100644
index 000000000000..9f44cb3fe103
--- /dev/null
+++ b/tests/perf/uninit/Cargo.toml
@@ -0,0 +1,14 @@
+# 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
new file mode 100644
index 000000000000..f7b4fd303a77
--- /dev/null
+++ b/tests/perf/uninit/expected
@@ -0,0 +1 @@
+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
new file mode 100644
index 000000000000..86b101c0e5d8
--- /dev/null
+++ b/tests/perf/uninit/src/lib.rs
@@ -0,0 +1,68 @@
+// 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/mem.expected b/tests/std-checks/core/mem.expected
index 8a3b89a8f66a..1484c83901fc 100644
--- a/tests/std-checks/core/mem.expected
+++ b/tests/std-checks/core/mem.expected
@@ -1,3 +1,7 @@
+Checking harness mem::verify::check_swap_unit...
+
+Failed Checks: ptr NULL or writable up to size
+
Summary:
Verification failed for - mem::verify::check_swap_unit
-Complete - 3 successfully verified harnesses, 1 failures, 4 total.
+Complete - 6 successfully verified harnesses, 1 failures, 7 total.
diff --git a/tests/std-checks/core/slice.expected b/tests/std-checks/core/slice.expected
new file mode 100644
index 000000000000..01a90d50b557
--- /dev/null
+++ b/tests/std-checks/core/slice.expected
@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/std-checks/core/src/lib.rs b/tests/std-checks/core/src/lib.rs
index f0e5b480a2d2..b0a4fbc6154f 100644
--- a/tests/std-checks/core/src/lib.rs
+++ b/tests/std-checks/core/src/lib.rs
@@ -7,3 +7,4 @@ extern crate kani;
pub mod mem;
pub mod ptr;
+pub mod slice;
diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs
index 4f41d176a73a..b0400d0a75f5 100644
--- a/tests/std-checks/core/src/mem.rs
+++ b/tests/std-checks/core/src/mem.rs
@@ -18,6 +18,11 @@ pub mod contracts {
pub fn swap(x: &mut T, y: &mut T) {
std::mem::swap(x, y)
}
+
+ #[kani::modifies(dest)]
+ pub fn replace(dest: &mut T, src: T) -> T {
+ std::mem::replace(dest, src)
+ }
}
#[cfg(kani)]
@@ -70,4 +75,34 @@ mod verify {
std::mem::forget(x);
std::mem::forget(y);
}
+
+ #[kani::proof_for_contract(contracts::replace)]
+ pub fn check_replace_primitive() {
+ let mut x: u8 = kani::any();
+ let x_before = x;
+
+ let y: u8 = kani::any();
+ let x_returned = contracts::replace(&mut x, y);
+
+ kani::assert(x_before == x_returned, "x_before == x_returned");
+ }
+
+ #[kani::proof_for_contract(contracts::replace)]
+ pub fn check_replace_adt_no_drop() {
+ let mut x: CannotDrop = kani::any();
+ let y: CannotDrop = kani::any();
+ let new_x = contracts::replace(&mut x, y);
+ std::mem::forget(x);
+ std::mem::forget(new_x);
+ }
+
+ /// Memory replace logic is optimized according to the size and alignment of a type.
+ #[kani::proof_for_contract(contracts::replace)]
+ pub fn check_replace_large_adt_no_drop() {
+ let mut x: CannotDrop<[u128; 4]> = kani::any();
+ let y: CannotDrop<[u128; 4]> = kani::any();
+ let new_x = contracts::replace(&mut x, y);
+ std::mem::forget(x);
+ std::mem::forget(new_x);
+ }
}
diff --git a/tests/std-checks/core/src/slice.rs b/tests/std-checks/core/src/slice.rs
new file mode 100644
index 000000000000..044f4bd38586
--- /dev/null
+++ b/tests/std-checks/core/src/slice.rs
@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// 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)
+ }
+}
+
+#[cfg(kani)]
+mod verify {
+ use super::*;
+
+ const MAX_LEN: usize = 2;
+
+ #[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);
+
+ let arr = vec![0u8; len];
+ let _slice = unsafe { contracts::from_raw_parts(arr.as_ptr(), len) };
+ }
+}
From f6d33854ca95e25cbd52d52f3ca842b7eb07793f Mon Sep 17 00:00:00 2001
From: "Celina G. Val"
Date: Tue, 2 Jul 2024 22:44:22 -0700
Subject: [PATCH 17/22] Remove deprecated `--enable-stubbing` (#3309)
Part of #2279
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>
---
kani-driver/src/args/mod.rs | 41 ++++++++-----------
tests/cargo-ui/stubbing-flag/src/main.rs | 3 +-
.../function-stubbing-no-harness/main.rs | 2 +-
.../expected/stubbing-ambiguous-path/main.rs | 2 +-
tests/ui/function-stubbing-error/main.rs | 2 +-
.../deprecated-enable-stable/deprecated.rs | 16 --------
.../deprecated-enable-stable/expected | 2 -
tests/ui/stubbing/invalid-path/invalid.rs | 2 +-
tests/ui/stubbing/stubbing-flag/main.rs | 4 +-
.../trait_mismatch.rs | 2 +-
.../stubbing-type-validation/type_mismatch.rs | 2 +-
11 files changed, 28 insertions(+), 50 deletions(-)
delete mode 100644 tests/ui/stubbing/deprecated-enable-stable/deprecated.rs
delete mode 100644 tests/ui/stubbing/deprecated-enable-stable/expected
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 4c0fe98cc65d..d043035bcab2 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -282,17 +282,6 @@ pub struct VerificationArgs {
#[arg(long)]
pub randomize_layout: Option