diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | scheduling/BTL_Livecheck.v | 44 | ||||
-rw-r--r-- | scheduling/BTL_Scheduler.v | 0 | ||||
-rw-r--r-- | scheduling/BTL_Schedulerproof.v | 0 | ||||
-rw-r--r-- | scheduling/BTLmatchRTL.v | 12 | ||||
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 12 | ||||
-rw-r--r-- | scheduling/RTLtoBTL.v | 3 | ||||
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 63 |
8 files changed, 99 insertions, 37 deletions
@@ -144,7 +144,7 @@ SCHEDULING= \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ - BTL_SEtheory.v + BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v BTL_SEtheory.v # C front-end modules (in cfrontend/) diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v new file mode 100644 index 00000000..2baba025 --- /dev/null +++ b/scheduling/BTL_Livecheck.v @@ -0,0 +1,44 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad. +Require Import Errors RTL BTL BTLmatchRTL. + +(** TODO: adapt stuff RTLpathLivegen *) + +Definition liveness_checker (f: BTL.function): res unit := OK tt. (* TODO: implement this ! *) + +Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. + +(** TODO: adapt stuff RTLpathLivegenproof *) + +Local Notation ext alive := (fun r => Regset.In r alive). + +Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live). +Proof. + destruct (Pos.eq_dec r1 r2). + - subst. intuition; eapply Regset.add_1; auto. + - intuition. + * right. eapply Regset.add_3; eauto. + * eapply Regset.add_2; auto. +Qed. + +Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop := + forall r, (alive r) -> rs1#r = rs2#r. + +(* continue to adapt stuff RTLpathLivegenproof *) + +Section FSEM_SIMULATES_CFGSEM. + +Variable prog: BTL.program. + +Let ge := Genv.globalenv prog. + +Hypothesis liveness_checker_correct: forall b f, Genv.find_funct_ptr ge b = Some (Internal f) -> liveness_ok_function f. + +Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog). +Proof. + exploit liveness_checker_correct. +Admitted. + +End FSEM_SIMULATES_CFGSEM. + + diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/scheduling/BTL_Scheduler.v diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/scheduling/BTL_Schedulerproof.v diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v index 23ff6681..8994579d 100644 --- a/scheduling/BTLmatchRTL.v +++ b/scheduling/BTLmatchRTL.v @@ -223,18 +223,6 @@ Record match_function dupmap f f': Prop := { preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' }. -Inductive match_fundef: BTL.fundef -> RTL.fundef -> Prop := - | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') - | match_External ef: match_fundef (External ef) (External ef). - -Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := - | match_stackframe_intro - dupmap res f sp pc rs f' pc' - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_stackframes (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). - - (** * Shared verifier between RTL -> BTL and BTL -> RTL *) Local Open Scope error_monad_scope. diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 765f9cad..75f67d51 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -6,6 +6,18 @@ Require Import Errors Linking BTLtoRTL. Require Import Linking. + +Inductive match_fundef: BTL.fundef -> RTL.fundef -> Prop := + | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: BTL.stackframe -> RTL.stackframe -> Prop := + | match_stackframe_intro + dupmap res f sp pc rs f' pc' + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc = Some pc') + : match_stackframes (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). + Inductive match_states: BTL.state -> RTL.state -> Prop := | match_states_intro dupmap st f sp pc rs m st' f' pc' diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v index 507fc9d9..309c616e 100644 --- a/scheduling/RTLtoBTL.v +++ b/scheduling/RTLtoBTL.v @@ -1,7 +1,7 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad BTL. -Require Export BTLmatchRTL. +Require Export BTLmatchRTL BTL_Livecheck. Require Import Errors Linking. @@ -17,6 +17,7 @@ Definition transf_function (f: RTL.function) : res BTL.function := let (tc, te) := tcte in let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) tc te in do u <- verify_function dupmap f' f; + do u <- liveness_checker f'; OK f'. Definition transf_fundef (f: RTL.fundef) : res fundef := diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index ef336de5..18ff8d5f 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -230,20 +230,33 @@ Qed. (** * Matching relation on functions *) (* we simply switch [f] and [tf] in the usual way *) -Definition match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := - BTLmatchRTL.match_function dupmap tf f. +Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { + matchRTL:> BTLmatchRTL.match_function dupmap tf f; + liveness_ok: liveness_ok_function tf; +}. -Definition match_fundef f tf := BTLmatchRTL.match_fundef tf f. +Local Hint Resolve matchRTL: core. -Definition match_stackframes stk stk' := BTLmatchRTL.match_stackframes stk' stk. +Inductive match_fundef: RTL.fundef -> BTL.fundef -> Prop := + | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: RTL.stackframe -> BTL.stackframe -> Prop := + | match_stackframe_intro + dupmap res f sp pc rs f' pc' + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc' = Some pc) + : match_stackframes (RTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc' rs). Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. Proof. unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. +(* eexists; eapply verify_function_correct; simpl; eauto. -Qed. +*) +Admitted. Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. @@ -362,7 +375,7 @@ Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.f Proof. intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto. erewrite preserv_fnsig; eauto. -Qed. +Admitted. Lemma transf_initial_states s1: RTL.initial_state prog s1 -> @@ -525,8 +538,8 @@ Proof. - (* Bgoto *) inv MSS2. inversion MIB; subst; try inv H4. remember H2 as ODUPLIC; clear HeqODUPLIC. - eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - apply DMC in H2 as [ib [FNC MI]]; clear DMC. + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. eexists; left; eexists; split; eauto. repeat econstructor; eauto. apply iblock_istep_run_equiv in BTL_RUN; eauto. @@ -584,9 +597,8 @@ Proof. * repeat (econstructor; eauto). eapply transf_fundef_correct; eauto. + (* Bbuiltin *) - eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - remember H1 as ODUPLIC; clear HeqODUPLIC. - apply DMC in H1 as [ib [FNC MI]]; clear DMC. + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. exists (Some (normRTL (entry ib))); left; eexists; split; eauto. econstructor; eauto. econstructor. eexists; eexists; split. @@ -598,9 +610,8 @@ Proof. + (* Bjumptable *) exploit list_nth_z_rev_dupmap; eauto. intros (pc'0 & LNZ & DM). - eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - remember DM as ODUPLIC; clear HeqODUPLIC. - apply DMC in DM as [ib [FNC MI]]; clear DMC. + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. exists (Some (normRTL (entry ib))); left; eexists; split; eauto. econstructor; eauto. econstructor. eexists; eexists; split. @@ -687,11 +698,10 @@ Proof. inv H. + (* Internal function *) inv TRANSF. - rename H1 into TRANSF. - eapply dupmap_entrypoint in TRANSF as ENTRY. - eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - apply DMC in ENTRY as DMC'. - destruct DMC' as [ib [CENTRY MI]]; clear DMC. + rename H0 into TRANSF. + exploit dupmap_entrypoint; eauto. intros ENTRY. + exploit dupmap_correct; eauto. + intros [ib [CENTRY MI]]. exists (Some (normRTL (entry ib))); left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. @@ -705,16 +715,15 @@ Proof. * econstructor; eauto. - (* Returnstate *) inv H. inv STACKS. inv H1. - eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - remember DUPLIC as ODUPLIC; clear HeqODUPLIC. - apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. + exploit dupmap_correct; eauto. + intros [ib [FNC MI]]. eexists; left; eexists; split; eauto. eapply exec_return. Qed. Local Hint Resolve plus_one star_refl: core. -Theorem transf_program_correct: +Theorem transf_program_correct_cfg: forward_simulation (RTL.semantics prog) (BTLmatchRTL.cfgsem tprog). Proof. eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states). @@ -729,4 +738,12 @@ Proof. - eapply senv_preserved. Qed. +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (BTL.fsem tprog). +Proof. + eapply compose_forward_simulations. + - eapply transf_program_correct_cfg. + - eapply cfgsem2fsem. +Admitted. + End BTL_SIMULATES_RTL. |