fix aarch64 merge?

6 files changed, 17 insertions, 846 deletions

diff --git a/aarch64/TO_MERGE/Archi.v b/aarch64/Archi.v
index eb022db9..b47ce91f 100644
--- a/aarch64/TO_MERGE/Archi.v
+++ b/aarch64/Archi.v
@@ -87,14 +87,12 @@ Global Opaque ptr64 big_endian splitlong
 
 (** Which ABI to implement *)
 
-<<<<<<< HEAD
 Parameter pic_code: unit -> bool.
 
 Definition has_notrap_loads := false.
-=======
+
 Inductive abi_kind: Type :=
   | AAPCS64 (**r ARM's standard as used in Linux and other ELF platforms *)
   | Apple.  (**r the variant used in macOS and iOS *)
 
 Parameter abi: abi_kind.
->>>>>>> master
diff --git a/aarch64/TO_MERGE/Asmgen.v b/aarch64/Asmgen.v
index c8e48b40..6bb791c4 100644
--- a/aarch64/TO_MERGE/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -17,121 +17,8 @@
 
 Require Import Recdef Coqlib Zwf Zbits.
 Require Import Errors AST Integers Floats Op.
-<<<<<<< HEAD
 Require Import Locations Compopts.
 Require Import Mach Asm Asmblock Asmblockgen Machblockgen PostpassScheduling.
-=======
-Require Import Locations Mach Asm.
-Require SelectOp.
-
-Local Open Scope string_scope.
-Local Open Scope list_scope.
-Local Open Scope error_monad_scope.
-
-(** Alignment check for symbols *)
-
-Parameter symbol_is_aligned : ident -> Z -> bool.
-(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
-
-(** Extracting integer or float registers. *)
-
-Definition ireg_of (r: mreg) : res ireg :=
-  match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end.
-
-Definition freg_of (r: mreg) : res freg :=
-  match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end.
-
-(** Recognition of immediate arguments for logical integer operations.*)
-
-(** Valid immediate arguments are repetitions of a bit pattern [B]
-  of length [e] = 2, 4, 8, 16, 32 or 64.
-  The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*]
-  but must not be all zeros or all ones. *)
-
-(** The following automaton recognizes [0*1*0*|1*0*1*].
-<<
-               0          1          0
-              / \        / \        / \
-              \ /        \ /        \ /
-        -0--> [B] --1--> [D] --0--> [F]
-       /
-     [A]
-       \
-        -1--> [C] --0--> [E] --1--> [G]
-              / \        / \        / \
-              \ /        \ /        \ /
-               1          0          1
->>
-*)
-
-Module Automaton.
-
-Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad.
-
-Definition start := SA.
-
-Definition next (s: state) (b: bool) :=
-  match s, b with
-    | SA,false => SB      | SA,true => SC
-    | SB,false => SB      | SB,true => SD
-    | SC,false => SE      | SC,true => SC
-    | SD,false => SF      | SD,true => SD
-    | SE,false => SE      | SE,true => SG
-    | SF,false => SF      | SF,true => Sbad
-    | SG,false => Sbad    | SG,true => SG
-    | Sbad,_ => Sbad
-  end.
-
-Definition accepting (s: state) :=
-  match s with
-  | SA | SB | SC | SD | SE | SF | SG => true
-  | Sbad => false
-  end.
-
-Fixpoint run (len: nat) (s: state) (x: Z) : bool :=
-  match len with
-  | Datatypes.O => accepting s
-  | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x)
-  end.
-
-End Automaton.
-
-(** The following function determines the candidate length [e],
-    ensuring that [x] is a repetition [BB...B] 
-    of a bit pattern [B] of length [e]. *)
-
-Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat :=
-  (** [test n] checks that the low [2n] bits of [x] are of the
-      form [BB], that is, two occurrences of the same [n] bits *)
-  let test (n: Z) : bool :=
-    Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in
-  (** If [test n] fails, we know that the candidate length [e] is
-      at least [2n].  Hence we test with decreasing values of [n]:
-      32, 16, 8, 4, 2. *)
-  if sixtyfour && negb (test 32) then 64%nat
-  else if negb (test 16) then 32%nat
-  else if negb (test 8) then 16%nat
-  else if negb (test 4) then 8%nat
-  else if negb (test 2) then 4%nat
-  else 2%nat.
-
-(** A valid logical immediate is 
-- neither [0] nor [-1];
-- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e]
-- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*].
-*)
-
-Definition is_logical_imm32 (x: int) : bool :=
-  negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) &&
-  Automaton.run (logical_imm_length (Int.unsigned x) false)
-                Automaton.start (Int.unsigned x).
-
-Definition is_logical_imm64 (x: int64) : bool :=
-  negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) &&
-  Automaton.run (logical_imm_length (Int64.unsigned x) true)
-                Automaton.start (Int64.unsigned x).
->>>>>>> master
-
 
 Local Open Scope error_monad_scope.
 
@@ -194,86 +81,7 @@ Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code :=
   else if Int64.eq m (Int64.zero_ext 24 m) then
     addimm_aux (Asm.Psubimm X) rd r1 (Int64.unsigned m) k
   else if Int64.lt n Int64.zero then
-<<<<<<< HEAD
     loadimm64 X16 m (Asm.Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
-=======
-    loadimm64 X16 m (Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
-  else
-    loadimm64 X16 n (Paddext rd r1 X16 (EOuxtx Int.zero) :: k).
-
-(** Logical immediate *)
-
-Definition logicalimm32
-              (insn1: ireg -> ireg0 -> Z -> instruction)
-              (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
-              (rd r1: ireg) (n: int) (k: code) : code :=
-  if is_logical_imm32 n
-  then insn1 rd r1 (Int.unsigned n) :: k
-  else loadimm32 X16 n (insn2 rd r1 X16 SOnone :: k).
-
-Definition logicalimm64
-              (insn1: ireg -> ireg0 -> Z -> instruction)
-              (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
-              (rd r1: ireg) (n: int64) (k: code) : code :=
-  if is_logical_imm64 n
-  then insn1 rd r1 (Int64.unsigned n) :: k
-  else loadimm64 X16 n (insn2 rd r1 X16 SOnone :: k).
-
-(** Sign- or zero-extended arithmetic *)
-
-Definition transl_extension (ex: extension) (a: int) : extend_op :=
-  match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end.
-
-Definition move_extended_base
-              (rd: ireg) (r1: ireg) (ex: extension) (k: code) : code :=
-  match ex with
-  | Xsgn32 => Pcvtsw2x rd r1 :: k
-  | Xuns32 => Pcvtuw2x rd r1 :: k
-  end.
-
-Definition move_extended
-              (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: code) : code :=
-  if Int.eq a Int.zero then
-    move_extended_base rd r1 ex k
-  else
-    move_extended_base rd r1 ex (Padd X rd XZR rd (SOlsl a) :: k).
-
-Definition arith_extended 
-              (insnX: iregsp -> iregsp -> ireg -> extend_op -> instruction)
-              (insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction)
-              (rd r1 r2: ireg) (ex: extension) (a: int) (k: code) : code :=
-  if Int.ltu a (Int.repr 5) then
-    insnX rd r1 r2 (transl_extension ex a) :: k
-  else
-    move_extended_base X16 r2 ex (insnS rd r1 X16 (SOlsl a) :: k).
-
-(** Extended right shift *)
-
-Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code :=
-  if Int.eq n Int.zero then
-    Pmov rd r1 :: k
-  else
-    Porr W X16 XZR r1 (SOasr (Int.repr 31)) ::
-    Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) ::
-    Porr W rd XZR X16 (SOasr n) :: k.
-
-Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code :=
-  if Int.eq n Int.zero then
-    Pmov rd r1 :: k
-  else
-    Porr X X16 XZR r1 (SOasr (Int.repr 63)) ::
-    Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) ::
-    Porr X rd XZR X16 (SOasr n) :: k.
-
-(** Load the address [id + ofs] in [rd] *)
-
-Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code :=
-  if SelectOp.symbol_is_relocatable id then
-    if Ptrofs.eq ofs Ptrofs.zero then
-      Ploadsymbol rd id :: k
-    else
-      Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k
->>>>>>> master
   else
     loadimm64 X16 n (Asm.Paddext rd r1 X16 (EOuxtx Int.zero) :: k).
 
@@ -565,7 +373,6 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
   | Pnop                   => OK (Asm.Pnop)
   end.
 
-<<<<<<< HEAD
 Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction :=
   match cfi with
   | Pb l => Asm.Pb l
@@ -580,59 +387,6 @@ Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction
   | Ptbnz sz r n lbl => Asm.Ptbnz sz r n lbl
   | Ptbz sz r n lbl => Asm.Ptbz sz r n lbl
   | Pbtbl r1 tbl => Asm.Pbtbl r1 tbl
-=======
-(** Translation of addressing modes *)
-
-Definition offset_representable (sz: Z) (ofs: int64) : bool :=
-  let isz := Int64.repr sz in
-  (** either unscaled 9-bit signed *)
-  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
-  (** or scaled 12-bit unsigned *)
-  (Int64.eq (Int64.modu ofs isz) Int64.zero
-   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
- 
-Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
-                             (insn: Asm.addressing -> instruction) (k: code) : res code :=
-  match addr, args with
-  | Aindexed ofs, a1 :: nil =>
-      do r1 <- ireg_of a1;
-       if offset_representable sz ofs then
-        OK (insn (ADimm r1 ofs) :: k)
-      else
-        OK (loadimm64 X16 ofs (insn (ADreg r1 X16) :: k))
-  | Aindexed2, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (insn (ADreg r1 r2) :: k)
-  | Aindexed2shift a, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      if Int.eq a Int.zero then
-        OK (insn (ADreg r1 r2) :: k)
-      else if Int.eq (Int.shl Int.one a) (Int.repr sz) then
-        OK (insn (ADlsl r1 r2 a) :: k)
-      else
-        OK (Padd X X16 r1 r2 (SOlsl a) :: insn (ADimm X16 Int64.zero) :: k)
-  | Aindexed2ext x a, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then
-        OK (insn (match x with Xsgn32 => ADsxt r1 r2 a
-                             | Xuns32 => ADuxt r1 r2 a end) :: k)
-      else
-        OK (arith_extended Paddext (Padd X) X16 r1 r2 x a
-                           (insn (ADimm X16 Int64.zero) :: k))
-  | Aglobal id ofs, nil =>
-      assertion (negb (SelectOp.symbol_is_relocatable id));
-      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
-      then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k)
-      else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k))
-  | Ainstack ofs, nil =>
-      let ofs := Ptrofs.to_int64 ofs in
-      if offset_representable sz ofs then
-        OK (insn (ADimm XSP ofs) :: k)
-      else
-        OK (loadimm64 X16 ofs (insn (ADreg XSP X16) :: k))
-  | _, _ =>
-      Error(msg "Asmgen.transl_addressing")
->>>>>>> master
   end.
 
 Definition control_to_instruction (c: control) :=
diff --git a/aarch64/TO_MERGE/Asmgenproof.v b/aarch64/Asmgenproof.v
index 8af013fd..d27b3f8c 100644
--- a/aarch64/TO_MERGE/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -209,7 +209,6 @@ Definition max_pos (f : Asm.function) := list_length_z f.(Asm.fn_code).
 Lemma functions_bound_max_pos: forall fb f tf,
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   transf_function f = OK tf ->
-<<<<<<< HEAD
   max_pos tf <= Ptrofs.max_unsigned.
 Proof.
   intros fb f tf FINDf TRANSf.
@@ -223,66 +222,6 @@ Proof.
     assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. }
     rewrite H; lia.
 Qed.
-=======
-  Genv.find_funct_ptr tge fb = Some (Internal tf).
-Proof.
-  intros. exploit functions_translated; eauto. intros [tf' [A B]].
-  monadInv B. rewrite H0 in EQ; inv EQ; auto.
-Qed.
-
-(** * Properties of control flow *)
-
-Lemma transf_function_no_overflow:
-  forall f tf,
-  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.
-  lia.
-Qed.
-
-Lemma exec_straight_exec:
-  forall fb f c ep tf tc c' rs m rs' m',
-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
-  exec_straight tge tf tc rs m c' rs' m' ->
-  plus step tge (State rs m) E0 (State rs' m').
-Proof.
-  intros. inv H.
-  eapply exec_straight_steps_1; eauto.
-  eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto.
-Qed.
-
-Lemma exec_straight_at:
-  forall fb f c ep tf tc c' ep' tc' rs m rs' m',
-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
-  transl_code f c' ep' = OK tc' ->
-  exec_straight tge tf tc rs m tc' rs' m' ->
-  transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
-Proof.
-  intros. inv H.
-  exploit exec_straight_steps_2; eauto.
-  eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto.
-  intros [ofs' [PC' CT']].
-  rewrite PC'. constructor; auto.
-Qed.
-
-(** The following lemmas show that the translation from Mach to Asm
-  preserves labels, in the sense that the following diagram commutes:
-<<
-                          translation
-        Mach code ------------------------ Asm instr sequence
-            |                                          |
-            | Mach.find_label lbl       find_label lbl |
-            |                                          |
-            v                                          v
-        Mach code tail ------------------- Asm instr seq tail
-                          translation
->>
-  The proof demands many boring lemmas showing that Asm constructor
-  functions do not introduce new labels.
-*)
->>>>>>> master
 
 Lemma one_le_max_unsigned:
   1 <= Ptrofs.max_unsigned.
@@ -427,16 +366,9 @@ Lemma unfold_cdr bb bbs tc:
   unfold (bb :: bbs) = OK tc ->
   exists tc', unfold bbs = OK tc'.
 Proof.
-<<<<<<< HEAD
   intros; exploit unfold_car_cdr; eauto. intros (_ & ? & _ & ? & _).
   eexists; eauto.
 Qed.
-=======
-  intros; unfold loadsymbol.
-  destruct (SelectOp.symbol_is_relocatable id); TailNoLabel. destruct Ptrofs.eq; TailNoLabel.
-Qed. 
-Hint Resolve loadsymbol_label: labels.
->>>>>>> master
 
 Lemma unfold_car bb bbs tc:
   unfold (bb :: bbs) = OK tc ->
@@ -1182,7 +1114,6 @@ Proof.
   * eapply ptrofs_nextinstr_agree; eauto.
 Qed.
 
-<<<<<<< HEAD
 Lemma store_rs_a_preserved n rs1 m1 rs1' m1' rs2 m2 v chk a: forall
   (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
   (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
@@ -1201,33 +1132,6 @@ Proof.
     * eapply ptrofs_nextinstr_agree; subst; eauto.
   + next_stuck_cong.
 Qed.
-=======
-Lemma find_label_goto_label:
-  forall f tf lbl rs m c' b ofs,
-  Genv.find_funct_ptr ge b = Some (Internal f) ->
-  transf_function f = OK tf ->
-  rs PC = Vptr b ofs ->
-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  exists tc', exists rs',
-     goto_label tf lbl rs m = Next rs' m
-  /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc'
-  /\ forall r, r <> PC -> rs'#r = rs#r.
-Proof.
-  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2.
-  intros [tc [A B]].
-  exploit label_pos_code_tail; eauto. instantiate (1 := 0).
-  intros [pos' [P [Q R]]].
-  exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
-  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. lia.
-  generalize (transf_function_no_overflow _ _ H0). lia.
-  intros. apply Pregmap.gso; auto.
-Qed.
-
-(** Existence of return addresses *)
->>>>>>> master
 
 Lemma store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk1 chk2 a: forall
   (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
@@ -2141,7 +2045,6 @@ Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop :=
   | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl
   end.
 
-<<<<<<< HEAD
 Remark preg_notin_charact:
   forall r rl,
   preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr).
@@ -2153,378 +2056,6 @@ Proof.
   rewrite IHrl. split.
   intros [A B]. intros. destruct H. congruence. auto.
   auto.
-=======
-Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r.
-Proof.
-  intros. change (IR X29) with (preg_of R29). red; intros.
-  exploit preg_of_injective; eauto. intros; subst r; discriminate.
-Qed.
-
-Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP.
-Proof.
-  intros. eapply sp_val; eauto. 
-Qed. 
-
-(** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
-
-Theorem step_simulation:
-  forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
-  forall S1' (MS: match_states S1 S1'),
-  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
-  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
-Proof.
-  induction 1; intros; inv MS.
-
-- (* Mlabel *)
-  left; eapply exec_straight_steps; eauto; intros.
-  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. apply agree_nextinstr; auto. simpl; congruence.
-
-- (* Mgetstack *)
-  unfold load_stack in H.
-  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
-  rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
-  exists rs'; split. eauto.
-  split. eapply agree_set_mreg; eauto with asmgen. congruence.
-  simpl; congruence.
-
-- (* Msetstack *)
-  unfold store_stack in H.
-  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
-  exploit Mem.storev_extends; eauto. intros [m2' [A B]].
-  left; eapply exec_straight_steps; eauto.
-  rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
-  exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
-  exists rs'; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; intros. rewrite Q; auto with asmgen.
-
-- (* Mgetparam *)
-  assert (f0 = f) by congruence; subst f0.
-  unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H0. auto.
-  intros [parent' [A B]]. rewrite (sp_val' _ _ _ AG) in A.
-  exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto.
-  intros [v' [C D]].
-Opaque loadind.
-  left; eapply exec_straight_steps; eauto; intros. monadInv TR. 
-  destruct ep.
-(* X30 contains parent *)
-  exploit loadind_correct. eexact EQ.
-  instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence.
-  intros [rs1 [P [Q R]]].
-  exists rs1; split. eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
-  simpl; intros. rewrite R; auto with asmgen.
-  apply preg_of_not_X29; auto.
-(* X30 does not contain parent *)
-  exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]].
-  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence.
-  intros [rs2 [S [T U]]].
-  exists rs2; split. eapply exec_straight_trans; eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
-  instantiate (1 := rs1#X29 <- (rs2#X29)). intros.
-  rewrite Pregmap.gso; auto with asmgen.
-  congruence.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
-  simpl; intros. rewrite U; auto with asmgen.
-  apply preg_of_not_X29; auto.
-
-- (* Mop *)
-  assert (eval_operation tge sp op (map rs args) m = Some v).
-  { rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. }
-  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
-  intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
-  exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
-  exists rs2; split. eauto. split.
-  apply agree_set_undef_mreg with rs0; auto. 
-  apply Val.lessdef_trans with v'; auto.
-  simpl; intros. InvBooleans. 
-  rewrite R; auto. apply preg_of_not_X29; auto.
-Local Transparent destroyed_by_op.
-  destruct op; try exact I; simpl; congruence.
-
-- (* Mload *)
-  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
-  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
-  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
-  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
-  exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]].
-  exists rs2; split. eauto.
-  split. eapply agree_set_undef_mreg; eauto. congruence.
-  simpl; congruence.
-
-- (* Mstore *)
-  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
-  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
-  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
-  exploit Mem.storev_extends; eauto. intros [m2' [C D]].
-  left; eapply exec_straight_steps; eauto.
-  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]].
-  exists rs2; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; congruence.
-
-- (* Mcall *)
-  assert (f0 = f) by congruence.  subst f0.
-  inv AT.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-  { eapply transf_function_no_overflow; eauto. }
-  destruct ros as [rf|fid]; simpl in H; monadInv H5.
-+ (* Indirect call *)
-  assert (rs rf = Vptr f' Ptrofs.zero).
-  { destruct (rs rf); try discriminate.
-    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
-  assert (rs0 x0 = Vptr f' Ptrofs.zero).
-  { exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. }
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
-  {  econstructor; eauto. }
-  exploit return_address_offset_correct; eauto. intros; subst ra.
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
-  simpl. eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl.
-  Simpl. rewrite <- H2. auto.
-+ (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
-    econstructor; eauto.
-  exploit return_address_offset_correct; eauto. intros; subst ra.
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_internal. eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
-  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl.
-  Simpl. rewrite <- H2. auto.
-
-- (* Mtailcall *)
-  assert (f0 = f) by congruence.  subst f0.
-  inversion AT; subst.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-  { eapply transf_function_no_overflow; eauto. }
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
-  destruct ros as [rf|fid]; simpl in H; monadInv H7.
-+ (* Indirect call *)
-  assert (rs rf = Vptr f' Ptrofs.zero).
-  { destruct (rs rf); try discriminate.
-    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
-  assert (rs0 x0 = Vptr f' Ptrofs.zero).
-  { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. }
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-  Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. 
-+ (* Direct call *)
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-  Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
-
-- (* Mbuiltin *)
-  inv AT. monadInv H4.
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
-  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2' [A [B [C D]]]]].
-  left. econstructor; split. apply plus_one.
-  eapply exec_step_builtin. eauto. eauto.
-  eapply find_instr_tail; eauto.
-  erewrite <- sp_val by eauto.
-  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  eauto.
-  econstructor; eauto.
-  instantiate (2 := tf); instantiate (1 := x).
-  unfold nextinstr. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other.
-  rewrite <- H1. simpl. econstructor; eauto.
-  eapply code_tail_next_int; eauto.
-  simpl; intros. destruct H4. congruence. destruct H4. congruence.
-  exploit list_in_map_inv; eauto. intros (mr & U & V). subst.
-  auto with asmgen.
-  auto with asmgen.
-  apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros.
-  simpl. rewrite undef_regs_other_2; auto. Simpl.
-  congruence.
-
-- (* Mgoto *)
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H4.
-  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
-  left; exists (State rs' m'); split.
-  apply plus_one. econstructor; eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail; eauto.
-  simpl; eauto.
-  econstructor; eauto.
-  eapply agree_exten; eauto with asmgen.
-  congruence.
-
-- (* Mcond true *)
-  assert (f0 = f) by congruence. subst f0.
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_opt_steps_goto; eauto.
-  intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C).
-  exists jmp; exists k; exists rs'.
-  split. eexact A. 
-  split. apply agree_exten with rs0; auto with asmgen.
-  exact B. 
-
-- (* Mcond false *)
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C).
-  econstructor; split.
-  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto.
-  split. apply agree_exten with rs0; auto. intros. Simpl.
-  simpl; congruence.
-
-- (* Mjumptable *)
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H6.
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H5); intro NOOV.
-  exploit find_label_goto_label. eauto. eauto.
-  instantiate (2 := rs0#X16 <- Vundef).
-  Simpl. eauto.
-  eauto.
-  intros [tc' [rs' [A [B C]]]].
-  exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
-  left; econstructor; split.
-  apply plus_one. econstructor; eauto.
-  eapply find_instr_tail; eauto.
-  simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
-  econstructor; eauto.
-  eapply agree_undef_regs; eauto.
-  simpl. intros. rewrite C; auto with asmgen. Simpl.
-  congruence.
-
-- (* Mreturn *)
-  assert (f0 = f) by congruence. subst f0.
-  inversion AT; subst. simpl in H6; monadInv H6.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-    eapply transf_function_no_overflow; eauto.
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-
-- (* internal function *)
-
-  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
-  generalize EQ; intros EQ'. monadInv EQ'.
-  destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0.
-  unfold store_stack in *.
-  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
-  intros [m1' [C D]].
-  exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
-  intros [m2' [F G]].
-  simpl chunk_of_type in F.
-  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
-  intros [m3' [P Q]].
-  change (chunk_of_type Tptr) with Mint64 in *.
-  (* Execution of function prologue *)
-  monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
-  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
-                 storeptr RA XSP (fn_retaddr_ofs f) x0) in *.
-  set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
-  set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)).
-  exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2).
-    simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. 
-    change (rs2 X2) with sp. eexact P. 
-    simpl; congruence. congruence.
-  intros (rs3 & U & V).
-  assert (EXEC_PROLOGUE:
-            exec_straight tge tf
-              tf.(fn_code) rs0 m'
-              x0 rs3 m3').
-  { change (fn_code tf) with tfbody; unfold tfbody.
-    apply exec_straight_step with rs2 m2'.
-    unfold exec_instr. rewrite C. fold sp.
-    rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
-    reflexivity. 
-    eexact U. }
-  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. lia. constructor.
-  econstructor; eauto.
-  rewrite X; econstructor; eauto. 
-  apply agree_exten with rs2; eauto with asmgen.
-  unfold rs2. 
-  apply agree_nextinstr. apply agree_set_other; auto with asmgen.
-  apply agree_change_sp with (parent_sp s). 
-  apply agree_undef_regs with rs0. auto.
-Local Transparent destroyed_at_function_entry. simpl.
-  simpl; intros; Simpl.
-  unfold sp; congruence.
-  intros. rewrite V by auto with asmgen. reflexivity.
-
-- (* external function *)
-  exploit functions_translated; eauto.
-  intros [tf [A B]]. simpl in B. inv B.
-  exploit extcall_arguments_match; eauto.
-  intros [args' [C D]].
-  exploit external_call_mem_extends; eauto.
-  intros [res' [m2' [P [Q [R S]]]]].
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_external; eauto.
-  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  econstructor; eauto.
-  unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto.
-  apply agree_undef_caller_save_regs; auto. 
-
-- (* return *)
-  inv STACKS. simpl in *.
-  right. split. lia. split. auto.
-  rewrite <- ATPC in H5.
-  econstructor; eauto. congruence.
->>>>>>> master
 Qed.
 
 Lemma undef_regs_other_2:
diff --git a/aarch64/TO_MERGE/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 93c1f1ed..93c1f1ed 100644
--- a/aarch64/TO_MERGE/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
diff --git a/aarch64/TO_MERGE/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index bc4279a0..229aa1b4 100644
--- a/aarch64/TO_MERGE/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -21,28 +21,6 @@ open AisAnnot
 open PrintAsmaux
 open Fileinfo
 
-<<<<<<< HEAD
-(* Module containing the printing functions *)
-
-module Target (*: TARGET*) =
-=======
-(* Recognition of FP numbers that are supported by the fmov #imm instructions:
-   "a normalized binary floating point encoding with 1 sign bit,
-    4 bits of fraction and a 3-bit exponent"
-*)
-
-let is_immediate_float64 bits =
-  let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
-  let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
-  exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
-
-let is_immediate_float32 bits =
-  let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
-  let mant = Int32.logand bits 0x7F_FFFFl in
-  exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
-
-(* Naming and printing registers *)
-
 let intsz oc (sz, n) =
   match sz with X -> coqint64 oc n | W -> coqint oc n
 
@@ -112,14 +90,14 @@ let freg oc (sz, r) =
   output_string oc (match sz with D -> dreg_name r | S -> sreg_name r)
 
 let preg_asm oc ty = function
-  | IR r -> if ty = Tint then wreg oc r else xreg oc r
-  | FR r -> if ty = Tsingle then sreg oc r else dreg oc r
-  | _    -> assert false
+    | DR (IR (RR1 r)) -> if ty = Tint then wreg oc r else xreg oc r
+    | DR (FR r) -> if ty = Tsingle then sreg oc r else dreg oc r
+| _    -> assert false
 
 let preg_annot = function
-  | IR r -> xreg_name r
-  | FR r -> dreg_name r
-  | _ -> assert false
+    | DR (IR (RR1 r)) -> xreg_name r
+    | DR (FR r) -> dreg_name r
+    | _ -> assert false
 
 (* Base-2 log of a Caml integer *)
 let rec log2 n =
@@ -147,7 +125,6 @@ module type SYSTEM =
   end
 
 module ELF_System : SYSTEM =
->>>>>>> master
   struct
     let comment = "//"
     let raw_symbol = output_string
@@ -161,105 +138,18 @@ module ELF_System : SYSTEM =
     let label_low oc lbl =
       fprintf oc "#:lo12:%a" elf_label lbl
 
-<<<<<<< HEAD
-    let print_label oc lbl = label oc (transl_label lbl)
+    let load_symbol_address oc rd id =
+        fprintf oc "	adrp	%a, :got:%a\n" xreg rd symbol id;
+        fprintf oc "	ldr	%a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id
 
-    let intsz oc (sz, n) =
-      match sz with X -> coqint64 oc n | W -> coqint oc n
-
-    let xreg_name = function
-    | X0 -> "x0"   | X1 -> "x1"   | X2 -> "x2"   | X3 -> "x3"
-    | X4 -> "x4"   | X5 -> "x5"   | X6 -> "x6"   | X7 -> "x7"
-    | X8 -> "x8"   | X9 -> "x9"   | X10 -> "x10" | X11 -> "x11"
-    | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15"
-    | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19"
-    | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23"
-    | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27"
-    | X28 -> "x28" | X29 -> "x29" | X30 -> "x30"
-
-    let wreg_name = function
-    | X0 -> "w0"   | X1 -> "w1"   | X2 -> "w2"   | X3 -> "w3"
-    | X4 -> "w4"   | X5 -> "w5"   | X6 -> "w6"   | X7 -> "w7"
-    | X8 -> "w8"   | X9 -> "w9"   | X10 -> "w10" | X11 -> "w11"
-    | X12 -> "w12" | X13 -> "w13" | X14 -> "w14" | X15 -> "w15"
-    | X16 -> "w16" | X17 -> "w17" | X18 -> "w18" | X19 -> "w19"
-    | X20 -> "w20" | X21 -> "w21" | X22 -> "w22" | X23 -> "w23"
-    | X24 -> "w24" | X25 -> "w25" | X26 -> "w26" | X27 -> "w27"
-    | X28 -> "w28" | X29 -> "w29" | X30 -> "w30"
-
-    let xreg0_name = function RR0 r -> xreg_name r | XZR -> "xzr"
-    let wreg0_name = function RR0 r -> wreg_name r | XZR -> "wzr"
-
-    let xregsp_name = function RR1 r -> xreg_name r | XSP -> "sp"
-    let wregsp_name = function RR1 r -> wreg_name r | XSP -> "wsp"
-
-    let dreg_name = function
-    | D0 -> "d0"   | D1 -> "d1"   | D2 -> "d2"   | D3 -> "d3"
-    | D4 -> "d4"   | D5 -> "d5"   | D6 -> "d6"   | D7 -> "d7"
-    | D8 -> "d8"   | D9 -> "d9"   | D10 -> "d10" | D11 -> "d11"
-    | D12 -> "d12" | D13 -> "d13" | D14 -> "d14" | D15 -> "d15"
-    | D16 -> "d16" | D17 -> "d17" | D18 -> "d18" | D19 -> "d19"
-    | D20 -> "d20" | D21 -> "d21" | D22 -> "d22" | D23 -> "d23"
-    | D24 -> "d24" | D25 -> "d25" | D26 -> "d26" | D27 -> "d27"
-    | D28 -> "d28" | D29 -> "d29" | D30 -> "d30" | D31 -> "d31"
-
-    let sreg_name = function
-    | D0 -> "s0"   | D1 -> "s1"   | D2 -> "s2"   | D3 -> "s3"
-    | D4 -> "s4"   | D5 -> "s5"   | D6 -> "s6"   | D7 -> "s7"
-    | D8 -> "s8"   | D9 -> "s9"   | D10 -> "s10" | D11 -> "s11"
-    | D12 -> "s12" | D13 -> "s13" | D14 -> "s14" | D15 -> "s15"
-    | D16 -> "s16" | D17 -> "s17" | D18 -> "s18" | D19 -> "s19"
-    | D20 -> "s20" | D21 -> "s21" | D22 -> "s22" | D23 -> "s23"
-    | D24 -> "s24" | D25 -> "s25" | D26 -> "s26" | D27 -> "s27"
-    | D28 -> "s28" | D29 -> "s29" | D30 -> "s30" | D31 -> "s31"
-
-    let xreg oc r = output_string oc (xreg_name r)
-    let wreg oc r = output_string oc (wreg_name r)
-    let ireg oc (sz, r) =
-      output_string oc (match sz with X -> xreg_name r | W -> wreg_name r)
-
-    let xreg0 oc r = output_string oc (xreg0_name r)
-    let wreg0 oc r = output_string oc (wreg0_name r)
-    let ireg0 oc (sz, r) =
-      output_string oc (match sz with X -> xreg0_name r | W -> wreg0_name r)
-
-    let xregsp oc r = output_string oc (xregsp_name r)
-    let iregsp oc (sz, r) =
-      output_string oc (match sz with X -> xregsp_name r | W -> wregsp_name r)
-
-    let dreg oc r = output_string oc (dreg_name r)
-    let sreg oc r = output_string oc (sreg_name r)
-    let freg oc (sz, r) =
-      output_string oc (match sz with D -> dreg_name r | S -> sreg_name r)
-
-    let preg_asm oc ty = function
-      | DR (IR (RR1 r)) -> if ty = Tint then wreg oc r else xreg oc r
-      | DR (FR r) -> if ty = Tsingle then sreg oc r else dreg oc r
-      | _    -> assert false
-
-    let preg_annot = function
-      | DR (IR (RR1 r)) -> xreg_name r
-      | DR (FR r) -> dreg_name r
-      | _ -> assert false
-
-(* Names of sections *)
+    (* Names of sections *)
 
     let name_of_section = function
       | Section_text         -> ".text"
       | 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 ()
-=======
-    let load_symbol_address oc rd id =
-      fprintf oc "	adrp	%a, :got:%a\n" xreg rd symbol id;
-      fprintf oc "	ldr	%a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id
-
-    let name_of_section = function
-      | Section_text         -> ".text"
-      | Section_data i | Section_small_data i ->
           variable_section ~sec:".data" ~bss:".bss" i
->>>>>>> master
       | Section_const i | Section_small_const i ->
           variable_section ~sec:".section	.rodata" i
       | Section_string       -> ".section	.rodata"
@@ -320,7 +210,9 @@ module MacOS_System : SYSTEM =
 
     let name_of_section = function
       | Section_text -> ".text"
-      | Section_data i | Section_small_data i ->
+      | Section_data(i, true) ->
+         failwith "_Thread_local unsupported on this platform"
+      | Section_data(i, false) | Section_small_data i ->
           variable_section ~sec:".data" i
       | Section_const i  | Section_small_const i ->
           variable_section ~sec:".const" ~reloc:".const_data" i
diff --git a/aarch64/TO_MERGE/extractionMachdep.v b/aarch64/extractionMachdep.v
index 947fa38b..dc117744 100644
--- a/aarch64/TO_MERGE/extractionMachdep.v
+++ b/aarch64/extractionMachdep.v
@@ -19,6 +19,9 @@ Require Archi Asm Asmgen SelectOp.
 
 (* Archi *)
 
+
+Extract Constant Archi.pic_code => "fun () -> false".  (* for the time being *)
+
 Extract Constant Archi.abi =>
   "match Configuration.abi with
     | ""apple"" -> Apple
@@ -35,11 +38,4 @@ Extract Constant SelectOp.symbol_is_relocatable =>
 
 Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false".
-<<<<<<< HEAD
 Extract Constant Asmblockgen.symbol_is_aligned => "C2C.atom_is_aligned".
-=======
-
-(* Asmgen *)
-
-Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned".
->>>>>>> master