From 138f4fb80d3dc6cce396dc57e64c28dc949ab94a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 29 Apr 2019 14:32:06 +0200 Subject: removed fake ops for int32 -> double --- mppa_k1c/Asm.v | 4 ---- mppa_k1c/Asmblockdeps.v | 2 -- mppa_k1c/Asmblockgen.v | 6 ------ mppa_k1c/Asmvliw.v | 4 ---- mppa_k1c/PostpassSchedulingOracle.ml | 4 ---- mppa_k1c/TargetPrinter.ml | 4 ---- 6 files changed, 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) -> -- cgit