Expand "j_s symb" to "jump symb, x31" assembly pseudo-instruction

As suggested by Léo Gourdin in #437. The previous expansion as a plain "j" instruction fails when the jump offset is too large to be represented (issue #436). Fixes: #436 Closes: #437
AbsInt · Jun 24, 2022 · a34adc8 · a34adc8
1 parent 44a668f
commit a34adc8
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 5 deletions.
diff --git a/Changelog b/Changelog
@@ -18,7 +18,7 @@ Usability:
   trigger only if parameters were declared.)
 - Check (and warn if requested) for arguments of struct/union types passed
   to a variable-argument function.
-	
+
 Bug fixes:
 - RISC-V: fixed an error in the modeling of float32 <-> float64 conversions
   when the argument is a NaN (#428).
@@ -29,6 +29,8 @@ Bug fixes:
   in correct but different allocations.)
 - Hardened the configure script against Cygwin installations that produce
   \r\n for end-of-lines (#434).
+- RISC-V: tail calls to far-away functions were causing link-time errors
+  (#436, #437).
 
 Coq development:
 - Updated the Flocq library to version 4.1.

diff --git a/riscV/Asm.v b/riscV/Asm.v
@@ -751,7 +751,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pj_l l =>
       goto_label f l rs m
   | Pj_s s sg =>
-      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
+      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero) #X31 <- Vundef) m
   | Pj_r r sg =>
       Next (rs#PC <- (rs#r)) m
   | Pjal_s s sg =>

diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
@@ -816,6 +816,7 @@ Local Transparent destroyed_by_op.
   (* match states *)
   econstructor; eauto.
   apply agree_set_other; auto with asmgen.
+  apply agree_set_other; auto with asmgen.
   Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
 
 - (* Mbuiltin *)

diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
@@ -315,12 +315,10 @@ module Target : TARGET =
          fprintf oc "	sra	%a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2
 
       (* Unconditional jumps.  Links are always to X1/RA. *)
-      (* TODO: fix up arguments for calls to variadics, to move *)
-      (* floating point arguments to integer registers.  How? *)
       | Pj_l(l) ->
          fprintf oc "	j	%a\n" print_label l
       | Pj_s(s, sg) ->
-         fprintf oc "	j	%a\n" symbol s
+         fprintf oc "	jump	%a, x31\n" symbol s
       | Pj_r(r, sg) ->
          fprintf oc "	jr	%a\n" ireg r
       | Pjal_s(s, sg) ->