From d357b5c52fb9ac70679fa8abd47094e89a6c3fa1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 25 May 2022 15:32:17 +0200 Subject: 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. --- aarch64/Asm.v | 2 +- aarch64/Asmexpand.ml | 20 ++++++++++---------- aarch64/Asmgen.v | 10 +++++----- aarch64/Asmgenproof.v | 24 ++++++++++++------------ aarch64/Conventions1.v | 6 +++--- aarch64/Machregs.v | 6 +++--- 6 files changed, 34 insertions(+), 34 deletions(-) diff --git a/aarch64/Asm.v b/aarch64/Asm.v index b5f4c838..c5f4032e 100644 --- a/aarch64/Asm.v +++ b/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 diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 573e8b92..7754a023 100644 --- a/aarch64/Asmexpand.ml +++ b/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 -> diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index baaab6c4..2237c66a 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -1057,7 +1057,7 @@ 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 @@ -1065,8 +1065,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) 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. diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index dc0bc509..b46f7491 100644 --- a/aarch64/Asmgenproof.v +++ b/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. diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index f401458c..3e7159ac 100644 --- a/aarch64/Conventions1.v +++ b/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. diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index 704c392e..f9b9fd79 100644 --- a/aarch64/Machregs.v +++ b/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). -- cgit