From 7afc85c95aaec5cc0935733cac487e13f114cc46 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 13:07:56 +0100
Subject: cmov on integers

---
 riscV/SelectOpproof.v | 89 +++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 80 insertions(+), 9 deletions(-)

(limited to 'riscV/SelectOpproof.v')

diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 9dfe9b6e..7f7474b6 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -24,6 +24,7 @@ Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 Require Import OpHelpers.
 Require Import OpHelpersproof.
+Require Import Lia.
 
 Local Open Scope cminorsel_scope.
 
@@ -875,6 +876,58 @@ Proof.
   red; intros. unfold floatofsingle. TrivialExists.
 Qed.
 
+Lemma mod_small_negative:
+  forall a modulus,
+    modulus > 0 -> -modulus < a < 0 -> a mod modulus = a + modulus.
+Proof.
+  intros.
+  replace (a mod modulus) with ((a + modulus) mod modulus).
+  apply Z.mod_small.
+  lia.
+  rewrite <- Zplus_mod_idemp_r.
+  rewrite Z.mod_same by lia.
+  rewrite Z.add_0_r.
+  reflexivity.
+Qed.
+
+Remark normalize_low_long: forall
+  (PTR64 : Archi.ptr64 = true) v1,
+    Val.loword (Val.normalize (Val.longofint v1) Tlong) = Val.normalize v1 Tint.
+Proof.
+  intros.
+  destruct v1; cbn; try rewrite PTR64; trivial.
+  f_equal.
+  unfold Int64.loword.
+  unfold Int.signed.
+  destruct zlt.
+  { rewrite Int64.int_unsigned_repr.
+    apply Int.repr_unsigned.
+  }
+  pose proof (Int.unsigned_range i).
+  rewrite Int64.unsigned_repr_eq.
+  replace ((Int.unsigned i - Int.modulus) mod Int64.modulus)
+    with (Int64.modulus + Int.unsigned i - Int.modulus).
+  {
+    rewrite <- (Int.repr_unsigned i) at 2.
+    apply Int.eqm_samerepr.
+    unfold Int.eqm, eqmod.
+    change Int.modulus with 4294967296 in *.
+    change Int64.modulus with 18446744073709551616 in *.
+    exists 4294967295.
+    lia.
+  }
+  { rewrite mod_small_negative.
+    lia.
+    constructor.
+    constructor.
+    change Int.modulus with 4294967296 in *.
+    change Int.half_modulus with 2147483648 in *.
+    change Int64.modulus with 18446744073709551616 in *.
+    lia.
+    lia.
+  }
+Qed.
+
 Theorem eval_select:
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
@@ -887,16 +940,34 @@ Theorem eval_select:
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
   unfold select; intros.
+  destruct Archi.ptr64 eqn:PTR64.
+  2: discriminate.
   destruct ty; cbn in *; try discriminate.
-  inv H.
-  TrivialExists.
-  - cbn. constructor.
-    { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
-    constructor. eassumption. constructor. eassumption. constructor.
-  - cbn. f_equal. rewrite ExtValues.normalize_select01.
-    destruct b.
-    + rewrite ExtValues.select01_long_true. reflexivity.
-    + rewrite ExtValues.select01_long_false. reflexivity.
+  - inv H. TrivialExists.
+    + cbn. constructor.
+      { econstructor.
+        { constructor.
+          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
+          constructor. econstructor. constructor. eassumption.
+          constructor. cbn. reflexivity.
+          constructor. econstructor. constructor. eassumption. constructor.
+          cbn. reflexivity. constructor.
+        }
+        constructor.
+      }
+      constructor.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      destruct b.
+      * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
+      * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
+  - inv H. TrivialExists.
+    + cbn. constructor.
+      { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
+      constructor. eassumption. constructor. eassumption. constructor.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      destruct b.
+      * rewrite ExtValues.select01_long_true. reflexivity.
+      * rewrite ExtValues.select01_long_false. reflexivity.
 Qed.
 
 Theorem eval_addressing:
-- 
cgit