AArch64: make register X29 callee-save

CompCert doesn't maintain a frame pointer in X29.  However, it must treat
X29 as callee-save, so that CompCert-generated code can be called from code
that uses X29 as frame pointer.

This commit makes X29 callee-save.  In places where X29 was used as a
temporary, X15 or X14 is used instead.

Author: xavierleroy

aarch64/Asm.v

@@ -1067,7 +1067,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       let sp := (Vptr stk Ptrofs.zero) in
       match Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP with
       | None => Stuck
-      | Some m2 => Next (nextinstr (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2
+      | Some m2 => Next (nextinstr (rs #X15 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2
       end
   | Pfreeframe sz pos =>
       match Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) with

aarch64/Asmexpand.ml

@@ -192,8 +192,8 @@ let memcpy_small_arg sz arg tmp =
       assert false
 
 let expand_builtin_memcpy_small sz al src dst =
-  let tsrc = if dst <> BA (IR X17) then X17 else X29 in
-  let tdst = if src <> BA (IR X29) then X29 else X17 in
+  let tsrc = if dst <> BA (IR X17) then X17 else X15 in
+  let tdst = if src <> BA (IR X15) then X15 else X17 in
   let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
   let (rdst, odst) = memcpy_small_arg sz dst tdst in
   let rec copy osrc odst sz =
@@ -233,29 +233,29 @@ let memcpy_big_arg arg tmp =
 let expand_builtin_memcpy_big sz al src dst =
   assert (sz >= 16);
   memcpy_big_arg src X30;
-  memcpy_big_arg dst X29;
+  memcpy_big_arg dst X14;
   let lbl = new_label () in
   expand_loadimm32 X15 (Z.of_uint (sz / 16));
   emit (Plabel lbl);
   emit (Pldp(X16, X17, ADpostincr(RR1 X30, _16)));
-  emit (Pstp(X16, X17, ADpostincr(RR1 X29, _16)));
+  emit (Pstp(X16, X17, ADpostincr(RR1 X14, _16)));
   emit (Psubimm(W, RR1 X15, RR1 X15, _1));
   emit (Pcbnz(W, X15, lbl));
   if sz mod 16 >= 8 then begin
     emit (Pldrx(X16, ADpostincr(RR1 X30, _8)));
-    emit (Pstrx(X16, ADpostincr(RR1 X29, _8)))
+    emit (Pstrx(X16, ADpostincr(RR1 X14, _8)))
   end;
   if sz mod 8 >= 4 then begin
     emit (Pldrw(X16, ADpostincr(RR1 X30, _4)));
-    emit (Pstrw(X16, ADpostincr(RR1 X29, _4)))
+    emit (Pstrw(X16, ADpostincr(RR1 X14, _4)))
   end;
   if sz mod 4 >= 2 then begin
     emit (Pldrh(W, X16, ADpostincr(RR1 X30, _2)));
-    emit (Pstrh(X16, ADpostincr(RR1 X29, _2)))
+    emit (Pstrh(X16, ADpostincr(RR1 X14, _2)))
   end;
   if sz mod 2 >= 1 then begin
     emit (Pldrb(W, X16, ADpostincr(RR1 X30, _1)));
-    emit (Pstrb(X16, ADpostincr(RR1 X29, _1)))
+    emit (Pstrb(X16, ADpostincr(RR1 X14, _1)))
   end
 
 let expand_builtin_memcpy  sz al args =
@@ -412,7 +412,7 @@ let expand_builtin_inline name args res =
 let expand_instruction instr =
   match instr with
   | Pallocframe (sz, ofs) ->
-      emit (Pmov (RR1 X29, XSP));
+      emit (Pmov (RR1 X15, XSP));
       if is_current_function_variadic() && Archi.abi = Archi.AAPCS64 then begin
         let (ir, fr, _) =
           next_arg_locations 0 0 0 (get_current_function_args ()) in
@@ -423,7 +423,7 @@ let expand_instruction instr =
         current_function_stacksize := Z.to_int64 sz
       end;
       expand_addimm64 XSP XSP (Ptrofs.repr (Z.neg sz));
-      expand_storeptr X29 XSP ofs
+      expand_storeptr X15 XSP ofs
   | Pfreeframe (sz, ofs) ->
       expand_addimm64 XSP XSP (coqint_of_camlint64 !current_function_stacksize)
   | Pcvtx2w rd ->

aarch64/Asmgen.v

@@ -1057,16 +1057,16 @@ Definition make_epilogue (f: Mach.function) (k: code) :=
 (** Translation of a Mach instruction. *)
 
 Definition transl_instr (f: Mach.function) (i: Mach.instruction)
-                        (r29_is_parent: bool) (k: code) : res code :=
+                        (r15_is_parent: bool) (k: code) : res code :=
   match i with
   | Mgetstack ofs ty dst =>
       loadind XSP ofs ty dst k
   | Msetstack src ofs ty =>
       storeind src XSP ofs ty k
   | Mgetparam ofs ty dst =>
       (* load via the frame pointer if it is valid *)
-      do c <- loadind X29 ofs ty dst k;
-      OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 c)
+      do c <- loadind X15 ofs ty dst k;
+      OK (if r15_is_parent then c else loadptr XSP f.(fn_link_ofs) X15 c)
   | Mop op args res =>
       transl_op op args res k
   | Mload chunk addr args dst =>
@@ -1102,8 +1102,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
 Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool :=
   match i with
   | Msetstack src ofs ty => before
-  | Mgetparam ofs ty dst => negb (mreg_eq dst R29)
-  | Mop op args res => before && negb (mreg_eq res R29)
+  | Mgetparam ofs ty dst => negb (mreg_eq dst R15)
+  | Mop op args res => before && negb (mreg_eq res R15)
   | _ => false
   end.
 

aarch64/Asmgenproof.v

@@ -472,7 +472,7 @@ Inductive match_states: Mach.state -> Asm.state -> Prop :=
         (MEXT: Mem.extends m m')
         (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
         (AG: agree ms sp rs)
-        (DXP: ep = true -> rs#X29 = parent_sp s),
+        (DXP: ep = true -> rs#X15 = parent_sp s),
       match_states (Mach.State s fb sp c ms m)
                    (Asm.State rs m')
   | match_states_call:
@@ -503,7 +503,7 @@ Lemma exec_straight_steps:
    exists rs2,
        exec_straight tge tf c rs1 m1' k rs2 m2'
     /\ agree ms2 sp rs2
-    /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)) ->
+    /\ (it1_is_parent ep i = true -> rs2#X15 = parent_sp s)) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
   match_states (Mach.State s fb sp c ms2 m2) st'.
@@ -614,9 +614,9 @@ Definition measure (s: Mach.state) : nat :=
   | Mach.Returnstate _ _ _ => 1%nat
   end.
 
-Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r.
+Remark preg_of_not_X15: forall r, negb (mreg_eq r R15) = true -> IR X15 <> preg_of r.
 Proof.
-  intros. change (IR X29) with (preg_of R29). red; intros.
+  intros. change (IR X15) with (preg_of R15). red; intros.
   exploit preg_of_injective; eauto. intros; subst r; discriminate.
 Qed.
 
@@ -672,26 +672,26 @@ Proof.
 Opaque loadind.
   left; eapply exec_straight_steps; eauto; intros. monadInv TR. 
   destruct ep.
-(* X30 contains parent *)
+(* X15 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 *)
+  apply preg_of_not_X15; auto.
+(* X15 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.
+  instantiate (1 := rs1#X15 <- (rs2#X15)). intros.
   rewrite Pregmap.gso; auto with asmgen.
   congruence.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r' X15). congruence. auto with asmgen.
   simpl; intros. rewrite U; auto with asmgen.
-  apply preg_of_not_X29; auto.
+  apply preg_of_not_X15; auto.
 
 - (* Mop *)
   assert (eval_operation tge sp op (map rs args) m = Some v).
@@ -704,7 +704,7 @@ Opaque loadind.
   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.
+  rewrite R; auto. apply preg_of_not_X15; auto.
 Local Transparent destroyed_by_op.
   destruct op; try exact I; simpl; congruence.
 
@@ -933,7 +933,7 @@ Local Transparent destroyed_by_op.
   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)).
+  set (rs2 := nextinstr (rs0#X15 <- (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. 

aarch64/Conventions1.v

@@ -38,7 +38,7 @@ Definition is_callee_save (r: mreg): bool :=
   | R17 => false
   | R19 | R20 | R21 |  R22 | R23 => true
   | R24 | R25 | R26 | R27 | R28 => true
-  | R29 => false
+  | R29 => true
   | F0  | F1  | F2  | F3  | F4  | F5  | F6  | F7 => false
   | F8  | F9  | F10 | F11 | F12 | F13 | F14 | F15 => true
   | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 => false
@@ -48,7 +48,7 @@ Definition is_callee_save (r: mreg): bool :=
 Definition int_caller_save_regs :=
      R0  :: R1  :: R2  :: R3  :: R4  :: R5  :: R6  :: R7
   :: R8  :: R9  :: R10 :: R11 :: R12 :: R13 :: R14 :: R15
-  :: R17 :: R29 :: nil.
+  :: R17 :: nil.
 
 Definition float_caller_save_regs :=
      F0  :: F1  :: F2  :: F3  :: F4  :: F5  :: F6  :: F7
@@ -57,7 +57,7 @@ Definition float_caller_save_regs :=
 
 Definition int_callee_save_regs :=
      R19 :: R20 :: R21 ::  R22 :: R23
-  :: R24 :: R25 :: R26 :: R27 :: R28 :: nil.
+  :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: nil.
 
 Definition float_callee_save_regs :=
      F8  :: F9  :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil.

aarch64/Machregs.v

@@ -156,18 +156,18 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
 
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
-  | EF_memcpy sz al => R15 :: R17 :: R29 :: nil
+  | EF_memcpy sz al => R14 :: R15 :: R17 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
   end.
 
 Definition destroyed_by_setstack (ty: typ): list mreg := nil.
 
-Definition destroyed_at_function_entry: list mreg := R29 :: nil.
+Definition destroyed_at_function_entry: list mreg := R15 :: nil.
 
 Definition destroyed_at_indirect_call: list mreg := nil.
 
-Definition temp_for_parent_frame: mreg := R29.
+Definition temp_for_parent_frame: mreg := R15.
 
 Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
   (nil, None).