Hi,
I was wondering whether it would make sense for Rust to offer an "extension" of unsafe
whereby we could annotate it with something denoting the invariants that it expects from callers.
For example, something like unsafe<'a>
would denote the invariant 'a
that callers must assert (which would be documented somewhere).
This idea comes from the following code snipped: assume that we store an array of utf8-encoded u8's of a fixed size size
as &[u8]
.
The function to get a specific element i
is
impl MyUtf8Array {
fn value(&self, i: usize) -> &str {
let slice = &self.values[i * self.size..(i+1) * self.size];
// soundness: we checked that every item is valid utf8 on the constructor
return unsafe {std::str::from_utf8_unchecked(slice)}
}
}
we also provide an extra method,
impl MyUtf8Array {
/// # Safety
/// `i` must be smaller than `self.values.len() / self.size`;
unsafe fn value_unchecked(&self, i: usize) -> &str {
// soundness: the invariant.
let slice = self.values.get_unchecked(i * self.size..(i+1) * self.size);
// soundness: we checked that every item is valid utf8 on the constructor
return std::str::from_utf8_unchecked(slice)
}
}
the issue is that, on the second example, there are two independent invariants (say 'a
and 'b
) that we must uphold, and the fn unsafe
masks them both.
If the from_utf8_unchecked
's unsafe
would be annotated (e.g. 'b
), we could write things like
impl MyUtf8Array {
/// # Safety
/// `i` must be smaller than `self.values.len() / self.size`;
unsafe<'a> fn value_unchecked(&self, i: usize) -> &str {
// soundness: the invariant.
let slice = self.values.get_unchecked(i * self.size..(i+1) * self.size);
// soundness: we checked that every item is valid utf8 on the constructor
return unsafe<'b> {std::str::from_utf8_unchecked(slice)}
}
}
for backward compatibility, when a user writes unsafe
without any annotation, we would assume that it covers all invariants inside the block it annotates.
This could make it easier to read which invariants each part of the code base covers. We could even use things like 'a < 'b
to indicate that invariants 'b
covers all invariants 'a
.
Not sure, trying to express a problem whereby a block of unsafe
masks certain invariants just because we have no mechanism to express the existence of different invariants in the language.