ARM port: replace Psavelr pseudo-instruction by actual instructions

Saving the return address register (R14) in the function prologue can be done either with a single "str" instruction if the offset is small enough, or by constructing the address using the R12 register as a temporary then storing with "str" relative to R12.

R12 can be used as a temporary because it is marked as destroyed at function entry.  We just need to tell Asmgen.translcode whether R12 still contains the back link left there by Pallocframe, or R12 was trashed.  In the latter case R12 will be reloaded from the stack at the next Mgetparam instruction.

6 files changed, 88 insertions, 47 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 7a393139..85eb94c1 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -201,7 +201,6 @@ Inductive instruction : Type :=
   (* Pseudo-instructions *)
   | Pallocframe: Z -> ptrofs -> instruction         (**r allocate new stack frame *)
   | Pfreeframe: Z -> ptrofs -> instruction          (**r deallocate stack frame and restore previous frame *)
-  | Psavelr: ptrofs -> instruction                  (**r store link register in allocated stack frame *)
   | Plabel: label -> instruction                    (**r define a code label *)
   | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *)
   | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
@@ -270,18 +269,6 @@ lbl:    .word   symbol
 >>
   Again, our memory model cannot comprehend that this operation
   frees (logically) the current stack frame.
-- [Psavelr pos]: this pseudo-instruction stores the link register in the
-  stackframe at the specified position. It handles out-of-range offsets,
-  i.e. the generated code for in-range offsets is:
-<<
-        str     lr, [sp, #pos]
->>
-  and for out-of-range offsets:
-<<
-        add     sp, sp, #pos   (* code to expand the immediate *)
-        str     lr, [sp]
-        sub     sp, sp, #pos   (* code to expand the immediate *)
->>
 - [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
   as follows:
 <<
@@ -750,8 +737,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
           | _ => Stuck
           end
       end
-  | Psavelr pos =>
-      exec_store Mint32 (Val.offset_ptr rs#IR13 pos) IR14 rs m
   | Plabel lbl =>
       Next (nextinstr rs) m
   | Ploadsymbol r1 lbl ofs =>
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index c4e7e77d..04b4152d 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -445,13 +445,6 @@ let expand_instruction instr =
        end else
          emit (Pldr (IR13,IR13,SOimm ofs));
      end
-  | Psavelr ofs ->
-     if camlint_of_coqint ofs >= 4096l then begin
-       expand_addimm IR13 IR13 ofs;
-       emit (Pstr (IR14,IR13,SOimm _0));
-       expand_subimm IR13 IR13 ofs
-     end else
-       emit (Pstr (IR14,IR13,SOimm ofs))
   | Pbuiltin (ef,args,res) ->
      begin match ef with
 	   | EF_builtin (name,sg) ->
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 8c49d881..1b96416d 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -602,6 +602,22 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :
       Error (msg "Asmgen.storeind")
   end.
 
+(** This is a variant of [storeind] that is used to save the return address
+  at the beginning of a function.  It uses [R12] instead of [R14] as
+  temporary register. *)
+
+Definition save_lr (ofs: ptrofs) (k: code) :=
+  let n := Ptrofs.to_int ofs in
+  let n1 := mk_immed_mem_word n in
+  if Int.eq n n1
+  then Pstr IR14 IR13 (SOimm n) :: k
+  else addimm IR12 IR13 (Int.sub n n1) (Pstr IR14 IR12 (SOimm n1) :: k).
+
+Definition save_lr_preserves_R12 (ofs: ptrofs) : bool :=
+  let n := Ptrofs.to_int ofs in
+  let n1 := mk_immed_mem_word n in
+  Int.eq n n1.
+
 (** Translation of memory accesses *)
 
 Definition transl_memory_access
@@ -787,11 +803,12 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo
   around, leading to incorrect executions. *)
 
 Definition transl_function (f: Mach.function) :=
-  do c <- transl_code f f.(Mach.fn_code) true;
+  do c <- transl_code f f.(Mach.fn_code)
+                      (save_lr_preserves_R12 f.(fn_retaddr_ofs));
   OK (mkfunction f.(Mach.fn_sig)
         (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-         Psavelr f.(fn_retaddr_ofs) ::
-         Pcfi_rel_offset (Ptrofs.to_int f.(fn_retaddr_ofs)):: c)).
+         save_lr f.(fn_retaddr_ofs)
+           (Pcfi_rel_offset (Ptrofs.to_int f.(fn_retaddr_ofs)):: c))).
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
   do tf <- transl_function f;
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 7d963a47..71a0e049 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -241,6 +241,15 @@ Proof.
   destruct ty, (preg_of src); inv H; TailNoLabel.
 Qed.
 
+Remark save_lr_label:
+  forall ofs k, tail_nolabel k (save_lr ofs k).
+Proof.
+  unfold save_lr; intros.
+  destruct (Int.eq (Ptrofs.to_int ofs) (mk_immed_mem_word (Ptrofs.to_int ofs))).
+  TailNoLabel.
+  eapply tail_nolabel_trans; TailNoLabel.
+Qed.
+
 Remark transl_cond_label:
   forall cond args k c, transl_cond cond args k = OK c -> tail_nolabel k c.
 Proof.
@@ -338,7 +347,7 @@ Lemma transl_find_label:
   end.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0.
-  monadInv EQ. simpl.
+  monadInv EQ. simpl. erewrite tail_nolabel_find_label by (apply save_lr_label). simpl.
   eapply transl_code_label; eauto.
 Qed.
 
@@ -382,7 +391,8 @@ Proof.
   destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
 - intros. monadInv H0.
   destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ.
-  exists x; exists true; split; auto. repeat constructor.
+  exists x; exists (save_lr_preserves_R12 (fn_retaddr_ofs f0)); split; auto.
+  constructor. eapply is_tail_trans. 2: apply tail_nolabel_is_tail; apply save_lr_label. repeat constructor.  
 - exact transf_function_no_overflow.
 Qed.
 
@@ -854,9 +864,10 @@ Opaque loadind.
   generalize EQ; intros EQ'. monadInv EQ'.
   destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. subst x0.
   monadInv EQ0.
+  set (ra_ofs := fn_retaddr_ofs f) in *.
+  set (ra_ofs' := Ptrofs.to_int ra_ofs) in *.
   set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
-                 Psavelr (fn_retaddr_ofs f) ::
-                 Pcfi_rel_offset (Ptrofs.to_int (fn_retaddr_ofs f)) :: x0) in *.
+                 save_lr ra_ofs (Pcfi_rel_offset ra_ofs' :: x0)) in *.
   set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
   unfold store_stack in *.
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
@@ -867,34 +878,40 @@ Opaque loadind.
   intros [m3' [P Q]].
   (* Execution of function prologue *)
   set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Ptrofs.zero))).
-  set (rs3 := nextinstr rs2).
+  edestruct (save_lr_correct tge tf ra_ofs (Pcfi_rel_offset ra_ofs' :: x0) rs2) as (rs3 & X & Y & Z).
+    change (rs2 IR13) with sp. change (rs2 IR14) with (rs0 IR14). rewrite ATLR. eexact P.  
   set (rs4 := nextinstr rs3).
   assert (EXEC_PROLOGUE:
             exec_straight tge tf
               (fn_code tf) rs0 m'
               x0 rs4 m3').
+  {
   change (fn_code tf) with tfbody; unfold tfbody.
-  apply exec_straight_three with rs2 m2' rs3 m3'.
+  eapply exec_straight_trans with (rs2 := rs2) (m2 := m2').
+  apply exec_straight_one. 
   unfold exec_instr. rewrite C. fold sp.
   rewrite <- (sp_val _ _ _ AG). unfold Tptr, chunk_of_type, Archi.ptr64 in F. rewrite F. auto.
-  simpl. auto.
-  simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14).
-  rewrite Ptrofs.add_zero_l. simpl. unfold Tptr, chunk_of_type, Archi.ptr64 in P. simpl in P.
-  rewrite Ptrofs.add_zero_l in P. rewrite ATLR.
-  rewrite P. auto. auto. auto. auto. auto.
+  auto.
+  eapply exec_straight_trans with (rs2 := rs3) (m2 := m3').
+  eexact X.
+  apply exec_straight_one.
+  simpl; reflexivity. reflexivity.
+  }
+  (* After the function prologue is the code for the function body *)
+  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
+  intros (ofsbody & U & V).
+  (* Conclusions *)
   left; exists (State rs4 m3'); split.
   eapply exec_straight_steps_1; eauto. omega. constructor.
-  econstructor; eauto.
-  change (rs4 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one).
-  rewrite ATPC. simpl. constructor; eauto.
-  eapply code_tail_next_int. omega.
-  eapply code_tail_next_int. omega.
-  eapply code_tail_next_int. omega. constructor.
-  unfold rs4, rs2.
-  apply agree_nextinstr. apply agree_nextinstr. apply agree_nextinstr.
+  econstructor; eauto. rewrite U. econstructor; eauto. 
+  apply agree_nextinstr.
+  apply agree_undef_regs2 with rs2.
+  apply agree_nextinstr. 
   eapply agree_change_sp.
   apply agree_undef_regs with rs0; eauto.
-  intros. Simpl. congruence.
+  intros; Simpl.
+  congruence.
+  intros; apply Y; eauto with asmgen. 
 
 - (* external function *)
   exploit functions_translated; eauto.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index eec531dc..7084336e 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -616,6 +616,37 @@ Proof.
   intros; Simpl.
 Qed.
 
+(** Saving the link register *)
+
+Lemma save_lr_correct:
+  forall ofs k (rs: regset) m m',
+  Mem.storev Mint32 m (Val.offset_ptr rs#IR13 ofs) (rs#IR14) = Some m' ->
+  exists rs',
+     exec_straight ge fn (save_lr ofs k) rs m k rs' m'
+  /\ (forall r, if_preg r = true -> r <> IR12 -> rs'#r = rs#r)
+  /\ (save_lr_preserves_R12 ofs = true -> rs'#IR12 = rs#IR12).
+Proof.
+  intros; unfold save_lr, save_lr_preserves_R12.
+  set (n := Ptrofs.to_int ofs). set (n1 := mk_immed_mem_word n).
+  assert (EQ: Val.offset_ptr rs#IR13 ofs = Val.add rs#IR13 (Vint n)).
+  { destruct rs#IR13; try discriminate. simpl. f_equal; f_equal. unfold n; symmetry; auto with ptrofs. }
+  destruct (Int.eq n n1).
+- econstructor; split. apply exec_straight_one. simpl; unfold exec_store. rewrite <- EQ, H; reflexivity. auto.
+  split. intros; Simpl. intros; Simpl.
+- destruct (addimm_correct IR12 IR13 (Int.sub n n1) (Pstr IR14 IR12 (SOimm n1) :: k) rs m)
+  as (rs1 & A & B & C).
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. 
+  apply exec_straight_one. simpl; unfold exec_store.
+  rewrite B. rewrite Val.add_assoc. simpl.
+  rewrite Int.sub_add_opp. rewrite Int.add_assoc.
+  rewrite (Int.add_commut (Int.neg n1)).
+  rewrite Int.add_neg_zero. rewrite Int.add_zero. 
+  rewrite <- EQ. rewrite C by eauto with asmgen. rewrite H. reflexivity.
+  auto.
+  split. intros; Simpl. congruence.
+Qed.
+  
 (** Translation of shift immediates *)
 
 Lemma transl_shift_correct:
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 02c348a8..1dfe8af6 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -693,8 +693,6 @@ struct
       assert false
     | Pfreeframe(sz, ofs) ->
       assert false
-    | Psavelr(ofs) ->
-      assert false
     | Plabel lbl ->
       fprintf oc "%a:\n" print_label lbl; 0
     | Ploadsymbol(r1, id, ofs) ->