The definition of the function is_aligned_addr overlaps with the function is_aligned

[KotorinMinami]

In riscv_insts_base.sail:311-317 , we have:

function is_aligned(vaddr : xlenbits, width : word_width) -> bool =
  match width {
    BYTE   => true,
    HALF   => vaddr[0..0] == zeros(),
    WORD   => vaddr[1..0] == zeros(),
    DOUBLE => vaddr[2..0] == zeros(),
  }

but in riscv_mem.sail:42-43 , we have:

function is_aligned_addr forall 'n. (addr : xlenbits, width : int('n)) -> bool =
  unsigned(addr) % width == 0

Obviously the latter can implement the former, and there is code implementation redundancy between the two, of course we can implement is_aligned using is_aligned(vaddr, width) = is_aligned(vaddr, size_bytes(width)) to avoid somehow different definitions or duplicated definitions

[Timmmm]

I agree. There are only 4 places where is_aligned() is called actually (3 for atomics, and 1 in check_misaligned()), so I would say we just remove it and replace it with is_aligned_addr(..., size_bytes(...)), and then probably rename is_aligned_addr to just is_aligned.

[Alasdair]

One issue is the big integer modulus on the alignment check is very expensive, and it's effectively in a hot path where it gets called a lot. Back when I was optimising the Arm spec to improve the Linux boot times for our old POPL paper changing the alignment check was one of the biggest speedups.

[arichardson]

One issue is the big integer modulus on the alignment check is very expensive, and it's effectively in a hot path where it gets called a lot. Back when I was optimising the Arm spec to improve the Linux boot times for our old POPL paper changing the alignment check was one of the biggest speedups.

I imagine this could be fixed by rewriting the expression as unsigned(addr) & (width - 1) == 0?

[KotorinMinami]

I imagine this could be fixed by rewriting the expression as unsigned(addr) & (width - 1) == 0?

I just don't know how the C code will handle it during execution, and function is_aligned_addr doesn't seem to limit the input range of width, which I think may need to be limited to $2^n, n=0,1,2,3...$, and really should be, by the definition of RISC-V address alignment, and by this optimization