From 1e0b71dfa44176c32d1ac80bfee375c6ff64d5b8 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 30 Jul 2024 00:11:40 -0400 Subject: [PATCH 01/11] Function Contracts: Interior Mutability Tests (#3351) Test cases for interior mutability using Cell, OnceCell, UnsafeCell, and RefCell. 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: Matias Scharager Co-authored-by: Felipe R. Monteiro --- .../interior-mutability/api/cell.expected | 6 +++ .../interior-mutability/api/cell.rs | 25 ++++++++++++ .../api/cell_stub.expected | 9 +++++ .../interior-mutability/api/cell_stub.rs | 40 +++++++++++++++++++ .../api/unsafecell.expected | 6 +++ .../interior-mutability/api/unsafecell.rs | 24 +++++++++++ .../whole-struct/cell.expected | 6 +++ .../interior-mutability/whole-struct/cell.rs | 25 ++++++++++++ .../whole-struct/oncecell.expected | 6 +++ .../whole-struct/oncecell.rs | 24 +++++++++++ .../whole-struct/refcell.expected | 6 +++ .../whole-struct/refcell.rs | 25 ++++++++++++ .../whole-struct/unsafecell.expected | 6 +++ .../whole-struct/unsafecell.rs | 25 ++++++++++++ 14 files changed, 233 insertions(+) create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.expected create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.rs create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.expected create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.rs create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.expected create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs diff --git a/tests/expected/function-contract/interior-mutability/api/cell.expected b/tests/expected/function-contract/interior-mutability/api/cell.expected new file mode 100644 index 000000000000..d9b0f5d51e5c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| im.x.get() < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs new file mode 100644 index 000000000000..671b6b206ef3 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// Mutating Cell via `as_ptr` in contracts +use std::cell::Cell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: Cell, +} + +#[kani::requires(im.x.get() < 100)] +#[kani::modifies(im.x.as_ptr())] +#[kani::ensures(|_| im.x.get() < 101)] +///im is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + im.x.set(im.x.get() + 1) +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.expected b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected new file mode 100644 index 000000000000..b8da35411e53 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected @@ -0,0 +1,9 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| old(im.x.get() + im.x.get()) == im.x.get()"\ + +assertion\ +- Status: SUCCESS\ +- Description: "|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs new file mode 100644 index 000000000000..d01ca379655f --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs @@ -0,0 +1,40 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple. +/// This shows that we can generate `kani::any()` for Cell. +use std::cell::Cell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: Cell, +} + +#[kani::ensures(|_| old(im.x.get() + im.x.get()) == im.x.get())] +#[kani::requires(im.x.get() < 100)] +#[kani::modifies(im.x.as_ptr())] +fn double(im: &InteriorMutability) { + im.x.set(im.x.get() + im.x.get()) +} + +#[kani::proof_for_contract(double)] +fn double_harness() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + double(&im); +} + +#[kani::ensures(|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get())] +#[kani::requires(im.x.get() < 50)] +#[kani::modifies(im.x.as_ptr())] +fn quadruple(im: &InteriorMutability) { + double(im); + double(im) +} + +#[kani::proof_for_contract(quadruple)] +#[kani::stub_verified(double)] +fn quadruple_harness() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + quadruple(&im); +} diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.expected b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected new file mode 100644 index 000000000000..1646a8a78e7f --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| unsafe{ *im.x.get() } < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs new file mode 100644 index 000000000000..8125e3e3c077 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +use std::cell::UnsafeCell; + +/// This struct contains UnsafeCell which can be mutated +struct InteriorMutability { + x: UnsafeCell, +} + +#[kani::requires(unsafe{*im.x.get()} < 100)] +#[kani::modifies(im.x.get())] +#[kani::ensures(|_| unsafe{*im.x.get()} < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + unsafe { *im.x.get() += 1 } +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected new file mode 100644 index 000000000000..d9b0f5d51e5c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| im.x.get() < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs new file mode 100644 index 000000000000..9f42f6fa1f6c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct +use std::cell::Cell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: Cell, +} + +#[kani::requires(im.x.get() < 100)] +#[kani::modifies(&im.x)] +#[kani::ensures(|_| im.x.get() < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + im.x.set(im.x.get() + 1) +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected new file mode 100644 index 000000000000..a367bcd9fb95 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| im.x.get().is_some()"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs new file mode 100644 index 000000000000..6ca32251b60c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of an OnceCell used as interior mutability in an immutable struct +use std::cell::OnceCell; + +/// This struct contains OnceCell which can be mutated +struct InteriorMutability { + x: OnceCell, +} + +#[kani::requires(im.x.get().is_none())] +#[kani::modifies(&im.x)] +#[kani::ensures(|_| im.x.get().is_some())] +fn modify(im: &InteriorMutability) { + im.x.set(5).expect("") +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: OnceCell::new() }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected new file mode 100644 index 000000000000..225c290a171e --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs new file mode 100644 index 000000000000..1cce5e2364c3 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct +use std::cell::RefCell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: RefCell, +} + +#[kani::requires(unsafe{*im.x.as_ptr()} < 100)] +#[kani::modifies(&im.x)] +#[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + im.x.replace_with(|&mut old| old + 1); +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: RefCell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected new file mode 100644 index 000000000000..1646a8a78e7f --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| unsafe{ *im.x.get() } < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs new file mode 100644 index 000000000000..6adb7b12c8b1 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct +use std::cell::UnsafeCell; + +/// This struct contains UnsafeCell which can be mutated +struct InteriorMutability { + x: UnsafeCell, +} + +#[kani::requires(unsafe{*im.x.get()} < 100)] +#[kani::modifies(im.x.get())] +#[kani::ensures(|_| unsafe{*im.x.get()} < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + unsafe { *im.x.get() += 1 } +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) }; + modify(&im) +} From 1553ae21369ada3a0bb58ef42d61bbdb8676da5a Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 30 Jul 2024 10:54:17 +0000 Subject: [PATCH 02/11] Automatic toolchain upgrade to nightly-2024-07-30 (#3395) Update Rust toolchain from nightly-2024-07-29 to nightly-2024-07-30 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/2cbbe8b8bb2be672b14cf741a2f0ec24a49f3f0b up to https://github.com/rust-lang/rust/commit/612a33f20b9b2c27380edbc4b26a01433ed114bc. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 18eb2aa4836f..10c7645cf1d7 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-07-29" +channel = "nightly-2024-07-30" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 39c6bc1cacbd57089e0b0602a14daec412cbb2e7 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 30 Jul 2024 22:26:24 -0700 Subject: [PATCH 03/11] Automatic toolchain upgrade to nightly-2024-07-31 (#3397) Update Rust toolchain from nightly-2024-07-30 to nightly-2024-07-31 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/612a33f20b9b2c27380edbc4b26a01433ed114bc up to https://github.com/rust-lang/rust/commit/f8060d282d42770fadd73905e3eefb85660d3278. The log for this commit range is: https://github.com/rust-lang/rust/commit/f8060d282d Auto merge of #128083 - Mark-Simulacrum:bump-bootstrap, r=albertlarsan68 https://github.com/rust-lang/rust/commit/006c8df322 Auto merge of #124339 - oli-obk:supports_feature, r=wesleywiser https://github.com/rust-lang/rust/commit/abb1ebaae1 Revert "opt-dist: dont overrwite config.toml when verifying" https://github.com/rust-lang/rust/commit/92f263b792 Make RUSTC_OVERRIDE_VERSION_STRING overwrite the rendered version output, too https://github.com/rust-lang/rust/commit/cbab16feaf Test RUSTC_OVERRIDE_VERSION_STRING https://github.com/rust-lang/rust/commit/595316b400 Auto merge of #127955 - chenyukang:yukang-fix-mismatched-delimiter-issue-12786, r=nnethercote https://github.com/rust-lang/rust/commit/1ddedbaa59 Auto merge of #125929 - Bryanskiy:delegation-generics-3, r=petrochenkov https://github.com/rust-lang/rust/commit/e69c19ea0b Auto merge of #128336 - Bryanskiy:inst-binder-with-fresh, r=lcnr https://github.com/rust-lang/rust/commit/7e3a971870 Auto merge of #128378 - matthiaskrgr:rollup-i3qz9uo, r=matthiaskrgr https://github.com/rust-lang/rust/commit/710ce90fbe Auto merge of #128250 - Amanieu:select_unpredictable, r=nikic https://github.com/rust-lang/rust/commit/c2b085b4d4 Rollup merge of #128339 - GuillaumeGomez:click-code-example, r=notriddle https://github.com/rust-lang/rust/commit/f396a42ed6 Rollup merge of #128315 - zetanumbers:psvita-unsafe-in-unsafe, r=workingjubilee https://github.com/rust-lang/rust/commit/6b23cb5cdf Rollup merge of #128141 - nikic:aarch64-bti, r=DianQK,cuviper https://github.com/rust-lang/rust/commit/ae92125a75 Rollup merge of #127574 - lcnr:coherence-check-supertrait, r=compiler-errors https://github.com/rust-lang/rust/commit/dba8e2d2c2 Auto merge of #128234 - jcsp:retain-empty-case, r=tgross35 https://github.com/rust-lang/rust/commit/368e2fd458 Auto merge of #128360 - matthiaskrgr:rollup-wwy5mkj, r=matthiaskrgr https://github.com/rust-lang/rust/commit/c2616203bc Rollup merge of #128355 - jieyouxu:rename-nora, r=aDotInTheVoid https://github.com/rust-lang/rust/commit/4d78d11bf9 Rollup merge of #128342 - onur-ozkan:ci-env-usage, r=Kobzol https://github.com/rust-lang/rust/commit/a73a025190 Rollup merge of #128284 - GKFX:stabilize-offset-of-nested, r=dtolnay,jieyouxu https://github.com/rust-lang/rust/commit/b02cf4c274 Rollup merge of #128153 - compiler-errors:mdpe, r=cjgillot https://github.com/rust-lang/rust/commit/91b18a058c Rollup merge of #128104 - mu001999-contrib:fix/128053, r=petrochenkov https://github.com/rust-lang/rust/commit/9aedec9313 Rollup merge of #126247 - notriddle:notriddle/word-wrap-item-table, r=GuillaumeGomez https://github.com/rust-lang/rust/commit/99906dc89c Add rustdoc GUI test to check click on code examples https://github.com/rust-lang/rust/commit/a7cb1a5352 Make the buttons remain when code example is clicked https://github.com/rust-lang/rust/commit/ac303df4e2 rustdoc: move the wbr after the underscore, instead of before https://github.com/rust-lang/rust/commit/3bf8bcfbe0 rustdoc: properly handle path wrapping https://github.com/rust-lang/rust/commit/1d339b07ca rustdoc: use `` in sidebar headers https://github.com/rust-lang/rust/commit/f2f9aab380 Delegation: support generics for delegation from free functions https://github.com/rust-lang/rust/commit/f4fa80ff5a triagebot: make sure Nora is called Nora https://github.com/rust-lang/rust/commit/23f46e5b99 Stabilize offset_of_nested https://github.com/rust-lang/rust/commit/f990239b34 Stop using MoveDataParamEnv for places that don't need a param-env https://github.com/rust-lang/rust/commit/9186001f34 rustdoc: avoid redundant HTML when there's already line breaks https://github.com/rust-lang/rust/commit/0d0e18e7f6 rustdoc: use ``-tolerant function to check text contents https://github.com/rust-lang/rust/commit/583bf1e5bf Fix tidy call in runtest with custom HTML element https://github.com/rust-lang/rust/commit/f3661dce09 rustdoc: word wrap CamelCase in the item list table https://github.com/rust-lang/rust/commit/06d64ea4c4 simplify the use of `CiEnv` https://github.com/rust-lang/rust/commit/8a5efd1456 Use Vec in instantiate_binder_with_fresh_vars https://github.com/rust-lang/rust/commit/6a6824a0ab Optimize empty case in Vec::retain https://github.com/rust-lang/rust/commit/649d99b973 Bless a bootstrap-dependent UI test https://github.com/rust-lang/rust/commit/5eca36d27a step cfg(bootstrap) https://github.com/rust-lang/rust/commit/fceb0863d8 Bump stage0 to 1.81 beta https://github.com/rust-lang/rust/commit/e8644f85b8 Update CURRENT_RUSTC_VERSION https://github.com/rust-lang/rust/commit/0a5a84ee34 Add forbid(unsafe_op_in_unsafe_fn) https://github.com/rust-lang/rust/commit/352707da76 fix: psvita's std code https://github.com/rust-lang/rust/commit/4f78f9fbb0 Force LLVM to use CMOV for binary search https://github.com/rust-lang/rust/commit/adf0dff10c Not lint pub structs without pub constructors if containing fields of unit, never type, PhantomData and positional ZST https://github.com/rust-lang/rust/commit/94a3fd7678 add limit for unclosed delimiters in lexer diagnostic https://github.com/rust-lang/rust/commit/9a5e41c56f add testcase for 127868 https://github.com/rust-lang/rust/commit/ea7625f426 Set branch protection function attributes https://github.com/rust-lang/rust/commit/fe0bd76a8b elaborate unknowable goals 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 10c7645cf1d7..f7324e45d06d 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-07-30" +channel = "nightly-2024-07-31" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From e4078b4bdb2bb44c048d7880f9220297dd886a44 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 31 Jul 2024 11:55:12 +0200 Subject: [PATCH 04/11] Update to CBMC version 6.1.1 (#2995) Updates to match changes to the GOTO binary format. Resolves: #2952, #2972, #3287, #3391 This includes changes our handling of storage markers to be marking is-alive only rather than treating StorageLive as creating a new object. That is, object instances are now tied to their Mir-provided declarations (which, at present, only appear once per function). To still account for when Rust scopes deem an object to be alive, we use StorageLive and StorageDead to update __CPROVER_dead_object. This (global) variable is used by CBMC's pointer checks to track when a pointer may not be safe to dereference for it could be pointing to an object that no longer is in scope. Resolves: #3099 --- cprover_bindings/src/env.rs | 15 ++++- .../src/irep/goto_binary_serde.rs | 10 ++-- cprover_bindings/src/irep/irep_id.rs | 4 +- cprover_bindings/src/irep/to_irep.rs | 2 +- cprover_bindings/src/lib.rs | 1 + kani-compiler/src/args.rs | 3 - .../codegen/statement.rs | 59 +++++++++++++++++-- .../context/current_fn.rs | 31 +++++++++- kani-dependencies | 6 +- kani-driver/src/args/mod.rs | 8 --- kani-driver/src/call_cbmc.rs | 39 ++++++++---- kani-driver/src/call_goto_instrument.rs | 2 + kani-driver/src/call_single_file.rs | 4 -- kani-driver/src/cbmc_output_parser.rs | 4 ++ .../dead-invalid-access-via-raw/main.expected | 6 -- .../value.expected | 1 - .../shadow/unsupported_num_objects/test.rs | 10 ++-- tests/kani/FloatingPoint/main.rs | 1 - .../Intrinsics/Math/Rounding/Ceil/ceilf64.rs | 2 - .../Math/Rounding/Floor/floorf64.rs | 2 - .../Math/Rounding/NearbyInt/nearbyintf32.rs | 2 - .../Math/Rounding/NearbyInt/nearbyintf64.rs | 2 - .../Intrinsics/Math/Rounding/RInt/rintf32.rs | 2 - .../Intrinsics/Math/Rounding/RInt/rintf64.rs | 2 - .../Math/Rounding/Round/roundf32.rs | 2 - .../Math/Rounding/Round/roundf64.rs | 2 - .../Math/Rounding/Trunc/truncf64.rs | 2 - .../main.rs} | 2 +- tests/perf/btreeset/insert_any/Cargo.toml | 5 -- tests/perf/btreeset/insert_multi/Cargo.toml | 5 -- tests/perf/btreeset/insert_same/Cargo.toml | 5 -- tests/perf/hashset/Cargo.toml | 5 -- tests/perf/s2n-quic | 2 +- .../Strings/copy_empty_string_by_intrinsic.rs | 0 .../{ => slow}/kani/Vectors/any/push_slow.rs | 0 .../signed-overflow/check_message.rs | 1 - tests/ui/cbmc_checks/signed-overflow/expected | 1 - tools/benchcomp/configs/perf-regression.yaml | 4 +- 38 files changed, 152 insertions(+), 102 deletions(-) rename tests/kani/{Spurious/storage_fixme.rs => StorageMarkers/main.rs} (99%) rename tests/{ => slow}/kani/Strings/copy_empty_string_by_intrinsic.rs (100%) rename tests/{ => slow}/kani/Vectors/any/push_slow.rs (100%) diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs index 42080e52119a..d31d213aa7d2 100644 --- a/cprover_bindings/src/env.rs +++ b/cprover_bindings/src/env.rs @@ -8,7 +8,7 @@ //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp]. //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\]. -use super::goto_program::{Expr, Location, Symbol, Type}; +use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type}; use super::MachineModel; use num::bigint::BigInt; fn int_constant(name: &str, value: T) -> Symbol @@ -71,6 +71,8 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec { ] } +const DEAD_OBJECT_IDENTIFIER: &str = "__CPROVER_dead_object"; + pub fn additional_env_symbols() -> Vec { vec![ Symbol::builtin_function("__CPROVER_initialize", vec![], Type::empty()), @@ -82,5 +84,16 @@ pub fn additional_env_symbols() -> Vec { Location::none(), ) .with_is_extern(true), + Symbol::static_variable( + DEAD_OBJECT_IDENTIFIER, + DEAD_OBJECT_IDENTIFIER, + Type::void_pointer(), + Location::none(), + ) + .with_is_extern(true), ] } + +pub fn global_dead_object(symbol_table: &SymbolTable) -> Expr { + symbol_table.lookup(DEAD_OBJECT_IDENTIFIER).unwrap().to_expr() +} diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index 324c5e764d1a..6f821768f996 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/cprover_bindings/src/irep/goto_binary_serde.rs @@ -11,7 +11,7 @@ use std::io::{self, BufReader}; use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write}; use std::path::Path; -/// Writes a symbol table to a file in goto binary format in version 5. +/// Writes a symbol table to a file in goto binary format in version 6. /// /// In CBMC, the serialization rules are defined in : /// - src/goto-programs/write_goto_binary.h @@ -26,7 +26,7 @@ pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::Sym serializer.write_file(irep_symbol_table); } -/// Reads a symbol table from a file expected to be in goto binary format in version 5. +/// Reads a symbol table from a file expected to be in goto binary format in version 6. // /// In CBMC, the deserialization rules are defined in : /// - src/goto-programs/read_goto_binary.h @@ -540,7 +540,7 @@ where assert!(written == 4); // Write goto binary version - self.write_usize_varenc(5); + self.write_usize_varenc(6); } /// Writes the symbol table using the GOTO binary file format to the byte stream. @@ -921,12 +921,12 @@ where // Read goto binary version let goto_binary_version = self.read_usize_varenc()?; - if goto_binary_version != 5 { + if goto_binary_version != 6 { return Err(Error::new( ErrorKind::Other, format!( "Unsupported GOTO binary version: {}. Supported version: {}", - goto_binary_version, 5 + goto_binary_version, 6 ), )); } diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 9d52f4ef32fa..69962edf150e 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -366,7 +366,7 @@ pub enum IrepId { Div, Power, FactorialPower, - PrettyName, + CPrettyName, CClass, CField, CInterface, @@ -1242,7 +1242,7 @@ impl Display for IrepId { IrepId::Div => "/", IrepId::Power => "**", IrepId::FactorialPower => "factorial_power", - IrepId::PrettyName => "pretty_name", + IrepId::CPrettyName => "#pretty_name", IrepId::CClass => "#class", IrepId::CField => "#field", IrepId::CInterface => "#interface", diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 05774fdf8b43..bf0b8ce862dd 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -132,7 +132,7 @@ impl ToIrep for DatatypeComponent { match self { DatatypeComponent::Field { name, typ } => Irep::just_named_sub(linear_map![ (IrepId::Name, Irep::just_string_id(name.to_string())), - (IrepId::PrettyName, Irep::just_string_id(name.to_string())), + (IrepId::CPrettyName, Irep::just_string_id(name.to_string())), (IrepId::Type, typ.to_irep(mm)), ]), DatatypeComponent::Padding { name, bits } => Irep::just_named_sub(linear_map![ diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs index e77b29a24ca2..a5901afbac2d 100644 --- a/cprover_bindings/src/lib.rs +++ b/cprover_bindings/src/lib.rs @@ -33,6 +33,7 @@ #![feature(f16)] mod env; +pub use env::global_dead_object; pub mod goto_program; pub mod irep; mod machine_model; diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index e4b7a4435b0f..3efc5c0f4f61 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -74,9 +74,6 @@ pub struct Arguments { /// Enable specific checks. #[clap(long)] pub ub_check: Vec, - /// Ignore storage markers. - #[clap(long)] - pub ignore_storage_markers: bool, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 697cacd3b191..b8db1a3d52b6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -75,18 +75,68 @@ impl<'tcx> GotocCtx<'tcx> { .goto_expr; self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } + // StorageLive and StorageDead are modelled via CBMC's internal means of detecting + // accesses to dangling pointers, which uses demonic non-determinism. That is, CBMC + // non-deterministically chooses a single object's address to be tracked in a + // pointer-typed global instrumentation variable __CPROVER_dead_object. Any dereference + // entails a check that the pointer being dereferenced is not equal to the pointer held + // in __CPROVER_dead_object. We use this to bridge the difference between Rust and MIR + // semantics as follows: + // + // 1. (At the time of writing) MIR declares all function-local variables at function + // scope, irrespective of the scope/block that Rust code originally used. + // 2. In MIR, StorageLive and StorageDead markers are inserted at the beginning and end + // of the Rust block to record the Rust-level lifetime of the object. + // 3. We translate MIR declarations into GOTO declarations, implying that we will have + // a single object per function for a local variable, even when Rust had a variable + // declared in a sub-scope of the function where said scope was entered multiple + // times (e.g., a loop body). + // 4. To enable detection of use of dangling pointers, we now use + // __CPROVER_dead_object, unless the address of the local object is never taken + // (implying that there cannot be a use of a dangling pointer with respect to said + // object). We update __CPROVER_dead_object as follows: + // * StorageLive is set to NULL when __CPROVER_dead_object pointed to the object + // (re-)entering scope, or else is left unchanged. + // * StorageDead non-deterministically updates (or leaves unchanged) + // __CPROVER_dead_object to point to the object going out of scope. (This is the + // same update approach as used within CBMC.) + // + // This approach will also work when there are multiple occurrences of StorageLive (or + // StorageDead) on a path, or across control-flow branches, and even when StorageDead + // occurs without a preceding StorageLive. StatementKind::StorageLive(var_id) => { - if self.queries.args().ignore_storage_markers { + if !self.current_fn().is_address_taken_local(*var_id) { Stmt::skip(location) } else { - Stmt::decl(self.codegen_local(*var_id, location), None, location) + let global_dead_object = cbmc::global_dead_object(&self.symbol_table); + Stmt::assign( + global_dead_object.clone(), + global_dead_object + .clone() + .eq(self + .codegen_local(*var_id, location) + .address_of() + .cast_to(global_dead_object.typ().clone())) + .ternary(global_dead_object.typ().null(), global_dead_object), + location, + ) } } StatementKind::StorageDead(var_id) => { - if self.queries.args().ignore_storage_markers { + if !self.current_fn().is_address_taken_local(*var_id) { Stmt::skip(location) } else { - Stmt::dead(self.codegen_local(*var_id, location), location) + let global_dead_object = cbmc::global_dead_object(&self.symbol_table); + Stmt::assign( + global_dead_object.clone(), + Type::bool().nondet().ternary( + self.codegen_local(*var_id, location) + .address_of() + .cast_to(global_dead_object.typ().clone()), + global_dead_object, + ), + location, + ) } } StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( @@ -424,6 +474,7 @@ impl<'tcx> GotocCtx<'tcx> { .branches() .map(|(c, bb)| { Expr::int_constant(c, switch_ty.clone()) + .with_location(loc) .switch_case(Stmt::goto(bb_label(bb), loc)) }) .collect(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index 32c5d72f7007..ea3c9e909eb6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -7,9 +7,9 @@ use cbmc::InternedString; use rustc_middle::ty::Instance as InstanceInternal; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, Local, LocalDecl}; +use stable_mir::mir::{visit::Location, visit::MirVisitor, Body, Local, LocalDecl, Rvalue}; use stable_mir::CrateDef; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; /// This structure represents useful data about the function we are currently compiling. #[derive(Debug)] @@ -26,6 +26,8 @@ pub struct CurrentFnCtx<'tcx> { locals: Vec, /// A list of pretty names for locals that corrspond to user variables. local_names: HashMap, + /// Collection of variables that are used in a reference or address-of expression. + address_taken_locals: HashSet, /// The symbol name of the current function name: String, /// A human readable pretty name for the current function @@ -34,6 +36,24 @@ pub struct CurrentFnCtx<'tcx> { temp_var_counter: u64, } +struct AddressTakenLocalsCollector { + /// Locals that appear in `Rvalue::Ref` or `Rvalue::AddressOf` expressions. + address_taken_locals: HashSet, +} + +impl MirVisitor for AddressTakenLocalsCollector { + fn visit_rvalue(&mut self, rvalue: &Rvalue, _location: Location) { + match rvalue { + Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => { + if p.projection.is_empty() { + self.address_taken_locals.insert(p.local); + } + } + _ => (), + } + } +} + /// Constructor impl<'tcx> CurrentFnCtx<'tcx> { pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self { @@ -46,6 +66,8 @@ impl<'tcx> CurrentFnCtx<'tcx> { .iter() .filter_map(|info| info.local().map(|local| (local, (&info.name).into()))) .collect::>(); + let mut visitor = AddressTakenLocalsCollector { address_taken_locals: HashSet::new() }; + visitor.visit_body(body); Self { block: vec![], instance, @@ -53,6 +75,7 @@ impl<'tcx> CurrentFnCtx<'tcx> { krate: instance.def.krate().name, locals, local_names, + address_taken_locals: visitor.address_taken_locals, name, readable_name, temp_var_counter: 0, @@ -106,6 +129,10 @@ impl<'tcx> CurrentFnCtx<'tcx> { pub fn local_name(&self, local: Local) -> Option { self.local_names.get(&local).copied() } + + pub fn is_address_taken_local(&self, local: Local) -> bool { + self.address_taken_locals.contains(&local) + } } /// Utility functions diff --git a/kani-dependencies b/kani-dependencies index 844d83c23dc7..421188a08762 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,6 +1,6 @@ -CBMC_MAJOR="5" -CBMC_MINOR="95" -CBMC_VERSION="5.95.1" +CBMC_MAJOR="6" +CBMC_MINOR="1" +CBMC_VERSION="6.1.1" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_MAJOR="3" diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index d043035bcab2..158f1c001b5b 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -245,14 +245,6 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true, requires("enable_unstable"))] pub ignore_global_asm: bool, - /// Ignore lifetimes of local variables. This effectively extends their - /// lifetimes to the function scope, and hence may cause Kani to miss - /// undefined behavior resulting from using the variable after it dies. - /// This option may impact the soundness of the analysis and may cause false - /// proofs and/or counterexamples - #[arg(long, hide_short_help = true, requires("enable_unstable"))] - pub ignore_locals_lifetime: bool, - /// Write the GotoC symbol table to a file in JSON format instead of goto binary format. #[arg(long, hide_short_help = true)] pub write_json_symtab: bool, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 81d50865cc13..387a9723fcdb 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -153,6 +153,11 @@ impl KaniSession { args.push(file.to_owned().into_os_string()); + // Make CBMC verbose by default to tell users about unwinding progress. This should be + // reviewed as CBMC's verbosity defaults evolve. + args.push("--verbosity".into()); + args.push("9".into()); + Ok(args) } @@ -160,18 +165,25 @@ impl KaniSession { pub fn cbmc_check_flags(&self) -> Vec { let mut args = Vec::new(); - if self.args.checks.memory_safety_on() { - args.push("--bounds-check".into()); - args.push("--pointer-check".into()); + // We assume that malloc cannot fail, see https://github.com/model-checking/kani/issues/891 + args.push("--no-malloc-may-fail".into()); + + // With PR #2630 we generate the appropriate checks directly rather than relying on CBMC's + // checks (which are for C semantics). + args.push("--no-undefined-shift-check".into()); + // With PR #647 we use Rust's `-C overflow-checks=on` instead of: + // --unsigned-overflow-check + // --signed-overflow-check + // So these options are deliberately skipped to avoid erroneously re-checking operations. + args.push("--no-signed-overflow-check".into()); + + if !self.args.checks.memory_safety_on() { + args.push("--no-bounds-check".into()); + args.push("--no-pointer-check".into()); } if self.args.checks.overflow_on() { - args.push("--div-by-zero-check".into()); args.push("--float-overflow-check".into()); args.push("--nan-check".into()); - // With PR #647 we use Rust's `-C overflow-checks=on` instead of: - // --unsigned-overflow-check - // --signed-overflow-check - // So these options are deliberately skipped to avoid erroneously re-checking operations. // TODO: Implement conversion checks as an optional check. // They are a well defined operation in rust, but they may yield unexpected results to @@ -179,11 +191,13 @@ impl KaniSession { // We might want to create a transformation pass instead of enabling CBMC since Kani // compiler sometimes rely on the bitwise conversion of signed <-> unsigned. // args.push("--conversion-check".into()); + } else { + args.push("--no-div-by-zero-check".into()); } - if self.args.checks.unwinding_on() { - // TODO: With CBMC v6 the below can be removed as those are defaults. - args.push("--unwinding-assertions".into()); + if !self.args.checks.unwinding_on() { + args.push("--no-unwinding-assertions".into()); + } else { args.push("--no-self-loops-to-assumptions".into()); } @@ -192,7 +206,8 @@ impl KaniSession { // still catch any invalid dereference with --pointer-check. Thus, only enable them // if the user explicitly request them. args.push("--pointer-overflow-check".into()); - args.push("--pointer-primitive-check".into()); + } else { + args.push("--no-pointer-primitive-check".into()); } args diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 83744eddabfd..ae76be150871 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -93,6 +93,7 @@ impl KaniSession { fn add_library(&self, file: &Path) -> Result<()> { let args: Vec = vec![ "--add-library".into(), + "--no-malloc-may-fail".into(), file.to_owned().into_os_string(), // input file.to_owned().into_os_string(), // output ]; @@ -173,6 +174,7 @@ impl KaniSession { assigns.contracted_function_name.as_str().into(), "--nondet-static-exclude".into(), assigns.recursion_tracker.as_str().into(), + "--no-malloc-may-fail".into(), file.into(), file.into(), ]; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 411dabb5270e..bbeb5bfa417d 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -146,10 +146,6 @@ impl KaniSession { flags.push("--ub-check=uninit".into()); } - if self.args.ignore_locals_lifetime { - flags.push("--ignore-storage-markers".into()) - } - flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); // This argument will select the Kani flavour of the compiler. It will be removed before diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 127f98beab56..b3a78e8d03e2 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -329,6 +329,7 @@ pub enum CheckStatus { Satisfied, // for `cover` properties only Success, Undetermined, + Unknown, Unreachable, Uncovered, // for `code_coverage` properties only Unsatisfiable, // for `cover` properties only @@ -344,6 +345,9 @@ impl std::fmt::Display for CheckStatus { CheckStatus::Failure => style("FAILURE").red(), CheckStatus::Unreachable => style("UNREACHABLE").yellow(), CheckStatus::Undetermined => style("UNDETERMINED").yellow(), + // CBMC 6+ uses UNKNOWN when another property of undefined behavior failed, making it + // impossible to definitively conclude whether other properties hold or not. + CheckStatus::Unknown => style("UNDETERMINED").yellow(), CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(), }; write!(f, "{check_str}") diff --git a/tests/expected/dead-invalid-access-via-raw/main.expected b/tests/expected/dead-invalid-access-via-raw/main.expected index 1d464eb5f031..1cdbd0547226 100644 --- a/tests/expected/dead-invalid-access-via-raw/main.expected +++ b/tests/expected/dead-invalid-access-via-raw/main.expected @@ -1,7 +1,5 @@ SUCCESS\ address must be a multiple of its type's alignment -FAILURE\ -unsafe { *raw_ptr } == 10 SUCCESS\ pointer NULL SUCCESS\ @@ -10,7 +8,3 @@ SUCCESS\ deallocated dynamic object FAILURE\ dead object -SUCCESS\ -pointer outside object bounds -SUCCESS\ -invalid integer address diff --git a/tests/expected/dead-invalid-access-via-raw/value.expected b/tests/expected/dead-invalid-access-via-raw/value.expected index 858d44d54ea4..525e5e40a3b2 100644 --- a/tests/expected/dead-invalid-access-via-raw/value.expected +++ b/tests/expected/dead-invalid-access-via-raw/value.expected @@ -1,2 +1 @@ -Failed Checks: assertion failed: *p_subscoped == 7 Failed Checks: dereference failure: dead object diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index f60d0020e989..88b1171ef09d 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -15,14 +15,14 @@ fn check_max_objects() { // - the NULL pointer whose object ID is 0, and // - the object ID for `i` while i < N { - let x = i; - assert_eq!(kani::mem::pointer_object(&x as *const usize), i + 2); + let x: Box = Box::new(i); + assert_eq!(kani::mem::pointer_object(&*x as *const usize), 2 * i + 2); i += 1; } // create a new object whose ID is `N` + 2 let x = 42; - assert_eq!(kani::mem::pointer_object(&x as *const i32), N + 2); + assert_eq!(kani::mem::pointer_object(&x as *const i32), 2 * N + 2); // the following call to `set` would fail if the object ID for `x` exceeds // the maximum allowed by Kani's shadow memory model unsafe { @@ -32,10 +32,10 @@ fn check_max_objects() { #[kani::proof] fn check_max_objects_pass() { - check_max_objects::<1021>(); + check_max_objects::<510>(); } #[kani::proof] fn check_max_objects_fail() { - check_max_objects::<1022>(); + check_max_objects::<511>(); } diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs index 93a29f169f27..f8ebccdac02a 100644 --- a/tests/kani/FloatingPoint/main.rs +++ b/tests/kani/FloatingPoint/main.rs @@ -26,7 +26,6 @@ macro_rules! test_floats { } #[kani::proof] -#[kani::solver(minisat)] fn main() { assert!(1.1 == 1.1 * 1.0); assert!(1.1 != 1.11 / 1.0); diff --git a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs index 642d984a7e2b..09c630aa94a7 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs @@ -45,7 +45,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_inf() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -54,7 +53,6 @@ fn test_towards_inf() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs index 54ad74c33430..0560a2c55064 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs @@ -45,7 +45,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_neg_inf() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -54,7 +53,6 @@ fn test_towards_neg_inf() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs index 7ffdb5f28747..25e02f45a943 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs @@ -50,7 +50,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -89,7 +88,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs index bf656512562e..589a44a4d1ac 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs @@ -50,7 +50,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -89,7 +88,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs index 53d9d7d5fc73..79a0a4f9be2c 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs @@ -55,7 +55,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -94,7 +93,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs index de608e7cdb9f..8c8ea583a2d5 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs @@ -55,7 +55,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -94,7 +93,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs index 04893727dcfa..8a8780878925 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs @@ -39,7 +39,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_closer() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -62,7 +61,6 @@ fn test_towards_closer() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs index cd61e9607646..ddafc45a2e9e 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs @@ -39,7 +39,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_closer() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -62,7 +61,6 @@ fn test_towards_closer() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs index a8a80672e36b..5fcc8c80606d 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs @@ -38,7 +38,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_zero() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -51,7 +50,6 @@ fn test_towards_zero() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Spurious/storage_fixme.rs b/tests/kani/StorageMarkers/main.rs similarity index 99% rename from tests/kani/Spurious/storage_fixme.rs rename to tests/kani/StorageMarkers/main.rs index 51d13f31bcef..770995605ded 100644 --- a/tests/kani/Spurious/storage_fixme.rs +++ b/tests/kani/StorageMarkers/main.rs @@ -3,7 +3,7 @@ // Modifications Copyright Kani Contributors // See GitHub history for details. -// Our handling of storage markers causes spurious failures in this test. +// Our handling of storage markers used to cause spurious failures in this test. // https://github.com/model-checking/kani/issues/3099 // The code is extracted from the implementation of `BTreeMap` which is where we // originally saw the spurious failures while trying to enable storage markers diff --git a/tests/perf/btreeset/insert_any/Cargo.toml b/tests/perf/btreeset/insert_any/Cargo.toml index 66d8ecdddeb1..41fa0a2db3ba 100644 --- a/tests/perf/btreeset/insert_any/Cargo.toml +++ b/tests/perf/btreeset/insert_any/Cargo.toml @@ -9,8 +9,3 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/btreeset/insert_multi/Cargo.toml b/tests/perf/btreeset/insert_multi/Cargo.toml index 44028f8c842d..bdd2f4e3528a 100644 --- a/tests/perf/btreeset/insert_multi/Cargo.toml +++ b/tests/perf/btreeset/insert_multi/Cargo.toml @@ -9,8 +9,3 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/btreeset/insert_same/Cargo.toml b/tests/perf/btreeset/insert_same/Cargo.toml index 465119c74fbe..0a4e0f7ee037 100644 --- a/tests/perf/btreeset/insert_same/Cargo.toml +++ b/tests/perf/btreeset/insert_same/Cargo.toml @@ -9,8 +9,3 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/hashset/Cargo.toml b/tests/perf/hashset/Cargo.toml index 464fba412e6d..d0757e11154b 100644 --- a/tests/perf/hashset/Cargo.toml +++ b/tests/perf/hashset/Cargo.toml @@ -12,8 +12,3 @@ description = "Verify HashSet basic behavior" [package.metadata.kani.unstable] stubbing = true - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index cc4e6d023f8e..71f8d9f5aafb 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit cc4e6d023f8edf92fea294dcaea2fd5a1132cb47 +Subproject commit 71f8d9f5aafbf59f31ad85eeb7b4b67a7564a685 diff --git a/tests/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs similarity index 100% rename from tests/kani/Strings/copy_empty_string_by_intrinsic.rs rename to tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs diff --git a/tests/kani/Vectors/any/push_slow.rs b/tests/slow/kani/Vectors/any/push_slow.rs similarity index 100% rename from tests/kani/Vectors/any/push_slow.rs rename to tests/slow/kani/Vectors/any/push_slow.rs diff --git a/tests/ui/cbmc_checks/signed-overflow/check_message.rs b/tests/ui/cbmc_checks/signed-overflow/check_message.rs index 0a1527e9a8fc..af496192ee60 100644 --- a/tests/ui/cbmc_checks/signed-overflow/check_message.rs +++ b/tests/ui/cbmc_checks/signed-overflow/check_message.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // // Check we don't print temporary variables as part of CBMC messages. -// cbmc-flags: --signed-overflow-check extern crate kani; use kani::any; diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected index 70669b325e9e..80d3eef3cd25 100644 --- a/tests/ui/cbmc_checks/signed-overflow/expected +++ b/tests/ui/cbmc_checks/signed-overflow/expected @@ -7,4 +7,3 @@ Failed Checks: attempt to calculate the remainder with a divisor of zero Failed Checks: attempt to calculate the remainder with overflow Failed Checks: attempt to shift left with overflow Failed Checks: attempt to shift right with overflow -Failed Checks: arithmetic overflow on signed shl diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml index c938b3dd861f..d1e65b24ca2c 100644 --- a/tools/benchcomp/configs/perf-regression.yaml +++ b/tools/benchcomp/configs/perf-regression.yaml @@ -10,13 +10,13 @@ variants: kani_new: config: directory: new - command_line: scripts/kani-perf.sh + command_line: "scripts/setup/ubuntu/install_deps.sh && scripts/kani-perf.sh" env: RUST_TEST_THREADS: "1" kani_old: config: directory: old - command_line: scripts/kani-perf.sh + command_line: "scripts/setup/ubuntu/install_deps.sh && scripts/kani-perf.sh" env: RUST_TEST_THREADS: "1" From 7e02353ff36bc6d08ede14c4e52c5f46c8f3b7f1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 31 Jul 2024 17:11:01 +0200 Subject: [PATCH 05/11] Reduce memory consumption of cell_stub.rs test (#3399) With MiniSat the test takes 45 seconds instead of 30 seconds, but only consumes 5.5 GB of memory instead of 9 GB. This will hopefully fix CI failures. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../function-contract/interior-mutability/api/cell_stub.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs index d01ca379655f..9752bec5d272 100644 --- a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs +++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts +// kani-flags: -Zfunction-contracts --solver minisat /// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple. /// This shows that we can generate `kani::any()` for Cell. From b5d306ac9ababf8045cf1f6abefb1616fe0ee651 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 31 Jul 2024 11:58:29 -0400 Subject: [PATCH 06/11] Define a struct-level `#[safety_constraint(...)]` attribute (#3270) This PR defines a struct-level `#[safety_constraint()]` macro attribute that allows users to define the type invariant as the predicate passed as an argument to the attribute. This safety constraint is picked up when deriving `Arbitrary` and `Invariant` implementations so that the values generated with `any()` or checked with `is_safe()` satisfy the constraint. This attribute is similar to the helper attribute introduced in #3283, and they cannot be used together. It's preferable to use this attribute when the constraint implies some relation between different fields. But, at the moment, there's no practical difference between them because the helper attribute allows users to refer to any fields. If we imposed that restriction, this attribute would be the only way to specify struct-wide invariants. An example: ```rs #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] #[safety_constraint(*x == *y)] struct SameCoordsPoint { x: i32, y: i32, } #[kani::proof] fn check_invariant() { let point: SameCoordsPoint = kani::any(); assert!(point.is_safe()); } ``` Resolves #3095 --- library/kani_macros/src/derive.rs | 321 ++++++++++++------ .../abstract-value/abstract-value.rs | 30 ++ .../abstract-value/expected | 7 + .../check-arbitrary/check-arbitrary.rs | 24 ++ .../check-arbitrary/expected | 11 + .../check-invariant/check-invariant.rs | 27 ++ .../check-invariant/expected | 7 + .../grade-example/expected | 11 + .../grade-example/grade-example.rs | 43 +++ .../double-attribute/double-attribute.rs | 16 + .../double-attribute/expected | 6 + .../invalid-pred-error/expected | 19 ++ .../invalid-pred-error/invalid-pred-error.rs | 19 ++ .../mixed-attributes/expected | 6 + .../mixed-attributes/mixed-attributes.rs | 17 + .../no-struct-error/expected | 6 + .../no-struct-error/no-struct-error.rs | 18 + 17 files changed, 490 insertions(+), 98 deletions(-) create mode 100644 tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs create mode 100644 tests/expected/safety-constraint-attribute/abstract-value/expected create mode 100644 tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs create mode 100644 tests/expected/safety-constraint-attribute/check-arbitrary/expected create mode 100644 tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs create mode 100644 tests/expected/safety-constraint-attribute/check-invariant/expected create mode 100644 tests/expected/safety-constraint-attribute/grade-example/expected create mode 100644 tests/expected/safety-constraint-attribute/grade-example/grade-example.rs create mode 100644 tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs create mode 100644 tests/ui/safety-constraint-attribute/double-attribute/expected create mode 100644 tests/ui/safety-constraint-attribute/invalid-pred-error/expected create mode 100644 tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs create mode 100644 tests/ui/safety-constraint-attribute/mixed-attributes/expected create mode 100644 tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs create mode 100644 tests/ui/safety-constraint-attribute/no-struct-error/expected create mode 100644 tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index a7aaa8ae334e..cc936560e510 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -19,20 +19,20 @@ use syn::{ }; pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream { + let trait_name = "Arbitrary"; let derive_item = parse_macro_input!(item as DeriveInput); let item_name = &derive_item.ident; + let body = fn_any_body(&item_name, &derive_item.data); + // Get the safety constraints (if any) to produce type-safe values + let safety_conds_opt = safety_conds_opt(&item_name, &derive_item, trait_name); + // Add a bound `T: Arbitrary` to every type parameter T. let generics = add_trait_bound_arbitrary(derive_item.generics); // Generate an expression to sum up the heap size of each field. let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); - let body = fn_any_body(&item_name, &derive_item.data); - - // Get the safety constraints (if any) to produce type-safe values - let safety_conds_opt = safety_conds(&item_name, &derive_item.data); - - let expanded = if let Some(safety_cond) = safety_conds_opt { + let expanded = if let Some(safety_conds) = safety_conds_opt { let field_refs = field_refs(&item_name, &derive_item.data); quote! { // The generated implementation. @@ -40,7 +40,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok fn any() -> Self { let obj = #body; #field_refs - kani::assume(#safety_cond); + kani::assume(#safety_conds); obj } } @@ -94,48 +94,6 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// Parse the condition expressions in `#[safety_constraint()]` attached to struct -/// fields and, it at least one was found, generate a conjunction to be assumed. -/// -/// For example, if we're deriving implementations for the struct -/// ``` -/// #[derive(Arbitrary)] -/// #[derive(Invariant)] -/// struct PositivePoint { -/// #[safety_constraint(*x >= 0)] -/// x: i32, -/// #[safety_constraint(*y >= 0)] -/// y: i32, -/// } -/// ``` -/// this function will generate the `TokenStream` -/// ``` -/// *x >= 0 && *y >= 0 -/// ``` -/// which can be passed to `kani::assume` to constrain the values generated -/// through the `Arbitrary` impl so that they are type-safe by construction. -fn safety_conds(ident: &Ident, data: &Data) -> Option { - match data { - Data::Struct(struct_data) => safety_conds_inner(ident, &struct_data.fields), - Data::Enum(_) => None, - Data::Union(_) => None, - } -} - -/// Generates an expression resulting from the conjunction of conditions -/// specified as safety constraints for each field. See `safety_conds` for more details. -fn safety_conds_inner(ident: &Ident, fields: &Fields) -> Option { - match fields { - Fields::Named(ref fields) => { - let conds: Vec = - fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect(); - if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None } - } - Fields::Unnamed(_) => None, - Fields::Unit => None, - } -} - /// Generates the sequence of expressions to initialize the variables used as /// references to the struct fields. /// @@ -191,6 +149,55 @@ fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream { } } +fn safe_body_default(ident: &Ident, data: &Data) -> TokenStream { + match data { + Data::Struct(struct_data) => safe_body_default_inner(ident, &struct_data.fields), + Data::Enum(_) => unreachable!(), + Data::Union(_) => unreachable!(), + } +} + +fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream { + match fields { + Fields::Named(ref fields) => { + let field_safe_calls: Vec = fields + .named + .iter() + .map(|field| { + let name = &field.ident; + quote_spanned! {field.span()=> + #name.is_safe() + } + }) + .collect(); + if !field_safe_calls.is_empty() { + quote! { #( #field_safe_calls )&&* } + } else { + quote! { true } + } + } + Fields::Unnamed(ref fields) => { + let field_safe_calls: Vec = fields + .unnamed + .iter() + .enumerate() + .map(|(idx, field)| { + let field_idx = Index::from(idx); + quote_spanned! {field.span()=> + #field_idx.is_safe() + } + }) + .collect(); + if !field_safe_calls.is_empty() { + quote! { #( #field_safe_calls )&&* } + } else { + quote! { true } + } + } + Fields::Unit => quote! { true }, + } +} + /// Generate an item initialization where an item can be a struct or a variant. /// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` /// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` @@ -267,6 +274,38 @@ fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option { } } +fn parse_safety_expr_input(ident: &Ident, derive_input: &DeriveInput) -> Option { + let name = ident; + let mut safety_attr = None; + + // Keep the attribute if we find it + for attr in &derive_input.attrs { + if attr.path().is_ident("safety_constraint") { + safety_attr = Some(attr); + } + } + + // Parse the arguments in the `#[safety_constraint(...)]` attribute + if let Some(attr) = safety_attr { + let expr_args: Result = attr.parse_args(); + + // Check if there was an error parsing the arguments + if let Err(err) = expr_args { + abort!(Span::call_site(), "Cannot derive impl for `{}`", ident; + note = attr.span() => + "safety constraint in `{}` could not be parsed: {}", name.to_string(), err + ) + } + + // Return the expression associated to the safety constraint + let safety_expr = expr_args.unwrap(); + Some(quote_spanned! {derive_input.span()=> + #safety_expr + }) + } else { + None + } +} /// Generate the body of the function `any()` for enums. The cases are: /// 1. For zero-variants enumerations, this will encode a `panic!()` statement. /// 2. For one or more variants, the code will be something like: @@ -318,33 +357,112 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream { } } +fn safe_body_with_calls( + item_name: &Ident, + derive_input: &DeriveInput, + trait_name: &str, +) -> TokenStream { + let safety_conds_opt = safety_conds_opt(&item_name, &derive_input, trait_name); + let safe_body_default = safe_body_default(&item_name, &derive_input.data); + + if let Some(safety_conds) = safety_conds_opt { + quote! { #safe_body_default && #safety_conds } + } else { + safe_body_default + } +} + pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::TokenStream { + let trait_name = "Invariant"; let derive_item = parse_macro_input!(item as DeriveInput); let item_name = &derive_item.ident; + let safe_body = safe_body_with_calls(&item_name, &derive_item, trait_name); + let field_refs = field_refs(&item_name, &derive_item.data); + // Add a bound `T: Invariant` to every type parameter T. let generics = add_trait_bound_invariant(derive_item.generics); // Generate an expression to sum up the heap size of each field. let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); - let body = is_safe_body(&item_name, &derive_item.data); - let field_refs = field_refs(&item_name, &derive_item.data); - let expanded = quote! { // The generated implementation. impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause { fn is_safe(&self) -> bool { let obj = self; #field_refs - #body + #safe_body } } }; proc_macro::TokenStream::from(expanded) } +/// Looks for `#[safety_constraint(...)]` attributes used in the struct or its +/// fields, and returns the constraints if there were any, otherwise returns +/// `None`. +/// Note: Errors out if the attribute is used in both the struct and its fields. +fn safety_conds_opt( + item_name: &Ident, + derive_input: &DeriveInput, + trait_name: &str, +) -> Option { + let has_item_safety_constraint = + has_item_safety_constraint(&item_name, &derive_input, trait_name); + + let has_field_safety_constraints = has_field_safety_constraints(&item_name, &derive_input.data); + + if has_item_safety_constraint && has_field_safety_constraints { + abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, item_name; + note = item_name.span() => + "`#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously" + ) + } + + if has_item_safety_constraint { + Some(safe_body_from_struct_attr(&item_name, &derive_input, trait_name)) + } else if has_field_safety_constraints { + Some(safe_body_from_fields_attr(&item_name, &derive_input.data, trait_name)) + } else { + None + } +} + +fn has_item_safety_constraint(ident: &Ident, derive_input: &DeriveInput, trait_name: &str) -> bool { + let safety_constraints_in_item = + derive_input.attrs.iter().filter(|attr| attr.path().is_ident("safety_constraint")).count(); + if safety_constraints_in_item > 1 { + abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident; + note = ident.span() => + "`#[safety_constraint(...)]` cannot be used more than once." + ) + } + safety_constraints_in_item == 1 +} + +fn has_field_safety_constraints(ident: &Ident, data: &Data) -> bool { + match data { + Data::Struct(struct_data) => has_field_safety_constraints_inner(ident, &struct_data.fields), + Data::Enum(_) => false, + Data::Union(_) => false, + } +} + +/// Checks if the `#[safety_constraint(...)]` attribute is attached to any +/// field. +fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool { + match fields { + Fields::Named(ref fields) => fields + .named + .iter() + .any(|field| field.attrs.iter().any(|attr| attr.path().is_ident("safety_constraint"))), + Fields::Unnamed(_) => false, + Fields::Unit => false, + } +} + /// Add a bound `T: Invariant` to every type parameter T. -fn add_trait_bound_invariant(mut generics: Generics) -> Generics { +pub fn add_trait_bound_invariant(mut generics: Generics) -> Generics { generics.params.iter_mut().for_each(|param| { if let GenericParam::Type(type_param) = param { type_param.bounds.push(parse_quote!(kani::Invariant)); @@ -353,17 +471,51 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics { generics } -fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { +fn safe_body_from_struct_attr( + ident: &Ident, + derive_input: &DeriveInput, + trait_name: &str, +) -> TokenStream { + if !matches!(derive_input.data, Data::Struct(_)) { + abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident; + note = ident.span() => + "`#[safety_constraint(...)]` can only be used in structs" + ) + }; + parse_safety_expr_input(ident, derive_input).unwrap() +} + +/// Parse the condition expressions in `#[safety_constraint()]` attached to struct +/// fields and, it at least one was found, generate a conjunction to be assumed. +/// +/// For example, if we're deriving implementations for the struct +/// ``` +/// #[derive(Arbitrary)] +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` +/// this function will generate the `TokenStream` +/// ``` +/// *x >= 0 && *y >= 0 +/// ``` +/// which can be used by the `Arbitrary` and `Invariant` to generate and check +/// type-safe values for the struct, respectively. +fn safe_body_from_fields_attr(ident: &Ident, data: &Data, trait_name: &str) -> TokenStream { match data { - Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields), + Data::Struct(struct_data) => safe_body_from_fields_attr_inner(ident, &struct_data.fields), Data::Enum(_) => { - abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident; + abort!(Span::call_site(), "Cannot derive `{}` for `{}` enum", trait_name, ident; note = ident.span() => "`#[derive(Invariant)]` cannot be used for enums such as `{}`", ident ) } Data::Union(_) => { - abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` union", ident; + abort!(Span::call_site(), "Cannot derive `{}` for `{}` union", trait_name, ident; note = ident.span() => "`#[derive(Invariant)]` cannot be used for unions such as `{}`", ident ) @@ -371,50 +523,23 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// Generates an expression that is the conjunction of safety constraints for each field in the struct. -fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { +/// Generates an expression resulting from the conjunction of conditions +/// specified as safety constraints for each field. +/// See `safe_body_from_fields_attr` for more details. +fn safe_body_from_fields_attr_inner(ident: &Ident, fields: &Fields) -> TokenStream { match fields { // Expands to the expression - // `true && && && ..` - // where `safety_condN` is - // - `self.fieldN.is_safe() && ` if a condition `` was - // specified through the `#[safety_constraint()]` helper attribute, or - // - `self.fieldN.is_safe()` otherwise - // - // Therefore, if `#[safety_constraint()]` isn't specified for any field, this expands to - // `true && self.field1.is_safe() && self.field2.is_safe() && ..` + // ` && && ..` + // where `` is the safety condition specified for the N-th field. Fields::Named(ref fields) => { - let safety_conds: Vec = fields - .named - .iter() - .map(|field| { - let name = &field.ident; - let default_expr = quote_spanned! {field.span()=> - #name.is_safe() - }; - parse_safety_expr(ident, field) - .map(|expr| quote! { #expr && #default_expr}) - .unwrap_or(default_expr) - }) - .collect(); - // An initial value is required for empty structs - safety_conds.iter().fold(quote! { true }, |acc, cond| { - quote! { #acc && #cond } - }) + let safety_conds: Vec = + fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect(); + quote! { #(#safety_conds)&&* } } - Fields::Unnamed(ref fields) => { - // Expands to the expression - // `true && self.0.is_safe() && self.1.is_safe() && ..` - let safe_calls = fields.unnamed.iter().enumerate().map(|(i, field)| { - let idx = syn::Index::from(i); - quote_spanned! {field.span()=> - self.#idx.is_safe() - } - }); - // An initial value is required for empty structs - safe_calls.fold(quote! { true }, |acc, call| { - quote! { #acc && #call } - }) + Fields::Unnamed(_) => { + quote! { + true + } } // Expands to the expression // `true` diff --git a/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs b/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs new file mode 100644 index 000000000000..6e29938d4d5a --- /dev/null +++ b/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +//! In this case, we test the attribute on a struct with a generic type `T` +//! which requires the bound `From` because of the comparisons in the +//! `#[safety_constraint(...)]` predicate. The struct represents an abstract +//! value for which we only track its sign. The actual value is kept private. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint((*positive && *conc_value >= 0.into()) || (!*positive && *conc_value < 0.into()))] +struct AbstractValue +where + T: PartialOrd + From, +{ + pub positive: bool, + conc_value: T, +} + +#[kani::proof] +fn check_abstract_value() { + let value: AbstractValue = kani::any(); + assert!(value.is_safe()); +} diff --git a/tests/expected/safety-constraint-attribute/abstract-value/expected b/tests/expected/safety-constraint-attribute/abstract-value/expected new file mode 100644 index 000000000000..2fc76378041d --- /dev/null +++ b/tests/expected/safety-constraint-attribute/abstract-value/expected @@ -0,0 +1,7 @@ +Check 1: check_abstract_value.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: value.is_safe()" + +VERIFICATION:- SUCCESSFUL + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs b/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs new file mode 100644 index 000000000000..6e2b3ab97812 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint(*x >= 0 && *y >= 0)] +struct Point { + x: i32, + y: i32, +} + +#[kani::proof] +fn check_arbitrary() { + let point: Point = kani::any(); + assert!(point.x >= 0); + assert!(point.y >= 0); + assert!(point.is_safe()); +} diff --git a/tests/expected/safety-constraint-attribute/check-arbitrary/expected b/tests/expected/safety-constraint-attribute/check-arbitrary/expected new file mode 100644 index 000000000000..ee1e13bb726d --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-arbitrary/expected @@ -0,0 +1,11 @@ +Check 1: check_arbitrary.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: point.x >= 0" + +Check 2: check_arbitrary.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: point.y >= 0" + +Check 3: check_arbitrary.assertion.3\ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" diff --git a/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs b/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs new file mode 100644 index 000000000000..fce7319779f0 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint(*x == *y)] +struct SameCoordsPoint { + x: i32, + y: i32, +} + +#[kani::proof] +fn check_invariant() { + let point: SameCoordsPoint = kani::any(); + assert!(point.is_safe()); + + // Assuming `point.x != point.y` here should be like assuming `false`. + // The assertion should be unreachable because we're blocking the path. + kani::assume(point.x != point.y); + assert!(false, "this assertion should be unreachable"); +} diff --git a/tests/expected/safety-constraint-attribute/check-invariant/expected b/tests/expected/safety-constraint-attribute/check-invariant/expected new file mode 100644 index 000000000000..a4605f03b7b4 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-invariant/expected @@ -0,0 +1,7 @@ +Check 1: check_invariant.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" + +Check 2: check_invariant.assertion.2\ + - Status: UNREACHABLE\ + - Description: ""this assertion should be unreachable"" diff --git a/tests/expected/safety-constraint-attribute/grade-example/expected b/tests/expected/safety-constraint-attribute/grade-example/expected new file mode 100644 index 000000000000..fd95a713d65a --- /dev/null +++ b/tests/expected/safety-constraint-attribute/grade-example/expected @@ -0,0 +1,11 @@ +Grade::check_percentage_safety.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: self.percentage <= 100" + +check_grade_safe.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: grade.is_safe()" + +VERIFICATION:- SUCCESSFUL + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs b/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs new file mode 100644 index 000000000000..7998ab27df49 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs @@ -0,0 +1,43 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +//! In this case, we test the attribute on a struct that represents a hybrid +//! grade (letter-numerical) which should keep the following equivalences: +//! - A for 90-100% +//! - B for 80-89% +//! - C for 70-79% +//! - D for 60-69% +//! - F for 0-59% +//! +//! In addition, we explicitly test that `percentage` is 0-100% + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint((*letter == 'A' && *percentage >= 90 && *percentage <= 100) || + (*letter == 'B' && *percentage >= 80 && *percentage < 90) || + (*letter == 'C' && *percentage >= 70 && *percentage < 80) || + (*letter == 'D' && *percentage >= 60 && *percentage < 70) || + (*letter == 'F' && *percentage < 60))] +struct Grade { + letter: char, + percentage: u32, +} + +impl Grade { + pub fn check_percentage_safety(&self) { + assert!(self.percentage <= 100); + } +} + +#[kani::proof] +fn check_grade_safe() { + let grade: Grade = kani::any(); + assert!(grade.is_safe()); + grade.check_percentage_safety(); +} diff --git a/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs b/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs new file mode 100644 index 000000000000..ef7be7fe0e03 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that there is a compilation error when the `#[safety_constraint(...)]` +//! attribute is used more than once on the same struct. + +extern crate kani; +use kani::Invariant; + +#[derive(Invariant)] +#[safety_constraint(*x >= 0)] +#[safety_constraint(*y >= 0)] +struct Point { + x: i32, + y: i32, +} diff --git a/tests/ui/safety-constraint-attribute/double-attribute/expected b/tests/ui/safety-constraint-attribute/double-attribute/expected new file mode 100644 index 000000000000..899b85e20e9a --- /dev/null +++ b/tests/ui/safety-constraint-attribute/double-attribute/expected @@ -0,0 +1,6 @@ +error: Cannot derive `Invariant` for `Point` + | +| #[derive(Invariant)] + | ^^^^^^^^^ + | +note: `#[safety_constraint(...)]` cannot be used more than once. diff --git a/tests/ui/safety-constraint-attribute/invalid-pred-error/expected b/tests/ui/safety-constraint-attribute/invalid-pred-error/expected new file mode 100644 index 000000000000..e15e3ff7cf7d --- /dev/null +++ b/tests/ui/safety-constraint-attribute/invalid-pred-error/expected @@ -0,0 +1,19 @@ +error[E0308]: mismatched types + | +| #[safety_constraint(x >= 0 && y >= 0)] + | ^ expected `&i32`, found integer + | +help: consider dereferencing the borrow + | +| #[safety_constraint(*x >= 0 && y >= 0)] + | + + +error[E0308]: mismatched types + | +| #[safety_constraint(x >= 0 && y >= 0)] + | ^ expected `&i32`, found integer + | +help: consider dereferencing the borrow + | +| #[safety_constraint(x >= 0 && *y >= 0)] + | diff --git a/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs b/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs new file mode 100644 index 000000000000..89c862bb50c3 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that there is a compilation error when the predicate passed to the +//! `#[safety_constraint(...)]` attribute would result in a compiler error. +//! +//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error, +//! otherwise the `#[safety_constraint(...)]` attribute is ignored. + +extern crate kani; + +// Note: The struct fields `x` and `y` are references in this context, we should +// refer to `*x` and `*y` instead. +#[derive(kani::Invariant)] +#[safety_constraint(x >= 0 && y >= 0)] +struct Point { + x: i32, + y: i32, +} diff --git a/tests/ui/safety-constraint-attribute/mixed-attributes/expected b/tests/ui/safety-constraint-attribute/mixed-attributes/expected new file mode 100644 index 000000000000..bca53d41bf13 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/mixed-attributes/expected @@ -0,0 +1,6 @@ +error: Cannot derive `Invariant` for `Point` + | +| #[derive(Invariant)] + | ^^^^^^^^^ + | +note: `#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously diff --git a/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs b/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs new file mode 100644 index 000000000000..931cebd4839d --- /dev/null +++ b/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that there is a compilation error when the `#[safety_constraint(...)]` +//! attribute for struct and the `#[safety_constraint(...)]` attribute for +//! fields is used at the same time. + +extern crate kani; +use kani::Invariant; + +#[derive(Invariant)] +#[safety_constraint(*x >= 0)] +struct Point { + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/expected b/tests/ui/safety-constraint-attribute/no-struct-error/expected new file mode 100644 index 000000000000..df6bd82f00d6 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/no-struct-error/expected @@ -0,0 +1,6 @@ +error: Cannot derive `Invariant` for `MyEnum` + | +| #[derive(kani::Invariant)] + | ^^^^^^^^^^^^^^^ + | +note: `#[safety_constraint(...)]` can only be used in structs diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs b/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs new file mode 100644 index 000000000000..092bbe1319c7 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani raises an error when a derive macro with the +//! `#[safety_constraint(...)]` attribute is is used in items which are not a +//! struct. +//! +//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error, +//! otherwise the `#[safety_constraint(...)]` attribute is ignored. + +extern crate kani; + +#[derive(kani::Invariant)] +#[safety_constraint(true)] +enum MyEnum { + A, + B(i32), +} From 43d87134746f6f1f0671eecf9cb3a1052c2a9dc4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 31 Jul 2024 18:32:10 +0200 Subject: [PATCH 07/11] Fix cbmc-nightly for macOS (#3400) With macOS, cmake needs a full path to the C++ compiler. (Documented in CBMC's COMPILING.md.) --- .github/workflows/cbmc-latest.yml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index f707c5d558a5..696f08fd44b8 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -38,7 +38,8 @@ jobs: repository: diffblue/cbmc path: cbmc - - name: Build CBMC + - name: Build CBMC (Linux) + if: ${{ startsWith(matrix.os, 'ubuntu') }} working-directory: ./cbmc run: | cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" @@ -46,6 +47,15 @@ jobs: # Prepend the bin directory to $PATH echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH + - name: Build CBMC (macOS) + if: ${{ startsWith(matrix.os, 'macos') }} + working-directory: ./cbmc + run: | + cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_COMPILER=$(which clang++) + cmake --build build -- -j 4 + # Prepend the bin directory to $PATH + echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH + - name: Execute Kani regressions working-directory: ./kani run: ./scripts/kani-regression.sh From 3bc4f0c76f8a64e62241daf61e81de18b66f0cd2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 31 Jul 2024 11:50:08 -0700 Subject: [PATCH 08/11] Enable concrete playback for contract and stubs (#3389) This PR enables concrete playback for contract and stubs. Since these two cases may not actually behave as users expect (it can even have an internal failure), I am adding documentation to the generated test calling that out. As I was testing this issue, I realized that concrete playback didn't quite work for arrays. So I introduced a new private function `any_raw_array`, which doesn't change the behavior during verification, but allow us to special case it in the concrete playback flow. Resolves #3383 --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-compiler/src/kani_middle/attributes.rs | 45 +++++----- .../src/kani_middle/codegen_units.rs | 2 +- kani-compiler/src/kani_middle/metadata.rs | 4 +- kani-driver/src/args/mod.rs | 13 +-- .../src/concrete_playback/test_generator.rs | 85 +++++++++++++++---- kani-driver/src/metadata.rs | 16 ++-- kani_metadata/src/harness.rs | 32 ++++++- library/kani/src/arbitrary.rs | 2 +- library/kani/src/concrete_playback.rs | 5 ++ library/kani/src/lib.rs | 16 ++-- library/kani_core/src/arbitrary.rs | 2 +- library/kani_core/src/lib.rs | 16 ++-- .../kani_macros/src/sysroot/contracts/mod.rs | 11 +-- .../playback_expected/config.yml | 4 + .../playback_expected/expected | 8 ++ .../playback_expected/playback.sh | 42 +++++++++ .../src/playback_contract.rs | 19 +++++ .../playback_expected/src/playback_stubs.rs | 34 ++++++++ .../verify_std_cmd/verify_std.sh | 2 +- 19 files changed, 279 insertions(+), 79 deletions(-) create mode 100644 tests/script-based-pre/playback_expected/config.yml create mode 100644 tests/script-based-pre/playback_expected/expected create mode 100755 tests/script-based-pre/playback_expected/playback.sh create mode 100644 tests/script-based-pre/playback_expected/src/playback_contract.rs create mode 100644 tests/script-based-pre/playback_expected/src/playback_stubs.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 9eb6d3d6ee4e..8c729bbdec9f 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -4,7 +4,7 @@ use std::collections::BTreeMap; -use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; +use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use rustc_ast::{ attr, token::Token, @@ -310,7 +310,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// the session and emit all errors found. pub(super) fn check_attributes(&self) { // Check that all attributes are correctly used and well formed. - let is_harness = self.is_harness(); + let is_harness = self.is_proof_harness(); for (&kind, attrs) in self.map.iter() { let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg); @@ -454,7 +454,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Is this item a harness? (either `proof` or `proof_for_contract` /// attribute are present) - fn is_harness(&self) -> bool { + fn is_proof_harness(&self) -> bool { self.map.contains_key(&KaniAttributeKind::Proof) || self.map.contains_key(&KaniAttributeKind::ProofForContract) } @@ -469,13 +469,18 @@ impl<'tcx> KaniAttributes<'tcx> { panic!("Expected a local item, but got: {:?}", self.item); }; trace!(?self, "extract_harness_attributes"); - assert!(self.is_harness()); - self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| { + assert!(self.is_proof_harness()); + let harness_attrs = if let Some(Ok(harness)) = self.proof_for_contract() { + HarnessAttributes::new(HarnessKind::ProofForContract { target_fn: harness.to_string() }) + } else { + HarnessAttributes::new(HarnessKind::Proof) + }; + self.map.iter().fold(harness_attrs, |mut harness, (kind, attributes)| { match kind { KaniAttributeKind::ShouldPanic => harness.should_panic = true, KaniAttributeKind::Recursion => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), "The attribute `kani::recursion` should only be used in combination with function contracts."); - }, + } KaniAttributeKind::Solver => { harness.solver = parse_solver(self.tcx, attributes[0]); } @@ -485,7 +490,7 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::Unwind => { harness.unwind_value = parse_unwind(self.tcx, attributes[0]) } - KaniAttributeKind::Proof => harness.proof = true, + KaniAttributeKind::Proof => { /* no-op */ } KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness), KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness), KaniAttributeKind::Unstable => { @@ -498,7 +503,7 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::InnerCheck | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); - }, + } KaniAttributeKind::DisableChecks => { // Internal attribute which shouldn't exist here. unreachable!() @@ -552,14 +557,14 @@ impl<'tcx> KaniAttributes<'tcx> { self.item_name(), ), ) - .with_span_note( - self.tcx.def_span(def_id), - format!( - "Try adding a contract to this function or use the unsound `{}` attribute instead.", - KaniAttributeKind::Stub.as_ref(), + .with_span_note( + self.tcx.def_span(def_id), + format!( + "Try adding a contract to this function or use the unsound `{}` attribute instead.", + KaniAttributeKind::Stub.as_ref(), + ), ) - ) - .emit(); + .emit(); continue; } Some(Ok(replacement_name)) => replacement_name, @@ -689,7 +694,7 @@ fn has_kani_attribute bool>( tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate) } -/// Same as [`KaniAttributes::is_harness`] but more efficient because less +/// Same as [`KaniAttributes::is_proof_harness`] but more efficient because less /// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool { let def_id = rustc_internal::internal(tcx, instance.def.def_id()); @@ -896,7 +901,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { tcx.dcx().span_err( error_span, - "attribute `kani::stub` takes two path arguments; found argument that is not a path", + "attribute `kani::stub` takes two path arguments; found argument that is not a path", ); None } @@ -910,9 +915,9 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { const ATTRIBUTE: &str = "#[kani::solver]"; let invalid_arg_err = |attr: &Attribute| { tcx.dcx().span_err( - attr.span, - format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)") - ) + attr.span, + format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)"), + ) }; let attr_args = attr.meta_item_list().unwrap(); diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 260b363a868a..b4ea06c8d5db 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -104,7 +104,7 @@ impl CodegenUnits { /// Generate [KaniMetadata] for the target crate. fn generate_metadata(&self) -> KaniMetadata { let (proof_harnesses, test_harnesses) = - self.harness_info.values().cloned().partition(|md| md.attributes.proof); + self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness()); KaniMetadata { crate_name: self.crate_info.name.clone(), proof_harnesses, diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index c00f38be4cb0..2f0f22d49e1c 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -6,7 +6,7 @@ use std::path::Path; use crate::kani_middle::attributes::test_harness_name; -use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata}; +use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::CrateDef; @@ -61,7 +61,7 @@ pub fn gen_test_metadata( original_file: loc.filename, original_start_line: loc.start_line, original_end_line: loc.end_line, - attributes: HarnessAttributes::default(), + attributes: HarnessAttributes::new(HarnessKind::Test), // TODO: This no longer needs to be an Option. goto_file: Some(model_file), contract: Default::default(), diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 158f1c001b5b..2d7593e8050a 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -559,13 +559,6 @@ impl ValidateArgs for VerificationArgs { --output-format=old.", )); } - if self.concrete_playback.is_some() && self.is_stubbing_enabled() { - // Concrete playback currently does not work with contracts or stubbing. - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Conflicting options: --concrete-playback isn't compatible with stubbing.", - )); - } if self.concrete_playback.is_some() && self.jobs() != Some(1) { // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called. return Err(Error::raw( @@ -869,13 +862,13 @@ mod tests { let res = parse_unstable_disabled("--harness foo -Z stubbing").unwrap(); assert!(res.verify_opts.is_stubbing_enabled()); - // `-Z stubbing` cannot be called with `--concrete-playback` + // `-Z stubbing` can now be called with concrete playback. let res = parse_unstable_disabled( "--harness foo --concrete-playback=print -Z concrete-playback -Z stubbing", ) .unwrap(); - let err = res.validate().unwrap_err(); - assert_eq!(err.kind(), ErrorKind::ArgumentConflict); + // Note that `res.validate()` fails because input file does not exist. + assert!(matches!(res.verify_opts.validate(), Ok(()))); } #[test] diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index dbd2fb9e03d2..5faa6299a5d3 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -6,10 +6,11 @@ use crate::args::ConcretePlaybackMode; use crate::call_cbmc::VerificationResult; +use crate::cbmc_output_parser::Property; use crate::session::KaniSession; use anyhow::{Context, Result}; use concrete_vals_extractor::{extract_harness_values, ConcreteVal}; -use kani_metadata::HarnessMetadata; +use kani_metadata::{HarnessKind, HarnessMetadata}; use std::collections::hash_map::DefaultHasher; use std::ffi::OsString; use std::fs::{read_to_string, File}; @@ -32,7 +33,7 @@ impl KaniSession { }; if let Ok(result_items) = &verification_result.results { - let harness_values: Vec> = extract_harness_values(result_items); + let harness_values = extract_harness_values(result_items); if harness_values.is_empty() { println!( @@ -43,9 +44,9 @@ impl KaniSession { } else { let mut unit_tests: Vec = harness_values .iter() - .map(|concrete_vals| { + .map(|(prop, concrete_vals)| { let pretty_name = harness.get_harness_name_unqualified(); - format_unit_test(&pretty_name, &concrete_vals) + format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness, prop)) }) .collect(); unit_tests.dedup_by(|a, b| a.name == b.name); @@ -168,6 +169,9 @@ impl KaniSession { writeln!(temp_file, "{line}")?; if curr_line_num == proof_harness_end_line { for unit_test in unit_tests.iter() { + // Write an empty line before the unit test. + writeln!(temp_file)?; + for unit_test_line in unit_test.code.iter() { curr_line_num += 1; writeln!(temp_file, "{unit_test_line}")?; @@ -176,7 +180,7 @@ impl KaniSession { } } - // Renames are usually automic, so we won't corrupt the user's source file during a + // Renames are usually atomic, so we won't corrupt the user's source file during a // crash; but first flush all updates to disk, which persist wouldn't take care of. temp_file.as_file().sync_all()?; temp_file.persist(source_path).expect("Could not rename file"); @@ -231,8 +235,52 @@ impl KaniSession { } } +fn gen_test_doc(harness: &HarnessMetadata, property: &Property) -> String { + let mut doc_str = match &harness.attributes.kind { + HarnessKind::Proof => { + format!("/// Test generated for harness `{}` \n", harness.pretty_name) + } + HarnessKind::ProofForContract { target_fn } => { + format!( + "/// Test generated for harness `{}` that checks contract for `{target_fn}`\n", + harness.pretty_name + ) + } + HarnessKind::Test => { + unreachable!("Concrete playback for tests is not supported") + } + }; + doc_str.push_str("///\n"); + doc_str.push_str(&format!( + "/// Check for `{}`: \"{}\"\n", + property.property_class(), + property.description + )); + if !harness.attributes.stubs.is_empty() { + doc_str.push_str( + r#"/// +/// # Warning +/// +/// Concrete playback tests combined with stubs or contracts is highly +/// experimental, and subject to change. +/// +/// The original harness has stubs which are not applied to this test. +/// This may cause a mismatch of non-deterministic values if the stub +/// creates any non-deterministic value. +/// The execution path may also differ, which can be used to refine the stub +/// logic. +"#, + ); + } + doc_str +} + /// Generate a formatted unit test from a list of concrete values. -fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTest { +fn format_unit_test( + harness_name: &str, + concrete_vals: &[ConcreteVal], + doc_str: String, +) -> UnitTest { // Hash the concrete values along with the proof harness name. let mut hasher = DefaultHasher::new(); harness_name.hash(&mut hasher); @@ -241,6 +289,7 @@ fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTe let func_name = format!("kani_concrete_playback_{harness_name}_{hash}"); let func_before_concrete_vals = [ + doc_str, "#[test]".to_string(), format!("fn {func_name}() {{"), format!("{:<4}let concrete_vals: Vec> = vec![", " "), @@ -324,7 +373,7 @@ mod concrete_vals_extractor { /// Extract a set of concrete values that trigger one assertion /// failure. Each element of the outer vector corresponds to /// inputs triggering one assertion failure or cover statement. - pub fn extract_harness_values(result_items: &[Property]) -> Vec> { + pub fn extract_harness_values(result_items: &[Property]) -> Vec<(&Property, Vec)> { result_items .iter() .filter(|prop| { @@ -340,7 +389,7 @@ mod concrete_vals_extractor { let concrete_vals: Vec = trace.iter().filter_map(&extract_from_trace_item).collect(); - concrete_vals + (property, concrete_vals) }) .collect() } @@ -359,7 +408,7 @@ mod concrete_vals_extractor { { if trace_item.step_type == "assignment" && lhs.starts_with("goto_symex$$return_value") - && func.starts_with("kani::any_raw_internal") + && func.starts_with("kani::any_raw_") { let declared_width = width_u64 as usize; let actual_width = bit_concrete_val.len(); @@ -484,9 +533,10 @@ mod tests { /// Since hashes can not be relied on in tests, this compares all parts of a unit test except the hash. #[test] fn format_unit_test_full_func() { + let doc_str = "/// Test documentation"; let harness_name = "test_proof_harness"; let concrete_vals = [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }]; - let unit_test = format_unit_test(harness_name, &concrete_vals); + let unit_test = format_unit_test(harness_name, &concrete_vals, doc_str.to_string()); let full_func = unit_test.code; let split_unit_test_name = split_unit_test_name(&unit_test.name); let expected_after_func_name = vec![ @@ -498,18 +548,23 @@ mod tests { "}".to_string(), ]; - assert_eq!(full_func[0], "#[test]"); + assert_eq!(full_func[0], doc_str); + assert_eq!(full_func[1], "#[test]"); assert_eq!( split_unit_test_name.before_hash, format!("kani_concrete_playback_{harness_name}") ); - assert_eq!(full_func[1], format!("fn {}() {{", unit_test.name)); - assert_eq!(full_func[2..], expected_after_func_name); + assert_eq!(full_func[2], format!("fn {}() {{", unit_test.name)); + assert_eq!(full_func[3..], expected_after_func_name); } /// Generates a unit test and returns its hash. fn extract_hash_from_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> String { - let unit_test = format_unit_test(harness_name, concrete_vals); + let unit_test = format_unit_test( + harness_name, + concrete_vals, + "/// Harness created for unit test".to_string(), + ); split_unit_test_name(&unit_test.name).hash } @@ -603,7 +658,7 @@ mod tests { }), }]), }]; - let concrete_vals = extract_harness_values(&processed_items).pop().unwrap(); + let (_, concrete_vals) = extract_harness_values(&processed_items).pop().unwrap(); let concrete_val = &concrete_vals[0]; assert_eq!(concrete_val.byte_arr, vec![1, 3]); diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index cd916358d92e..3f9cd8f2bf84 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -200,7 +200,7 @@ fn find_proof_harnesses<'a>( #[cfg(test)] pub mod tests { use super::*; - use kani_metadata::HarnessAttributes; + use kani_metadata::{HarnessAttributes, HarnessKind}; use std::path::PathBuf; pub fn mock_proof_harness( @@ -209,6 +209,8 @@ pub mod tests { krate: Option<&str>, model_file: Option, ) -> HarnessMetadata { + let mut attributes = HarnessAttributes::new(HarnessKind::Proof); + attributes.unwind_value = unwind_value; HarnessMetadata { pretty_name: name.into(), mangled_name: name.into(), @@ -216,7 +218,7 @@ pub mod tests { original_file: "".into(), original_start_line: 0, original_end_line: 0, - attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, + attributes, goto_file: model_file, contract: Default::default(), } @@ -236,7 +238,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_three".to_string()]), &ref_harnesses, - false + false, ) .len(), 1 @@ -245,7 +247,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_two".to_string()]), &ref_harnesses, - false + false, ) .first() .unwrap() @@ -256,7 +258,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_one".to_string()]), &ref_harnesses, - false + false, ) .first() .unwrap() @@ -280,7 +282,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_three".to_string()]), &ref_harnesses, - true + true, ) .is_empty() ); @@ -299,7 +301,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"module::not_check_three".to_string()]), &ref_harnesses, - true + true, ) .first() .unwrap() diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 3dd6c82ebd39..41eb4eb20919 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -38,10 +38,10 @@ pub struct HarnessMetadata { } /// The attributes added by the user to control how a harness is executed. -#[derive(Debug, Clone, Serialize, Deserialize, Default, PartialEq)] +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct HarnessAttributes { /// Whether the harness has been annotated with proof. - pub proof: bool, + pub kind: HarnessKind, /// Whether the harness is expected to panic or not. pub should_panic: bool, /// Optional data to store solver. @@ -52,6 +52,34 @@ pub struct HarnessAttributes { pub stubs: Vec, } +#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)] +pub enum HarnessKind { + /// Function was annotated with `#[kani::proof]`. + Proof, + /// Function was annotated with `#[kani::proof_for_contract(target_fn)]`. + ProofForContract { target_fn: String }, + /// This is a test harness annotated with `#[test]`. + Test, +} + +impl HarnessAttributes { + /// Create a new harness of the provided kind. + pub fn new(kind: HarnessKind) -> HarnessAttributes { + HarnessAttributes { + kind, + should_panic: false, + solver: None, + unwind_value: None, + stubs: vec![], + } + } + + /// Return whether this is a proof harness. + pub fn is_proof_harness(&self) -> bool { + matches!(self.kind, HarnessKind::Proof | HarnessKind::ProofForContract { .. }) + } +} + /// The stubbing type. #[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct Stub { diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index ef6e2ef23dd4..83b113d64927 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -31,7 +31,7 @@ macro_rules! trivial_arbitrary { unsafe { crate::any_raw_internal::() } } fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } + unsafe { crate::any_raw_array::() } } } }; diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs index aa6cd7e4018d..0de51862b7d8 100644 --- a/library/kani/src/concrete_playback.rs +++ b/library/kani/src/concrete_playback.rs @@ -40,6 +40,11 @@ pub fn concrete_playback_run(mut local_concrete_vals: Vec>, pro }); } +/// Iterate over `any_raw_internal` since CBMC produces assignment per element. +pub(crate) unsafe fn any_raw_array() -> [T; N] { + [(); N].map(|_| crate::any_raw_internal::()) +} + /// Concrete playback implementation of /// kani::any_raw_internal. Because CBMC does not bother putting in /// Zero-Sized Types, those are defaulted to an empty vector. diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 3cf46bd7af07..046c6e7a0667 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -249,21 +249,25 @@ pub fn any_where bool>(f: F) -> T { /// Note that SIZE_T must be equal the size of type T in bytes. #[inline(never)] #[cfg(not(feature = "concrete_playback"))] -pub(crate) unsafe fn any_raw_internal() -> T { - any_raw_inner::() +unsafe fn any_raw_internal() -> T { + any_raw::() } +/// This is the same as [any_raw_internal] for verification flow, but not for concrete playback. #[inline(never)] -#[cfg(feature = "concrete_playback")] -pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() +#[cfg(not(feature = "concrete_playback"))] +unsafe fn any_raw_array() -> [T; N] { + any_raw::<[T; N]>() } +#[cfg(feature = "concrete_playback")] +use concrete_playback::{any_raw_array, any_raw_internal}; + /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] #[inline(never)] #[allow(dead_code)] -fn any_raw_inner() -> T { +fn any_raw() -> T { kani_intrinsic() } diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 7cfb649b11a0..8c6cfd335104 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -34,7 +34,7 @@ macro_rules! generate_arbitrary { unsafe { crate::kani::any_raw_internal::() } } fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } + unsafe { crate::kani::any_raw_array::() } } } }; diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 016c805e8f8e..9baba1abe886 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -248,21 +248,25 @@ macro_rules! kani_intrinsics { /// Note that SIZE_T must be equal the size of type T in bytes. #[inline(never)] #[cfg(not(feature = "concrete_playback"))] - pub(crate) unsafe fn any_raw_internal() -> T { - any_raw_inner::() + unsafe fn any_raw_internal() -> T { + any_raw::() } + /// This is the same as [any_raw_internal] for verification flow, but not for concrete playback. #[inline(never)] - #[cfg(feature = "concrete_playback")] - pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() + #[cfg(not(feature = "concrete_playback"))] + unsafe fn any_raw_array() -> [T; N] { + any_raw::<[T; N]>() } + #[cfg(feature = "concrete_playback")] + use concrete_playback::{any_raw_array, any_raw_internal}; + /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] #[inline(never)] #[allow(dead_code)] - pub fn any_raw_inner() -> T { + fn any_raw() -> T { kani_intrinsic() } diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index defcd9dae1b4..12a1215de2c7 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -336,7 +336,7 @@ use proc_macro::TokenStream; use proc_macro2::{Ident, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; -use syn::{parse_macro_input, Expr, ExprClosure, ItemFn}; +use syn::{parse_macro_input, parse_quote, Expr, ExprClosure, ItemFn}; mod bootstrap; mod check; @@ -387,15 +387,12 @@ passthrough!(stub_verified, false); pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { let args = proc_macro2::TokenStream::from(attr); - let ItemFn { attrs, vis, sig, block } = parse_macro_input!(item as ItemFn); + let mut fn_item = parse_macro_input!(item as ItemFn); + fn_item.block.stmts.insert(0, parse_quote!(kani::internal::init_contracts();)); quote!( #[allow(dead_code)] #[kanitool::proof_for_contract = stringify!(#args)] - #(#attrs)* - #vis #sig { - kani::internal::init_contracts(); - #block - } + #fn_item ) .into() } diff --git a/tests/script-based-pre/playback_expected/config.yml b/tests/script-based-pre/playback_expected/config.yml new file mode 100644 index 000000000000..d15b5d277ed6 --- /dev/null +++ b/tests/script-based-pre/playback_expected/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback.sh +expected: expected diff --git a/tests/script-based-pre/playback_expected/expected b/tests/script-based-pre/playback_expected/expected new file mode 100644 index 000000000000..bedb39581b7f --- /dev/null +++ b/tests/script-based-pre/playback_expected/expected @@ -0,0 +1,8 @@ +[TEST] Generate test for playback_contract.rs... +Verification failed for - check_modify_slice +Result for playback_contract.rs: test result: FAILED. 1 passed; 1 failed + +[TEST] Generate test for playback_stubs.rs... +Verification failed for - check_lt_0 +Verification failed for - check_bad_stub +Result for playback_stubs.rs: test result: FAILED. 1 passed; 1 failed diff --git a/tests/script-based-pre/playback_expected/playback.sh b/tests/script-based-pre/playback_expected/playback.sh new file mode 100755 index 000000000000..3b358db257a2 --- /dev/null +++ b/tests/script-based-pre/playback_expected/playback.sh @@ -0,0 +1,42 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# This will run Kani verification in every `src/*.rs` file followed by playback command. +# Expected output is generated from individual expected files. +set -o nounset + +run() { + local input_rs=${1:?"Missing input file"} + + echo "[TEST] Generate test for ${input_rs}..." + kani "${input_rs}" \ + -Z concrete-playback --concrete-playback=inplace \ + -Z function-contracts -Z stubbing --output-format terse + + # Note that today one of the tests will succeed since the contract pre-conditions are not inserted by Kani. + # Hopefully this will change with https://github.com/model-checking/kani/issues/3326 + echo "[TEST] Run test for ${input_rs}..." + summary=$(kani playback -Z concrete-playback "${input_rs}" -- kani_concrete_playback | grep "test result") + echo "Result for ${input_rs}: ${summary}" +} + +ROOT_DIR=$(git rev-parse --show-toplevel) +MODIFIED_DIR=modified +rm -rf "${MODIFIED_DIR}" +mkdir "${MODIFIED_DIR}" + +for rs in src/*.rs; do + if [[ -e "${rs}" ]]; then + echo "Running ${rs}" + cp "${rs}" "${MODIFIED_DIR}" + pushd "${MODIFIED_DIR}" > /dev/null + run "$(basename "${rs}")" + popd > /dev/null + else + echo "No .rs files found in src directory" + exit 1 + fi +done + + # Cleanup +rm -rf "${MODIFIED_DIR}" \ No newline at end of file diff --git a/tests/script-based-pre/playback_expected/src/playback_contract.rs b/tests/script-based-pre/playback_expected/src/playback_contract.rs new file mode 100644 index 000000000000..8271e9a3d03f --- /dev/null +++ b/tests/script-based-pre/playback_expected/src/playback_contract.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani correctly adds tests to when the harness is a proof for contract. +extern crate kani; + +#[kani::requires(idx < slice.len())] +#[kani::modifies(slice)] +#[kani::ensures(| _ | slice[idx] == new_val)] +fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) { + // Inject bug by incrementing index first. + let new_idx = idx + 1; + *slice.get_mut(new_idx).expect("Expected valid index, but contract is wrong") = new_val; +} + +#[kani::proof_for_contract(modify_slice)] +fn check_modify_slice() { + let mut data: [u32; 4] = kani::any(); + modify_slice(&mut data, kani::any(), kani::any()) +} diff --git a/tests/script-based-pre/playback_expected/src/playback_stubs.rs b/tests/script-based-pre/playback_expected/src/playback_stubs.rs new file mode 100644 index 000000000000..ce5107949f04 --- /dev/null +++ b/tests/script-based-pre/playback_expected/src/playback_stubs.rs @@ -0,0 +1,34 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani playback works with stubs. +#![allow(dead_code)] + +fn is_zero(val: u8) -> bool { + val == 0 +} + +fn not_zero(val: u8) -> bool { + val != 0 +} + +/// Add a harness that will fail due to incorrect stub but the test will succeed. +#[kani::proof] +#[kani::stub(is_zero, not_zero)] +fn check_bad_stub() { + assert!(is_zero(kani::any())) +} + +fn lt_zero(val: i8) -> bool { + val < 0 +} + +fn lt_ten(val: i8) -> bool { + val < 10 +} + +/// Add a harness that will fail in an equivalent way. +#[kani::proof] +#[kani::stub(lt_zero, lt_ten)] +fn check_lt_0() { + assert!(lt_zero(kani::any())) +} diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 91454c4b65e7..3a24bf15241e 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -29,7 +29,7 @@ mod verify { use core::kani; #[kani::proof] fn check_non_zero() { - let orig: u32 = kani::any_raw_inner(); + let orig: u32 = kani::any(); if let Some(val) = core::num::NonZeroU32::new(orig) { assert!(orig == val.into()); } else { From 695e6f76832bafd379a9fea2e6434032cebb6166 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 31 Jul 2024 16:15:45 -0400 Subject: [PATCH 09/11] Tutorial Sections 2.1 and 2.2 Updates (#3387) Update the tutorial, namely: - Update the [bounds checking and pointers example](https://model-checking.github.io/kani/tutorial-kinds-of-failure.html#bounds-checking-and-pointers). `cargo test` catches the UB in the current example, so this PR modifies the code slightly so that `cargo test` still misses the UB, as desired. - Rather than including larger sections on experimental features throughout the tutorial, create a separate experimental features section and include (briefer) references to them in the tutorial. - The old text recommended debugging by generating a trace with `--visualize`, with a briefer mention of `--concrete-playback`. Since `--visualize` is deprecated, revise the debugging exercises to recommend `--concrete-playback` instead. 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: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- docs/src/SUMMARY.md | 7 +- docs/src/reference/attributes.md | 2 +- .../experimental/concrete-playback.md} | 19 ++--- docs/src/reference/experimental/coverage.md | 32 ++++++++ .../experimental/experimental-features.md | 5 ++ .../reference/{ => experimental}/stubbing.md | 2 +- docs/src/tutorial-first-steps.md | 60 ++------------- docs/src/tutorial-kinds-of-failure.md | 74 ++++++------------- docs/src/tutorial-real-code.md | 2 +- .../kinds-of-failure/src/bounds_check.rs | 2 +- docs/src/usage.md | 2 +- docs/src/verification-results.md | 2 +- 12 files changed, 81 insertions(+), 128 deletions(-) rename docs/src/{debugging-verification-failures.md => reference/experimental/concrete-playback.md} (87%) create mode 100644 docs/src/reference/experimental/coverage.md create mode 100644 docs/src/reference/experimental/experimental-features.md rename docs/src/reference/{ => experimental}/stubbing.md (99%) diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index ff7914c1a07a..784ec075d183 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -12,12 +12,13 @@ - [Failures that Kani can spot](./tutorial-kinds-of-failure.md) - [Loop unwinding](./tutorial-loop-unwinding.md) - [Nondeterministic variables](./tutorial-nondeterministic-variables.md) - - [Debugging verification failures](./debugging-verification-failures.md) - [Reference](./reference.md) - [Attributes](./reference/attributes.md) - - [Stubbing](./reference/stubbing.md) - + - [Experimental features](./reference/experimental/experimental-features.md) + - [Coverage](./reference/experimental/coverage.md) + - [Stubbing](./reference/experimental/stubbing.md) + - [Concrete Playback](./reference/experimental/concrete-playback.md) - [Application](./application.md) - [Comparison with other tools](./tool-comparison.md) - [Where to start on real code](./tutorial-real-code.md) diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md index bd8b80cbbdaa..4556077911fc 100644 --- a/docs/src/reference/attributes.md +++ b/docs/src/reference/attributes.md @@ -60,7 +60,7 @@ For example, the class in `Check 1: my_harness.assertion.1` is `assertion`, so t > **NOTE**: The `#[kani::should_panic]` is only recommended for writing > harnesses which complement existing harnesses that don't use the same -> attribute. In order words, it's only recommended to write *negative harnesses* +> attribute. In other words, it's only recommended to write *negative harnesses* > after having written *positive* harnesses that successfully verify interesting > properties about the function under verification. diff --git a/docs/src/debugging-verification-failures.md b/docs/src/reference/experimental/concrete-playback.md similarity index 87% rename from docs/src/debugging-verification-failures.md rename to docs/src/reference/experimental/concrete-playback.md index c5dae6e74308..237f5673caf0 100644 --- a/docs/src/debugging-verification-failures.md +++ b/docs/src/reference/experimental/concrete-playback.md @@ -1,20 +1,13 @@ -# Debugging verification failures +# Concrete Playback -When the result of a certain check comes back as a `FAILURE`, -Kani offers different options to help debug: -* `--concrete-playback`. This _experimental_ feature generates a Rust unit test case that plays back a failing -proof harness using a concrete counterexample. -* `--visualize`. This feature generates an HTML text-based trace that -enumerates the execution steps leading to the check failure. - -## Concrete playback +When the result of a certain check comes back as a `FAILURE`, Kani offers the `concrete-playback` option to help debug. This feature generates a Rust unit test case that plays back a failing proof harness using a concrete counterexample. When concrete playback is enabled, Kani will generate unit tests for assertions that failed during verification, as well as cover statements that are reachable. These tests can then be executed using Kani's playback subcommand. -### Usage +## Usage In order to enable this feature, run Kani with the `-Z concrete-playback --concrete-playback=[print|inplace]` flag. After getting a verification failure, Kani will generate a Rust unit test case that plays back a failing @@ -46,7 +39,7 @@ The output will have a line in the beginning like You can further debug the binary with tools like `rust-gdb` or `lldb`. -### Example +## Example Running `kani -Z concrete-playback --concrete-playback=print` on the following source file: ```rust @@ -75,7 +68,7 @@ Here, `133` and `35207` are the concrete values that, when substituted for `a` a cause an assertion failure. `vec![135, 137]` is the byte array representation of `35207`. -### Request for comments +## Request for comments This feature is experimental and is therefore subject to change. If you have ideas for improving the user experience of this feature, @@ -83,7 +76,7 @@ please add them to [this GitHub issue](https://github.com/model-checking/kani/is We are tracking the existing feature requests in [this GitHub milestone](https://github.com/model-checking/kani/milestone/10). -### Limitations +## Limitations * This feature does not generate unit tests for failing non-panic checks (e.g., UB checks). This is because checks would not trigger runtime errors during concrete playback. diff --git a/docs/src/reference/experimental/coverage.md b/docs/src/reference/experimental/coverage.md new file mode 100644 index 000000000000..fb73d5f7c05b --- /dev/null +++ b/docs/src/reference/experimental/coverage.md @@ -0,0 +1,32 @@ +## Coverage + +Recall our `estimate_size` example from [First steps](../../tutorial-first-steps.md), +where we wrote a proof harness constraining the range of inputs to integers less than 4096: + +```rust +{{#include ../../tutorial/first-steps-v2/src/lib.rs:kani}} +``` + +We must wonder if we've really fully tested our function. +What if we revise the function, but forget to update the assumption in our proof harness to cover the new range of inputs? + +Fortunately, Kani is able to report a coverage metric for each proof harness. +In the `first-steps-v2` directory, try running: + +``` +cargo kani --coverage -Z line-coverage --harness verify_success +``` + +which verifies the harness, then prints coverage information for each line. +In this case, we see that each line of `estimate_size` is followed by `FULL`, indicating that our proof harness provides full coverage. + +Try changing the assumption in the proof harness to `x < 2048`. +Now the harness won't be testing all possible cases. +Rerun the command. +You'll see this line: + +``` +src/lib.rs, 24, NONE +``` + +which indicates that the proof no longer covers line 24, which addresses the case where `x >= 2048`. diff --git a/docs/src/reference/experimental/experimental-features.md b/docs/src/reference/experimental/experimental-features.md new file mode 100644 index 000000000000..bd9fb6cd8572 --- /dev/null +++ b/docs/src/reference/experimental/experimental-features.md @@ -0,0 +1,5 @@ +# Experimental Features + +We elaborate on some of the more commonly used experimental features in Kani. +This is not an exhaustive list; to see all of Kani's experimental features, run `cargo kani --help`. +To use an experimental feature, invoke Kani with the `--unstable` or `-Z` flag followed by the name of the feature. \ No newline at end of file diff --git a/docs/src/reference/stubbing.md b/docs/src/reference/experimental/stubbing.md similarity index 99% rename from docs/src/reference/stubbing.md rename to docs/src/reference/experimental/stubbing.md index b4eeb4fe6b98..0ffbba5f0b0b 100644 --- a/docs/src/reference/stubbing.md +++ b/docs/src/reference/experimental/stubbing.md @@ -113,7 +113,7 @@ In the following, we describe all the limitations of the stubbing feature. The usage of stubbing is limited to the verification of a single harness. Therefore, users are **required to pass the `--harness` option** when using the stubbing feature. -In addition, this feature **isn't compatible with [concrete playback](../debugging-verification-failures.md#concrete-playback)**. +In addition, this feature **isn't compatible with [concrete playback](./concrete-playback.md)**. ### Support diff --git a/docs/src/tutorial-first-steps.md b/docs/src/tutorial-first-steps.md index 57e70edb96dd..bbfd236c6b58 100644 --- a/docs/src/tutorial-first-steps.md +++ b/docs/src/tutorial-first-steps.md @@ -53,40 +53,11 @@ Kani has immediately found a failure. Notably, we haven't had to write explicit assertions in our proof harness: by default, Kani will find a host of erroneous conditions which include a reachable call to `panic` or a failing `assert`. If Kani had run successfully on this harness, this amounts to a mathematical proof that there is no input that could cause a panic in `estimate_size`. -### Getting a trace +> By default, Kani only reports failures, not how the failure happened. +> In this example, it would be nice to get a concrete example of a value of `x` that triggers the failure. +> Kani offers an (experimental) [concrete playback](reference/experimental/concrete-playback.md) feature that serves this purpose. +> As an exercise, try applying concrete playback to this example and see what Kani outputs. -By default, Kani only reports failures, not how the failure happened. -In this running example, it seems obvious what we're interested in (the value of `x` that caused the failure) because we just have one unknown input at the start (similar to the property test), but that's kind of a special case. -In general, understanding how a failure happened requires exploring a full (potentially large) _execution trace_. - -An execution trace is a record of exactly how a failure can occur. -Nondeterminism (like a call to `kani::any()`, which could return any value) can appear in the middle of its execution. -A trace is a record of exactly how execution proceeded, including concrete choices (like `1023`) for all of these nondeterministic values. - -To get a trace for a failing check in Kani, run: - -``` -cargo kani --visualize --enable-unstable -``` - -This command runs Kani and generates an HTML report that includes a trace. -Open the report with your preferred browser. -Under the "Errors" heading, click on the "trace" link to find the trace for this failure. - -From this trace report, we can filter through it to find relevant lines. -A good rule of thumb is to search for either `kani::any()` or assignments to variables you're interested in. -At present time, an unfortunate amount of generated code is present in the trace. -This code isn't a part of the Rust code you wrote, but is an internal implementation detail of how Kani runs proof harnesses. -Still, searching for `kani::any()` quickly finds us these lines: - -``` -let x: u32 = kani::any(); -x = 1023u -``` - -Here we're seeing the line of code and the value assigned in this particular trace. -Like property testing, this is just one **example** of a failure. -To proceed, we recommend fixing the code to avoid this particular issue and then re-running Kani to see if you find more issues. ### Exercise: Try other failures @@ -193,25 +164,6 @@ Here's a revised example of the proof harness, one that now succeeds: {{#include tutorial/first-steps-v2/src/lib.rs:kani}} ``` -But now we must wonder if we've really fully tested our function. -What if we revise the function, but forget to update the assumption in our proof harness to cover the new range of inputs? - -Fortunately, Kani is able to report a coverage metric for each proof harness. -Try running: - -``` -cargo kani --visualize --harness verify_success -``` - -The beginning of the report includes coverage information. -Clicking through to the file will show fully-covered lines in green. -Lines not covered by our proof harness will show in red. - -Try changing the assumption in the proof harness to `x < 2048`. -Now the harness won't be testing all possible cases. -Rerun `cargo kani --visualize`. -Look at the report: you'll see we no longer have 100% coverage of the function. - ## Summary In this section: @@ -219,6 +171,4 @@ In this section: 1. We saw Kani find panics, assertion failures, and even some other failures like unsafe dereferencing of null pointers. 2. We saw Kani find failures that testing could not easily find. 3. We saw how to write a proof harness and use `kani::any()`. -4. We saw how to get a failing **trace** using `kani --visualize` -5. We saw how proof harnesses are used to set up preconditions with `kani::assume()`. -6. We saw how to obtain **coverage** metrics and use them to ensure our proofs are covering as much as they should be. +4. We saw how proof harnesses are used to set up preconditions with `kani::assume()`. diff --git a/docs/src/tutorial-kinds-of-failure.md b/docs/src/tutorial-kinds-of-failure.md index 29236b95db0c..00f9408ca709 100644 --- a/docs/src/tutorial-kinds-of-failure.md +++ b/docs/src/tutorial-kinds-of-failure.md @@ -25,7 +25,7 @@ This property test will immediately find a failing case, thanks to Rust's built- But what if we change this function to use unsafe Rust? ```rust -return unsafe { *a.get_unchecked(i % a.len() + 1) }; +return unsafe { *a.as_ptr().add(i % a.len() + 1) }; ``` Now the error becomes invisible to this test: @@ -55,7 +55,7 @@ cargo kani --harness bound_check We still see a failure from Kani, even without Rust's runtime bounds checking. > Also, notice there were many checks in the verification output. -> (At time of writing, 351.) +> (At time of writing, 345.) > This is a result of using the standard library `Vec` implementation, which means our harness actually used quite a bit of code, short as it looks. > Kani is inserting a lot more checks than appear as asserts in our code, so the output can be large. @@ -63,7 +63,7 @@ We get the following summary at the end: ``` SUMMARY: - ** 1 of 351 failed + ** 1 of 345 failed (8 unreachable) Failed Checks: dereference failure: pointer outside object bounds File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped @@ -79,71 +79,44 @@ Consider trying a few more small exercises with this example: 1. Exercise: Switch back to the normal/safe indexing operation and re-try Kani. How does Kani's output change, compared to the unsafe operation? (Try predicting the answer, then seeing if you got it right.) -2. Exercise: [Remember how to get a trace from Kani?](./tutorial-first-steps.md#getting-a-trace) Find out what inputs it failed on. +2. Exercise: Try Kani's experimental [concrete playback](reference/experimental/concrete-playback.md) feature on this example. 3. Exercise: Fix the error, run Kani, and see a successful verification. 4. Exercise: Try switching back to the unsafe code (now with the error fixed) and re-run Kani. Does it still verify successfully?
Click to see explanation for exercise 1 -Having switched back to the safe indexing operation, Kani reports two failures: +Having switched back to the safe indexing operation, Kani reports a bounds check failure: ``` -SUMMARY: - ** 2 of 350 failed +SUMMARY: + ** 1 of 343 failed (8 unreachable) Failed Checks: index out of bounds: the length is less than or equal to the given index - File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped -Failed Checks: dereference failure: pointer outside object bounds - File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped + File: "src/bounds_check.rs", line 11, in bounds_check::get_wrapped VERIFICATION:- FAILED ``` -The first is Rust's runtime bounds checking for the safe indexing operation. -The second is Kani's check to ensure the pointer operation is actually safe. -This pattern (two checks for similar issues in safe Rust code) is common to see, and we'll see it again in the next section. - -> **NOTE**: While Kani will always be checking for both properties, [in the future the output here may change](https://github.com/model-checking/kani/issues/1349). -> You might have noticed that the bad pointer dereference can't happen, since the bounds check would panic first. -> In the future, Kani's output may report only the bounds checking failure in this example. -
Click to see explanation for exercise 2 -Having run `cargo kani --harness bound_check --visualize` and clicked on one of the failures to see a trace, there are three things to immediately notice: - -1. This trace is huge. Because the standard library `Vec` is involved, there's a lot going on. -2. The top of the trace file contains some "trace navigation tips" that might be helpful in navigating the trace. -3. There's a lot of generated code and it's really hard to just read the trace itself. - -To navigate this trace to find the information you need, we again recommend searching for things you expect to be somewhere in the trace: - -1. Search the page for `kani::any` or ` =` such as `size =` or `let size`. -We can use this to find out what example values lead to a problem. -In this case, where we just have a couple of `kani::any` values in our proof harness, we can learn a lot just by seeing what these are. -In this trace we find (and the values you get may be different): - -``` -Step 36: Function bound_check, File src/bounds_check.rs, Line 37 -let size: usize = kani::any(); -size = 2464ul - -Step 39: Function bound_check, File src/bounds_check.rs, Line 39 -let index: usize = kani::any(); -index = 2463ul +`cargo kani -Z concrete-playback --concrete-playback=inplace --harness bound_check` produces the following test: +``` +rust +#[test] +fn kani_concrete_playback_bound_check_4752536404478138800() { + let concrete_vals: Vec> = vec![ + // 1ul + vec![1, 0, 0, 0, 0, 0, 0, 0], + // 18446744073709551615ul + vec![255, 255, 255, 255, 255, 255, 255, 255], + ]; + kani::concrete_playback_run(concrete_vals, bound_check); +} ``` - -You may see different values here, as it depends on the solver's behavior. - -2. Try searching for `failure:`. This will be near the end of the page. -You can now search upwards from a failure to see what values certain variables had. -Sometimes it can be helpful to change the source code to add intermediate variables, so their value is visible in the trace. -For instance, you might want to compute the index before indexing into the array. -That way you'd see in the trace exactly what value is being used. - -These two techniques should help you find both the nondeterministic inputs, and the values that were involved in the failing assertion. +which indicates that substituting the concrete values `size = 1` and `index = 2^64` in our proof harness will produce the out of bounds access.
@@ -247,6 +220,5 @@ In this section: 1. We saw Kani spot out-of-bounds accesses. 2. We saw Kani spot actually-unsafe dereferencing of a raw pointer to invalid memory. -3. We got more experience reading the traces that Kani generates, to debug a failing proof harness. 3. We saw Kani spot a division by zero error and an overflowing addition. -5. As an exercise, we tried proving an assertion (finding the midpoint) that was not completely trivial. +4. As an exercise, we tried proving an assertion (finding the midpoint) that was not completely trivial. diff --git a/docs/src/tutorial-real-code.md b/docs/src/tutorial-real-code.md index c4bad5a2d82e..3dd216cd6258 100644 --- a/docs/src/tutorial-real-code.md +++ b/docs/src/tutorial-real-code.md @@ -74,7 +74,7 @@ A first proof will likely start in the following form: Running Kani on this simple starting point will help figure out: 1. What unexpected constraints might be needed on your inputs (using `kani::assume`) to avoid "expected" failures. -2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs). +2. Whether you're over-constrained. Check the coverage report using `--coverage -Z line-coverage`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs). 3. Whether Kani will support all the Rust features involved. 4. Whether you've started with a tractable problem. (Remember to try setting `#[kani::unwind(1)]` to force early termination and work up from there.) diff --git a/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs b/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs index 9204d8f0f17e..c4a30982c95d 100644 --- a/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs +++ b/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs @@ -13,7 +13,7 @@ fn get_wrapped(i: usize, a: &[u32]) -> u32 { // ANCHOR_END: code // Alternative unsafe return for the above function: -// return unsafe { *a.get_unchecked(i % a.len() + 1) }; +// return unsafe { *a.as_ptr().add(i % a.len() + 1) }; #[cfg(test)] mod tests { diff --git a/docs/src/usage.md b/docs/src/usage.md index 459916c87222..aaa5d3fa234c 100644 --- a/docs/src/usage.md +++ b/docs/src/usage.md @@ -26,7 +26,7 @@ Common to both `kani` and `cargo kani` are many command-line flags: * `--concrete-playback=[print|inplace]`: _Experimental_, `--enable-unstable` feature that generates a Rust unit test case that plays back a failing proof harness using a concrete counterexample. If used with `print`, Kani will only print the unit test to stdout. - If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [debugging verification failures](./debugging-verification-failures.md) section. + If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [concrete playback](./experimental/concrete-playback.md) section. * `--visualize`: _Experimental_, `--enable-unstable` feature that generates an HTML report providing traces (i.e., counterexamples) for each failure found by Kani. diff --git a/docs/src/verification-results.md b/docs/src/verification-results.md index a8187163d41b..100c9ed554be 100644 --- a/docs/src/verification-results.md +++ b/docs/src/verification-results.md @@ -38,7 +38,7 @@ Check 4: success_example.assertion.4 ``` 2. `FAILURE`: This indicates that the check failed (i.e., the property doesn't -hold). In this case, please see the [debugging verification failures](./debugging-verification-failures.md) +hold). In this case, please see the [concrete playback](./experimental/concrete-playback.md) section for more help. Example: From 9d1cc0ee89c8510c7208867cd4becd9d3dc6b9a5 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 31 Jul 2024 17:01:16 -0700 Subject: [PATCH 10/11] Add code scanner tool (#3120) This is just a utility tool that allow us to scan a crate and extract some metrics out of it. I also added a script to scan the standard library. Currently, the tool will produce a few CSV files with raw data. --------- Co-authored-by: Qinheping Hu --- Cargo.lock | 31 + Cargo.toml | 1 + scripts/std-analysis.sh | 115 ++++ tests/perf/s2n-quic | 2 +- .../script-based-pre/tool-scanner/config.yml | 4 + .../tool-scanner/scanner-test.expected | 6 + .../tool-scanner/scanner-test.sh | 20 + tests/script-based-pre/tool-scanner/test.rs | 77 +++ tools/scanner/Cargo.toml | 23 + tools/scanner/build.rs | 26 + tools/scanner/src/analysis.rs | 629 ++++++++++++++++++ tools/scanner/src/bin/scan.rs | 31 + tools/scanner/src/lib.rs | 103 +++ 13 files changed, 1067 insertions(+), 1 deletion(-) create mode 100755 scripts/std-analysis.sh create mode 100644 tests/script-based-pre/tool-scanner/config.yml create mode 100644 tests/script-based-pre/tool-scanner/scanner-test.expected create mode 100755 tests/script-based-pre/tool-scanner/scanner-test.sh create mode 100644 tests/script-based-pre/tool-scanner/test.rs create mode 100644 tools/scanner/Cargo.toml create mode 100644 tools/scanner/build.rs create mode 100644 tools/scanner/src/analysis.rs create mode 100644 tools/scanner/src/bin/scan.rs create mode 100644 tools/scanner/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index 01dbccdd546a..d68b8db21918 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -288,6 +288,27 @@ dependencies = [ "winapi", ] +[[package]] +name = "csv" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac574ff4d437a7b5ad237ef331c17ccca63c46479e5b5453eb8e10bb99a759fe" +dependencies = [ + "csv-core", + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "csv-core" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5efa2b3d7902f4b634a20cae3c9c4e6209dc4779feb6863329607560143efa70" +dependencies = [ + "memchr", +] + [[package]] name = "either" version = "1.13.0" @@ -892,6 +913,16 @@ dependencies = [ "winapi-util", ] +[[package]] +name = "scanner" +version = "0.0.0" +dependencies = [ + "csv", + "serde", + "strum", + "strum_macros", +] + [[package]] name = "scopeguard" version = "1.2.0" diff --git a/Cargo.toml b/Cargo.toml index 1b4933c5bdcf..68b5bcc20ff3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -40,6 +40,7 @@ members = [ "library/std", "tools/compiletest", "tools/build-kani", + "tools/scanner", "kani-driver", "kani-compiler", "kani_metadata", diff --git a/scripts/std-analysis.sh b/scripts/std-analysis.sh new file mode 100755 index 000000000000..87ac991cb00d --- /dev/null +++ b/scripts/std-analysis.sh @@ -0,0 +1,115 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Collect some metrics related to the crates that compose the standard library. +# +# Files generates so far: +# +# - ${crate}_scan_overall.csv: Summary of function metrics, such as safe vs unsafe. +# - ${crate}_scan_input_tys.csv: Detailed information about the inputs' type of each +# function found in this crate. +# +# How we collect metrics: +# +# - Compile the standard library using the `scan` tool to collect some metrics. +# - After compilation, move all CSV files that were generated by the scanner, +# to the results folder. +set -eu + +# Test for platform +PLATFORM=$(uname -sp) +if [[ $PLATFORM == "Linux x86_64" ]] +then + TARGET="x86_64-unknown-linux-gnu" + # 'env' necessary to avoid bash built-in 'time' + WRAPPER="env time -v" +elif [[ $PLATFORM == "Darwin i386" ]] +then + TARGET="x86_64-apple-darwin" + # mac 'time' doesn't have -v + WRAPPER="time" +elif [[ $PLATFORM == "Darwin arm" ]] +then + TARGET="aarch64-apple-darwin" + # mac 'time' doesn't have -v + WRAPPER="time" +else + echo + echo "Std-Lib codegen regression only works on Linux or OSX x86 platforms, skipping..." + echo + exit 0 +fi + +# Get Kani root +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" +KANI_DIR=$(dirname "$SCRIPT_DIR") + +echo "-------------------------------------------------------" +echo "-- Starting analysis of the Rust standard library... --" +echo "-------------------------------------------------------" + +echo "-- Build scanner" +cd $KANI_DIR +cargo build -p scanner + +echo "-- Build std" +cd /tmp +if [ -d std_lib_analysis ] +then + rm -rf std_lib_analysis +fi +cargo new std_lib_analysis --lib +cd std_lib_analysis + +echo ' +pub fn dummy() { +} +' > src/lib.rs + +# Use same nightly toolchain used to build Kani +cp ${KANI_DIR}/rust-toolchain.toml . + +export RUST_BACKTRACE=1 +export RUSTC_LOG=error + +RUST_FLAGS=( + "-Cpanic=abort" + "-Zalways-encode-mir" +) +export RUSTFLAGS="${RUST_FLAGS[@]}" +export RUSTC="$KANI_DIR/target/debug/scan" +# Compile rust with our extension +$WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET + +echo "-- Process results" + +# Move files to results folder +results=/tmp/std_lib_analysis/results +mkdir $results +find /tmp/std_lib_analysis/target -name "*.csv" -exec mv {} $results \; + +# Create a summary table +summary=$results/summary.csv + +# write header +echo -n "crate," > $summary +tr -d "[:digit:],;" < $results/alloc_scan_overall.csv \ + | tr -s '\n' ',' >> $summary +echo "" >> $summary + +# write body +for f in $results/*overall.csv; do + # Join all crate summaries into one table + fname=$(basename $f) + crate=${fname%_scan_overall.csv} + echo -n "$crate," >> $summary + tr -d [:alpha:]_,; < $f | tr -s '\n' ',' \ + >> $summary + echo "" >> $summary +done + +echo "-------------------------------------------------------" +echo "Finished analysis successfully..." +echo "- See results at ${results}" +echo "-------------------------------------------------------" diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 71f8d9f5aafb..2d5e891f3fdc 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 71f8d9f5aafbf59f31ad85eeb7b4b67a7564a685 +Subproject commit 2d5e891f3fdc8a88b2d457baceedea5751efaa0d diff --git a/tests/script-based-pre/tool-scanner/config.yml b/tests/script-based-pre/tool-scanner/config.yml new file mode 100644 index 000000000000..6fd2895971a4 --- /dev/null +++ b/tests/script-based-pre/tool-scanner/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: scanner-test.sh +expected: scanner-test.expected diff --git a/tests/script-based-pre/tool-scanner/scanner-test.expected b/tests/script-based-pre/tool-scanner/scanner-test.expected new file mode 100644 index 000000000000..c8f9af0ef1b7 --- /dev/null +++ b/tests/script-based-pre/tool-scanner/scanner-test.expected @@ -0,0 +1,6 @@ +2 test_scan_fn_loops.csv +16 test_scan_functions.csv +5 test_scan_input_tys.csv +14 test_scan_overall.csv +3 test_scan_recursion.csv +5 test_scan_unsafe_ops.csv diff --git a/tests/script-based-pre/tool-scanner/scanner-test.sh b/tests/script-based-pre/tool-scanner/scanner-test.sh new file mode 100755 index 000000000000..2cd5a33a3f8e --- /dev/null +++ b/tests/script-based-pre/tool-scanner/scanner-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -e + +# Run this inside a tmp folder in the current directory +OUT_DIR=output_dir +# Ensure output folder is clean +rm -rf ${OUT_DIR} +mkdir output_dir +# Move the original source to the output folder since it will be modified +cp test.rs ${OUT_DIR} +pushd $OUT_DIR + +cargo run -p scanner test.rs --crate-type lib +wc -l *csv + +popd +rm -rf ${OUT_DIR} diff --git a/tests/script-based-pre/tool-scanner/test.rs b/tests/script-based-pre/tool-scanner/test.rs new file mode 100644 index 000000000000..24b346e535b5 --- /dev/null +++ b/tests/script-based-pre/tool-scanner/test.rs @@ -0,0 +1,77 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Sanity check for the utility tool `scanner`. + +pub fn check_outer_coercion() { + assert!(false); +} + +unsafe fn do_nothing() {} + +pub fn generic() -> T { + unsafe { do_nothing() }; + T::default() +} + +pub struct RecursiveType { + pub inner: Option<*const RecursiveType>, +} + +pub enum RecursiveEnum { + Base, + Recursion(Box), + RefCell(std::cell::RefCell), +} + +pub fn recursive_type(input1: RecursiveType, input2: RecursiveEnum) { + let _ = (input1, input2); +} + +pub fn with_iterator(input: &[usize]) -> usize { + input + .iter() + .copied() + .find(|e| *e == 0) + .unwrap_or_else(|| input.iter().fold(0, |acc, i| acc + 1)) +} + +static mut COUNTER: Option = Some(0); +static OK: bool = true; + +pub unsafe fn next_id() -> usize { + let sum = COUNTER.unwrap() + 1; + COUNTER = Some(sum); + sum +} + +pub unsafe fn current_id() -> usize { + COUNTER.unwrap() +} + +pub fn ok() -> bool { + OK +} + +pub unsafe fn raw_to_ref<'a, T>(raw: *const T) -> &'a T { + &*raw +} + +pub fn recursion_begin(stop: bool) { + if !stop { + recursion_tail() + } +} + +pub fn recursion_tail() { + recursion_begin(false); + not_recursive(); +} + +pub fn start_recursion() { + recursion_begin(true); +} + +pub fn not_recursive() { + let _ = ok(); +} diff --git a/tools/scanner/Cargo.toml b/tools/scanner/Cargo.toml new file mode 100644 index 000000000000..edbd330bea47 --- /dev/null +++ b/tools/scanner/Cargo.toml @@ -0,0 +1,23 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + + +[package] +name = "scanner" +description = "A rustc extension used to scan rust features in a crate" +version = "0.0.0" +edition = "2021" +license = "MIT OR Apache-2.0" +publish = false + +[dependencies] +csv = "1.3" +serde = {version = "1", features = ["derive"]} +strum = "0.26" +strum_macros = "0.26" + +[package.metadata.rust-analyzer] +# This crate uses rustc crates. +# More info: https://github.com/rust-analyzer/rust-analyzer/pull/7891 +rustc_private = true + diff --git a/tools/scanner/build.rs b/tools/scanner/build.rs new file mode 100644 index 000000000000..775a0f507a45 --- /dev/null +++ b/tools/scanner/build.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use std::env; +use std::path::PathBuf; + +macro_rules! path_str { + ($input:expr) => { + String::from( + $input + .iter() + .collect::() + .to_str() + .unwrap_or_else(|| panic!("Invalid path {}", stringify!($input))), + ) + }; +} + +/// Configure the compiler to properly link the scanner binary with rustc's library. +pub fn main() { + // Add rustup to the rpath in order to properly link with the correct rustc version. + let rustup_home = env::var("RUSTUP_HOME").unwrap(); + let rustup_tc = env::var("RUSTUP_TOOLCHAIN").unwrap(); + let rustup_lib = path_str!([&rustup_home, "toolchains", &rustup_tc, "lib"]); + println!("cargo:rustc-link-arg-bin=scan=-Wl,-rpath,{rustup_lib}"); +} diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs new file mode 100644 index 000000000000..c376af9662f8 --- /dev/null +++ b/tools/scanner/src/analysis.rs @@ -0,0 +1,629 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Provide different static analysis to be performed in the crate under compilation + +use crate::info; +use csv::WriterBuilder; +use serde::{ser::SerializeStruct, Serialize, Serializer}; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; +use stable_mir::mir::{ + Body, MirVisitor, Mutability, ProjectionElem, Safety, Terminator, TerminatorKind, +}; +use stable_mir::ty::{AdtDef, AdtKind, FnDef, GenericArgs, MirConst, RigidTy, Ty, TyKind}; +use stable_mir::visitor::{Visitable, Visitor}; +use stable_mir::{CrateDef, CrateItem}; +use std::collections::{HashMap, HashSet}; +use std::ops::ControlFlow; +use std::path::{Path, PathBuf}; + +#[derive(Clone, Debug)] +pub struct OverallStats { + /// The key and value of each counter. + counters: Vec<(&'static str, usize)>, + /// TODO: Group stats per function. + fn_stats: HashMap, +} + +#[derive(Clone, Debug, Serialize)] +struct FnStats { + name: String, + is_unsafe: Option, + has_unsafe_ops: Option, + has_unsupported_input: Option, + has_loop: Option, +} + +impl FnStats { + fn new(fn_item: CrateItem) -> FnStats { + FnStats { + name: fn_item.name(), + is_unsafe: None, + has_unsafe_ops: None, + has_unsupported_input: None, + // TODO: Implement this. + has_loop: None, + } + } +} + +impl OverallStats { + pub fn new() -> OverallStats { + let all_items = stable_mir::all_local_items(); + let fn_stats: HashMap<_, _> = all_items + .into_iter() + .filter_map(|item| item.ty().kind().is_fn().then_some((item, FnStats::new(item)))) + .collect(); + let counters = vec![("total_fns", fn_stats.len())]; + OverallStats { counters, fn_stats } + } + + pub fn store_csv(&self, base_path: PathBuf, file_stem: &str) { + let filename = format!("{}_overall", file_stem); + let mut out_path = base_path.parent().map_or(PathBuf::default(), Path::to_path_buf); + out_path.set_file_name(filename); + dump_csv(out_path, &self.counters); + + let filename = format!("{}_functions", file_stem); + let mut out_path = base_path.parent().map_or(PathBuf::default(), Path::to_path_buf); + out_path.set_file_name(filename); + dump_csv(out_path, &self.fn_stats.values().collect::>()); + } + + /// Iterate over all functions defined in this crate and log generic vs monomorphic. + pub fn generic_fns(&mut self) { + let all_items = stable_mir::all_local_items(); + let fn_items = + all_items.into_iter().filter(|item| item.ty().kind().is_fn()).collect::>(); + let (mono_fns, generics) = fn_items + .iter() + .partition::, _>(|fn_item| Instance::try_from(**fn_item).is_ok()); + self.counters + .extend_from_slice(&[("generic_fns", generics.len()), ("mono_fns", mono_fns.len())]); + } + + /// Iterate over all functions defined in this crate and log safe vs unsafe. + pub fn safe_fns(&mut self, _base_filename: PathBuf) { + let all_items = stable_mir::all_local_items(); + let (unsafe_fns, safe_fns) = all_items + .into_iter() + .filter_map(|item| { + let kind = item.ty().kind(); + if !kind.is_fn() { + return None; + }; + let fn_sig = kind.fn_sig().unwrap(); + let is_unsafe = fn_sig.skip_binder().safety == Safety::Unsafe; + self.fn_stats.get_mut(&item).unwrap().is_unsafe = Some(is_unsafe); + Some((item, is_unsafe)) + }) + .partition::, _>(|(_, is_unsafe)| *is_unsafe); + self.counters + .extend_from_slice(&[("safe_fns", safe_fns.len()), ("unsafe_fns", unsafe_fns.len())]); + } + + /// Iterate over all functions defined in this crate and log the inputs. + pub fn supported_inputs(&mut self, filename: PathBuf) { + let all_items = stable_mir::all_local_items(); + let (supported, unsupported) = all_items + .into_iter() + .filter_map(|item| { + let kind = item.ty().kind(); + if !kind.is_fn() { + return None; + }; + let fn_sig = kind.fn_sig().unwrap(); + let props = FnInputProps::new(item.name()).collect(fn_sig.skip_binder().inputs()); + self.fn_stats.get_mut(&item).unwrap().has_unsupported_input = + Some(!props.is_supported()); + Some(props) + }) + .partition::, _>(|props| props.is_supported()); + self.counters.extend_from_slice(&[ + ("supported_inputs", supported.len()), + ("unsupported_inputs", unsupported.len()), + ]); + dump_csv(filename, &unsupported); + } + + /// Iterate over all functions defined in this crate and log any unsafe operation. + pub fn unsafe_operations(&mut self, filename: PathBuf) { + let all_items = stable_mir::all_local_items(); + let (has_unsafe, no_unsafe) = all_items + .into_iter() + .filter_map(|item| { + let kind = item.ty().kind(); + if !kind.is_fn() { + return None; + }; + let unsafe_ops = FnUnsafeOperations::new(item.name()).collect(&item.body()); + let fn_sig = kind.fn_sig().unwrap(); + let is_unsafe = fn_sig.skip_binder().safety == Safety::Unsafe; + self.fn_stats.get_mut(&item).unwrap().has_unsafe_ops = + Some(unsafe_ops.has_unsafe()); + Some((is_unsafe, unsafe_ops)) + }) + .partition::, _>(|(_, props)| props.has_unsafe()); + self.counters.extend_from_slice(&[ + ("has_unsafe_ops", has_unsafe.len()), + ("no_unsafe_ops", no_unsafe.len()), + ("safe_abstractions", has_unsafe.iter().filter(|(is_unsafe, _)| !is_unsafe).count()), + ]); + dump_csv(filename, &has_unsafe.into_iter().map(|(_, props)| props).collect::>()); + } + + /// Iterate over all functions defined in this crate and log any loop / "hidden" loop. + /// + /// A hidden loop is a call to a iterator function that has a loop inside. + pub fn loops(&mut self, filename: PathBuf) { + let all_items = stable_mir::all_local_items(); + let (has_loops, no_loops) = all_items + .into_iter() + .filter_map(|item| { + let kind = item.ty().kind(); + if !kind.is_fn() { + return None; + }; + Some(FnLoops::new(item.name()).collect(&item.body())) + }) + .partition::, _>(|props| props.has_loops()); + self.counters + .extend_from_slice(&[("has_loops", has_loops.len()), ("no_loops", no_loops.len())]); + dump_csv(filename, &has_loops); + } + + /// Create a callgraph for this crate and try to find recursive calls. + pub fn recursion(&mut self, filename: PathBuf) { + let all_items = stable_mir::all_local_items(); + let recursions = Recursion::collect(&all_items); + self.counters.extend_from_slice(&[ + ("with_recursion", recursions.with_recursion.len()), + ("recursive_fns", recursions.recursive_fns.len()), + ]); + dump_csv( + filename, + &recursions + .with_recursion + .iter() + .map(|def| { + ( + def.name(), + if recursions.recursive_fns.contains(&def) { "recursive" } else { "" }, + ) + }) + .collect::>(), + ); + } +} + +macro_rules! fn_props { + ($(#[$attr:meta])* + struct $name:ident { + $( + $(#[$prop_attr:meta])* + $prop:ident, + )+ + }) => { + #[derive(Debug)] + struct $name { + fn_name: String, + $($(#[$prop_attr])* $prop: usize,)+ + } + + impl $name { + const fn num_props() -> usize { + [$(stringify!($prop),)+].len() + } + + fn new(fn_name: String) -> Self { + Self { fn_name, $($prop: 0,)+} + } + } + + /// Need to manually implement this, since CSV serializer does not support map (i.e.: flatten). + impl Serialize for $name { + fn serialize(&self, serializer: S) -> Result + where + S: Serializer, + { + let mut state = serializer.serialize_struct("FnInputProps", Self::num_props())?; + state.serialize_field("fn_name", &self.fn_name)?; + $(state.serialize_field(stringify!($prop), &self.$prop)?;)+ + state.end() + } + } + }; +} + +fn_props! { + struct FnInputProps { + boxes, + closures, + coroutines, + floats, + fn_defs, + fn_ptrs, + generics, + interior_muts, + raw_ptrs, + recursive_types, + mut_refs, + simd, + unions, + } +} + +impl FnInputProps { + pub fn collect(mut self, inputs: &[Ty]) -> FnInputProps { + for input in inputs { + let mut visitor = TypeVisitor { metrics: &mut self, visited: HashSet::new() }; + let _ = visitor.visit_ty(input); + } + self + } + + pub fn is_supported(&self) -> bool { + (self.closures + + self.coroutines + + self.floats + + self.fn_defs + + self.fn_ptrs + + self.interior_muts + + self.raw_ptrs + + self.recursive_types + + self.mut_refs) + == 0 + } +} + +struct TypeVisitor<'a> { + metrics: &'a mut FnInputProps, + visited: HashSet, +} + +impl<'a> TypeVisitor<'a> { + pub fn visit_variants(&mut self, def: AdtDef, _args: &GenericArgs) -> ControlFlow<()> { + for variant in def.variants_iter() { + for field in variant.fields() { + self.visit_ty(&field.ty())? + } + } + ControlFlow::Continue(()) + } +} + +impl<'a> Visitor for TypeVisitor<'a> { + type Break = (); + + fn visit_ty(&mut self, ty: &Ty) -> ControlFlow { + if self.visited.contains(ty) { + self.metrics.recursive_types += 1; + ControlFlow::Continue(()) + } else { + self.visited.insert(*ty); + let kind = ty.kind(); + match kind { + TyKind::Alias(..) => {} + TyKind::Param(_) => self.metrics.generics += 1, + TyKind::RigidTy(rigid) => match rigid { + RigidTy::Coroutine(..) => self.metrics.coroutines += 1, + RigidTy::Closure(..) => self.metrics.closures += 1, + RigidTy::FnDef(..) => self.metrics.fn_defs += 1, + RigidTy::FnPtr(..) => self.metrics.fn_ptrs += 1, + RigidTy::Float(..) => self.metrics.floats += 1, + RigidTy::RawPtr(..) => self.metrics.raw_ptrs += 1, + RigidTy::Ref(_, _, Mutability::Mut) => self.metrics.mut_refs += 1, + RigidTy::Adt(def, args) => match def.kind() { + AdtKind::Union => self.metrics.unions += 1, + _ => { + let name = def.name(); + if def.is_box() { + self.metrics.boxes += 1; + } else if name.ends_with("UnsafeCell") { + self.metrics.interior_muts += 1; + } else { + self.visit_variants(def, &args)?; + } + } + }, + _ => {} + }, + kind => unreachable!("Expected rigid type, but found: {kind:?}"), + } + ty.super_visit(self) + } + } +} + +fn dump_csv(mut out_path: PathBuf, data: &[T]) { + out_path.set_extension("csv"); + info(format!("Write file: {out_path:?}")); + let mut writer = WriterBuilder::new().delimiter(b';').from_path(&out_path).unwrap(); + for d in data { + writer.serialize(d).unwrap(); + } +} + +fn_props! { + struct FnUnsafeOperations { + inline_assembly, + /// Dereference a raw pointer. + /// This is also counted when we access a static variable since it gets translated to a raw pointer. + unsafe_dereference, + /// Call an unsafe function or method. + unsafe_call, + /// Access or modify a mutable static variable. + unsafe_static_access, + /// Access fields of unions. + unsafe_union_access, + } +} + +impl FnUnsafeOperations { + pub fn collect(self, body: &Body) -> FnUnsafeOperations { + let mut visitor = BodyVisitor { props: self, body }; + visitor.visit_body(body); + visitor.props + } + + pub fn has_unsafe(&self) -> bool { + (self.inline_assembly + + self.unsafe_static_access + + self.unsafe_dereference + + self.unsafe_union_access + + self.unsafe_call) + > 0 + } +} + +struct BodyVisitor<'a> { + props: FnUnsafeOperations, + body: &'a Body, +} + +impl<'a> MirVisitor for BodyVisitor<'a> { + fn visit_terminator(&mut self, term: &Terminator, location: Location) { + match &term.kind { + TerminatorKind::Call { func, .. } => { + let fn_sig = func.ty(self.body.locals()).unwrap().kind().fn_sig().unwrap(); + if fn_sig.value.safety == Safety::Unsafe { + self.props.unsafe_call += 1; + } + } + TerminatorKind::InlineAsm { .. } => self.props.inline_assembly += 1, + _ => { /* safe */ } + } + self.super_terminator(term, location) + } + + fn visit_projection_elem( + &mut self, + place: PlaceRef, + elem: &ProjectionElem, + ptx: PlaceContext, + location: Location, + ) { + match elem { + ProjectionElem::Deref => { + if place.ty(self.body.locals()).unwrap().kind().is_raw_ptr() { + self.props.unsafe_dereference += 1; + } + } + ProjectionElem::Field(_, ty) => { + if ty.kind().is_union() { + self.props.unsafe_union_access += 1; + } + } + ProjectionElem::Downcast(_) => {} + ProjectionElem::OpaqueCast(_) => {} + ProjectionElem::Subtype(_) => {} + ProjectionElem::Index(_) + | ProjectionElem::ConstantIndex { .. } + | ProjectionElem::Subslice { .. } => { /* safe */ } + } + self.super_projection_elem(elem, ptx, location) + } + + fn visit_mir_const(&mut self, constant: &MirConst, location: Location) { + if constant.ty().kind().is_raw_ptr() { + self.props.unsafe_static_access += 1; + } + self.super_mir_const(constant, location) + } +} + +fn_props! { + struct FnLoops { + iterators, + nested_loops, + /// TODO: Collect loops. + loops, + } +} + +impl FnLoops { + pub fn collect(self, body: &Body) -> FnLoops { + let mut visitor = IteratorVisitor { props: self, body }; + visitor.visit_body(body); + visitor.props + } + + pub fn has_loops(&self) -> bool { + (self.iterators + self.loops + self.nested_loops) > 0 + } +} + +/// Try to find hidden loops by looking for calls to Iterator functions that has a loop in them. +/// +/// Note that this will not find a loop, if the iterator is called inside a closure. +/// Run with -C opt-level 2 to help with this issue (i.e.: inline). +struct IteratorVisitor<'a> { + props: FnLoops, + body: &'a Body, +} + +impl<'a> MirVisitor for IteratorVisitor<'a> { + fn visit_terminator(&mut self, term: &Terminator, location: Location) { + if let TerminatorKind::Call { func, .. } = &term.kind { + let kind = func.ty(self.body.locals()).unwrap().kind(); + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = kind { + let fullname = def.name(); + let names = fullname.split("::").collect::>(); + if let [.., s_last, last] = names.as_slice() { + if *s_last == "Iterator" + && [ + "for_each", + "collect", + "advance_by", + "all", + "any", + "partition", + "partition_in_place", + "fold", + "try_fold", + "spec_fold", + "spec_try_fold", + "try_for_each", + "for_each", + "try_reduce", + "reduce", + "find", + "find_map", + "try_find", + "position", + "rposition", + "nth", + "count", + "last", + "find", + ] + .contains(last) + { + self.props.iterators += 1; + } + } + } + } + self.super_terminator(term, location) + } +} + +#[derive(Debug, Default)] +struct Recursion { + /// Collect the functions that may lead to a recursion loop. + /// I.e., for the following control flow graph: + /// ```dot + /// A -> B + /// B -> C + /// C -> [B, D] + /// ``` + /// this field value would contain A, B, and C since they can all lead to a recursion. + with_recursion: HashSet, + /// Collect the functions that are part of a recursion loop. + /// For the following control flow graph: + /// ```dot + /// A -> [B, C] + /// B -> B + /// C -> D + /// D -> [C, E] + /// ``` + /// The recursive functions would be B, C, and D. + recursive_fns: HashSet, +} + +impl Recursion { + pub fn collect<'a>(items: impl IntoIterator) -> Recursion { + let call_graph = items + .into_iter() + .filter_map(|item| { + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = item.ty().kind() { + let body = item.body(); + let mut visitor = FnCallVisitor { body: &body, fns: vec![] }; + visitor.visit_body(&body); + Some((def, visitor.fns)) + } else { + None + } + }) + .collect::>(); + let mut recursions = Recursion::default(); + recursions.analyze(call_graph); + recursions + } + + /// DFS post-order traversal to collect all loops in our control flow graph. + /// We only include direct call recursions which can only happen within a crate. + /// + /// # How it works + /// + /// Given a call graph, [(fn_def, [fn_def]*)]*, enqueue all existing nodes together with the + /// graph distance. + /// Keep track of the current path and the visiting status of each node. + /// For those that we have visited once, store whether a loop is reachable from them. + fn analyze(&mut self, call_graph: HashMap>) { + #[derive(Copy, Clone, PartialEq, Eq)] + enum Status { + ToVisit, + Visiting, + Visited, + } + let mut visit_status = HashMap::::new(); + let mut queue: Vec<_> = call_graph.keys().map(|node| (*node, 0)).collect(); + let mut path: Vec = vec![]; + while let Some((next, level)) = queue.last().copied() { + match visit_status.get(&next).unwrap_or(&Status::ToVisit) { + Status::ToVisit => { + assert_eq!(path.len(), level); + path.push(next); + visit_status.insert(next, Status::Visiting); + let next_level = level + 1; + if let Some(callees) = call_graph.get(&next) { + queue.extend(callees.iter().map(|callee| (*callee, next_level))); + } + } + Status::Visiting => { + if level < path.len() { + // We have visited all callees in this node. + visit_status.insert(next, Status::Visited); + path.pop(); + } else { + // Found a loop. + let mut in_loop = false; + for def in &path { + in_loop |= *def == next; + if in_loop { + self.recursive_fns.insert(*def); + } + self.with_recursion.insert(*def); + } + } + queue.pop(); + } + Status::Visited => { + queue.pop(); + if self.with_recursion.contains(&next) { + self.with_recursion.extend(&path); + } + } + } + } + } +} + +struct FnCallVisitor<'a> { + body: &'a Body, + fns: Vec, +} + +impl<'a> MirVisitor for FnCallVisitor<'a> { + fn visit_terminator(&mut self, term: &Terminator, location: Location) { + if let TerminatorKind::Call { func, .. } = &term.kind { + let kind = func.ty(self.body.locals()).unwrap().kind(); + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = kind { + self.fns.push(def); + } + } + self.super_terminator(term, location) + } +} diff --git a/tools/scanner/src/bin/scan.rs b/tools/scanner/src/bin/scan.rs new file mode 100644 index 000000000000..92b5319ec780 --- /dev/null +++ b/tools/scanner/src/bin/scan.rs @@ -0,0 +1,31 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// This is a modified version of project-stable-mir `test-drive` +// + +//! Provide a binary that can be used as a replacement to rustc. +//! +//! Besides executing the regular compilation, this binary will run a few static analyses. +//! +//! The result for each analysis will be stored in a file with the same prefix as an object file, +//! together with the name of the analysis. +//! +//! Look at each analysis documentation to see which files an analysis produces. + +use scanner::run_all; +use std::process::ExitCode; + +// ---- Arguments that should be parsed by the test-driver (w/ "scan" prefix) +/// Enable verbose mode. +const VERBOSE_ARG: &str = "--scan-verbose"; + +/// This is a wrapper that can be used to replace rustc. +fn main() -> ExitCode { + let args = std::env::args(); + let (scan_args, rustc_args): (Vec, _) = args.partition(|arg| arg.starts_with("--scan")); + let verbose = scan_args.contains(&VERBOSE_ARG.to_string()); + run_all(rustc_args, verbose) +} diff --git a/tools/scanner/src/lib.rs b/tools/scanner/src/lib.rs new file mode 100644 index 000000000000..7f9555781ccf --- /dev/null +++ b/tools/scanner/src/lib.rs @@ -0,0 +1,103 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// This is a modified version of project-stable-mir `test-drive` +// + +//! This library provide different ways of scanning a crate. + +#![feature(rustc_private)] + +mod analysis; + +extern crate rustc_driver; +extern crate rustc_interface; +extern crate rustc_middle; +extern crate rustc_session; +#[macro_use] +extern crate rustc_smir; +extern crate stable_mir; + +use crate::analysis::OverallStats; +use rustc_middle::ty::TyCtxt; +use rustc_session::config::OutputType; +use rustc_smir::{run_with_tcx, rustc_internal}; +use stable_mir::CompilerError; +use std::ops::ControlFlow; +use std::path::{Path, PathBuf}; +use std::process::ExitCode; +use std::sync::atomic::{AtomicBool, Ordering}; +use strum::IntoEnumIterator; +use strum_macros::{AsRefStr, EnumIter}; + +// Use a static variable for simplicity. +static VERBOSE: AtomicBool = AtomicBool::new(false); + +pub fn run_all(rustc_args: Vec, verbose: bool) -> ExitCode { + run_analyses(rustc_args, &Analysis::iter().collect::>(), verbose) +} + +/// Executes a compilation and run the analysis that were requested. +pub fn run_analyses(rustc_args: Vec, analyses: &[Analysis], verbose: bool) -> ExitCode { + VERBOSE.store(verbose, Ordering::Relaxed); + let result = run_with_tcx!(rustc_args, |tcx| analyze_crate(tcx, analyses)); + if result.is_ok() || matches!(result, Err(CompilerError::Skipped)) { + ExitCode::SUCCESS + } else { + ExitCode::FAILURE + } +} + +#[derive(AsRefStr, EnumIter, Debug, PartialEq)] +#[strum(serialize_all = "snake_case")] +pub enum Analysis { + /// Collect information about generic functions. + MonoFns, + /// Collect information about function safety. + SafeFns, + /// Collect information about function inputs. + InputTys, + /// Collect information about unsafe operations. + UnsafeOps, + /// Collect information about loops inside a function. + FnLoops, + /// Collect information about recursion via direct calls. + Recursion, +} + +fn info(msg: String) { + if VERBOSE.load(Ordering::Relaxed) { + eprintln!("[INFO] {}", msg); + } +} + +/// This function invoke the required analyses in the given order. +fn analyze_crate(tcx: TyCtxt, analyses: &[Analysis]) -> ControlFlow<()> { + let object_file = tcx.output_filenames(()).path(OutputType::Object); + let base_path = object_file.as_path().to_path_buf(); + // Use name for now to make it more friendly. Change to base_path.file_stem() to avoid conflict. + // let file_stem = base_path.file_stem().unwrap(); + let file_stem = format!("{}_scan", stable_mir::local_crate().name); + let mut crate_stats = OverallStats::new(); + for analysis in analyses { + let filename = format!("{}_{}", file_stem, analysis.as_ref()); + let mut out_path = base_path.parent().map_or(PathBuf::default(), Path::to_path_buf); + out_path.set_file_name(filename); + match analysis { + Analysis::MonoFns => { + crate_stats.generic_fns(); + } + Analysis::SafeFns => { + crate_stats.safe_fns(out_path); + } + Analysis::InputTys => crate_stats.supported_inputs(out_path), + Analysis::UnsafeOps => crate_stats.unsafe_operations(out_path), + Analysis::FnLoops => crate_stats.loops(out_path), + Analysis::Recursion => crate_stats.recursion(out_path), + } + } + crate_stats.store_csv(base_path, &file_stem); + ControlFlow::<()>::Continue(()) +} From 370b2159ce179b82c4781fe7db1e93de68c900aa Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 1 Aug 2024 09:38:47 +0200 Subject: [PATCH 11/11] Automatic toolchain upgrade to nightly-2024-08-01 (#3402) Update Rust toolchain from nightly-2024-07-31 to nightly-2024-08-01 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/f8060d282d42770fadd73905e3eefb85660d3278 up to https://github.com/rust-lang/rust/commit/28a58f2fa7f0c46b8fab8237c02471a915924fe5. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index f7324e45d06d..8753157827b5 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-07-31" +channel = "nightly-2024-08-01" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]