diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 15:10:20 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 15:10:20 +0100 |
commit | 40bc8bf185c5cd3c5620cf4fe24ebcc9511c79fb (patch) | |
tree | 24d61f0ca190e6416bdd9081f51ae36ee4403de0 | |
parent | 1f38df638dfd4ae2aa85467cc28f6b4fa1da03b1 (diff) | |
download | compcert-kvx-40bc8bf185c5cd3c5620cf4fe24ebcc9511c79fb.tar.gz compcert-kvx-40bc8bf185c5cd3c5620cf4fe24ebcc9511c79fb.zip |
Added Ofloatconst and Osingleconst (not integrated in scheduler yet)
-rw-r--r-- | mppa_k1c/Asm.v | 12 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 23 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 14 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 2 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 12 |
5 files changed, 53 insertions, 10 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 0ce3b455..b22ea100 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -105,6 +105,12 @@ Inductive instruction : Type := (** Arith RI64 *)
| Pmakel (rd: ireg) (imm: int64) (**r load immediate long *)
+ (** Arith RF32 *)
+ | Pmakefs (rd: ireg) (imm: float32)
+
+ (** Arith RF64 *)
+ | Pmakef (rd: ireg) (imm: float)
+
(** Arith RRR *)
| Pcompw (it: itest) (rd rs1 rs2: ireg) (**r comparison word *)
| Pcompl (it: itest) (rd rs1 rs2: ireg) (**r comparison long *)
@@ -195,6 +201,12 @@ Definition basic_to_instruction (b: basic) := (* RI64 *)
| PArithRI64 Asmblock.Pmakel rd imm => Pmakel rd imm
+ (* RF32 *)
+ | PArithRF32 Asmblock.Pmakefs rd imm => Pmakefs rd imm
+
+ (* RF64 *)
+ | PArithRF64 Asmblock.Pmakef rd imm => Pmakef rd imm
+
(* RRR *)
| PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2
| PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index fcf45bf8..aa59d645 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -293,6 +293,14 @@ Inductive arith_name_ri64 : Type := | Pmakel (**r load immediate long *) . +Inductive arith_name_rf32 : Type := + | Pmakefs (**r load immediate single *) +. + +Inductive arith_name_rf64 : Type := + | Pmakef (**r load immediate float *) +. + Inductive arith_name_rrr : Type := | Pcompw (it: itest) (**r comparison word *) | Pcompl (it: itest) (**r comparison long *) @@ -347,6 +355,8 @@ Inductive ar_instruction : Type := | PArithRR (i: arith_name_rr) (rd rs: ireg) | PArithRI32 (i: arith_name_ri32) (rd: ireg) (imm: int) | PArithRI64 (i: arith_name_ri64) (rd: ireg) (imm: int64) + | PArithRF32 (i: arith_name_rf32) (rd: ireg) (imm: float32) + | PArithRF64 (i: arith_name_rf64) (rd: ireg) (imm: float) | PArithRRR (i: arith_name_rrr) (rd rs1 rs2: ireg) | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int) | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64) @@ -356,6 +366,8 @@ Coercion PArithR: arith_name_r >-> Funclass. Coercion PArithRR: arith_name_rr >-> Funclass. Coercion PArithRI32: arith_name_ri32 >-> Funclass. Coercion PArithRI64: arith_name_ri64 >-> Funclass. +Coercion PArithRF32: arith_name_rf32 >-> Funclass. +Coercion PArithRF64: arith_name_rf64 >-> Funclass. Coercion PArithRRR: arith_name_rrr >-> Funclass. Coercion PArithRRI32: arith_name_rri32 >-> Funclass. Coercion PArithRRI64: arith_name_rri64 >-> Funclass. @@ -844,6 +856,7 @@ Definition compare_long (t: itest) (v1 v2: val) (m: mem): val := | None => Vundef end . + (** Execution of arith instructions TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma... @@ -883,6 +896,16 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | Pmakel => rs#d <- (Vlong i) end + | PArithRF32 n d i => + match n with + | Pmakefs => rs#d <- (Vsingle i) + end + + | PArithRF64 n d i => + match n with + | Pmakef => rs#d <- (Vfloat i) + end + | PArithRRR n d s1 s2 => match n with | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2 m) diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 553d20d4..b82ada55 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -350,19 +350,13 @@ Definition transl_op | Olongconst n, nil => do rd <- ireg_of res; OK (loadimm64 rd n ::i k) - | Ofloatconst _, _ => Error(msg "Asmblockgen.transl_op: Ofloatconst") - | Osingleconst _, _ => Error(msg "Asmblockgen.transl_op: Osingleconst") -(*| Ofloatconst f, nil => + | Ofloatconst f, nil => do rd <- freg_of res; - OK (if Float.eq_dec f Float.zero - then Pfcvtdw rd GPR0 :: k - else Ploadfi rd f :: k) + OK (Pmakef rd f ::i k) | Osingleconst f, nil => do rd <- freg_of res; - OK (if Float32.eq_dec f Float32.zero - then Pfcvtsw rd GPR0 :: k - else Ploadsi rd f :: k) -*)| Oaddrsymbol s ofs, nil => + OK (Pmakefs rd f ::i k) + | Oaddrsymbol s ofs, nil => do rd <- ireg_of res; OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero) then Ploadsymbol s Ptrofs.zero rd ::i addptrofs rd rd ofs ::i k diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 040e9e8d..614af7f5 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -127,6 +127,8 @@ let arith_rec i = | PArithRRR (i, rd, rs1, rs2) -> arith_rrr_rec i (IR rd) (IR rs1) (IR rs2) | PArithRI32 (rd, imm32) -> { inst = arith_ri32_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I32 imm32)) ; is_control = false} | PArithRI64 (rd, imm64) -> { inst = arith_ri64_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I64 imm64)) ; is_control = false} + | PArithRF32 (rd, f) -> raise OpaqueInstruction (* FIXME - complete later *) + | PArithRF64 (rd, f) -> raise OpaqueInstruction | PArithRR (i, rd, rs) -> arith_rr_rec i (IR rd) (IR rs) | PArithR (i, rd) -> arith_r_rec i (IR rd) diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index d7926c23..aa6c167d 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -303,6 +303,18 @@ module Target (*: TARGET*) = | Pmakel (rd, imm) -> fprintf oc " make %a, %a\n" ireg rd coqint64 imm + (* Arith RF32 instructions *) + | Pmakefs (rd, f) -> + let d = Floats.Float32.to_bits f in + fprintf oc " make %a, %a %s %.18g\n" + ireg rd coqint d comment (camlfloat_of_coqfloat32 f) + + (* Arith RF64 instructions *) + | Pmakef (rd, f) -> + let d = Floats.Float.to_bits f in + fprintf oc " make %a, %a %s %.18g\n" + ireg rd coqint64 d comment (camlfloat_of_coqfloat f) + (* Arith RRR instructions *) | Pcompw (it, rd, rs1, rs2) -> fprintf oc " compw.%a %a = %a, %a\n" icond it ireg rd ireg rs1 ireg rs2 |