MB2AB - un peu d'avancement sur internal function

3 files changed, 214 insertions, 14 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 4a4ffc10..2720f3e5 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -99,13 +99,6 @@ End PregEq.
 
 Module Pregmap := EMap(PregEq).
 
-Definition pregs_to_bregs {A} (rs: Pregmap.t A): (Bregmap.t A)
-  := fun r => rs (BaR r).
-
-Definition update_pregs {A} (rs1: Pregmap.t A) (rs2:Bregmap.t A): Pregmap.t A 
-  := fun r => match r with BaR r => rs2 r | _ => rs1 r end.
-
-
 (** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
 
 Notation "'SP'" := GPR12 (only parsing) : asm.
@@ -537,6 +530,11 @@ Notation "a # b <-- c" := (Pregmap.set b c a) (at level 1, b at next level) : as
 
 Open Scope asm.
 
+Definition pregs_to_bregs {A} (rs: Pregmap.t A): (Bregmap.t A)
+  := fun r => rs (BaR r).
+
+Definition update_pregs {A} (rs1: Pregmap.t A) (rs2:Bregmap.t A): Pregmap.t A 
+  := fun r => match r with BaR r => rs2 r | _ => rs1 r end.
 
 (** Undefining some registers *)
 
@@ -1033,7 +1031,7 @@ end.
 
 Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome regset :=
   match exec_body (body b) rs0 m with
-  | Next rs' m' => 
+  | Next rs' m' =>
     let rs1 := nextblock b (update_pregs rs0 rs') in
     match (exit b) with
     | None => Next rs1 m'
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.
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index 15cd88b5..f6e89a36 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -70,6 +70,24 @@ Qed.
 
 Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
 
+Lemma nextblock_pc:
+  forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)).
+Proof.
+  intros. apply Pregmap.gss.
+Qed.
+
+Lemma nextblock_inv:
+  forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r.
+Proof.
+  intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto.
+Qed.
+
+Lemma nextblock_inv1:
+  forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
+Proof.
+  intros. apply nextblock_inv. red; intro; subst; discriminate.
+Qed.
+
 (** * Agreement between Mach registers and processor registers *)
 
 Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree {
@@ -401,7 +419,6 @@ Qed.
 
 Local Hint Resolve code_tail_next.
 
-(* is it useful ?
 Lemma code_tail_next_int:
   forall fn ofs bi c,
   size_blocks fn <= Ptrofs.max_unsigned ->
@@ -417,7 +434,6 @@ Proof.
     omega.
   - rewrite Ptrofs.unsigned_repr; omega.
 Qed.
-*)
 
 (** Predictor for return addresses in generated Asm code.
 
@@ -532,6 +548,120 @@ Inductive transl_code_at_pc (ge: MB.genv):
     code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc ->
     transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc.
 
+Section STRAIGHTLINE.
+
+Variable ge: genv.
+Variable fn: function.
+
+(** Straight-line code is composed of processor instructions that execute
+  in sequence (no branches, no function calls and returns).
+  The following inductive predicate relates the machine states
+  before and after executing a straight-line sequence of instructions.
+  Instructions are taken from the first list instead of being fetched
+  from memory. *)
+
+Inductive exec_straight: bblocks -> regset -> mem ->
+                         bblocks -> regset -> mem -> Prop :=
+  | exec_straight_one:
+      forall b1 c rs1 m1 rs2 m2,
+      exec_bblock ge fn b1 rs1 m1 = Next rs2 m2 ->
+      rs2#PC = Val.offset_ptr (rs1 PC) (Ptrofs.repr (size b1)) ->
+      exec_straight (b1 :: c) rs1 m1 c rs2 m2
+  | exec_straight_step:
+      forall b c rs1 m1 rs2 m2 c' rs3 m3,
+      exec_bblock ge fn b rs1 m1 = Next rs2 m2 ->
+      rs2#PC = Val.offset_ptr (rs1 PC) (Ptrofs.repr (size b)) ->
+      exec_straight c rs2 m2 c' rs3 m3 ->
+      exec_straight (b :: c) rs1 m1 c' rs3 m3.
+
+Lemma exec_straight_trans:
+  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+  exec_straight c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight c1 rs1 m1 c3 rs3 m3.
+Proof.
+  induction 1; intros.
+  apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_step with rs2 m2; auto.
+Qed.
+
+Lemma exec_straight_two:
+  forall b1 b2 c rs1 m1 rs2 m2 rs3 m3,
+  exec_bblock ge fn b1 rs1 m1 = Next rs2 m2 ->
+  exec_bblock ge fn b2 rs2 m2 = Next rs3 m3 ->
+  rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) ->
+  rs3#PC = Val.offset_ptr rs2#PC (Ptrofs.repr (size b2)) ->
+  exec_straight (b1 :: b2 :: c) rs1 m1 c rs3 m3.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  apply exec_straight_one; auto.
+Qed.
+
+Lemma exec_straight_three:
+  forall b1 b2 b3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
+  exec_bblock ge fn b1 rs1 m1 = Next rs2 m2 ->
+  exec_bblock ge fn b2 rs2 m2 = Next rs3 m3 ->
+  exec_bblock ge fn b3 rs3 m3 = Next rs4 m4 ->
+  rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) ->
+  rs3#PC = Val.offset_ptr rs2#PC (Ptrofs.repr (size b2)) ->
+  rs4#PC = Val.offset_ptr rs3#PC (Ptrofs.repr (size b3)) ->
+  exec_straight (b1 :: b2 :: b3 :: c) rs1 m1 c rs4 m4.
+Proof.
+  intros. apply exec_straight_step with rs2 m2; auto.
+  eapply exec_straight_two; eauto.
+Qed.
+
+(** The following lemmas show that straight-line executions
+  (predicate [exec_straight]) correspond to correct Asm executions. *)
+
+Lemma exec_straight_steps_1:
+  forall c rs m c' rs' m',
+  exec_straight c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  plus step ge (State rs m) E0 (State rs' m').
+Proof.
+  induction 1; intros.
+  apply plus_one.
+  repeat (econstructor; eauto).
+  eapply find_bblock_tail. eauto.
+  eapply plus_left'.
+  repeat (econstructor; eauto).
+  eapply find_bblock_tail. eauto.
+  apply IHexec_straight with b0 (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity.
+  auto.
+  apply code_tail_next_int; auto.
+  traceEq.
+Qed.
+
+Lemma exec_straight_steps_2:
+  forall c rs m c' rs' m',
+  exec_straight c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  exists ofs',
+     rs'#PC = Vptr b ofs'
+  /\ code_tail (Ptrofs.unsigned ofs') (fn_blocks fn) c'.
+Proof.
+  induction 1; intros.
+  exists (Ptrofs.add ofs (Ptrofs.repr (size b1))). split.
+  rewrite H0. rewrite H2. auto.
+  apply code_tail_next_int; auto.
+  apply IHexec_straight with (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity. auto.
+  apply code_tail_next_int; auto.
+Qed.
+
+End STRAIGHTLINE.
+
+
 (** * Properties of the Machblock call stack *)
 
 Section MATCH_STACK.