RISC-V Pbtbl pseudoinstruction: use x6 as temporary

The register `x5` can be used as an alternate link register for function
calls, and thus we want to avoid using it for regular jumps.
(This could confuse disassemblers and binary code analysis.)

Author: bschommer

riscV/Asm.v

@@ -966,7 +966,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | Vint n =>
           match list_nth_z tbl (Int.unsigned n) with
           | None => Stuck
-          | Some lbl => goto_label f lbl (rs#X5 <- Vundef #X31 <- Vundef) m
+          | Some lbl => goto_label f lbl (rs#X6 <- Vundef #X31 <- Vundef) m
           end
       | _ => Stuck
       end

riscV/Asmgenproof.v

@@ -881,7 +881,7 @@ Local Transparent destroyed_by_op.
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H5); intro NOOV.
   exploit find_label_goto_label. eauto. eauto.
-  instantiate (2 := rs0#X5 <- Vundef #X31 <- Vundef).
+  instantiate (2 := rs0#X6 <- Vundef #X31 <- Vundef).
   Simpl. eauto.
   eauto.
   intros [tc' [rs' [A [B C]]]].

riscV/Machregs.v

@@ -174,7 +174,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre
 
 Definition destroyed_by_cond (cond: condition): list mreg := nil.
 
-Definition destroyed_by_jumptable: list mreg := R5 :: nil.
+Definition destroyed_by_jumptable: list mreg := R6 :: nil.
 
 Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
   match cl with

riscV/TargetPrinter.ml

@@ -526,12 +526,12 @@ module Target : TARGET =
          fprintf oc "%s jumptable [ " comment;
          List.iter (fun l -> fprintf oc "%a " print_label l) tbl;
          fprintf oc "]\n";
-         fprintf oc "	sll	x5, %a, 2\n" ireg r;
+         fprintf oc "	sll	x6, %a, 2\n" ireg r;
          fprintf oc "	lla	x31, %a\n" label lbl;
-         fprintf oc "	add	x5, x31, x5\n";
-         fprintf oc "	lw	x5, 0(x5)\n";
-         fprintf oc "	add	x5, x31, x5\n";
-         fprintf oc "	jr	x5\n";
+         fprintf oc "	add	x6, x31, x6\n";
+         fprintf oc "	lw	x6, 0(x6)\n";
+         fprintf oc "	add	x6, x31, x6\n";
+         fprintf oc "	jr	x6\n";
          jumptables := (lbl, tbl) :: !jumptables;
          fprintf oc "%s end pseudoinstr btbl\n" comment
       | Pnop ->