MBsetstack done!

3 files changed, 38 insertions, 33 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index fb0f8c37..cf6fef3b 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -816,14 +816,14 @@ Definition eval_offset (ofs: offset) : ptrofs :=
   end.
 
 Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem)
-                     (d: ireg) (a: ireg) (ofs: offset) :=
+                     (d: preg) (a: ireg) (ofs: offset) :=
   match Mem.loadv chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) with
   | None => Stuck
   | Some v => Next (rs#d <- v) m
   end.
 
 Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
-                      (s: ireg) (a: ireg) (ofs: offset) :=
+                      (s: preg) (a: ireg) (ofs: offset) :=
   match Mem.storev chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) (rs s) with
   | None => Stuck
   | Some m' => Next rs m'
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 6b83d110..ba6ecb66 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1445,11 +1445,9 @@ Admitted.
 Lemma step_simu_basic:

   forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy,

   MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->

-(*   (bdy <> nil \/ MB.exit bb <> None) -> *)

   bb' = {| MB.header := MB.header bb; MB.body := bdy; MB.exit := MB.exit bb |} ->

   basic_step ge s fb sp ms m bi ms' m' ->

   pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy ->

-(*   pstate cs2 = (State rs2 m2) -> pbody1 cs2 = tbdy' -> *)

   match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->

   (exists rs2 m2 l cs2 tbdy',

        cs2 = {| pstate := (State rs2 m2); pheader := pheader cs1; pbody1 := tbdy'; pbody2 := pbody2 cs1;

@@ -1467,7 +1465,7 @@ Proof.
     unfold Mach.load_stack in H.

     exploit Mem.loadv_extends; eauto. intros [v' [A B]].

     rewrite (sp_val _ _ _ AG) in A.

-    exploit loadind_correct; eauto with asmgen. { destruct TODO. }

+    exploit loadind_correct; eauto with asmgen.

     intros (rs2 & EXECS & Hrs'1 & Hrs'2).

     eapply exec_straight_body in EXECS. destruct EXECS as (l & Hlbi & EXECB).

     exists rs2, m1, l.

@@ -1479,7 +1477,23 @@ Proof.
     eapply agree_set_mreg; eauto with asmgen.

     intro Hep. simpl in Hep. inv Hep.

   - (* MBsetstack *)

-    destruct TODO.

+    simpl in EQ0.

+    unfold Mach.store_stack in H.

+    assert (Val.lessdef (ms src) (rs1 (preg_of src))). { eapply preg_val; eauto. }

+    exploit Mem.storev_extends; eauto. intros [m2' [A B]].

+    exploit storeind_correct; eauto with asmgen.

+    rewrite (sp_val _ _ _ AG) in A. eauto. intros [rs' [P Q]].

+

+    eapply exec_straight_body in P. destruct P as (l & Hlbi & EXECB).

+    exists rs', m2', l.

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

+    repeat (split; auto). 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.

+

+    eapply agree_undef_regs; eauto with asmgen.

+    simpl; intros. rewrite Q; auto with asmgen.

   - (* MBgetparam *)

     destruct TODO.

   - (* MBop *)

@@ -1733,7 +1747,7 @@ Proof.
   left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0.

   all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; 

             try (rewrite MBE; try discriminate); eauto).

-  + destruct TODO. (* MBbuiltin *)

+  + (* MBbuiltin *) destruct TODO.

   + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto.

 

 - (* internal function *)

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 08be374a..4abf1d52 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1277,16 +1277,16 @@ Proof.
 *)*)
 Qed.
 
-(*
+
 Lemma indexed_load_access_correct:
-  forall chunk (mk_instr: ireg -> offset -> instruction) rd m,
+  forall chunk (mk_instr: ireg -> offset -> basic) rd m,
   (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) ->
   forall (base: ireg) ofs k (rs: regset) v,
   Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> GPR31 -> rd <> PC ->
   exists rs',
-     exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m
+     exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m
   /\ rs'#rd = v
   /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r.
 Proof.
@@ -1296,11 +1296,8 @@ Proof.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC.
   unfold exec_load. rewrite B, LOAD. eauto. Simpl. 
-  split; intros; Simpl.
+  split; intros; Simpl. auto.
 Qed.
-*)
-
-Definition noscroll := 0.
 
 Lemma indexed_store_access_correct:
   forall chunk (mk_instr: ireg -> offset -> basic) r1 m,
@@ -1308,7 +1305,7 @@ Lemma indexed_store_access_correct:
      exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
   forall (base: ireg) ofs k (rs: regset) m',
   Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
-  base <> GPR31 -> r1 <> GPR31 -> IR r1 <> PC ->
+  base <> GPR31 -> r1 <> GPR31 -> r1 <> PC ->
   exists rs',
      exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
@@ -1318,13 +1315,10 @@ Proof.
   intros (base' & ofs' & rs' & A & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC.
-  unfold exec_store. rewrite B, C, STORE. eauto. eauto. 
-  destruct r1; try discriminate. contradiction NOT31'. auto. auto.
-(*   intros; Simpl. *)
+  unfold exec_store. rewrite B, C, STORE. eauto. eauto. auto.
+  intros; Simpl. rewrite C; auto.
 Qed.
 
-
-
 Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k c (rs: regset) m v,
   loadind base ofs ty dst k = OK c ->
@@ -1334,42 +1328,39 @@ Lemma loadind_correct:
      exec_straight ge c rs m k rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r.
-Proof. Admitted.
-(*   intros until v; intros TR LOAD NOT31. 
+Proof.
+  intros until v; intros TR LOAD NOT31. 
   assert (A: exists mk_instr,
-                c = indexed_memory_access mk_instr base ofs k
+                c = indexed_memory_access mk_instr base ofs :: k
              /\ forall base' ofs' rs',
-                   exec_instr ge fn (mk_instr base' ofs') rs' m =
+                   exec_basic_instr ge (mk_instr base' ofs') rs' m =
                    exec_load ge (chunk_of_type ty) rs' m (preg_of dst) base' ofs').
   { unfold loadind in TR.
     destruct ty, (preg_of dst); inv TR; econstructor; split; eauto. }
   destruct A as (mk_instr & B & C). subst c. 
   eapply indexed_load_access_correct; eauto with asmgen. 
-Qed. *)
+Qed.
 
-(*
 Lemma storeind_correct:
   forall (base: ireg) ofs ty src k c (rs: regset) m m',
   storeind src base ofs ty k = OK c ->
   Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' ->
   base <> GPR31 ->
   exists rs',
-     exec_straight ge fn c rs m k rs' m'
+     exec_straight ge c rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
-  intros until m'; intros TR STORE NOT31. 
+  intros until m'; intros TR STORE NOT31.
   assert (A: exists mk_instr,
-                c = indexed_memory_access mk_instr base ofs k
+                c = indexed_memory_access mk_instr base ofs :: k
              /\ forall base' ofs' rs',
-                   exec_instr ge fn (mk_instr base' ofs') rs' m =
+                   exec_basic_instr ge (mk_instr base' ofs') rs' m =
                    exec_store ge (chunk_of_type ty) rs' m (preg_of src) base' ofs').
   { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; split; eauto. }
   destruct A as (mk_instr & B & C). subst c. 
   eapply indexed_store_access_correct; eauto with asmgen. 
 Qed.
 
-*)
-
 Ltac bsimpl := unfold exec_bblock; simpl.
 
 Lemma Pget_correct: