Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work

19 files changed, 705 insertions, 20 deletions

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 4d075f4a..8f3f5f00 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -783,6 +783,8 @@ Lemma sel_select_opt_correct:
   Cminor.eval_expr ge sp e m cond vcond ->
   Cminor.eval_expr ge sp e m a1 v1 ->
   Cminor.eval_expr ge sp e m a2 v2 ->
+  Val.has_type v1 ty ->
+  Val.has_type v2 ty ->
   Val.bool_of_val vcond b ->
   env_lessdef e e' -> Mem.extends m m' ->
   exists v', eval_expr tge sp e' m' le a v' /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v'.
@@ -792,7 +794,7 @@ Proof.
   exploit sel_expr_correct. eexact H0. eauto. eauto. intros (vcond' & EVC & LDC).
   exploit sel_expr_correct. eexact H1. eauto. eauto. intros (v1' & EV1 & LD1).
   exploit sel_expr_correct. eexact H2. eauto. eauto. intros (v2' & EV2 & LD2).
-  assert (Val.bool_of_val vcond' b) by (inv H3; inv LDC; constructor).
+  assert (Val.bool_of_val vcond' b) by (inv H5; inv LDC; constructor).
   exploit eval_condition_of_expr. eexact EVC. eauto. rewrite C. intros (vargs' & EVARGS & EVCOND).
   exploit eval_select; eauto. intros (v' & X & Y). 
   exists v'; split; eauto. 
diff --git a/common/Values.v b/common/Values.v
index 4146dd59..5d32e54e 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -89,6 +89,27 @@ Definition has_type (v: val) (t: typ) : Prop :=
   | _, _ => False
   end.
 
+Definition has_type_b (v: val) (t: typ) :=
+  match v, t with
+  | Vundef, _ => true
+  | Vint _, Tint => true
+  | Vlong _, Tlong => true
+  | Vfloat _, Tfloat => true
+  | Vsingle _, Tsingle => true
+  | Vptr _ _, Tint => negb Archi.ptr64
+  | Vptr _ _, Tlong => Archi.ptr64
+  | (Vint _ | Vsingle _), Tany32 => true
+  | Vptr _ _, Tany32 => negb Archi.ptr64
+  | _, Tany64 => true
+  | _, _ => false
+  end.
+
+Lemma has_type_b_correct: forall v t,
+    has_type_b v t = true <-> has_type v t.
+Proof.
+  destruct v; destruct t; cbn; destruct Archi.ptr64; cbn; split; intros; auto; discriminate.
+Qed.
+
 Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop :=
   match vl, tl with
   | nil, nil => True
diff --git a/configure b/configure
index 35954c85..812ad6f7 100755
--- a/configure
+++ b/configure
@@ -842,6 +842,13 @@ BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
 EOF
 fi
 
+if [ "$arch" = "riscV" ] ; then
+cat >> Makefile.config <<EOF
+EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq
+BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v
+EOF
+fi
+
 #
 # Generate Merlin and CoqProject files to simplify development
 #
diff --git a/riscV/Asm.v b/riscV/Asm.v
index dc410a3b..5d3518f2 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -30,6 +30,7 @@ Require Import Smallstep.
 Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
+Require ExtValues.
 
 (** * Abstract syntax *)
 
@@ -62,10 +63,10 @@ Inductive freg: Type :=
   | F24: freg | F25: freg | F26: freg | F27: freg
   | F28: freg | F29: freg | F30: freg | F31: freg.
 
-Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
+Definition ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
-Lemma ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}.
+Definition ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}.
 Proof. decide equality. apply ireg_eq. Defined.
 
 Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
@@ -255,8 +256,10 @@ Inductive instruction : Type :=
 
   (* floating point register move *)
   | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
-  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
-  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
+  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r bitwise move FP single to integer register *)
+  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r bitwise move FP double to integer register *)
+  | Pfmvsx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP single *)
+  | Pfmvdx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP double*)
 
   (* 32-bit (single-precision) floating point *)
   | Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
@@ -345,6 +348,7 @@ Inductive instruction : Type :=
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
               -> builtin_res preg -> instruction    (**r built-in function (pseudo) *)
+  | Pselectl (rd: ireg) (rb: ireg0) (rt: ireg0) (rf: ireg0)
   | Pnop : instruction.                             (**r nop instruction *)
 
 
@@ -918,6 +922,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.floatofsingle rs#s))) m
   | Pfcvtsd d s =>
       Next (nextinstr (rs#d <- (Val.singleoffloat rs#s))) m
+          
+  | Pfmvxs d s =>
+      Next (nextinstr (rs#d <- (ExtValues.bits_of_single rs#s))) m
+  | Pfmvxd d s =>
+      Next (nextinstr (rs#d <- (ExtValues.bits_of_float rs#s))) m
+          
+  | Pfmvsx d s =>
+      Next (nextinstr (rs#d <- (ExtValues.single_of_bits rs#s))) m
+  | Pfmvdx d s =>
+      Next (nextinstr (rs#d <- (ExtValues.float_of_bits rs#s))) m
+
 
 (** Pseudo-instructions *)
   | Pallocframe sz pos =>
@@ -940,6 +955,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
           | _ => Stuck
           end
       end
+  | Pselectl rd rb rt rf =>
+    Next (nextinstr (rs#rd <- (ExtValues.select01_long
+                                 (rs###rb) (rs###rt) (rs###rf)))
+                     #X31 <- Vundef) m
   | Plabel lbl =>
       Next (nextinstr rs) m
   | Ploadsymbol rd s ofs =>
@@ -968,9 +987,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       so we do not model them. *)
   | Pfence
 
-  | Pfmvxs _ _
-  | Pfmvxd _ _
-
   | Pfmins _ _ _
   | Pfmaxs _ _ _
   | Pfsqrts _ _
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 810514a3..c5cd6817 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -582,9 +582,49 @@ let expand_builtin_inline name args res =
      raise (Error ("unrecognized builtin " ^ name))
 
 (* Expansion of instructions *)
-
+                                 
 let expand_instruction instr =
   match instr with
+  | Pselectl(rd, rb, rt, rf) ->
+     if not Archi.ptr64
+     then failwith "Pselectl not available on RV32, only on RV64"
+     else
+       if ireg0_eq rt rf then
+         begin
+           if ireg0_eq (X rd) rt then
+             begin
+             end
+           else
+             begin
+               emit (Paddl(rd, X0, rt))
+             end
+         end
+       else
+         if (ireg0_eq (X rd) rt) then
+           begin
+             emit (Psubl(X31, X0, rb));
+             emit (Pandl(X31, X X31, rt));
+             emit (Paddil(rd, rb, Int64.mone));
+             emit (Pandl(rd, X rd, rf));
+             emit (Porl(rd, X rd, X X31))
+           end
+         else
+           if (ireg0_eq (X rd) rf) then
+             begin
+               emit (Paddil(X31, rb, Int64.mone));
+               emit (Pandl(X31, X X31, rf));
+               emit (Psubl(rd, X0, rb));
+               emit (Pandl(rd, X rd, rt));
+               emit (Porl(rd, X rd, X X31))
+             end  
+           else
+             begin
+               emit (Psubl(X31, X0, rb));
+               emit (Paddil(rd, rb, Int64.mone));
+               emit (Pandl(X31, X X31, rt));
+               emit (Pandl(rd, X rd, rf));
+               emit (Porl(rd, X rd, X X31))
+             end
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (X30, X2));
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 4876f7ec..252a9270 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -899,6 +899,31 @@ Definition transl_op
       do r1 <- freg_of f1;
       do r2 <- freg_of f2;
       OK (Pfles rd r1 r2 :: k)
+
+  | Obits_of_single, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfmvxs rd rs :: k)
+  | Obits_of_float, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfmvxd rd rs :: k)
+  | Osingle_of_bits, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfmvsx rd rs :: k)
+  | Ofloat_of_bits, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfmvdx rd rs :: k)
+                               
+  | Ocmp cmp, _ =>
+      do rd <- ireg_of res;
+      transl_cond_op cmp rd args k
+
+  | Oselectl, b::t::f::nil =>
+      do rd <- ireg_of res;
+      do rb <- ireg_of b;
+      do rt <- ireg_of t;
+      do rf <- ireg_of f;
+      OK (Pselectl rd rb rt rf :: k)
+         
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index a826455e..1b3a0dbf 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1268,6 +1268,54 @@ Opaque Int.eq.
   split; intros; Simpl.
   all: destruct (rs x0); auto.
   all: destruct (rs x1); auto.
+  exists rs'; split; eauto. rewrite B; auto with asmgen.
+- (* shrxlimm *)
+  destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
+  {
+   exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
+  destruct (Int.eq n Int.zero).
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl. 
++ destruct (Int.eq n Int.one).
+  * econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    apply exec_straight_one. simpl; reflexivity. auto.
+    split; intros; Simpl.
+
+  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+    econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    apply exec_straight_one. simpl; reflexivity. auto. 
+    split; intros; Simpl.
+  }
+  destruct (Int.eq n Int.zero).
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl. 
++ destruct (Int.eq n Int.one).
+  * econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    apply exec_straight_one. simpl; reflexivity. auto.
+    split; intros; Simpl.
+
+  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+    econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    apply exec_straight_one. simpl; reflexivity. auto. 
+    split; intros; Simpl.
+  
+- (* cond *)
+  exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. eauto with asmgen.
+- (* select *)
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl.
+  apply Val.lessdef_normalize.
 Qed.
 
 (** Memory accesses *)
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index 53c83d7e..47bacffa 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.v
@@ -18,16 +18,35 @@
 Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
+Require ExtValues.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+| BI_bits_of_float
+| BI_bits_of_double
+| BI_float_of_bits
+| BI_double_of_bits.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+     ("__builtin_bits_of_float", BI_bits_of_float)
+  :: ("__builtin_bits_of_double", BI_bits_of_double)
+  :: ("__builtin_float_of_bits", BI_float_of_bits)
+  :: ("__builtin_double_of_bits", BI_double_of_bits)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  match b with
+  | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default
+  | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default
+  | BI_float_of_bits => mksignature (Tint :: nil) Tsingle cc_default
+  | BI_double_of_bits => mksignature (Tlong :: nil) Tfloat cc_default
+  end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  match b with
+  | BI_bits_of_float => mkbuiltin_n1t Tsingle Tint Float32.to_bits
+  | BI_bits_of_double => mkbuiltin_n1t Tfloat Tlong Float.to_bits
+  | BI_float_of_bits => mkbuiltin_n1t Tint Tsingle Float32.of_bits
+  | BI_double_of_bits => mkbuiltin_n1t Tlong Tfloat Float.of_bits
+  end.
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index a2087cb7..00b44fd5 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -46,6 +46,14 @@ let builtins = {
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmin",
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+    "__builtin_bits_of_double",
+      (TInt(IULong, []), [TFloat(FDouble, [])], false);
+    "__builtin_bits_of_float",
+      (TInt(IUInt, []), [TFloat(FFloat, [])], false);
+    "__builtin_double_of_bits",
+      (TFloat(FDouble, []), [TInt(IULong, [])], false);
+    "__builtin_float_of_bits",
+      (TFloat(FFloat, []), [TInt(IUInt, [])], false);
   ]
 }
 
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
new file mode 100644
index 00000000..edf359ef
--- /dev/null
+++ b/riscV/ExtValues.v
@@ -0,0 +1,123 @@
+Require Import Coqlib.
+Require Import Integers.
+Require Import Values.
+Require Import Floats.
+Require Import Memory.
+Require Import Lia.
+    
+Definition bits_of_float x :=
+  match x with
+  | Vfloat f => Vlong (Float.to_bits f)
+  | _ => Vundef
+  end.
+
+Definition bits_of_single x :=
+  match x with
+  | Vsingle f => Vint (Float32.to_bits f)
+  | _ => Vundef
+  end.
+
+Definition float_of_bits x :=
+  match x with
+  | Vlong f => Vfloat (Float.of_bits f)
+  | _ => Vundef
+  end.
+
+Definition single_of_bits x :=
+  match x with
+  | Vint f => Vsingle (Float32.of_bits f)
+  | _ => Vundef
+  end.
+
+Definition bitwise_select_long b vtrue vfalse :=
+  Int64.or (Int64.and (Int64.neg b) vtrue)
+           (Int64.and (Int64.sub b Int64.one) vfalse).
+
+Lemma bitwise_select_long_true :
+  forall vtrue vfalse,
+    bitwise_select_long Int64.one vtrue vfalse = vtrue.
+Proof.
+  intros. unfold bitwise_select_long. cbn.
+  change (Int64.neg Int64.one) with Int64.mone.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_mone.
+  rewrite Int64.sub_idem.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_zero.
+  apply Int64.or_zero.
+Qed.
+
+Lemma bitwise_select_long_false :
+  forall vtrue vfalse,
+    bitwise_select_long Int64.zero vtrue vfalse = vfalse.
+Proof.
+  intros. unfold bitwise_select_long. cbn.
+  rewrite Int64.neg_zero.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_zero.
+  rewrite Int64.sub_zero_r.
+  change (Int64.neg Int64.one) with Int64.mone.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_mone.
+  rewrite Int64.or_commut.
+  apply Int64.or_zero.
+Qed.
+
+Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val :=
+  match vb with
+  | (Vint b) =>
+    if Int.eq b Int.one
+    then vtrue
+    else if Int.eq b Int.zero
+         then vfalse
+         else Vundef
+  | _ => Vundef
+  end.
+
+Lemma normalize_select01:
+  forall x y z, Val.normalize (select01_long x y z) AST.Tlong = select01_long x (Val.normalize y AST.Tlong) (Val.normalize z AST.Tlong).
+Proof.
+  unfold select01_long.
+  intros.
+  destruct x; cbn; trivial.
+  destruct (Int.eq i Int.one); trivial.
+  destruct (Int.eq i Int.zero); trivial.
+Qed.
+
+Lemma select01_long_true:
+  forall vt vf,
+    select01_long Vtrue vt vf = vt.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true. reflexivity.
+Qed.
+
+Lemma select01_long_false:
+  forall vt vf,
+    select01_long Vfalse vt vf = vf.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true.
+  rewrite Int.eq_false. reflexivity.
+  cbv. discriminate.
+Qed.
+
+Lemma float_bits_normalize:
+  forall v1,
+  ExtValues.float_of_bits (Val.normalize (ExtValues.bits_of_float v1) AST.Tlong) =
+  Val.normalize v1 AST.Tfloat.
+Proof.
+  destruct v1; cbn; trivial.
+  f_equal.
+  apply Float.of_to_bits.
+Qed.
+
+Lemma single_bits_normalize:
+  forall v1,
+  ExtValues.single_of_bits (Val.normalize (ExtValues.bits_of_single v1) AST.Tint) =
+  Val.normalize v1 AST.Tsingle.
+Proof.
+  destruct v1; cbn; trivial.
+  f_equal.
+  apply Float32.of_to_bits.
+Qed.
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index d90c1b66..4b309f5b 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -116,6 +116,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEfeqs => op2 (default nv)
   | OEflts => op2 (default nv)
   | OEfles => op2 (default nv)
+  | Obits_of_single => op1 (default nv)
+  | Obits_of_float => op1 (default nv)
+  | Osingle_of_bits => op1 (default nv)
+  | Ofloat_of_bits => op1 (default nv)
+  | Oselectl => All :: nv :: nv :: nil
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -184,6 +189,16 @@ Proof.
 - apply shrimm_sound; auto.
 - apply shruimm_sound; auto.
 - apply xor_sound; auto with na.
+- (* selectl *)
+  unfold ExtValues.select01_long.
+  destruct v0; auto with na.
+  assert (Val.lessdef (Vint i) v4) as LESSDEF by auto with na.
+  inv LESSDEF.
+  destruct (Int.eq i Int.one).
+  { apply normalize_sound; auto. }
+  destruct (Int.eq i Int.zero).
+  { apply normalize_sound; auto. }
+  cbn. auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/riscV/Op.v b/riscV/Op.v
index cd74080f..4c2390a1 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -32,6 +32,7 @@
 Require Import BoolEqual Coqlib.
 Require Import AST Integers Floats.
 Require Import Values Memory Globalenvs Events.
+Require ExtValues.
 
 Set Implicit Arguments.
 
@@ -200,6 +201,12 @@ Inductive operation : Type :=
   | OEfeqs                                       (**r compare equal *)
   | OEflts                                       (**r compare less-than *)
   | OEfles.                                      (**r compare less-than/equal *)
+  | Ocmp (cond: condition)  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Obits_of_single
+  | Obits_of_float
+  | Osingle_of_bits
+  | Ofloat_of_bits
+  | Oselectl.
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -411,6 +418,10 @@ Definition eval_operation
   | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1))
   | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
+  | Obits_of_single, v1::nil => Some (ExtValues.bits_of_single v1)
+  | Obits_of_float, v1::nil => Some (ExtValues.bits_of_float v1)
+  | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1)
+  | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1)
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   (* Expansed conditions *)
   | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32)
@@ -442,6 +453,7 @@ Definition eval_operation
   | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2)
   | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2)
   | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2)
+  | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
   | _, _ => None
   end.
 
@@ -472,9 +484,9 @@ Qed.
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
-      destruct x; simpl in H; FuncInv
+      destruct x; cbn in H; FuncInv
   | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ =>
-      destruct v; simpl in H; FuncInv
+      destruct v; cbn in H; FuncInv
   | H: (if Archi.ptr64 then _ else _) = Some _ |- _ =>
       destruct Archi.ptr64 eqn:?; FuncInv
   | H: (Some _ = Some _) |- _ =>
@@ -643,6 +655,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEfeqs => (Tsingle :: Tsingle :: nil, Tint)
   | OEflts => (Tsingle :: Tsingle :: nil, Tint)
   | OEfles => (Tsingle :: Tsingle :: nil, Tint)
+  | Obits_of_single => (Tsingle :: nil, Tint)
+  | Obits_of_float => (Tfloat :: nil, Tlong)
+  | Osingle_of_bits => (Tint :: nil, Tsingle)
+  | Ofloat_of_bits => (Tlong :: nil, Tfloat)
+  | Oselectl => (Tint :: Tlong :: Tlong :: nil, Tlong)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -929,6 +946,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OEfles *)
   - destruct v0; destruct v1; cbn; auto.
     destruct Float32.cmp; cbn; auto.
+  (* Bits_of_single, float *)
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
+  (* single, float of bits *)
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
+  (* selectl *)
+  - destruct v0; cbn; trivial.
+    destruct Int.eq; cbn.
+    apply Val.normalize_type.
+    destruct Int.eq; cbn; trivial.
+    apply Val.normalize_type.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -1767,6 +1796,17 @@ Proof.
   (* OEfles *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto.
+  (* Bits_of_single, double *)
+  - inv H4; simpl; auto.
+  - inv H4; simpl; auto.
+  (* single, double of bits *)
+  - inv H4; simpl; auto.
+  - inv H4; simpl; auto.
+  (* selectl *)
+  - inv H4; trivial. cbn.
+    destruct (Int.eq i Int.one).
+    + auto using Val.normalize_inject.
+    + destruct (Int.eq i Int.zero); cbn; auto using Val.normalize_inject.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index e11dd530..84380251 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -222,6 +222,11 @@ let print_operation reg pp = function
   | OEfeqs, [r1;r2] -> fprintf pp "OEfeqs(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
   | OEflts, [r1;r2] -> fprintf pp "OEflts(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
   | OEfles, [r1;r2] -> fprintf pp "OEfles(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2
+  | Obits_of_single, [r1] -> fprintf pp "bits_of_single(%a)" reg r1
+  | Obits_of_float, [r1] -> fprintf pp "bits_of_float(%a)" reg r1
+  | Osingle_of_bits, [r1] -> fprintf pp "single_of_bits(%a)" reg r1
+  | Ofloat_of_bits, [r1] -> fprintf pp "float_of_bits(%a)" reg r1
+  | Oselectl, [rb;rt;rf] -> fprintf pp "selectl(b:%a, t:%a, f:%a)" reg rb reg rt reg rf
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index e9920e46..9932aaf8 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -419,9 +419,39 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 (** ** Selection *)
 
+Definition same_expr_pure (e1 e2: expr) :=
+  match e1, e2 with
+  | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false
+  | _, _ => false
+  end.
+
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
-   : option expr
-   := None.
+  : option expr :=
+  if same_expr_pure e1 e2
+  then Some e1
+  else
+     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))
+      | Tfloat => Some (Eop Ofloat_of_bits ((Eop Oselectl
+                       ((Eop (Ocmp cond) args) :::
+		         (Eop Obits_of_float (e1 ::: Enil)) :::
+			 (Eop Obits_of_float (e2 ::: Enil)) ::: Enil)) ::: Enil))
+      | Tsingle => Some
+         (Eop Osingle_of_bits
+           ((Eop Olowlong ((Eop Oselectl
+             ((Eop (Ocmp cond) args) :::
+         (Eop Ocast32signed ((Eop Obits_of_single (e1 ::: Enil)) ::: Enil)) :::
+	 (Eop Ocast32signed ((Eop Obits_of_single (e2 ::: Enil)) ::: Enil))
+	 ::: Enil)) ::: Enil)) ::: Enil))
+      | _ => None
+      end
+      else None.
  
 (** ** Recognition of addressing modes for load and store operations *)
 
@@ -462,4 +492,9 @@ Definition divfs_base (e1: expr) (e2: expr) :=
 (** Platform-specific known builtins *)
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
-  None.
+  match b with
+  | BI_bits_of_float => Some (Eop Obits_of_single args)
+  | BI_bits_of_double => Some (Eop Obits_of_float args)
+  | BI_float_of_bits => Some (Eop Osingle_of_bits args)
+  | BI_double_of_bits => Some (Eop Ofloat_of_bits args)
+  end.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 1d13702a..ce80fc57 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,71 @@ 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.
+
+Lemma same_expr_pure_correct:
+  forall le a1 a2 v1 v2
+    (PURE : same_expr_pure a1 a2 = true)
+    (EVAL1 : eval_expr ge sp e m le a1 v1)
+    (EVAL2 : eval_expr ge sp e m le a2 v2),
+    v1 = v2.
+Proof.
+  intros.
+  destruct a1; destruct a2; cbn in *; try discriminate.
+  inv EVAL1. inv EVAL2.
+  destruct (ident_eq i i0); congruence.
+Qed.
+  
 Theorem eval_select:
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
@@ -886,7 +952,56 @@ Theorem eval_select:
      eval_expr ge sp e m le a v
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
-  unfold select; intros; discriminate.
+  unfold select; intros.
+  pose proof (same_expr_pure_correct le a1 a2 v1 v2) as PURE.
+  destruct (same_expr_pure a1 a2).
+  { rewrite <- PURE by auto.
+    inv H.
+    exists v1. split. assumption.
+    unfold Val.select.
+    destruct b; apply Val.lessdef_normalize.
+  }
+  clear PURE.
+  destruct Archi.ptr64 eqn:PTR64.
+  2: discriminate.
+  destruct ty; cbn in *; try discriminate.
+  - (* Tint *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      rewrite H3. destruct b.
+      * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
+      * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
+        
+  - (* Tfloat *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      rewrite H3. destruct b.
+      * rewrite ExtValues.select01_long_true.
+        apply ExtValues.float_bits_normalize.
+      * rewrite ExtValues.select01_long_false.
+        apply ExtValues.float_bits_normalize.
+
+  - (* Tlong *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      rewrite H3. destruct b.
+      * rewrite ExtValues.select01_long_true. reflexivity.
+      * rewrite ExtValues.select01_long_false. reflexivity.
+
+  - (* Tsingle *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      rewrite H3. destruct b.
+      * rewrite ExtValues.select01_long_true.
+        rewrite normalize_low_long by assumption.
+        apply ExtValues.single_bits_normalize.
+      * rewrite ExtValues.select01_long_false.
+        rewrite normalize_low_long by assumption.
+        apply ExtValues.single_bits_normalize.
 Qed.
 
 Theorem eval_addressing:
@@ -969,7 +1084,10 @@ Theorem eval_platform_builtin:
   platform_builtin_sem bf vl = Some v ->
   exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
 Proof.
-  intros. discriminate.
+  destruct bf; intros until le; intro Heval.
+  all: try (inversion Heval; subst a; clear Heval;
+       exists v; split; trivial;
+       repeat (try econstructor; try eassumption)).
 Qed.
 
 End CMCONSTR.
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 1f02ca71..1f00c440 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -396,6 +396,10 @@ module Target : TARGET =
          fprintf oc "	fmv.x.s	%a, %a\n"     ireg rd freg fs
       | Pfmvxd (rd,fs) ->
          fprintf oc "	fmv.x.d	%a, %a\n"     ireg rd freg fs
+      | Pfmvsx (fd,rs) ->
+         fprintf oc "	fmv.s.x	%a, %a\n"     freg fd ireg rs
+      | Pfmvdx (fd,rs) ->
+         fprintf oc "	fmv.d.x	%a, %a\n"     freg fd ireg rs
 
       (* 32-bit (single-precision) floating point *)
       | Pfls (fd, ra, ofs) ->
@@ -525,6 +529,8 @@ module Target : TARGET =
          fprintf oc "	fcvt.s.d	%a, %a\n" freg fd freg fs
 
       (* Pseudo-instructions expanded in Asmexpand *)
+      | Pselectl(_, _, _, _) ->
+         assert false
       | Pallocframe(sz, ofs) ->
          assert false
       | Pfreeframe(sz, ofs) ->
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 00b49bc1..97f3ff61 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -86,6 +86,39 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
   | _, _ => Vbot
   end.
 
+Definition bits_of_single (v : aval) : aval :=
+  match v with
+  | FS f => I (Float32.to_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition bits_of_float (v : aval) : aval :=
+  match v with
+  | F f => L (Float.to_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition single_of_bits (v : aval) : aval :=
+  match v with
+  | I f => FS (Float32.of_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition float_of_bits (v : aval) : aval :=
+  match v with
+  | L f => F (Float.of_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition select01_long (vb : aval) (vt : aval) (vf : aval) :=
+  match vb with
+  | I b =>
+    if Int.eq b Int.one then add_undef vt
+    else if Int.eq b Int.zero then add_undef vf
+         else add_undef (vlub vt vf)
+  | _ => add_undef (vlub vt vf)
+  end.
+
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -210,6 +243,11 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2)
   | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2)
   | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2)
+  | Obits_of_single, v1::nil => bits_of_single v1
+  | Obits_of_float, v1::nil => bits_of_float v1
+  | Osingle_of_bits, v1::nil => single_of_bits v1
+  | Ofloat_of_bits, v1::nil => float_of_bits v1
+  | Oselectl, vb::vt::vf::nil => select01_long vb vt vf
   | _, _ => Vbot
   end.
 
@@ -221,6 +259,75 @@ Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
 Hypothesis STACK: bc sp = BCstack.
 
+Lemma bits_of_single_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_single v) (bits_of_single x).
+Proof.
+  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
+Qed.
+
+Lemma bits_of_float_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_float v) (bits_of_float x).
+Proof.
+  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
+Qed.
+
+Lemma single_of_bits_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.single_of_bits v) (single_of_bits x).
+Proof.
+  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
+Qed.
+
+Lemma float_of_bits_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.float_of_bits v) (float_of_bits x).
+Proof.
+  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
+Qed.
+
+  
+Lemma select01_long_sound:
+  forall vb xb vt xt vf xf
+         (MATCH_b : vmatch bc vb xb)
+         (MATCH_t : vmatch bc vt xt)
+         (MATCH_f : vmatch bc vf xf),
+    vmatch bc (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
+              (select01_long xb xt xf).
+Proof.
+  intros.
+  inv MATCH_b; cbn; try apply add_undef_undef.
+  - destruct (Int.eq i Int.one). { apply add_undef_normalize; trivial. }
+    destruct (Int.eq i Int.zero). { apply add_undef_normalize; trivial. }
+    cbn. apply add_undef_undef.
+  - destruct (Int.eq i Int.one).
+    { apply add_undef_normalize.
+      apply vmatch_lub_l.
+      trivial. }
+    destruct (Int.eq i Int.zero).
+    { apply add_undef_normalize.
+      apply vmatch_lub_r.
+      trivial. }
+    cbn. apply add_undef_undef.
+  - destruct (Int.eq i Int.one).
+    { apply add_undef_normalize.
+      apply vmatch_lub_l.
+      trivial. }
+    destruct (Int.eq i Int.zero).
+    { apply add_undef_normalize.
+      apply vmatch_lub_r.
+      trivial. }
+    cbn. apply add_undef_undef.
+  - destruct (Int.eq i Int.one).
+    { apply add_undef_normalize.
+      apply vmatch_lub_l.
+      trivial. }
+    destruct (Int.eq i Int.zero).
+    { apply add_undef_normalize.
+      apply vmatch_lub_r.
+      trivial. }
+    cbn. apply add_undef_undef.
+Qed.
+
+Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound select01_long_sound : va.
+
 Theorem eval_static_condition_sound:
   forall cond vargs m aargs,
   list_forall2 (vmatch bc) vargs aargs ->
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.));
+}
diff --git a/test/monniaux/cmov/cmov2.c b/test/monniaux/cmov/cmov2.c
new file mode 100644
index 00000000..6ecab61b
--- /dev/null
+++ b/test/monniaux/cmov/cmov2.c
@@ -0,0 +1,28 @@
+#include <stdio.h>
+
+long cmovl(int x, long y, long z) {
+  return x ? y : z;
+}
+
+int cmovi(int x, int y, int z) {
+  return x ? y : z;
+}
+
+double cmovd(int x, double y, double z) {
+  return x ? y : z;
+}
+
+float cmovf(int x, float y, float z) {
+  return 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.));
+  printf("%f\n", cmovf(1, 42.f, 65.f));
+  printf("%f\n", cmovf(0, 42.f, 65.f));
+}