Merge pull request #22 from AbsIntPrivate/arm_large_offsets

Issue #P18: handle large offsets when accessing return address and back link in the stack frame

arm/Asm.v

@@ -199,15 +199,16 @@ Inductive instruction : Type :=
   | Pfsts: freg -> ireg -> int -> instruction       (**r float32 store *)
 
   (* Pseudo-instructions *)
-  | Pallocframe: Z -> ptrofs -> instruction      (**r allocate new stack frame *)
-  | Pfreeframe: Z -> ptrofs -> instruction       (**r deallocate stack frame and restore previous frame *)
-  | Plabel: label -> instruction                   (**r define a code label *)
+  | Pallocframe: Z -> ptrofs -> instruction         (**r allocate new stack frame *)
+  | Pfreeframe: Z -> ptrofs -> instruction          (**r deallocate stack frame and restore previous 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 *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *)
   | Padc: ireg -> ireg -> shift_op -> instruction     (**r add with carry *)
   | Pcfi_adjust: int -> instruction                   (**r .cfi_adjust debug directive *)
+  | Pcfi_rel_offset: int -> instruction               (**r .cfi_rel_offset debug directive *)
   | Pclz: ireg -> ireg -> instruction                 (**r count leading zeros. *)
   | Pfsqrt: freg -> freg -> instruction               (**r floating-point square root. *)
   | Prev: ireg -> ireg -> instruction                 (**r reverse bytes and reverse bits. *)
@@ -757,6 +758,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
           end
       | _ => Stuck
       end
+  | Pcfi_rel_offset ofs =>
+      Next (nextinstr rs) m
   | Pbuiltin ef args res => Stuck    (**r treated specially below *)
   (** The following instructions and directives are not generated directly by Asmgen,
       so we do not model them. *)

arm/Asmexpand.ml

@@ -46,18 +46,22 @@ let expand_movimm dst n =
        (fun n -> emit (Porr (dst,dst, SOimm n))) tl
 
 let expand_subimm dst src n =
-  match Asmgen.decompose_int n with
-  | [] -> assert false
-  | hd::tl ->
-     emit (Psub(dst,src,SOimm hd));
-     List.iter (fun n -> emit (Psub (dst,dst,SOimm n))) tl
+  if dst <> src || n <> _0 then begin
+    match Asmgen.decompose_int n with
+    | [] -> assert false
+    | hd::tl ->
+       emit (Psub(dst,src,SOimm hd));
+       List.iter (fun n -> emit (Psub (dst,dst,SOimm n))) tl
+  end
 
 let expand_addimm dst src n =
-  match Asmgen.decompose_int n with
-  | [] -> assert false
-  | hd::tl ->
-     emit (Padd (dst,src,SOimm hd));
-     List.iter (fun n -> emit (Padd (dst,dst,SOimm n))) tl
+  if dst <> src || n <> _0 then begin
+    match Asmgen.decompose_int n with
+    | [] -> assert false
+    | hd::tl ->
+       emit (Padd (dst,src,SOimm hd));
+       List.iter (fun n -> emit (Padd (dst,dst,SOimm n))) tl
+  end
 
 let expand_int64_arith conflict rl fn =
   if conflict then
@@ -410,12 +414,22 @@ let expand_instruction instr =
   | Pallocframe (sz, ofs) ->
      emit (Pmov (IR12,SOreg IR13));
      if (is_current_function_variadic ()) then begin
-	 emit (Ppush [IR0;IR1;IR2;IR3]);
-	 emit (Pcfi_adjust _16);
-       end;
-     expand_subimm IR13 IR13 sz;
-     emit (Pcfi_adjust sz);
-     emit (Pstr (IR12,IR13,SOimm ofs));
+       emit (Ppush [IR0;IR1;IR2;IR3]);
+       emit (Pcfi_adjust _16);
+     end;
+     let sz' = camlint_of_coqint sz in
+     let ofs' = camlint_of_coqint ofs in
+     if ofs' >= 4096l && sz' >= ofs' then begin
+       expand_subimm IR13 IR13 (coqint_of_camlint (Int32.sub sz' (Int32.add ofs' 4l)));
+       emit (Ppush [IR12]);
+       expand_subimm IR13 IR13 ofs;
+       emit (Pcfi_adjust sz);
+     end else begin
+        assert (ofs' < 4096l);
+        expand_subimm IR13 IR13 sz;
+        emit (Pcfi_adjust sz);
+        emit (Pstr (IR12,IR13,SOimm ofs));
+     end;
      PrintAsmaux.current_function_stacksize := camlint_of_coqint sz
   | Pfreeframe (sz, ofs) ->
      let sz =
@@ -424,7 +438,13 @@ let expand_instruction instr =
        else sz in
      if Asmgen.is_immed_arith sz
      then emit (Padd (IR13,IR13,SOimm sz))
-     else emit (Pldr (IR13,IR13,SOimm ofs))
+     else begin
+       if camlint_of_coqint ofs >= 4096l then begin
+         expand_addimm IR13 IR13 ofs;
+         emit (Pldr (IR13,IR13,SOimm _0))
+       end else
+         emit (Pldr (IR13,IR13,SOimm ofs));
+     end
   | Pbuiltin (ef,args,res) ->
      begin match ef with
 	   | EF_builtin (name,sg) ->

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,10 +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) ::
-         Pstr IR14 IR13 (SOimm (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;

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,7 +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 (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x0) in *.
+  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) ::
+                 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.
@@ -865,32 +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 rs3 m3').
+              x0 rs4 m3').
+  {
   change (fn_code tf) with tfbody; unfold tfbody.
-  apply exec_straight_two with rs2 m2'.
+  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 Ptrofs.of_int_to_int by auto.
-  rewrite P. auto. auto. auto.
-  left; exists (State rs3 m3'); split.
+  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 (rs3 PC) with (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one).
-  rewrite ATPC. simpl. constructor; eauto.
-  eapply code_tail_next_int. omega.
-  eapply code_tail_next_int. omega. constructor.
-  unfold rs3, rs2.
-  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.

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: