proposed bugfix for issue #436

[Yuki21]

More information about the bugfix:

1. We don't need to modify the TargetPrinter for Pj_l, as it is only used for goto inside a function. (We can suppose that the case where an address does not fit is very unlikely for gotos inside a function; moreover, even if we have a huge function where it happens, we would then have more important problems to deal with such as the conditional jumps which are addressed on 12bits only).
2. Of course, modifying the Pj_s printer rule as above implies a modification in the Asm semantics of CompCert, as the pseudo instruction clobbers x6. This modification itself implies some small changes in the proof, and the need to declare x6 as a scratch register. It must thus be invisible from Mach.

I modified the Asm semantics, as well as the Machregs builtins parameters, because x6 can not be used as an input for builtins anymore. Thus, we use x8 instead, and, consequentially, I adapted Asmexpand untrusted file to change builtins functions and corresponding assertions.

Don't hesitate to tell me if I forgot something here, but I think this commit solves the issue. The non-regression tests are passing successfully.

[xavierleroy]

Thanks for the proposal, but I'm not happy with losing X6 as an allocatable register. You're right that the pseudo-instructions tail and call use X6 as a temporary register, but I hope this could be handled differently.

[Yuki21]

Your comment made me want to dig a little deeper into the question.
The call macro is using x1 (the return address) instead of x6. I thought the only way to avoid loosing x6 was to generate manually the auipc + jalr pair, but in fact it is not a great solution as you will not succeed to obtain the right relocation tag.
Loading the relative address manually using:

auipc	a0, %pcrel_hi(msg + 1)
addi	a0, a0, %pcrel_lo(1b)

will generates relative address loading tags in the object file, and it is not exactly what we want.

However, there is a special pseudo instruction jump (see https://github.com/riscv-non-isa/riscv-asm-manual/blob/master/riscv-asm.md#function-calls) that can do the job. This pseudo instruction is expanded in the same way as the tail but with a specified scratch register.

For instance, if I have a jump func, x31 in the asm file: I compile it with the gcc assembler, and then l look the objdump with riscv64-linux-gnu-objdump -Mnumeric -r -d. We obtain:

  38:   00000f97                auipc   x31,0x0
                        38: R_RISCV_CALL        func
                        38: R_RISCV_RELAX       *ABS*
  3c:   000f8067                jr      x31 # 38 <_start+0x18>

and thus we can use x31 as a scratch register for tailcalls (and x31 is already marked as scratch in CompCert)!

I have made a new proposition in Yuki21@b14d831.

[xavierleroy]

Thanks for the suggestion to use jump symb, x31. The jump pseudo is not documented in the 2019 RISC-V ISA manual, but has been mentioned in the assembly language manual since 2020, and the GNU assembler handles it fine. I didn't see your second push before implementing the jump-based solution. It's now in trunk. Let me know if it doesn't work for you.