diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmblock.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 5 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 8 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 | ||||
| -rw-r--r-- | test/mppa/instr/floatconv.c | 9 |
7 files changed, 26 insertions, 6 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index cf7d1ef1..35e3710c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -99,6 +99,7 @@ Inductive instruction : Type := | 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 *)
+ | Pfixedwrzz (rd rs: ireg) (**r Integer conversion from floating point *)
(** Arith RI32 *)
| Pmake (rd: ireg) (imm: int) (**r load immediate *)
@@ -196,6 +197,7 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmblock.Pzxwd rd rs => Pzxwd rd rs
| PArithRR Asmblock.Pfnegd rd rs => Pfnegd rd rs
| PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
+ | PArithRR Asmblock.Pfixedwrzz rd rs => Pfixedwrzz rd rs
(* RI32 *)
| PArithRI32 Asmblock.Pmake rd imm => Pmake rd imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index fbc9a5c6..643870ea 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -283,7 +283,8 @@ 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 *) + | Pfloatwrnsz (**r Floating Point Conversion from integer (single -> int) *) + | Pfixedwrzz (**r Integer conversion from floating point (int -> single) *) . Inductive arith_name_ri32 : Type := @@ -886,6 +887,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | 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) + | Pfixedwrzz => rs#d <- (match Val.intofsingle rs#s with Some i => i | _ => Vundef end) end | PArithRI32 n d i => diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 07051111..80790465 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -548,8 +548,11 @@ Definition transl_op 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; + do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfloatwrnsz rd rs ::i k) + | Ointofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedwrzz 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") diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 2338da91..a09d696f 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -35,6 +35,7 @@ let arith_rr_str = function | Psxwd -> "Psxwd" | Pzxwd -> "Pzxwd" | Pfloatwrnsz -> "Pfloatwrnsz" + | Pfixedwrzz -> "Pfixedwrzz" let arith_rrr_str = function | Pcompw it -> "Pcompw" @@ -344,7 +345,7 @@ type real_instruction = (* BCU *) | Icall | Call | Cb | Igoto | Goto | Ret | Get | Set (* FPU *) - | Fnegd | Floatwz + | Fnegd | Floatwz | Fixedwz let ab_inst_to_real = function | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw @@ -372,6 +373,7 @@ let ab_inst_to_real = function | "Psxwd" -> Sxwd | "Pzxwd" -> Zxwd | "Pfloatwrnsz" -> Floatwz + | "Pfixedwrzz" -> Fixedwz | "Plb" -> Lbs | "Plbu" -> Lbz @@ -433,7 +435,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 + | Fixedwz | 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 @@ -452,7 +454,7 @@ let real_inst_to_latency = function | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make | Sxwd | Zxwd -> 1 - | Floatwz -> 4 + | Floatwz | Fixedwz -> 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 ceea8de5..492687cd 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -154,7 +154,7 @@ Proof. 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.
+ all: try (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 9a96cf3b..1a73ae7a 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -296,6 +296,8 @@ module Target (*: TARGET*) = 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 + | Pfixedwrzz(rd, rs) -> + fprintf oc " fixedw.rz %a = %a, 0\n" ireg rd ireg rs (* Arith RI32 instructions *) | Pmake (rd, imm) -> diff --git a/test/mppa/instr/floatconv.c b/test/mppa/instr/floatconv.c new file mode 100644 index 00000000..025f968b --- /dev/null +++ b/test/mppa/instr/floatconv.c @@ -0,0 +1,9 @@ +#include "framework.h" + +float int2float(int v){ + return v; +} + +BEGIN_TEST(int) + c = (int) int2float(a) + (int) int2float(b) + (int) int2float(42.3); +END_TEST() |