Added Osingleofint

6 files changed, 28 insertions, 16 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index b22ea100..cf7d1ef1 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -98,6 +98,7 @@ Inductive instruction : Type :=
   | Pcvtl2w (rd rs: ireg)                           (**r Convert Long to Word *)

   | Psxwd   (rd rs: ireg)                           (**r Sign Extend Word to Double Word *)

   | Pzxwd   (rd rs: ireg)                           (**r Zero Extend Word to Double Word *)

+  | Pfloatwrnsz (rd rs: ireg)                       (**r Floating Point Conversion from integer *)

 

   (** Arith RI32 *)

   | Pmake   (rd: ireg) (imm: int)                   (**r load immediate *)

@@ -194,6 +195,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRR Asmblock.Psxwd rd rs  => Psxwd rd rs

   | PArithRR Asmblock.Pzxwd rd rs  => Pzxwd rd rs

   | PArithRR Asmblock.Pfnegd rd rs  => Pfnegd rd rs

+  | PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs

 

   (* RI32 *)

   | PArithRI32 Asmblock.Pmake rd imm  => Pmake rd imm

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index aa59d645..fbc9a5c6 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -283,6 +283,7 @@ Inductive arith_name_rr : Type :=
   | Pcvtl2w                                         (**r Convert Long to Word *)
   | Psxwd                                           (**r Sign Extend Word to Double Word *)
   | Pzxwd                                           (**r Zero Extend Word to Double Word *)
+  | Pfloatwrnsz                                     (**r Floating Point Conversion from integer *)
 .
 
 Inductive arith_name_ri32 : Type :=
@@ -884,6 +885,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
       | Pcvtl2w => rs#d <- (Val.loword rs#s)
       | Psxwd => rs#d <- (Val.longofint rs#s)
       | Pzxwd => rs#d <- (Val.longofintu rs#s)
+      | Pfloatwrnsz => rs#d <- (match Val.singleofint rs#s with Some f => f | _ => Vundef end)
       end
 
   | PArithRI32 n d i =>
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index b82ada55..07051111 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -544,17 +544,12 @@ Definition transl_op
           Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i
           Paddl RTMP rs RTMP ::i
           Psrail rd RTMP n ::i k)
-(*| Oshrxlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (if Int.eq n Int.zero then Pmv rd rs :: k else
-          Psrail GPR31 rs (Int.repr 63) ::
-          Psrlil GPR31 GPR31 (Int.sub Int64.iwordsize' n) ::
-          Paddl GPR31 rs GPR31 ::
-          Psrail rd GPR31 n :: k)
-
-*)| Onegf, a1 :: nil =>
+  | Onegf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfnegd rd rs ::i k)
+  | Osingleofint, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfloatwrnsz 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")
@@ -566,6 +561,10 @@ Definition transl_op
   | Osubfs , _ => Error (msg "Asmblockgen.transl_op: Osubfs")
   | Omulfs , _ => Error (msg "Asmblockgen.transl_op: Omulfs")
   | Odivfs , _ => Error (msg "Asmblockgen.transl_op: Odivfs")
+  | Ofloatoflong , _ => Error (msg "Asmblockgen.transl_op: Ofloatoflong")
+  | Ofloatoflongu , _ => Error (msg "Asmblockgen.transl_op: Ofloatoflongu")
+  | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong")
+  | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu")
   | Osingleoffloat , _ => Error (msg "Asmblockgen.transl_op: Osingleoffloat")
   | Ofloatofsingle , _ => Error (msg "Asmblockgen.transl_op: Ofloatofsingle")
   | Ointoffloat , _ => Error (msg "Asmblockgen.transl_op: Ointoffloat")
@@ -578,12 +577,12 @@ Definition transl_op
   | Osingleofintu , _ => Error (msg "Asmblockgen.transl_op: Osingleofintu")
   | Olongoffloat , _ => Error (msg "Asmblockgen.transl_op: Olongoffloat")
   | Olonguoffloat , _ => Error (msg "Asmblockgen.transl_op: Olonguoffloat")
-  | Ofloatoflong , _ => Error (msg "Asmblockgen.transl_op: Ofloatoflong")
-  | Ofloatoflongu , _ => Error (msg "Asmblockgen.transl_op: Ofloatoflongu")
+
+
   | Olongofsingle , _ => Error (msg "Asmblockgen.transl_op: Olongofsingle")
   | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle")
-  | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong")
-  | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu")
+
+
 (*| Oabsf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfabsd rd rs :: k)
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index b5f74a6d..2338da91 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -34,6 +34,7 @@ let arith_rr_str = function
   | Pfnegd -> "Pfnegd"
   | Psxwd -> "Psxwd"
   | Pzxwd -> "Pzxwd"
+  | Pfloatwrnsz -> "Pfloatwrnsz"
 
 let arith_rrr_str = function
   | Pcompw it -> "Pcompw"
@@ -343,7 +344,7 @@ type real_instruction =
   (* BCU *)
   | Icall | Call | Cb | Igoto | Goto | Ret | Get | Set
   (* FPU *)
-  | Fnegd
+  | Fnegd | Floatwz
 
 let ab_inst_to_real = function
   | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw
@@ -370,6 +371,7 @@ let ab_inst_to_real = function
   | "Pnop" | "Pcvtw2l" -> Nop
   | "Psxwd" -> Sxwd
   | "Pzxwd" -> Zxwd
+  | "Pfloatwrnsz" -> Floatwz
 
   | "Plb" -> Lbs
   | "Plbu" -> Lbz
@@ -431,6 +433,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)
+  | Floatwz -> mau
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 
       (match encoding with None | Some U6 | Some S10 -> lsu_data 
                           | Some U27L5 | Some U27L10 -> lsu_data_x 
@@ -449,6 +452,7 @@ let real_inst_to_latency = function
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
   | Sxwd | Zxwd
         -> 1
+  | Floatwz -> 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/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index d0aa89a4..ceea8de5 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -149,9 +149,12 @@ Lemma exec_basic_instr_pc_var:
   exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.

 Proof.

   intros. unfold exec_basic_instr in *. destruct i.

-  - unfold exec_arith_instr in *. exploreInst.

-      all: try (inv H; apply next_eq; auto;

+  - unfold exec_arith_instr in *. destruct i; destruct i.

+      all: try (exploreInst; inv H; apply next_eq; auto;

       apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).

+

+      (* Some cases treated seperately because exploreInst destructs too much *)

+      inv H. apply next_eq; auto. apply functional_extensionality; intros. rewrite regset_double_set; auto. discriminate.

   - exploreInst; apply exec_load_pc_var; auto.

   - exploreInst; apply exec_store_pc_var; auto.

   - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).

diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index aa6c167d..9a96cf3b 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -294,6 +294,8 @@ module Target (*: TARGET*) =
          fprintf oc "	sxwd	%a = %a\n" ireg rd ireg rs
       | Pzxwd(rd, rs) ->
          fprintf oc "	zxwd	%a = %a\n" ireg rd ireg rs
+      | Pfloatwrnsz(rd, rs) ->
+         fprintf oc "	floatw.rn.s	%a = %a, 0\n" ireg rd ireg rs
 
       (* Arith RI32 instructions *)
       | Pmake (rd, imm) ->