Reasoning about ZST addresses about kani HOT 7 CLOSED

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.

from kani.

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.

from kani.

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.

from kani.

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.

from kani.

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.

from kani.

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.

from kani.

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)?

from kani.