search

microsoft / cheriot-ibex

cheriot-ibex is a RTL implementation of CHERIoT ISA based on LowRISC's Ibex core.
Apache License 2.0
73 stars 14 forks source link

MEPCC set_address #36

Closed mndstrmr closed 4 months ago

mndstrmr commented 4 months ago

In pcc2mepcc, you write that set_address is not required since we know the PC is in bounds according to IF.

https://github.com/microsoft/cheriot-ibex/blob/097d962f143b40e0cf120227f5dbc8d74a123dc4/rtl/cheri_pkg.sv#L594-L600

I do not believe this to be the case. Consider the following trace:

  1. At cycle t, we branch (CJALR) to a new PCC with small bounds and to a PC that is outside of those bounds. This is legal according to the Sail (and the RTL).
  2. In the following cycle (t + 1) the new PCC is set and IF clears its FIFO and sends a request for the next instruction at the new address. When this succeeds we will get an error, but suppose that instruction memory takes a long time to respond. Since no error is raised until an actual instruction is received, during this time no exception will be raised. That said, pc_if_o will become the new address anyway.
  3. Suppose instead that during that same cycle (t + 1) an interrupt is raised. Now MEPCC is set to pcc_exc_cap = pcc2mepcc(pcc_cap_q, exception_pc, csr_mepcc_clrtag_i). exception_pc = pc_if since this is an interrupt, but as we arranged at time t, pc_if is outside of the bounds of the PCC, meaning the invariant fails and pcc2mepcc ends up with moved bounds (breaking monotonicity I believe).

I would suggest that pcc2mepcc needs to use set_address.

kliuMsft commented 4 months ago

Great finding.. Yes when making the change I missed this condition where we save pc_if instead of pc_id. I am reversing back to always doing representability check.

kliuMsft commented 4 months ago

The RTL commit 4a739b4 reverted back to include set_address check for pcc2mepcc

mndstrmr commented 4 months ago

Fix verifies, thanks.