diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-13 11:44:32 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-13 11:44:32 +0200 |
| commit | 378ac3925503e6efd24cc34796e85d95c031e72d (patch) | |
| tree | 98005d8fc2dfdd4b0e48aebbd3aaaa1c3b8adc0e /powerpc/extractionMachdep.v | |
| parent | 470f6402ea49a81a5c861fcce66cb05ebff977c1 (diff) | |
| download | compcert-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/extractionMachdep.v')
| -rw-r--r-- | powerpc/extractionMachdep.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index b448e3d2..b0f05536 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -23,3 +23,11 @@ Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data". Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y". Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". + +(* Choice of PPC variant *) +Extract Constant Archi.ppc64 => + "begin match Configuration.model with + | ""ppc64"" -> true + | ""e5500"" -> true + | _ -> false + end". |