align_to and align_to_mut contract and harnesses #405
Conversation
|
Thank you! We should have a fix for the Kani issue with model-checking/kani#4151 really soon, so I'd love to hold off on this one for about a week so that we can get the Kani fix merged and have this repository use the updated Kani version. |
| ((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) && | ||
| ((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) ) | ||
| ) | ||
| )] |
There was a problem hiding this comment.
I don't see in the ensures clauses the condition that the middle part is correctly aligned.
There was a problem hiding this comment.
Actually, this is something I was wondering about -- my impression was that because it's UB to create a misaligned reference, it would be redundant to have a check for the middle part being aligned (since if it isn't, there would already be UB by the time the ensures clause is checked, meaning the check would either return true or something potentially invalid due to previous UB). But of course it's possible that Kani might have some way to circumvent this problem that I'm not familiar with (otherwise the only way I can think of would be to write this check as an assert inside the body of align_to, right before where there could potentially be UB). Would be happy to hear your thoughts on this whenever you have a chance!
| ((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) && | ||
| ((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) ) | ||
| ) | ||
| )] |
There was a problem hiding this comment.
I don't see in the ensures clauses the condition that the middle part is correctly aligned.
@AlexLB99 We now have the Kani fix merged and the version of Kani that this repository uses includes this fix. Could you please adjust your implementation so as not to use a workaround anymore? |
Towards solving #19
This PR adds harnesses and contracts for align_to() and align_to_mut(). For the contract for align_to_mut(), we're using a wrapper and writing a contract for that instead, due to model-checking/kani#3764.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.