From c736e7d34560fef54ec4ab652be28bf2df4e907f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 13 Feb 2017 10:49:33 +0100 Subject: ARM, PowerPC: update Asmgenproof for Coq 8.6 --- arm/Asmgenproof.v | 16 ++++++++-------- powerpc/Asmgenproof.v | 19 +++++++++++++------ 2 files changed, 21 insertions(+), 14 deletions(-) diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index ade121c5..09c20d5c 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -852,8 +852,10 @@ Opaque loadind. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. + 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 (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. intros [m1' [C D]]. @@ -865,12 +867,10 @@ Opaque loadind. set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Ptrofs.zero))). set (rs3 := nextinstr rs2). assert (EXEC_PROLOGUE: - exec_straight tge x - (fn_code x) rs0 m' - x1 rs3 m3'). - replace (fn_code x) - with (Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x1) - by (rewrite <- H5; auto). + exec_straight tge tf + (fn_code tf) rs0 m' + x0 rs3 m3'). + change (fn_code tf) with tfbody; unfold tfbody. apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). unfold Tptr, chunk_of_type, Archi.ptr64 in F. rewrite F. auto. @@ -884,7 +884,7 @@ Opaque loadind. econstructor; eauto. change (rs3 PC) with (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. - subst x. 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. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 447a53a0..6f0390b9 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -876,7 +876,7 @@ Local Transparent destroyed_by_jumptable. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. + destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. @@ -887,15 +887,23 @@ Local Transparent destroyed_by_jumptable. intros [m3' [P Q]]. (* Execution of function prologue *) monadInv EQ0. rewrite transl_code'_transl_code in EQ1. + set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) + (fn_retaddr_ofs f) + :: Pmflr GPR0 + :: Pstw GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) + GPR1 + :: Pcfi_rel_offset + (Ptrofs.to_int (fn_retaddr_ofs f)) :: x0) in *. + set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)). set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))). set (rs4 := nextinstr rs3). set (rs5 := nextinstr rs4). assert (EXEC_PROLOGUE: - exec_straight tge x - x.(fn_code) rs0 m' - x1 rs5 m3'). - rewrite <- H5 at 2. simpl. + exec_straight tge tf + tf.(fn_code) rs0 m' + x0 rs5 m3'). + change (fn_code tf) with tfbody; unfold tfbody. apply exec_straight_step with rs2 m2'. unfold exec_instr. rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite F. auto. auto. @@ -911,7 +919,6 @@ Local Transparent destroyed_by_jumptable. econstructor; eauto. change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. - subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. -- cgit