diff options
Diffstat (limited to 'kvx/Builtins1.v')
| -rw-r--r-- | kvx/Builtins1.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index de0d9885..163dcbd8 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -27,7 +27,8 @@ Inductive platform_builtin : Type := | BI_fma | BI_fmaf | BI_lround_ne -| BI_luround_ne. +| BI_luround_ne +| BI_fp_udiv32. Local Open Scope string_scope. @@ -40,6 +41,7 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmaf", BI_fmaf) :: ("__builtin_lround_ne", BI_lround_ne) :: ("__builtin_luround_ne", BI_luround_ne) + :: ("__builtin_fp_udiv32", BI_fp_udiv32) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -54,6 +56,8 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := 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 end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -66,4 +70,8 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | 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)) end. |