Repository navigation
__rdl_dealloc / __rdl_realloc contracts don't require ptr to come from the allocator #712
Description
The contracts on alloc::__default_lib_allocator::__rdl_dealloc and __rdl_realloc (library/std/src/alloc.rs) only require align.is_power_of_two(). Their actual safety condition is that ptr was allocated by this allocator with the given layout, and that isn't encoded.
Why it surfaced now: until recently autoharness skipped both ("Missing Arbitrary implementation for argument(s) ptr: *mut u8"), so they were never verified. Kani main can generate arbitrary raw pointers, so on #687 autoharness checks them for the first time. An arbitrary pointer then reaches libc::free / libc::realloc:
Failed Checks: free argument must be dynamic object (std/src/sys/alloc/unix.rs, line 65, in dealloc)
Failed Checks: free argument has offset zero
Failed Checks: realloc argument is dynamic object (std/src/sys/alloc/unix.rs, line 71, in realloc)
#687 excludes both from the autoharness job so it keeps their previous status (unverified). To re-enable them, the contracts need a precondition saying ptr came from this allocator, e.g. in terms of Kani's memory predicates (a live heap object at offset 0 whose size matches size), and then the exclusion can go.
Activity
Drop the allocator and Unicode conversion functions from autoharness …
feliperodri commentedon Oct 5, 2026
@Tianshu-Huang let's take a look at this issue as well.
Tianshu-Huang commentedon Oct 5, 2026
Just looked into this. Two separate things are missing.
First, there is no word for it in a contract. The public memory predicates can only say "readable", "writable" or "same allocation". None of them can say "this is a heap object at offset 0 of size N". CBMC has the primitives and Kani already binds them (dynamic_object, pointer_offset, object_size), they are just not exposed. Same gap behind model-checking/kani#3864.
Second, autoharness only generates raw pointers into a stack local of the harness. None of them is a heap object, so even with the right precondition the harness for __rdl_dealloc itself would still fail in free.
Two ways to go:
A. Fix it in Kani. Add kani::mem::can_free(ptr, size) from those three primitives, following the pointer_offset hook. Then let autoharness back a raw pointer with heap memory when the precondition asks for it. Once both land, write the contracts with can_free and drop the exclusion. I can take the predicate; the autoharness part I'd open an issue for first.
B. Hand-written harness here. Allocate with __rdl_alloc, then call __rdl_dealloc / __rdl_realloc on that pointer. Needs no Kani change, but the contracts stay as they are and the exclusion stays.
I think A is worth doing even though only two functions are blocked today. These two contracts are what every deallocation in alloc (Vec, Box, Rc, Arc, BTree) is checked against under -Z function-contracts, and right now they accept any pointer, so the callers are being checked against a precondition that is too weak. And "I own this heap block and may free it" is a precondition that shows up in any Rust code managing memory through raw pointers, not just here, so the predicate is useful well beyond std. The predicate itself is a small change; the autoharness half is the bigger one.
Which do you prefer?