From 5222d4cfa56c20bf0da05b61af122eaa00b24ad6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 22 Aug 2026 15:08:12 +0200 Subject: [PATCH 1/3] x86-64 `Pjmptbl`: normalize the argument before indexing into the jump table The index argument of Pjmptbl is an unsigned 32-bit integer, not a 64-bit integer, so it must be converted to 64 bits (by zeroing the top 32 bits) before it can be used as an index into the jump table. --- x86/TargetPrinter.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 3bc863f7d..397ebe78b 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -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 From 5f232ad2a5b31e2a733698faad4021feb531df7e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 23 Aug 2026 11:25:14 +0200 Subject: [PATCH 2/3] Add non-regression test for the x86-64 `Pjmptbl` issue. --- test | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test b/test index 27899bbab..4df7312a3 160000 --- a/test +++ b/test @@ -1 +1 @@ -Subproject commit 27899bbabecd10148c2a2f1b3b62f55b8edca556 +Subproject commit 4df7312a3ff71037c20856dfeff727e36c77848e From bc5a65ff14213f280d0ac647e012e2ecb483caef Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 23 Aug 2026 17:16:30 +0200 Subject: [PATCH 3/3] RISC-V 64 `Pbtbl`: normalize the argument before indexing into the jump table The index argument of Pbtbl is an unsigned 32-bit integer. However, RV64 stores it sign-extended in a 64-bit register. This can cause an incorrect access in the jump table in the unlikely case where the jump table has 2^31 entries or more. This commit uses two shifts instead of one so as to zero-extend the index while multiplying it by 4. --- riscV/TargetPrinter.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index f4cea9dda..1ca13ff36 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -522,10 +522,17 @@ module Target : TARGET = freg rd label lbl comment (camlfloat_of_coqfloat32 f) | Pbtbl(r, tbl) -> let lbl = new_label() in - fprintf oc "%s jumptable [ " comment; + fprintf oc "%s pseudoinstr btbl [ " comment; List.iter (fun l -> fprintf oc "%a " print_label l) tbl; fprintf oc "]\n"; - fprintf oc " sll x5, %a, 2\n" ireg r; + if Archi.ptr64 then begin + (* Zero-extend [r] (a 32-bit integer) to 64-bit + and multiply it by 4. *) + fprintf oc " sll x5, %a, 32\n" ireg r; + fprintf oc " srl x5, x5, 30\n" + end else begin + fprintf oc " sll x5, %a, 2\n" ireg r + end; fprintf oc " lla x31, %a\n" label lbl; fprintf oc " add x5, x31, x5\n"; fprintf oc " lw x5, 0(x5)\n";