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, 107 insertions, 109 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index d9901960..93bc31b8 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -1276,7 +1276,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/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index cb6a659f..df712b9d 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -388,8 +388,9 @@ let rec next_arg_locations ir fr ofs = function
       then next_arg_locations ir (fr + 1) ofs l
       else next_arg_locations ir fr (align ofs 8 + 8) l
   | Tlong :: l ->
-      if ir < 7
-      then next_arg_locations (align ir 2 + 2) fr ofs l
+      let ir = align ir 2 in
+      if ir < 8
+      then next_arg_locations (ir + 2) fr ofs l
       else next_arg_locations ir fr (align ofs 8 + 8) l
 
 let expand_builtin_va_start r =
@@ -830,7 +831,7 @@ let expand_builtin_inline name args res =
    function is unprototyped. *)
 
 let set_cr6 sg =
-  if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin
+  if (sg.sig_cc.cc_vararg <> None) || sg.sig_cc.cc_unproto then begin
     if List.exists (function Tfloat | Tsingle -> true | _ -> false) sg.sig_args
     then emit (Pcreqv(CRbit_6, CRbit_6, CRbit_6))
     else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6))
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 93589a31..2fab6d57 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -69,7 +69,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:
@@ -402,8 +402,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.
 
@@ -934,14 +934,14 @@ Local Transparent destroyed_by_jumptable.
   simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence.
   auto. auto. auto.
   left; exists (State rs5 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor.
+  eapply exec_straight_steps_1; eauto. lia. constructor.
   econstructor; eauto.
   change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one).
   rewrite ATPC. simpl. constructor; eauto.
-  eapply code_tail_next_int. omega.
-  eapply code_tail_next_int. omega.
-  eapply code_tail_next_int. omega.
-  eapply code_tail_next_int. omega.
+  eapply code_tail_next_int. lia.
+  eapply code_tail_next_int. lia.
+  eapply code_tail_next_int. lia.
+  eapply code_tail_next_int. lia.
   constructor.
   unfold rs5, rs4, rs3, rs2.
   apply agree_nextinstr. apply agree_nextinstr.
@@ -966,7 +966,7 @@ Local Transparent destroyed_by_jumptable.
 
 - (* return *)
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto.
   congruence.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 850e95c7..9f928ff8 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -81,12 +81,12 @@ Proof.
     unfold Int.modu, Int.zero. decEq.
     change 0 with (0 mod 65536).
     change (Int.unsigned (Int.repr 65536)) with 65536.
-    apply eqmod_mod_eq. omega.
+    apply eqmod_mod_eq. lia.
     unfold x, low_s. eapply eqmod_trans.
     apply  eqmod_divides with Int.modulus.
     unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
     exists 65536. compute; auto.
-    replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
+    replace 0 with (Int.unsigned n - Int.unsigned n) by lia.
     apply eqmod_sub. apply eqmod_refl. apply Int.eqmod_sign_ext'.
     compute; auto.
   rewrite H0 in H. rewrite Int.add_zero in H.
@@ -132,7 +132,7 @@ Lemma important_diff:
 Proof.
   congruence.
 Qed.
-Hint Resolve important_diff: asmgen.
+Global Hint Resolve important_diff: asmgen.
 
 Lemma important_data_preg_1:
   forall r, data_preg r = true -> important_preg r = true.    
@@ -146,7 +146,7 @@ Proof.
   intros. destruct (data_preg r) eqn:E; auto. apply important_data_preg_1 in E. congruence.
 Qed.  
 
-Hint Resolve important_data_preg_1 important_data_preg_2: asmgen.
+Global Hint Resolve important_data_preg_1 important_data_preg_2: asmgen.
 
 Lemma nextinstr_inv2:
   forall r rs, important_preg r = true -> (nextinstr rs)#r = rs#r.
@@ -166,7 +166,7 @@ Lemma gpr_or_zero_zero:
 Proof.
   intros. reflexivity.
 Qed.
-Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen.
+Global Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen.
 
 Lemma gpr_or_zero_l_not_zero:
   forall rs r, r <> GPR0 -> gpr_or_zero_l rs r = rs#r.
@@ -178,21 +178,21 @@ Lemma gpr_or_zero_l_zero:
 Proof.
   intros. reflexivity.
 Qed.
-Hint Resolve gpr_or_zero_l_not_zero gpr_or_zero_l_zero: asmgen.
+Global Hint Resolve gpr_or_zero_l_not_zero gpr_or_zero_l_zero: asmgen.
 
 Lemma ireg_of_not_GPR0:
   forall m r, ireg_of m = OK r -> IR r <> IR GPR0.
 Proof.
   intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
-Hint Resolve ireg_of_not_GPR0: asmgen.
+Global Hint Resolve ireg_of_not_GPR0: asmgen.
 
 Lemma ireg_of_not_GPR0':
   forall m r, ireg_of m = OK r -> r <> GPR0.
 Proof.
   intros. generalize (ireg_of_not_GPR0 _ _ H). congruence.
 Qed.
-Hint Resolve ireg_of_not_GPR0': asmgen.
+Global Hint Resolve ireg_of_not_GPR0': asmgen.
 
 (** Useful properties of the LR register *)
 
@@ -208,7 +208,7 @@ Proof.
   intros. rewrite preg_notin_charact. intros. apply preg_of_not_LR. 
 Qed.
 
-Hint Resolve preg_of_not_LR preg_notin_LR: asmgen.
+Global Hint Resolve preg_of_not_LR preg_notin_LR: asmgen.
       
 (** Useful simplification tactic *)
 
@@ -543,7 +543,7 @@ Proof.
   - econstructor; split; [|split].
     + apply exec_straight_one. simpl; eauto. auto.
     + Simpl. rewrite Int64.add_zero_l. rewrite H. unfold low64_s.
-      rewrite Int64.sign_ext_widen by omega. auto.
+      rewrite Int64.sign_ext_widen by lia. auto.
     + intros; Simpl.
   - econstructor; split; [|split].
     + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
@@ -551,16 +551,16 @@ Proof.
       apply Int64.same_bits_eq; intros.  assert (Int64.zwordsize = 64) by auto.
       rewrite Int64.bits_or, Int64.bits_shl by auto.
       unfold low64_s, low64_u.
-      rewrite Int64.bits_zero_ext by omega.
+      rewrite Int64.bits_zero_ext by lia.
       change (Int64.unsigned (Int64.repr 16)) with 16.
       destruct (zlt i 16).
-      * rewrite Int64.bits_sign_ext by omega. rewrite zlt_true by omega. auto.
-      * rewrite ! Int64.bits_sign_ext by omega. rewrite orb_false_r.
+      * rewrite Int64.bits_sign_ext by lia. rewrite zlt_true by lia. auto.
+      * rewrite ! Int64.bits_sign_ext by lia. rewrite orb_false_r.
         destruct (zlt i 32).
-        ** rewrite zlt_true by omega. rewrite Int64.bits_shr by omega.
+        ** rewrite zlt_true by lia. rewrite Int64.bits_shr by lia.
            change (Int64.unsigned (Int64.repr 16)) with 16.
-           rewrite zlt_true by omega. f_equal; omega.
-        ** rewrite zlt_false by omega. rewrite Int64.bits_shr by omega.
+           rewrite zlt_true by lia. f_equal; lia.
+        ** rewrite zlt_false by lia. rewrite Int64.bits_shr by lia.
            change (Int64.unsigned (Int64.repr 16)) with 16.
            reflexivity.
     + intros; Simpl.
@@ -605,11 +605,11 @@ Proof.
     rewrite Int64.bits_shl by auto.
     change (Int64.unsigned (Int64.repr 32)) with 32.
     destruct (zlt i 32); auto.
-    rewrite Int64.bits_sign_ext by omega.
-    rewrite zlt_true by omega.
-    unfold n2. rewrite Int64.bits_shru by omega.
+    rewrite Int64.bits_sign_ext by lia.
+    rewrite zlt_true by lia.
+    unfold n2. rewrite Int64.bits_shru by lia.
     change (Int64.unsigned (Int64.repr 32)) with 32.
-    rewrite zlt_true by omega. f_equal; omega.
+    rewrite zlt_true by lia. f_equal; lia.
   }
   assert (MI: forall i, 0 <= i < Int64.zwordsize ->
               Int64.testbit mi i =
@@ -619,21 +619,21 @@ Proof.
     rewrite Int64.bits_shl by auto.
     change (Int64.unsigned (Int64.repr 16)) with 16.
     destruct (zlt i 16); auto.
-    unfold n1. rewrite Int64.bits_zero_ext by omega.
-    rewrite Int64.bits_shru by omega.
+    unfold n1. rewrite Int64.bits_zero_ext by lia.
+    rewrite Int64.bits_shru by lia.
     destruct (zlt i 32).
-    rewrite zlt_true by omega.
+    rewrite zlt_true by lia.
     change (Int64.unsigned (Int64.repr 16)) with 16.
-    rewrite zlt_true by omega. f_equal; omega.
-    rewrite zlt_false by omega. auto.
+    rewrite zlt_true by lia. f_equal; lia.
+    rewrite zlt_false by lia. auto.
   }
   assert (EQ: Int64.or (Int64.or hi mi) n0 = n).
   { apply Int64.same_bits_eq; intros.
     rewrite ! Int64.bits_or by auto.
-    unfold n0; rewrite Int64.bits_zero_ext by omega.
+    unfold n0; rewrite Int64.bits_zero_ext by lia.
     rewrite HI, MI by auto.
     destruct (zlt i 16).
-    rewrite zlt_true by omega. auto.
+    rewrite zlt_true by lia. auto.
     destruct (zlt i 32); rewrite ! orb_false_r; auto.
   }
   edestruct (loadimm64_32s_correct r n2) as (rs' & A & B & C).
@@ -1180,7 +1180,7 @@ Local Transparent Int.repr.
    rewrite H2. apply Int.mkint_eq; reflexivity.
   rewrite Int.not_involutive in H3.
   congruence.
-  omega.
+  lia.
 Qed.
 
 Remark add_carry_ne0:
@@ -1198,8 +1198,8 @@ Transparent Int.eq.
   rewrite Int.unsigned_zero.  rewrite Int.unsigned_mone.
   unfold negb, Val.of_bool, Vtrue, Vfalse.
   destruct (zeq (Int.unsigned i) 0); decEq.
-  apply zlt_true. omega.
-  apply zlt_false. generalize (Int.unsigned_range i). omega.
+  apply zlt_true. lia.
+  apply zlt_false. generalize (Int.unsigned_range i). lia.
 Qed.
 
 Lemma transl_cond_op_correct:
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 8687b056..1dd2e0e4 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -374,7 +374,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/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 5c9cbd4f..f05e77df 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -268,7 +268,7 @@ Remark loc_arguments_rec_charact:
   forall_rpair (loc_argument_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. }
   assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p).
   { destruct p; simpl; intuition eauto. }
 Opaque list_nth_z.
@@ -279,52 +279,52 @@ Opaque list_nth_z.
   destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
   subst. left. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  subst. split. omega. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. split. lia. apply Z.divide_1_l.
+  eapply Y; eauto. lia.
 - (* float *)
-  assert (ofs <= align ofs 2) by (apply align_le; omega).
+  assert (ofs <= align ofs 2) by (apply align_le; lia).
   destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  subst. split. omega. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. split. lia. apply Z.divide_1_l.
+  eapply Y; eauto. lia.
 - (* long *)
-  assert (ofs <= align ofs 2) by (apply align_le; omega).
+  assert (ofs <= align ofs 2) by (apply align_le; lia).
   set (ir' := align ir 2) in *.
   destruct (list_nth_z int_param_regs ir') as [r1|] eqn:E1.
   destruct (list_nth_z int_param_regs (ir' + 1)) as [r2|] eqn:E2.
   destruct H. subst; split; left; eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
   destruct H.
-  subst. destruct Archi.ptr64; [split|split;split]; try omega.
-  apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. destruct Archi.ptr64; [split|split;split]; try lia.
+  apply align_divides; lia. apply Z.divide_1_l. apply Z.divide_1_l.
+  eapply Y; eauto. lia.
   destruct H.
-  subst. destruct Archi.ptr64; [split|split;split]; try omega.
-  apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. destruct Archi.ptr64; [split|split;split]; try lia.
+  apply align_divides; lia. apply Z.divide_1_l. apply Z.divide_1_l.
+  eapply Y; eauto. lia.
 - (* single *)
-  assert (ofs <= align ofs 1) by (apply align_le; omega).
-  assert (ofs <= align ofs 2) by (apply align_le; omega).
+  assert (ofs <= align ofs 1) by (apply align_le; lia).
+  assert (ofs <= align ofs 2) by (apply align_le; lia).
   destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  subst. split. destruct Archi.single_passed_as_single; simpl; omega.
+  subst. split. destruct Archi.single_passed_as_single; simpl; lia.
   destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l.
-  eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega.
+  eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; lia.
 - (* any32 *)
   destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
   subst. left. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  subst. split. omega. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. split. lia. apply Z.divide_1_l.
+  eapply Y; eauto. lia.
 - (* float *)
-  assert (ofs <= align ofs 2) by (apply align_le; omega).
+  assert (ofs <= align ofs 2) by (apply align_le; lia).
   destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  subst. split. omega. apply Z.divide_1_l.
-  eapply Y; eauto. omega.
+  subst. split. lia. apply Z.divide_1_l.
+  eapply Y; eauto. lia.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -341,7 +341,7 @@ Proof.
   unfold forall_rpair; destruct p; intuition auto.
 Qed.
 
-Hint Resolve loc_arguments_acceptable: locs.
+Global Hint Resolve loc_arguments_acceptable: locs.
 
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
@@ -349,8 +349,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/powerpc/NeedOp.v b/powerpc/NeedOp.v
index 74ee6b85..85dd9b2e 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -162,8 +162,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.
 - apply rolm_redundant_sound; auto.
diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v
index eba071eb..2264451d 100644
--- a/powerpc/SelectLongproof.v
+++ b/powerpc/SelectLongproof.v
@@ -222,15 +222,15 @@ Proof.
   change (Int64.unsigned Int64.iwordsize) with 64.
   f_equal.
   rewrite Int.unsigned_repr. 
-  apply eqmod_mod_eq. omega. 
+  apply eqmod_mod_eq. lia. 
   apply eqmod_trans with a.
   apply eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
   exists (two_p (32-6)); auto.
   apply eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr.
   exists (two_p (64-6)); auto.
-  assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; omega).
+  assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; lia).
   assert (64 < Int.max_unsigned) by (compute; auto).
-  omega.
+  lia.
 - InvEval. TrivialExists. simpl. rewrite <- H.
   unfold Val.rolml; destruct v1; simpl; auto. unfold Int64.rolm.
   rewrite Int64.rol_and. rewrite Int64.and_assoc. auto.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index ed81c83f..edc935d4 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -809,7 +809,7 @@ Qed.
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
 Proof.
   red; intros. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm; auto. omega.
+  rewrite Val.zero_ext_and. apply eval_andimm; auto. lia.
 Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
@@ -822,7 +822,7 @@ Qed.
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
 Proof.
   red; intros. unfold cast16unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm; auto. omega.
+  rewrite Val.zero_ext_and. apply eval_andimm; auto. lia.
 Qed.
 
 Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
@@ -860,7 +860,7 @@ Proof.
   simpl; rewrite Heqo; simpl; eauto. constructor.
   simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto.
   assert (Int.modulus < Int64.max_unsigned) by (compute; auto).
-  generalize (Int.unsigned_range n). omega.  
+  generalize (Int.unsigned_range n). lia.  
 - set (im := Int.repr Int.half_modulus).
   set (fm := Float.of_intu im).
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v
index cb3806bd..32b11ad5 100644
--- a/powerpc/Stacklayout.v
+++ b/powerpc/Stacklayout.v
@@ -77,11 +77,11 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ostkdata := align oendcs 8).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
   unfold fe_ofs_arg.
-  assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; omega).
-  assert (ol <= ora) by (unfold ora; omega).
-  assert (ora <= ocs) by (unfold ocs; omega).
+  assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; lia).
+  assert (ol <= ora) by (unfold ora; lia).
+  assert (ora <= ocs) by (unfold ocs; lia).
   assert (ocs <= oendcs) by (apply size_callee_save_area_incr).
-  assert (oendcs <= ostkdata) by (apply align_le; omega).
+  assert (oendcs <= ostkdata) by (apply align_le; lia).
 (* Reorder as:
      back link
      outgoing
@@ -90,12 +90,12 @@ Local Opaque Z.add Z.mul sepconj range.
      callee-save *)
   rewrite sep_swap3.
 (* Apply range_split and range_split2 repeatedly *)
-  apply range_drop_right with 8. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol; omega. omega.
-  apply range_split. omega.
-  apply range_split. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_drop_right with 8. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol; lia. lia.
+  apply range_split. lia.
+  apply range_split. lia.
+  apply range_drop_right with ostkdata. lia.
   eapply sep_drop2. eexact H.
 Qed.
 
@@ -112,12 +112,12 @@ Proof.
   set (ostkdata := align oendcs 8).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
   unfold fe_ofs_arg.
-  assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; omega).
-  assert (ol <= ora) by (unfold ora; omega).
-  assert (ora <= ocs) by (unfold ocs; omega).
+  assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; lia).
+  assert (ol <= ora) by (unfold ora; lia).
+  assert (ora <= ocs) by (unfold ocs; lia).
   assert (ocs <= oendcs) by (apply size_callee_save_area_incr).
-  assert (oendcs <= ostkdata) by (apply align_le; omega).
-  split. omega. apply align_le. omega.
+  assert (oendcs <= ostkdata) by (apply align_le; lia).
+  split. lia. apply align_le. lia.
 Qed.
 
 Lemma frame_env_aligned:
@@ -136,10 +136,10 @@ Proof.
   set (oendcs := size_callee_save_area b ocs).
   set (ostkdata := align oendcs 8).
   split. exists (fe_ofs_arg / 8); reflexivity.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
   split. apply Z.divide_0_r.
   apply Z.divide_add_r.
-    apply Z.divide_trans with 8. exists 2; auto. apply align_divides; omega.
+    apply Z.divide_trans with 8. exists 2; auto. apply align_divides; lia.
     apply Z.divide_factor_l.
 Qed.
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 554bfe09..a82fa5d9 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -120,22 +120,16 @@ module Linux_System : SYSTEM =
       | Section_data(i, true) ->
          failwith "_Thread_local unsupported on this platform"
       | Section_data(i, false) ->
-          if i then
-            ".data"
-          else
-            common_section ~sec:".section	.bss" ()
+          variable_section ~sec:".data" ~bss:".section	.bss" i
       | Section_small_data i ->
-          if i then
-            ".section	.sdata,\"aw\",@progbits"
-          else
-            common_section ~sec:".section	.sbss,\"aw\",@nobits" ()
+          variable_section
+            ~sec:".section	.sdata,\"aw\",@progbits"
+            ~bss:".section	.sbss,\"aw\",@nobits"
+            i
       | Section_const i ->
-          if i || (not !Clflags.option_fcommon) then ".rodata" else "COMM"
+          variable_section ~sec:".rodata" i
       | Section_small_const i ->
-          if i || (not !Clflags.option_fcommon) then
-            ".section	.sdata2,\"a\",@progbits"
-          else
-            "COMM"
+          variable_section ~sec:".section	.sdata2,\"a\",@progbits" i
       | Section_string -> ".rodata"
       | Section_literal -> ".section	.rodata.cst8,\"aM\",@progbits,8"
       | Section_jumptable -> ".text"
@@ -222,8 +216,10 @@ module Diab_System : SYSTEM =
       | Section_text -> ".text"
       | Section_data(i, true) ->
          failwith "_Thread_local unsupported on this platform"
-      | Section_data (i, false) -> if i then ".data" else common_section ()
-      | Section_small_data i -> if i then ".sdata" else ".sbss"
+      | Section_data (i, false) ->
+          variable_section ~sec:".data" ~bss:".bss" i
+      | Section_small_data i ->
+          variable_section ~sec:".sdata" ~bss:".sbss" ~common:false i
       | Section_const _ -> ".text"
       | Section_small_const _ -> ".sdata2"
       | Section_string -> ".text"