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

1 files changed, 29 insertions, 16 deletions

diff --git a/kvx/Conventions1.v b/kvx/Conventions1.v
index 0b2cf406..d8eff34e 100644
--- a/kvx/Conventions1.v
+++ b/kvx/Conventions1.v
@@ -240,11 +240,18 @@ Fixpoint loc_arguments_rec (va: bool)
 *)
   end.
 
+(* FIX Sylvain: not sure to understand what I have done... *)
+Definition has_va (s: signature) : bool :=
+  match s.(sig_cc).(cc_vararg) with
+  | Some n => true
+  | None => false
+  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.
+  loc_arguments_rec (has_va s) s.(sig_args) 0 0.
 
 (** [size_arguments s] returns the number of [Outgoing] slots used
   to call a function with signature [s]. *)
@@ -287,11 +294,11 @@ Proof.
   assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0).
   { intros. 
     assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos).
-    omega. }
+    lia. }
   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 regs rn ofs ty f,
              OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)).
   { intros until f; intros OR OF OO; red; unfold one_arg; intros.
@@ -300,7 +307,7 @@ Proof.
   - eapply OF; eauto. 
   - subst p; cbn. 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 regs rn ofs f,
              OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)).
@@ -312,8 +319,8 @@ Proof.
                      :: f rn' (ofs' + 2))).
     { red; cbn; intros. destruct H.
     - subst p; cbn. 
-      repeat split; auto using Z.divide_1_l. omega.
-    - eapply OF; [idtac|eauto]. omega.
+      repeat split; auto using Z.divide_1_l. lia.
+    - eapply OF; [idtac|eauto]. lia.
     }
     destruct (list_nth_z regs rn') as [r1|] eqn:NTH1;
     destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2;
@@ -330,7 +337,7 @@ Proof.
   - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. 
   - eapply OF; eauto. 
   - subst p; cbn. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. 
-  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; omega.
+  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; lia.
   }
   assert (D: OKREGS param_regs).
   { red. decide_goal. }
@@ -359,7 +366,7 @@ 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.
 
 (** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
@@ -368,9 +375,9 @@ Remark fold_max_outgoing_above:
   forall l n, fold_left max_outgoing_2 l n >= n.
 Proof.
   assert (A: forall n l, max_outgoing_1 n l >= n).
-  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+  { intros; unfold max_outgoing_1. destruct l as [_ | []]; lia. }
   induction l; cbn; intros. 
-  - omega.
+  - lia.
   - eapply Zge_trans. eauto.
     destruct a; cbn. apply A. eapply Zge_trans; eauto.
 Qed.
@@ -388,14 +395,14 @@ Lemma loc_arguments_bounded:
 Proof.
   intros until ty.
   assert (A: forall n l, n <= max_outgoing_1 n l).
-  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+  { intros; unfold max_outgoing_1. destruct l as [_ | []]; lia. }
   assert (B: forall p n,
              In (S Outgoing ofs ty) (regs_of_rpair p) ->
              ofs + typesize ty <= max_outgoing_2 n p).
   { intros. destruct p; cbn in H; intuition; subst; cbn.
-  - xomega.
-  - eapply Z.le_trans. 2: apply A. xomega.
-  - xomega. }
+  - lia.
+  - eapply Z.le_trans. 2: apply A. lia.
+  - lia. }
   assert (C: forall l n,
              In (S Outgoing ofs ty) (regs_of_rpairs l) ->
              ofs + typesize ty <= fold_left max_outgoing_2 l n).
@@ -415,4 +422,10 @@ Proof.
 Qed.
 
 
-Definition return_value_needs_normalization (t: rettype) : bool := false.
+(** ** Normalization of function results and parameters *)
+
+(** No normalization needed. *)
+
+Definition return_value_needs_normalization (t: rettype): bool := false.
+Definition parameter_needs_normalization (t: rettype): bool := false.
+