Added Ofloatconst and Osingleconst (not integrated in scheduler yet)

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