removed fake ops for int32 -> double

6 files changed, 0 insertions, 24 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 53747851..d1ac8a67 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -149,9 +149,7 @@ Inductive instruction : Type :=
   | Pfloatwrnsz (rd rs: ireg)                       (**r Floating Point Conversion from integer (32 -> 32) *)

   | Pfloatuwrnsz (rd rs: ireg)                      (**r Floating Point Conversion from integer (u32 -> 32) *)

   | Pfloatudrnsz (rd rs: ireg)                       (**r Floating Point Conversion from unsigned integer (64 bits) *)

-  | Pfloatudrnsz_i32 (rd rs: ireg)                       (**r Floating Point Conversion from unsigned integer (32 bits) *)

   | Pfloatdrnsz (rd rs: ireg)                       (**r Floating Point Conversion from integer (64 bits) *)

-  | Pfloatdrnsz_i32 (rd rs: ireg)                       (**r Floating Point Conversion from integer (32 bits) *)

   | Pfixedwrzz (rd rs: ireg)                        (**r Integer conversion from floating point *)

   | Pfixeduwrzz (rd rs: ireg)                        (**r Integer conversion from floating point (f32 -> 32 bits unsigned *)

   | Pfixeddrzz (rd rs: ireg)                        (**r Integer conversion from floating point (i64 -> 64 bits) *)

@@ -309,8 +307,6 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRR Asmvliw.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs

   | PArithRR Asmvliw.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs

   | PArithRR Asmvliw.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs

-  | PArithRR Asmvliw.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs

-  | PArithRR Asmvliw.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs

   | PArithRR Asmvliw.Pfixedwrzz rd rs => Pfixedwrzz rd rs

   | PArithRR Asmvliw.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs

   | PArithRR Asmvliw.Pfixeddrzz rd rs => Pfixeddrzz rd rs

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index ff625bdd..2e83fb44 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1237,9 +1237,7 @@ Definition string_of_name_rr (n: arith_name_rr): pstring :=
   | Pfloatwrnsz => "Pfloatwrnsz"
   | Pfloatuwrnsz => "Pfloatuwrnsz"
   | Pfloatudrnsz => "Pfloatudrnsz"
-  | Pfloatudrnsz_i32 => "Pfloatudrnsz_i32"
   | Pfloatdrnsz => "Pfloatdrnsz"
-  | Pfloatdrnsz_i32 => "Pfloatdrnsz_i32"
   | Pfixedwrzz => "Pfixedwrzz"
   | Pfixeduwrzz => "Pfixeduwrzz"
   | Pfixeddrzz => "Pfixeddrzz"
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 49f6e4f9..6cd31468 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -696,12 +696,6 @@ Definition transl_op
   | Ofloatoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfloatudrnsz rd rs ::i k)
-  | Ofloatofint, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfloatdrnsz_i32 rd rs ::i k)
-  | Ofloatofintu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfloatudrnsz_i32 rd rs ::i k)
   | Ointofsingle, a1 :: nil =>
       do rd <- ireg_of res; do rs <- freg_of a1;
       OK (Pfixedwrzz rd rs ::i k)
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 3f2179c2..cf827818 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -322,9 +322,7 @@ Inductive arith_name_rr : Type :=
   | Pfloatwrnsz                                     (**r Floating Point conversion from integer (int -> SINGLE) *)
   | Pfloatuwrnsz                                    (**r Floating Point conversion from integer (unsigned int -> SINGLE) *)
   | Pfloatudrnsz                                    (**r Floating Point Conversion from integer (unsigned long -> float) *)
-  | Pfloatudrnsz_i32                                (**r Floating Point Conversion from integer (unsigned int -> float) *)
   | Pfloatdrnsz                                     (**r Floating Point Conversion from integer (long -> float) *)
-  | Pfloatdrnsz_i32                                 (**r Floating Point Conversion from integer (int -> float) *)
   | Pfixedwrzz                                      (**r Integer conversion from floating point (single -> int) *)
   | Pfixeduwrzz                                     (**r Integer conversion from floating point (single -> unsigned int) *)
   | Pfixeddrzz                                      (**r Integer conversion from floating point (float -> long) *)
@@ -909,8 +907,6 @@ Definition arith_eval_rr n v :=
   | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end
   | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end
   | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end
-  | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end
-  | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end
   | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end
   | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end
   | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index af40d4d1..f931b64b 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -46,10 +46,8 @@ let arith_rr_str = function
   | Pfwidenlwd -> "Pfwidenlwd"
   | Pfloatwrnsz -> "Pfloatwrnsz"
   | Pfloatuwrnsz -> "Pfloatuwrnsz"
-  | Pfloatudrnsz_i32 -> "Pfloatudrnsz_i32"
   | Pfloatudrnsz -> "Pfloatudrnsz"
   | Pfloatdrnsz -> "Pfloatdrnsz"
-  | Pfloatdrnsz_i32 -> "Pfloatdrnsz_i32"
   | Pfixedwrzz -> "Pfixedwrzz"
   | Pfixeduwrzz -> "Pfixeduwrzz"
   | Pfixeddrzz -> "Pfixeddrzz"
@@ -500,9 +498,7 @@ let ab_inst_to_real = function
   | "Pfloatwrnsz" -> Floatwz
   | "Pfloatuwrnsz" -> Floatuwz
   | "Pfloatdrnsz" -> Floatdz
-  | "Pfloatdrnsz_i32" -> Floatdz
   | "Pfloatudrnsz" -> Floatudz
-  | "Pfloatudrnsz_i32" -> Floatudz
   | "Pfixedwrzz" -> Fixedwz
   | "Pfixeduwrzz" -> Fixeduwz
   | "Pfixeddrzz" -> Fixeddz
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 8e8efefc..506faa1c 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -401,12 +401,8 @@ module Target (*: TARGET*) =
          fprintf oc "	floatw.rn.s	%a = %a, 0\n" ireg rd ireg rs
       | Pfloatudrnsz(rd, rs) ->
          fprintf oc "	floatud.rn.s	%a = %a, 0\n" ireg rd ireg rs
-      | Pfloatudrnsz_i32(rd, rs) ->
-         fprintf oc "	zxwd %a = %a\n # FIXME\n	;;\n	floatud.rn.s	%a = %a, 0\n" ireg rd ireg rs ireg rd ireg rd
       | Pfloatdrnsz(rd, rs) ->
           fprintf oc "	floatd.rn.s	%a = %a, 0\n" ireg rd ireg rs
-      | Pfloatdrnsz_i32(rd, rs) ->
-         fprintf oc "	sxwd %a = %a\n # FIXME\n	;;\n	floatd.rn.s	%a = %a, 0\n" ireg rd ireg rs ireg rd ireg rd
       | Pfixedwrzz(rd, rs) ->
          fprintf oc "	fixedw.rz	%a = %a, 0\n" ireg rd ireg rs
       | Pfixeduwrzz(rd, rs) ->