Description of is_PTE_ptr is inconsistent with qemu/spike/sail implementations

[trdthg]

Otherwise, the PTE is valid. If pte.r=1 or pte.x=1, go to step 5. Otherwise, this PTE is a pointer to the next level of the page table. Let i=i-1. If i<0, stop and raise a page-fault exception corresponding to the original access type. Otherwise, let a=pte.ppn×PAGESIZE and go to step 2.

I found some minor inconsistencies comparing the implementation of sail with the description in the spec, but I don't know why.

The documentation requires r, x, but all implementations coincidentally added w

sail

// PRIVATE: check if a PTE is a pointer to next level (non-leaf)
function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0)
                                                      & (pte_flags[W] == 0b0)
                                                      & (pte_flags[R] == 0b0)

spike

#define PTE_TABLE(PTE) (((PTE) & (PTE_V | PTE_R | PTE_W | PTE_X)) == PTE_V)

qemu

       if (pte & (PTE_R | PTE_W | PTE_X)) {
            goto leaf;
        }

[ved-rivos]

They are equivalent. In the specification, the step 3 disallows r=0, x=?, w=1. This gets extended by Zicdiss as the xwr = 010 encoding, which is reserved without Zicfiss, denotes a shadow stack page with Zicfiss.

[trdthg]

Oh, Thanks