Does reading MTCC with CSRR return the address or the offset?

[tariqkurd-repo]

The spec says:

Where an SCR extends a RISC-V CSR, e.g. MTCC extending mtvec, 
any read to the CSR shall return the address of the corresponding 
SCR. Similarly, any write to the CSR shall set the address of the SCR 
to the value written. This shall be equivalent to a CSetAddr instruction.

The SAIL says:

function get_mtvec() -> xlenbits =
  getCapOffsetBits(MTCC)

function getCapOffsetBits(c) : Capability -> CapAddrBits =
    let base : CapAddrBits = getCapBaseBits(c) in
    c.address - base

function getCapOffset(c) : Capability -> CapAddrInt =
    unsigned(getCapOffsetBits(c))

I expect to read the address not the offset, so is the SAIL out of date? For reference, CSetAddr does set the address field not the offset in the SAIL:

val setCapAddr : (Capability, CapAddrBits) -> (bool, Capability)
function setCapAddr(c, addr) =
    let newCap = { c with address = addr } in
    let representable = capBoundsEqual(c, newCap) in
    (representable, newCap)

[arichardson]

The sail was updated recently, this was aligned with the spec in https://github.com/CTSRD-CHERI/sail-cheri-riscv/commit/8d390d9e11f3d1563983d0f7a1a65317a6187adc

[tariqkurd-repo]

perfect, thanks Alex, I've updated my checkout.

[tariqkurd-repo]

function legalize_tcc(o : Capability, v : Capability) -> Capability = {
...
    let legalized_tvec = legalize_tvec(Mk_Mtvec(cap_to_integer_pc(o)), new_tvec);
...
}

quick question @arichardson, as this does the representability check on the legalized address (i.e. including a valid MODE setting in bits [1:0]), then it's not actually doing the representability check on the address field of MTCC which would have address[1:0]=0 if either vectored or CLIC mode is programmed where MODE>0.

Does this matter, or should the check be done with address[1:0]=0 to be strictly accurate? I can't imagine any real cases where altering address[1:0] would change the representability, but I thought I'd ask the question.

[jrtc27]

You'd have to have a degenerate capability format, i.e. one with almost no bits of precision. Even today's RV32 capability format guarantees you can be at least 2^2 - 1 out of bounds.

[tariqkurd-repo]

that's what I thought - so it's nothing to worry about. Thanks.