aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-03-01 14:44:09 +0100
committerCyril SIX <cyril.six@kalray.eu>2019-03-01 14:44:09 +0100
commitdf32503f46a62b18f92363ac7f81ec0d5b36c64a (patch)
treeb11b1282e4b44e96c84dcaad438ee4e264fcacc9 /mppa_k1c
parent50affca71434b1e1ca3e75ce8f62a304ed1913cf (diff)
downloadcompcert-kvx-df32503f46a62b18f92363ac7f81ec0d5b36c64a.tar.gz
compcert-kvx-df32503f46a62b18f92363ac7f81ec0d5b36c64a.zip
Ointuofsingle done
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asm.v2
-rw-r--r--mppa_k1c/Asmblock.v2
-rw-r--r--mppa_k1c/Asmblockdeps.v1
-rw-r--r--mppa_k1c/Asmblockgen.v40
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml8
-rw-r--r--mppa_k1c/TargetPrinter.ml2
6 files changed, 23 insertions, 32 deletions
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) ->