CJALR/CJAL - PCC, instr_fault and perm_vio

[mndstrmr]

According to the Sail the new PCC set by a CJALR instruction does not have its address changed to the new PC, it is just cs1_val. Currently CherIoT-ibex sets it to setaddr2_outcap, but unseal_cap(rf_fullcap_a) would suffice.

instr_fault will therefore need to do its bounds checks another way. Using setaddr2_outcap anyway won't work as it also does representability checks which we don't want (either for CJALR or CJAL).

perm_vio for CJALR also doesn't need the rf_fullcap_a.base32[0] term (nothing like it exists in the Sail).

[kliuMsft]

You are right - and I would be very happy to get rid of setaddr2.

@rmn30 , could you confirm the last point? In the PDF version of arch spec (p108) we have the following as part of exception conditions:

cs1.address + imm is unaligned, ignoring bit 0

[rmn30]

I'm not sure exactly what the issue in question is here? The intention in the Sail is to compute the new PC as for RISC-V JALR i.e. ignoring bit 0. We then check that that address is in the bounds of the new PCC (and allows us to fetch at least two bytes). The check for bit 1 alignment is redundant because CHERIoT always has the C extension enabled.

[mndstrmr]

rf_fullcap_a.base32[0] is not checking anything to do with the alignment of the new PC, it is checking the alignment of the base bound, which unless I am missing something, is unrelated.

[rmn30]

CHERI-RISC-V does have an alignment check on the base, but we don't need it for CHERIoT. This is because we don't support hybrid mode. In hybrid mode the PC is logically an offset from PCC.base so an odd base would lead to confusion as it would require the PC to be odd to be aligned!

[mndstrmr]

Aah I see, I was not aware of that. Thanks for pointing that out.

[rmn30]

Yes, it looks like the spec. is a bit wrong there: we don't need the alignment check on the base (although an unaligned base would definitely be weird). The alignment check for cs1.address+imm is not incorrect but is redundant because we only support misa.C==1 so the destination PC is guaranteed to be aligned after clearing bit 0.

[kliuMsft]

RTL is updated (commit 1e52a94). We no longer uses setaddr2, rather CJAL/CJALR address bound checking is now done explicitly in check_cheri. The base alignment checking is also removed in CJALR. Please verify, thanks.

[kliuMsft]

Also - I made some structural changes about pcc_cap again, hopefully making thing more intuitive and consistent.

• pcc_cap_t now only holds the necessary information (tag, expanded bounds, exp, perm/cperm, obj_type, rsvd).
• Rather than passing pcc_fullcap around with the redundant information, we now just send pcc_cap to if_stage for fetch checking
• We only do pcc2fullcap conversion explicitly in a couple of places now and the result is only used locally, which hopefull reduce some confusion and risk
• Also we no longer touch pcc_cap for CJAL.

[mndstrmr]

Proofs are getting high (though not yet infinite - that's an issue on my end), so I'm happy to say this is solved, thanks!

[kliuMsft]

Thanks for following through!

From: Louis-Emile Ploix @.> Sent: Saturday, January 20, 2024 4:57 AM To: microsoft/cheriot-ibex @.> Cc: Comment @.>; Subscribed @.> Subject: Re: [microsoft/cheriot-ibex] CJALR/CJAL - PCC, instr_fault and perm_vio (Issue #8)

Proofs are getting high (though not yet infinite - that's an issue on my end), so I'm happy to say this is solved, thanks!

- Reply to this email directly, view it on GitHubhttps://github.com/microsoft/cheriot-ibex/issues/8#issuecomment-1902087648 or unsubscribehttps://github.com/notifications/unsubscribe-auth/A3V7IMBLBJGXCATC72NDGL3YPO5LRBFKMF2HI4TJMJ2XIZLTSOBKK5TBNR2WLJDUOJ2WLJDOMFWWLO3UNBZGKYLEL5YGC4TUNFRWS4DBNZ2F6YLDORUXM2LUPGBKK5TBNR2WLJDUOJ2WLJDOMFWWLLTXMF2GG2C7MFRXI2LWNF2HTAVFOZQWY5LFUVUXG43VMWSG4YLNMWVXI2DSMVQWIX3UPFYGLLDTOVRGUZLDORPXI6LQMWWES43TOVSUG33NNVSW45FGORXXA2LDOOJIFJDUPFYGLKTSMVYG643JORXXE6NFOZQWY5LFVE2TSMBRGM3DKOBZQKSHI6LQMWSWS43TOVS2K5TBNR2WLKRRHEYTGMRVG4YDMMNHORZGSZ3HMVZKMY3SMVQXIZI. You are receiving this email because you commented on the thread.

Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.