aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v16
-rw-r--r--mppa_k1c/Asmblock.v16
-rw-r--r--mppa_k1c/Asmblockdeps.v6
-rw-r--r--mppa_k1c/Asmblockgen.v24
-rw-r--r--mppa_k1c/PostpassScheduling.v1
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml18
-rw-r--r--mppa_k1c/SelectLong.v17
-rw-r--r--mppa_k1c/SelectLong.vp17
-rw-r--r--mppa_k1c/SelectLongproof.v16
-rw-r--r--mppa_k1c/TargetPrinter.ml10
-rw-r--r--runtime/Makefile6
-rw-r--r--test/mppa/instr/faddw.c4
-rw-r--r--test/mppa/instr/fmulw.c2
-rw-r--r--test/mppa/instr/fnegw.c2
-rw-r--r--test/mppa/instr/fsbfw.c2
15 files changed, 123 insertions, 34 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 7c735bf1..d930b168 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -103,11 +103,17 @@ Inductive instruction : Type :=
| Pfnegw (rd rs: ireg) (**r float negate word *)
| Pfnarrowdw (rd rs: ireg) (**r float narrow 64 -> 32 bits *)
| Pfwidenlwd (rd rs: ireg) (**r float widen 32 -> 64 bits *)
- | Pfloatwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer *)
+ | Pfloatwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (32 -> 32) *)
+ | Pfloatuwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (u32 -> 32) *)
| Pfloatudrnsz (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (64 bits) *)
+ | Pfloatudrnsz_i32 (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (32 bits) *)
| 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 *)
- | Pfixeddrzz (rd rs: ireg) (**r Integer conversion from floating point (64 bits) *)
+ | 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) *)
+ | Pfixedudrzz_i32 (rd rs: ireg) (**r unsigned Integer conversion from floating point (u32 -> 64 bits) *)
(** Arith RI32 *)
| Pmake (rd: ireg) (imm: int) (**r load immediate *)
@@ -216,11 +222,17 @@ Definition basic_to_instruction (b: basic) :=
| PArithRR Asmblock.Pfnegw rd rs => Pfnegw rd rs
| PArithRR Asmblock.Pfnarrowdw rd rs => Pfnarrowdw rd rs
| PArithRR Asmblock.Pfwidenlwd rd rs => Pfwidenlwd rd rs
+ | PArithRR Asmblock.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs
| PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
| PArithRR Asmblock.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs
| PArithRR Asmblock.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs
+ | 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.Pfixeddrzz rd rs => Pfixeddrzz rd rs
+ | PArithRR Asmblock.Pfixedudrzz rd rs => Pfixedudrzz rd rs
+ | PArithRR Asmblock.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs
+ | PArithRR Asmblock.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs
(* RI32 *)
| PArithRI32 Asmblock.Pmake rd imm => Pmake rd imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index cade1ba8..a5c7f495 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -287,11 +287,17 @@ Inductive arith_name_rr : Type :=
| Pfnegw (**r float negate word *)
| Pfnarrowdw (**r float narrow 64 -> 32 bits *)
| Pfwidenlwd (**r Floating Point widen from 32 bits to 64 bits *)
- | Pfloatwrnsz (**r Floating Point Conversion from integer (int -> single) *)
- | Pfloatudrnsz (**r Floating Point Conversion from unsigned integer (ulong -> float) *)
+ | Pfloatwrnsz (**r Floating Point conversion from integer (int -> SINGLE) *)
+ | Pfloatuwrnsz (**r Floating Point conversion from integer (unsigned int -> SINGLE) *)
+ | Pfloatudrnsz (**r Floating Point Conversion from integer (unsigned long -> float) *)
+ | Pfloatudrnsz_i32 (**r Floating Point Conversion from integer (unsigned int -> float) *)
| 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) *)
| 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) *)
+ | Pfixedudrzz_i32 (**r Integer conversion from floating point (float -> unsigned int) *)
.
Inductive arith_name_ri32 : Type :=
@@ -936,10 +942,16 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset
| Pfnarrowdw => rs#d <- (Val.singleoffloat rs#s)
| Pfwidenlwd => rs#d <- (Val.floatofsingle rs#s)
| Pfloatwrnsz => rs#d <- (match Val.singleofint rs#s with Some f => f | _ => Vundef end)
+ | Pfloatuwrnsz => rs#d <- (match Val.singleofintu rs#s with Some f => f | _ => Vundef end)
| Pfloatudrnsz => rs#d <- (match Val.floatoflongu rs#s with Some f => f | _ => Vundef end)
+ | Pfloatudrnsz_i32 => rs#d <- (match Val.floatofintu rs#s with Some f => f | _ => Vundef end)
| 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)
| 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)
+ | Pfixedudrzz_i32 => rs#d <- (match Val.intuoffloat rs#s with Some i => i | _ => Vundef end)
end
| PArithRI32 n d i =>
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 4d1a0d38..ee087d44 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -117,10 +117,16 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
| Pfnarrowdw => Some (Val (Val.singleoffloat v))
| Pfwidenlwd => Some (Val (Val.floatofsingle v))
| Pfloatwrnsz => Some (Val (match Val.singleofint v with Some f => f | _ => Vundef end))
+ | Pfloatuwrnsz => Some (Val (match Val.singleofintu v with Some f => f | _ => Vundef end))
| Pfloatudrnsz => Some (Val (match Val.floatoflongu v with Some f => f | _ => Vundef end))
| Pfloatdrnsz => Some (Val (match Val.floatoflong v with Some f => f | _ => Vundef end))
+ | 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))
| 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))
+ | Pfixedudrzz_i32 => Some (Val (match Val.intuoffloat v with Some i => i | _ => Vundef end))
end
| OArithRI32 n i, [] =>
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 95bb5a36..8dfa2cee 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -579,18 +579,42 @@ Definition transl_op
| Osingleofint, a1 :: nil =>
do rd <- freg_of res; do rs <- ireg_of a1;
OK (Pfloatwrnsz rd rs ::i k)
+ | Osingleofintu, a1 :: nil =>
+ do rd <- freg_of res; do rs <- ireg_of a1;
+ OK (Pfloatuwrnsz rd rs ::i k)
| Ofloatoflong, a1 :: nil =>
do rd <- freg_of res; do rs <- ireg_of a1;
OK (Pfloatdrnsz rd rs ::i k)
| Ofloatoflongu, a1 :: nil =>
do rd <- freg_of res; do rs <- ireg_of a1;
OK (Pfloatudrnsz rd rs ::i k)
+ | Ofloatofint, a1 :: nil =>
+ do rd <- freg_of res; do rs <- ireg_of a1;
+ OK (Pfloatdrnsz_i32 rd rs ::i k)
+ | 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)
| 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)
| Ofloatofsingle, a1 :: nil =>
do rd <- freg_of res; do rs <- freg_of a1;
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 6bf97279..fa0ebfe6 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -13,7 +13,6 @@
Require Import Coqlib Errors AST Integers.
Require Import Asmblock Axioms Memory Globalenvs.
Require Import Asmblockdeps Asmblockgenproof0.
-Require Import ImpDep.
Local Open Scope error_monad_scope.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 54a27966..d9a60fb4 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -40,10 +40,16 @@ let arith_rr_str = function
| Pfnarrowdw -> "Pfnarrowdw"
| Pfwidenlwd -> "Pfwidenlwd"
| Pfloatwrnsz -> "Pfloatwrnsz"
+ | Pfloatuwrnsz -> "Pfloatuwrnsz"
+ | Pfloatudrnsz_i32 -> "Pfloatudrnsz_i32"
| Pfloatudrnsz -> "Pfloatudrnsz"
| Pfloatdrnsz -> "Pfloatdrnsz"
+ | Pfloatdrnsz_i32 -> "Pfloatdrnsz_i32"
| Pfixedwrzz -> "Pfixedwrzz"
| Pfixeddrzz -> "Pfixeddrzz"
+ | Pfixedudrzz -> "Pfixedudrzz"
+ | Pfixeddrzz_i32 -> "Pfixeddrzz_i32"
+ | Pfixedudrzz_i32 -> "Pfixedudrzz_i32"
let arith_rrr_str = function
| Pcompw it -> "Pcompw"
@@ -365,7 +371,7 @@ type real_instruction =
(* FPU *)
| Fabsd | Fabsw | Fnegw | Fnegd
| Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
- | Fnarrowdw | Fwidenlwd | Floatwz | Floatdz | Floatudz | Fixedwz | Fixeddz
+ | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeddz | Fixedudz
let ab_inst_to_real = function
| "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw
@@ -395,10 +401,16 @@ let ab_inst_to_real = function
| "Pfnarrowdw" -> Fnarrowdw
| "Pfwidenlwd" -> Fwidenlwd
| "Pfloatwrnsz" -> Floatwz
+ | "Pfloatuwrnsz" -> Floatuwz
| "Pfloatdrnsz" -> Floatdz
+ | "Pfloatdrnsz_i32" -> Floatdz
| "Pfloatudrnsz" -> Floatudz
+ | "Pfloatudrnsz_i32" -> Floatudz
| "Pfixedwrzz" -> Fixedwz
| "Pfixeddrzz" -> Fixeddz
+ | "Pfixedudrzz" -> Fixedudz
+ | "Pfixeddrzz_i32" -> Fixeddz
+ | "Pfixedudrzz_i32" -> Fixedudz
| "Plb" -> Lbs
| "Plbu" -> Lbz
@@ -469,7 +481,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 | Fixeddz | Floatdz | Floatudz -> mau
+ | 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
@@ -490,7 +502,7 @@ let real_inst_to_latency = function
| Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
| Sxwd | Zxwd
-> 1
- | Floatwz | Fixedwz | Floatdz | Floatudz | Fixeddz -> 4
+ | Floatwz | Floatuwz | 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/SelectLong.v b/mppa_k1c/SelectLong.v
index f2aa6be2..ea42b9c3 100644
--- a/mppa_k1c/SelectLong.v
+++ b/mppa_k1c/SelectLong.v
@@ -755,20 +755,29 @@ Definition floatoflongu (e: expr) :=
if Archi.splitlong then SplitLong.floatoflongu e else
Eop Ofloatoflongu (e:::Enil).
-Definition longofsingle (e: expr) :=
+(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *)
+Definition longofsingle (e: expr) := SplitLong.longofsingle e.
+(*
if Archi.splitlong then SplitLong.longofsingle e else
Eop Olongofsingle (e:::Enil).
+*)
-Definition longuofsingle (e: expr) :=
+Definition longuofsingle (e: expr) := SplitLong.longuofsingle e.
+(*
if Archi.splitlong then SplitLong.longuofsingle e else
Eop Olonguofsingle (e:::Enil).
+*)
-Definition singleoflong (e: expr) :=
+Definition singleoflong (e: expr) := SplitLong.singleoflong e.
+(*
if Archi.splitlong then SplitLong.singleoflong e else
Eop Osingleoflong (e:::Enil).
+*)
-Definition singleoflongu (e: expr) :=
+Definition singleoflongu (e: expr) := SplitLong.singleoflongu e.
+(*
if Archi.splitlong then SplitLong.singleoflongu e else
Eop Osingleoflongu (e:::Enil).
+*)
End SELECT.
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 26735c99..a3aefb15 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -341,20 +341,29 @@ Definition floatoflongu (e: expr) :=
if Archi.splitlong then SplitLong.floatoflongu e else
Eop Ofloatoflongu (e:::Enil).
-Definition longofsingle (e: expr) :=
+(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *)
+Definition longofsingle (e: expr) := SplitLong.longofsingle e.
+(*
if Archi.splitlong then SplitLong.longofsingle e else
Eop Olongofsingle (e:::Enil).
+*)
-Definition longuofsingle (e: expr) :=
+Definition longuofsingle (e: expr) := SplitLong.longuofsingle e.
+(*
if Archi.splitlong then SplitLong.longuofsingle e else
Eop Olonguofsingle (e:::Enil).
+*)
-Definition singleoflong (e: expr) :=
+Definition singleoflong (e: expr) := SplitLong.singleoflong e.
+(*
if Archi.splitlong then SplitLong.singleoflong e else
Eop Osingleoflong (e:::Enil).
+*)
-Definition singleoflongu (e: expr) :=
+Definition singleoflongu (e: expr) := SplitLong.singleoflongu e.
+(*
if Archi.splitlong then SplitLong.singleoflongu e else
Eop Osingleoflongu (e:::Enil).
+*)
End SELECT.
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index d12fb9ae..44846a6f 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -582,30 +582,30 @@ Qed.
Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
Proof.
- unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL.
+ unfold longofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
eapply SplitLongproof.eval_longofsingle; eauto.
- TrivialExists.
+(* TrivialExists. *)
Qed.
Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle.
Proof.
- unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL.
+ unfold longuofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
eapply SplitLongproof.eval_longuofsingle; eauto.
- TrivialExists.
+(* TrivialExists. *)
Qed.
Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
Proof.
- unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL.
+ unfold singleoflong; red; intros. (* destruct Archi.splitlong eqn:SL. *)
eapply SplitLongproof.eval_singleoflong; eauto.
- TrivialExists.
+(* TrivialExists. *)
Qed.
Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
Proof.
- unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL.
+ unfold singleoflongu; red; intros. (* destruct Archi.splitlong eqn:SL. *)
eapply SplitLongproof.eval_singleoflongu; eauto.
- TrivialExists.
+(* TrivialExists. *)
Qed.
End CMCONSTR.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index c1339af5..8d053cde 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -302,16 +302,20 @@ module Target (*: TARGET*) =
fprintf oc " fnarrowdw %a = %a\n" ireg rd ireg rs
| Pfwidenlwd(rd, rs) ->
fprintf oc " fwidenlwd %a = %a\n" ireg rd ireg rs
+ | Pfloatuwrnsz(rd, rs) ->
+ fprintf oc " floatuw.rn.s %a = %a, 0\n" ireg rd ireg rs
| Pfloatwrnsz(rd, rs) ->
fprintf oc " floatw.rn.s %a = %a, 0\n" ireg rd ireg rs
- | Pfloatudrnsz(rd, rs) ->
+ | Pfloatudrnsz(rd, rs) | Pfloatudrnsz_i32(rd, rs) ->
fprintf oc " floatud.rn.s %a = %a, 0\n" ireg rd ireg rs
- | Pfloatdrnsz(rd, rs) ->
+ | Pfloatdrnsz(rd, rs) | Pfloatdrnsz_i32(rd, rs) ->
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
- | Pfixeddrzz(rd, 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) ->
+ fprintf oc " fixedud.rz %a = %a, 0\n" ireg rd ireg rs
(* Arith RI32 instructions *)
| Pmake (rd, imm) ->
diff --git a/runtime/Makefile b/runtime/Makefile
index 66ec6fec..f58d4b6a 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -23,7 +23,9 @@ OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o
else ifeq ($(ARCH),powerpc64)
OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o
else ifeq ($(ARCH),mppa_k1c)
-OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o
+OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o\
+ i64_dtos.o i64_dtou.o i64_utod.o i64_utof.o i64_stod.o i64_stof.o
+# Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o
DOMAKE:=$(shell (cd mppa_k1c && make))
else
OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
@@ -66,7 +68,7 @@ $(LIB): $(OBJS)
../ccomp -O2 -S -o $*.s -I./c c/$*.c
sed -i -e 's/i64_/__compcert_i64_/g' $*.s
$(CASMRUNTIME) -o $*.o $*.s
- @rm -f $*.s
+ @rm $*.s
clean::
rm -f *.o $(LIB) *.tmp?.s
diff --git a/test/mppa/instr/faddw.c b/test/mppa/instr/faddw.c
index a00e9afe..e0e635ae 100644
--- a/test/mppa/instr/faddw.c
+++ b/test/mppa/instr/faddw.c
@@ -1,5 +1,5 @@
#include "framework.h"
-BEGIN_TEST(double)
+BEGIN_TEST(float)
c = ((float)a + (float)b);
-END_TESTF64()
+END_TESTF32()
diff --git a/test/mppa/instr/fmulw.c b/test/mppa/instr/fmulw.c
index 67d645c3..f85eba64 100644
--- a/test/mppa/instr/fmulw.c
+++ b/test/mppa/instr/fmulw.c
@@ -1,6 +1,6 @@
#include "framework.h"
-BEGIN_TEST(double)
+BEGIN_TEST(float)
{
c = ((float)a * (float)b);
}
diff --git a/test/mppa/instr/fnegw.c b/test/mppa/instr/fnegw.c
index acbabf68..fbeaab8e 100644
--- a/test/mppa/instr/fnegw.c
+++ b/test/mppa/instr/fnegw.c
@@ -1,6 +1,6 @@
#include "framework.h"
-BEGIN_TEST(double)
+BEGIN_TEST(float)
{
c = (-(float)a);
}
diff --git a/test/mppa/instr/fsbfw.c b/test/mppa/instr/fsbfw.c
index 835963d5..067c40b5 100644
--- a/test/mppa/instr/fsbfw.c
+++ b/test/mppa/instr/fsbfw.c
@@ -1,6 +1,6 @@
#include "framework.h"
-BEGIN_TEST(double)
+BEGIN_TEST(float)
{
c = ((float)a - (float)b);
}
generated by cgit (git 2.34.1) at 2024-06-03 04:22:25 +0000