Merge branch 'master' into merge_master_8.13.1

PARTIAL MERGE (PARTLY BROKEN).

See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE

WARNING:
 interface of va_args and assembly sections have changed

11 files changed, 761 insertions, 177 deletions

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index c5cd6817..a49efce8 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -24,6 +24,7 @@ open Asmexpandaux
 open AST
 open Camlcoq
 open! Integers
+open Locations
 
 exception Error of string
 
@@ -50,6 +51,86 @@ let expand_addptrofs dst src n =
 let expand_storeind_ptr src base ofs =
   List.iter emit (Asmgen.storeind_ptr src base ofs [])
 
+(* Fix-up code around function calls and function entry.
+   Some floating-point arguments residing in FP registers need to be
+   moved to integer registers or register pairs.
+   Symmetrically, some floating-point parameter passed in integer
+   registers or register pairs need to be moved to FP registers. *)
+
+let int_param_regs = [| X10; X11; X12; X13; X14; X15; X16; X17 |]
+
+let move_single_arg fr i =
+  emit (Pfmvxs(int_param_regs.(i), fr))
+
+let move_double_arg fr i =
+  if Archi.ptr64 then begin
+    emit (Pfmvxd(int_param_regs.(i), fr))
+  end else begin
+    emit (Paddiw(X2, X X2, Integers.Int.neg _16));
+    emit (Pfsd(fr, X2, Ofsimm _0));
+    emit (Plw(int_param_regs.(i), X2, Ofsimm _0));
+    if i < 7 then begin
+      emit (Plw(int_param_regs.(i + 1), X2, Ofsimm _4))
+    end else begin
+      emit (Plw(X31, X2, Ofsimm _4));
+      emit (Psw(X31, X2, Ofsimm _16))
+    end;
+    emit (Paddiw(X2, X X2, _16))
+  end
+
+let move_single_param fr i =
+  emit (Pfmvsx(fr, int_param_regs.(i)))
+
+let move_double_param fr i =
+  if Archi.ptr64 then begin
+    emit (Pfmvdx(fr, int_param_regs.(i)))
+  end else begin
+    emit (Paddiw(X2, X X2, Integers.Int.neg _16));
+    emit (Psw(int_param_regs.(i), X2, Ofsimm _0));
+    if i < 7 then begin
+      emit (Psw(int_param_regs.(i + 1), X2, Ofsimm _4))
+    end else begin
+      emit (Plw(X31, X2, Ofsimm _16));
+      emit (Psw(X31, X2, Ofsimm _4))
+    end;
+    emit (Pfld(fr, X2, Ofsimm _0));
+    emit (Paddiw(X2, X X2, _16))
+  end
+
+let float_extra_index = function
+  | Machregs.F0 -> Some (F0, 0)
+  | Machregs.F1 -> Some (F1, 1)
+  | Machregs.F2 -> Some (F2, 2)
+  | Machregs.F3 -> Some (F3, 3)
+  | Machregs.F4 -> Some (F4, 4)
+  | Machregs.F5 -> Some (F5, 5)
+  | Machregs.F6 -> Some (F6, 6)
+  | Machregs.F7 -> Some (F7, 7)
+  | _  -> None
+
+let fixup_gen single double sg =
+  let fixup ty loc =
+    match ty, loc with
+    | Tsingle, One (R r) ->
+        begin match float_extra_index r with
+        | Some(r, i) -> single r i
+        | None -> ()
+        end
+    | (Tfloat | Tany64), One (R r) ->
+        begin match float_extra_index r with
+        | Some(r, i) -> double r i
+        | None -> ()
+        end
+    | _, _ -> ()
+  in
+    List.iter2 fixup sg.sig_args (Conventions1.loc_arguments sg)
+
+let fixup_call sg =
+  fixup_gen move_single_arg move_double_arg sg
+
+let fixup_function_entry sg =
+  fixup_gen move_single_param move_double_param sg
+
 (* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
      locations; generate no code;
@@ -57,51 +138,6 @@ let expand_storeind_ptr src base ofs =
      registers.
 *)
 
-(* Fix-up code around calls to variadic functions.  Floating-point arguments
-   residing in FP registers need to be moved to integer registers. *)
-
-let int_param_regs   = [| X10; X11; X12; X13; X14; X15; X16; X17 |]
-let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |]
-
-let rec fixup_variadic_call ri rf tyl =
-  if ri < 8 then
-    match tyl with
-    | [] ->
-        ()
-    | (Tint | Tany32) :: tyl ->
-        fixup_variadic_call (ri + 1) rf tyl
-    | Tsingle :: tyl ->
-        let rs = float_param_regs.(rf)
-        and rd = int_param_regs.(ri) in
-        emit (Pfmvxs(rd, rs));
-        fixup_variadic_call (ri + 1) (rf + 1) tyl
-    | Tlong :: tyl ->
-        let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in
-        fixup_variadic_call ri' rf tyl
-    | (Tfloat | Tany64) :: tyl ->
-        if Archi.ptr64 then begin
-          let rs = float_param_regs.(rf)
-          and rd = int_param_regs.(ri) in
-          emit (Pfmvxd(rd, rs));
-          fixup_variadic_call (ri + 1) (rf + 1) tyl
-        end else begin
-          let ri = align ri 2 in
-          if ri < 8 then begin
-            let rs = float_param_regs.(rf)
-            and rd1 = int_param_regs.(ri)
-            and rd2 = int_param_regs.(ri + 1) in
-            emit (Paddiw(X2, X X2, Integers.Int.neg _16));
-            emit (Pfsd(rs, X2, Ofsimm _0));
-            emit (Plw(rd1, X2, Ofsimm _0));
-            emit (Plw(rd2, X2, Ofsimm _4));
-            emit (Paddiw(X2, X X2, _16));
-            fixup_variadic_call (ri + 2) (rf + 1) tyl
-          end
-        end
-        
-let fixup_call sg =
-  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args
-
 (* Handling of annotations *)
 
 let expand_annot_val kind txt targ args res =
@@ -305,18 +341,53 @@ let expand_builtin_vstore chunk args =
 
 (* Handling of varargs *)
 
-(* Size in words of the arguments to a function.  This includes both
-   arguments passed in registers and arguments passed on stack. *)
+(* Number of integer registers, FP registers, and stack words
+   used to pass the (fixed) arguments to a function. *)
+
+let arg_int_size ri rf ofs k =
+  if ri < 8
+  then k (ri + 1) rf ofs
+  else k ri rf (ofs + 1)
+
+let arg_single_size ri rf ofs k =
+  if rf < 8
+  then k ri (rf + 1) ofs
+  else arg_int_size ri rf ofs k
+
+let arg_long_size ri rf ofs k =
+  if Archi.ptr64 then
+    if ri < 8
+    then k (ri + 1) rf ofs
+    else k ri rf (ofs + 1)
+  else
+    if ri < 7 then k (ri + 2) rf ofs
+    else if ri = 7 then k (ri + 1) rf (ofs + 1)
+    else k ri rf (align ofs 2 + 2)
+
+let arg_double_size ri rf ofs k =
+  if rf < 8
+  then k ri (rf + 1) ofs
+  else arg_long_size ri rf ofs k
+
+let rec args_size l ri rf ofs =
+  match l with
+  | [] -> (ri, rf, ofs)
+  | (Tint | Tany32) :: l ->
+      arg_int_size ri rf ofs (args_size l)
+  | Tsingle :: l ->
+      arg_single_size ri rf ofs (args_size l)
+  | Tlong :: l ->
+      arg_long_size ri rf ofs (args_size l)
+  | (Tfloat | Tany64) :: l ->
+      arg_double_size ri rf ofs (args_size l)
 
-let rec args_size sz = function
-  | [] -> sz
-  | (Tint | Tsingle | Tany32) :: l ->
-      args_size (sz + 1) l
-  | (Tlong | Tfloat | Tany64) :: l ->
-      args_size (if Archi.ptr64 then sz + 1 else align sz 2 + 2) l
+(* Size in words of the arguments to a function.  This includes both
+   arguments passed in integer registers and arguments passed on stack,
+   but not arguments passed in FP registers. *)
 
 let arguments_size sg =
-  args_size 0 sg.sig_args
+  let (ri, _, ofs) = args_size sg.sig_args 0 0 0 in
+  ri + ofs
 
 let save_arguments first_reg base_ofs =
   for i = first_reg to 7 do
@@ -628,7 +699,7 @@ let expand_instruction instr =
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (X30, X2));
-      if sg.sig_cc.cc_vararg then begin
+      if (sg.sig_cc.cc_vararg <> None) then begin
         let n = arguments_size sg in
         let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
@@ -646,7 +717,7 @@ let expand_instruction instr =
   | Pfreeframe (sz, ofs) ->
      let sg = get_current_function_sig() in
      let extra_sz =
-      if sg.sig_cc.cc_vararg then begin
+      if (sg.sig_cc.cc_vararg <> None) then begin
         let n = arguments_size sg in
         if n >= 8 then 0 else align ((8 - n) * wordsize) 16
       end else 0 in
@@ -746,6 +817,7 @@ let preg_to_dwarf = function
 let expand_function id fn =
   try
     set_current_function fn;
+    fixup_function_entry fn.fn_sig;
     expand id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 6abad4ed..d9715984 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -67,7 +67,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Lemma exec_straight_exec:
@@ -332,8 +332,8 @@ Proof.
   split. unfold goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto.
   rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
+  auto. lia.
+  generalize (transf_function_no_overflow _ _ H0). lia.
   intros. apply Pregmap.gso; auto.
 Qed.
 
@@ -854,10 +854,10 @@ Local Transparent destroyed_by_op.
     rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. rewrite F. reflexivity.
     reflexivity. 
     eexact U. }
-  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
+  exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor.
   intros (ofs' & X & Y).                    
   left; exists (State rs3 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor.
+  eapply exec_straight_steps_1; eauto. lia. constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
   apply agree_exten with rs2; eauto with asmgen.
@@ -886,7 +886,7 @@ Local Transparent destroyed_at_function_entry.
 
 - (* return *)
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
 Qed.
diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v
index 26a50317..74dc4a05 100644
--- a/riscV/ConstpropOpproof.v
+++ b/riscV/ConstpropOpproof.v
@@ -365,7 +365,7 @@ Proof.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
   rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto.
   rewrite Int.bits_not by auto. apply negb_involutive.
   rewrite H6 by auto. auto.
   econstructor; split; eauto. auto.
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 17326139..eeaae3c4 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -172,25 +172,29 @@ Qed.
 (** ** Location of function arguments *)
 
 (** The RISC-V ABI states the following conventions for passing arguments
-  to a function:
+  to a function.  First for non-variadic functions:
 
-- RV64, not variadic: pass the first 8 integer arguments in
-  integer registers (a1...a8: int_param_regs), the first 8 FP arguments
-  in FP registers (fa1...fa8: float_param_regs), and the remaining
-  arguments on the stack, in 8-byte slots.
+- RV64: pass the first 8 integer arguments in integer registers
+  (a1...a8: int_param_regs), the first 8 FP arguments in FP registers
+  (fa1...fa8: float_param_regs) then in integer registers (a1...a8),
+  and the remaining arguments on the stack, in 8-byte slots.
 
-- RV32, not variadic: same, but arguments of 64-bit integer type
-  are passed in two consecutive integer registers (a(i), a(i+1))
-  or in a(8) and on a 32-bit word on the stack.  Stack-allocated
-  arguments are aligned to their natural alignment.
+- RV32: same, but arguments of size 64 bits that must be passed in
+  integer registers are passed in two consecutive integer registers
+  (a(i), a(i+1)), or in a(8) and on a 32-bit word on the stack.
+  Stack-allocated arguments are aligned to their natural alignment.
 
-- RV64, variadic: pass the first 8 arguments in integer registers
-  (a1...a8), including FP arguments; pass the remaining arguments on
-  the stack, in 8-byte slots.
+For variadic functions, the fixed arguments are passed as described
+above, then the variadic arguments receive special treatment:
 
-- RV32, variadic: same, but arguments of 64-bit types (integers as well
+- RV64: FP registers are not used for passing variadic arguments.
+  All variadic arguments, including FP arguments, are passed in the
+  remaining integer registers (a1...a8), then on the stack, in 8-byte
+  slots.
+
+- RV32: likewise, but arguments of 64-bit types (integers as well
   as floats) are passed in two consecutive aligned integer registers
-  (a(2i), a(2i+1)).  
+  (a(2i), a(2i+1)), or on the stack, in aligned 8-byte slots.
 
 The passing of FP arguments to variadic functions in integer registers
 doesn't quite fit CompCert's model.  We do our best by passing the FP
@@ -204,6 +208,15 @@ Definition int_param_regs :=
 Definition float_param_regs :=
   F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil.
 
+(** To evaluate FP arguments that must be passed in integer registers,
+    we can use any FP caller-save register that is not already used to pass
+    a fixed FP argument.  Since there are 8 integer registers for argument
+    passing, we need at most 8 extra more FP registers for these FP
+    arguments. *)
+
+Definition float_extra_param_regs :=
+  F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil.
+
 Definition int_arg (ri rf ofs: Z) (ty: typ)
                    (rec: Z -> Z -> Z -> list (rpair loc)) :=
   match list_nth_z int_param_regs ri with
@@ -217,26 +230,27 @@ Definition int_arg (ri rf ofs: Z) (ty: typ)
 
 Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ)
                      (rec: Z -> Z -> Z -> list (rpair loc)) :=
-  match list_nth_z float_param_regs rf with
+  match list_nth_z (if va then nil else float_param_regs) rf with
   | Some r =>
-      if va then
-       (let ri' :=  (* reserve 1 or 2 aligned integer registers *)
-          if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2 in
-        if zle ri' 8 then
-            (* we have enough integer registers, put argument in FP reg
-               and fixup code will put it in one or two integer regs *)
-            One (R r) :: rec ri' (rf + 1) ofs
-        else
-            (* we are out of integer registers, pass argument on stack *)
+      One (R r) :: rec ri (rf + 1) ofs
+  | None =>
+      (* We are out of FP registers, or cannot use them because vararg,
+         so try to put the argument in an extra FP register while
+         reserving an integer register or register pair into which
+         fixup code will move the extra FP register. *)
+      let regpair := negb Archi.ptr64 && zeq (typesize ty) 2 in
+      let ri' := if va && regpair then align ri 2 else ri in
+      match list_nth_z float_extra_param_regs ri' with
+      | Some r =>
+          let ri'' := ri' + (if Archi.ptr64 then 1 else typesize ty) in
+          let ofs'' := if regpair && zeq ri' 7 then ofs + 1 else ofs in
+          One (R r) :: rec ri'' rf ofs''
+      | None =>
+          (* We are out of integer registers, pass argument on stack *)
             let ofs := align ofs (typesize ty) in
             One(S Outgoing ofs ty)
-            :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)))
-      else
-        One (R r) :: rec ri (rf + 1) ofs
-  | None   =>
-      let ofs := align ofs (typesize ty) in
-      One(S Outgoing ofs ty)
-      :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
+            :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
+      end
   end.
 
 Definition split_long_arg (va: bool) (ri rf ofs: Z)
@@ -253,35 +267,43 @@ Definition split_long_arg (va: bool) (ri rf ofs: Z)
       rec ri rf (ofs + 2)
   end.
 
-Fixpoint loc_arguments_rec (va: bool)
-    (tyl: list typ) (ri rf ofs: Z) {struct tyl} : list (rpair loc) :=
+Fixpoint loc_arguments_rec
+    (tyl: list typ) (fixed ri rf ofs: Z) {struct tyl} : list (rpair loc) :=
   match tyl with
   | nil => nil
   | (Tint | Tany32) as ty :: tys =>
       (* pass in one integer register or on stack *)
-      int_arg ri rf ofs ty (loc_arguments_rec va tys)
+      int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
   | Tsingle as ty :: tys =>
       (* pass in one FP register or on stack.
          If vararg, reserve 1 integer register. *)
-      float_arg va ri rf ofs ty (loc_arguments_rec va tys)
+      float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
   | Tlong as ty :: tys =>
       if Archi.ptr64 then
         (* pass in one integer register or on stack *)
-        int_arg ri rf ofs ty (loc_arguments_rec va tys)
+        int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
       else
         (* pass in register pair or on stack; align register pair if vararg *)
-        split_long_arg va ri rf ofs(loc_arguments_rec va tys)
+        split_long_arg (zle fixed 0) ri rf ofs(loc_arguments_rec tys (fixed - 1))
   | (Tfloat | Tany64) as ty :: tys =>
       (* pass in one FP register or on stack.
          If vararg, reserve 1 or 2 integer registers. *)
-      float_arg va ri rf ofs ty (loc_arguments_rec va tys)
+      float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1))
+  end.
+
+(** Number of fixed arguments for a function with signature [s]. *)
+
+Definition fixed_arguments (s: signature) : Z :=
+  match s.(sig_cc).(cc_vararg) with
+  | Some n => n
+  | None => list_length_z s.(sig_args)
   end.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0.
+  loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -306,17 +328,19 @@ Proof.
   { decide_goal. }
   assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false).
   { decide_goal. }
+  assert (CSFX: forall r, In r float_extra_param_regs -> is_callee_save r = false).
+  { decide_goal. }
   assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0).
   { intros. 
     assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos).
-    omega. }
+    lia. }
   assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))).
   { intros. eapply Z.divide_trans. apply typealign_typesize.
     apply align_divides. apply typesize_pos. }
   assert (SK: (if Archi.ptr64 then 2 else 1) > 0).
-  { destruct Archi.ptr64; omega. }
+  { destruct Archi.ptr64; lia. }
   assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0).
-  { intros. destruct Archi.ptr64. omega. apply typesize_pos.  }
+  { intros. destruct Archi.ptr64. lia. apply typesize_pos.  }
   assert (A: forall ri rf ofs ty f,
              OKF f -> ofs >= 0 -> OK (int_arg ri rf ofs ty f)).
   { intros until f; intros OF OO; red; unfold int_arg; intros.
@@ -325,23 +349,22 @@ Proof.
   - eapply OF; eauto. 
   - subst p; simpl. auto using align_divides, typealign_pos.
   - eapply OF; [idtac|eauto].
-    generalize (AL ofs ty OO) (SKK ty); omega.
+    generalize (AL ofs ty OO) (SKK ty); lia.
   }
   assert (B: forall va ri rf ofs ty f,
              OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)).
   { intros until f; intros OF OO; red; unfold float_arg; intros.
-    destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH.
-  - set (ri' := if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2) in *.
-    destruct va; [destruct (zle ri' 8)|idtac]; destruct H.
-    + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
-    + eapply OF; eauto.
-    + subst p; repeat split; auto.
-    + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
-    + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
-    + eapply OF; eauto.
+    destruct (list_nth_z (if va then nil else float_param_regs) rf) as [r|] eqn:NTH.
   - destruct H.
-    + subst p; repeat split; auto.
-    + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+    + subst p; simpl. apply CSF. destruct va. simpl in NTH; discriminate. eapply list_nth_z_in; eauto.
+    + eapply OF; eauto.
+  - set (regpair := negb Archi.ptr64 && zeq (typesize ty) 2) in *.
+    set (ri' := if va && regpair then align ri 2 else ri) in *.
+    destruct (list_nth_z float_extra_param_regs ri') as [r|] eqn:NTH'; destruct H.
+    + subst p; simpl. apply CSFX. eapply list_nth_z_in; eauto.
+    + eapply OF; [|eauto]. destruct (regpair && zeq ri' 7); lia.
+    + subst p; simpl. auto.
+    + eapply OF; [|eauto]. generalize (AL ofs ty OO) (SKK ty); lia.
   }
   assert (C: forall va ri rf ofs f,
              OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)).
@@ -353,35 +376,35 @@ Proof.
     [destruct (list_nth_z int_param_regs (ri'+1)) as [r2|] eqn:NTH2 | idtac].
   - red; simpl; intros; destruct H.
     + subst p; split; apply CSI; eauto using list_nth_z_in.
-    + eapply OF; [idtac|eauto]. omega.
+    + eapply OF; [idtac|eauto]. lia.
   - red; simpl; intros; destruct H.
     + subst p; split. split; auto using Z.divide_1_l. apply CSI; eauto using list_nth_z_in.
-    + eapply OF; [idtac|eauto]. omega.
+    + eapply OF; [idtac|eauto]. lia.
   - red; simpl; intros; destruct H.
-    + subst p; repeat split; auto using Z.divide_1_l. omega. 
-    + eapply OF; [idtac|eauto]. omega.
+    + subst p; repeat split; auto using Z.divide_1_l. lia. 
+    + eapply OF; [idtac|eauto]. lia.
   }
-  cut (forall va tyl ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl ri rf ofs)).
+  cut (forall tyl fixed ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec tyl fixed ri rf ofs)).
   unfold OK. eauto.
   induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.
 - red; simpl; tauto.
 - destruct ty1.
-+ (* int *) apply A; auto.
-+ (* float *) apply B; auto.
++ (* int *) apply A; unfold OKF; auto.
++ (* float *) apply B; unfold OKF; auto.
 + (* long *)
   destruct Archi.ptr64.
-  apply A; auto.
-  apply C; auto.
-+ (* single *) apply B; auto.
-+ (* any32 *) apply A; auto.
-+ (* any64 *) apply B; auto.
+  apply A; unfold OKF; auto.
+  apply C; unfold OKF; auto.
++ (* single *) apply B; unfold OKF; auto.
++ (* any32 *) apply A; unfold OKF; auto.
++ (* any64 *) apply B; unfold OKF; auto.
 Qed.
 
 Lemma loc_arguments_acceptable:
   forall (s: signature) (p: rpair loc),
   In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
 Proof.
-  unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega.
+  unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. lia.
 Qed.
 
 Lemma loc_arguments_main:
@@ -390,8 +413,9 @@ Proof.
   reflexivity.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** No normalization needed. *)
 
 Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 4b309f5b..fe000976 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -209,8 +209,8 @@ Lemma operation_is_redundant_sound:
   vagree v arg1' nv.
 Proof.
   intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst.
-- apply sign_ext_redundant_sound; auto. omega.
-- apply sign_ext_redundant_sound; auto. omega.
+- apply sign_ext_redundant_sound; auto. lia.
+- apply sign_ext_redundant_sound; auto. lia.
 - apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 Qed.
diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v
index d0c6a526..25f02aab 100644
--- a/riscV/Stacklayout.v
+++ b/riscV/Stacklayout.v
@@ -68,15 +68,15 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
 (* Reorder as:
      outgoing
      back link
@@ -89,11 +89,11 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap45.
 (* Apply range_split and range_split2 repeatedly *)
   unfold fe_ofs_arg.
-  apply range_split_2. fold olink; omega. omega.
-  apply range_split. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol. omega. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_split_2. fold olink; lia. lia.
+  apply range_split. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol. lia. lia.
+  apply range_drop_right with ostkdata. lia.
   eapply sep_drop2. eexact H.
 Qed.
 
@@ -109,16 +109,16 @@ Proof.
   set (ocs := oretaddr + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
-  split. omega. apply align_le. omega. 
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
+  split. lia. apply align_le. lia. 
 Qed.
 
 Lemma frame_env_aligned:
@@ -137,11 +137,11 @@ Proof.
   set (ocs := oretaddr + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
   split. apply Z.divide_0_r.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl.
 Qed.
diff --git a/riscV/Asm.v b/riscV/TO_MERGE/Asm.v
index 5d3518f2..f75825a1 100644
--- a/riscV/Asm.v
+++ b/riscV/TO_MERGE/Asm.v
@@ -256,10 +256,17 @@ Inductive instruction : Type :=
 
   (* floating point register move *)
   | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
+<<<<<<< HEAD
   | 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*)
+=======
+  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
+  | Pfmvsx   (rd: freg) (rs: ireg)                  (**r move integer register to FP single *)
+  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
+  | Pfmvdx   (rd: freg) (rs: ireg)                  (**r move integer register to FP double *)
+>>>>>>> master
 
   (* 32-bit (single-precision) floating point *)
   | Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
@@ -987,6 +994,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       so we do not model them. *)
   | Pfence
 
+<<<<<<< HEAD
+=======
+  | Pfmvxs _ _
+  | Pfmvsx _ _
+  | Pfmvxd _ _
+  | Pfmvdx _ _
+
+>>>>>>> master
   | Pfmins _ _ _
   | Pfmaxs _ _ _
   | Pfsqrts _ _
@@ -1173,7 +1188,7 @@ Ltac Equalities :=
   split. auto. intros. destruct B; auto. subst. auto.
 - (* trace length *)
   red; intros. inv H; simpl.
-  omega.
+  lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 - (* initial states *)
diff --git a/riscV/Asmgenproof1.v b/riscV/TO_MERGE/Asmgenproof1.v
index f0def29b..1a8ce27d 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/TO_MERGE/Asmgenproof1.v
@@ -35,7 +35,7 @@ Proof.
 - set (m := Int.sub n lo).
   assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
   assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
-  { replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
+  { replace 0 with (Int.unsigned n - Int.unsigned n) by lia.
     auto using eqmod_sub, eqmod_refl. }
   assert (C: eqmod (two_p 12) (Int.unsigned m) 0).
   { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
@@ -45,7 +45,7 @@ Proof.
   { apply eqmod_mod_eq in C. unfold Int.modu. 
     change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. 
     reflexivity.
-    apply two_p_gt_ZERO; omega. }
+    apply two_p_gt_ZERO; lia. }
   rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto.
   rewrite Int.shl_mul_two_p. 
   change (two_p (Int.unsigned (Int.repr 12))) with 4096.
@@ -88,7 +88,7 @@ Proof.
   intros. apply ireg_of_not_X31 in H. congruence.
 Qed.
 
-Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen.
+Global Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen.
 
 (** Useful simplification tactic *)
 
@@ -432,6 +432,408 @@ Proof.
   intros; Simpl. 
 Qed.
 
+<<<<<<< HEAD
+=======
+(** Translation of condition operators *)
+
+Lemma transl_cond_int32s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
+  /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
+  simpl. rewrite (Val.negate_cmp_bool Clt). 
+  destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). 
+  destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_cond_int32u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
+  /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
+  simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_cond_int64s_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
+  simpl. rewrite (Val.negate_cmpl_bool Clt). 
+  destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). 
+  destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_cond_int64u_correct:
+  forall cmp rd r1 r2 k rs m,
+  exists rs',
+     exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
+  /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2)
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
+Proof.
+  intros. destruct cmp; simpl. 
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
+  simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
+- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
+  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
+- econstructor; split.
+  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
+  split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
+Qed.
+
+Lemma transl_condimm_int32s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int32s.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
+  exists rs'; eauto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ unfold xorimm32. 
+  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ unfold xorimm32. 
+  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
+* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. 
+  unfold Int.lt. rewrite zlt_false. auto. 
+  change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
+  generalize (Int.signed_range i); lia.
+* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto.
+  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
+  destruct (zlt (Int.signed n) (Int.signed i)).
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+  assert (Int.signed n <> Int.max_signed).
+  { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
+  generalize (Int.signed_range n); lia.
++ apply DFL.
++ apply DFL.
+Qed.
+
+Lemma transl_condimm_int32u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int32u.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto. rewrite B; auto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ apply DFL.
++ apply DFL.
++ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
+  intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ apply DFL.
++ apply DFL.
++ apply DFL.
+Qed.
+
+Lemma transl_condimm_int64s_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int64s.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
+  exists rs'; eauto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ unfold xorimm64. 
+  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ unfold xorimm64. 
+  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
+  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
+  exists rs2; split. 
+  eapply exec_straight_trans. eexact A1. eexact A2. 
+  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
+  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
+  intros; transitivity (rs1 r); auto.
++ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
+* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. 
+  unfold Int64.lt. rewrite zlt_false. auto. 
+  change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
+  generalize (Int64.signed_range i); lia.
+* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. 
+  rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto.
+  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
+  destruct (zlt (Int64.signed n) (Int64.signed i)).
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
+  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
+  assert (Int64.signed n <> Int64.max_signed).
+  { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
+  generalize (Int64.signed_range n); lia.
++ apply DFL.
++ apply DFL.
+Qed.
+
+Lemma transl_condimm_int64u_correct:
+  forall cmp rd r1 n k rs m,
+  r1 <> X31 ->
+  exists rs',
+     exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
+  /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  intros. unfold transl_condimm_int64u.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero.
+- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. split; auto. rewrite B; auto.
+- assert (DFL:
+    exists rs',
+      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m
+   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
+   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
+  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
+    exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
+    exists rs2; split. 
+    eapply exec_straight_trans. eexact A1. eexact A2. 
+    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
+    intros; transitivity (rs1 r); auto. }
+  destruct cmp.
++ apply DFL.
++ apply DFL.
++ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
+  intros (rs1 & A1 & B1 & C1).
+  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
++ apply DFL.
++ apply DFL.
++ apply DFL.
+Qed.
+
+Lemma transl_cond_op_correct:
+  forall cond rd args k c rs m,
+  transl_cond_op cond rd args k = OK c ->
+  exists rs',
+     exec_straight ge fn c rs m k rs' m
+  /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
+  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
+Proof.
+  assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)).
+  { destruct ob as [[]|]; reflexivity. }
+  intros until m; intros TR.
+  destruct cond; simpl in TR; ArgsInv.
++ (* cmp *)
+  exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
++ (* cmpu *)
+  exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite B; auto.
++ (* cmpimm *)
+  apply transl_condimm_int32s_correct; eauto with asmgen.
++ (* cmpuimm *)
+  apply transl_condimm_int32u_correct; eauto with asmgen.
++ (* cmpl *)
+  exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmplu *)
+  exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
++ (* cmplimm *)
+  exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. 
+  intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpluimm *)
+  exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. 
+  intros (rs' & A & B & C).
+  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
++ (* cmpf *)
+  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
+  fold (Val.cmpf c0 (rs x) (rs x0)).
+  set (v := Val.cmpf c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
+  split; intros; Simpl.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
++ (* notcmpf *)
+  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
+  rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
+  set (v := Val.cmpf c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_float_correct with (v := v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
+  split; intros; Simpl.
++ (* cmpfs *)
+  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
+  fold (Val.cmpfs c0 (rs x) (rs x0)).
+  set (v := Val.cmpfs c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
+  split; intros; Simpl.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
++ (* notcmpfs *)
+  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
+  rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
+  set (v := Val.cmpfs c0 (rs x) (rs x0)).
+  destruct normal; inv EQ2.
+* econstructor; split.
+  eapply exec_straight_two.
+  eapply transl_cond_single_correct with (v := v); eauto.
+  simpl; reflexivity.
+  auto. auto.
+  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+* econstructor; split.
+  apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
+  split; intros; Simpl.
+Qed.
+
+>>>>>>> master
 (** Some arithmetic properties. *)
 
 Remark cast32unsigned_from_cast32signed:
diff --git a/riscV/SelectLongproof.v b/riscV/TO_MERGE/SelectLongproof.v
index 0fc578bf..954dd134 100644
--- a/riscV/SelectLongproof.v
+++ b/riscV/TO_MERGE/SelectLongproof.v
@@ -506,9 +506,39 @@ Proof.
 - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
   change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
 - TrivialExists.
+<<<<<<< HEAD
   cbn.
   rewrite H0.
   reflexivity.
+=======
+(*
+  intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL.
++ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
++ destruct x; simpl in H0; try discriminate. 
+  destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  - subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto.
+  - assert (NZ: Int.unsigned n <> 0).
+    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
+    assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption).
+    assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true).
+    { unfold Int.ltu; apply zlt_true.
+      unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64. 
+      rewrite Int.unsigned_repr. lia. 
+      assert (64 < Int.max_unsigned) by reflexivity. lia. }
+    assert (X: eval_expr ge sp e m le
+               (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil))
+               (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))).
+    { EvalOp. }
+    assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n)
+               (Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))).
+    { EvalOp. simpl. rewrite LTU2. auto. }
+    TrivialExists. 
+    constructor. EvalOp. simpl; eauto. constructor. 
+    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity. 
+    change (Int.unsigned Int64.iwordsize') with 64; lia.
+*)
+>>>>>>> master
 Qed.
 
 Theorem eval_cmplu:
diff --git a/riscV/SelectOpproof.v b/riscV/TO_MERGE/SelectOpproof.v
index ce80fc57..9bd66213 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/TO_MERGE/SelectOpproof.v
@@ -370,20 +370,20 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
-  unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
-  assert (N1: 0 <= n < 64) by omega.
+  assert (N1: 0 <= n < 64) by lia.
   rewrite Int64.bits_loword by auto.
   rewrite Int64.bits_shr' by auto.
   change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
-  rewrite zlt_true by omega.
+  rewrite zlt_true by lia.
   rewrite Int.testbit_repr by auto. 
-  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia).
   transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)).
-  rewrite Z.shiftr_spec by omega. auto.
+  rewrite Z.shiftr_spec by lia. auto.
   apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
-  change Int64.zwordsize with 64; omega.
+  change Int64.zwordsize with 64; lia.
 - TrivialExists.
 Qed.
 
@@ -398,20 +398,20 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
-  unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
-  assert (N1: 0 <= n < 64) by omega.
+  assert (N1: 0 <= n < 64) by lia.
   rewrite Int64.bits_loword by auto.
   rewrite Int64.bits_shru' by auto.
   change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
-  rewrite zlt_true by omega.
+  rewrite zlt_true by lia.
   rewrite Int.testbit_repr by auto. 
-  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia).
   transitivity (Z.testbit (Int.unsigned i * Int.unsigned i0) (n + 32)).
-  rewrite Z.shiftr_spec by omega. auto.
+  rewrite Z.shiftr_spec by lia. auto.
   apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
-  change Int64.zwordsize with 64; omega.
+  change Int64.zwordsize with 64; lia.
 - TrivialExists.
 Qed.
 
@@ -574,12 +574,43 @@ Proof.
   replace (Int.shrx i Int.zero) with i. auto.
   unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+<<<<<<< HEAD
   econstructor; split. EvalOp.
   cbn.
   rewrite H0.
   cbn.
   reflexivity.
   apply Val.lessdef_refl.
+=======
+  econstructor; split. EvalOp. auto.
+(*
+  intros. destruct x; simpl in H0; try discriminate. 
+  destruct (Int.ltu n (Int.repr 31)) eqn:LTU; inv H0.
+  unfold shrximm.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  - subst n. exists (Vint i); split; auto.
+    unfold Int.shrx, Int.divs. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
+  - assert (NZ: Int.unsigned n <> 0).
+    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
+    assert (LT: 0 <= Int.unsigned n < 31) by (apply Int.ltu_inv in LTU; assumption).
+    assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
+    { unfold Int.ltu; apply zlt_true.
+      unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32. 
+      rewrite Int.unsigned_repr. lia. 
+      assert (32 < Int.max_unsigned) by reflexivity. lia. }
+    assert (X: eval_expr ge sp e m le
+               (Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil))
+               (Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))).
+    { EvalOp. }
+    assert (Y: eval_expr ge sp e m le (shrximm_inner a n)
+               (Vint (Int.shru (Int.shr i (Int.repr (Int.zwordsize - 1))) (Int.sub Int.iwordsize n)))).
+    { EvalOp. simpl. rewrite LTU2. auto. }
+    TrivialExists. 
+    constructor. EvalOp. simpl; eauto. constructor. 
+    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity. 
+    change (Int.unsigned Int.iwordsize) with 32; lia.
+*)
+>>>>>>> master
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
@@ -766,7 +797,7 @@ Qed.
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
 Proof.
   red; intros until x. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm. omega.
+  rewrite Val.zero_ext_and. apply eval_andimm. lia.
 Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
@@ -779,7 +810,7 @@ Qed.
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
 Proof.
   red; intros until x. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm. omega.
+  rewrite Val.zero_ext_and. apply eval_andimm. lia.
 Qed.
 
 Theorem eval_intoffloat:
diff --git a/riscV/TargetPrinter.ml b/riscV/TO_MERGE/TargetPrinter.ml
index 1f00c440..23fbeb8b 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TO_MERGE/TargetPrinter.ml
@@ -107,12 +107,17 @@ module Target : TARGET =
 
     let name_of_section = function
       | Section_text         -> ".text"
+<<<<<<< HEAD
       | Section_data(i, true) ->
          failwith "_Thread_local unsupported on this platform"
       | Section_data(i, false) | Section_small_data i ->
           if i then ".data" else common_section ()
+=======
+      | Section_data i | Section_small_data i ->
+          variable_section ~sec:".data" ~bss:".bss" i
+>>>>>>> master
       | Section_const i | Section_small_const i ->
-          if i || (not !Clflags.option_fcommon) then ".section	.rodata" else "COMM"
+          variable_section ~sec:".section	.rodata" i
       | Section_string       -> ".section	.rodata"
       | Section_literal      -> ".section	.rodata"
       | Section_jumptable    -> ".section	.rodata"
@@ -394,10 +399,15 @@ module Target : TARGET =
          fprintf oc "	fmv.d	%a, %a\n"     freg fd freg fs
       | Pfmvxs (rd,fs) ->
          fprintf oc "	fmv.x.s	%a, %a\n"     ireg rd freg fs
+      | Pfmvsx (fd,rs) ->
+         fprintf oc "	fmv.s.x	%a, %a\n"     freg fd ireg rs
       | Pfmvxd (rd,fs) ->
          fprintf oc "	fmv.x.d	%a, %a\n"     ireg rd freg fs
+<<<<<<< HEAD
       | Pfmvsx (fd,rs) ->
          fprintf oc "	fmv.s.x	%a, %a\n"     freg fd ireg rs
+=======
+>>>>>>> master
       | Pfmvdx (fd,rs) ->
          fprintf oc "	fmv.d.x	%a, %a\n"     freg fd ireg rs