Merge pull request #595 from AbsInt/x86_64-jmptbl

x86-64 `Pjmptbl`: normalize the argument before indexing into the jump table

Author: xavierleroy

Changelog.md

@@ -12,6 +12,7 @@ Bug fixes:
 - Thread the current typing environment through `Elab.elab_initializer`.
 - Printing of assembly files: quote command-line arguments when needed (#586)
 - Printing of assembly files: revised string quoting in debugging information (#588)
+- x86 64 bits, `Pjmptbl` instruction: make sure the 32-bit argument is zero-extended to 64 bits before indexing in the jump table (#595)
 
 Usability:
 - AArch64 asm clobbers: recognize more register names (#576)

riscV/TargetPrinter.ml

@@ -521,6 +521,7 @@ module Target : TARGET =
          fprintf oc "	flw	%a, %a, x31 %s %.18g\n"
                     freg rd label lbl comment (camlfloat_of_coqfloat32 f)
       | Pbtbl(r, tbl) ->
+         assert (Int64.of_int (List.length tbl) <= 0x8000_0000L);
          let lbl = new_label() in
          fprintf oc "%s jumptable [ " comment;
          List.iter (fun l -> fprintf oc "%a " print_label l) tbl;

test

@@ -752,7 +752,9 @@ module Target(System: SYSTEM):TARGET =
             let (tmp1, tmp2) =
               if r = RAX then (RDX, RAX) else (RAX, RDX) in
             fprintf oc "	leaq	%a(%%rip), %a\n" label l ireg tmp1;
-            fprintf oc "	movslq	(%a, %a, 4), %a\n" ireg tmp1 ireg r ireg tmp2;
+            (* Normalize r to 32-bit unsigned *)
+            fprintf oc "	movl	%a, %a\n" ireg32 r ireg32 tmp2;
+            fprintf oc "	movslq	(%a, %a, 4), %a\n" ireg tmp1 ireg tmp2 ireg tmp2;
             fprintf oc "	addq	%a, %a\n" ireg tmp2 ireg tmp1;
             fprintf oc "	jmp	*%a\n" ireg tmp1
           end else begin