search

CHERIoT-Platform / cheriot-sail

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

v2: Split sentries by direction #42

Closed nwf-msr closed 5 months ago

nwf-msr commented 9 months ago

We have reserved space for, but do not presently implement, differentiating forward and backward sentries. There would then be at least five forms: forward with IRQ {preserved, disabled, enabled} and backward with IRQ {enabled, disabled}.

The ISA itself would need some tweaking: cjalr would need to seal PCC as one of the reverse types rather than one of the forward types, and cj and cjalr would need to differentiate between return and non-return transfers. Likely, absent any other encoding changes, this would enshrine cj ra (that is, cjalr x0, ra) as being a return instruction and prohibit its use for forward transfers, requiring modest toolchain work.

nwf-msr commented 5 months ago

This is in fact landed in v1. See #54 and https://cheriot.org/isa/ibex/2024/06/26/sentries-cfi.html