Page table extension state not updated during walk?

[nwf]

The ext_ptw tokens that get passed around the PTW machinery appear not to be updated as the walk functions do their thing.

Specifically, the initial ext_ptw state is constructed at
https://github.com/rems-project/sail-riscv/blob/38f52c99289e31aef72a4272e1a46b7a3398e076/model/riscv_vmem_rv64.sail#L47 (or at https://github.com/rems-project/sail-riscv/blob/38f52c99289e31aef72a4272e1a46b7a3398e076/model/riscv_vmem_rv32.sail#L40) and is passed down to translateNN a few lines later.

Focusing on Sv39 by way of example, we see that translate39 either takes this initial value and allows checkPTEPermission to filter it in the case of a TLB hit ...
https://github.com/rems-project/sail-riscv/blob/392dba44738d9c4702ef822a44772b73099b0d92/model/riscv_vmem_sv39.sail#L120-L122
... or passes it to walk39 for filtering in the case of a TLB miss ...
https://github.com/rems-project/sail-riscv/blob/392dba44738d9c4702ef822a44772b73099b0d92/model/riscv_vmem_sv39.sail#L149-L151

So far so good. However, internally, walk39 simply punts its given ext_ptw token downwards. At the time of its recursive call ...
https://github.com/rems-project/sail-riscv/blob/392dba44738d9c4702ef822a44772b73099b0d92/model/riscv_vmem_sv39.sail#L36
... ext_ptw is simply that of its argument. Therefore, when walk39 reaches its leaf call to checkPTEPermissions ...
https://github.com/rems-project/sail-riscv/blob/392dba44738d9c4702ef822a44772b73099b0d92/model/riscv_vmem_sv39.sail#L43
... ext_ptw is simply the initial state.

I think the thing to do is to make isPTEPtr have type (pteAttribs, extPte, ext_ptw) -> option(ext_ptw), so that it can mutate the state at internal nodes of the tree. Does that seem right?

[pmundkur]

Yes, that makes sense. It was supposed to accumulate information, as the comment next to init_ext_ptw indicates. Doing it at isPTEPtr seems reasonable. Perhaps we should rename isPTEPtr to something more sensible though