You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
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:
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.
The text was updated successfully, but these errors were encountered:
Yuki21
pushed a commit
to Yuki21/CompCert
that referenced
this issue
Jun 22, 2022
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.
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 thejal
(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
andMtailcall
are translated toPj_l
andPj_s
respectively, we just have to modify the following code in the target printer (replacing thej
pseudo instruction by atail
:from
to
Indeed,
j
is a pseudo instruction corresponding to ajal x0, offset
whiletail
is expanded into the sequence:It is not a problem to always generate
tail
pseudo instructions instead ofj
since the linker is able to replace thetail
pair to a singlejal
when the address fits.For reference and discussion on this topic, see the following resources:
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.
The text was updated successfully, but these errors were encountered: