Jump macro instructions in the RISC-V target printer

[lgourdin]

I found a relocation error while compiling heavy programs on RISC-V:
Using CompCert, if the destination symbol of a goto or a tailcall (Mtailcall sig (inr s) in Mach) is far away from the current pc (for program size over 1MB), then the address may not fit in the 21-bits address offset supported by the jal (jump and link) instruction.
In such a case, the linker will reject the program (fortunately, no buggy code is produced).

To fix this problem, we can modify the target printer and rely on the linker relaxation:

As Mgoto and Mtailcall are translated to Pj_l and Pj_s respectively, we just have to modify the following code in the target printer (replacing the j pseudo instruction by a tail:

from

      | Pj_l(l) ->
         fprintf oc "	j	%a\n" print_label l
      | Pj_s(s, sg) ->
         fprintf oc "	j	%a\n" symbol s

to

      | Pj_l(l) ->
         fprintf oc "	tail	%a\n" print_label l
      | Pj_s(s, sg) ->
         fprintf oc "	tail	%a\n" symbol s

Indeed, j is a pseudo instruction corresponding to a jal x0, offset while tail is expanded into the sequence:

auipc x6, offset[31 : 12] + offset[11]
jalr x0, offset[11:0](x6)

It is not a problem to always generate tail pseudo instructions instead of j since the linker is able to replace the tail pair to a single jal when the address fits.

For reference and discussion on this topic, see the following resources:

• Pseudo instructions for jumps on RISC-V: Volume I Unprivileged ISA V20191213, p140
• SiFive forum discussion here
• SiFive blog article about linker relaxation on RISC-V here

Is the target printer written this way on purpose, or is this a bug? We consider it is a bug on our side, and we have fixed our CompCert fork as explained above.

[xavierleroy]

Thanks for this report. It's quite possible that the original author of the RISC-V back-end was not aware of the "tail" pseudo-instruction. Will look into using it.