TB: update terminology to match paper & MiniRust #4595
Conversation
|
Thank you for contributing to Miri! |
| /// For all non-accessed locations in the RangeMap (those that haven't had an | ||
| /// implicit read), their SIFA must be weaker than or as weak as the SIFA of | ||
| /// `default_perm`. | ||
| /// `default_perm`; otherwise, this will panic. |
There was a problem hiding this comment.
@JoJoDeveloping I am actually a bit confused by this. The assertion looks as follows:
assert!(
default_strongest_idempotent
>= perm.permission.strongest_idempotent_foreign_access(protected)
);This seems to run for all locations in initial_perms, not just the non-accessed ones. Why that?
There was a problem hiding this comment.
It could be changed to the following, I think:
assert!(
perm.is_accessed()
|| default_strongest_idempotent
>= perm.permission.strongest_idempotent_foreign_access(protected)
);
But the way it is currently makes it easier to reason about because the SIFA correction can be proven correct without considering the initial read.
There was a problem hiding this comment.
Then we should update the comments to match, though.
There was a problem hiding this comment.
Instead of tracking this assertion all the way through, wouldn't it be easier to just compute the maximum SIFA and pass that to update_last_accessed_after_retag? I've done that now in the 2nd commit, could you take a look if that makes sense?
RalfJung
force-pushed
the
tb-terms
branch
3 times, most recently
from
4305e61 to
9591c61
Compare
| { | ||
| assert!(perm.is_initial()); | ||
| max_sifa = | ||
| cmp::max(max_sifa, perm.permission.strongest_idempotent_foreign_access(protected)); |
There was a problem hiding this comment.
perm.permission.strongest_idempotent_foreign_access is odd, isn't it? perm already contains a SIFA. We should just read that.
There was a problem hiding this comment.
I think we could. If that field is wrongly initialized it is a bug anyways.
There was a problem hiding this comment.
Yeah my latest revision does that.
|
Looks reasonable now. |
|
Thanks for taking a look! |
No description provided.