diff options
| -rw-r--r-- | arm/Asm.v | 15 | ||||
| -rw-r--r-- | arm/Asmexpand.ml | 7 | ||||
| -rw-r--r-- | arm/Asmgen.v | 23 | ||||
| -rw-r--r-- | arm/Asmgenproof.v | 57 | ||||
| -rw-r--r-- | arm/Asmgenproof1.v | 31 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 2 |
6 files changed, 88 insertions, 47 deletions
@@ -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) -> |