diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 6 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 4 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 8 | ||||
-rw-r--r-- | powerpc/ConstpropOp.vp | 2 | ||||
-rw-r--r-- | powerpc/Op.v | 10 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 8 | ||||
-rw-r--r-- | powerpc/PrintOp.ml | 2 | ||||
-rw-r--r-- | powerpc/SelectOp.vp | 20 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 15 | ||||
-rw-r--r-- | powerpc/extractionMachdep.v | 3 |
10 files changed, 16 insertions, 62 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 2d71ca9..ea5e416 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -162,10 +162,8 @@ Inductive instruction : Type := | Pfcmpu: freg -> freg -> instruction (**r float comparison *) | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion *) | Pfdiv: freg -> freg -> freg -> instruction (**r float division *) - | Pfmadd: freg -> freg -> freg -> freg -> instruction (**r float multiply-add *) | Pfmake: freg -> ireg -> ireg -> instruction (**r build a float from 2 ints *) | Pfmr: freg -> freg -> instruction (**r float move *) - | Pfmsub: freg -> freg -> freg -> freg -> instruction (**r float multiply-sub *) | Pfmul: freg -> freg -> freg -> instruction (**r float multiply *) | Pfneg: freg -> freg -> instruction (**r float negation *) | Pfrsp: freg -> freg -> instruction (**r float round to single precision *) @@ -632,14 +630,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m | Pfdiv rd r1 r2 => OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m - | Pfmadd rd r1 r2 r3 => - OK (nextinstr (rs#rd <- (Val.addf (Val.mulf rs#r1 rs#r2) rs#r3))) m | Pfmake rd r1 r2 => OK (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m | Pfmr rd r1 => OK (nextinstr (rs#rd <- (rs#r1))) m - | Pfmsub rd r1 r2 r3 => - OK (nextinstr (rs#rd <- (Val.subf (Val.mulf rs#r1 rs#r2) rs#r3))) m | Pfmul rd r1 r2 => OK (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m | Pfneg rd r1 => diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index b166d34..f9e4b2c 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -394,10 +394,6 @@ Definition transl_op Pfmul (freg_of r) (freg_of a1) (freg_of a2) :: k | Odivf, a1 :: a2 :: nil => Pfdiv (freg_of r) (freg_of a1) (freg_of a2) :: k - | Omuladdf, a1 :: a2 :: a3 :: nil => - Pfmadd (freg_of r) (freg_of a1) (freg_of a2) (freg_of a3) :: k - | Omulsubf, a1 :: a2 :: a3 :: nil => - Pfmsub (freg_of r) (freg_of a1) (freg_of a2) (freg_of a3) :: k | Osingleoffloat, a1 :: nil => Pfrsp (freg_of r) (freg_of a1) :: k | Ointoffloat, a1 :: nil => diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 076288e..50b9be1 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -39,6 +39,14 @@ let builtins = { (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false); + "__builtin_fnmadd", + (TFloat(FDouble, []), + [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], + false); + "__builtin_fnmsub", + (TFloat(FDouble, []), + [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], + false); "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); "__builtin_frsqrte", diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index cb958d4..3298671 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -117,8 +117,6 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) := | Osubf, F n1 :: F n2 :: nil => F(Float.sub n1 n2) | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2) | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2) - | Omuladdf, F n1 :: F n2 :: F n3 :: nil => F(Float.add (Float.mul n1 n2) n3) - | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3) | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1) | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1 | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2) diff --git a/powerpc/Op.v b/powerpc/Op.v index 64e47e3..76c426b 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -94,8 +94,6 @@ Inductive operation : Type := | Osubf: operation (**r [rd = r1 - r2] *) | Omulf: operation (**r [rd = r1 * r2] *) | Odivf: operation (**r [rd = r1 / r2] *) - | Omuladdf: operation (**r [rd = r1 * r2 + r3] *) - | Omulsubf: operation (**r [rd = r1 * r2 - r3] *) | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) @@ -203,8 +201,6 @@ Definition eval_operation | Osubf, v1::v2::nil => Some(Val.subf v1 v2) | Omulf, v1::v2::nil => Some(Val.mulf v1 v2) | Odivf, v1::v2::nil => Some(Val.divf v1 v2) - | Omuladdf, v1::v2::v3::nil => Some(Val.addf (Val.mulf v1 v2) v3) - | Omulsubf, v1::v2::v3::nil => Some(Val.subf (Val.mulf v1 v2) v3) | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) | Ointoffloat, v1::nil => Val.intoffloat v1 | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2) @@ -292,8 +288,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) - | Omuladdf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat) - | Omulsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat) | Osingleoffloat => (Tfloat :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) @@ -366,8 +360,6 @@ Proof with (try exact I). destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... - destruct v0; destruct v1; destruct v2... - destruct v0; destruct v1; destruct v2... destruct v0... destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2... destruct v0; destruct v1... @@ -796,8 +788,6 @@ Proof. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. - inv H4; simpl; auto; inv H2; simpl; auto; inv H3; simpl; auto. - inv H4; simpl; auto; inv H2; simpl; auto; inv H3; simpl; auto. inv H4; simpl; auto. inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2. exists (Vint i); auto. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 8323d56..3492de4 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -476,6 +476,10 @@ let print_builtin_inline oc name args res = fprintf oc " fmadd %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 | "__builtin_fmsub", [FR a1; FR a2; FR a3], FR res -> fprintf oc " fmsub %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + | "__builtin_fnmadd", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fnmadd %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + | "__builtin_fnmsub", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fnmsub %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 | "__builtin_fabs", [FR a1], FR res -> fprintf oc " fabs %a, %a\n" freg res freg a1 | "__builtin_fsqrt", [FR a1], FR res -> @@ -636,8 +640,6 @@ let print_instruction oc tbl pc = function fprintf oc "%s end pseudoinstr fcti\n" comment | Pfdiv(r1, r2, r3) -> fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfmadd(r1, r2, r3, r4) -> - fprintf oc " fmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Pfmake(rd, r1, r2) -> fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n" comment freg rd ireg r1 ireg r2; @@ -648,8 +650,6 @@ let print_instruction oc tbl pc = function fprintf oc "%s end pseudoinstr fmake\n" comment | Pfmr(r1, r2) -> fprintf oc " fmr %a, %a\n" freg r1 freg r2 - | Pfmsub(r1, r2, r3, r4) -> - fprintf oc " fmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Pfmul(r1, r2, r3) -> fprintf oc " fmul %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfneg(r1, r2) -> diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 13eb4ae..5bc4658 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -93,8 +93,6 @@ let print_operation reg pp = function | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2 | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2 | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 - | Omuladdf, [r1;r2;r3] -> fprintf pp "%a *f %a +f %a" reg r1 reg r2 reg r3 - | Omulsubf, [r1;r2;r3] -> fprintf pp "%a *f %a -f %a" reg r1 reg r2 reg r3 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2 diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 943c400..d7944b6 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -370,24 +370,8 @@ Nondetfunction shru (e1: expr) (e2: expr) := Definition negf (e: expr) := Eop Onegf (e ::: Enil). Definition absf (e: expr) := Eop Oabsf (e ::: Enil). - -Parameter use_fused_mul : unit -> bool. - -Nondetfunction addf (e1: expr) (e2: expr) := - if negb(use_fused_mul tt) then Eop Oaddf (e1:::e2:::Enil) else - match e1, e2 with - | Eop Omulf (t1:::t2:::Enil), t3 => Eop Omuladdf (t1:::t2:::t3:::Enil) - | t1, Eop Omulf (t2:::t3:::Enil) => Eop Omuladdf (t2:::t3:::t1:::Enil) - | _, _ => Eop Oaddf (e1:::e2:::Enil) - end. - -Nondetfunction subf (e1: expr) (e2: expr) := - if negb(use_fused_mul tt) then Eop Osubf (e1:::e2:::Enil) else - match e1 with - | Eop Omulf (t1:::t2:::Enil) => Eop Omulsubf (t1:::t2:::e2:::Enil) - | _ => Eop Osubf (e1:::e2:::Enil) - end. - +Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). +Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 1d35d9f..27a0fd0 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -631,23 +631,12 @@ Qed. Theorem eval_addf: binary_constructor_sound addf Val.addf. Proof. - red; intros until y; unfold addf. - destruct (use_fused_mul tt); simpl. - case (addf_match a b); intros; InvEval. - TrivialExists. simpl. congruence. - TrivialExists. simpl. rewrite Val.addf_commut. congruence. - intros. TrivialExists. - intros. TrivialExists. + red; intros; TrivialExists. Qed. Theorem eval_subf: binary_constructor_sound subf Val.subf. Proof. - red; intros until y; unfold subf. - destruct (use_fused_mul tt); simpl. - case (subf_match a); intros; InvEval. - TrivialExists. simpl. congruence. - TrivialExists. - intros. TrivialExists. + red; intros; TrivialExists. Qed. Theorem eval_mulf: binary_constructor_sound mulf Val.mulf. diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index cb4c3c2..bc0184e 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -12,9 +12,6 @@ (* Additional extraction directives specific to the PowerPC port *) -(* Selection *) -Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". - (* Asm *) Extract Constant Asm.low_half => "fun _ -> assert false". Extract Constant Asm.high_half => "fun _ -> assert false". |