From 378ac3925503e6efd24cc34796e85d95c031e72d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 13 Sep 2015 11:44:32 +0200 Subject: 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-". --- configure | 58 +++++++++++++++++++++++++-------------------- powerpc/Archi.v | 4 ++++ powerpc/Asm.v | 19 +++++++++++++++ powerpc/AsmToJSON.ml | 8 +++++++ powerpc/Asmexpand.ml | 53 +++++++++++++++++++++++++++++++++++++++-- powerpc/Asmgen.v | 9 +++++++ powerpc/Asmgenproof1.v | 12 ++++++++++ powerpc/Machregs.v | 2 +- powerpc/NeedOp.v | 2 +- powerpc/Op.v | 16 +++++++++++++ powerpc/SelectOp.vp | 25 +++++++++++-------- powerpc/SelectOpproof.v | 6 +++++ powerpc/TargetPrinter.ml | 17 +++++++++++++ powerpc/ValueAOp.v | 3 +++ powerpc/extractionMachdep.v | 8 +++++++ 15 files changed, 202 insertions(+), 40 deletions(-) diff --git a/configure b/configure index b906e38f..9646449e 100755 --- a/configure +++ b/configure @@ -38,6 +38,10 @@ Supported targets: ia32-cygwin (x86 32 bits, Cygwin environment under Windows) manual (edit configuration file by hand) +For PowerPC targets, the "ppc-" prefix can be refined into: + ppc64- PowerPC 64 bits + e5500- FreeCell e5500 core (PowerPC 64 bits + EREF extensions) + For ARM targets, the "arm-" prefix can be refined into: armv6- ARMv6 + VFPv2 armv7a- ARMv7-A + VFPv3-d16 (default) @@ -88,38 +92,40 @@ struct_passing="" struct_return="" case "$target" in - powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi) + powerpc-*|ppc-*|powerpc64-*|ppc64-*|e5500-*) arch="powerpc" - model="standard" + case "$target" in + powerpc64-*|ppc64-*) model="ppc64";; + e5500-*) model="e5500";; + *) model="ppc32";; + esac abi="eabi" struct_passing="ref-caller" case "$target" in *-linux) struct_return="ref";; - *-eabi) struct_return="int1-8";; + *) struct_return="int1-8";; esac - system="linux" - cc="${toolprefix}gcc" - cprepro="${toolprefix}gcc -std=c99 -U__GNUC__ -E" - casm="${toolprefix}gcc -c" - casmruntime="${toolprefix}gcc -c -Wa,-mregnames" - clinker="${toolprefix}gcc" - libmath="-lm" - cchecklink=${build_checklink};; - powerpc-eabi-diab|ppc-eabi-diab) - arch="powerpc" - model="standard" - abi="eabi" - struct_passing="ref-caller" - struct_return="int1-8" - system="diab" - cc="${toolprefix}dcc" - cprepro="${toolprefix}dcc -E -D__GNUC__" - casm="${toolprefix}das" - asm_supports_cfi=false - clinker="${toolprefix}dcc" - libmath="-lm" - cchecklink=${build_checklink} - advanced_debug=true;; + case "$target" in + *-eabi-diab) + system="diab" + cc="${toolprefix}dcc" + cprepro="${toolprefix}dcc -E -D__GNUC__" + casm="${toolprefix}das" + asm_supports_cfi=false + clinker="${toolprefix}dcc" + libmath="-lm" + cchecklink=${build_checklink} + advanced_debug=true;; + *) + system="linux" + cc="${toolprefix}gcc" + cprepro="${toolprefix}gcc -std=c99 -U__GNUC__ -E" + casm="${toolprefix}gcc -c" + casmruntime="${toolprefix}gcc -c -Wa,-mregnames" + clinker="${toolprefix}gcc" + libmath="-lm" + cchecklink=${build_checklink};; + esac;; arm*-*) arch="arm" case "$target" in diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 058b057f..cf1a0fe3 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -43,3 +43,7 @@ Global Opaque big_endian default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. + +(** Can we use the 64-bit extensions to the PowerPC architecture? *) +Parameter ppc64: bool. + diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 3c7bdd15..c1cc1052 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -178,13 +178,19 @@ Inductive instruction : Type := | Peqv: ireg -> ireg -> ireg -> instruction (**r bitwise not-xor *) | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) + | Pextsw: ireg -> ireg -> instruction (**r 64-bit sign extension (PPC64) *) | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame (pseudo) *) | Pfabs: freg -> freg -> instruction (**r float absolute value *) | Pfabss: freg -> freg -> instruction (**r float absolute value *) | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfadds: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) + | Pfcfi: freg -> ireg -> instruction (**r signed-int-to-float conversion (pseudo, PPC64) *) + | Pfcfiu: freg -> ireg -> instruction (**r unsigned-int-to-float conversion (pseudo, PPC64) *) + | Pfcfid: freg -> freg -> instruction (**r signed-long-to-float conversion (PPC64) *) | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo) *) + | Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *) + | Pfctidz: freg -> freg -> instruction (**r float-to-signed-long conversion, round towards 0 (PPC64) *) | Pfctiw: freg -> freg -> instruction (**r float-to-signed-int conversion, round by default *) | Pfctiwz: freg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 *) | Pfdiv: freg -> freg -> freg -> instruction (**r float division *) @@ -252,6 +258,7 @@ Inductive instruction : Type := | Porc: ireg -> ireg -> ireg -> instruction (**r bitwise or-complement *) | Pori: ireg -> ireg -> constant -> instruction (**r or with immediate *) | Poris: ireg -> ireg -> constant -> instruction (**r or with immediate high *) + | Prldicl: ireg -> ireg -> int -> int -> instruction (**r rotate and mask left (PPC64) *) | Prlwinm: ireg -> ireg -> int -> int -> instruction (**r rotate and mask *) | Prlwimi: ireg -> ireg -> int -> int -> instruction (**r rotate and insert *) | Pslw: ireg -> ireg -> ireg -> instruction (**r shift left *) @@ -260,6 +267,7 @@ Inductive instruction : Type := | Psrw: ireg -> ireg -> ireg -> instruction (**r shift right unsigned *) | Pstb: ireg -> constant -> ireg -> instruction (**r store 8-bit int *) | Pstbx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) + | Pstdu: ireg -> constant -> ireg -> instruction (**r store 64-bit integer with update (PPC64) *) | Pstfd: freg -> constant -> ireg -> instruction (**r store 64-bit float *) | Pstfdu: freg -> constant -> ireg -> instruction (**r store 64-bit float with update *) | Pstfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) @@ -716,8 +724,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m | Pfcmpu r1 r2 => Next (nextinstr (compare_float rs rs#r1 rs#r2)) m + | Pfcfi rd r1 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m + | Pfcfiu rd r1 => + Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m | Pfcti rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m + | Pfctiu rd r1 => + Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m | Pfdiv rd r1 r2 => Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m | Pfdivs rd r1 r2 => @@ -883,7 +897,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pdcbtst _ _ _ | Pdcbtls _ _ _ | Pdcbz _ _ + | Pextsw _ _ | Peieio + | Pfcfid _ _ + | Pfctidz _ _ | Pfctiw _ _ | Pfctiwz _ _ | Pfmadd _ _ _ _ @@ -907,6 +924,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmfcr _ | Pmfspr _ _ | Pmtspr _ _ + | Prldicl _ _ _ _ + | Pstdu _ _ _ | Pstwbrx _ _ _ | Pstwcx_ _ _ _ | Pstfdu _ _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index a7e66701..d82b9730 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -188,13 +188,19 @@ let p_instruction oc ic = | Peqv (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Peqv\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pextsb (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsb\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pextsh (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsh\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pextsw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pfreeframe (c,i) -> assert false (* Should not occur *) | Pfabs (fr1,fr2) | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfadd (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadd\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfadds (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadds\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfcmpu (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfcmpu\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfcfi (ir,fr) -> assert false (* Should not occur *) + | Pfcfid (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfcfid\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfcfiu (ir,fr) -> assert false (* Should not occur *) | Pfcti (ir,fr) -> assert false (* Should not occur *) + | Pfctiu (ir,fr) -> assert false (* Should not occur *) + | Pfctidz (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctidz\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfctiw (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiw\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfctiwz (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiwz\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfdiv (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdiv\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 @@ -263,6 +269,7 @@ let p_instruction oc ic = | Porc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Porc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Poris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Poris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Prldicl (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prldicl\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2 | Prlwinm (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwinm\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2 | Prlwimi (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwimi\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2 | Pslw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pslw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 @@ -271,6 +278,7 @@ let p_instruction oc ic = | Psrw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstb (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstdu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstdu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Pstfd (fr,c,ir) | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 3fffc037..49f796ca 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -23,6 +23,13 @@ open Asmexpandaux exception Error of string +(* FreeScale's EREF extensions *) + +let eref = + match Configuration.model with + | "e5500" -> true + | _ -> false + (* Useful constants and helper functions *) let _0 = Integers.Int.zero @@ -485,8 +492,24 @@ let expand_builtin_inline name args res = emit (Plwz (res, Cint! retaddr_offset,GPR1)) (* isel *) | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> - emit (Pcmpwi (a1,Cint (Int.zero))); - emit (Pisel (res,a3,a2,CRbit_2)) + if eref then begin + emit (Pcmpwi (a1,Cint (Int.zero))); + emit (Pisel (res,a3,a2,CRbit_2)) + end else if a2 = a3 then + emit (Pmr (res, a2)) + else begin + (* a1 has type _Bool, hence it is 0 or 1 *) + emit (Psubfic (GPR0, a1, Cint _0)); + (* r0 = 0xFFFF_FFFF if a1 is true, r0 = 0 if a1 is false *) + if res <> a3 then begin + emit (Pand_ (res, a2, GPR0)); + emit (Pandc (GPR0, a3, GPR0)) + end else begin + emit (Pandc (res, a3, GPR0)); + emit (Pand_ (GPR0, a2, GPR0)) + end; + emit (Por (res, res, GPR0)) + end (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -547,6 +570,24 @@ let expand_instruction instr = emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz))) else emit (Plwz(GPR1, Cint ofs, GPR1)) + | Pfcfi(r1, r2) -> + assert (Archi.ppc64); + emit (Pextsw(GPR0, r2)); + emit (Pstdu(GPR0, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plfd(r1, Cint _0, GPR1)); + emit (Pfcfid(r1, r1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) + | Pfcfiu(r1, r2) -> + assert (Archi.ppc64); + emit (Prldicl(GPR0, r2, _0, coqint_of_camlint 32l)); + emit (Pstdu(GPR0, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plfd(r1, Cint _0, GPR1)); + emit (Pfcfid(r1, r1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) | Pfcti(r1, r2) -> emit (Pfctiwz(FPR13, r2)); emit (Pstfdu(FPR13, Cint _m8, GPR1)); @@ -554,6 +595,14 @@ let expand_instruction instr = emit (Plwz(r1, Cint _4, GPR1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) + | Pfctiu(r1, r2) -> + assert (Archi.ppc64); + emit (Pfctidz(FPR13, r2)); + emit (Pstfdu(FPR13, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plwz(r1, Cint _4, GPR1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) | Pfmake(rd, r1, r2) -> emit (Pstwu(r1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index db3b7028..fe3a6441 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -496,6 +496,15 @@ Definition transl_op | Ointoffloat, a1 :: nil => do r1 <- freg_of a1; do r <- ireg_of res; OK (Pfcti r r1 :: k) + | Ointuoffloat, a1 :: nil => + do r1 <- freg_of a1; do r <- ireg_of res; + OK (Pfctiu r r1 :: k) + | Ofloatofint, a1 :: nil => + do r1 <- ireg_of a1; do r <- freg_of res; + OK (Pfcfi r r1 :: k) + | Ofloatofintu, a1 :: nil => + do r1 <- ireg_of a1; do r <- freg_of res; + OK (Pfcfiu r r1 :: k) | Ofloatofwords, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res; OK (Pfmake r r1 r2 :: k) diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index cb94c555..25e8bf07 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -941,6 +941,18 @@ Opaque Val.add. replace v with (Val.maketotal (Val.intoffloat (rs x))). TranslOpSimpl. rewrite H1; auto. + (* Ointuoffloat *) + replace v with (Val.maketotal (Val.intuoffloat (rs x))). + TranslOpSimpl. + rewrite H1; auto. + (* Ofloatofint *) + replace v with (Val.maketotal (Val.floatofint (rs x))). + TranslOpSimpl. + rewrite H1; auto. + (* Ofloatofintu *) + replace v with (Val.maketotal (Val.floatofintu (rs x))). + TranslOpSimpl. + rewrite H1; auto. (* Ocmp *) destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto. exists rs'; auto with asmgen. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index a2017dca..e4006523 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -134,7 +134,7 @@ Definition destroyed_by_op (op: operation): list mreg := match op with | Ofloatconst _ => R12 :: nil | Osingleconst _ => R12 :: nil - | Ointoffloat => F13 :: nil + | Ointoffloat | Ointuoffloat => F13 :: nil | _ => nil end. diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index e1307492..71c16ab9 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -56,7 +56,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Osingleoffloat | Ofloatofsingle => op1 (default nv) - | Ointoffloat => op1 (default nv) + | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) | Ofloatofwords | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocmp c => needs_of_condition c diff --git a/powerpc/Op.v b/powerpc/Op.v index 3ff08791..6866b086 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -107,6 +107,9 @@ Inductive operation : Type := | Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) + | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] (PPC64 only) *) + | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] (PPC64 only) *) + | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] (PPC64 only *) | Ofloatofwords: operation (**r [rd = float_of_words(r1,r2)] *) (*c Manipulating 64-bit integers: *) | Omakelong: operation (**r [rd = r1 << 32 | r2] *) @@ -231,6 +234,9 @@ Definition eval_operation | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 + | Ointuoffloat, v1::nil => Val.intuoffloat v1 + | Ofloatofint, v1::nil => Val.floatofint v1 + | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2) | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) | Olowlong, v1::nil => Some(Val.loword v1) @@ -332,6 +338,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) + | Ointuoffloat => (Tfloat :: nil, Tint) + | Ofloatofint => (Tint :: nil, Tfloat) + | Ofloatofintu => (Tint :: nil, Tfloat) | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) @@ -420,6 +429,9 @@ Proof with (try exact I). destruct v0... destruct v0... destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... + destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2... + destruct v0; simpl in H0; inv H0... + destruct v0; simpl in H0; inv H0... destruct v0; destruct v1... destruct v0; destruct v1... destruct v0... @@ -783,6 +795,10 @@ Proof. inv H4; simpl; auto. inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. + inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. + exists (Vint i); auto. + inv H4; simpl in H1; inv H1; simpl. TrivialExists. + inv H4; simpl in H1; inv H1; simpl. TrivialExists. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 6d39569e..a1fcecc7 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -466,19 +466,23 @@ Nondetfunction cast16signed (e: expr) := Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := - Elet e - (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) - (intoffloat (Eletvar 1)) - (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. + if Archi.ppc64 then + Eop Ointuoffloat (e ::: Enil) + else + Elet e + (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) + (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (intoffloat (Eletvar 1)) + (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. Nondetfunction floatofintu (e: expr) := match e with | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil | _ => - subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) - (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) + if Archi.ppc64 then Eop Ofloatofintu (e ::: Enil) else + subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) + (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) end. Nondetfunction floatofint (e: expr) := @@ -486,9 +490,10 @@ Nondetfunction floatofint (e: expr) := | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil | _ => - subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil - ::: addimm Float.ox8000_0000 e ::: Enil)) - (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil) + if Archi.ppc64 then Eop Ofloatofint (e ::: Enil) else + subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil + ::: addimm Float.ox8000_0000 e ::: Enil)) + (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil) end. Definition intofsingle (e: expr) := diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 147132dd..ad1adc47 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -838,6 +838,8 @@ Proof. intros. destruct x; simpl in H0; try discriminate. destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. + destruct Archi.ppc64. + econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto. set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). @@ -875,6 +877,8 @@ Theorem eval_floatofint: Proof. intros until y. unfold floatofint. destruct (floatofint_match a); intros. InvEval. TrivialExists. + destruct Archi.ppc64. + TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_int i)); split; auto. set (t1 := addimm Float.ox8000_0000 a). @@ -897,6 +901,8 @@ Theorem eval_floatofintu: Proof. intros until y. unfold floatofintu. destruct (floatofintu_match a); intros. InvEval. TrivialExists. + destruct Archi.ppc64. + TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_intu i)); split; auto. unfold floatofintu. 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) -> diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index 8cb29145..bcd1e80e 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -102,6 +102,9 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 + | Ointuoffloat, v1::nil => intuoffloat v1 + | Ofloatofint, v1::nil => floatofint v1 + | Ofloatofintu, v1::nil => floatofintu v1 | Ofloatofwords, v1::v2::nil => floatofwords v1 v2 | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 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". -- cgit