MB2AB - un peu d'avancement sur internal function

1 files changed, 76 insertions, 4 deletions

diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index f0842c4d..a9604c14 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1081,10 +1081,82 @@ Theorem step_simulation:
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
   induction 1; intros; inv MS.
-  - destruct TODO.
-  - destruct TODO.
 
-- (* external function *)
+- destruct TODO.
+
+- (* internal function *)
+  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
+  generalize EQ; intros EQ'. monadInv EQ'.
+  destruct (zlt Ptrofs.max_unsigned (size_blocks x0.(fn_blocks))); inversion EQ1. clear EQ1. subst x0.
+  unfold Mach.store_stack in *.
+  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
+  intros [m1' [C D]].
+  exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
+  intros [m2' [F G]].
+  simpl chunk_of_type in F.
+  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
+  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) ::b
+                 Pget GPR8 RA ::b
+                 storeind_ptr GPR8 SP (fn_retaddr_ofs f) ::b x0) in *.
+  set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.
+  set (rs2 := nextblock (bblock_single_inst (Pallocframe (fn_stacksize f) (fn_link_ofs f))) 
+                          (rs0#FP <-- (parent_sp s) #SP <-- sp #GPR31 <-- Vundef)).
+  destruct TODO.
+(*   exploit (Pget_correct tge tf GPR8 RA (storeind_ptr GPR8 SP (fn_retaddr_ofs f) x0) rs2 m2'); auto.
+  intros (rs' & U' & V').
+  exploit (storeind_ptr_correct tge tf SP (fn_retaddr_ofs f) GPR8 x0 rs' m2').
+    rewrite chunk_of_Tptr in P.
+    assert (rs' GPR8 = rs0 RA). { apply V'. }
+    assert (rs' GPR12 = rs2 GPR12). { apply V'; discriminate. }
+    rewrite H3. rewrite H4.
+    (* change (rs' GPR8) with (rs0 RA). *)
+    rewrite ATLR.
+    change (rs2 GPR12) with sp. eexact P.
+    congruence. congruence.
+  intros (rs3 & U & V).
+  assert (EXEC_PROLOGUE:
+            exec_straight tge tf
+              tf.(fn_code) rs0 m'
+              x0 rs3 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 chunk_of_Tptr in F. rewrite F. reflexivity.
+    reflexivity.
+    eapply exec_straight_trans.
+    - eexact U'.
+    - eexact U. }
+  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
+  intros (ofs' & X & Y).                    
+  left; exists (State rs3 m3'); split.
+  eapply exec_straight_steps_1; eauto. omega. constructor.
+  econstructor; eauto.
+  rewrite X; econstructor; eauto. 
+  apply agree_exten with rs2; eauto with asmgen.
+  unfold rs2. 
+  apply agree_nextinstr. apply agree_set_other; auto with asmgen.
+  apply agree_change_sp with (parent_sp s). 
+  apply agree_undef_regs with rs0. auto.
+Local Transparent destroyed_at_function_entry.
+  simpl; intros; Simpl.
+  unfold sp; congruence.
+
+  intros.
+  assert (r <> GPR31). { contradict H3; rewrite H3; unfold data_preg; auto. }
+  rewrite V.
+  assert (r <> GPR8). { contradict H3; rewrite H3; unfold data_preg; auto. }
+  assert (forall r : preg, r <> PC -> r <> GPR8 -> rs' r = rs2 r). { apply V'. }
+  rewrite H6; auto.
+  contradict H3; rewrite H3; unfold data_preg; auto.
+  contradict H3; rewrite H3; unfold data_preg; auto.
+  contradict H3; rewrite H3; unfold data_preg; auto.
+  intros. rewrite V by auto with asmgen.
+  assert (forall r : preg, r <> PC -> r <> GPR8 -> rs' r = rs2 r). { apply V'. }
+  rewrite H4 by auto with asmgen. reflexivity.
+ *) - (* external function *)
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B.
   exploit extcall_arguments_match; eauto.
@@ -1099,7 +1171,7 @@ Proof.
   apply agree_set_other; auto.
   apply agree_set_pair; auto.
 
-  - (* return *) 
+- (* return *) 
   inv STACKS. simpl in *.
   right. split. omega. split. auto.
   rewrite <- ATPC in H5.