mul immediate begin

8 files changed, 28 insertions, 4 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 1a57e554..0ca554ab 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -177,6 +177,7 @@ Inductive instruction : Type :=
   | Pcompiw (it: itest) (rd rs: ireg) (imm: int)    (**r comparison imm word *)

 

   | Paddiw              (rd rs: ireg) (imm: int)    (**r add imm word *)

+  | Pmuliw              (rd rs: ireg) (imm: int)    (**r mul imm word *)

   | Pandiw              (rd rs: ireg) (imm: int)    (**r and imm word *)

   | Pnandiw             (rd rs: ireg) (imm: int)    (**r nand imm word *)

   | Poriw               (rd rs: ireg) (imm: int)    (**r or imm word *)

@@ -197,6 +198,7 @@ Inductive instruction : Type :=
   (** Arith RRI64 *)

   | Pcompil (it: itest) (rd rs: ireg) (imm: int64)  (**r comparison imm long *)

   | Paddil              (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

+  | Pmulil              (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

   | Pandil              (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

   | Pnandil             (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

   | Poril               (rd rs: ireg) (imm: int64)  (**r or immediate long *) 

@@ -319,6 +321,7 @@ Definition basic_to_instruction (b: basic) :=
   (* RRI32 *)

   | PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm

   | PArithRRI32 Asmblock.Paddiw rd rs imm       => Paddiw rd rs imm

+  | PArithRRI32 Asmblock.Pmuliw rd rs imm       => Pmuliw rd rs imm

   | PArithRRI32 Asmblock.Pandiw rd rs imm       => Pandiw rd rs imm

   | PArithRRI32 Asmblock.Pnandiw rd rs imm      => Pnandiw rd rs imm

   | PArithRRI32 Asmblock.Poriw rd rs imm        => Poriw rd rs imm

@@ -338,6 +341,7 @@ Definition basic_to_instruction (b: basic) :=
   (* RRI64 *)

   | PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm

   | PArithRRI64 Asmblock.Paddil rd rs imm       => Paddil rd rs imm

+  | PArithRRI64 Asmblock.Pmulil rd rs imm       => Pmulil rd rs imm

   | PArithRRI64 Asmblock.Pandil rd rs imm       => Pandil rd rs imm

   | PArithRRI64 Asmblock.Pnandil rd rs imm      => Pnandil rd rs imm

   | PArithRRI64 Asmblock.Poril rd rs imm        => Poril rd rs imm

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index b3e1532d..386106d6 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -376,6 +376,7 @@ Inductive arith_name_rri32 : Type :=
   | Pcompiw (it: itest)                             (**r comparison imm word *)
 
   | Paddiw                                          (**r add imm word *)
+  | Pmuliw                                          (**r add imm word *)
   | Pandiw                                          (**r and imm word *)
   | Pnandiw                                         (**r nand imm word *)
   | Poriw                                           (**r or imm word *)
@@ -396,6 +397,7 @@ Inductive arith_name_rri32 : Type :=
 Inductive arith_name_rri64 : Type :=
   | Pcompil (it: itest)                             (**r comparison imm long *)
   | Paddil                                          (**r add immediate long *) 
+  | Pmulil                                          (**r mul immediate long *) 
   | Pandil                                          (**r and immediate long *) 
   | Pnandil                                         (**r nand immediate long *) 
   | Poril                                           (**r or immediate long *) 
@@ -1168,6 +1170,7 @@ Definition arith_eval_rri32 n v i :=
   match n with
   | Pcompiw c => compare_int c v (Vint i)
   | Paddiw  => Val.add   v (Vint i)
+  | Pmuliw  => Val.mul   v (Vint i)
   | Pandiw  => Val.and   v (Vint i)
   | Pnandiw => Val.notint (Val.and  v (Vint i))
   | Poriw   => Val.or    v (Vint i)
@@ -1189,6 +1192,7 @@ Definition arith_eval_rri64 n v i :=
   match n with
   | Pcompil c => compare_long c v (Vlong i)
   | Paddil  => Val.addl v (Vlong i)
+  | Pmulil  => Val.mull v (Vlong i)
   | Pandil  => Val.andl v (Vlong i)
   | Pnandil  => Val.notl (Val.andl v (Vlong i))
   | Poril   => Val.orl  v (Vlong i)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index e05f92a7..f50b7d4a 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1382,6 +1382,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   match n with
     Pcompiw _ => "Pcompiw"
   | Paddiw => "Paddiw"
+  | Pmuliw => "Pmuliw"
   | Pandiw => "Pandiw"
   | Pnandiw => "Pnandiw"
   | Poriw => "Poriw"
@@ -1403,6 +1404,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   match n with
     Pcompil _ => "Pcompil"
   | Paddil => "Paddil"
+  | Pmulil => "Pmulil"
   | Pandil => "Pandil"
   | Pnandil => "Pnandil"
   | Poril => "Poril"
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 801a520e..c7b59a34 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -45,6 +45,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oneg => op1 (modarith nv)
   | Osub => op2 (default nv)
   | Omul => op2 (modarith nv)
+  | Omulimm _ => op1 (modarith nv)
   | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv)
   | Oand => op2 (bitwise nv)
   | Oandimm n => op1 (andimm nv n)
@@ -171,6 +172,7 @@ Proof.
 - apply add_sound; auto with na.
 - apply neg_sound; auto.
 - apply mul_sound; auto.
+- apply mul_sound; auto with na.
 - apply and_sound; auto.
 - apply andimm_sound; auto.
 - apply notint_sound; apply and_sound; auto.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index c56a9649..04081158 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -70,6 +70,7 @@ Inductive operation : Type :=
   | Oneg                     (**r [rd = - r1]   *)                     
   | Osub                     (**r [rd = r1 - r2] *)
   | Omul                     (**r [rd = r1 * r2] *)
+  | Omulimm (n: int)         (**r [rd = r1 * n] *)
   | Omulhs                   (**r [rd = high part of r1 * r2, signed] *)
   | Omulhu                   (**r [rd = high part of r1 * r2, unsigned] *)
   | Odiv                     (**r [rd = r1 / r2] (signed) *)
@@ -268,6 +269,7 @@ Definition eval_operation
   | Oneg, v1 :: nil => Some (Val.neg v1)
   | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2)
   | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
+  | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n))
   | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
   | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
   | Odiv, v1 :: v2 :: nil => Val.divs v1 v2
@@ -456,6 +458,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oneg => (Tint :: nil, Tint)
   | Osub => (Tint :: Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
+  | Omulimm _ => (Tint :: nil, Tint)
   | Omulhs => (Tint :: Tint :: nil, Tint)
   | Omulhu => (Tint :: Tint :: nil, Tint)
   | Odiv => (Tint :: Tint :: nil, Tint)
@@ -623,8 +626,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* neg, sub *)
   - destruct v0...
   - unfold Val.sub. destruct v0; destruct v1... 
-  (* mul, mulhs, mulhu *)
+  (* mul, mulimm, mulhs, mulhu *)
   - destruct v0; destruct v1...
+  - destruct v0...
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* div, divu *)
@@ -1124,8 +1128,9 @@ Proof.
   (* neg, sub *)
   - inv H4; simpl; auto.
   - apply Val.sub_inject; auto.
-  (* mul, mulhs, mulhu *)
+  (* mul, mulimm, mulhs, mulhu *)
   - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   (* div, divu *)
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index f7702a9d..e1948a03 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -95,6 +95,7 @@ let arith_rrr_str = function
 let arith_rri32_str = function
   | Pcompiw it -> "Pcompiw"
   | Paddiw -> "Paddiw"
+  | Pmuliw -> "Pmuliw"
   | Pandiw -> "Pandiw"
   | Pnandiw -> "Pnandiw"
   | Poriw -> "Poriw"
@@ -114,6 +115,7 @@ let arith_rri32_str = function
 let arith_rri64_str = function
   | Pcompil it -> "Pcompil"
   | Paddil -> "Paddil"
+  | Pmulil -> "Pmulil"
   | Pandil -> "Pandil"
   | Pnandil -> "Pnandil"
   | Poril -> "Poril"
@@ -437,8 +439,8 @@ let ab_inst_to_real = function
   | "Pcompl" | "Pcompil" -> Compd
   | "Pfcompw" -> Fcompw
   | "Pfcompl" -> Fcompd
-  | "Pmulw" -> Mulw
-  | "Pmull" -> Muld
+  | "Pmulw" | "Pmuliw" -> Mulw
+  | "Pmull" | "Pmulil" -> Muld
   | "Porw" | "Poriw" -> Orw
   | "Pnorw" | "Pnoriw" -> Norw
   | "Porl" | "Poril" -> Ord
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 5c5d6c79..69824852 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -442,6 +442,8 @@ module Target (*: TARGET*) =
          fprintf oc "	compw.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint imm
       | Paddiw (rd, rs, imm) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Pmuliw (rd, rs, imm) ->
+         fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pandiw (rd, rs, imm) ->
          fprintf oc "	andw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pnandiw (rd, rs, imm) ->
@@ -481,6 +483,8 @@ module Target (*: TARGET*) =
          fprintf oc "	compd.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm
       | Paddil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Pmulil (rd, rs, imm) -> assert Archi.ptr64;
+         fprintf oc "	muld	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pandil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pnandil (rd, rs, imm) -> assert Archi.ptr64;
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index a92358ca..3bb25807 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -57,6 +57,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oneg, v1::nil => neg v1
   | Osub, v1::v2::nil => sub v1 v2
   | Omul, v1::v2::nil => mul v1 v2
+  | Omulimm n, v1::nil => mul v1 (I n)
   | Omulhs, v1::v2::nil => mulhs v1 v2
   | Omulhu, v1::v2::nil => mulhu v1 v2
   | Odiv, v1::v2::nil => divs v1 v2