Intrinsic types

[marcfedorow]

There are more SEXT32(rd) functions but they does not follow the maddr32's logic (check #43 for more information). E.g. kaddh, kaddw, ksubh, ksubw, raddw, rsubwand their unsigned analogues return intXLEN_t and uintXLEN_t respectively. I think that all such intrinsics should return [u]int32_t. Also sign-extension of unsigned results (e.g. in uraddw) seems strange to me.

There are more problems with intrinsic types: I think, kabsw may return uint32_t; SE64 may be removed. kslra8 and kslra8.u should take the second argument as int32_t, not int. Same for kslra16[.u]. smul8, smulx8, umul8, umulx8, umul16, umulx16 should take uint32_t arguments as smul[x]16 does. sunpkd8xy intrinsics should probably return intXLEN_t instead of uintXLEN_t while it is a signed unpack operation (opposed to zunpkd8xy insns).

There are also some lack of logic in shift-amount-operands' types. E.g. sra32[i][.u] checks whether sa is positive, but the second argument of its intrinsic is uint32_t. It seems like -1 is much more adequate immediate value than 0x1F (even though -1 == 0x1F this case) so int32_t is more verbose.

[rsnikhil]

Tbh I think we should probably try to fully use Sail's fancy type system in this new VM code rather than just expanding everything to 64 bits immediately. It's very useful for catching bugs like this.

We're currently building for either RV32/Sv32 or RV64/Sv39/Sv48. But I believe the spec permits supporting all the options simultaneously in a single implementation. The do-everything-at-64-bits regime in the current vmem code was geared towards doing that in the future; I don't know how we can restrict this with types.

[Timmmm]

I don't know how we can restrict this with types.

You should be able to make the widths of everything type parameters. One issue is that there are quite a lot of type parameters. However you could in theory just have a single type parameter for the whole thing, based on the Sv?? number - i.e. {32, 39, 48, 57}. Then you can use Sail's very recent support for if/else in types to derive all the other parameters where needed (I don't think this was an option when you wrote this code). There's an example of that here:

val fsplit : forall 'n, 'n in {16, 32, 64}.
  bits('n) -> (
    bits(1),
    bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
    bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
  )

So for example instead of:

// PRIVATE: extract PPNs of PTE
function PPNs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = {
  let mask : bits(64) = zero_extend(ones(sv_params.pte_PPNs_size_bits));
  (pte >> sv_params.pte_PPNs_lsb_index) & mask
}

You can condition it on the PTE size, so that it returns bits(22) or bits(44).

val PPNs_of_PTE : forall 'pte_size, 'pte_size in {32, 64}.
  bits('pte_size) -> bits(if 'pte_size == 32 then 22 else 44)
function PPNs_of_PTE(pte) = if sizeof('pte_size) == 32 then pte[31 .. 10] else pte[53 .. 10]

It is a fair bit of work to make Sail happy though. I might have a go one day.