Added semantics for fmin/fmax for RISC-V

The semantics of the RISC-V variant of fmin and fmax are slightly
different to the other architectures. In case of NaN instead of
returning always the second one for RISC-V we return the non-NaN
parameter or canonical NaN in the case that both are NaN.
Bug 30035

Author: bschommer

riscV/Builtins1.v

@@ -19,15 +19,47 @@ Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+  | BI_fmin
+  | BI_fmax.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+    ("__builtin_fmin", BI_fmin)
+  :: ("__builtin_fmax", BI_fmax)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  match b with
+  | BI_fmin | BI_fmax =>
+      mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default
+  end.
+
+(* Canonical NaN as defined in the RISC-V ISA, all expontent bits one, sign bit
+   zero and quiet bit one. *)
+Definition canonical_nan := Float.of_bits (Int64.repr 9221120237041090560).
+
+(* NaN handling as described for fmin/fmax by the RISC-V Isa. If one of the
+   parameters is NaN, the other one is returned. Otherwise the canonical NaN
+   value is returned. *)
+Definition nan_handling (f1 f2: float) : float :=
+  if negb (Binary.is_nan _ _ f1) then f1
+  else if negb (Binary.is_nan _ _ f2) then f2
+  else canonical_nan.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  match b with
+  | BI_fmin =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Lt => f1
+                      | Some Gt | None => nan_handling f1 f2
+                      end)
+  | BI_fmax =>
+      mkbuiltin_n2t Tfloat Tfloat Tfloat
+        (fun f1 f2 => match Float.compare f1 f2 with
+                      | Some Eq | Some Gt => f1
+                      | Some Lt | None => nan_handling f1 f2
+                      end)
+  end.