Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
xavierleroy merged 4 commits into from
Aug 27, 2026
+6 −2
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
736b181
x86-64 `Pjmptbl`: normalize the argument before indexing into the jum…
xavierleroy Aug 22, 2026
7aee5c2
Add non-regression test for the x86-64 `Pjmptbl` issue.
xavierleroy Aug 23, 2026
70077da
RISC-V 64 `Pbtbl`: assert that the jump table contains less than 2^31…
xavierleroy Aug 26, 2026
1e42571
Change entry for #595
xavierleroy Aug 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions riscV/TargetPrinter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion test
Open in desktop
Submodule test updated 2 files
+1 −0 regression/Results/switch
+3 −0 regression/switch.c
4 changes: 3 additions & 1 deletion x86/TargetPrinter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading