aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/TargetPrinter.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-09-13 11:44:32 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-09-13 11:44:32 +0200
commit378ac3925503e6efd24cc34796e85d95c031e72d (patch)
tree98005d8fc2dfdd4b0e48aebbd3aaaa1c3b8adc0e /powerpc/TargetPrinter.ml
parent470f6402ea49a81a5c861fcce66cb05ebff977c1 (diff)
downloadcompcert-kvx-378ac3925503e6efd24cc34796e85d95c031e72d.tar.gz
compcert-kvx-378ac3925503e6efd24cc34796e85d95c031e72d.zip
Use PowerPC 64 bits instructions (when available) for int<->FP conversions.
Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
Diffstat (limited to 'powerpc/TargetPrinter.ml')
-rw-r--r--powerpc/TargetPrinter.ml17
1 files changed, 17 insertions, 0 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index eca7a1b8..bc990de5 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -484,6 +484,8 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " extsb %a, %a\n" ireg r1 ireg r2
| Pextsh(r1, r2) ->
fprintf oc " extsh %a, %a\n" ireg r1 ireg r2
+ | Pextsw(r1, r2) ->
+ fprintf oc " extsw %a, %a\n" ireg r1 ireg r2
| Pfreeframe(sz, ofs) ->
assert false
| Pfabs(r1, r2) | Pfabss(r1, r2) ->
@@ -494,8 +496,18 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3
| Pfcmpu(r1, r2) ->
fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2
+ | Pfcfi(r1, r2) ->
+ assert false
+ | Pfcfid(r1, r2) ->
+ fprintf oc " fcfid %a, %a\n" freg r1 freg r2
+ | Pfcfiu(r1, r2) ->
+ assert false
| Pfcti(r1, r2) ->
assert false
+ | Pfctidz(r1, r2) ->
+ fprintf oc " fctidz %a, %a\n" freg r1 freg r2
+ | Pfctiu(r1, r2) ->
+ assert false
| Pfctiw(r1, r2) ->
fprintf oc " fctiw %a, %a\n" freg r1 freg r2
| Pfctiwz(r1, r2) ->
@@ -628,6 +640,9 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " ori %a, %a, %a\n" ireg r1 ireg r2 constant c
| Poris(r1, r2, c) ->
fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c
+ | Prldicl(r1, r2, c1, c2) ->
+ fprintf oc " rldicl %a, %a, %ld, %ld\n"
+ ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2)
| Prlwinm(r1, r2, c1, c2) ->
let (mb, me) = rolm_mask (camlint_of_coqint c2) in
fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n"
@@ -650,6 +665,8 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " stb %a, %a(%a)\n" ireg r1 constant c ireg r2
| Pstbx(r1, r2, r3) ->
fprintf oc " stbx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
+ | Pstdu(r1, c, r2) ->
+ fprintf oc " stdu %a, %a(%a)\n" ireg r1 constant c ireg r2
| Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) ->
fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2
| Pstfdu(r1, c, r2) ->