Risc-v: proper management of the return address

[eponier]

On RISC-V, the return address is read from register RA. This was not reflected in the model and generated wrong programs.

The RAstack case of return_address_location is given an additional optional argument ra_return that specifies what register to use (if any) when returning from a function. linearization is adapted to generate the right code. reg alloc and merge_varmaps take into account this potential new register.

I'm unsure of the changes I did. In particular, for linearization_proof, I have the impression that there is some kind of duplication between the semantics (ra_vm, ra_undef, ...) and the proof that introduces killed_by_entry, killed_on_exit, killed_by_exit. I managed to have a working version of the proof, but this may not be the principled one.

And the history is horrible, I still have some changes to do, I'll clean it at some point.

[eponier]

I also have to rebase on branch risc-v, and to undo the commit adding ra to the callee_saved registers (even if that could make sense, ra contains the return address both when entering and leaving the function).

[eponier]

Btw, there is something to be checked about RISC-V, related to the linearization_params. The code was copied from arm, and it should work. But if I'm not mistaken, there are two constraints on ARM that make the code more complex:

1. there are some operations that we cannot do directly on RSP
2. instructions do not accept large immediate.

For RISC-V, 2. is true, but 1. is not. Does this mean we should adapt a bit the code?

[eponier]

I've just rebased on top of #934

[eponier]

Btw, there is something to be checked about RISC-V, related to the linearization_params. The code was copied from arm, and it should work. But if I'm not mistaken, there are two constraints on ARM that make the code more complex:

1. there are some operations that we cannot do directly on RSP

2. instructions do not accept large immediate.

For RISC-V, 2. is true, but 1. is not. Does this mean we should adapt a bit the code?

I created issue #954 to keep track of that part.

[eponier]

I also have to rebase on branch risc-v, and to undo the commit adding ra to the callee_saved registers (even if that could make sense, ra contains the return address both when entering and leaving the function).

done