Reasoning about ZST addresses

[nishanthkarthik]

I assumed ZST addresses are dangling, so they may or may not be equal for different instances of a type.

I tried this code:

#[repr(C)]
#[derive(Copy, Clone)]
struct Z(i8, i64);

struct Y;

#[kani::proof]
fn test_z() -> Z {
	let m = Y;
	let n = Y;
	let zz = Z(1, -1);
	
	let ptr: *const Z = if &n as *const _ == &m as *const _ {
		std::ptr::null()
	} else {
		&zz
	};
	unsafe{ *ptr }
}

using the following command line invocation:

kani main.rs

with Kani version: 0.48.0

I expected to see this happen: An error because addresses to ZSTs are not guaranteed to have distinct addresses at runtime. Running this snippet crashes playground

Instead, this happened:

...
SUMMARY:
 ** 0 of 7 failed

VERIFICATION:- SUCCESSFUL

Thanks!

[tautschnig]

Thank you very much for your report. We will investigate how to fix this in Kani (CBMC as the underlying verification engine assumes that each object has a unique address), but ZST objects are a Rust peculiarity.

[nishanthkarthik]

Thank you. Is there an easy way to see how a rust snippet is converted to a CBMC input file? I looked for something like kani --keep-temporary-files but I did not find any.

[tautschnig]

You'll want kani --verbose --keep-temps -- the latter keeps the temporary files, and the --verbose will tell you the exact commands that were invoked on those files.

[celinval]

Hi @nishanthkarthik, I am not sure this assumption holds, do you have any reference on this?

AFAIK, a pointer to a ZST is still a thin pointer (at least for now, there has been discussions to change that). So I believe thin pointer comparison rules still apply to them (which are also not well defined).

The main difference when it comes to ZST pointers is that a ZST access is valid even for dangling points (rust-lang/unsafe-code-guidelines#472).

There is one interesting thing though that it is worth mentioning, you do have to be careful when it comes to relying on address values in Kani. They do translate to concrete values, and each allocation will always have its unique value, even if their lifetime do not overlap.

[celinval]

BTW, I ran your test case, and it also succeeds in MIRI, since there is no UB and each local variable is considered a different allocation.

[nishanthkarthik]

I did not find a source that said pointers to different ZST objects are guaranteed to be distinct, so I assumed they would be havoc'd by default and consequently a program trace may set ptr to null.

Is comparing pointers of ZSTs UB (or just valid but unspecified behavior)?

[adpaco-aws]

Hi @nishanthkarthik , just wanted to let you know that @celinval and @tautschnig have been trying to get some clarity on guarantees over ZST pointers in rust-lang/unsafe-code-guidelines#503 . Please feel free to join the discussion if you have more questions yourself.