Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make panic and assert const functions #1590

Merged
merged 2 commits into from
Aug 26, 2022
Merged

Make panic and assert const functions #1590

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
817310a
Make panic a const function
zhassan-aws Aug 26, 2022
1591fa4
Make assert const as well
zhassan-aws Aug 26, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions library/kani/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ pub fn assume(_cond: bool) {
/// ```
#[inline(never)]
#[rustc_diagnostic_item = "KaniAssert"]
pub fn assert(_cond: bool, _msg: &'static str) {
pub const fn assert(_cond: bool, _msg: &'static str) {
if cfg!(feature = "concrete_playback") {
assert!(_cond, "{}", _msg);
}
Expand Down Expand Up @@ -134,7 +134,7 @@ pub fn expect_fail(_cond: bool, _message: &'static str) {
#[inline(never)]
#[rustc_diagnostic_item = "KaniPanic"]
#[doc(hidden)]
pub fn panic(message: &'static str) -> ! {
pub const fn panic(message: &'static str) -> ! {
panic!("{}", message)
}

Expand Down
15 changes: 15 additions & 0 deletions tests/kani/Assert/in_const_fn.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! This test checks that `assert!` can be used in a const fn

const fn const_add(x: i32, y: i32) {
assert!(x + y == x);
}

#[kani::proof]
fn check() {
let x = kani::any();
let y = 0;
const_add(x, y);
}
16 changes: 16 additions & 0 deletions tests/kani/Panic/const.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! This test checks that `panic!` can be used in a const fn

const fn my_const_fn() {
panic!()
}

#[kani::proof]
pub fn check_something() {
let x: u8 = if kani::any() { 3 } else { 95 };
if x > 100 {
my_const_fn();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This call isn't reachable (x > 100 is always false). The test shows you can use panic! in a const fn but I think you want to also call it, right?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The impetus for this was definitely a compile-time error, so maybe not

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Correct, I'm intentionally not calling it so that the test passes. As Ted pointed out, compilation currently fails. The purpose of the kani::any() is to make sure the compiler doesn't optimize the function out (so we still have to codegen it).

}
}