diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-17 09:45:44 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-17 09:45:44 +0200 |
| commit | c9d01df3577a23e20abbe934f6f36f17dbbb82cd (patch) | |
| tree | 3347d5103efbdd6f0ca445b648763389097d3833 /arm/Asmgenproof.v | |
| parent | e5d8d8d2d67daed762f6e0cc8f486b2c1b37bb20 (diff) | |
| download | compcert-kvx-c9d01df3577a23e20abbe934f6f36f17dbbb82cd.tar.gz compcert-kvx-c9d01df3577a23e20abbe934f6f36f17dbbb82cd.zip | |
ARM: Generate Pcfi_rel_offset directives directly from Asmgen
This is what we do for PowerPC and is more resilient to changes in code generation. We need to give Pcfi_rel_offset a dynamic semantics, but that's just a no-op.
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index f306f43a..7d963a47 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -854,7 +854,9 @@ 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) :: Psavelr (fn_retaddr_ofs f) :: x0) 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 *. 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. @@ -866,28 +868,30 @@ Opaque loadind. (* Execution of function prologue *) set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Ptrofs.zero))). set (rs3 := nextinstr rs2). + 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'. + apply exec_straight_three with rs2 m2' rs3 m3'. 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. - left; exists (State rs3 m3'); split. + rewrite P. auto. auto. auto. auto. auto. + 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). + 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 rs3, rs2. - apply agree_nextinstr. apply agree_nextinstr. + unfold rs4, rs2. + apply agree_nextinstr. apply agree_nextinstr. apply agree_nextinstr. eapply agree_change_sp. apply agree_undef_regs with rs0; eauto. intros. Simpl. congruence. |