fmin/fmax/fminf/fmaxf non bien testés

12 files changed, 102 insertions, 11 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 620aa91e..35eebb11 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -227,6 +227,10 @@ 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 *)

 

   (** Arith RRI32 *)

   | Pcompiw (it: itest) (rd rs: ireg) (imm: int)    (**r comparison imm word *)

@@ -395,6 +399,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

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 9855afa2..cb219f00 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1423,6 +1423,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 :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index e5b9b35a..1f3f7539 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -775,6 +775,18 @@ 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)
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index c5b7db45..a733b54c 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -470,6 +470,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 :=
@@ -1072,6 +1076,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
 
diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v
index f6e643d2..73d1bcf4 100644
--- a/mppa_k1c/Builtins1.v
+++ b/mppa_k1c/Builtins1.v
@@ -16,18 +16,36 @@
 (** Platform-specific built-in functions *)
 
 Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+Require Import AST Integers Floats Values ExtFloats.
 Require Import Builtins0.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+| BI_fmin
+| BI_fmax
+| BI_fminf
+| BI_fmaxf.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+     ("__builtin_fmin", BI_fmin)
+  :: ("__builtin_fmax", BI_fmax)
+  :: ("__builtin_fminf", BI_fminf)
+  :: ("__builtin_fmaxf", BI_fmaxf)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  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
+  end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  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
+  end.
diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml
index 09a9ba97..43f3d98c 100644
--- a/mppa_k1c/CBuiltins.ml
+++ b/mppa_k1c/CBuiltins.ml
@@ -114,14 +114,20 @@ 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_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);
+]
 }
 
 let va_list_type = TPtr(TVoid [], [])  (* to check! *)
diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v
index efea278b..090844f6 100644
--- a/mppa_k1c/ExtFloats.v
+++ b/mppa_k1c/ExtFloats.v
@@ -1,7 +1,8 @@
 Require Import Floats.
 
 Module ExtFloat.
-(** TODO check with the actual K1c *)
+(** 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
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 895f9f40..21cabfe9 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -31,6 +31,7 @@ type real_instruction =
   (* FPU *)
   | Fabsd | Fabsw | Fnegw | Fnegd
   | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
+  | Fmind | Fminw | Fmaxd | Fmaxw
   | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz
   | Fcompw | Fcompd
 
@@ -119,6 +120,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
@@ -578,10 +583,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
 
+
 let real_inst_to_latency = function
   | Nop -> 0 (* Only goes through ID *)
   | Addw | Andw | Compw | Orw | Sbfw | Sbfxw | Sraw | Srsw | Srlw | Sllw | Xorw
@@ -590,6 +597,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 *)
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 688820b3..72597a2b 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -675,7 +675,13 @@ Definition divfs_base (e1: expr) (e2: expr) :=
 End SELECT.
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
-  None.
+  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)
+  end.
+
 (* Local Variables: *)
 (* mode: coq *)
 (* End: *)
\ No newline at end of file
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index e009ed98..65685201 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -1641,7 +1641,9 @@ Theorem eval_platform_builtin:
   platform_builtin_sem bf vl = Some v ->
   exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
 Proof.
-  intros. discriminate.
+  destruct bf; intros until le; intro Heval; inversion Heval; subst a; clear Heval.
+  all: exists v; split; trivial;
+  try repeat (try econstructor; try eassumption).
 Qed.
 
 End CMCONSTR.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index dafad7fb..3ff016c2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -628,6 +628,14 @@ 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
 
       (* Arith RRI32 instructions *)
       | Pcompiw (it, rd, rs, imm) ->
diff --git a/runtime/include/math.h b/runtime/include/math.h
index 805cc8e7..07feb14d 100644
--- a/runtime/include/math.h
+++ b/runtime/include/math.h
@@ -3,5 +3,14 @@
 
 #define isfinite(__y) (fpclassify((__y)) >= FP_ZERO)
 
+#ifndef COMPCERT_NO_FP_MACROS
+#define fmin(x, y) __builtin_fmin((x),(y))
+#define fmax(x, y) __builtin_fmax((x),(y))
+#define fminf(x, y) __builtin_fminf((x),(y))
+#define fmaxf(x, y) __builtin_fmaxf((x),(y))
+#define fabs(x) __builtin_fabs((x))
+#define fabsf(x) __builtin_fabsf((x))
+#endif
+
 #include_next <math.h>
 #endif