aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2023-01-06 11:06:44 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2023-02-20 13:29:07 +0100
commit431b64db94583fc5e8d08ecc9bd4e105567ed4d5 (patch)
tree74c5ac3194f06ab0e76b16603708f0e4a47218a4
parent2057282e475c72a14651c2ec4a66bfe0287a9d43 (diff)
downloadcompcert-431b64db94583fc5e8d08ecc9bd4e105567ed4d5.tar.gz
compcert-431b64db94583fc5e8d08ecc9bd4e105567ed4d5.zip
For Thumb, use `movs` for loading immediate constants
It is supported and produces shorter code than `mov`.
-rw-r--r--arm/TargetPrinter.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 953bc4f4..3f67dc24 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -277,9 +277,9 @@ struct
thumbS ireg r1 ireg r2 ireg r3
| Pmla(r1, r2, r3, r4) ->
fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4
- | Pmov(r1, (SOimm _ | SOreg _ as so)) ->
+ | Pmov(r1, SOreg reg) ->
(* No S flag even in Thumb2 mode *)
- fprintf oc " mov %a, %a\n" ireg r1 shift_op so
+ fprintf oc " mov %a, %a\n" ireg r1 ireg reg
| Pmov(r1, so) ->
fprintf oc " mov%t %a, %a\n" thumbS ireg r1 shift_op so
| Pmovw(r1, n) ->