Skip to content

NonZero (clamp) Proof #200

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

Closed
wants to merge 6 commits into from
Closed

NonZero (clamp) Proof #200

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5d800ef
clamp
lang280 Dec 1, 2024
8e81c29
directly use nonezero type for kani::any instead of using primitive i…
lang280 Dec 4, 2024
24f90a2
macro for clamp in case it should panic
lang280 Dec 4, 2024
33e0316
no -> not
lang280 Dec 5, 2024
cdaaa9e
delete the checking on clamp result in panic case
lang280 Dec 5, 2024
899c0d8
Merge branch 'main' into nonezero_clamp
carolynzech Dec 5, 2024
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
74 changes: 74 additions & 0 deletions library/core/src/num/nonzero.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2265,3 +2265,77 @@ mod verify {
nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128);
nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize);
}

#[cfg(kani)]
mod macro_nonzero_check_clamp {
Copy link
Member

Choose a reason for hiding this comment

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

Could you please merge this into the verify module as you did in #202?

use super::*;
macro_rules! nonzero_check_clamp {
($nonzero_type:ty, $nonzero_check_clamp_for:ident) => {
#[kani::proof]
pub fn $nonzero_check_clamp_for() {
let x: $nonzero_type = kani::any();
let min: $nonzero_type = kani::any();
let max: $nonzero_type = kani::any();
// Ensure min <= max, so the function should not panic
kani::assume(min <= max);
// Use the clamp function and check the result
let result = x.clamp(min, max);
if x < min {
assert!(result == min);
} else if x > max {
assert!(result == max);
} else {
assert!(result == x);
}
}
};
}

// Use the macro to generate different versions of the function for multiple types
nonzero_check_clamp!(core::num::NonZeroI8, nonzero_check_clamp_for_i8);
nonzero_check_clamp!(core::num::NonZeroI16, nonzero_check_clamp_for_16);
nonzero_check_clamp!(core::num::NonZeroI32, nonzero_check_clamp_for_32);
nonzero_check_clamp!(core::num::NonZeroI64, nonzero_check_clamp_for_64);
nonzero_check_clamp!(core::num::NonZeroI128, nonzero_check_clamp_for_128);
nonzero_check_clamp!(core::num::NonZeroIsize, nonzero_check_clamp_for_isize);
nonzero_check_clamp!(core::num::NonZeroU8, nonzero_check_clamp_for_u8);
nonzero_check_clamp!(core::num::NonZeroU16, nonzero_check_clamp_for_u16);
nonzero_check_clamp!(core::num::NonZeroU32, nonzero_check_clamp_for_u32);
nonzero_check_clamp!(core::num::NonZeroU64, nonzero_check_clamp_for_u64);
nonzero_check_clamp!(core::num::NonZeroU128, nonzero_check_clamp_for_u128);
nonzero_check_clamp!(core::num::NonZeroUsize, nonzero_check_clamp_for_usize);
}

#[cfg(kani)]
mod macro_nonzero_check_clamp_panic {
use super::*;
macro_rules! nonzero_check_clamp_panic {
($nonzero_type:ty, $nonzero_check_clamp_for:ident) => {
#[kani::proof]
#[kani::should_panic]
pub fn $nonzero_check_clamp_for() {
let x: $nonzero_type = kani::any();
let min: $nonzero_type = kani::any();
let max: $nonzero_type = kani::any();
// Ensure min > max, so the function should panic
kani::assume(min > max);
// Use the clamp function which should cause panic
let result = x.clamp(min, max);
}
};
}

// Use the macro to generate different versions of the function for multiple types
nonzero_check_clamp_panic!(core::num::NonZeroI8, nonzero_check_clamp_panic_for_i8);
nonzero_check_clamp_panic!(core::num::NonZeroI16, nonzero_check_clamp_panic_for_16);
nonzero_check_clamp_panic!(core::num::NonZeroI32, nonzero_check_clamp_panic_for_32);
nonzero_check_clamp_panic!(core::num::NonZeroI64, nonzero_check_clamp_panic_for_64);
nonzero_check_clamp_panic!(core::num::NonZeroI128, nonzero_check_clamp_panic_for_128);
nonzero_check_clamp_panic!(core::num::NonZeroIsize, nonzero_check_clamp_panic_for_isize);
nonzero_check_clamp_panic!(core::num::NonZeroU8, nonzero_check_clamp_panic_for_u8);
nonzero_check_clamp_panic!(core::num::NonZeroU16, nonzero_check_clamp_panic_for_u16);
nonzero_check_clamp_panic!(core::num::NonZeroU32, nonzero_check_clamp_panic_for_u32);
nonzero_check_clamp_panic!(core::num::NonZeroU64, nonzero_check_clamp_panic_for_u64);
nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128);
nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize);
}