New algorithm for bounds calculation and changes to cap encoding#76
New algorithm for bounds calculation and changes to cap encoding#76vmurali wants to merge 3 commits intoCHERIoT-Platform:mainfrom
Conversation
vmurali
force-pushed
the
newbounds
branch
4 times, most recently
from
2fe9238 to
dd4ffd8
Compare
|
Note that I use the same names |
…ource of error in pdf (PDF is still inconsitent with sail spec)
src/cheri_cap_common.sail
Outdated
| let E = if c.cE == zeros(cap_cE_width) then zeros(cap_E_width) else c.ME @ (c.cE - zero_extend(c.ME)); | ||
| let M = if c.cE == zeros(cap_cE_width) then c.ME @ c.cM else 0b1 @ c.cM; |
There was a problem hiding this comment.
If I understand this correctly this works as follows:
| cE | ME | E | M8 |
|---|---|---|---|
| 0 | 0 | 0 | 0 |
| 0 | 1 | 0 | 1 |
| 1..15 | 0 | 1..15 | 1 |
| 1..15 | 1 | 16 .. 30 | 1 |
That works but I think it would be simpler to use a 5 bit cE with a single special value for E=0, M8=0 as follows:
| cE | E | M8 |
|---|---|---|
| 0..30 | 0..30 | 1 |
| 31 | 0 | 0 |
It just uses two values to encode E=0 depending on the value of M8.
These two lines would become:
let E = if c.E == ones(cap_cE_width) then zeros(cap_E_width) else c.E;
let M = (if c.E == ones(cap_cE_width) then 0b0 else 0b1) @ c.cM;
|
Yes and yes! |
|
@rmn30 https://gist.github.com/vmurali/fc50a31be8a2cdd2b82e9a1e3d164e59 seems to be the changes that you suggested. I am not sure what the problem is. It fails for 05.sealing test. The symptom I am seeing is that an untagged 64-bit 0 is interpreted as an untagged 0x100 length capability because the mantissa's MSB is 1. Is this problematic for code? I tried to invert the polarity (all zeros means mantissa MSB is 0, all ones means mantissa MSB is 1), but that didn't work at all. |
…n't work - a null capability is interpreted with 0x100 length and hence fails), namely E = if cE == 31 then 0 else cE M8 = if cE == 0 then 0 else 1 cE = if E == 0 && M8 == 1 then 31 else E
|
It looks like the null cap with non zero length is an issue in the code (at least for 06.sealing). Robert's suggestion with reversed polarity is implemented now: cE = if E == 0 && M8 == 1 then 31 else E |
2 participants
The algorithm implements Issue #75 . I also changed the encoding to represent base (B) and difference (M) rather than base (B) and top (T). This also simplified the expressions overall.