diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-02-18 17:46:50 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-02-18 17:46:50 +0100 |
| commit | 4bd80095720ca873b6ded9b169bbc6a8be9e11d7 (patch) | |
| tree | ca50d8574f65083a8d4b4964c66a4d8bc98573f4 | |
| parent | 86cc275b2b0b6e89d2b9e5b476e6a10163a8ed42 (diff) | |
| download | compcert-kvx-4bd80095720ca873b6ded9b169bbc6a8be9e11d7.tar.gz compcert-kvx-4bd80095720ca873b6ded9b169bbc6a8be9e11d7.zip | |
Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode.
Two reasons:
- The movs is not supported if rd or rs is r13 (the stack ptr register).
Newer versions of GNU as reject it, older versions were probably
emulating it.
- The purpose of setting the "s" flag on some operations is to
enable 16-bit encoding in Thumb2 mode. However, for "mov"
it is the non-s form that has a 16-bit encoding; the s form
is never more compact.
| -rw-r--r-- | arm/TargetPrinter.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 22d41c4d..6536bc55 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -126,11 +126,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = eor lsl lsr - mov mvn orr rsb sub (but not sp - imm) + On the other hand, "mov rd, rs" and "mov rd, #imm" have shorter + encodings if they do not have the "S" flag. Moreover, the "S" + flag is not supported if rd or rs is sp. + The proof of Asmgen shows that CompCert-generated code behaves the same whether flags are updated or not by those instructions. The following printing function adds a "S" suffix if we are in Thumb2 @@ -320,7 +323,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_int64_arith oc conflict rl fn = if conflict then begin let n = fn IR14 in - fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14; + fprintf oc " mov %a, %a\n" ireg rl ireg IR14; n + 1 end else fn rl @@ -551,6 +554,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = thumbS ireg r1 ireg r2 ireg r3; 1 | Pmla(r1, r2, r3, r4) -> fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 + | Pmov(r1, (SOimm _ | SOreg _ as so)) -> + (* No S flag even in Thumb2 mode *) + fprintf oc " mov %a, %a\n" ireg r1 shift_op so; 1 | Pmov(r1, so) -> fprintf oc " mov%t %a, %a\n" thumbS ireg r1 shift_op so; 1 | Pmovw(r1, n) -> |