diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 21:36:57 +0100 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 21:36:57 +0100 |
commit | 16715e5efd6ce899eb3d544fd71751f367eaa370 (patch) | |
tree | fb5cc283dec59bf362a4515e0212165832e5b0a9 /kvx/Builtins1.v | |
parent | bc33b3536cc9985a6dddacadfaa9c2f5a111f4ac (diff) | |
download | compcert-kvx-16715e5efd6ce899eb3d544fd71751f367eaa370.tar.gz compcert-kvx-16715e5efd6ce899eb3d544fd71751f367eaa370.zip |
modulos
Diffstat (limited to 'kvx/Builtins1.v')
-rw-r--r-- | kvx/Builtins1.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index 9a04815b..a0473d07 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -29,7 +29,9 @@ Inductive platform_builtin : Type := | BI_lround_ne | BI_luround_ne | BI_fp_udiv32 -| BI_fp_udiv64. +| BI_fp_udiv64 +| BI_fp_umod32 +| BI_fp_umod64. Local Open Scope string_scope. @@ -44,6 +46,8 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__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) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -62,6 +66,10 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := 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 end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -82,4 +90,12 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl (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)) end. |