diff options
| author | Valoran <valomay@protonmail.com> | 2023-04-05 19:37:20 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-04-05 19:37:20 +0200 |
| commit | 358230d26eb5d29cb12c6c16e4e4f60117647a23 (patch) | |
| tree | 47c7e4049fc5e3ab8916e3093d5bbf7c40663fad | |
| parent | f4ddce910894bf6dbdf83c0642c4b275854b60dd (diff) | |
| download | compcert-358230d26eb5d29cb12c6c16e4e4f60117647a23.tar.gz compcert-358230d26eb5d29cb12c6c16e4e4f60117647a23.zip | |
Use a shorter insruction on x86 for loading unsigned 32-bit immediates into 64-bit registers.(#487)
Writing into a 32-bit register erases the upper 32 bits of a 64-bit
register. This is the shortest instruction for loading unsigned
32-bit immediates. The length of those instructions is:
- movl: 5 bytes
- movq: 7 bytes
- movabsq: 10 bytes
Some assemblers will choose the proper instruction by themselves;
the GNU assembler does not, apparently. So it's better to make
the choice of instruction explicit.
| -rw-r--r-- | x86/TargetPrinter.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index a289127a..91e0b18e 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -432,7 +432,9 @@ module Target(System: SYSTEM):TARGET = | Pmovq_ri(rd, n) -> let n1 = camlint64_of_coqint n in let n2 = Int64.to_int32 n1 in - if n1 = Int64.of_int32 n2 then + if Int64.shift_right_logical n1 32 = Int64.zero then + fprintf oc " movl $%Ld, %a\n" n1 ireg32 rd + else if n1 = Int64.of_int32 n2 then fprintf oc " movq $%ld, %a\n" n2 ireg64 rd else fprintf oc " movabsq $%Ld, %a\n" n1 ireg64 rd |