diff options
Diffstat (limited to 'kvx/Builtins1.v')
| -rw-r--r-- | kvx/Builtins1.v | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index b5fc7459..5536e58c 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -26,6 +26,16 @@ Inductive platform_builtin : Type := | BI_fmaxf | BI_fma | BI_fmaf +| BI_lround_ne +| BI_luround_ne +| BI_fp_udiv32 +| BI_fp_udiv64 +| BI_fp_umod32 +| BI_fp_umod64 +| BI_fp_sdiv32 +| BI_fp_sdiv64 +| BI_fp_smod32 +| BI_fp_smod64 | BI_abs | BI_absl. @@ -38,6 +48,16 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmaxf", BI_fmaxf) :: ("__builtin_fma", BI_fma) :: ("__builtin_fmaf", BI_fmaf) + :: ("__builtin_lround_ne", BI_lround_ne) + :: ("__builtin_luround_ne", BI_luround_ne) + :: ("__builtin_fp_udiv32", BI_fp_udiv32) + :: ("__builtin_fp_udiv64", BI_fp_udiv64) + :: ("__builtin_fp_umod32", BI_fp_umod32) + :: ("__builtin_fp_umod64", BI_fp_umod64) + :: ("__builtin_fp_sdiv32", BI_fp_sdiv32) + :: ("__builtin_fp_sdiv64", BI_fp_sdiv64) + :: ("__builtin_fp_smod32", BI_fp_smod32) + :: ("__builtin_fp_smod64", BI_fp_smod64) :: ("__builtin_abs", BI_abs) :: ("__builtin_absl", BI_absl) :: nil. @@ -52,6 +72,24 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle cc_default + | BI_lround_ne | BI_luround_ne => + mksignature (Tfloat :: nil) Tlong cc_default + | BI_fp_udiv32 => + mksignature (Tint :: Tint :: nil) Tint cc_default + | BI_fp_udiv64 => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default + | BI_fp_umod32 => + mksignature (Tint :: Tint :: nil) Tint cc_default + | BI_fp_umod64 => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default + | BI_fp_sdiv32 => + mksignature (Tint :: Tint :: nil) Tint cc_default + | BI_fp_sdiv64 => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default + | BI_fp_smod32 => + mksignature (Tint :: Tint :: nil) Tint cc_default + | BI_fp_smod64 => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_abs => mksignature (Tint :: nil) Tint cc_default | BI_absl => @@ -66,6 +104,40 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma + | BI_lround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_long_ne + | BI_luround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_longu_ne + | BI_fp_udiv32 => mkbuiltin_n2p Tint Tint Tint + (fun n1 n2 => if Int.eq n2 Int.zero + then None + else Some (Int.divu n1 n2)) + | BI_fp_udiv64 => mkbuiltin_n2p Tlong Tlong Tlong + (fun n1 n2 => if Int64.eq n2 Int64.zero + then None + else Some (Int64.divu n1 n2)) + | BI_fp_umod32 => mkbuiltin_n2p Tint Tint Tint + (fun n1 n2 => if Int.eq n2 Int.zero + then None + else Some (Int.modu n1 n2)) + | BI_fp_umod64 => mkbuiltin_n2p Tlong Tlong Tlong + (fun n1 n2 => if Int64.eq n2 Int64.zero + then None + else Some (Int64.modu n1 n2)) + | BI_fp_sdiv32 => mkbuiltin_n2p Tint Tint Tint + (fun n1 n2 => if Int.eq n2 Int.zero + then None + else Some (Int.divs n1 n2)) + | BI_fp_sdiv64 => mkbuiltin_n2p Tlong Tlong Tlong + (fun n1 n2 => if Int64.eq n2 Int64.zero + then None + else Some (Int64.divs n1 n2)) + | BI_fp_smod32 => mkbuiltin_n2p Tint Tint Tint + (fun n1 n2 => if Int.eq n2 Int.zero + then None + else Some (Int.mods n1 n2)) + | BI_fp_smod64 => mkbuiltin_n2p Tlong Tlong Tlong + (fun n1 n2 => if Int64.eq n2 Int64.zero + then None + else Some (Int64.mods n1 n2)) | BI_abs => mkbuiltin_n1t Tint Tint ExtValues.int_abs | BI_absl => mkbuiltin_n1t Tlong Tlong ExtValues.long_abs end. |