From ae22df3c5ef0a60527ea85b83bb71e8c95a6ab9c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 07:59:11 +0200 Subject: Pmsub compiled --- mppa_k1c/Asmblockgen.v | 12 ++++++++++++ mppa_k1c/ExtValues.v | 16 ++++++++++++++++ mppa_k1c/Machregs.v | 3 +-- mppa_k1c/NeedOp.v | 19 +------------------ mppa_k1c/Op.v | 14 +------------- mppa_k1c/PostpassSchedulingOracle.ml | 12 +++++++----- mppa_k1c/SelectOp.vp | 4 ++++ mppa_k1c/SelectOpproof.v | 6 ++++++ mppa_k1c/ValueAOp.v | 2 -- 9 files changed, 48 insertions(+), 40 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 4cce7075..7be83962 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -558,6 +558,12 @@ Definition transl_op do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pmaddiw r1 r2 n ::i k) + | Omsub, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmsubw r1 r2 r3 ::i k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -686,6 +692,12 @@ Definition transl_op do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pmaddil r1 r2 n ::i k) + | Omsubl, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmsubl r1 r2 r3 ::i k) | Oabsf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfabsd rd rs ::i k) diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 1aa17458..0d56fd1c 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -131,3 +131,19 @@ Definition val_shrxl (v1 v2: val): val := else Vundef | _, _ => Vundef end. + +Lemma sub_add_neg : + forall x y, Val.sub x y = Val.add x (Val.neg y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int.sub_add_opp. +Qed. + +Lemma neg_mul_distr_r : + forall x y, Val.neg (Val.mul x y) = Val.mul x (Val.neg y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int.neg_mul_distr_r. +Qed. \ No newline at end of file diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 6e0efe28..db3dfe64 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -215,8 +215,7 @@ Definition two_address_op (op: operation) : bool := match op with | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ - | Omsub | Omsubimm _ - | Omsubl | Omsublimm _ + | Omsub | Omsubl | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index ced31758..5ba9851f 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -78,7 +78,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Omadd => op3 (modarith nv) | Omaddimm n => op2 (modarith nv) | Omsub => op3 (modarith nv) - | Omsubimm n => op2 (modarith nv) | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocast32signed => op1 (default nv) @@ -120,7 +119,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Omaddl => op3 (default nv) | Omaddlimm n => op2 (default nv) | Omsubl => op3 (default nv) - | Omsublimm n => op2 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) @@ -457,14 +455,6 @@ Remark default_idem: forall nv, default (default nv) = default nv. Proof. destruct nv; simpl; trivial. Qed. - -Remark sub_add_neg : - forall x y, Val.sub x y = Val.add x (Val.neg y). -Proof. - destruct x; destruct y; simpl; trivial. - f_equal. - apply Int.sub_add_opp. -Qed. Lemma needs_of_operation_sound: forall op args v nv args', @@ -508,19 +498,12 @@ Proof. (* madd *) - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. -- repeat rewrite sub_add_neg. - apply add_sound; trivial. - apply neg_sound; trivial. - rewrite modarith_idem. - apply mul_sound; - rewrite modarith_idem; trivial. -- repeat rewrite sub_add_neg. +- repeat rewrite ExtValues.sub_add_neg. apply add_sound; trivial. apply neg_sound; trivial. rewrite modarith_idem. apply mul_sound; rewrite modarith_idem; trivial. - apply vagree_same. (* maddl *) - apply addl_sound; trivial. apply mull_sound; trivial. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index fb6c454c..ac40c293 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -122,7 +122,6 @@ Inductive operation : Type := | Omadd (**r [rd = rd + r1 * r2] *) | Omaddimm (n: int) (**r [rd = rd + r1 * imm] *) | Omsub (**r [rd = rd - r1 * r2] *) - | Omsubimm (n: int) (**r [rd = rd - r1 * imm] *) (*c 64-bit integer arithmetic: *) | Omakelong (**r [rd = r1 << 32 | r2] *) | Olowlong (**r [rd = low-word(r1)] *) @@ -173,7 +172,6 @@ Inductive operation : Type := | Omaddl (**r [rd = rd + r1 * r2] *) | Omaddlimm (n: int64) (**r [rd = rd + r1 * imm] *) | Omsubl (**r [rd = rd - r1 * r2] *) - | Omsublimm (n: int64) (**r [rd = rd - r1 * imm] *) (*c Floating-point arithmetic: *) | Onegf (**r [rd = - r1] *) | Oabsf (**r [rd = abs(r1)] *) @@ -448,7 +446,6 @@ Definition eval_operation | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3)) | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n))) | Omsub, v1::v2::v3::nil => Some (Val.sub v1 (Val.mul v2 v3)) - | (Omsubimm n), v1::v2::nil => Some (Val.sub v1 (Val.mul v2 (Vint n))) | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2) | Olowlong, v1::nil => Some (Val.loword v1) @@ -499,7 +496,6 @@ Definition eval_operation | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3)) | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n))) | Omsubl, v1::v2::v3::nil => Some (Val.subl v1 (Val.mull v2 v3)) - | (Omsublimm n), v1::v2::nil => Some (Val.subl v1 (Val.mull v2 (Vlong n))) | Onegf, v1::nil => Some (Val.negf v1) | Oabsf, v1::nil => Some (Val.absf v1) @@ -659,7 +655,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omadd => (Tint :: Tint :: Tint :: nil, Tint) | Omaddimm _ => (Tint :: Tint :: nil, Tint) | Omsub => (Tint :: Tint :: Tint :: nil, Tint) - | Omsubimm _ => (Tint :: Tint :: nil, Tint) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) @@ -710,7 +705,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong) | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong) | Omsubl => (Tlong :: Tlong :: Tlong :: nil, Tlong) - | Omsublimm _ => (Tlong :: Tlong :: nil, Tlong) | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) @@ -905,7 +899,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_add. (* msub *) - apply type_sub. - - apply type_sub. (* makelong, lowlong, highlong *) - destruct v0; destruct v1... - destruct v0... @@ -982,8 +975,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* maddl, maddlim *) - apply type_addl. - apply type_addl. - (* msubl, msublim *) - - apply type_subl. + (* msubl *) - apply type_subl. (* negf, absf *) - destruct v0... @@ -1528,8 +1520,6 @@ Proof. (* msub *) - apply Val.sub_inject; auto. inv H3; inv H2; simpl; auto. - - apply Val.sub_inject; trivial. - inv H2; inv H4; simpl; auto. (* makelong, highlong, lowlong *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1621,8 +1611,6 @@ Proof. (* msubl, msublimm *) - apply Val.subl_inject; auto. inv H2; inv H3; inv H4; simpl; auto. - - apply Val.subl_inject; auto. - inv H4; inv H2; simpl; auto. (* negf, absf *) - inv H4; simpl; auto. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 9dc1ab44..f428fe49 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -464,7 +464,7 @@ type real_instruction = | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Srsd | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd - | Maddw | Maddd | Cmoved + | Maddw | Maddd | Msbfw | Msbfd | Cmoved | Make | Nop | Extfz | Extfs | Insf (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo @@ -505,6 +505,7 @@ let ab_inst_to_real = function | "Psllw" | "Pslliw" -> Sllw | "Proriw" -> Rorw | "Pmaddw" | "Pmaddiw" -> Maddw + | "Pmsubw" | "Pmsubiw" -> Msbfw | "Pslll" | "Psllil" -> Slld | "Pxorw" | "Pxoriw" -> Xorw | "Pnxorw" | "Pnxoriw" -> Nxorw @@ -514,7 +515,8 @@ let ab_inst_to_real = function | "Pnxorl" | "Pnxoril" -> Nxord | "Pandnl" | "Pandnil" -> Andnd | "Pornl" | "Pornil" -> Ornd - | "Pmaddl" -> Maddd + | "Pmaddl" | "Pmaddil" -> Maddd + | "Pmsubl" | "Pmsubil" -> Msbfd | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop | "Pextfz" | "Pextfzl" | "Pzxwd" -> Extfz @@ -608,10 +610,10 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y | _ -> raise InvalidEncoding) - | Mulw| Maddw -> (match encoding with None -> mau + | Mulw| Maddw | Msbfw -> (match encoding with None -> mau | Some U6 | Some S10 | Some U27L5 -> mau_x | _ -> raise InvalidEncoding) - | Muld | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau + | Muld | Maddd | Msbfd -> (match encoding with None | Some U6 | Some S10 -> mau | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop @@ -644,7 +646,7 @@ let real_inst_to_latency = function | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 - | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) + | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3 | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See k1c-Optimization.pdf page 19 *) | Get -> 1 diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 6adcebe5..81e288cb 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -151,6 +151,10 @@ Nondetfunction sub (e1: expr) (e2: expr) := addimm n1 (Eop Osub (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) + | t1, (Eop Omul (t2:::t3:::Enil)) => + Eop Omsub (t1:::t2:::t3:::Enil) + | t1, (Eop (Omulimm n) (t2:::Enil)) => + Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) | _, _ => Eop Osub (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 9e2eec8b..17024826 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -251,6 +251,12 @@ Proof. apply eval_addimm; EvalOp. - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. - subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp. + - TrivialExists. simpl. subst. reflexivity. + - TrivialExists. simpl. subst. + rewrite sub_add_neg. + rewrite neg_mul_distr_r. + unfold Val.neg. + reflexivity. - TrivialExists. Qed. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 00e8a1d8..adc27010 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -204,7 +204,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3) | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n)) | Omsub, v1::v2::v3::nil => sub v1 (mul v2 v3) - | Omsubimm n, v1::v2::nil => sub v1 (mul v2 (I n)) | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 @@ -254,7 +253,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3) | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n)) | Omsubl, v1::v2::v3::nil => subl v1 (mull v2 v3) - | Omsublimm n, v1::v2::nil => subl v1 (mull v2 (L n)) | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 -- cgit