From 736b181a58c076475792bf815c6c06a814c7b5a8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 22 Aug 2026 15:08:12 +0200 Subject: [PATCH 1/4] 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 7aee5c296e82c026bf13514d4a9556441a0f85a1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 23 Aug 2026 11:25:14 +0200 Subject: [PATCH 2/4] 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 70077daf12314ca564bdd65449e714778b620f14 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 26 Aug 2026 15:40:30 +0200 Subject: [PATCH 3/4] RISC-V 64 `Pbtbl`: assert that the jump table contains less than 2^31 elements The index argument of Pbtbl is an unsigned 32-bit integer. However, RV64 stores it sign-extended in a 64-bit register. This could cause an incorrect access in the jump table if the index is 2^31 or more. However, this can only happen if the jump table itself has at least 2^31 entries, which is highly unlikely (a source C program that would produce such a huge table would itself be huge and CompCert would probably run out of memory compiling it). To be on the safe side, we just add a run-time assertion that the jump table is no bigger than 2^31 entries. --- riscV/TargetPrinter.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index f4cea9dda..6e38ec1ae 100644 --- a/riscV/TargetPrinter.ml +++ b/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; From 1e42571f7f905ec46a025ab594aa669f05a4c4e4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 27 Aug 2026 12:04:48 +0200 Subject: [PATCH 4/4] Change entry for #595 --- Changelog.md | 1 + 1 file changed, 1 insertion(+) diff --git a/Changelog.md b/Changelog.md index 453c92911..5ed65e600 100644 --- a/Changelog.md +++ b/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)