Merge branch 'mppa-madd' into mppa_postpass

1 files changed, 45 insertions, 0 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 03c7e6d5..d335801e 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -379,6 +379,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 *)
@@ -399,6 +400,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 *) 
@@ -409,6 +411,19 @@ Inductive arith_name_rri64 : Type :=
   | Pornil                                          (**r orn immediate long *)
 .
 
+Inductive arith_name_arrr : Type :=
+  | Pmaddw                                           (**r multiply add word *)
+  | Pmaddl                                           (**r multiply add long *)
+.
+
+Inductive arith_name_arri32 : Type :=
+  | Pmaddiw                                           (**r multiply add word *)
+.
+
+Inductive arith_name_arri64 : Type :=
+  | Pmaddil                                           (**r multiply add long *)
+.
+
 Inductive ar_instruction : Type :=
   | PArithR     (i: arith_name_r)     (rd: ireg)
   | PArithRR    (i: arith_name_rr)    (rd rs: ireg)
@@ -419,6 +434,9 @@ Inductive ar_instruction : Type :=
   | PArithRRR   (i: arith_name_rrr)   (rd rs1 rs2: ireg)
   | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int)
   | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64)
+  | PArithARRR   (i: arith_name_arrr)   (rd rs1 rs2: ireg)
+  | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int)
+  | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64)
 .
 
 Coercion PArithR:       arith_name_r        >-> Funclass.
@@ -430,6 +448,9 @@ Coercion PArithRF64:    arith_name_rf64     >-> Funclass.
 Coercion PArithRRR:     arith_name_rrr      >-> Funclass.
 Coercion PArithRRI32:   arith_name_rri32    >-> Funclass.
 Coercion PArithRRI64:   arith_name_rri64    >-> Funclass.
+Coercion PArithARRR:     arith_name_arrr      >-> Funclass.
+Coercion PArithARRI32:   arith_name_arri32    >-> Funclass.
+Coercion PArithARRI64:   arith_name_arri64    >-> Funclass.
 
 Inductive basic : Type :=
   | PArith          (i: ar_instruction)
@@ -1151,6 +1172,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)
@@ -1172,6 +1194,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)
@@ -1182,6 +1205,22 @@ Definition arith_eval_rri64 n v i :=
   | Pornil  => Val.orl (Val.notl v) (Vlong i)
   end.
 
+Definition arith_eval_arrr n v1 v2 v3 :=
+  match n with
+  | Pmaddw => Val.add v1 (Val.mul v2 v3)
+  | Pmaddl => Val.addl v1 (Val.mull v2 v3)
+  end.                    
+
+Definition arith_eval_arri32 n v1 v2 v3 :=
+  match n with
+  | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
+  end.                    
+
+Definition arith_eval_arri64 n v1 v2 v3 :=
+  match n with
+  | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3))
+  end.                    
+
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithR n d => rs#d <- (arith_eval_r n)
@@ -1198,6 +1237,12 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i)
 
   | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i)
+
+  | PArithARRR n d s1 s2 => rs#d <- (arith_eval_arrr n rs#d rs#s1 rs#s2)
+
+  | PArithARRI32 n d s i => rs#d <- (arith_eval_arri32 n rs#d rs#s i)
+
+  | PArithARRI64 n d s i => rs#d <- (arith_eval_arri64 n rs#d rs#s i)
   end.
 
 (** * load/store *)