builtins pour signed div/mod

4 files changed, 144 insertions, 0 deletions

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.
diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml
index d712eecd..c0b69adf 100644
--- a/kvx/CBuiltins.ml
+++ b/kvx/CBuiltins.ml
@@ -145,6 +145,14 @@ let builtins = {
     (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
     "__builtin_fp_umod64",
     (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false);
+    "__builtin_fp_sdiv32",
+    (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false);
+    "__builtin_fp_sdiv64",
+    (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
+    "__builtin_fp_smod32",
+    (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false);
+    "__builtin_fp_smod64",
+    (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
     "__builtin_abs",
       (TInt(IInt, []), [TInt(IInt, [])], false);
     "__builtin_absl",
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 63c7d73b..5225a71c 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -788,6 +788,22 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
                      | a:::b:::Enil => Some (FPDivision64.fp_modu64 a b)
                      | _ => None
                      end)
+  | BI_fp_sdiv32 => (match args with
+                     | a:::b:::Enil => Some (FPDivision32.fp_divs32 a b)
+                     | _ => None
+                     end)
+  | BI_fp_sdiv64 => (match args with
+                     | a:::b:::Enil => Some (FPDivision64.fp_divs64 a b)
+                     | _ => None
+                     end)
+  | BI_fp_smod32 => (match args with
+                     | a:::b:::Enil => Some (FPDivision32.fp_mods32 a b)
+                     | _ => None
+                     end)
+  | BI_fp_smod64 => (match args with
+                     | a:::b:::Enil => Some (FPDivision64.fp_mods64 a b)
+                     | _ => None
+                     end)
   | BI_abs => gen_abs args
   | BI_absl => gen_absl args
   end.
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index a45d367f..19393091 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -2046,6 +2046,94 @@ Proof.
     }
     inv EVAL.
     constructor.
+  - cbn in *.
+    intro EVAL.
+    inv EVAL. discriminate.
+    inv H0. discriminate.
+    inv H2. 2: discriminate.
+    inv Heval.
+    intro EVAL.
+    destruct v1; try discriminate.
+    destruct v0; try discriminate.
+    unfold Int.eq in EVAL.
+    change (Int.unsigned Int.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vint (Int.divs i i0)). split.
+    {
+      apply FPDivision32.fp_divs32_correct; auto.
+      pose proof (Int.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
+  - cbn in *.
+    intro EVAL.
+    inv EVAL. discriminate.
+    inv H0. discriminate.
+    inv H2. 2: discriminate.
+    inv Heval.
+    intro EVAL.
+    destruct v1; try discriminate.
+    destruct v0; try discriminate.
+    unfold Int64.eq in EVAL.
+    change (Int64.unsigned Int64.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vlong (Int64.divs i i0)). split.
+    {
+      apply FPDivision64.fp_divs64_correct; auto.
+      pose proof (Int64.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
+  - cbn in *.
+    intro EVAL.
+    inv EVAL. discriminate.
+    inv H0. discriminate.
+    inv H2. 2: discriminate.
+    inv Heval.
+    intro EVAL.
+    destruct v1; try discriminate.
+    destruct v0; try discriminate.
+    unfold Int.eq in EVAL.
+    change (Int.unsigned Int.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vint (Int.mods i i0)). split.
+    {
+      apply FPDivision32.fp_mods32_correct; auto.
+      pose proof (Int.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
+  - cbn in *.
+    intro EVAL.
+    inv EVAL. discriminate.
+    inv H0. discriminate.
+    inv H2. 2: discriminate.
+    inv Heval.
+    intro EVAL.
+    destruct v1; try discriminate.
+    destruct v0; try discriminate.
+    unfold Int64.eq in EVAL.
+    change (Int64.unsigned Int64.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vlong (Int64.mods i i0)). split.
+    {
+      apply FPDivision64.fp_mods64_correct; auto.
+      pose proof (Int64.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
   - apply eval_abs; assumption.
   - apply eval_absl; assumption.
 Qed.