Repository navigation
[Challenge 6 Safety of NonNull] Verify contracts and proofs within the library source file #84
Description
We are AWS team 4 from CMU(@QinyuanWu @danielhumanmod @Jimmycreative @Dhvani-Kapadia) working on Challenge 6: Safety of Nonnull. We have written the contract and proof for the new_unchecked function in library/core/src/ptr/non_null.rs. We followed a similar structure as contracts and proofs in library/core/src/ptr/unique.rs.
Target function with contract:
impl<T: Sized> NonNull<T> {
#[requires(!ptr.is_null())]
#[ensures(|result| result.as_ptr() == ptr)]
pub const unsafe fn new_unchecked(ptr: *mut T) -> Self {
// SAFETY: the caller must guarantee that `ptr` is non-null.
unsafe {
assert_unsafe_precondition!(
check_language_ub,
"NonNull::new_unchecked requires that the pointer is non-null",
(ptr: *mut () = ptr as *mut ()) => !ptr.is_null()
);
NonNull { pointer: ptr as _ }
}
}#[cfg(kani)]
use crate::kani;
mod verify {
use super::*;
// pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
#[kani::proof_for_contract(NonNull::new_unchecked)]
pub fn check_new_unchecked() {
let mut x : i32 = kani::any();
let xptr = &mut x;
unsafe {
let _ = NonNull::new_unchecked(xptr as *mut i32);
}
}
}We followed the instructions on this page with the command kani verify-std -Z unstable-options "path/to/library/" -Z function-contracts -Z mem-predicates, and we have two issues:
- According to the verification result, we couldn't find any relevant check that was run for the
check_new_uncheckedproof innon_null.rs. Are we writing proofs in the correct location? - It seems like when we run the command above many functions are being verified at the same time. Is there a way to only verify a single contract/harness when using
verify-std -Z unstable-options?
Thank you and we appreciate your guidance^_^ @feliperodri @rahulku
Activity
zhassan-aws commentedon Sep 12, 2024
Hi @QinyuanWu. Thanks for opening this issue. The contract for
new_uncheckedlooks good.From looking at the log, it seems that the harness you wrote was not run. You can specify the
--harnessoption to run a specific one, e.g.You might also want to use the fully-qualified name for the harness to avoid running other harnesses with the same name, e.g.
--harness core::ptr::non_null::verify::check_new_unchecked.QinyuanWu commentedon Sep 13, 2024
Thank you for the response @zhassan-aws. I found that without supplying the
--harnessoption, both proofs inunique.rsandnon_null.rsare not run. Why is this? If we want to batch run proofs innon_null.rsin the future what command should we use?--harness core::ptr::non_null::verify::check_new_uncheckeddid not work(error: no harnesses matched the harness filter) and so does--harness core::ptr::non_null::NonNull::check_new_unchecked. I ended up changing the harness function name to a unique one(--harness non_null_check_new_unchecked) and that was successful(the fully-qualified name still has an error).A second question is if the contract has specified a pre-condition(e.g.
!ptr.is_null()), does that mean in the harness we don't need to make the assumption thatxptris not null? In other words, theensuresclause acts like anassumestatement?feliperodri commentedon Sep 13, 2024
Hi, @QinyuanWu! We should keep all communication about this challenge in the specific GitHub issue referenced in the book. #53 is the corresponding issue for challenge 6. I'll close this one and we can continue the discussion there.