Repository navigation
Challenge 3: Verifying Raw Pointer Arithmetic Operations #76
Description
Activity
Here’s Kai from CMU III. We’re taking on this challenge and will keep you updated on our progress along the way.
Reacted by rahulkuProblem 1: Defining Valid Input Space for Pointer Parameters (solved)
Challenge:
Our main challenge in writing function contracts is precisely defining the valid input space for pointer parameters. Specifically, we are struggling to express accurate kani::requires attributes for pointer parameters in the functions we need to verify.
For non-pointer inputs like
u64, defining the valid input space is straightforward. For example, in thegcd(x, y)function, the valid input space can be represented by a precondition like#[kani::requires(x != 0 && y != 0)].However, for pointer parameters, defining the valid input space is non-trivial. We need a way to exclude invalid pointers (such as dangling, misaligned, or out-of-bounds pointers) while covering all valid ones to ensure the function contract remains sound. The challenge lies in expressing these conditions using kani::requires attributes.So far, we haven’t found a feasible solution or a Kani API that directly addresses this problem. Could you provide guidance on how we can define preconditions for pointer parameters in our function contracts?
Answer:
There’s an API called can_dereference that can be used for this purpose: can_dereference API
You can see an example of its usage in this test: valid_ptr.rsProblem 2: Handling Undefined Behavior in Function Verification (solved)
Challenge:
We are also encountering an issue related to undefined behavior (UB) in the verification of pointer arithmetic functions, such as
*const T::offset. If the function contains potential safety issues, such as valid inputs that trigger UB, Kani (as documented here: Kani undefined behavior documentation) cannot perform checks once UB occurs. This creates a dilemma: we need to verify whether the function may cause UB, but Kani’s checks become ineffective in the presence of UB. Could you advise on how we can approach this situation?Answer:
Kani automatically checks for certain types of UB (e.g. a dereference operation is valid), and verification will fail if one of those types of UB were found in a function. For other properties, such as this one mentioned in the documentation of offset:
the entire memory range between self and the result must be in bounds of that allocated object.
One needs to express this property as a requires clause that the function is annotated with.
Problem 3: Determining the valid value range for
*const T::offset(self, count: i32)'scountparameterTo write a function contract for this function, we need to add a precondition that defines the valid input range for the
countparameter. However, we cannot infer this information solely based on the input pointer. For example, consider the following pointers:let nums = vec![0i32, 1, 2, 3]; let n = 42; let ptr1: *const i32 = nums.as_ptr(); let ptr2: *const i32 = ptr1.wrapping_offset(1); let ptr3: *const i32 = &n;
All of these pointers are of type
*const i32—the only information we know when inside the offset function. However, when we call the.offset(count)method on them, the valid range ofcountdiffers for each pointer. Thus, it becomes unclear how to properly write thekani::requiresattribute for thecountparameter.Is there a way to resolve this issue?
Problem 4: determing whether two raw pointers point to the same object during runtime
To implement function contracts for
*const T::offset_from(self, origin: *const T), we need to guarantee that bothselfandoriginpoint to the same allocated object. Is there any way to access and compare the provenance information of these raw pointers to guarantee that they belong to the same object?@feliperodri , the other two people working on this issue are @stogaru and @MayureshJoshi25.
Mayuresh here! Would be working on this challenge and would report any problems/doubts on the way.
Problem 5: Calling Pointer Arithmetic Methods on
dyn TraitPointersCalling pointer arithmetic methods, such as
addorsub, requires the pointee type to be sized. However,dyn Traitobjects are inherently unsized, resulting in a compile-time error when attempting to call these methods on a pointer to adyn Trait. For example:struct ConcreteType { size: i32, } trait AbstractTrait {} impl AbstractTrait for ConcreteType {} fn get_box(size: i32) -> Box<dyn AbstractTrait> { Box::new(ConcreteType { size }) } fn test() { let rand_box = get_box(42); let ptr = Box::into_raw(rand_box); unsafe { let ptr1 = ptr.offset(0); } // error }
In our challenge, we need to verify function contracts for at least one
dyn Traittype, but we are blocked by this issue. Is there a workaround for handling this scenario?Reacted by szlee118Problem 6: Precondition
#[requires(kani::mem::can_dereference(self))]Fails on function<*mut T>::byte_addIssue:
When adding the precondition#[requires(kani::mem::can_dereference(self))]to the functionbyte_add(pub const unsafe fn byte_add(self, count: usize) -> Self), running Kani produces the following error:error[E0277]: the trait bound `<T as ptr::metadata::Pointee>::Metadata: kani::mem::PtrProperties<T>` is not satisfied --> /Users/xsxsz/vscode-projects/verify-rust-std/library/core/src/ptr/mut_ptr.rs:440:43 | 440 | #[requires(kani::mem::can_dereference(self))] | -------------------------- ^^^^ the trait `kani::mem::PtrProperties<T>` is not implemented for `<T as ptr::metadata::Pointee>::Metadata` | | | required by a bound introduced by this call | note: required by a bound in `kani::mem::can_dereference` --> /Users/xsxsz/vscode-projects/verify-rust-std/library/core/src/lib.rs:426:1 | 426 | kani_core::kani_lib!(core); | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | | | required by a bound in this function | required by this bound in `can_dereference` = note: this error originates in the macro `kani_core::kani_mem` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info) help: consider further restricting the associated type | 444 | pub const unsafe fn byte_offset(self, count: isize) -> Self where <T as ptr::metadata::Pointee>::Metadata: kani::mem::PtrProperties<T> { | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ error: aborting due to 1 previous error
Context:
This precondition works for other non-byte pointer methods includingadd,sub,offset, andoffset_from. However, it consistently fails with the same error on all byte-prefixed functions, includingbyte_add,byte_sub,byte_offset, andbyte_offset_from. Additionally, this behavior is consistent on bothconstandmutpointer methods.We are currently using a custom-built version of Kani from the
features/verify-rust-stdbranch, not the stable release. This branch is necessary for us as it enables verification on primitive types.Question:
Is this issue a bug of the branch we are using, or is it a feature that has yet to be implemented in Kani? We're uncertain if this behavior is a bug or an expected result.Hi @feliperodri, after contacting with Team 4, we have a few updates on the issues we've been discussing in today's (Oct. 11) meeting:
- For Problem 3 and 4, We’ve confirmed that Zyad, Team 4’s POC, is already working on new Kani APIs to address these issues.
- Regarding the new problem mentioned in today’s meeting: We initially discovered this problem during our joint meeting with Team 4 on Oct. 9, and they have received clarification during their sponsor meeting, so we don't need to post a new Problem here. Specifically, a pointer that points one byte past the end of its allocated object is still valid, but cannot be dereferenced. For example,
vec.as_ptr().add(vec.len())is a valid pointer, but dereferencing it would result in undefined behavior.
Reacted by szlee118It is not possible to verify
offset,offset_from,addandsubfor the following dynamically sized types:slicesdyn Traits
Function signatures:
Observe that the
Tneeds to sized for all pointers*mut Tor*const Tinvoking these functions as per the function signatures.add:
pub const unsafe fn add(self, count: usize) -> Self where T: Sized
The same applies for
sub,offsetandoffset_from.Invoking above methods:
Slices
Code:
fn main() { let arr = [1, 2, 3, 4, 5]; let slice = &arr[..]; let slice_ptr: *const [u32] = slice.as_ptr() as *const [u32]; let new_slice_ptr: *const [u32] = unsafe { slice_ptr.offset(1) }; }
Error as expected:
Compiling playground v0.0.1 (/playground) error[E0277]: the size for values of type `[u32]` cannot be known at compilation time --> src/main.rs:29:58 | 29 | let new_slice_ptr: *const [u32] = unsafe { slice_ptr.offset(1) }; | ^^^^^^ doesn't have a size known at compile-time | = help: the trait `Sized` is not implemented for `[u32]` note: required by a bound in `std::ptr::const_ptr::<impl *const T>::offset` --> /playground/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:393:12 | 391 | pub const unsafe fn offset(self, count: isize) -> *const T | ------ required by a bound in this associated function 392 | where 393 | T: Sized, | ^^^^^ required by this bound in `std::ptr::const_ptr::<impl *const T>::offset`dyn Traits
Code:
trait Greet { fn greet(&self); } struct Person { name: &'static str, } impl Greet for Person { fn greet(&self) { println!("Hello, my name is {}!", self.name); } } fn main() { let person = Person { name: "Alice" }; let greet_ptr: *const dyn Greet = &person as *const dyn Greet; unsafe { greet_ptr.offset(1); } }
Error as expected:
error[E0277]: the size for values of type `dyn Greet` cannot be known at compilation time --> src/main.rs:19:19 | 19 | greet_ptr.offset(1); | ^^^^^^ doesn't have a size known at compile-time | = help: the trait `Sized` is not implemented for `dyn Greet` note: required by a bound in `std::ptr::const_ptr::<impl *const T>::offset` --> /playground/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:393:12 | 391 | pub const unsafe fn offset(self, count: isize) -> *const T | ------ required by a bound in this associated function 392 | where 393 | T: Sized, | ^^^^^ required by this bound in `std::ptr::const_ptr::<impl *const T>::offset`- added a commit that references this issue
on Dec 3, 2024 - added a commit that references this issue
on Dec 5, 2024 - added a commit that references this issue
on Dec 12, 2024
Tracking issue for Challenge 3: Verifying Raw Pointer Arithmetic Operations.