Verifying methods of `<*const T>` #92

stogaru · 2024-09-20T23:45:54Z

Changes made:

Adds the function contracts and proof for the const offset function.

Problems :

What should be the valid input range for the count argument as asked here? How will we know the start address and the length of the allocated object from a raw pointer?

Works toward resolving #76

By submitting this pull request, we confirm that our contribution is made under the terms of the Apache 2.0 and MIT licenses.

Refactors by removing unused crates and importing safety crate

stogaru · 2024-09-20T23:48:53Z

library/core/src/ptr/const_ptr.rs

@@ -388,6 +400,10 @@ impl<T: ?Sized> *const T {
    #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
    #[inline(always)]
    #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(kani::mem::can_dereference(self))]
+    // TODO: Determine the valid value range for 'count' and update the precondition accordingly.
+    #[requires(count == 0)] // This precondition is currently a placeholder.


This precondition needs to be changed based on the valid input range agreed.

Could you elaborate more? Is there a GitHub issue to link here? What does the documentation say? How can we "determine the valid value range for count"?

Problem 3 in the issue here gives some details. We need to add a precondition that defines the valid input range for the count parameter. This is because the offset guarantees the safety of the resulting pointer only when the self and the result are in bounds of that allocated object.
Therefore, count should be bounded such that self.addr() +/- count is within the start and end addresses of the allocated object. However, we cannot infer the start and end addresses of the allocated object solely based on the input pointer. How can we overcome this?

feliperodri · 2024-09-27T17:30:23Z

library/core/src/ptr/const_ptr.rs

+        if self.is_null() {
+            None
+        } else {
+            unsafe { Some(&*self) }
+        }


Why is the format change necessary?

It was a side-effect of running cargo fmt. I'll remove it.

feliperodri · 2024-09-27T17:31:24Z

library/core/src/ptr/const_ptr.rs

+mod verify {
+    use crate::kani;
+
+    #[allow(unused)]
+    #[kani::proof_for_contract(<*const i32>::offset)]
+    fn check_offset_i32() {
+        let mut test_val: i32 = kani::any();
+        let test_ptr: *const i32 = &test_val;
+        let offset: isize = kani::any();
+        unsafe { test_ptr.offset(offset) };
+    }
+}


We can expand this to other types. Please, see my comment here for clarity.

Thank you! We will implement that for other types.

feliperodri · 2024-09-27T17:31:49Z

library/core/src/ptr/const_ptr.rs

+// This module contains all proof harnesses for function contracts.
+// Each proof harness verifies the soundness of a function contract for a specific type.


This comment is unnecessary, you can remove it.

feliperodri · 2024-09-27T17:32:50Z

library/core/src/ptr/const_ptr.rs

@@ -388,6 +400,10 @@ impl<T: ?Sized> *const T {
    #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
    #[inline(always)]
    #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(kani::mem::can_dereference(self))]
+    // TODO: Determine the valid value range for 'count' and update the precondition accordingly.
+    #[requires(count == 0)] // This precondition is currently a placeholder.


Could you elaborate more? Is there a GitHub issue to link here? What does the documentation say? How can we "determine the valid value range for count"?

Verify/ptr const integer types

Adds proofs for composite type - tuple

Verify/ptr const slice type

feliperodri · 2024-10-05T22:43:44Z

library/core/src/ptr/const_ptr.rs

+     macro_rules! generate_add_harness {
+        ($type:ty, $proof_name:ident) => {
+            #[allow(unused)]
+            #[kani::proof_for_contract(<*const $type>::add)]
+            pub fn $proof_name() {
+                let mut test_val: $type = kani::any::<$type>();
+                let test_ptr: *const $type = &test_val;
+                let count: usize = kani::any();
+                unsafe {
+                    test_ptr.add(count);
+                }
+            }
+        };
+    }
+
+    generate_add_harness!(i8, check_add_i8);
+    generate_add_harness!(i16, check_add_i16);
+    generate_add_harness!(i32, check_add_i32);
+    generate_add_harness!(i64, check_add_i64);
+    generate_add_harness!(i128, check_add_i128);
+    generate_add_harness!(isize, check_add_isize);
+    generate_add_harness!(u8, check_add_u8);
+    generate_add_harness!(u16, check_add_u16);
+    generate_add_harness!(u32, check_add_u32);
+    generate_add_harness!(u64, check_add_u64);
+    generate_add_harness!(u128, check_add_u128);
+    generate_add_harness!(usize, check_add_usize);
+    generate_add_harness!((i8, i8), check_add_tuple_1);
+    generate_add_harness!((f64, bool), check_add_tuple_2);
+    generate_add_harness!((i32, f64, bool), check_add_tuple_3);
+    generate_add_harness!((i8, u16, i32, u64, isize), check_add_tuple_4);
+    // fn <*const T>::add verification end
+
+    // fn <*const T>::sub verification begin
+    macro_rules! generate_sub_harness {
+        ($type:ty, $proof_name:ident) => {
+            #[allow(unused)]
+            #[kani::proof_for_contract(<*const $type>::sub)]
+            pub fn $proof_name() {
+                let mut test_val: $type = kani::any::<$type>();
+                let test_ptr: *const $type = &test_val;
+                let count: usize = kani::any();
+                unsafe {
+                    test_ptr.sub(count);
+                }
+            }
+        };
+    }
+
+    generate_sub_harness!(i8, check_sub_i8);
+    generate_sub_harness!(i16, check_sub_i16);
+    generate_sub_harness!(i32, check_sub_i32);
+    generate_sub_harness!(i64, check_sub_i64);
+    generate_sub_harness!(i128, check_sub_i128);
+    generate_sub_harness!(isize, check_sub_isize);
+    generate_sub_harness!(u8, check_sub_u8);
+    generate_sub_harness!(u16, check_sub_u16);
+    generate_sub_harness!(u32, check_sub_u32);
+    generate_sub_harness!(u64, check_sub_u64);
+    generate_sub_harness!(u128, check_sub_u128);
+    generate_sub_harness!(usize, check_sub_usize);
+    generate_sub_harness!((i8, i8), check_sub_tuple_1);
+    generate_sub_harness!((f64, bool), check_sub_tuple_2);
+    generate_sub_harness!((i32, f64, bool), check_sub_tuple_3);
+    generate_sub_harness!((i8, u16, i32, u64, isize), check_sub_tuple_4);
+    // fn <*const T>::sub verification end
+
+    // fn <*const T>::offset verification begin
+    macro_rules! generate_offset_harness {
+        ($type:ty, $proof_name:ident) => {
+            #[allow(unused)]
+            #[kani::proof_for_contract(<*const $type>::offset)]
+            pub fn $proof_name() {
+                let mut test_val: $type = kani::any::<$type>();
+                let test_ptr: *const $type = &test_val;
+                let count: isize = kani::any();
+                unsafe {
+                    test_ptr.offset(count);
+                }
+            }
+        };
+    }
+
+    generate_offset_harness!(i8, check_offset_i8);
+    generate_offset_harness!(i16, check_offset_i16);
+    generate_offset_harness!(i32, check_offset_i32);
+    generate_offset_harness!(i64, check_offset_i64);
+    generate_offset_harness!(i128, check_offset_i128);
+    generate_offset_harness!(isize, check_offset_isize);
+    generate_offset_harness!(u8, check_offset_u8);
+    generate_offset_harness!(u16, check_offset_u16);
+    generate_offset_harness!(u32, check_offset_u32);
+    generate_offset_harness!(u64, check_offset_u64);
+    generate_offset_harness!(u128, check_offset_u128);
+    generate_offset_harness!(usize, check_offset_usize);
+    generate_offset_harness!((i8, i8), check_offset_tuple_1);
+    generate_offset_harness!((f64, bool), check_offset_tuple_2);
+    generate_offset_harness!((i32, f64, bool), check_offset_tuple_3);
+    generate_offset_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4);
+    // fn <*const T>::offset verification end


Comments should go at the top of each code block. Also, you can consolidate all three macros into a single declarative macro using a parameter to specify the type of pointer operation (i.e., add, sub, or offset).

Would update in the next PR.

feliperodri · 2024-10-05T22:43:57Z

library/core/src/ptr/const_ptr.rs

+mod verify {
+    use crate::kani;
+
+    #[allow(unused)]


Why is this necessary?

#[allow(unused)] was added to suppress unused code warnings during development, but it's not necessary anymore. We'll remove it to ensure we catch any unused code warnings.

feliperodri · 2024-10-05T22:47:10Z

library/core/src/ptr/const_ptr.rs

+    #[kani::proof_for_contract(<*const i32>::offset)]
+    fn check_offset_slice_i32(){
+        let mut arr: [i32; 5] = kani::any();
+        let test_ptr: *const i32 = arr.as_ptr();
+        let offset: isize = kani::any();
+
+        unsafe{
+            let new_ptr = test_ptr.offset(offset);
+        }
+    }
+
+    #[kani::proof_for_contract(<*const i32>::add)]
+    fn check_add_slice_i32() {
+        let mut arr: [i32; 5] = kani::any();
+        let test_ptr: *const i32 = arr.as_ptr();
+        let count: usize = kani::any();
+        unsafe {
+            let new_ptr = test_ptr.add(count);
+        }
+    }
+
+
+    #[kani::proof_for_contract(<*const i32>::sub)]
+    fn check_sub_slice_i32() {
+        let mut arr: [i32; 5] = kani::any();
+        let test_ptr: *const i32 = arr.as_ptr();
+        let count: usize = kani::any();
+        unsafe {
+            let new_ptr = test_ptr.sub(count);
+        }
+    }


Would this be extended to different types or only i32? We can avoid code repeition using a macro here as well.

Why are we picking 5 for the length of the array? We need to add documentation for any magical numbers.

Have you tried to use here kani::any_array?

Yes it could be extended to different type, here it is following the minimum requirement in challenge 3.

Since the length of array must be defined, I was following the test 1

kani::any_array() would still need to define the size of array, by referring to test2. However, I would use it in the next PR.

szlee118 and others added 6 commits September 12, 2024 18:34

Add verification contract for *const T::add and *const T::add

500f249

Update const_ptr.rs

99701ff

Merge branch 'model-checking:main' into test

31c82a9

Changes generic type to i32 in proof.

f84b7a6

Refactors by removing unused crates and importing safety crate

Remove unneeded file

a839820

added comments for function contracts and harnesses

21e0ab8

stogaru requested a review from a team as a code owner September 20, 2024 23:45

stogaru commented Sep 20, 2024

View reviewed changes

Merge branch 'main' into verify/ptr_const_offset

b54ce9e

feliperodri changed the title ~~AWS Team 3: Verifying <*const T>::offset~~ Verifying <*const T>::offset Sep 27, 2024

feliperodri changed the title ~~Verifying <*const T>::offset~~ Verifying <*const T>::offset Sep 27, 2024

feliperodri requested changes Sep 27, 2024

View reviewed changes

feliperodri assigned stogaru Sep 27, 2024

xsxszab and others added 17 commits September 30, 2024 15:29

reverted library code format change and removed unnecessary comments

0c0078f

added macros for verifying all integer types for offset and add

a192129

implemented function contract and integer type proofs for fn sub

2ef5923

Add verification of slice type proofs for fn offset

f1602aa

add TODOs for proof for contracts

1b467d5

verified *mut T::offset for all integer types

9461027

Add verification of slice type proofs for fn add and sub

159137b

Remove commented code

df56d18

removed unnecessary comments

eab0a15

reverted changes to mut_ptr.rs

e07040f

removed necessary comments

0ff52b5

aligned format for mut_ptr.rs

ccd5c3c

aligned format for mut_ptr.rs

180a276

Merge pull request #1 from stogaru/verify/ptr_const_integer_types

6a85e3e

Verify/ptr const integer types

Merge branch 'model-checking:main' into verify/ptr_const_offset

6853284

Adds proofs for composite type - tuple

fb79caf

Change function proof names

7d05c96

stogaru and others added 3 commits October 2, 2024 18:43

Merge pull request #2 from stogaru/verify/ptr_const_composite

8e49dcd

Adds proofs for composite type - tuple

Merge branch 'verify/ptr_const_offset' into verify/ptr_const_slice_type

9af0e39

Merge pull request #4 from stogaru/verify/ptr_const_slice_type

31532c9

Verify/ptr const slice type

stogaru changed the title ~~Verifying <*const T>::offset~~ Verifying methods of <*const T> Oct 4, 2024

feliperodri requested changes Oct 5, 2024

View reviewed changes

stogaru closed this Oct 7, 2024

stogaru deleted the verify/ptr_const_offset branch October 7, 2024 20:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Verifying methods of `<*const T>` #92

Verifying methods of `<*const T>` #92

stogaru commented Sep 20, 2024 •

edited

Loading

stogaru Sep 20, 2024

feliperodri Sep 27, 2024

stogaru Sep 27, 2024 •

edited

Loading

feliperodri Sep 27, 2024

stogaru Sep 27, 2024

feliperodri Sep 27, 2024

stogaru Sep 27, 2024

feliperodri Sep 27, 2024

feliperodri Sep 27, 2024

feliperodri Oct 5, 2024

szlee118 Oct 12, 2024

feliperodri Oct 5, 2024

szlee118 Oct 12, 2024

feliperodri Oct 5, 2024

szlee118 Oct 12, 2024

		// This module contains all proof harnesses for function contracts.
		// Each proof harness verifies the soundness of a function contract for a specific type.

Verifying methods of <*const T> #92

Verifying methods of <*const T> #92

Conversation

stogaru commented Sep 20, 2024 • edited Loading

Changes made:

Problems :

Choose a reason for hiding this comment

Choose a reason for hiding this comment

stogaru Sep 27, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Verifying methods of `<*const T>` #92

Verifying methods of `<*const T>` #92

stogaru commented Sep 20, 2024 •

edited

Loading

stogaru Sep 27, 2024 •

edited

Loading