progress on cmove

5 files changed, 17 insertions, 3 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 0ca554ab..1e022218 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -208,6 +208,7 @@ Inductive instruction : Type :=
   | Pandnil             (rd rs: ireg) (imm: int64)  (**r andn long *)

   | Pornil              (rd rs: ireg) (imm: int64)  (**r orn long *)

   | Pmaddil             (rd rs: ireg) (imm: int64)  (**r multiply add imm long *)

+  | Pcmove (bt: btest) (rcond rd rs : ireg) (** conditional move *) 

 .

 

 (** Correspondance between Asmblock and Asm *)

@@ -354,6 +355,7 @@ Definition basic_to_instruction (b: basic) :=
   (** ARRR *)

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

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

+  | PArithARRR (Asmblock.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2

 

   (** ARRI32 *)

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

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index ac4b7951..66181978 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -370,9 +370,6 @@ Inductive arith_name_rrr : Type :=
   | Pfsbfw                                          (**r float sub word *)
   | Pfmuld                                          (**r float multiply double *)
   | Pfmulw                                          (**r float multiply word *)
-(*
-  | Pcmove (it: itest)                              (**r conditional move *)
- *)
 .
 
 Inductive arith_name_rri32 : Type :=
@@ -414,6 +411,7 @@ Inductive arith_name_rri64 : Type :=
 Inductive arith_name_arrr : Type :=
   | Pmaddw                                           (**r multiply add word *)
   | Pmaddl                                           (**r multiply add long *)
+  | Pcmove (bt: btest)                               (**r conditional move *)
 .
 
 Inductive arith_name_arri32 : Type :=
@@ -1209,6 +1207,14 @@ 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)
+  | Pcmove bt =>
+    match cmp_for_btest bt with
+    | (Some c, Int)  =>
+      if (Val.cmp_bool c v2 (Vint Int.zero)) then v3 else v1
+    | (Some c, Long) =>
+      if (Val.cmpl_bool c v2 (Vlong Int64.zero)) then v3 else v1
+    | (None, _) => Vundef
+    end
   end.                    
 
 Definition arith_eval_arri32 n v1 v2 v3 :=
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index ad96ae87..7ea4c9ee 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1433,6 +1433,7 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
   match n with
   | Pmaddw  => "Pmaddw"
   | Pmaddl  => "Pmaddl"
+  | Pcmove _ => "Pcmove"
   end.
 
 Definition string_of_name_arri32 (n: arith_name_arri32): pstring :=
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 56b00c7e..27a4845f 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -128,6 +128,7 @@ let arith_rri64_str = function
 let arith_arrr_str = function
   | Pmaddw -> "Pmaddw"
   | Pmaddl -> "Pmaddl"
+  | Pcmove _ -> "Pcmove"
             
 let arith_ri32_str = "Pmake"
 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 41a6622a..9d816f36 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -504,6 +504,10 @@ module Target (*: TARGET*) =
       | Pmaddil (rd, rs, imm) ->
          fprintf oc "	maddd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
 
+      | Pcmove (bt, rd, rcond, rs) ->
+         fprintf oc "   cmove.%a %a? %a = %a\n"
+           bcond bt ireg rd ireg rcond ireg rs
+        
     let get_section_names name =
       let (text, lit) =
         match C2C.atom_sections name with