From 16715e5efd6ce899eb3d544fd71751f367eaa370 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Feb 2022 21:36:57 +0100
Subject: modulos

---
 kvx/Builtins1.v     | 18 +++++++++++++++++-
 kvx/CBuiltins.ml    |  4 ++++
 kvx/SelectOp.vp     |  8 ++++++++
 kvx/SelectOpproof.v | 44 ++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 73 insertions(+), 1 deletion(-)

(limited to 'kvx')

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.
diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml
index 49534867..5ca5ddba 100644
--- a/kvx/CBuiltins.ml
+++ b/kvx/CBuiltins.ml
@@ -141,6 +141,10 @@ let builtins = {
     (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
     "__builtin_fp_udiv64",
     (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false);
+    "__builtin_fp_umod32",
+    (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
+    "__builtin_fp_umod64",
+    (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false);
 ]
 }
 
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 72a6e4b3..089afe1d 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -762,6 +762,14 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
                      | a:::b:::Enil => Some (FPDivision64.fp_divu64 a b)
                      | _ => None
                      end)
+  | BI_fp_umod32 => (match args with
+                     | a:::b:::Enil => Some (FPDivision32.fp_modu32 a b)
+                     | _ => None
+                     end)
+  | BI_fp_umod64 => (match args with
+                     | a:::b:::Enil => Some (FPDivision64.fp_modu64 a b)
+                     | _ => None
+                     end)
   end.
 End SELECT.
 
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index e6cce0fa..cffa2583 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1951,6 +1951,50 @@ 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.modu i i0)). split.
+    {
+      apply FPDivision32.fp_modu32_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.modu i i0)). split.
+    {
+      apply FPDivision64.fp_modu64_correct; auto.
+      pose proof (Int64.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
 Qed.
 
 End CMCONSTR.
-- 
cgit