Use of Layout,alloc and dealloc to create and free dynamic arrays

[QinyuanWu]

In our discussion with @zhassan-aws, we are trying to use core::Layout to dynamically allocate an array with size:usize = kani::any() instead of initializing a large fixed size built-in array in the proofs so that we can cover all possible array sizes. We followed this example and have the following harness:

    use crate::alloc::{self, Layout}; // use crate::alloc::{Layout, alloc, dealloc} result in error saying alloc and dealloc are not found

    // pub const unsafe fn add(self, count: usize) -> Self
    #[kani::proof_for_contract(NonNull::add)]
    pub fn non_null_check_add() {
        let size: usize = kani::any();
        let layout = Layout::array::<i8>(size).unwrap();
        let raw_ptr = unsafe { alloc(self, layout) as *mut i8 };

        // NonNull pointer to the random offset
        let ptr = unsafe { NonNull::new(raw_ptr).unwrap()};  
        // Create a non-deterministic count value
        let count: usize = kani::any();  

        // Workaround: SAFETY: Ensure that the pointer operation does not go out of the bounds of the array
        kani::assume(count < size);

        unsafe {
            // Add a positive offset to pointer
            let result = ptr.add(count);
            dealloc(self, raw_ptr as *mut u8, layout);
        }
    }

But received the following compilation error starting with:

Kani Rust Verifier 0.55.0 (standalone)
error[E0773]: attempted to define built-in macro more than once
    --> /rustc/bd53aa3bf7a24a70d763182303bd75e5fc51a9af/library/core/src/macros/mod.rs:1468:5
     |
note: previously defined here
    --> core/src/macros/mod.rs:1468:5
     |
1468 | /     macro_rules! cfg {
1469 | |         ($($cfg:tt)*) => {
1470 | |             /* compiler built-in */
1471 | |         };
1472 | |     }
     | |_____^

 ......
 
 error[E0423]: expected function, found module `alloc`
    --> core/src/ptr/non_null.rs:1858:32
     |
1858 |         let raw_ptr = unsafe { alloc(layout) as *mut i8 };
     |                                ^^^^^ not a function

error[E0425]: cannot find function `dealloc` in this scope
    --> core/src/ptr/non_null.rs:1872:13
     |
1872 |             dealloc(raw_ptr as *mut u8, layout);
     |             ^^^^^^^ not found in this scope

......(a bunch of multiple applicable items in scope error)

Appreciate any suggestion on how to potentially resolve these errors. Thanks!

[celinval]

Hi @QinyuanWu, since the code you are trying to verify (NonNull) is part of the core crate, you cannot use dynamic allocation. In this case, I would recommend that you use a fixed array size, and an index variable with non-deterministic value that is less than length to cover different scenarios.

Another possibility is to use the new PointerGenerator that we recently added to Kani.

[zhassan-aws]

@QinyuanWu my bad.

@celinval my suggestion to use Layout was because they were running into some performance scaling issues when using an array, so I thought CBMC might work better with a plain memory allocation. Looks like we'll have to stick to using an array.