MBload proved

2 files changed, 37 insertions, 19 deletions

diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index e049ac58..8343272a 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1536,7 +1536,31 @@ Proof.
 Local Transparent destroyed_by_op.

     destruct op; simpl; auto; congruence.

   - (* MBload *)

-    destruct TODO.

+    simpl in EQ0. rewrite Hheader in DXP.

+

+    assert (eval_addressing tge sp addr (map ms args) = Some a).

+      rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.

+    exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.

+    intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.

+    exploit Mem.loadv_extends; eauto. intros [v' [C D]].

+    exploit transl_load_correct; eauto.

+    intros [rs2 [P [Q R]]].

+

+    eapply exec_straight_body in P.

+      2: eapply code_to_basics_id; eauto.

+    destruct P as (l & ll & TBC & CTB & EXECB).

+    exists rs2, m1, ll.

+    eexists. eexists. split. instantiate (1 := x). eauto.

+    repeat (split; auto).

+      eapply basics_to_code_app; eauto.

+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

+(*     assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }

+    rewrite <- Hheadereq. *) subst.

+    eapply match_codestate_intro; eauto. simpl. simpl in EQ.

+

+    eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.

+    simpl; congruence.

+

   - (* MBstore *)

     destruct TODO.

 Qed.

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 3858571f..d0c205cd 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1451,14 +1451,12 @@ Proof.
   intros. unfold Mptr. assert (Archi.ptr64 = true); auto.
 Qed.
 
-
-(*
 Lemma transl_memory_access_correct:
   forall mk_instr addr args k c (rs: regset) m v,
   transl_memory_access mk_instr addr args k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
   exists base ofs rs',
-     exec_straight_opt c rs m (mk_instr base ofs :: k) rs' m
+     exec_straight_opt (basics_to_code c) rs m (mk_instr base ofs ::g (basics_to_code k)) rs' m
   /\ Val.offset_ptr rs'#base (eval_offset ge ofs) = v
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
@@ -1488,15 +1486,15 @@ Proof.
 Qed.
 
 Lemma transl_load_access_correct:
-  forall chunk (mk_instr: ireg -> offset -> instruction) addr args k c rd (rs: regset) m v v',
+  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v',
   (forall base ofs rs,
-     exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
   transl_memory_access mk_instr addr args k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
   Mem.loadv chunk m v = Some v' ->
   rd <> PC ->
   exists rs',
-     exec_straight ge fn c rs m k rs' m
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
   /\ rs'#rd = v'
   /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r.
 Proof.
@@ -1506,19 +1504,19 @@ Proof.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
   rewrite INSTR. unfold exec_load. rewrite B, LOAD. reflexivity. Simpl. 
-  split; intros; Simpl.
+  split; intros; Simpl. auto.
 Qed.
 
 Lemma transl_store_access_correct:
-  forall chunk (mk_instr: ireg -> offset -> instruction) addr args k c r1 (rs: regset) m v m',
+  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
   (forall base ofs rs,
-     exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
   transl_memory_access mk_instr addr args k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
   Mem.storev chunk m v rs#r1 = Some m' ->
   r1 <> PC -> r1 <> GPR31 ->
   exists rs',
-     exec_straight ge fn c rs m k rs' m'
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
   intros until m'; intros INSTR TR EV STORE NOTPC NOT31. 
@@ -1527,7 +1525,6 @@ Proof.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
   rewrite INSTR. unfold exec_store. rewrite B, C, STORE by auto. reflexivity. auto.
-  intros; Simpl.
 Qed.
 
 Lemma transl_load_correct:
@@ -1536,7 +1533,7 @@ Lemma transl_load_correct:
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
-     exec_straight ge fn c rs m k rs' m
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
@@ -1544,7 +1541,7 @@ Proof.
   assert (A: exists mk_instr,
       transl_memory_access mk_instr addr args k = OK c
    /\ forall base ofs rs,
-        exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m (preg_of dst) base ofs).
+        exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m (preg_of dst) base ofs).
   { unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (split; [eassumption|auto]). }
   destruct A as (mk_instr & B & C).
   eapply transl_load_access_correct; eauto with asmgen.
@@ -1556,14 +1553,14 @@ Lemma transl_store_correct:
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
   Mem.storev chunk m a rs#(preg_of src) = Some m' ->
   exists rs',
-     exec_straight ge fn c rs m k rs' m'
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
   intros until m'; intros TR EV STORE. 
   assert (A: exists mk_instr chunk',
       transl_memory_access mk_instr addr args k = OK c
    /\ (forall base ofs rs,
-        exec_instr ge fn (mk_instr base ofs) rs m = exec_store ge chunk' rs m (preg_of src) base ofs)
+        exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk' rs m (preg_of src) base ofs)
    /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)).
   { unfold transl_store in TR; destruct chunk; ArgsInv;
     (econstructor; econstructor; split; [eassumption | split; [ intros; simpl; reflexivity | auto]]).
@@ -1574,9 +1571,6 @@ Proof.
   rewrite D in STORE; clear D. 
   eapply transl_store_access_correct; eauto with asmgen.
 Qed.
-*)
-
-Definition noscroll := 0.
 
 Lemma make_epilogue_correct:
   forall ge0 f m stk soff cs m' ms rs k tm,