additional transmute and transmute_unchecked harnesses #264
Conversation
|
Would be to happy hear your thoughts on this (@celinval, @feliperodri, or anyone else interested in this challenge). In particular, we would like to hear what you think about the completeness of part 1 of challenge 1 (i.e., is there anything major that Kani can do that isn't currently being verified here?). For our own thoughts on this, we refer to the above linked completeness document. Thank you! |
carolynzech
requested review from
tautschnig,
qinheping,
carolynzech and
thanhnguyen-aws
library/core/src/intrinsics/mod.rs
Outdated
| transmute_two_ways!(transmute_2ways_u64_to_i64, u64, i64); | ||
| transmute_two_ways!(transmute_2ways_i64_to_f64, i64, f64); | ||
| transmute_two_ways!(transmute_2ways_u64_to_f64, u64, f64); | ||
| //transmute 2-ways between arrays of bytes and numerical types |
There was a problem hiding this comment.
Shouldn't you also try some other data structures? Arguably, as also stated in your doc, you have no way to enumerate all possible types, but at least one harness where both "to" and "from" are not just numeric types would seem called for?
There was a problem hiding this comment.
Thanks for the feedback @tautschnig -- I've added a new commit that extends the cases handled by these 2-way harnesses. For harnesses where both the input and output are non-numerical, I didn't see a way to do that with the standard primitives, but the new harnesses for compound types would accomplish this (e.g., transmuting a tuple of chars to an array of chars).
|
The new commit adds some harnesses for transmute/transmute_unchecked. In particular, it adds "2-way" harnesses for additional primitives (including floats), as well as for references, pointers, and slices. It also introduces a macro that generates these 2-way harnesses between more complex types (currently arrays, tuples, and structs). As always, any feedback is greatly appreciated! I'm especially wondering if there are other properties we want to verify in this "part 1" (i.e., harnesses for the transmute intrinsics directly), or if it makes sense to do the rest of the verification at the part 2/3/4 level. In any case, thanks in advance! |
| //This tests that transmute does not mutate the bit patterns | ||
| //Note: this would not catch reversible mutations | ||
| //e.g., deterministically flipping a bit | ||
| //we then assert that the resulting value is equal to the initial value | ||
| macro_rules! transmute_unchecked_two_ways { | ||
| ($harness:ident, $src:ty, $dst:ty) => { | ||
| #[kani::proof_for_contract(transmute_unchecked_wrapper)] |
There was a problem hiding this comment.
This one should not be a proof_for_contract because it does not prove the contract of the transmute_unchecked_wrapper.
| transmute_unchecked_two_ways!(transmute_unchecked_2ways_i32_to_f32, i32, f32); | ||
| transmute_unchecked_two_ways!(transmute_unchecked_2ways_i32_to_char, i32, char); |
There was a problem hiding this comment.
The proof_for_contract attribute causes a problem here. The harness should panic here: let dst: $dst = unsafe { transmute_unchecked_wrapper(src) };, but it did not because the proof_for_contract replace the requires clause by an assume clause, which is not correct according to your contract.
There was a problem hiding this comment.
Thank you @thanhnguyen-aws for the review! For this point, I just had some questions.
The intended purpose of the two_ways harnesses is to check that transmute & transmute_unchecked don't mutate the bit patterns in any way, which we can only check if the input is valid for the output type (otherwise we have UB before reaching our assert), hence the need to assume the validity precondition. As for the cases where we transmute an input that is invalid for the output type (e.g., a u8 with value 3 into a bool), we don't have a harness that explicitly allows such a value to be transmuted, since this case just quietly causes UB without panicking anyways (unless there's some external flag like valid-value-checks). We could be missing something though -- do you think that it would be worthwhile to have separate harnesses that allow these invalid transmutes to go through nonetheless?
Also, I see what you mean about not using #[proof_for_contract] if we're not proving the contract. Would the best solution in that case be to rewrite transmute_unchecked_two_ways in a similar way to transmute_two_ways, where we have a #[kani::proof] and we just explicitly assume the validity precondition in the macro/harness? Or would you suggest another approach?
There was a problem hiding this comment.
Also, I see what you mean about not using #[proof_for_contract] if we're not proving the contract. Would the best solution in that case be to rewrite transmute_unchecked_two_ways in a similar way to transmute_two_ways, where we have a #[kani::proof] and we just explicitly assume the validity precondition in the macro/harness? Or would you suggest another approach?
I agree with this approach.
| transmute_unchecked_should_fail!(transmute_unchecked_u8_to_bool, u8, bool); | ||
| transmute_unchecked_should_fail!(transmute_unchecked_i32_to_char, i32, char); | ||
| transmute_unchecked_should_fail!(transmute_unchecked_u32_to_char, u32, char); |
There was a problem hiding this comment.
It is nice if for each should_fail harness, you can add a should_succeed one for the same type pair to cover the case where the transmute is safe. We can replace kani::any() in the should_fail harness by kani::any_where(...). Let's try let src = kani::any_where(|x| from_u32(*x).is_some()); for (u32, char) case.
Toward solving #19
This pr adds some additional harnesses for transmute_unchecked and transmute.
With this, we suspect that the main harnesses for part 1 of challenge 1 (verifying the transmute intrinsics directly) are there (besides adding more of the same kinds of harnesses, like the 2-way harnesses for more types). We go into more detail about what needs to be done for part 1, as well as what has been done and what can't be done here: https://docs.google.com/document/d/1zFGANNMx8mZ8fucKrN--ELwKASUPeP20THH6M_fQ7jg/edit?usp=sharing
Just one note: transmute has far fewer harnesses than transmute_unchecked here -- this is because it is not currently possible to write a wrapper for transmute, and it is thus not possible to write a function contract. A lot of the harnesses for transmute_unchecked test the function contract's validity clause, rather than the function itself, explaining this disparity.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.