diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-17 14:22:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-06-17 17:19:05 +0200 |
| commit | ed0cfe4b38208f15763f2d1c0372c441a320ea56 (patch) | |
| tree | 0b1d49bede1a0b9d3d1392809d354fefa5f695ef /riscV | |
| parent | 0a4e441a722c6aa9921ff47bd1a411e274e24047 (diff) | |
| download | compcert-ed0cfe4b38208f15763f2d1c0372c441a320ea56.tar.gz compcert-ed0cfe4b38208f15763f2d1c0372c441a320ea56.zip | |
Extended asm: print register names according to their types
When printing an extended asm code fragment, placeholders %n
are replaced by register names.
Currently we ignore the fact that some assemblers use different
register names depending on the width of the data that resides
in the register.
For example, x86_64 uses %rax for a 64-bit quantity and %eax for
a 32-bit quantity, but CompCert always prints %rax in extended asm
statements. This is problematic if we want to use 32-bit integer
instructions in extended asm, e.g.
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
produces
addl %rax, %rdx
which is syntactically incorrect.
Another example is ARM FP registers: D0 is a double-precision float,
but S0 is a single-precision float.
This commit partially solves this issue by taking into account the
Cminor type of the asm parameter when printing the corresponding register.
Continuing the previous example,
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
now produces
addl %eax, %edx
This is not perfect yet: we use Cminor types, because this is all we
have at hand, and not source C types, hence "char" and "short" parameters
are still printed like "int" parameters, which is not good for x86.
(I.e. we produce %eax where GCC might have produced %al or %ax.)
We'll leave this issue open.
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/TargetPrinter.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 92df7a76..64bcea4c 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -93,7 +93,7 @@ module Target : TARGET = | X0 -> output_string oc "x0" | X r -> ireg oc r - let preg oc = function + let preg_asm oc ty = function | IR r -> ireg oc r | FR r -> freg oc r | _ -> assert false @@ -582,7 +582,7 @@ module Target : TARGET = (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; + print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false |