From eaae75e487a82021cc615856b31f86bd05853b1e Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 16 Feb 2022 09:32:24 +0100
Subject: builtins pour signed div/mod

---
 kvx/Builtins1.v | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'kvx/Builtins1.v')

diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v
index e3e4f95d..5536e58c 100644
--- a/kvx/Builtins1.v
+++ b/kvx/Builtins1.v
@@ -32,6 +32,10 @@ Inductive platform_builtin : Type :=
 | 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.
 
@@ -50,6 +54,10 @@ 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_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.
@@ -74,6 +82,14 @@ 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_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 =>
@@ -106,6 +122,22 @@ 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_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.
-- 
cgit