Pmsub compiled

9 files changed, 48 insertions, 40 deletions

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