ARM, PowerPC: update Asmgenproof for Coq 8.6

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.