ça passe mais pas encore l'oracle

3 files changed, 98 insertions, 1 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 55143e4f..1a57e554 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -347,6 +347,16 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI64 Asmblock.Pandnil rd rs imm      => Pandnil rd rs imm

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

 

+  (** ARRR *)

+  | PArithARRR Asmblock.Pmaddw rd rs1 rs2       => Pmaddw rd rs1 rs2

+  | PArithARRR Asmblock.Pmaddl rd rs1 rs2       => Pmaddl rd rs1 rs2

+

+  (** ARRI32 *)

+  | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm    => Pmaddiw rd rs1 imm

+

+  (** ARRI64 *)

+  | PArithARRI64 Asmblock.Pmaddil rd rs1 imm    => Pmaddil rd rs1 imm

+                                                          

   (** Load *)

   | PLoadRRO Asmblock.Plb rd ra ofs   => Plb rd ra ofs

   | PLoadRRO Asmblock.Plbu rd ra ofs  => Plbu rd ra ofs

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index cdbe4eb3..9b51ea33 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -406,6 +406,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)
@@ -416,6 +429,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.
@@ -1180,6 +1196,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)
@@ -1196,6 +1228,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 *)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index d69903b4..5a138d00 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -52,6 +52,9 @@ Inductive arith_op :=
   | OArithRRR (n: arith_name_rrr)
   | OArithRRI32 (n: arith_name_rri32) (imm: int)
   | OArithRRI64 (n: arith_name_rri64) (imm: int64)
+  | OArithARRR (n: arith_name_arrr)
+  | OArithARRI32 (n: arith_name_arri32) (imm: int)
+  | OArithARRI64 (n: arith_name_arri64) (imm: int64)
 .
 
 Coercion OArithR: arith_name_r >-> arith_op.
@@ -109,10 +112,13 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
   | OArithRF64 n i, [] => Some (Val (arith_eval_rf64 n i))
 
   | OArithRRR n, [Val v1; Val v2] => Some (Val (arith_eval_rrr n v1 v2))
-
   | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i))
   | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i))
 
+  | OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3))
+  | OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i))
+  | OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i))
+
   | _, _ => None
   end.
 
@@ -525,6 +531,9 @@ Definition trans_arith (ai: ar_instruction) : macro :=
   | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))]
   | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))]
   | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))]
+  | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (Name(#d) @ Name (#s1) @ Name (#s2) @ Enil))]
+  | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (Name(#d) @ Name (#s) @ Enil))]
+  | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (Name(#d) @ Name (#s) @ Enil))]
   end.
 
 
@@ -711,6 +720,27 @@ Proof.
     * Simpl.
     * intros rr; destruct rr; Simpl.
       destruct (ireg_eq g rd); subst; Simpl.
+(* PArithARRR *)
+  - inv H; inv H0;
+    eexists; split; try split.
+    * simpl. pose (H1 rd); rewrite e. pose (H1 rs1); rewrite e0. pose (H1 rs2); rewrite e1. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithARRI32 *)
+  - inv H; inv H0;
+    eexists; split; try split.
+    * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithARRI64 *)
+  - inv H; inv H0;
+    eexists; split; try split.
+    * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
 Qed.
 
 Lemma forward_simu_basic:
@@ -1367,6 +1397,22 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   | Pornil => "Pornil"
   end.
 
+Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
+  match n with
+  | Pmaddw  => "Pmaddw"
+  | Pmaddl  => "Pmaddl"
+  end.
+
+Definition string_of_name_arri32 (n: arith_name_arri32): pstring :=
+  match n with
+  | Pmaddiw => "Pmaddw"
+  end.
+
+Definition string_of_name_arri64 (n: arith_name_arri64): pstring :=
+  match n with
+  | Pmaddil => "Pmaddl"
+  end.
+
 Definition string_of_arith (op: arith_op): pstring :=
   match op with
   | OArithR n => string_of_name_r n
@@ -1378,6 +1424,9 @@ Definition string_of_arith (op: arith_op): pstring :=
   | OArithRRR n => string_of_name_rrr n
   | OArithRRI32 n _ => string_of_name_rri32 n
   | OArithRRI64 n _ => string_of_name_rri64 n
+  | OArithARRR n => string_of_name_arrr n
+  | OArithARRI32 n _ => string_of_name_arri32 n
+  | OArithARRI64 n _ => string_of_name_arri64 n
   end.
 
 Definition string_of_name_lrro (n: load_name_rro) : pstring :=