Changing exec_straight to allow all instructions (prepare for MBtailcall proof)

4 files changed, 151 insertions, 57 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index c6c549cd..9da85fd0 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -506,6 +506,41 @@ Coercion PControl:  control >-> instruction.
 Definition code := list instruction.
 Definition bcode := list basic.
 
+Fixpoint basics_to_code (l: list basic) :=
+  match l with
+  | nil => nil
+  | bi::l => (PBasic bi)::(basics_to_code l)
+  end.
+
+Fixpoint code_to_basics (c: code) :=
+  match c with
+  | (PBasic i)::c =>
+    match code_to_basics c with
+    | None => None
+    | Some l => Some (i::l)
+    end
+  | _::c => None
+  | nil => Some nil
+  end.
+
+Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c.
+Proof.
+  intros. induction c as [|i c]; simpl; auto.
+  rewrite IHc. auto.
+Qed.
+
+Lemma code_to_basics_dist:
+  forall c c' l l',
+  code_to_basics c = Some l ->
+  code_to_basics c' = Some l' ->
+  code_to_basics (c ++ c') = Some (l ++ l').
+Proof.
+  induction c as [|i c]; simpl; auto.
+  - intros. inv H. simpl. auto.
+  - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate.
+    inv H. erewrite IHc; eauto. auto.
+Qed.
+
 (** 
   Asmblockgen will have to translate a Mach control into a list of instructions of the form
    i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index f72d8386..78aeba2a 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -925,7 +925,7 @@ Definition mb_remove_body (bb: MB.bblock) :=
 

 Lemma exec_straight_pnil:

   forall c rs1 m1 rs2 m2,

-  exec_straight tge c rs1 m1 (Pnop::nil) rs2 m2 ->

+  exec_straight tge c rs1 m1 (Pnop::gnil) rs2 m2 ->

   exec_straight tge c rs1 m1 nil rs2 m2.

 Proof.

   intros. eapply exec_straight_trans. eapply H. econstructor; eauto.

@@ -1006,9 +1006,20 @@ Proof.
           econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl.

         Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. simpl in H14. rewrite H14. auto.

         Simpl. simpl. subst. Simpl. simpl. unfold Val.offset_ptr. rewrite PCeq. auto.

-    + (* MBtailcall *)

-      destruct TODO.

-    + (* MBbuiltin *)

+    + (* MBtailcall *) destruct TODO.

+(*       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.

+      inv TBC. inv TIC. inv H0.

+

+      assert (f0 = f) by congruence.  subst f0.

+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).

+        eapply transf_function_no_overflow; eauto.

+      exploit Mem.loadv_extends. eauto. eexact H15. auto. simpl. intros [parent' [A B]].

+      destruct s1 as [rf|fid]; simpl in H13. 

+      * inv H1.

+      * monadInv H1. inv Hpstate. inv Hcur. assert (f = f1) by congruence. subst f1. clear FIND1. clear H14.

+        exploit make_epilogue_correct; eauto.

+ *)

+    + (* MBbuiltin (contradiction) *)

       assert (MB.exit bb' <> Some (MBbuiltin e l b)) by (apply Hbuiltin).

       rewrite <- H in H1. contradict H1; auto.

     + (* MBgoto *)

@@ -1040,17 +1051,44 @@ Definition mb_remove_first (bb: MB.bblock) :=
   {| MB.header := MB.header bb; MB.body := tail (MB.body bb); MB.exit := MB.exit bb |}.

 

 Lemma exec_straight_body:

-  forall c c' rs1 m1 rs2 m2,

+  forall c c' lc rs1 m1 rs2 m2,

   exec_straight tge c rs1 m1 c' rs2 m2 ->

-  exists l,

+  code_to_basics c = Some lc ->

+  exists l ll,

      c = l ++ c'

-  /\ exec_body tge l rs1 m1 = Next rs2 m2.

+  /\ code_to_basics l = Some ll

+  /\ exec_body tge ll rs1 m1 = Next rs2 m2.

 Proof.

   induction c; try (intros; inv H; fail).

-  intros. inv H.

-  - exists (a ::i nil). split; auto. simpl. rewrite H7. auto.

-  - apply IHc in H8. destruct H8 as (l & Hc & EXECB). subst.

-    exists (a ::i l). split; auto. simpl. rewrite H2. auto.

+  intros until m2. intros EXES CTB. inv EXES.

+  - exists (i1 ::g nil),(i1::nil). repeat (split; simpl; auto). rewrite H6. auto.

+  - inv CTB. destruct (code_to_basics c); try discriminate. inv H0.

+    eapply IHc in H7; eauto. destruct H7 as (l' & ll & Hc & CTB & EXECB). subst.

+    exists (i ::g l'),(i::ll). repeat (split; simpl; auto).

+      rewrite CTB. auto.

+      rewrite H1. auto.

+Qed.

+

+Lemma basics_to_code_app:

+  forall c l x ll,

+  basics_to_code c = l ++ basics_to_code x ->

+  code_to_basics l = Some ll ->

+  c = ll ++ x.

+Proof.

+  intros. apply (f_equal code_to_basics) in H.

+  erewrite code_to_basics_dist in H; eauto. 2: eapply code_to_basics_id.

+  rewrite code_to_basics_id in H. inv H. auto.

+Qed.

+

+Lemma basics_to_code_app2:

+  forall i c l x ll,

+  (PBasic i) :: basics_to_code c = l ++ basics_to_code x ->

+  code_to_basics l = Some ll ->

+  i :: c = ll ++ x.

+Proof.

+  intros until ll. intros.

+  exploit basics_to_code_app. instantiate (3 := (i::c)). simpl.

+  all: eauto.

 Qed.

 

 Lemma step_simu_basic:

@@ -1078,12 +1116,17 @@ Proof.
     rewrite (sp_val _ _ _ AG) in A.

     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.

+    eapply exec_straight_body in EXECS.

+      2: eapply code_to_basics_id; eauto.

+    destruct EXECS as (l & Hlbi & BTC & CTB & EXECB).

+    exists rs2, m1, Hlbi.

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

-    repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

+    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.

     eapply agree_set_mreg; eauto with asmgen.

     intro Hep. simpl in Hep. inv Hep.

@@ -1095,10 +1138,14 @@ Proof.
     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.

+    eapply exec_straight_body in P.

+      2: eapply code_to_basics_id; eauto.

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

+    exists rs', m2', ll.

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

-    repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

+    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.

@@ -1125,10 +1172,14 @@ Proof.
       instantiate (2 := rs1). rewrite DXP; eauto. congruence.

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

 

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

-      exists rs2, m1, l.

+      eapply exec_straight_body in P.

+        2: eapply code_to_basics_id; eauto.

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

+      exists rs2, m1, ll.

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

-      repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

+      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.

@@ -1147,10 +1198,14 @@ Proof.
         eapply S.

       intros EXES.

 

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

-      exists rs3, m1, l.

+      eapply exec_straight_body in EXES.

+        2: simpl. 2: erewrite code_to_basics_id; eauto.

+      destruct EXES as (l & ll & BTC & CTB & EXECB).

+      exists rs3, m1, ll.

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

-      repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.

+      repeat (split; auto).

+        eapply basics_to_code_app2; 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.

@@ -1213,7 +1268,7 @@ Proof.
     rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.

 Qed.

 

-Lemma exec_body_straight:

+(* Lemma exec_body_straight:

   forall l rs0 m0 rs1 m1,

   l <> nil ->

   exec_body tge l rs0 m0 = Next rs1 m1 ->

@@ -1228,7 +1283,7 @@ Proof.
   - intros until m1. intros _ EXEB. simpl in EXEB. simpl in IHl.

     destruct (exec_basic_instr tge i1 rs0 m0) eqn:EBI; try discriminate.

     econstructor; eauto. eapply IHl; eauto. discriminate.

-Qed.

+Qed. *)

 

 Lemma exec_body_pc:

   forall l rs1 m1 rs2 m2,

diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index 13100cdc..2b9fe5ef 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -678,17 +678,17 @@ Variable fn: function.
   Instructions are taken from the first list instead of being fetched
   from memory. *)
 
-Inductive exec_straight: list basic -> regset -> mem ->
-                         list basic -> regset -> mem -> Prop :=
+Inductive exec_straight: list instruction -> regset -> mem ->
+                         list instruction -> regset -> mem -> Prop :=
   | exec_straight_one:
       forall i1 c rs1 m1 rs2 m2,
       exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 ->
-      exec_straight (i1 :: c) rs1 m1 c rs2 m2
+      exec_straight ((PBasic i1) ::g c) rs1 m1 c rs2 m2
   | exec_straight_step:
       forall i c rs1 m1 rs2 m2 c' rs3 m3,
       exec_basic_instr ge i rs1 m1 = Next rs2 m2 ->
       exec_straight c rs2 m2 c' rs3 m3 ->
-      exec_straight (i :: c) rs1 m1 c' rs3 m3.
+      exec_straight ((PBasic i) :: c) rs1 m1 c' rs3 m3.
 
 Inductive exec_control_rel: option control -> bblock -> regset -> mem ->
                              regset -> mem -> Prop :=
@@ -705,21 +705,23 @@ Inductive exec_bblock_rel: bblock -> regset -> mem -> regset -> mem -> Prop :=
       exec_bblock_rel b rs1 m1 rs2 m2.
 
 Lemma exec_straight_body:
-  forall c rs1 m1 rs2 m2,
+  forall c l rs1 m1 rs2 m2,
   exec_straight c rs1 m1 nil rs2 m2 ->
-  exec_body ge c rs1 m1 = Next rs2 m2.
+  code_to_basics c = Some l ->
+  exec_body ge l rs1 m1 = Next rs2 m2.
 Proof.
   induction c as [|i c].
-  - intros. inv H.
-  - intros. inv H.
-    + simpl. rewrite H7. auto.
-    + apply IHc in H8. rewrite <- H8. simpl. rewrite H2. auto.
+  - intros until m2. intros EXES CTB. inv EXES.
+  - intros until m2. intros EXES CTB. inv EXES.
+    + inv CTB. simpl. rewrite H6. auto.
+    + inv CTB. destruct (code_to_basics c); try discriminate. inv H0. eapply IHc in H7; eauto.
+      rewrite <- H7. simpl. rewrite H1. auto.
 Qed.
 
 (*     + contradict H4. generalize i1. induction c; simpl; try discriminate.
         intros i0 X; inversion X. subst. eapply IHc. eauto. *)
 
-Theorem exec_straight_bblock:
+(* Theorem exec_straight_bblock:
   forall rs1 m1 rs2 m2 rs3 m3 b,
   exec_straight (body b) rs1 m1 nil rs2 m2 ->
   exec_control_rel (exit b) b rs2 m2 rs3 m3 ->
@@ -728,7 +730,7 @@ Proof.
   intros.
   econstructor; eauto. unfold exec_bblock. erewrite exec_straight_body; eauto.
   inv H0. auto.
-Qed.
+Qed. *)
 
 Lemma exec_straight_trans:
   forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
@@ -747,7 +749,7 @@ Lemma exec_straight_two:
   exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 ->
   rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
   rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one ->
-  exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
+  exec_straight (i1 ::g i2 ::g c) rs1 m1 c rs3 m3.
 Proof.
   intros. apply exec_straight_step with rs2 m2; auto.
   apply exec_straight_one; auto.
@@ -761,7 +763,7 @@ Lemma exec_straight_three:
   rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
   rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one ->
   rs4#PC = Val.offset_ptr rs3#PC Ptrofs.one ->
-  exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
+  exec_straight (i1 ::g i2 ::g i3 ::g c) rs1 m1 c rs4 m4.
 Proof.
   intros. apply exec_straight_step with rs2 m2; auto.
   eapply exec_straight_two; eauto.
@@ -847,7 +849,7 @@ Proof.
     erewrite exec_basic_instr_pc; eauto.
 Qed.
 
-Lemma exec_straight_through:
+(* Lemma exec_straight_through:
   forall c i b lb rs1 m1 rs2 m2 rs2' m2',
   bblock_basic_ctl c i = b ->
   exec_straight c rs1 m1 nil rs2 m2 ->
@@ -864,11 +866,11 @@ Proof.
     + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto.
     + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto.
 Qed.
-
+ *)
 Lemma exec_straight_through_singleinst:
   forall a b rs1 m1 rs2 m2 rs2' m2' lb,
   bblock_single_inst (PBasic a) = b ->
-  exec_straight (a::nil) rs1 m1 nil rs2 m2 ->
+  exec_straight (a ::g nil) rs1 m1 nil rs2 m2 ->
   nextblock b rs2 = rs2' -> m2 = m2' ->
   exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'.
 Proof.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 74b8f8b5..40e3f444 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -320,7 +320,7 @@ Ltac ArgsInv :=
 
 Definition bla := 0.
 
-Inductive exec_straight_opt: list basic -> regset -> mem -> list basic -> regset -> mem -> Prop :=
+Inductive exec_straight_opt: list instruction -> regset -> mem -> list instruction -> regset -> mem -> Prop :=
   | exec_straight_opt_refl: forall c rs m,
       exec_straight_opt c rs m c rs m
   | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2,
@@ -1235,8 +1235,8 @@ Lemma indexed_memory_access_correct:
   forall mk_instr base ofs k rs m,
   base <> GPR31 ->
   exists base' ofs' rs',
-     exec_straight_opt (indexed_memory_access mk_instr base ofs :: k) rs m
-                       (mk_instr base' ofs' :: k) rs' m
+     exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m
+                       (mk_instr base' ofs' ::g k) rs' m
   /\ Val.offset_ptr rs'#base' (eval_offset ge ofs') = Val.offset_ptr rs#base ofs
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
@@ -1286,7 +1286,7 @@ Lemma indexed_load_access_correct:
   Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> GPR31 -> rd <> PC ->
   exists rs',
-     exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m
+     exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m
   /\ rs'#rd = v
   /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r.
 Proof.
@@ -1307,7 +1307,7 @@ Lemma indexed_store_access_correct:
   Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
   base <> GPR31 -> r1 <> GPR31 -> r1 <> PC ->
   exists rs',
-     exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m'
+     exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
   intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31' NOTPC.
@@ -1325,7 +1325,7 @@ Lemma loadind_correct:
   Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> GPR31 ->
   exists rs',
-     exec_straight ge 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.
@@ -1347,7 +1347,7 @@ Lemma storeind_correct:
   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 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 STORE NOT31.
@@ -1367,7 +1367,7 @@ Lemma Pget_correct:
   forall (dst: gpreg) (src: preg) k (rs: regset) m,
   src = RA ->
   exists rs',
-     exec_straight ge (Pget dst src :: k) rs m k rs' m
+     exec_straight ge (Pget dst src ::g k) rs m k rs' m
   /\ rs'#dst = rs#src
   /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.
 Proof.
@@ -1401,7 +1401,7 @@ Lemma loadind_ptr_correct:
   Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> GPR31 ->
   exists rs',
-     exec_straight ge (loadind_ptr base ofs dst :: k) rs m k rs' m
+     exec_straight ge (loadind_ptr base ofs dst ::g k) rs m k rs' m
   /\ rs'#dst = v
   /\ forall r, r <> PC -> r <> GPR31 -> r <> dst -> rs'#r = rs#r.
 Proof.
@@ -1414,7 +1414,7 @@ Lemma storeind_ptr_correct:
   Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
   base <> GPR31 -> src <> GPR31 ->
   exists rs',
-     exec_straight ge (storeind_ptr src base ofs :: k) rs m k rs' m'
+     exec_straight ge (storeind_ptr src base ofs ::g k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
   intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen.
@@ -1544,17 +1544,20 @@ 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,
-  load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
-  load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) ->
+  Mach.load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
+  Mach.load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) ->
   Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
   agree ms (Vptr stk soff) rs ->
   Mem.extends m tm ->
   match_stack ge0 cs ->
   exists rs', exists tm',
-     exec_straight ge fn (make_epilogue f k) rs tm k rs' tm'
+     exec_straight ge (make_epilogue f k) rs tm k rs' tm'
   /\ agree ms (parent_sp cs) rs'
   /\ Mem.extends m' tm'
   /\ rs'#RA = parent_ra cs
@@ -1600,8 +1603,7 @@ Proof.
   intros. Simpl.
   rewrite C2; auto.
 Qed.
-
-*)
+ *)
 End CONSTRUCTORS.