With option returnaddress=stack, the compiler can use LR/ra as a result register

[eponier]

The problem arises both on ARM and RISC-V.

This progam

param int N = 5;

#[returnaddress=stack]
fn f () -> reg u32 {
  reg u32 x;
  x = 3;
  return x;
}

export fn main (reg u32 res) -> reg u32 {
  reg u32 tmp;
  reg u32[N] r;
  inline int i;

  for i = 0 to N {
    r[i] = 0;
  }
  tmp = f ();
  res = tmp;
  for i = 0 to N {
    res += r[i];
  }
  return res;
}

allows to reproduce the bug. After regalloc, the register chosen for the result of f is LR on ARM and ra on RISC-V. This obviously does not work, since the function then returns its return address instead of the expected result. I don't understand why this is not captured in the proofs.

First version of the bug found by @clebreto

[clebreto]

Adding RA to the list of callee_saved registers in the RISCV declaration seems to be enough to fix the issue on the RISCV side.

Independently (to the returnaddress=stack flag), omitting RA from the list of callee_saved registers let the compiler use RA to return a value and the return address at the same time making the return value garbage.

7a14e76

[eponier]

I thought about it, and I think the fact that adding RA to the callee_save registers avoids the problem on our examples is more or less luck. Indeed, callee_save registers can be used by reg alloc, but only if all others registers are used. What the change does is just that RA is picked less often. But it's not the proper solution.

[eponier]

In regalloc.ml, there is code to ensure that RA is in conflict with the results. It should certainly be patched. But the unclear part to me is what to do on the Coq side.

[vbgl]

I can’t reproduce the bug on ARM: LR is indeed use for passing the returned value of f, but that looks fine. The return address of f is read from the stack.

[eponier]

Indeed, so it is a problem only for RISC-V, but that means that the problem will be more subtle to fix.

[eponier]

Now I understand, the error is in the RISC-V implementation. We use ret like on x86 and on ARM, but on these two platforms the RA is on the top of the stack while on RISC-V it needs to be in register ra. Let me check if the patch is easy.

[vbgl]

Does returnaddress=stack makes sense on risc-v?

[bgregoir]

Sorry JC. I don't understand what you say here.
In Arm, return also expects to have the return address in RA.

[vbgl]

No, the POPPC instruction takes it from the top of the stack.

[eponier]

On ARM, it is passed in RA then put on the stack and popped from the stack. On RISC-V, it is both passed in RA and read from RA (for the return).

[eponier]

Does returnaddress=stack makes sense on risc-v?

Maybe not.

[eponier]

On ARM, it is passed in RA then put on the stack and popped from the stack. On RISC-V, it is both passed in RA and read from RA (for the return).

More precisely, on ARM we have plenty of ways to do the return. If the return address is in LR, we can use bx lr. If it is on the stack, we can use pop {pc}. On RISC-V, we are forced to use a register. So indeed I think returnaddress=stack does not make sense on RISC-V.

[eponier]

Hm, there is still a problem, because when a function is not a leaf function, the compiler correctly decides to save the return address on the stack. But then it issues a POPPC that we don't know how to implement on RISC-V.