diff options
-rw-r--r-- | mppa_k1c/PostpassScheduling.v | 34 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingProof.v | 116 |
2 files changed, 110 insertions, 40 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 8ec72f90..381e1214 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -10,29 +10,33 @@ (* *) (* *********************************************************************) +Require Import Coqlib Errors AST. Require Import Asmblock. +Local Open Scope error_monad_scope. + (** Oracle taking as input a basic block, - returns a basic block with its instruction reordered *) + returns a basic block with its instructions reordered *) Axiom schedule: bblock -> bblock. -(** Oracle taking as input a basic block - splits it into several bblocks (representing bundles *) -Axiom split: bblock -> list bblock. - -(* TODO - separate the postpass_schedule in two phases *) +(* TODO - implement the verificator *) +Definition transf_block (b : bblock) : res bblock := OK (schedule b). -Definition postpass_schedule (lb : list bblock) : list bblock := +Fixpoint transf_blocks (lb : list bblock) : res (list bblock) := match lb with - | nil => nil - | (cons b lb) => split (schedule b) ++ lb + | nil => OK nil + | (cons b lb) => + do lb' <- transf_blocks lb; + do b' <- transf_block b; + OK (b' :: lb') end. -Definition transf_function (f: function) : function := - mkfunction (fn_sig f) (postpass_schedule (fn_blocks f)). +Definition transf_function (f: function) : res function := + do lb <- transf_blocks (fn_blocks f); + OK (mkfunction (fn_sig f) lb). -Definition transf_fundef (f: fundef) : fundef := - AST.transf_fundef transf_function f. +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. -Definition transf_program (p: program) : program := - AST.transform_program transf_fundef p.
\ No newline at end of file +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p.
\ No newline at end of file diff --git a/mppa_k1c/PostpassSchedulingProof.v b/mppa_k1c/PostpassSchedulingProof.v index 3e3201bb..4f85444f 100644 --- a/mppa_k1c/PostpassSchedulingProof.v +++ b/mppa_k1c/PostpassSchedulingProof.v @@ -21,14 +21,24 @@ Require Import PostpassScheduling. (** * Relational characterization of the transformation *)
Definition match_prog (p tp: Asmblock.program) :=
- match_program (fun _ f tf => tf = transf_fundef f) eq p tp.
+ match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
- forall p, match_prog p (transf_program p).
+ forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
- intros. eapply match_transform_program; eauto.
+ intros. eapply match_transform_partial_program; eauto.
Qed.
+Inductive transf_block_spec (ge: Genv.t fundef unit) (f: function) (bb tbb: bblock) :=
+ | transf_block_spec_intro:
+ (forall rs m,
+ exec_bblock ge f bb rs m = exec_bblock ge f tbb rs m) ->
+ transf_block_spec ge f bb tbb.
+
+Axiom transf_block_inv:
+ forall ge f bb tbb,
+ transf_block bb = OK tbb -> transf_block_spec ge f bb tbb.
+
Section PRESERVATION.
Variables prog tprog: program.
@@ -39,59 +49,115 @@ Let tge := Genv.globalenv tprog. Lemma symbols_preserved:
forall id,
Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (Genv.find_symbol_transf TRANSL).
+Proof (Genv.find_symbol_match TRANSL).
Lemma senv_preserved:
Senv.equiv ge tge.
-Proof (Genv.senv_transf TRANSL).
+Proof (Genv.senv_match TRANSL).
Lemma functions_translated:
forall v f,
Genv.find_funct ge v = Some f ->
- Genv.find_funct tge v = Some (transf_fundef f).
-Proof (Genv.find_funct_transf TRANSL).
+ 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 ->
- Genv.find_funct_ptr tge v = Some (transf_fundef f).
-Proof (Genv.find_funct_ptr_transf TRANSL).
+ 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) ->
+ transf_function f = OK tf ->
+ Genv.find_funct_ptr tge fb = Some (Internal tf).
+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.
-(** TODO - continue *)
+Lemma prog_main_preserved:
+ prog_main tprog = prog_main prog.
+Proof (match_program_main TRANSL).
+
+Lemma prog_main_address_preserved:
+ (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) =
+ (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero).
+Proof.
+ unfold Genv.symbol_address. rewrite symbols_preserved.
+ rewrite prog_main_preserved. auto.
+Qed.
-(* Lemma transf_initial_states:
+Lemma transf_initial_states:
forall st1, initial_state prog st1 ->
exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
intros. inv H.
econstructor; split.
- eapply initial_state_intro with (m0 := m0).
- eapply (Genv.init_mem_transf TRANSL); eauto.
-(* rewrite (match_program_main TRANSL), symbols_preserved; eauto.
- apply function_ptr_translated; auto.
- rewrite sig_function_translated. auto. *)
- constructor; auto. constructor.
+ - eapply initial_state_intro.
+ eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+ - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto.
Qed.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
- intros. inv H0. inv H. inv H5. econstructor; eauto.
+ intros. inv H0. inv H. econstructor; eauto.
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 tbb,
+ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb
+ /\ transf_block bb = OK tbb.
+Proof.
+Admitted.
+
+Lemma transf_exec_bblock:
+ forall f tf bb rs m rs' m',
+ exec_bblock ge f bb rs m = Next rs' m' ->
+ transf_function f = OK tf ->
+ exec_bblock tge tf bb rs m = Next rs' m'.
+Proof.
+Admitted.
+
+Axiom TODO: False.
+
+Theorem transf_step_correct:
+ forall s1 t s2, step ge s1 t s2 ->
+ forall s1' (MS: match_states s1 s1'),
+ (exists s2', step tge s1' t s2' /\ match_states s2 s2').
+Proof.
+ induction 1; intros; inv MS.
+ - exploit function_ptr_translated; eauto. intros (tf & A & B). monadInv B.
+ exploit transf_find_bblock; eauto. intros (tbb & C & D).
+ exists (State rs' m'); split; try (constructor; auto).
+ econstructor; eauto.
+ exploit transf_block_inv; eauto. intros E. inv E.
+ erewrite <- H3.
+ eapply transf_exec_bblock; eauto.
+ - destruct TODO.
+ - destruct TODO.
+Admitted.
+
Theorem transf_program_correct:
- forward_simulation (Linear.semantics prog) (Linear.semantics tprog).
+ forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
Proof.
- eapply forward_simulation_opt.
- apply senv_preserved.
- eexact transf_initial_states.
- eexact transf_final_states.
- eexact transf_step_correct.
+ eapply forward_simulation_step.
+ - apply senv_preserved.
+ - apply transf_initial_states.
+ - apply transf_final_states.
+ - apply transf_step_correct.
Qed.
- *)
+
End PRESERVATION.
|