From df32503f46a62b18f92363ac7f81ec0d5b36c64a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Mar 2019 14:44:09 +0100 Subject: Ointuofsingle done --- mppa_k1c/Asm.v | 2 ++ mppa_k1c/Asmblock.v | 2 ++ mppa_k1c/Asmblockdeps.v | 1 + mppa_k1c/Asmblockgen.v | 40 ++++++++++-------------------------- mppa_k1c/PostpassSchedulingOracle.ml | 8 +++++--- mppa_k1c/TargetPrinter.ml | 2 ++ 6 files changed, 23 insertions(+), 32 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index d930b168..dcce98d0 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -110,6 +110,7 @@ Inductive instruction : Type := | 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) *) | Pfixeddrzz_i32 (rd rs: ireg) (**r Integer conversion from floating point (i32 -> f64) *) | Pfixedudrzz (rd rs: ireg) (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *) @@ -229,6 +230,7 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmblock.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs | PArithRR Asmblock.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs | PArithRR Asmblock.Pfixedwrzz rd rs => Pfixedwrzz rd rs + | PArithRR Asmblock.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs | PArithRR Asmblock.Pfixeddrzz rd rs => Pfixeddrzz rd rs | PArithRR Asmblock.Pfixedudrzz rd rs => Pfixedudrzz rd rs | PArithRR Asmblock.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index a5c7f495..54bf247f 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -294,6 +294,7 @@ Inductive arith_name_rr : Type := | 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) *) | Pfixedudrzz (**r Integer conversion from floating point (float -> unsigned long) *) | Pfixeddrzz_i32 (**r Integer conversion from floating point (float -> int) *) @@ -948,6 +949,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | Pfloatdrnsz => rs#d <- (match Val.floatoflong rs#s with Some f => f | _ => Vundef end) | Pfloatdrnsz_i32 => rs#d <- (match Val.floatofint rs#s with Some f => f | _ => Vundef end) | Pfixedwrzz => rs#d <- (match Val.intofsingle rs#s with Some i => i | _ => Vundef end) + | Pfixeduwrzz => rs#d <- (match Val.intuofsingle rs#s with Some i => i | _ => Vundef end) | Pfixeddrzz => rs#d <- (match Val.longoffloat rs#s with Some i => i | _ => Vundef end) | Pfixeddrzz_i32 => rs#d <- (match Val.intoffloat rs#s with Some i => i | _ => Vundef end) | Pfixedudrzz => rs#d <- (match Val.longuoffloat rs#s with Some i => i | _ => Vundef end) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index ee087d44..67ca94e2 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -123,6 +123,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := | Pfloatudrnsz_i32 => Some (Val (match Val.floatofintu v with Some f => f | _ => Vundef end)) | Pfloatdrnsz_i32 => Some (Val (match Val.floatofint v with Some f => f | _ => Vundef end)) | Pfixedwrzz => Some (Val (match Val.intofsingle v with Some i => i | _ => Vundef end)) + | Pfixeduwrzz => Some (Val (match Val.intuofsingle v with Some i => i | _ => Vundef end)) | Pfixeddrzz => Some (Val (match Val.longoffloat v with Some i => i | _ => Vundef end)) | Pfixedudrzz => Some (Val (match Val.longuoffloat v with Some i => i | _ => Vundef end)) | Pfixeddrzz_i32 => Some (Val (match Val.intoffloat v with Some i => i | _ => Vundef end)) diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 8dfa2cee..56d061c2 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -594,27 +594,24 @@ Definition transl_op | Ofloatofintu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfloatudrnsz_i32 rd rs ::i k) - (* | Ofloatofint, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pfloatwrnsz rd rs ::i k) - | Ofloatofintu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pfloatuwrnsz rd rs ::i k) *) (* FIXME - Ofloatofint and Ofloatofintu are currently incorrect *) | Ointofsingle, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixedwrzz rd rs ::i k) + | Ointuofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeduwrzz rd rs ::i k) | Olongoffloat, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixeddrzz rd rs ::i k) | Ointoffloat, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixeddrzz_i32 rd rs ::i k) - | Olonguoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfixedudrzz rd rs ::i k) | Ointuoffloat, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixedudrzz_i32 rd rs ::i k) + | Olonguoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedudrzz rd rs ::i k) | Ofloatofsingle, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; @@ -624,31 +621,16 @@ Definition transl_op OK (Pfnarrowdw rd rs ::i k) - | Oabsf , _ => Error (msg "Asmblockgen.transl_op: Oabsf") - | Oaddf , _ => Error (msg "Asmblockgen.transl_op: Oaddf") - | Osubf , _ => Error (msg "Asmblockgen.transl_op: Osubf") - | Omulf , _ => Error (msg "Asmblockgen.transl_op: Omulf") | Odivf , _ => Error (msg "Asmblockgen.transl_op: Odivf") - | Onegfs , _ => Error (msg "Asmblockgen.transl_op: Onegfs") - | Oabsfs , _ => Error (msg "Asmblockgen.transl_op: Oabsfs") - | Oaddfs , _ => Error (msg "Asmblockgen.transl_op: Oaddfs") - | Osubfs , _ => Error (msg "Asmblockgen.transl_op: Osubfs") - | Omulfs , _ => Error (msg "Asmblockgen.transl_op: Omulfs") - | Odivfs , _ => Error (msg "Asmblockgen.transl_op: Odivfs") - | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong") - | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu") - | Ointoffloat , _ => Error (msg "Asmblockgen.transl_op: Ointoffloat") - | Ointuoffloat , _ => Error (msg "Asmblockgen.transl_op: Ointuoffloat") - | Ofloatofint , _ => Error (msg "Asmblockgen.transl_op: Ofloatofint") - | Ofloatofintu , _ => Error (msg "Asmblockgen.transl_op: Ofloatofintu") - | Ointuofsingle , _ => Error (msg "Asmblockgen.transl_op: Ointuofsingle") - | Osingleofintu , _ => Error (msg "Asmblockgen.transl_op: Osingleofintu") - | Olonguoffloat , _ => Error (msg "Asmblockgen.transl_op: Olonguoffloat") - + (* We use the Splitlong instead for these four conversions *) + | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong") + | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu") | Olongofsingle , _ => Error (msg "Asmblockgen.transl_op: Olongofsingle") | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle") + + | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index d9a60fb4..c3473b9f 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -46,6 +46,7 @@ let arith_rr_str = function | Pfloatdrnsz -> "Pfloatdrnsz" | Pfloatdrnsz_i32 -> "Pfloatdrnsz_i32" | Pfixedwrzz -> "Pfixedwrzz" + | Pfixeduwrzz -> "Pfixeduwrzz" | Pfixeddrzz -> "Pfixeddrzz" | Pfixedudrzz -> "Pfixedudrzz" | Pfixeddrzz_i32 -> "Pfixeddrzz_i32" @@ -371,7 +372,7 @@ type real_instruction = (* FPU *) | Fabsd | Fabsw | Fnegw | Fnegd | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw - | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeddz | Fixedudz + | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz let ab_inst_to_real = function | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw @@ -407,6 +408,7 @@ let ab_inst_to_real = function | "Pfloatudrnsz" -> Floatudz | "Pfloatudrnsz_i32" -> Floatudz | "Pfixedwrzz" -> Fixedwz + | "Pfixeduwrzz" -> Fixeduwz | "Pfixeddrzz" -> Fixeddz | "Pfixedudrzz" -> Fixedudz | "Pfixeddrzz_i32" -> Fixeddz @@ -481,7 +483,7 @@ let rec_to_usage r = | Nop -> alu_nop | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) | Sxwd | Zxwd -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) - | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau + | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> (match encoding with None | Some U6 | Some S10 -> lsu_data | Some U27L5 | Some U27L10 -> lsu_data_x @@ -502,7 +504,7 @@ let real_inst_to_latency = function | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make | Sxwd | Zxwd -> 1 - | Floatwz | Floatuwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 + | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Sb | Sh | Sw | Sd diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 8d053cde..acb128de 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -312,6 +312,8 @@ module Target (*: TARGET*) = fprintf oc " floatd.rn.s %a = %a, 0\n" ireg rd ireg rs | Pfixedwrzz(rd, rs) -> fprintf oc " fixedw.rz %a = %a, 0\n" ireg rd ireg rs + | Pfixeduwrzz(rd, rs) -> + fprintf oc " fixeduw.rz %a = %a, 0\n" ireg rd ireg rs | Pfixeddrzz(rd, rs) | Pfixeddrzz_i32(rd, rs) -> fprintf oc " fixedd.rz %a = %a, 0\n" ireg rd ireg rs | Pfixedudrzz(rd, rs) | Pfixedudrzz_i32(rd, rs) -> -- cgit