cmov on integers

3 files changed, 110 insertions, 11 deletions

diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 0596ebf6..0e82f8ba 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -421,11 +421,17 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
    : option expr
-   := match ty with
+   := if Archi.ptr64 then
+      match ty with
       | Tlong => Some (Eop Oselectl
                        ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil))
+      | Tint => Some (Eop Olowlong ((Eop Oselectl
+                       ((Eop (Ocmp cond) args) :::
+		         (Eop Ocast32signed (e1 ::: Enil)) :::
+			 (Eop Ocast32signed (e2 ::: Enil)) ::: Enil)) ::: Enil))
       | _ => None
-      end.
+      end
+      else None.
  
 (** ** Recognition of addressing modes for load and store operations *)
 
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:
diff --git a/test/monniaux/cmov/cmov.c b/test/monniaux/cmov/cmov.c
new file mode 100644
index 00000000..2e388834
--- /dev/null
+++ b/test/monniaux/cmov/cmov.c
@@ -0,0 +1,22 @@
+#include <stdio.h>
+
+long cmovl(int x, long y, long z) {
+  return __builtin_sel(x, y, z);
+}
+
+int cmovi(int x, int y, int z) {
+  return __builtin_sel(x, y, z);
+}
+
+double cmovd(int x, double y, double z) {
+  return __builtin_sel(x, y, z);
+}
+
+int main() {
+  printf("%ld\n", cmovl(1, 42, 65));
+  printf("%ld\n", cmovl(0, 42, 65));
+  printf("%d\n", cmovi(1, 42, 65));
+  printf("%d\n", cmovi(0, 42, 65));
+  printf("%f\n", cmovd(1, 42., 65.));
+  printf("%f\n", cmovd(0, 42., 65.));
+}