Do not assume that ZST-typed symbols refer to unique objects

[tautschnig]

The Rust specification does not guarantee that ZST-typed symbols are backed by unique objects, and rustc appears to make use of this as can be demonstrated for both locals and statics. For parameters no such example has been found, but as there remains a lack of a guarantee we err on the safe side.

Resolves: #3129

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

[celinval]

Can you please confirm that is really the case and paste a reference here?

[tautschnig]

Can you please confirm that is really the case and paste a reference here?

Not exactly a "reference", but still a very extensive discussion including pointers to the actual implementation (yes, this is all about the implementation of the Rust compiler, nothing here is specified in the documentation): https://stackoverflow.com/questions/58529934/why-do-zero-sized-types-cause-real-allocations-in-some-cases

[celinval]

Thanks @tautschnig for working on this, but I really think we should ask the Rust team (maybe create an issue in https://github.com/rust-lang/unsafe-code-guidelines) about what guarantees we should expect when it comes to comparing two raw pointers to ZST objects.

I always find that searching for ZST related issues and guarantees is a rabbit hole. Just from my latest search:

• Iterators over slices of ZST behave strange rust-lang/rust#42789: This is a case where exact address is expected due to pointer identity.
• When are things guaranteed to have unique addresses? rust-lang/unsafe-code-guidelines#206: This issues does mention ZST a bit, and it seems that the address of a ZST may be the same as anything including a non-ZST.
• https://users.rust-lang.org/t/addresses-of-zsts/64106: When taking the address of a ZST field, the address is still expected to be in bounds of the struct.

[celinval]

Ok, I gave this a thought, and I think the correct solution would be to add a UB check if users try to compare two ZST pointers.

My reasoning is:

1. We shouldn't try to model UB. Any code following an UB is incorrect.
2. Accessing ZST pointers is a well defined operation. There's no need to change that.

[tautschnig]

Why should we add a UB check? Comparing any two (raw) pointers is explicitly permitted in Rust as far as I can tell?!

Edit:

Accessing ZST pointers is a well defined operation. There's no need to change that.

1. I am not sure whether accessing ZSTs already is a well defined operation. To me, Tracking Issue for allowing zero-sized memory accesses and offsets rust-lang/rust#117945 suggests that this is still in the making.
2. This PR does not actually change anything about the well-definedness of using ZST pointers in Kani.

[tautschnig]

Can you please confirm that is really the case and paste a reference here?

Not exactly a "reference", but still a very extensive discussion including pointers to the actual implementation (yes, this is all about the implementation of the Rust compiler, nothing here is specified in the documentation): https://stackoverflow.com/questions/58529934/why-do-zero-sized-types-cause-real-allocations-in-some-cases

A further note: the implementation pointed to in the above SO-post (rust-lang/rust#63635) continued to exist until rust-lang/rust#111768. It does seem, however, that at that point from_const_alloc wasn't actually used anymore (outside the SSA back-end). So I don't know how this really works in the compiler.

[celinval]

I created rust-lang/unsafe-code-guidelines#503 to hopefully get some answers to these questions.

[tautschnig]

I created rust-lang/unsafe-code-guidelines#503 to hopefully get some answers to these questions.

Thank you!!! Given their answers, my interpretation is that we should not do the parameter-specific piece and will instead have to modify the Closure/zst_param.rs test, because the non-equality asserted in there is not actually guaranteed.

[tautschnig]

I created rust-lang/unsafe-code-guidelines#503 to hopefully get some answers to these questions.

Thank you!!! Given their answers, my interpretation is that we should not do the parameter-specific piece and will instead have to modify the Closure/zst_param.rs test, because the non-equality asserted in there is not actually guaranteed.

I have now updated the implementation to the above effect.

[celinval]

The current fix will work for the exact issue at hand, but the following will still always evaluate to false, even though it could be true:

let a1 = &() as *const _;
let a2 = &() as *const _;
let a3 = &() as *const _;
let a4 = &() as *const _;
cover!(a1 == a2 && a3 == a4 && a1 != a3);

So to make this really sound, you need to set all addresses to be any non-null + aligned address value.

[tautschnig]

[...]

So to make this really sound, you need to set all addresses to be any non-null + aligned address value.

Hmm, yes, but still those also need to be addresses such that dereferencing pointers with such addresses also works. The following might work:

1. Create a global scope array of infinite size.
2. Each ZST "object" is just a non-deterministic index into to this array.

A problem, however, will arise when lifetimes of ZST objects are required to be honoured. Then we'd have to reference-count each entry in this array, which seems like unreasonable overhead.

[celinval]

Hmm, yes, but still those also need to be addresses such that dereferencing pointers with such addresses also works. The following might work:

De-referencing a ZST dangling pointer is considered valid in Rust since it is a no-op. So as long as the pointer is aligned, there should be no problem. I believe Kani also treats that as a no-op, i.e., it does not emit a de-reference instruction. I don't think we will be able to track ZST lifetimes until we have a different mechanism to handle provenance.

[celinval]

Which means that Kani cannot detect invalid ZST access due to deallocation. This is a limitation that should be documented, if you don't mind.

[tautschnig]

Summary of a discussion that @celinval and I had:

1. Given that Kani does not emit dereference instructions for ZSTs we should actually be fine when we just produce a nondet value for an address-of.
2. The constraints on that (numeric) nondet value should just be that it must not be 0 (to not produce a null pointer) and that casting to a pointer must result in an aligned address.
3. We can read the alignment from the type.
4. Taking these together, we will produce a statement expression that first creates a numeric nondet value, then assumes it is not zero, then assumes that the value modulo alignment equals zero, and finally casts to the desired pointer type.
5. We should confirm that CBMC simplifies modulo-1 (we believe the alignment will typically be 1) to zero. Edit: simplify_exprt::simplify_mod takes care of this.

6. kani/library/kani/src/mem.rs

   Lines 74 to 76 in ec34e01

   	if metadata.dangling(marker) as *const _ == data_ptr {
   	crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access")
   	} else {

   should be adjusted so as to just assert when sz != 0.

[celinval]

For 5, we should change the if to be:

if sz == 0 {
    true
} else {
    // invoke read ok
}

[celinval]

@tautschnig any updates?

[tautschnig]

@tautschnig any updates?

I have now pushed my update, but I am yet to understand why mem::tests::test_dangling_char and mem::tests::test_dangling_slice are now failing (or, rather, how to debug those tests as they are now reported to be running forever).

[celinval]

@tautschnig any updates?

I have now pushed my update, but I am yet to understand why mem::tests::test_dangling_char and mem::tests::test_dangling_slice are now failing (or, rather, how to debug those tests as they are now reported to be running forever).

Those tests used to exercise a path that no longer exists. With the new implementation, non-zst dangling pointers will reach the Kani intrinsic, which in regular tests is a loop.

I.e., we are no longer able to test those two cases with concrete tests, and they should be removed.

[tautschnig]

[...]

Those tests used to exercise a path that no longer exists. With the new implementation, non-zst dangling pointers will reach the Kani intrinsic, which in regular tests is a loop.

I.e., we are no longer able to test those two cases with concrete tests, and they should be removed.

Thanks, now done.

[celinval]

Can you please take a look at the s2n-quic test that regressed?

Everything else looks good!

[tautschnig]

Can you please take a look at the s2n-quic test that regressed?

I have now locally re-run this test multiple times both with current main and this branch/PR: the time spent to run cargo kani --harness inet::checksum::tests::differential (after running once to have the crate built) is always in the range of 178 to 183 seconds. Given this test has very high memory usage (see #3030), it is not too surprising that we are seeing high fluctuations on GitHub runners (where the memory usage is very close to the maximum available memory). But I don't think this PR actually has a meaningful impact on that fluctuation.