Legalise underivable caps #36
Conversation
|
I'm not sure how useful it is to share struct Capability between 64 and 128. We might provide a subset of permissions for 64 in the future? But I guess we could always hardcode the others to false. Also this PR needs to be rebased. |
Hmm, yes, or factor out the permissions into a separate struct in that case. It seemed silly to duplicate all the decoding logic at least... I'll do a rebase now. It seems to mostly be trivial mantissa_width vs cap_mantissa_width. |
PeterRugg
force-pushed
the
underivable
branch
2 times, most recently
from
080b6e0
to
69869a4
Compare
There was a problem hiding this comment.
Looks good to me, I've just left a few syntactic suggestions. The properties I've been SMT-checking before still hold, and I was able to strengthen the "(base <= top)" property by removing the precondition that the capability has canonical bounds, which is good.
PeterRugg
force-pushed
the
underivable
branch
from
78204bb
to
5a920b5
Compare
Sounds good, although we do expect differences: it might take some effort to differentiate bugs from intended changes. I haven't looked at the cheri-compressed-cap code much, but could add the changes to that if needed. |
|
@jrtc27 It would be nice to get this merged before too much rebasing is required. Any chance you're going to have time to take a look at it in the near future? |
PeterRugg
force-pushed
the
underivable
branch
5 times, most recently
from
5c8520c
to
053b8c3
Compare
PeterRugg
force-pushed
the
underivable
branch
from
053b8c3
to
f3a264c
Compare
|
I've tidied up the history and pulled most of the uncontroversial contents into master. |
| let correction_top = tHi - aHi in { | ||
| base_corrected : CapLenBits = base + (to_bits(cap_len_width, correction_base) << (cap_mantissa_width + E)); | ||
| top_corrected : CapLenBits = top + (to_bits(cap_len_width, correction_top) << (cap_mantissa_width + E)); | ||
| /* Interpret the top relative to the address space of the base. |
There was a problem hiding this comment.
Could you expand on this comment, e.g. explaining why this prevents base > top?
There was a problem hiding this comment.
Hmm, I don't think this alone prevents that. It's more ensuring that the top hasn't wrapped around to be in an entire address space (or more) below the base? I must admit, my memory is slightly hazy.
There was a problem hiding this comment.
Yeah it's been a while since I looked at this which is why I wasn't sure why we can now assert that base <= top. Adding some comments explaining where this is guaranteed would be helpful for future readers I believe.
There was a problem hiding this comment.
Right, agreed. I guess "it's been proved" is something, but it's also nice to see how it's been constructed to make this true.
Due to the way we decode top/bot it is possible for top to decode to 1<<66, but that is then truncated to zero and can therefore be less than the base of the capability. The example test case was found by TestRIG See CTSRD-CHERI/sail-cheri-riscv#36 for an alternative decoding approach that guarantees top >= base.
Due to the way we decode top/bot it is possible for top to decode to 1<<66, but that is then truncated to zero and can therefore be less than the base of the capability. The example test case was found by TestRIG See CTSRD-CHERI/sail-cheri-riscv#36 for an alternative decoding approach that guarantees top >= base.
Tested to match the Bluespec cheri-cap-lib implementation (PR pending).
Also includes refactoring to allow an intermediate struct without any decoding. This is required to neatly clear the IE bit, but has the side-effect of reducing duplicated code in preludes.