diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | mppa_k1c/lib/RTLpathLivegen.v | 19 | ||||
| -rw-r--r-- | mppa_k1c/lib/RTLpathLiveproofs.v | 66 |
3 files changed, 69 insertions, 18 deletions
@@ -849,7 +849,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure EXECUTE=k1-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __K1C_COS__ SIMU=k1-cluster -- -BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v RTLpathLivegen.v RTLpathSE_theory.v\\ +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v RTLpathLivegen.v RTLpathLiveproofs.v RTLpathSE_theory.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ diff --git a/mppa_k1c/lib/RTLpathLivegen.v b/mppa_k1c/lib/RTLpathLivegen.v index 58393f78..2c886774 100644 --- a/mppa_k1c/lib/RTLpathLivegen.v +++ b/mppa_k1c/lib/RTLpathLivegen.v @@ -359,7 +359,7 @@ Qed. Local Hint Resolve symbols_preserved senv_preserved. -Theorem transf_program_RTL_correct: +Lemma transf_program_RTL_correct: forward_simulation (RTL.semantics prog) (RTL.semantics (program_RTL tprog)). Proof. eapply forward_simulation_step with (match_states:=fun (s1 s2:RTL.state) => s1=s2); simpl; eauto. @@ -417,4 +417,21 @@ Proof. + eapply RTLpath_complete. Qed. + +(* Properties used in hypothesis of [RTLpathLiveproofs.step_eqlive] theorem *) +Theorem all_fundef_are_checked b f: + Genv.find_funct_ptr tpge b = Some f -> liveness_ok_fundef f. +Proof. + unfold match_prog, match_program in TRANSL. + unfold Genv.find_funct_ptr, tpge; simpl; intro X. + destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence. + destruct y as [tf0|]; try congruence. + inversion X as [H1]. subst. clear X. + remember (@Gfun fundef unit f) as f2. + destruct H as [ctx' f1 f2 H0|]; try congruence. + inversion Heqf2 as [H2]. subst; clear Heqf2. + exploit transf_fundef_correct; eauto. + intuition. +Qed. + End PRESERVATION. diff --git a/mppa_k1c/lib/RTLpathLiveproofs.v b/mppa_k1c/lib/RTLpathLiveproofs.v index c022e950..ea182d84 100644 --- a/mppa_k1c/lib/RTLpathLiveproofs.v +++ b/mppa_k1c/lib/RTLpathLiveproofs.v @@ -306,6 +306,16 @@ Proof. eapply all_fundef_are_checked; eauto. Qed. +Lemma find_function_eqlive alive ros rs1 rs2: + eqlive_reg (ext alive) rs1 rs2 -> + reg_sum_mem ros alive = true -> + find_function pge ros rs1 = find_function pge ros rs2. +Proof. + intros EQLIVE. + destruct ros; simpl; auto. + intros H; erewrite (EQLIVE r); eauto. +Qed. + Lemma inst_checker_from_iinst_checker i sp rs m st pm alive: istep ge i sp rs m = Some st -> inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt). @@ -328,7 +338,7 @@ Proof. rewrite regset_add_spec. intuition subst. Qed. -Lemma inst_checker_eqlive f sp alive pc i rs1 rs2 m stk1 stk2 t s1: +Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1: list_forall2 eqlive_stackframes stk1 stk2 -> eqlive_reg (ext alive) rs1 rs2 -> liveness_ok_function f -> @@ -339,7 +349,10 @@ Lemma inst_checker_eqlive f sp alive pc i rs1 rs2 m stk1 stk2 t s1: Proof. intros STACKS EQLIVE LIVENESS PC; destruct 1 as [i' sp pc rs1 m st1| - sp pc rs1 m sig ros args res pc' fd| | | | + sp pc rs1 m sig ros args res pc' fd| + st1 pc rs1 m sig ros args fd m'| + sp pc rs1 m ef args res pc' vargs t vres m'| + sp pc rs1 m arg tbl n pc' | st1 pc rs1 m optr m']; try_simplify_someHyps. + (* istate *) @@ -363,18 +376,24 @@ Proof. rewrite <- MEM, <- PC2. eapply eqlive_states_intro; eauto. + (* Icall *) - repeat inversion_ASSERT. intros. - exploit exit_checker_eqlive_ext1; eauto. - intros (path & PATH & EQLIVE2). - eexists; split. - - eapply exec_Icall; eauto. - admit. - - erewrite eqlive_reg_listmem; eauto. - eapply eqlive_states_call; eauto. - eapply find_function_liveness; eauto. - repeat (econstructor; eauto). + repeat inversion_ASSERT. intros. + exploit exit_checker_eqlive_ext1; eauto. + intros (path & PATH & EQLIVE2). + eexists; split. + - eapply exec_Icall; eauto. + erewrite <- find_function_eqlive; eauto. + - erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness; eauto. + repeat (econstructor; eauto). + (* Itailcall *) - admit. + repeat inversion_ASSERT. intros. + eexists; split. + - eapply exec_Itailcall; eauto. + erewrite <- find_function_eqlive; eauto. + - erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness; eauto. + (* Ibuiltin *) admit. + (* Ijumptable *) @@ -389,7 +408,6 @@ Proof. * eapply eqlive_states_return; eauto. Admitted. - Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2: path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 -> list_forall2 eqlive_stackframes stk1 stk2 -> @@ -401,11 +419,27 @@ Proof. intros STEP STACKS EQLIVE LIVE PC. unfold liveness_ok_function in LIVE. exploit LIVE; eauto. - clear LIVE; unfold path_checker. + unfold path_checker. inversion_SOME res; (* destruct res as [alive pc']. *) intros ICHECK. (* simpl. *) inversion_SOME i; intros PC'. destruct STEP as [st ISTEPS CONT|]. -Admitted. + - (* early_exit *) + intros; exploit ipath_checker_eqlive_stopped; eauto. + destruct 1 as (path2 & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]). + repeat (econstructor; simpl; eauto). + rewrite <- MEM, <- PC2. + eapply eqlive_states_intro; eauto. + - (* normal_exit *) + intros; exploit ipath_checker_eqlive_normal; eauto. + destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]). + exploit ipath_checker_isteps_continue; eauto. + intros PC3; rewrite <- PC3, <- PC2 in * |-. + exploit inst_checker_eqlive; eauto. + intros (s2 & LAST_STEP & EQLIVE2). + eexists; split; eauto. + eapply exec_normal_exit; eauto. + rewrite <- PC3, <- MEM; auto. +Qed. Theorem step_eqlive t s1 s1' s2: step ge pge s1 t s1' -> |