search

CHERIoT-Platform / cheriot-sail

Sail code model of the CHERIoT ISA
Other
34 stars 9 forks source link

New algorithm for bounds calculation and changes to cap encoding #76

Open vmurali opened 1 month ago

vmurali commented 1 month ago

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.

vmurali commented 1 month ago

Note that I use the same names $e, d, i$ in setCapBounds as in #75 , to correlate the code with the math.

vmurali commented 1 month ago

Yes and yes!

vmurali commented 1 month ago

@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.

vmurali commented 1 month ago

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: 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