diff options
30 files changed, 896 insertions, 43 deletions
@@ -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,39 +92,41 @@ 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} - advanced_debug=true;; - 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} + advanced_debug=true;; + 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 433beaeb..9d480ed5 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 00234f9b..9e22e4e0 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 (_0))); - 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 (* atomic operations *) | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ -> emit (Plwz (GPR10,Cint _0,a2)); @@ -598,6 +621,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)); @@ -605,6 +646,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 f94c3b64..20bec532 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 e65a8934..250686be 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". diff --git a/runtime/Makefile b/runtime/Makefile index 2fdaa4ec..99eeaa54 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -9,6 +9,16 @@ LIB=libcompcert.a INCLUDES=include/float.h include/stdarg.h include/stdbool.h \ include/stddef.h include/varargs.h +VPATH=$(ARCH) + +ifeq ($(ARCH),powerpc) +ifeq ($(MODEL),ppc64) +VPATH=powerpc/ppc64 $(ARCH) +else ifeq ($(MODEL),e5500) +VPATH=powerpc/ppc64 $(ARCH) +endif +endif + ifeq ($(strip $(HAS_RUNTIME_LIB)),true) all: $(LIB) else @@ -19,10 +29,10 @@ $(LIB): $(OBJS) rm -f $(LIB) ar rcs $(LIB) $(OBJS) -%.o: $(ARCH)/%.s +%.o: %.s $(CASMRUNTIME) -o $@ $^ -%.o: $(ARCH)/%.S +%.o: %.S $(CASMRUNTIME) -DMODEL_$(MODEL) -DABI_$(ABI) -DSYS_$(SYSTEM) -o $@ $^ clean:: diff --git a/runtime/powerpc/ppc64/i64_dtos.s b/runtime/powerpc/ppc64/i64_dtos.s new file mode 100644 index 00000000..95f7f700 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_dtos.s @@ -0,0 +1,52 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Conversion from double float to signed long + + .balign 16 + .globl __i64_dtos +__i64_dtos: + fctidz f1, f1 + stfdu f1, -16(r1) + lwz r3, 0(r1) + lwz r4, 4(r1) + addi r1, r1, 16 + blr + .type __i64_dtos, @function + .size __i64_dtos, .-__i64_dtos +
\ No newline at end of file diff --git a/runtime/powerpc/ppc64/i64_dtou.s b/runtime/powerpc/ppc64/i64_dtou.s new file mode 100644 index 00000000..60d5c9bf --- /dev/null +++ b/runtime/powerpc/ppc64/i64_dtou.s @@ -0,0 +1,66 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Conversion from double float to unsigned long + + .balign 16 + .globl __i64_dtou +__i64_dtou: + lis r0, 0x5f00 # 0x5f00_0000 = 2^63 in binary32 format + stwu r0, -16(r1) + lfs f2, 0(r1) # f2 = 2^63 + fcmpu cr0, f1, f2 # crbit 0 is f1 < f2 + bf 0, 1f # branch if f1 >= 2^63 (or f1 is NaN) + fctidz f1, f1 # convert as signed + stfd f1, 0(r1) + lwz r3, 0(r1) + lwz r4, 4(r1) + addi r1, r1, 16 + blr +1: fsub f1, f1, f2 # shift argument down by 2^63 + fctidz f1, f1 # convert as signed + stfd f1, 0(r1) + lwz r3, 0(r1) + lwz r4, 4(r1) + addis r3, r3, 0x8000 # shift result up by 2^63 + addi r1, r1, 16 + blr + .type __i64_dtou, @function + .size __i64_dtou, .-__i64_dtou + + diff --git a/runtime/powerpc/ppc64/i64_sar.s b/runtime/powerpc/ppc64/i64_sar.s new file mode 100644 index 00000000..4fc4451e --- /dev/null +++ b/runtime/powerpc/ppc64/i64_sar.s @@ -0,0 +1,51 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +# Shift right signed + + .balign 16 + .globl __i64_sar +__i64_sar: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + srad r4, r4, r5 + srdi r3, r4, 32 # split r4 into (r3,r4) + blr + .type __i64_sar, @function + .size __i64_sar, .-__i64_sar + +
\ No newline at end of file diff --git a/runtime/powerpc/ppc64/i64_sdiv.s b/runtime/powerpc/ppc64/i64_sdiv.s new file mode 100644 index 00000000..2bf5b574 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_sdiv.s @@ -0,0 +1,52 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Signed division + + .balign 16 + .globl __i64_sdiv +__i64_sdiv: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6 + divd r4, r4, r6 + srdi r3, r4, 32 # split r4 into (r3,r4) + blr + .type __i64_sdiv, @function + .size __i64_sdiv, .-__i64_sdiv + +
\ No newline at end of file diff --git a/runtime/powerpc/ppc64/i64_shl.s b/runtime/powerpc/ppc64/i64_shl.s new file mode 100644 index 00000000..955de565 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_shl.s @@ -0,0 +1,50 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +# Shift left + + .balign 16 + .globl __i64_shl +__i64_shl: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + sld r4, r4, r5 + srdi r3, r4, 32 # split r4 into (r3,r4) + blr + .type __i64_shl, @function + .size __i64_shl, .-__i64_shl +
\ No newline at end of file diff --git a/runtime/powerpc/ppc64/i64_shr.s b/runtime/powerpc/ppc64/i64_shr.s new file mode 100644 index 00000000..ca5ac9b2 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_shr.s @@ -0,0 +1,51 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +# Shift right unsigned + + .balign 16 + .globl __i64_shr +__i64_shr: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + srd r4, r4, r5 + srdi r3, r4, 32 # split r4 into (r3,r4) + blr + .type __i64_shr, @function + .size __i64_shr, .-__i64_shr + +
\ No newline at end of file diff --git a/runtime/powerpc/ppc64/i64_smod.s b/runtime/powerpc/ppc64/i64_smod.s new file mode 100644 index 00000000..35be366d --- /dev/null +++ b/runtime/powerpc/ppc64/i64_smod.s @@ -0,0 +1,54 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +## Signed remainder + + .balign 16 + .globl __i64_smod +__i64_smod: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6 + divd r0, r4, r6 + mulld r0, r0, r6 + subf r4, r0, r4 + srdi r3, r4, 32 # split r4 into (r3,r4) + blr + .type __i64_smod, @function + .size __i64_smod, .-__i64_smod + +
\ No newline at end of file diff --git a/runtime/powerpc/ppc64/i64_stod.s b/runtime/powerpc/ppc64/i64_stod.s new file mode 100644 index 00000000..3636d0b5 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_stod.s @@ -0,0 +1,50 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + +### Conversion from signed long to double float + + .balign 16 + .globl __i64_stod +__i64_stod: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + stdu r4, -16(r1) + lfd f1, 0(r1) + fcfid f1, f1 + addi r1, r1, 16 + blr + .type __i64_stod, @function + .size __i64_stod, .-__i64_stod + diff --git a/runtime/powerpc/ppc64/i64_stof.s b/runtime/powerpc/ppc64/i64_stof.s new file mode 100644 index 00000000..8830d594 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_stof.s @@ -0,0 +1,68 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Conversion from signed long to single float + + .balign 16 + .globl __i64_stof +__i64_stof: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + # Check whether -2^53 <= X < 2^53 + sradi r5, r4, 53 + addi r5, r5, 1 + cmpldi r5, 2 + blt 1f + # X is large enough that double rounding can occur. + # Avoid it by nudging X away from the points where double rounding + # occurs (the "round to odd" technique) + rldicl r5, r4, 0, 53 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-63 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X + rldicr r4, r4, 0, 52 # set to 0 bits 0 to 11 of X + # Convert to double, then round to single +1: stdu r4, -16(r1) + lfd f1, 0(r1) + fcfid f1, f1 + frsp f1, f1 + addi r1, r1, 16 + blr + .type __i64_stof, @function + .size __i64_stof, .-__i64_stof + diff --git a/runtime/powerpc/ppc64/i64_udiv.s b/runtime/powerpc/ppc64/i64_udiv.s new file mode 100644 index 00000000..a6a3bcb3 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_udiv.s @@ -0,0 +1,51 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Unsigned division + + .balign 16 + .globl __i64_udiv +__i64_udiv: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6 + divdu r4, r4, r6 + srdi r3, r4, 32 # split r4 into (r3,r4) + blr + .type __i64_udiv, @function + .size __i64_udiv, .-__i64_udiv + diff --git a/runtime/powerpc/ppc64/i64_umod.s b/runtime/powerpc/ppc64/i64_umod.s new file mode 100644 index 00000000..6bda1903 --- /dev/null +++ b/runtime/powerpc/ppc64/i64_umod.s @@ -0,0 +1,53 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Unsigned modulus + + .balign 16 + .globl __i64_umod +__i64_umod: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + rldimi r6, r5, 32, 0 # reassemble (r5,r6) as a 64-bit integer in r6 + divdu r0, r4, r6 + mulld r0, r0, r6 + subf r4, r0, r4 + srdi r3, r4, 32 # split r4 into (r3,r4) + blr + .type __i64_umod, @function + .size __i64_umod, .-__i64_umod + diff --git a/runtime/powerpc/ppc64/i64_utod.s b/runtime/powerpc/ppc64/i64_utod.s new file mode 100644 index 00000000..ddde91dd --- /dev/null +++ b/runtime/powerpc/ppc64/i64_utod.s @@ -0,0 +1,79 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the <organization> nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Conversion from unsigned long to double float + + .balign 16 + .globl __i64_utod +__i64_utod: + rldicl r3, r3, 0, 32 # clear top 32 bits + rldicl r4, r4, 0, 32 # clear top 32 bits + lis r5, 0x4f80 # 0x4f80_0000 = 2^32 in binary32 format + stdu r3, -32(r1) + std r4, 8(r1) + stw r5, 16(r1) + lfd f1, 0(r1) # high 32 bits of argument + lfd f2, 8(r1) # low 32 bits of argument + lfs f3, 16(r1) # 2^32 + fcfid f1, f1 # convert both 32-bit halves to FP (exactly) + fcfid f2, f2 + fmadd f1, f1, f3, f2 # compute hi * 2^32 + lo + addi r1, r1, 32 + blr + .type __i64_utod, @function + .size __i64_utod, .-__i64_utod + +# Alternate implementation using round-to-odd: +# rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 +# cmpdi r4, 0 # is r4 >= 2^63 ? +# blt 1f +# stdu r4, -16(r1) # r4 < 2^63: convert as signed +# lfd f1, 0(r1) +# fcfid f1, f1 +# addi r1, r1, 16 +# blr +#1: rldicl r0, r4, 0, 63 # extract low bit of r4 +# srdi r4, r4, 1 +# or r4, r4, r0 # round r4 to 63 bits, using round-to-odd +# stdu r4, -16(r1) # convert to binary64 +# lfd f1, 0(r1) +# fcfid f1, f1 +# fadd f1, f1, f1 # multiply result by 2 +# addi r1, r1, 16 +# blr +
\ No newline at end of file diff --git a/test/regression/Results/builtins-powerpc b/test/regression/Results/builtins-powerpc index 0fd07f69..b131e543 100644 --- a/test/regression/Results/builtins-powerpc +++ b/test/regression/Results/builtins-powerpc @@ -15,6 +15,8 @@ fsel(-3.141590, 2.718000, 1.414000) = 1.414000 fcti(3.141590) = 3 fcti(2.718000) = 3 fcti(1.414000) = 1 +isel(0, 305419896, -559038737) = -559038737 +isel(42, 305419896, -559038737) = 305419896 read_16_rev = 3412 read_32_rev = efbeadde after write_16_rev: 9a78 diff --git a/test/regression/builtins-powerpc.c b/test/regression/builtins-powerpc.c index 90030737..5cb2e293 100644 --- a/test/regression/builtins-powerpc.c +++ b/test/regression/builtins-powerpc.c @@ -41,6 +41,8 @@ int main(int argc, char ** argv) __builtin_eieio(); __builtin_sync(); __builtin_isync(); + printf("isel(%d, %d, %d) = %d\n", 0, x, y, __builtin_isel(0, x, y)); + printf("isel(%d, %d, %d) = %d\n", 42, x, y, __builtin_isel(42, x, y)); printf ("read_16_rev = %x\n", __builtin_read16_reversed(&s)); printf ("read_32_rev = %x\n", __builtin_read32_reversed(&y)); __builtin_write16_reversed(&s, 0x789A); |