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

3 files changed, 38 insertions, 23 deletions

diff --git a/kvx/Asmexpand.ml b/kvx/Asmexpand.ml
index 1e76a355..35c980bb 100644
--- a/kvx/Asmexpand.ml
+++ b/kvx/Asmexpand.ml
@@ -103,7 +103,7 @@ let fixup_variadic_call pos tyl = assert false
 *)
         
 let fixup_call sg =
-  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args
+  if sg.sig_cc.cc_vararg <> None then fixup_variadic_call 0 sg.sig_args
 
 (* Handling of annotations *)
 
@@ -501,7 +501,7 @@ let expand_instruction instr =
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (Asmvliw.GPR17, stack_pointer));
-      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 >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
@@ -524,7 +524,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 >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize)
       end else 0 in
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.
+
diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml
index 5b6230ca..9e2e3776 100644
--- a/kvx/TargetPrinter.ml
+++ b/kvx/TargetPrinter.ml
@@ -201,14 +201,16 @@ module Target (*: TARGET*) =
 
     let name_of_section = function
       | Section_text         -> ".text"
-      | Section_data(true, true) ->
+      | Section_data(Init, true) ->
          ".section .tdata,\"awT\",@progbits"
-      | Section_data(false, true) ->        
+      | Section_data(Uninit, true) ->        
          ".section .tbss,\"awT\",@nobits"
+      | Section_data(Init_reloc, true) ->
+         failwith "Sylvain does not how to fix this"
       | Section_data(i, false) | Section_small_data(i) ->
-         (if i then ".data" else "COMM")
+         variable_section ~sec:".data" ~bss:".bss" i
       | Section_const i | Section_small_const i ->
-          if i then ".section	.rodata" else "COMM"
+         variable_section ~sec:".section       .rodata" i
       | Section_string       -> ".section	.rodata"
       | Section_literal      -> ".section	.rodata"
       | Section_jumptable    -> ".section	.rodata"