Start of the postpasschedproof, redefining verify schedule lemmas

1 files changed, 129 insertions, 90 deletions

diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v
index 86a160bd..22daede9 100644
--- a/aarch64/PostpassSchedulingproof.v
+++ b/aarch64/PostpassSchedulingproof.v
@@ -128,14 +128,15 @@ Proof.
   rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq).
   rewrite <- Zplus_mod. auto.
 Qed.
-
+*)
 Section PRESERVATION_ASMBLOCK.
 
 Variables prog tprog: program.
+Variable lk: aarch64_linker.
 Hypothesis TRANSL: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
-
+(*
 Lemma transf_function_no_overflow:
   forall f tf,
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
@@ -143,7 +144,7 @@ Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
   omega.
 Qed.
-
+*)
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
@@ -152,21 +153,21 @@ Proof (Genv.find_symbol_match TRANSL).
 Lemma senv_preserved:
   Senv.equiv ge tge.
 Proof (Genv.senv_match TRANSL).
-
+(*
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
 Proof (Genv.find_funct_transf_partial TRANSL).
-
+*)
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   exists tf,
   Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
 Proof (Genv.find_funct_ptr_transf_partial TRANSL).
-
+(*
 Lemma functions_transl:
   forall fb f tf,
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
@@ -176,7 +177,7 @@ Proof.
   intros. exploit function_ptr_translated; eauto.
   intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto.
 Qed.
-
+*)
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
       forall s1 s2, s1 = s2 -> match_states s1 s2.
@@ -211,7 +212,7 @@ Proof.
   intros. inv H0. inv H. econstructor; eauto.
 Qed.
 
-Lemma tail_find_bblock:
+(* Lemma tail_find_bblock:
   forall lbb pos bb,
   find_bblock pos lbb = Some bb ->
   exists c, code_tail pos lbb (bb::c).
@@ -226,9 +227,9 @@ Proof.
       enough (pos = pos - size a + size a) as ->.
       apply code_tail_S; auto.
       omega.
-Qed.
+Qed. *)
 
-Lemma code_tail_head_app:
+(* Lemma code_tail_head_app:
   forall l pos c1 c2,
   code_tail pos c1 c2 ->
   code_tail (pos + size_blocks l) (l++c1) c2.
@@ -236,51 +237,81 @@ Proof.
   induction l.
   - intros. simpl. rewrite Z.add_0_r. auto.
   - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption.
-Qed.
+Qed. *)
 
-Lemma transf_blocks_verified:
+(* Lemma transf_blocks_verified:
   forall c tc pos bb c',
   transf_blocks c = OK tc ->
   code_tail pos c (bb::c') ->
   exists lbb,
-     verified_schedule bb = OK lbb
-  /\ exists tc', code_tail pos tc (lbb ++ tc').
+     verified_schedule bb = OK lbb.
 Proof.
   induction c; intros.
   - simpl in H. inv H. inv H0.
   - inv H0.
-    + monadInv H. exists x0.
-      split; simpl; auto. eexists; eauto. econstructor; eauto.
+    + monadInv H. exists x0; eauto.
     + unfold transf_blocks in H. fold transf_blocks in H. monadInv H.
       exploit IHc; eauto.
-      intros (lbb & TRANS & tc' & TAIL).
-(*       monadInv TRANS. *)
-      repeat eexists; eauto.
-      erewrite verified_schedule_size; eauto.
-      apply code_tail_head_app.
-      eauto.
-Qed.
+Qed. *)
 
 Lemma transf_find_bblock:
   forall ofs f bb tf,
   find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
   transf_function f = OK tf ->
-  exists lbb,
-     verified_schedule bb = OK lbb
-  /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c).
+  exists tbb,
+     verified_schedule bb = OK tbb
+     /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb.
 Proof.
   intros.
   monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.
-  monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL).
-  eapply transf_blocks_verified; eauto.
+  monadInv EQ. simpl in *.
+  generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0.
+  induction (fn_blocks f).
+  - intros. simpl in *. discriminate.
+  - intros. simpl in *.
+  monadInv EQ0. simpl.
+  destruct (zlt z 0); try discriminate.
+  destruct (zeq z 0).
+  + inv H. eauto.
+  + monadInv EQ0.
+   exploit IHb; eauto.
+    intros (tbb & SCH & FIND).
+    eexists; split; eauto.
+    inv FIND.
+    unfold verify_size in EQ0.
+    destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.
+    rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.
+    reflexivity.
 Qed.
 
+Lemma transf_exec_bblock:
+  forall f tf bb ofs t rs m rs' m',
+  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
+  transf_function f = OK tf ->
+  exec_bblock lk ge f bb rs m t rs' m' ->
+  exists tbb,
+    exec_bblock lk tge tf tbb rs m t rs' m'
+    /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb.
+Proof.
+  intros. inv H1.
+  monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try (inv EQ0; fail). inv EQ0.
+  monadInv EQ. simpl in *.
+  generalize (Ptrofs.unsigned ofs) H x0 g EQ0; clear ofs H x0 g EQ0.
+  induction (fn_blocks f).
+  - intros. simpl in *. discriminate.
+  - intros. simpl in *.
+  monadInv EQ0. simpl.
+  destruct (zlt z 0); try discriminate.
+  destruct (zeq z 0).
+  + inv H.
+Admitted.
+
 Lemma symbol_address_preserved:
   forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs.
 Proof.
   intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity.
 Qed.
-
+(*
 Lemma head_tail {A: Type}:
   forall (l: list A) hd, hd::l = hd :: (tail (hd::l)).
 Proof.
@@ -427,56 +458,81 @@ Proof.
   monadInv EQ0. simpl. eapply label_pos_preserved; eauto.
 Qed.
 
-Lemma transf_exec_control:
-  forall f tf ex rs m,
-  transf_function f = OK tf ->
-  exec_control ge f ex rs m = exec_control tge tf ex rs m.
+Lemma transf_exec_exit:
+  forall f sz cfi t rs m rs' m',
+  (exec_cfi ge f cfi (incrPC sz rs) m = Next rs' m') ->
+  exec_exit ge f sz rs m (Some (PCtlFlow cfi)) t rs' m'.
 Proof.
-  intros. destruct ex; simpl; auto.
-  assert (ge = Genv.globalenv prog). auto.
+  intros.
+  destruct t.
+  - constructor; auto.
+  - congruence.
+  destruct ex; try destruct c; simpl.
+  - generalize cfi_step. intros. apply H0.
+  
+  monadInv H. monadInv EQ.
+  destruct (zlt Ptrofs.max_unsigned _); try discriminate.
+  monadInv EQ0. simpl.
+   assert (ge = Genv.globalenv prog). auto.
   assert (tge = Genv.globalenv tprog). auto.
   pose symbol_address_preserved.
+  
+
+  exists rs; exists m. apply cfi_step. inv H.
+  destruct cfi; simpl; eauto.
+  assert (ge = Genv.globalenv prog); auto;
+  assert (tge = Genv.globalenv tprog); auto;
+  pose symbol_address_preserved; simpl.
+  - 
+  constructor.
+  unfold exec_exit.
   exploreInst; simpl; auto; try congruence;
     unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto.
 Qed.
-
-Lemma transf_exec_basic_instr:
-  forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.
+*)
+Lemma transf_exec_basic:
+  forall i rs m, exec_basic lk ge i rs m = exec_basic lk tge i rs m.
 Proof.
   intros. pose symbol_address_preserved.
-  unfold exec_basic_instr. unfold bstep. exploreInst; simpl; auto; try congruence.
-  unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
+  unfold exec_basic. 
+  destruct i; simpl; auto; try congruence.
 Qed.
 
 Lemma transf_exec_body:
-  forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m.
+  forall bdy rs m, exec_body lk ge bdy rs m = exec_body lk tge bdy rs m.
 Proof.
   induction bdy; intros.
   - simpl. reflexivity.
-  - simpl. rewrite transf_exec_basic_instr.
-    destruct (exec_basic_instr _ _ _); auto.
+  - simpl. rewrite transf_exec_basic.
+    destruct (exec_basic _ _ _); auto.
 Qed.
 
-Lemma transf_exec_bblock:
-  forall f tf bb rs m,
+(* Lemma transf_exec_bblock:
+  forall f tf bb b ofs t rs m rs' m',
+  rs PC = Vptr b ofs ->
   transf_function f = OK tf ->
-  exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m.
-Proof.
-  intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto.
-  eapply transf_exec_control; eauto.
-Qed.
-
+  exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk tge tf bb rs m t rs' m'.
+Proof.
+  intros. monadInv H. monadInv EQ. pose symbol_address_preserved.
+  simpl in *.
+  destruct (zlt Ptrofs.max_unsigned (size_blocks x0)); try discriminate.
+  monadInv EQ0. unfold transf_blocks in *. destruct f. simpl in *.
+  generalize H0 EQ1; clear H0 EQ1.
+  induction (fn_blocks).
+  - intros. monadInv EQ1. auto. admit.
+  - intros. apply IHb.
+Qed. *)
+(*
 Lemma transf_step_simu:
-  forall tf b lbb ofs c tbb rs m rs' m',
+  forall f b bb ofs c rs m t rs' m' rs1 m1,
   Genv.find_funct_ptr tge b = Some (Internal tf) ->
-  size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned ->
+  (* size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> *)
   rs PC = Vptr b ofs ->
-  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) ->
-  concat_all lbb = OK tbb ->
-  exec_bblock tge tf tbb rs m = Next rs' m' ->
-  plus step tge (State rs m) E0 (State rs' m').
+  exec_body lk ge (body bi) rs m = Next rs1 m1 ->
+  exec_exit ge f (Ptrofs.repr (size bb)) rs1 m1 (exit bb) t rs' m' ->
+  plus (step lk) tge (State rs m) t (State rs' m').
 Proof.
-  induction lbb.
+  induction bb'.
   - intros until m'. simpl. intros. discriminate.
   - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB.
     destruct lbb.
@@ -490,47 +546,28 @@ Proof.
     eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto.
     eapply code_tail_next_int; eauto.
 Qed.
-
+*)
 Theorem transf_step_correct:
-  forall s1 t s2, step ge s1 t s2 ->
+  forall s1 t s2, step lk ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1'),
-  (exists s2', plus step tge s1' t s2' /\ match_states s2 s2').
+  (exists s2', step lk tge s1' t s2' /\ match_states s2 s2').
 Proof.
   induction 1; intros; inv MS.
-  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
-    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
-    exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). inv CONC. rename H3 into CONC.
-    assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).
-      eapply transf_function_no_overflow; eauto. 
-
-    erewrite transf_exec_bblock in H2; eauto.
-    unfold bblock_simu in BBEQ. rewrite BBEQ in H2; try congruence.
-    exists (State rs' m'). split; try (constructor; auto).
-    eapply transf_step_simu; eauto.
-
-  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
-    exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
-    exploit verified_schedule_builtin_idem; eauto. intros. subst lbb.
-
-    remember (State (nextblock _ _) _) as s'. exists s'.
-    split; try constructor; auto.
-    eapply plus_one. subst s'.
-    eapply exec_step_builtin.
-      3: eapply find_bblock_tail. simpl in TAIL. 3: eauto.
-      all: eauto.
-    eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto.
-    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-
+  - inversion H2.
+  exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
+    exploit transf_exec_bblock; eauto. intros (lbb & EBB & FIND).
+    exists (State rs' m').
+    split; try (econstructor; eauto).
   - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
     remember (State _ m') as s'. exists s'. split; try constructor; auto.
-    subst s'. eapply plus_one. eapply exec_step_external; eauto.
+    subst s'. eapply exec_step_external; eauto.
     eapply external_call_symbols_preserved; eauto. apply senv_preserved.
 Qed.
 
 Theorem transf_program_correct_Asmblock: 
-  forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
+  forward_simulation (Asmblock.semantics lk prog) (Asmblock.semantics lk tprog).
 Proof.
-  eapply forward_simulation_plus.
+  eapply forward_simulation_step.
   - apply senv_preserved.
   - apply transf_initial_states.
   - apply transf_final_states.
@@ -539,8 +576,9 @@ Qed.
 
 End PRESERVATION_ASMBLOCK.
 
-Require Import Asmvliw.
+Require Import Asm.
 
+(*
 Lemma verified_par_checks_alls_bundles lb x: forall bundle,
   verify_par lb = OK x ->
   List.In bundle lb -> verify_par_bblock bundle = OK tt.
@@ -605,8 +643,9 @@ Proof.
   destruct (zlt ofs 0); try congruence.
   destruct (zeq ofs 0); eauto.
   intros X; inversion X; eauto.
-Qed.
+Qed.*)
 
+(*
 Section PRESERVATION_ASMVLIW.
 
 Variables prog tprog: program.