mul immediate

6 files changed, 18 insertions, 3 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 1646ff94..ba01883d 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -85,6 +85,7 @@ Definition opimm32 (op: arith_name_rrr)
   end.
 
 Definition addimm32 := opimm32 Paddw Paddiw.
+Definition mulimm32 := opimm32 Pmulw Pmuliw.
 Definition andimm32 := opimm32 Pandw Pandiw.
 Definition nandimm32 := opimm32 Pnandw Pnandiw.
 Definition orimm32  := opimm32 Porw Poriw.
@@ -109,6 +110,7 @@ Definition opimm64 (op: arith_name_rrr)
 end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
+Definition mulimm64 := opimm64 Pmull Pmulil.
 Definition orimm64  := opimm64 Porl  Poril.
 Definition andimm64 := opimm64 Pandl Pandil.
 Definition xorimm64 := opimm64 Pxorl  Pxoril.
@@ -420,6 +422,9 @@ Definition transl_op
   | Omul, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pmulw rd rs1 rs2 ::i k)
+  | Omulimm n, a1 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1;
+      OK (mulimm32 rd rs1 n ::i k)
   | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *)
   | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *)
   | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.")
@@ -546,6 +551,9 @@ Definition transl_op
   | Omull, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pmull rd rs1 rs2 ::i k)
+  | Omullimm n, a1 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1;
+      OK (mulimm64 rd rs1 n ::i k)
   | Omullhs, _ => Error (msg "Asmblockgen.transl_op: Omullhs") (* Normalement pas émis *)
   | Omullhu, _ => Error (msg "Asmblockgen.transl_op: Omullhu") (* Normalement pas émis *)
   | Odivl, _ => Error (msg "Asmblockgen.transl_op: Odivl") (* Géré par fonction externe *)
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index c7b59a34..68f43894 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -81,6 +81,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Onegl => op1 (default nv)
   | Osubl => op2 (default nv)
   | Omull => op2 (default nv)
+  | Omullimm _ => op1 (default nv)
   | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv)
   | Oandl => op2 (default nv)
   | Oandlimm n => op1 (default nv)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 04081158..0e9a7af9 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -115,6 +115,7 @@ Inductive operation : Type :=
   | Onegl                    (**r [rd = - r1] *)
   | Osubl                    (**r [rd = r1 - r2] *)
   | Omull                    (**r [rd = r1 * r2] *)
+  | Omullimm (n: int64)      (**r [rd = r1 * n] *)
   | Omullhs                  (**r [rd = high part of r1 * r2, signed] *)
   | Omullhu                  (**r [rd = high part of r1 * r2, unsigned] *)
   | Odivl                    (**r [rd = r1 / r2] (signed) *)
@@ -314,6 +315,7 @@ Definition eval_operation
   | Onegl, v1::nil => Some (Val.negl v1)
   | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
   | Omull, v1::v2::nil => Some (Val.mull v1 v2)
+  | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n))
   | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2)
   | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2)
   | Odivl, v1::v2::nil => Val.divls v1 v2
@@ -503,6 +505,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Onegl => (Tlong :: nil, Tlong)
   | Osubl => (Tlong :: Tlong :: nil, Tlong)
   | Omull => (Tlong :: Tlong :: nil, Tlong)
+  | Omullimm _ => (Tlong :: nil, Tlong)
   | Omullhs => (Tlong :: Tlong :: nil, Tlong)
   | Omullhu => (Tlong :: Tlong :: nil, Tlong)
   | Odivl => (Tlong :: Tlong :: nil, Tlong)
@@ -700,6 +703,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
     destruct (eq_block b b0)...
   (* mull, mullhs, mullhu *)
   - destruct v0; destruct v1...
+  - destruct v0...
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* divl, divlu *)
@@ -1205,6 +1209,7 @@ Proof.
   - apply Val.subl_inject; auto.
   (* mull, mullhs, mullhu *)
   - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   (* divl, divlu *)
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 22211167..d87c837e 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -173,7 +173,7 @@ Definition mulimm_base (n1: int) (e2: expr) :=
   | i :: j :: nil =>
       Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
   | _ =>
-      Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil)
+      Eop (Omulimm n1) (e2 ::: Enil)
   end.
 
 Nondetfunction mulimm (n1: int) (e2: expr) :=
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index fe678383..a8889430 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -301,7 +301,7 @@ Proof.
   generalize (Int.one_bits_decomp n).
   generalize (Int.one_bits_range n).
   destruct (Int.one_bits n).
-  - intros. auto.
+  - intros. TrivialExists.
   - destruct l.
     + intros. rewrite H1. simpl.
       rewrite Int.add_zero.
@@ -319,7 +319,7 @@ Proof.
       rewrite Val.mul_add_distr_r.
       repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto.
       simpl. repeat rewrite H0; auto with coqlib.
-      intros. auto.
+      intros. TrivialExists.
 Qed.
 
 Theorem eval_mulimm:
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 3bb25807..b43c4d78 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -101,6 +101,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Onegl, v1::nil => negl v1
   | Osubl, v1::v2::nil => subl v1 v2
   | Omull, v1::v2::nil => mull v1 v2
+  | Omullimm n, v1::nil => mull v1 (L n)
   | Omullhs, v1::v2::nil => mullhs v1 v2
   | Omullhu, v1::v2::nil => mullhu v1 v2
   | Odivl, v1::v2::nil => divls v1 v2