aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Archi.v37
-rw-r--r--mppa_k1c/Asm.v20
-rw-r--r--mppa_k1c/Asmblockdeps.v9
-rw-r--r--mppa_k1c/Asmblockgen.v40
-rw-r--r--mppa_k1c/Asmexpand.ml4
-rw-r--r--mppa_k1c/Asmvliw.v19
-rw-r--r--mppa_k1c/Builtins1.v66
-rw-r--r--mppa_k1c/CBuiltins.ml23
-rw-r--r--mppa_k1c/ExtFloats.v39
-rw-r--r--mppa_k1c/ExtValues.v49
-rw-r--r--mppa_k1c/Machregs.v2
-rw-r--r--mppa_k1c/NeedOp.v60
-rw-r--r--mppa_k1c/Op.v73
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml22
-rw-r--r--mppa_k1c/SelectOp.vp41
-rw-r--r--mppa_k1c/SelectOpproof.v103
-rw-r--r--mppa_k1c/TargetPrinter.ml22
-rw-r--r--mppa_k1c/ValueAOp.v134
18 files changed, 724 insertions, 39 deletions
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index 96571841..cdcf58c3 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -16,7 +16,8 @@
(** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *)
-Require Import ZArith.
+Require Import ZArith List.
+(*From Flocq*)
Require Import Binary Bits.
Definition ptr64 := true.
@@ -33,6 +34,8 @@ Proof.
unfold splitlong. destruct ptr64; simpl; congruence.
Qed.
+(** THIS IS NOT CHECKED ! NONE OF THIS ! *)
+
(** Section 7.3: "Except when otherwise stated, if the result of a
floating-point operation is NaN, it is the canonical NaN. The
canonical NaN has a positive sign and all significand bits clear
@@ -40,26 +43,36 @@ Qed.
We need to extend the [choose_binop_pl] functions to account for
this case. *)
-Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
- exist _ (B754_nan 53 1024 true (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
+Definition default_nan_32 := (false, iter_nat 22 _ xO xH).
-Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
- false. (**r always choose first NaN *)
+(* Always choose the first NaN argument, if any *)
-Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
- exist _ (B754_nan 24 128 true (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
+Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
+ match l with nil => default_nan_64 | n :: _ => n end.
-Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
- false. (**r always choose first NaN *)
+Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
+ match l with nil => default_nan_32 | n :: _ => n end.
-(* TODO check *)
Definition fpu_returns_default_qNaN := false.
+Lemma choose_nan_64_idem: forall n,
+ choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
+Proof. auto. Qed.
+
+Lemma choose_nan_32_idem: forall n,
+ choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
+Proof. auto. Qed.
+
+Definition fma_order {A: Type} (x y z: A) := (x, z, y).
+
+Definition fma_invalid_mul_is_nan := false.
Definition float_of_single_preserves_sNaN := false.
Global Opaque ptr64 big_endian splitlong
- default_nan_64 choose_binop_pl_64
- default_nan_32 choose_binop_pl_32
+ default_nan_64 choose_nan_64
+ default_nan_32 choose_nan_32
+ fma_order fma_invalid_mul_is_nan
float_of_single_preserves_sNaN.
(** Whether to generate position-independent code or not *)
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index a0c5e71c..f09aa99c 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -204,6 +204,10 @@ Inductive instruction : Type :=
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
| Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
| Pmsubw (rd rs1 rs2: ireg) (**r multiply-add words *)
+ | Pfmaddfw (rd rs1 rs2: ireg) (**r float fused multiply-add words *)
+ | Pfmsubfw (rd rs1 rs2: ireg) (**r float fused multiply-subtract words *)
+ | Pfmaddfl (rd rs1 rs2: ireg) (**r float fused multiply-add longs *)
+ | Pfmsubfl (rd rs1 rs2: ireg) (**r float fused multiply-subtract longs *)
| Paddl (rd rs1 rs2: ireg) (**r add long *)
| Paddxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r add long shift *)
@@ -231,7 +235,12 @@ Inductive instruction : Type :=
| Pfsbfw (rd rs1 rs2: ireg) (**r Float sub word *)
| Pfmuld (rd rs1 rs2: ireg) (**r Float mul double *)
| Pfmulw (rd rs1 rs2: ireg) (**r Float mul word *)
-
+ | Pfmind (rd rs1 rs2: ireg) (**r Float min double *)
+ | Pfminw (rd rs1 rs2: ireg) (**r Float min word *)
+ | Pfmaxd (rd rs1 rs2: ireg) (**r Float max double *)
+ | Pfmaxw (rd rs1 rs2: ireg) (**r Float max word *)
+ | Pfinvw (rd rs1: ireg) (**r Float invert word *)
+
(** Arith RRI32 *)
| Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *)
@@ -327,6 +336,7 @@ Definition basic_to_instruction (b: basic) :=
| PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs
| PArithRR Asmvliw.Pfnegd rd rs => Pfnegd rd rs
| PArithRR Asmvliw.Pfnegw rd rs => Pfnegw rd rs
+ | PArithRR Asmvliw.Pfinvw rd rs => Pfinvw rd rs
| PArithRR Asmvliw.Pfnarrowdw rd rs => Pfnarrowdw rd rs
| PArithRR Asmvliw.Pfwidenlwd rd rs => Pfwidenlwd rd rs
| PArithRR Asmvliw.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs
@@ -399,6 +409,10 @@ Definition basic_to_instruction (b: basic) :=
| PArithRRR Asmvliw.Pfsbfw rd rs1 rs2 => Pfsbfw rd rs1 rs2
| PArithRRR Asmvliw.Pfmuld rd rs1 rs2 => Pfmuld rd rs1 rs2
| PArithRRR Asmvliw.Pfmulw rd rs1 rs2 => Pfmulw rd rs1 rs2
+ | PArithRRR Asmvliw.Pfmind rd rs1 rs2 => Pfmind rd rs1 rs2
+ | PArithRRR Asmvliw.Pfminw rd rs1 rs2 => Pfminw rd rs1 rs2
+ | PArithRRR Asmvliw.Pfmaxd rd rs1 rs2 => Pfmaxd rd rs1 rs2
+ | PArithRRR Asmvliw.Pfmaxw rd rs1 rs2 => Pfmaxw rd rs1 rs2
(* RRI32 *)
| PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
@@ -446,6 +460,10 @@ Definition basic_to_instruction (b: basic) :=
| PArithARRR Asmvliw.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
| PArithARRR Asmvliw.Pmsubw rd rs1 rs2 => Pmsubw rd rs1 rs2
| PArithARRR Asmvliw.Pmsubl rd rs1 rs2 => Pmsubl rd rs1 rs2
+ | PArithARRR Asmvliw.Pfmaddfw rd rs1 rs2 => Pfmaddfw rd rs1 rs2
+ | PArithARRR Asmvliw.Pfmaddfl rd rs1 rs2 => Pfmaddfl rd rs1 rs2
+ | PArithARRR Asmvliw.Pfmsubfw rd rs1 rs2 => Pfmsubfw rd rs1 rs2
+ | PArithARRR Asmvliw.Pfmsubfl rd rs1 rs2 => Pfmsubfl rd rs1 rs2
| PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
| PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 2d144bb6..c4c1bbf1 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1338,6 +1338,7 @@ Definition string_of_name_rr (n: arith_name_rr): pstring :=
| Pfabsw => "Pfabsw"
| Pfnegd => "Pfnegd"
| Pfnegw => "Pfnegw"
+ | Pfinvw => "Pfinvw"
| Pfnarrowdw => "Pfnarrowdw"
| Pfwidenlwd => "Pfwidenlwd"
| Pfloatwrnsz => "Pfloatwrnsz"
@@ -1418,6 +1419,10 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
| Pfsbfw => "Pfsbfw"
| Pfmuld => "Pfmuld"
| Pfmulw => "Pfmulw"
+ | Pfmind => "Pfmind"
+ | Pfminw => "Pfminw"
+ | Pfmaxd => "Pfmaxd"
+ | Pfmaxw => "Pfmaxw"
end.
Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
@@ -1473,6 +1478,10 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
| Pmsubl => "Pmsubl"
| Pcmove _ => "Pcmove"
| Pcmoveu _ => "Pcmoveu"
+ | Pfmaddfw => "Pfmaddfw"
+ | Pfmaddfl => "Pfmaddfl"
+ | Pfmsubfw => "Pfmsubfw"
+ | Pfmsubfl => "Pfmsubfl"
end.
Definition string_of_name_arr (n: arith_name_arr): pstring :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 7e415c2a..ade84e7b 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -740,12 +740,52 @@ Definition transl_op
| Omulfs, a1 :: a2 :: nil =>
do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
OK (Pfmulw rd rs1 rs2 ::i k)
+ | Ominf, a1 :: a2 :: nil =>
+ do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+ OK (Pfmind rd rs1 rs2 ::i k)
+ | Ominfs, a1 :: a2 :: nil =>
+ do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+ OK (Pfminw rd rs1 rs2 ::i k)
+ | Omaxf, a1 :: a2 :: nil =>
+ do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+ OK (Pfmaxd rd rs1 rs2 ::i k)
+ | Omaxfs, a1 :: a2 :: nil =>
+ do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+ OK (Pfmaxw rd rs1 rs2 ::i k)
| Onegf, a1 :: nil =>
do rd <- freg_of res; do rs <- freg_of a1;
OK (Pfnegd rd rs ::i k)
| Onegfs, a1 :: nil =>
do rd <- freg_of res; do rs <- freg_of a1;
OK (Pfnegw rd rs ::i k)
+ | Oinvfs, a1 :: nil =>
+ do rd <- freg_of res; do rs <- freg_of a1;
+ OK (Pfinvw rd rs ::i k)
+
+ | Ofmaddf, a1 :: a2 :: a3 :: nil =>
+ assertion (mreg_eq a1 res);
+ do rs1 <- freg_of a1;
+ do rs2 <- freg_of a2;
+ do rs3 <- freg_of a3;
+ OK (Pfmaddfl rs1 rs2 rs3 ::i k)
+ | Ofmaddfs, a1 :: a2 :: a3 :: nil =>
+ assertion (mreg_eq a1 res);
+ do rs1 <- freg_of a1;
+ do rs2 <- freg_of a2;
+ do rs3 <- freg_of a3;
+ OK (Pfmaddfw rs1 rs2 rs3 ::i k)
+ | Ofmsubf, a1 :: a2 :: a3 :: nil =>
+ assertion (mreg_eq a1 res);
+ do rs1 <- freg_of a1;
+ do rs2 <- freg_of a2;
+ do rs3 <- freg_of a3;
+ OK (Pfmsubfl rs1 rs2 rs3 ::i k)
+ | Ofmsubfs, a1 :: a2 :: a3 :: nil =>
+ assertion (mreg_eq a1 res);
+ do rs1 <- freg_of a1;
+ do rs2 <- freg_of a2;
+ do rs3 <- freg_of a3;
+ OK (Pfmsubfw rs1 rs2 rs3 ::i k)
| Osingleofint, a1 :: nil =>
do rd <- freg_of res; do rs <- ireg_of a1;
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 20d27951..1e5149fd 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -467,11 +467,11 @@ let expand_builtin_inline name args res = let open Asmvliw in
emit (Pdzerol addr)
(*| "__builtin_k1_afaddd", [BA(IR addr); BA (IR incr_res)], BR(IR res) ->
(if res <> incr_res
- then (emit (Pmv(res, incr_res)); emit Psemi));
+ then (emit (Asm.Pmv(res, incr_res)); emit Psemi));
emit (Pafaddd(addr, res))
| "__builtin_k1_afaddw", [BA(IR addr); BA (IR incr_res)], BR(IR res) ->
(if res <> incr_res
- then (emit (Pmv(res, incr_res)); emit Psemi));
+ then (emit (Asm.Pmv(res, incr_res)); emit Psemi));
emit (Pafaddw(addr, res)) *) (* see #157 *)
| "__builtin_alclrd", [BA(IR addr)], BR(IR res) ->
emit (Palclrd(res, addr))
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 72584d2a..54654abb 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -375,6 +375,7 @@ Inductive arith_name_rr : Type :=
| Pfabsw (**r float absolute word *)
| Pfnegd (**r float negate double *)
| Pfnegw (**r float negate word *)
+ | Pfinvw (**r float invert 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) *)
@@ -453,6 +454,10 @@ Inductive arith_name_rrr : Type :=
| Pfsbfw (**r float sub word *)
| Pfmuld (**r float multiply double *)
| Pfmulw (**r float multiply word *)
+ | Pfmind (**r float min double *)
+ | Pfminw (**r float min word *)
+ | Pfmaxd (**r float max double *)
+ | Pfmaxw (**r float max word *)
.
Inductive arith_name_rri32 : Type :=
@@ -506,6 +511,10 @@ Inductive arith_name_arrr : Type :=
| Pmsubl (**r multiply subtract long *)
| Pcmove (bt: btest) (**r conditional move *)
| Pcmoveu (bt: btest) (**r conditional move, test on unsigned semantics *)
+ | Pfmaddfw (**r float fused multiply add word *)
+ | Pfmaddfl (**r float fused multiply add long *)
+ | Pfmsubfw (**r float fused multiply subtract word *)
+ | Pfmsubfl (**r float fused multiply subtract long *)
.
Inductive arith_name_arri32 : Type :=
@@ -975,6 +984,7 @@ Definition arith_eval_rr n v :=
| Pfnegw => Val.negfs v
| Pfabsd => Val.absf v
| Pfabsw => Val.absfs v
+ | Pfinvw => ExtValues.invfs v
| Pfnarrowdw => Val.singleoffloat v
| Pfwidenlwd => Val.floatofsingle v
| Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end
@@ -1055,6 +1065,11 @@ Definition arith_eval_rrr n v1 v2 :=
| Pfmuld => Val.mulf v1 v2
| Pfmulw => Val.mulfs v1 v2
+ | Pfmind => ExtValues.minf v1 v2
+ | Pfminw => ExtValues.minfs v1 v2
+ | Pfmaxd => ExtValues.maxf v1 v2
+ | Pfmaxw => ExtValues.maxfs v1 v2
+
| Paddxw shift => ExtValues.addx (int_of_shift1_4 shift) v1 v2
| Paddxl shift => ExtValues.addxl (int_of_shift1_4 shift) v1 v2
@@ -1149,6 +1164,10 @@ Definition arith_eval_arrr n v1 v2 v3 :=
| Pmsubl => Val.subl v1 (Val.mull v2 v3)
| Pcmove bt => cmove bt v1 v2 v3
| Pcmoveu bt => cmoveu bt v1 v2 v3
+ | Pfmaddfw => ExtValues.fmaddfs v1 v2 v3
+ | Pfmaddfl => ExtValues.fmaddf v1 v2 v3
+ | Pfmsubfw => ExtValues.fmsubfs v1 v2 v3
+ | Pfmsubfl => ExtValues.fmsubf v1 v2 v3
end.
Definition arith_eval_arr n v1 v2 :=
diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v
new file mode 100644
index 00000000..6186961f
--- /dev/null
+++ b/mppa_k1c/Builtins1.v
@@ -0,0 +1,66 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, Collège de France and Inria Paris *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(** Platform-specific built-in functions *)
+
+Require Import String Coqlib.
+Require Import AST Integers Floats Values ExtFloats.
+Require Import Builtins0.
+
+Inductive platform_builtin : Type :=
+| BI_fmin
+| BI_fmax
+| BI_fminf
+| BI_fmaxf
+| BI_fabsf
+| BI_fma
+| BI_fmaf.
+
+Local Open Scope string_scope.
+
+Definition platform_builtin_table : list (string * platform_builtin) :=
+ ("__builtin_fmin", BI_fmin)
+ :: ("__builtin_fmax", BI_fmax)
+ :: ("__builtin_fminf", BI_fminf)
+ :: ("__builtin_fmaxf", BI_fmaxf)
+ :: ("__builtin_fabsf", BI_fabsf)
+ :: ("__builtin_fma", BI_fma)
+ :: ("__builtin_fmaf", BI_fmaf)
+ :: nil.
+
+Definition platform_builtin_sig (b: platform_builtin) : signature :=
+ match b with
+ | BI_fmin | BI_fmax =>
+ mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default
+ | BI_fminf | BI_fmaxf =>
+ mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default
+ | BI_fabsf =>
+ mksignature (Tsingle :: nil) (Some Tsingle) cc_default
+ | BI_fma =>
+ mksignature (Tfloat :: Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default
+ | BI_fmaf =>
+ mksignature (Tsingle :: Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default
+ end.
+
+Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
+ match b with
+ | BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.min
+ | BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.max
+ | BI_fminf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.min
+ | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max
+ | BI_fabsf => mkbuiltin_n1t Tsingle Tsingle Float32.abs
+ | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma
+ | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma
+ end.
diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml
index 5fb69f62..235496c5 100644
--- a/mppa_k1c/CBuiltins.ml
+++ b/mppa_k1c/CBuiltins.ml
@@ -18,11 +18,11 @@
open C
let builtins = {
- Builtins.typedefs = [
+ builtin_typedefs = [
"__builtin_va_list", TPtr(TVoid [], [])
];
(* The builtin list is inspired from the GCC file builtin_k1.h *)
- Builtins.functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *)
+ builtin_functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *)
(* BCU Instructions *)
"__builtin_k1_await", (TVoid [], [], false); (* DONE *)
"__builtin_k1_barrier", (TVoid [], [], false); (* DONE *)
@@ -113,14 +113,29 @@ let builtins = {
[TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
"__builtin_fnmsub",
(TFloat(FDouble, []),
- [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
+ [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false); *)
+ "__builtin_fabsf",
+ (TFloat(FFloat, []),
+ [TFloat(FFloat, [])], false);
"__builtin_fmax",
(TFloat(FDouble, []),
[TFloat(FDouble, []); TFloat(FDouble, [])], false);
"__builtin_fmin",
(TFloat(FDouble, []),
[TFloat(FDouble, []); TFloat(FDouble, [])], false);
-*)]
+ "__builtin_fmaxf",
+ (TFloat(FFloat, []),
+ [TFloat(FFloat, []); TFloat(FFloat, [])], false);
+ "__builtin_fminf",
+ (TFloat(FFloat, []),
+ [TFloat(FFloat, []); TFloat(FFloat, [])], false);
+ "__builtin_fma",
+ (TFloat(FDouble, []),
+ [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
+ "__builtin_fmaf",
+ (TFloat(FFloat, []),
+ [TFloat(FFloat, []); TFloat(FFloat, []); TFloat(FFloat, [])], false);
+]
}
let va_list_type = TPtr(TVoid [], []) (* to check! *)
diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v
new file mode 100644
index 00000000..d9b9d3a6
--- /dev/null
+++ b/mppa_k1c/ExtFloats.v
@@ -0,0 +1,39 @@
+Require Import Floats Integers ZArith.
+
+Module ExtFloat.
+(** TODO check with the actual K1c;
+ this is what happens on x86 and may be inappropriate. *)
+
+Definition min (x : float) (y : float) : float :=
+ match Float.compare x y with
+ | Some Eq | Some Lt => x
+ | Some Gt | None => y
+ end.
+
+Definition max (x : float) (y : float) : float :=
+ match Float.compare x y with
+ | Some Eq | Some Gt => x
+ | Some Lt | None => y
+ end.
+End ExtFloat.
+
+Module ExtFloat32.
+(** TODO check with the actual K1c *)
+
+Definition min (x : float32) (y : float32) : float32 :=
+ match Float32.compare x y with
+ | Some Eq | Some Lt => x
+ | Some Gt | None => y
+ end.
+
+Definition max (x : float32) (y : float32) : float32 :=
+ match Float32.compare x y with
+ | Some Eq | Some Gt => x
+ | Some Lt | None => y
+ end.
+
+Definition one := Float32.of_int (Int.repr (1%Z)).
+Definition inv (x : float32) : float32 :=
+ Float32.div one x.
+
+End ExtFloat32.
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index e9c62a8d..5a890f3c 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -1,6 +1,7 @@
Require Import Coqlib.
Require Import Integers.
Require Import Values.
+Require Import Floats ExtFloats.
Open Scope Z_scope.
@@ -689,3 +690,51 @@ Definition revsubx sh v1 v2 :=
Definition revsubxl sh v1 v2 :=
Val.subl v2 (Val.shll v1 (Vint sh)).
+
+Definition minf v1 v2 :=
+ match v1, v2 with
+ | (Vfloat f1), (Vfloat f2) => Vfloat (ExtFloat.min f1 f2)
+ | _, _ => Vundef
+ end.
+
+Definition maxf v1 v2 :=
+ match v1, v2 with
+ | (Vfloat f1), (Vfloat f2) => Vfloat (ExtFloat.max f1 f2)
+ | _, _ => Vundef
+ end.
+
+Definition minfs v1 v2 :=
+ match v1, v2 with
+ | (Vsingle f1), (Vsingle f2) => Vsingle (ExtFloat32.min f1 f2)
+ | _, _ => Vundef
+ end.
+
+Definition maxfs v1 v2 :=
+ match v1, v2 with
+ | (Vsingle f1), (Vsingle f2) => Vsingle (ExtFloat32.max f1 f2)
+ | _, _ => Vundef
+ end.
+
+Definition invfs v1 :=
+ match v1 with
+ | (Vsingle f1) => Vsingle (ExtFloat32.inv f1)
+ | _ => Vundef
+ end.
+
+Definition triple_op_float f v1 v2 v3 :=
+ match v1, v2, v3 with
+ | (Vfloat f1), (Vfloat f2), (Vfloat f3) => Vfloat (f f1 f2 f3)
+ | _, _, _ => Vundef
+ end.
+
+Definition triple_op_single f v1 v2 v3 :=
+ match v1, v2, v3 with
+ | (Vsingle f1), (Vsingle f2), (Vsingle f3) => Vsingle (f f1 f2 f3)
+ | _, _, _ => Vundef
+ end.
+
+Definition fmaddf := triple_op_float (fun f1 f2 f3 => Float.fma f2 f3 f1).
+Definition fmaddfs := triple_op_single (fun f1 f2 f3 => Float32.fma f2 f3 f1).
+
+Definition fmsubf := triple_op_float (fun f1 f2 f3 => Float.fma (Float.neg f2) f3 f1).
+Definition fmsubfs := triple_op_single (fun f1 f2 f3 => Float32.fma (Float32.neg f2) f3 f1).
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 5a7d42b4..8098b5d1 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -213,6 +213,8 @@ Global Opaque
Definition two_address_op (op: operation) : bool :=
match op with
+ | Ofmaddf | Ofmaddfs
+ | Ofmsubf | Ofmsubfs
| Omadd | Omaddimm _
| Omaddl | Omaddlimm _
| Omsub | Omsubl
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 4748f38b..d2d4d5f5 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -121,9 +121,12 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Omaddlimm n => op2 (default nv)
| Omsubl => op3 (default nv)
| Onegf | Oabsf => op1 (default nv)
- | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
+ | Oaddf | Osubf | Omulf | Odivf | Ominf | Omaxf => op2 (default nv)
+ | Ofmaddf | Ofmsubf => op3 (default nv)
| Onegfs | Oabsfs => op1 (default nv)
- | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
+ | Oaddfs | Osubfs | Omulfs | Odivfs | Ominfs | Omaxfs => op2 (default nv)
+ | Oinvfs => op1 (default nv)
+ | Ofmaddfs | Ofmsubfs => op3 (default nv)
| Ofloatofsingle | Osingleoffloat => op1 (default nv)
| Ointoffloat | Ointuoffloat => op1 (default nv)
| Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv)
@@ -285,7 +288,53 @@ Remark default_idem: forall nv, default (default nv) = default nv.
Proof.
destruct nv; simpl; trivial.
Qed.
-
+
+Lemma vagree_triple_op_float :
+ forall f a b c x y z nv,
+ (vagree a x (default nv)) ->
+ (vagree b y (default nv)) ->
+ (vagree c z (default nv)) ->
+ (vagree (ExtValues.triple_op_float f a b c)
+ (ExtValues.triple_op_float f x y z) nv).
+Proof.
+ induction nv;
+ intros Hax Hby Hcz.
+ - trivial.
+ - simpl in *. destruct a; simpl; trivial.
+ destruct b; simpl; trivial.
+ destruct c; simpl; trivial.
+ - simpl in *. destruct a; simpl; trivial.
+ destruct b; simpl; trivial.
+ destruct c; simpl; trivial.
+ inv Hax. inv Hby. inv Hcz.
+ simpl.
+ constructor.
+Qed.
+
+Lemma vagree_triple_op_single :
+ forall f a b c x y z nv,
+ (vagree a x (default nv)) ->
+ (vagree b y (default nv)) ->
+ (vagree c z (default nv)) ->
+ (vagree (ExtValues.triple_op_single f a b c)
+ (ExtValues.triple_op_single f x y z) nv).
+Proof.
+ induction nv;
+ intros Hax Hby Hcz.
+ - trivial.
+ - simpl in *. destruct a; simpl; trivial.
+ destruct b; simpl; trivial.
+ destruct c; simpl; trivial.
+ - simpl in *. destruct a; simpl; trivial.
+ destruct b; simpl; trivial.
+ destruct c; simpl; trivial.
+ inv Hax. inv Hby. inv Hcz.
+ simpl.
+ constructor.
+Qed.
+
+Hint Resolve vagree_triple_op_float vagree_triple_op_single : na.
+
Lemma needs_of_operation_sound:
forall op args v nv args',
eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v ->
@@ -344,7 +393,10 @@ Proof.
apply mull_sound; trivial.
rewrite default_idem; trivial.
rewrite default_idem; trivial.
- (* select *)
+- apply vagree_triple_op_float; assumption.
+- apply vagree_triple_op_float; assumption.
+- apply vagree_triple_op_single; assumption.
+- apply vagree_triple_op_single; assumption.
- destruct (eval_condition0 _ _ _) as [b|] eqn:EC.
erewrite needs_of_condition0_sound by eauto.
apply select_sound; auto.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 815d3958..f9a774e8 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -179,12 +179,21 @@ Inductive operation : Type :=
| Osubf (**r [rd = r1 - r2] *)
| Omulf (**r [rd = r1 * r2] *)
| Odivf (**r [rd = r1 / r2] *)
+ | Ominf
+ | Omaxf
+ | Ofmaddf
+ | Ofmsubf
| Onegfs (**r [rd = - r1] *)
| Oabsfs (**r [rd = abs(r1)] *)
| Oaddfs (**r [rd = r1 + r2] *)
| Osubfs (**r [rd = r1 - r2] *)
| Omulfs (**r [rd = r1 * r2] *)
| Odivfs (**r [rd = r1 / r2] *)
+ | Ominfs
+ | Omaxfs
+ | Oinvfs
+ | Ofmaddfs
+ | Ofmsubfs
| Osingleoffloat (**r [rd] is [r1] truncated to single-precision float *)
| Ofloatofsingle (**r [rd] is [r1] extended to double-precision float *)
(*c Conversions between int and float: *)
@@ -426,12 +435,23 @@ Definition eval_operation
| Osubf, v1::v2::nil => Some (Val.subf v1 v2)
| Omulf, v1::v2::nil => Some (Val.mulf v1 v2)
| Odivf, v1::v2::nil => Some (Val.divf v1 v2)
+ | Ominf, v1::v2::nil => Some (ExtValues.minf v1 v2)
+ | Omaxf, v1::v2::nil => Some (ExtValues.maxf v1 v2)
+ | Ofmaddf, v1::v2::v3::nil => Some (ExtValues.fmaddf v1 v2 v3)
+ | Ofmsubf, v1::v2::v3::nil => Some (ExtValues.fmsubf v1 v2 v3)
+
| Onegfs, v1::nil => Some (Val.negfs v1)
| Oabsfs, v1::nil => Some (Val.absfs v1)
| Oaddfs, v1::v2::nil => Some (Val.addfs v1 v2)
| Osubfs, v1::v2::nil => Some (Val.subfs v1 v2)
| Omulfs, v1::v2::nil => Some (Val.mulfs v1 v2)
| Odivfs, v1::v2::nil => Some (Val.divfs v1 v2)
+ | Ominfs, v1::v2::nil => Some (ExtValues.minfs v1 v2)
+ | Omaxfs, v1::v2::nil => Some (ExtValues.maxfs v1 v2)
+ | Oinvfs, v1::nil => Some (ExtValues.invfs v1)
+ | Ofmaddfs, v1::v2::v3::nil => Some (ExtValues.fmaddfs v1 v2 v3)
+ | Ofmsubfs, v1::v2::v3::nil => Some (ExtValues.fmsubfs v1 v2 v3)
+
| Osingleoffloat, v1::nil => Some (Val.singleoffloat v1)
| Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1)
| Ointoffloat, v1::nil => Val.intoffloat v1
@@ -630,16 +650,25 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Onegf => (Tfloat :: nil, Tfloat)
| Oabsf => (Tfloat :: nil, Tfloat)
- | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
- | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
- | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
- | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
+ | Oaddf
+ | Osubf
+ | Omulf
+ | Odivf
+ | Ominf
+ | Omaxf => (Tfloat :: Tfloat :: nil, Tfloat)
+ | Ofmaddf | Ofmsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat)
+
| Onegfs => (Tsingle :: nil, Tsingle)
| Oabsfs => (Tsingle :: nil, Tsingle)
- | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle)
- | Osubfs => (Tsingle :: Tsingle :: nil, Tsingle)
- | Omulfs => (Tsingle :: Tsingle :: nil, Tsingle)
- | Odivfs => (Tsingle :: Tsingle :: nil, Tsingle)
+ | Oaddfs
+ | Osubfs
+ | Omulfs
+ | Odivfs
+ | Ominfs
+ | Omaxfs => (Tsingle :: Tsingle :: nil, Tsingle)
+ | Oinvfs => (Tsingle :: nil, Tsingle)
+ | Ofmaddfs | Ofmsubfs => (Tsingle :: Tsingle :: Tsingle :: nil, Tsingle)
+
| Osingleoffloat => (Tfloat :: nil, Tsingle)
| Ofloatofsingle => (Tsingle :: nil, Tfloat)
| Ointoffloat => (Tfloat :: nil, Tint)
@@ -906,6 +935,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(* mulf, divf *)
- destruct v0; destruct v1...
- destruct v0; destruct v1...
+ (* minf, maxf *)
+ - destruct v0; destruct v1...
+ - destruct v0; destruct v1...
+ (* fmaddf, fmsubf *)
+ - destruct v0; destruct v1; destruct v2...
+ - destruct v0; destruct v1; destruct v2...
(* negfs, absfs *)
- destruct v0...
- destruct v0...
@@ -915,6 +950,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(* mulfs, divfs *)
- destruct v0; destruct v1...
- destruct v0; destruct v1...
+ (* minfs, maxfs *)
+ - destruct v0; destruct v1...
+ - destruct v0; destruct v1...
+ (* invfs *)
+ - destruct v0...
+ (* fmaddfs, fmsubfs *)
+ - destruct v0; destruct v1; destruct v2...
+ - destruct v0; destruct v1; destruct v2...
(* singleoffloat, floatofsingle *)
- destruct v0...
- destruct v0...
@@ -1517,6 +1560,12 @@ Proof.
(* mulf, divf *)
- inv H4; inv H2; simpl; auto.
- inv H4; inv H2; simpl; auto.
+ (* minf, maxf *)
+ - inv H4; inv H2; simpl; auto.
+ - inv H4; inv H2; simpl; auto.
+ (* fmaddf, fmsubf *)
+ - inv H4; inv H3; inv H2; simpl; auto.
+ - inv H4; inv H3; inv H2; simpl; auto.
(* negfs, absfs *)
- inv H4; simpl; auto.
- inv H4; simpl; auto.
@@ -1526,6 +1575,14 @@ Proof.
(* mulfs, divfs *)
- inv H4; inv H2; simpl; auto.
- inv H4; inv H2; simpl; auto.
+ (* minfs, maxfs *)
+ - inv H4; inv H2; simpl; auto.
+ - inv H4; inv H2; simpl; auto.
+ (* invfs *)
+ - inv H4; simpl; auto.
+ (* fmaddfs, fmsubfs *)
+ - inv H4; inv H3; inv H2; simpl; auto.
+ - inv H4; inv H3; inv H2; simpl; auto.
(* singleoffloat, floatofsingle *)
- inv H4; simpl; auto.
- inv H4; simpl; auto.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 40f1d9c7..fa61d588 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -31,6 +31,8 @@ type real_instruction =
(* FPU *)
| Fabsd | Fabsw | Fnegw | Fnegd
| Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
+ | Fmind | Fminw | Fmaxd | Fmaxw | Finvw
+ | Ffmaw | Ffmad | Ffmsw | Ffmsd
| Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz
| Fcompw | Fcompd
@@ -63,6 +65,7 @@ let arith_rr_real = function
| Pfabsd -> Fabsd
| Pfnegw -> Fnegw
| Pfnegd -> Fnegd
+ | Pfinvw -> Finvw
| Pfnarrowdw -> Fnarrowdw
| Pfwidenlwd -> Fwidenlwd
| Pfloatwrnsz -> Floatwz
@@ -121,6 +124,10 @@ let arith_rrr_real = function
| Pfsbfw -> Fsbfw
| Pfmuld -> Fmuld
| Pfmulw -> Fmulw
+ | Pfmind -> Fmind
+ | Pfminw -> Fminw
+ | Pfmaxd -> Fmaxd
+ | Pfmaxw -> Fmaxw
let arith_rri32_real = function
| Pcompiw it -> Compw
@@ -169,6 +176,10 @@ let arith_arr_real = function
| Pinsfl (_, _) -> Insf
let arith_arrr_real = function
+ | Pfmaddfw -> Ffmaw
+ | Pfmaddfl -> Ffmad
+ | Pfmsubfw -> Ffmsw
+ | Pfmsubfl -> Ffmsd
| Pmaddw -> Maddw
| Pmaddl -> Maddd
| Pmsubw -> Msbfw
@@ -610,9 +621,12 @@ let rec_to_usage r =
| Some E27U27L10 -> lsu_acc_y)
| Icall | Call | Cb | Igoto | Goto | Ret | Set -> bcu
| Get -> bcu_tiny_tiny_mau_xnop
- | Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd -> alu_lite
+ | Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd
+ | Fmind | Fmaxd | Fminw | Fmaxw -> alu_lite
| Fnarrowdw -> alu_full
- | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw -> mau
+ | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Finvw
+ | Ffmad | Ffmaw | Ffmsd | Ffmsw -> mau
+
let inst_info_to_dlatency i =
begin
@@ -632,6 +646,7 @@ let real_inst_to_latency = function
| Nandd | Nord | Nxord | Ornd | Andnd
| Addd | Andd | Compd | Ord | Sbfd | Sbfxd | Srad | Srsd | Srld | Slld | Xord | Make
| Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd
+ | Fmind | Fmaxd | Fminw | Fmaxw
-> 1
| Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
| Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
@@ -641,7 +656,8 @@ let real_inst_to_latency = function
| Set -> 4 (* According to the manual should be 3, but I measured 4 *)
| Icall | Call | Cb | Igoto | Goto | Ret -> 42 (* Should not matter since it's the final instruction of the basic block *)
| Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd | Fnarrowdw -> 1
- | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw -> 4
+ | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Finvw
+ | Ffmaw | Ffmad | Ffmsw | Ffmsd -> 4
let rec empty_inter la = function
| [] -> true
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 3df0c682..ec3985c5 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -51,9 +51,10 @@ Require Import Floats.
Require Import Op.
Require Import CminorSel.
Require Import OpHelpers.
-Require Import ExtValues.
+Require Import ExtValues ExtFloats.
Require Import DecBoolOps.
Require Import Chunks.
+Require Import Builtins.
Require Compopts.
Local Open Scope cminorsel_scope.
@@ -668,9 +669,45 @@ Definition divf_base (e1: expr) (e2: expr) :=
(* Eop Odivf (e1 ::: e2 ::: Enil). *)
Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil).
-Definition divfs_base (e1: expr) (e2: expr) :=
+Definition divfs_base1 (e2 : expr) :=
+ Eop Oinvfs (e2 ::: Enil).
+Definition divfs_baseX (e1 : expr) (e2 : expr) :=
(* Eop Odivf (e1 ::: e2 ::: Enil). *)
Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil).
+
+Nondetfunction divfs_base (e1: expr) :=
+ match e1 with
+ | Eop (Osingleconst f) Enil =>
+ (if Float32.eq_dec f ExtFloat32.one
+ then divfs_base1
+ else divfs_baseX e1)
+ | _ => divfs_baseX e1
+ end.
+
+Nondetfunction gen_fma args :=
+ match args with
+ | (Eop Onegf (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubf (e3:::e1:::e2:::Enil))
+ | e1:::e2:::e3:::Enil => Some (Eop Ofmaddf (e3:::e1:::e2:::Enil))
+ | _ => None
+ end.
+
+Nondetfunction gen_fmaf args :=
+ match args with
+ | (Eop Onegfs (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubfs (e3:::e1:::e2:::Enil))
+ | e1:::e2:::e3:::Enil => Some (Eop Ofmaddfs (e3:::e1:::e2:::Enil))
+ | _ => None
+ end.
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+ match b with
+ | BI_fmin => Some (Eop Ominf args)
+ | BI_fmax => Some (Eop Omaxf args)
+ | BI_fminf => Some (Eop Ominfs args)
+ | BI_fmaxf => Some (Eop Omaxfs args)
+ | BI_fabsf => Some (Eop Oabsfs args)
+ | BI_fma => gen_fma args
+ | BI_fmaf => gen_fmaf args
+ end.
End SELECT.
(* Local Variables: *)
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 21a06857..583fb545 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -17,6 +17,7 @@
(** Correctness of instruction selection for operators *)
+Require Import Builtins.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
@@ -29,6 +30,7 @@ Require Import Globalenvs.
Require Import Cminor.
Require Import Op.
Require Import CminorSel.
+Require Import Builtins1.
Require Import SelectOp.
Require Import Events.
Require Import OpHelpers.
@@ -1620,6 +1622,29 @@ Proof.
econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
Qed.
+
+Lemma eval_divfs_base1:
+ forall le a b x y,
+ eval_expr ge sp e m le a x ->
+ eval_expr ge sp e m le b y ->
+ exists v, eval_expr ge sp e m le (divfs_base1 b) v /\ Val.lessdef (ExtValues.invfs y) v.
+Proof.
+ intros; unfold divfs_base1.
+ econstructor; split.
+ repeat (try econstructor; try eassumption).
+ trivial.
+Qed.
+
+Lemma eval_divfs_baseX:
+ forall le a b x y,
+ eval_expr ge sp e m le a x ->
+ eval_expr ge sp e m le b y ->
+ exists v, eval_expr ge sp e m le (divfs_baseX a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+ intros; unfold divfs_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
Theorem eval_divfs_base:
forall le a b x y,
eval_expr ge sp e m le a x ->
@@ -1627,6 +1652,82 @@ Theorem eval_divfs_base:
exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
Proof.
intros; unfold divfs_base.
- econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+ destruct (divfs_base_match _).
+ - destruct (Float32.eq_dec _ _).
+ + exists (Val.divfs x y).
+ split; trivial. repeat (try econstructor; try eassumption).
+ simpl. InvEval. reflexivity.
+ + apply eval_divfs_baseX; assumption.
+ - apply eval_divfs_baseX; assumption.
Qed.
+
+(** Platform-specific known builtins *)
+
+Lemma eval_fma:
+ forall al a vl v le,
+ gen_fma al = Some a ->
+ eval_exprlist ge sp e m le al vl ->
+ platform_builtin_sem BI_fma vl = Some v ->
+ exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+ unfold gen_fma.
+ intros until le.
+ intro Heval.
+ destruct (gen_fma_match _) in *; try discriminate.
+ all: inversion Heval; subst a; clear Heval; intro; InvEval.
+ - subst v1.
+ TrivialExists.
+ destruct v0; simpl; trivial;
+ destruct v2; simpl; trivial;
+ destruct v3; simpl; trivial.
+ - intro Heval.
+ simpl in Heval.
+ inv Heval.
+ TrivialExists.
+ destruct v0; simpl; trivial;
+ destruct v1; simpl; trivial;
+ destruct v2; simpl; trivial.
+Qed.
+
+Lemma eval_fmaf:
+ forall al a vl v le,
+ gen_fmaf al = Some a ->
+ eval_exprlist ge sp e m le al vl ->
+ platform_builtin_sem BI_fmaf vl = Some v ->
+ exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+ unfold gen_fmaf.
+ intros until le.
+ intro Heval.
+ destruct (gen_fmaf_match _) in *; try discriminate.
+ all: inversion Heval; subst a; clear Heval; intro; InvEval.
+ - subst v1.
+ TrivialExists.
+ destruct v0; simpl; trivial;
+ destruct v2; simpl; trivial;
+ destruct v3; simpl; trivial.
+ - intro Heval.
+ simpl in Heval.
+ inv Heval.
+ TrivialExists.
+ destruct v0; simpl; trivial;
+ destruct v1; simpl; trivial;
+ destruct v2; simpl; trivial.
+Qed.
+
+Theorem eval_platform_builtin:
+ forall bf al a vl v le,
+ platform_builtin bf al = Some a ->
+ eval_exprlist ge sp e m le al vl ->
+ platform_builtin_sem bf vl = Some v ->
+ exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+ destruct bf; intros until le; intro Heval.
+ all: try (inversion Heval; subst a; clear Heval;
+ exists v; split; trivial;
+ repeat (try econstructor; try eassumption)).
+ - apply eval_fma; assumption.
+ - apply eval_fmaf; assumption.
+Qed.
+
End CMCONSTR.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index c9822e13..5618875f 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -140,6 +140,8 @@ module Target (*: TARGET*) =
| RA -> output_string oc "$ra"
| _ -> assert false
+ let preg_asm oc ty = preg oc
+
let preg_annot = let open Asmvliw in function
| IR r -> int_reg_name r
| RA -> "$ra"
@@ -324,7 +326,7 @@ module Target (*: TARGET*) =
(P.to_int kind) (extern_atom txt) args
| EF_inline_asm(txt, sg, clob) ->
fprintf oc "%s begin inline assembly\n\t" comment;
- print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
+ print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
fprintf oc "%s end inline assembly\n" comment
| _ ->
assert false
@@ -572,6 +574,10 @@ module Target (*: TARGET*) =
fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Pmsubw (rd, rs1, rs2) ->
fprintf oc " msbfw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfmaddfw (rd, rs1, rs2) ->
+ fprintf oc " ffmaw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfmsubfw (rd, rs1, rs2) ->
+ fprintf oc " ffmsw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Paddl (rd, rs1, rs2) ->
fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -613,6 +619,10 @@ module Target (*: TARGET*) =
fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Pmsubl (rd, rs1, rs2) ->
fprintf oc " msbfd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfmaddfl (rd, rs1, rs2) ->
+ fprintf oc " ffmad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfmsubfl (rd, rs1, rs2) ->
+ fprintf oc " ffmsd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Pfaddd (rd, rs1, rs2) ->
fprintf oc " faddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -626,6 +636,16 @@ module Target (*: TARGET*) =
fprintf oc " fmuld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Pfmulw (rd, rs1, rs2) ->
fprintf oc " fmulw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfmind (rd, rs1, rs2) ->
+ fprintf oc " fmind %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfminw (rd, rs1, rs2) ->
+ fprintf oc " fminw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfmaxd (rd, rs1, rs2) ->
+ fprintf oc " fmaxd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfmaxw (rd, rs1, rs2) ->
+ fprintf oc " fmaxw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+ | Pfinvw (rd, rs1) ->
+ fprintf oc " finvw %a = %a\n" ireg rd ireg rs1
(* Arith RRI32 instructions *)
| Pcompiw (it, rd, rs, imm) ->
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 439138da..2c9bdf3e 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -12,7 +12,37 @@
Require Import Coqlib Compopts.
Require Import AST Integers Floats Values Memory Globalenvs.
-Require Import Op ExtValues RTL ValueDomain.
+Require Import Op ExtValues ExtFloats RTL ValueDomain.
+
+Definition minf := binop_float ExtFloat.min.
+Definition maxf := binop_float ExtFloat.max.
+Definition minfs := binop_single ExtFloat32.min.
+Definition maxfs := binop_single ExtFloat32.max.
+
+Definition ntop3 (x y z: aval) : aval := Ifptr (plub (provenance x) (plub (provenance y) (provenance z))).
+
+Definition triple_op_float (sem: float -> float -> float -> float) (x y z: aval) :=
+ match x, y, z with
+ | F a, F b, F c => F (sem a b c)
+ | _, _, _ => ntop3 x y z
+ end.
+
+Definition triple_op_single (sem: float32 -> float32 -> float32 -> float32) (x y z: aval) :=
+ match x, y, z with
+ | FS a, FS b, FS c => FS (sem a b c)
+ | _, _, _ => ntop3 x y z
+ end.
+
+Definition fmaddf := triple_op_float (fun x y z => Float.fma y z x).
+Definition fmsubf := triple_op_float (fun x y z => Float.fma (Float.neg y) z x).
+Definition fmaddfs := triple_op_single (fun x y z => Float32.fma y z x).
+Definition fmsubfs := triple_op_single (fun x y z => Float32.fma (Float32.neg y) z x).
+
+Definition invfs (y : aval) :=
+ match y with
+ | FS f => FS (ExtFloat32.inv f)
+ | _ => ntop1 y
+ end.
(** Value analysis for RISC V operators *)
@@ -235,12 +265,21 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Osubf, v1::v2::nil => subf v1 v2
| Omulf, v1::v2::nil => mulf v1 v2
| Odivf, v1::v2::nil => divf v1 v2
+ | Ominf, v1::v2::nil => minf v1 v2
+ | Omaxf, v1::v2::nil => maxf v1 v2
+ | Ofmaddf, v1::v2::v3::nil => fmaddf v1 v2 v3
+ | Ofmsubf, v1::v2::v3::nil => fmsubf v1 v2 v3
| Onegfs, v1::nil => negfs v1
| Oabsfs, v1::nil => absfs v1
| Oaddfs, v1::v2::nil => addfs v1 v2
| Osubfs, v1::v2::nil => subfs v1 v2
| Omulfs, v1::v2::nil => mulfs v1 v2
| Odivfs, v1::v2::nil => divfs v1 v2
+ | Ominfs, v1::v2::nil => minfs v1 v2
+ | Omaxfs, v1::v2::nil => maxfs v1 v2
+ | Oinvfs, v1::nil => invfs v1
+ | Ofmaddfs, v1::v2::v3::nil => fmaddfs v1 v2 v3
+ | Ofmsubfs, v1::v2::v3::nil => fmsubfs v1 v2 v3
| Osingleoffloat, v1::nil => singleoffloat v1
| Ofloatofsingle, v1::nil => floatofsingle v1
| Ointoffloat, v1::nil => intoffloat v1
@@ -278,6 +317,99 @@ Hypothesis GENV: genv_match bc ge.
Variable sp: block.
Hypothesis STACK: bc sp = BCstack.
+Lemma minf_sound:
+ forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y).
+Proof.
+ apply (binop_float_sound bc ExtFloat.min); assumption.
+Qed.
+
+Lemma maxf_sound:
+ forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.maxf v w) (maxf x y).
+Proof.
+ apply (binop_float_sound bc ExtFloat.max); assumption.
+Qed.
+
+Lemma minfs_sound:
+ forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minfs v w) (minfs x y).
+Proof.
+ apply (binop_single_sound bc ExtFloat32.min); assumption.
+Qed.
+
+Lemma maxfs_sound:
+ forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.maxfs v w) (maxfs x y).
+Proof.
+ apply (binop_single_sound bc ExtFloat32.max); assumption.
+Qed.
+
+Lemma invfs_sound:
+ forall v x, vmatch bc v x -> vmatch bc (ExtValues.invfs v) (invfs x).
+Proof.
+ intros v x;
+ intro MATCH;
+ inversion MATCH;
+ simpl;
+ constructor.
+Qed.
+
+Lemma triple_op_float_sound:
+ forall f a x b y c z,
+ vmatch bc a x -> vmatch bc b y -> vmatch bc c z ->
+ vmatch bc (ExtValues.triple_op_float f a b c)
+ (triple_op_float f x y z).
+Proof.
+ intros until z.
+ intros Hax Hby Hcz.
+ inv Hax; simpl; try constructor;
+ inv Hby; simpl; try constructor;
+ inv Hcz; simpl; try constructor.
+Qed.
+
+Lemma triple_op_single_sound:
+ forall f a x b y c z,
+ vmatch bc a x -> vmatch bc b y -> vmatch bc c z ->
+ vmatch bc (ExtValues.triple_op_single f a b c)
+ (triple_op_single f x y z).
+Proof.
+ intros until z.
+ intros Hax Hby Hcz.
+ inv Hax; simpl; try constructor;
+ inv Hby; simpl; try constructor;
+ inv Hcz; simpl; try constructor.
+Qed.
+
+Lemma fmaddf_sound :
+ forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z ->
+ vmatch bc (ExtValues.fmaddf a b c) (fmaddf x y z).
+Proof.
+ intros. unfold ExtValues.fmaddf, fmaddf.
+ apply triple_op_float_sound; assumption.
+Qed.
+
+Lemma fmaddfs_sound :
+ forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z ->
+ vmatch bc (ExtValues.fmaddfs a b c) (fmaddfs x y z).
+Proof.
+ intros. unfold ExtValues.fmaddfs, fmaddfs.
+ apply triple_op_single_sound; assumption.
+Qed.
+
+Lemma fmsubf_sound :
+ forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z ->
+ vmatch bc (ExtValues.fmsubf a b c) (fmsubf x y z).
+Proof.
+ intros. unfold ExtValues.fmsubf, fmsubf.
+ apply triple_op_float_sound; assumption.
+Qed.
+
+Lemma fmsubfs_sound :
+ forall a x b y c z, vmatch bc a x -> vmatch bc b y -> vmatch bc c z ->
+ vmatch bc (ExtValues.fmsubfs a b c) (fmsubfs x y z).
+Proof.
+ intros. unfold ExtValues.fmsubfs, fmsubfs.
+ apply triple_op_single_sound; assumption.
+Qed.
+Hint Resolve minf_sound maxf_sound minfs_sound maxfs_sound invfs_sound fmaddf_sound fmaddfs_sound fmsubf_sound fmsubfs_sound : va.
+
Theorem eval_static_condition_sound:
forall cond vargs m aargs,
list_forall2 (vmatch bc) vargs aargs ->
generated by cgit (git 2.34.1) at 2024-07-04 14:16:37 +0000