diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 18:51:52 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 18:51:52 +0100 |
| commit | 1ef9e303d7bd896b94afcc875136d8f3e94243cb (patch) | |
| tree | af2da3d2fdbc0be85d207bf20111162bcf0a4f56 /kvx/Builtins1.v | |
| parent | 882f1a1875089298937abf4ef854b221cab4eb8e (diff) | |
| parent | 2867dee21f6fb696db554679d8535306c7a9d4ea (diff) | |
| download | compcert-kvx-1ef9e303d7bd896b94afcc875136d8f3e94243cb.tar.gz compcert-kvx-1ef9e303d7bd896b94afcc875136d8f3e94243cb.zip | |
Merge remote-tracking branch 'origin/kvx-bits' into kvx_fp_division
Diffstat (limited to 'kvx/Builtins1.v')
| -rw-r--r-- | kvx/Builtins1.v | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index a0473d07..e3e4f95d 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -16,7 +16,7 @@ (** Platform-specific built-in functions *) Require Import String Coqlib. -Require Import AST Integers Floats Values ExtFloats. +Require Import AST Integers Floats Values ExtFloats ExtValues. Require Import Builtins0. Inductive platform_builtin : Type := @@ -31,7 +31,9 @@ Inductive platform_builtin : Type := | BI_fp_udiv32 | BI_fp_udiv64 | BI_fp_umod32 -| BI_fp_umod64. +| BI_fp_umod64 +| BI_abs +| BI_absl. Local Open Scope string_scope. @@ -48,6 +50,8 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fp_udiv64", BI_fp_udiv64) :: ("__builtin_fp_umod32", BI_fp_umod32) :: ("__builtin_fp_umod64", BI_fp_umod64) + :: ("__builtin_abs", BI_abs) + :: ("__builtin_absl", BI_absl) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -70,6 +74,10 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tint :: Tint :: nil) Tint cc_default | BI_fp_umod64 => mksignature (Tlong :: Tlong :: nil) Tlong cc_default + | BI_abs => + mksignature (Tint :: nil) Tint cc_default + | BI_absl => + mksignature (Tlong :: nil) Tlong cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -98,4 +106,6 @@ 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.modu n1 n2)) + | BI_abs => mkbuiltin_n1t Tint Tint ExtValues.int_abs + | BI_absl => mkbuiltin_n1t Tlong Tlong ExtValues.long_abs end. |