diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | scheduling/BTL.v | 119 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 50 | ||||
| -rw-r--r-- | scheduling/RTLtoBTL.v | 23 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 239 |
5 files changed, 383 insertions, 50 deletions
@@ -143,7 +143,7 @@ SCHEDULING= \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ - BTL.v BTLtoRTL.v BTLtoRTLproof.v \ + BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v # C front-end modules (in cfrontend/) diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 7bc091ef..fb67d150 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -342,6 +342,8 @@ Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) + (** Matching BTL and RTL code We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. @@ -429,49 +431,10 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc . -(* Partial copy of Duplicate and Duplicateproof. *) - Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := forall pc pc', dupmap!pc = Some pc' -> exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. -Record match_function dupmap f f': Prop := { - dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); - dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); - preserv_fnsig: fn_sig f = RTL.fn_sig f'; - preserv_fnparams: fn_params f = RTL.fn_params f'; - preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' -}. - -Inductive match_fundef: 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 (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). - -Inductive match_states: state -> RTL.state -> Prop := - | match_states_intro - dupmap st f sp pc rs m st' f' pc' - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) - | match_states_call - st st' f f' args m - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_fundef f f') - : match_states (Callstate st f args m) (RTL.Callstate st' f' args m) - | match_states_return - st st' v m - (STACKS: list_forall2 match_stackframes st st') - : match_states (Returnstate st v m) (RTL.Returnstate st' v m) - . - (** Shared verifier between RTL -> BTL and BTL -> RTL *) Local Open Scope error_monad_scope. @@ -536,7 +499,6 @@ Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. Global Opaque builtin_res_eq_pos. -(* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := match ib with | BF fi => @@ -801,14 +763,73 @@ Definition verify_function dupmap f f' : res unit := do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); verify_cfg dupmap (fn_code f) (RTL.fn_code f'). -Lemma verify_function_correct dupmap f f' tt: - verify_function dupmap f f' = OK tt -> - fn_sig f = RTL.fn_sig f' -> - fn_params f = RTL.fn_params f' -> - fn_stacksize f = RTL.fn_stacksize f' -> - match_function dupmap f f'. +Definition is_seq (ib: iblock): bool := + match ib with + | Bseq _ _ => true + | _ => false + end. + +Definition is_atom (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ => false + | _ => true + end. + + +Inductive is_right_assoc: iblock -> Prop := + | ira_Bseq ib1 ib2: + is_seq ib1 = false -> + is_right_assoc ib1 -> + is_right_assoc ib2 -> + is_right_assoc (Bseq ib1 ib2) + | ira_Bcond cond args ib1 ib2 i: + is_right_assoc ib1 -> + is_right_assoc ib2 -> + is_right_assoc (Bcond cond args ib1 ib2 i) + | ira_others ib: + is_atom ib = true -> + is_right_assoc ib + . +Local Hint Constructors is_right_assoc: core. + +Fixpoint right_assoc (ib: iblock): iblock := + match ib with + | Bseq ib1 ib2 => rec_rotate ib1 (right_assoc ib2) + | Bcond cond args ib1 ib2 i => + Bcond cond args (right_assoc ib1) (right_assoc ib2) i + | ib => ib + end +with rec_rotate (ib: iblock) rem: iblock := + match ib with + | Bseq ib1 ib2 => + rec_rotate ib1 (rec_rotate ib2 rem) + | Bcond cond args ib1 ib2 i => + Bseq (Bcond cond args (right_assoc ib1) (right_assoc ib2) i) rem + | ib => Bseq ib rem +end. + +Lemma right_assoc_rec_rotate_correct ib: + is_right_assoc (right_assoc ib) + /\ (forall rem, is_right_assoc rem -> is_right_assoc (rec_rotate ib rem)). Proof. - unfold verify_function; intro VERIF. monadInv VERIF. - constructor; eauto. - eapply verify_cfg_correct; eauto. + induction ib; simpl; intuition. Qed. + +Lemma right_assoc_correct ib: + is_right_assoc (right_assoc ib). +Proof. + destruct (right_assoc_rec_rotate_correct ib); auto. +Qed. + +Definition right_assoc_code (cfg: code): code := + (PTree.map (fun _ ib => {| entry:=right_assoc ib.(entry); input_regs := ib.(input_regs) |}) cfg). + +Lemma right_assoc_code_correct cfg pc ib : + (right_assoc_code cfg)!pc=Some ib -> is_right_assoc (ib.(entry)). +Proof. + unfold right_assoc_code. + rewrite PTree.gmap. + destruct (cfg!pc); simpl; intros; try_simplify_someHyps. + apply right_assoc_correct; auto. +Qed. + diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 3944e756..08a77ae4 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -6,6 +6,56 @@ Require Import Errors Linking BTLtoRTL. Require Import Linking. +Record match_function dupmap f f': Prop := { + dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); + dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); + preserv_fnsig: fn_sig f = RTL.fn_sig f'; + preserv_fnparams: fn_params f = RTL.fn_params f'; + preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' +}. + +Inductive match_fundef: 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 (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). + +Inductive match_states: state -> RTL.state -> Prop := + | match_states_intro + dupmap st f sp pc rs m st' f' pc' + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc = Some pc') + : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) + | match_states_call + st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states (Callstate st f args m) (RTL.Callstate st' f' args m) + | match_states_return + st st' v m + (STACKS: list_forall2 match_stackframes st st') + : match_states (Returnstate st v m) (RTL.Returnstate st' v m) + . + +Lemma verify_function_correct dupmap f f' tt: + verify_function dupmap f f' = OK tt -> + fn_sig f = RTL.fn_sig f' -> + fn_params f = RTL.fn_params f' -> + fn_stacksize f = RTL.fn_stacksize f' -> + match_function dupmap f f'. +Proof. + unfold verify_function; intro VERIF. monadInv VERIF. + constructor; eauto. + - eapply verify_cfg_correct; eauto. + - eapply verify_is_copy_correct; eauto. +Qed. + Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. Proof. diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v new file mode 100644 index 00000000..14aecb21 --- /dev/null +++ b/scheduling/RTLtoBTL.v @@ -0,0 +1,23 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. + +Require Import Errors Linking. + +(** External oracle *) +Parameter rtl2btl: RTL.function -> BTL.code * node * (PTree.t node). + +Local Open Scope error_monad_scope. + +Definition transf_function (f: RTL.function) : res BTL.function := + let (tcte, dupmap) := rtl2btl f in + let (tc, te) := tcte in + let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) (right_assoc_code tc) te in + do u <- verify_function dupmap f' f; + OK f'. + +Definition transf_fundef (f: RTL.fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: RTL.program) : res program := + transform_partial_program transf_fundef p. diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v new file mode 100644 index 00000000..4f76d0b7 --- /dev/null +++ b/scheduling/RTLtoBTLproof.v @@ -0,0 +1,239 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad BTL. + +Require Import Errors Linking RTLtoBTL. + +Require Import Linking. + +Record match_function dupmap f tf: Prop := { + dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f); + dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f); + code_right_assoc: forall pc ib, (fn_code tf)!pc=Some ib -> is_right_assoc ib.(entry); + preserv_fnsig: fn_sig tf = RTL.fn_sig f; + preserv_fnparams: fn_params tf = RTL.fn_params f; + preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f +}. + +Inductive match_fundef: RTL.fundef -> fundef -> Prop := + | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf) + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: RTL.stackframe -> 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) (Stackframe res f' sp pc' rs). + +Lemma verify_function_correct dupmap f f' tt: + verify_function dupmap f' f = OK tt -> + fn_sig f' = RTL.fn_sig f -> + fn_params f' = RTL.fn_params f -> + fn_stacksize f' = RTL.fn_stacksize f -> + (forall pc ib, (fn_code f')!pc=Some ib -> is_right_assoc ib.(entry)) -> + match_function dupmap f f'. +Proof. + unfold verify_function; intro VERIF. monadInv VERIF. + constructor; eauto. + - eapply verify_cfg_correct; eauto. + - eapply verify_is_copy_correct; eauto. +Qed. + +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. + eapply right_assoc_code_correct; eauto. +Qed. + +Lemma transf_fundef_correct f f': + transf_fundef f = OK f' -> match_fundef f f'. +Proof. + intros TRANSF; destruct f; simpl; monadInv TRANSF. + + exploit transf_function_correct; eauto. + intros (dupmap & MATCH_F). + eapply match_Internal; eauto. + + eapply match_External. +Qed. + +Definition match_prog (p: RTL.program) (tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. + +Section BTL_SIMULATES_RTL. + +Variable prog: RTL.program. +Variable tprog: program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Local Open Scope nat_scope. + +(* TODO: + faire un dessin ASCII art de la simulation avec match_states_intro + +Le iblock en paramètre représente l'état de l'exécution côté BTL +depuis le début de l'exécution du block +*) + +Inductive match_states: iblock -> RTL.state -> state -> Prop := + | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *) + ib dupmap st f sp pc rs m st' f' pc' pc0' pc0 rs0 m0 isfst ib0 + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function dupmap f f') + (ATpc0: (fn_code f')!pc0' = Some ib0) + (DUPLIC: dupmap!pc0' = Some pc0) + (MIB: match_iblock dupmap (RTL.fn_code f) isfst pc' ib None) + (RIGHTA: is_right_assoc ib) + (RTL_RUN: star RTL.step ge (RTL.State st f sp pc0 rs0 m0) E0 (RTL.State st f sp pc rs m)) + (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m) + : match_states ib (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m) + | match_states_call + ib st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states ib (RTL.Callstate st f args m) (Callstate st' f' args m) + | match_states_return + ib st st' v m + (STACKS: list_forall2 match_stackframes st st') + : match_states ib (RTL.Returnstate st v m) (Returnstate st' v m) + . + +Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. +Qed. + +Lemma senv_preserved: Senv.equiv ge tge. +Proof. + eapply (Genv.senv_match TRANSL). +Qed. + +Lemma functions_translated (v: val) (f: RTL.fundef): + Genv.find_funct ge v = Some f -> + exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog. +Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & A & B & C). + repeat eexists; intuition eauto. + + unfold incl; auto. + + eapply linkorder_refl. +Qed. + +Lemma function_ptr_translated 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. + intros. + exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + +Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.funsig f. +Proof. + intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto. + erewrite preserv_fnsig; eauto. +Qed. + +Lemma transf_initial_states s1: + RTL.initial_state prog s1 -> + exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). + eexists. eexists. split. + - econstructor; eauto. + + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + erewrite function_sig_translated; eauto. + - constructor; eauto. + constructor. + apply transf_fundef_correct; auto. +Admitted. (* TODO *) + +Lemma transf_final_states ib s1 s2 r: + match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Lemma find_function_preserved ri rs0 fd + (FIND : RTL.find_function ge ri rs0 = Some fd) + : exists fd', find_function tge ri rs0 = Some fd' + /\ transf_fundef fd = OK fd'. +Proof. + pose symbols_preserved as SYMPRES. + destruct ri. + + simpl in FIND; apply functions_translated in FIND. + destruct FIND as (tf & cunit & TFUN & GFIND & LO). + eexists; split. eauto. assumption. + + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF). + eexists; split. simpl. rewrite symbols_preserved. + rewrite GFS. eassumption. assumption. +Qed. + +(* Inspired from Duplicateproof.v *) +Lemma list_nth_z_dupmap: + forall dupmap ln ln' (pc pc': node) val, + list_nth_z ln val = Some pc -> + list_forall2 (fun n n' => dupmap!n = Some n') ln ln' -> + exists (pc': node), + list_nth_z ln' val = Some pc' + /\ dupmap!pc = Some pc'. +Proof. + induction ln; intros until val; intros LNZ LFA. + - inv LNZ. + - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + + inv H0. destruct ln'; inv LFA. + simpl. exists n. split; auto. + + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. +Qed. + +(* TODO: definir une measure sur les iblocks. +Cette mesure décroit strictement quand on exécute un "petit-pas" de iblock. +Par exemple, le nombre de noeuds (ou d'instructions "RTL") dans le iblock devrait convenir. +La hauteur de l'arbre aussi. +*) +Parameter measure: iblock -> nat. + +Theorem opt_simu s1 t s1': + RTL.step ge s1 t s1' -> + forall ib s2, + match_states ib s1 s2 -> + exists (ib' : iblock), + (exists s2', step tge s2 t s2' /\ match_states ib' s1' s2') + \/ (measure ib' < measure ib /\ t=E0 /\ match_states ib' s1' s2) + . +Admitted. + +Local Hint Resolve plus_one star_refl: core. + +Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (BTL.semantics tprog). +Proof. + eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ measure) match_states). + constructor 1; simpl. + - apply well_founded_ltof. + - eapply transf_initial_states. + - eapply transf_final_states. + - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP. + destruct 1 as (ib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]). + + repeat eexists; eauto. + + subst. repeat eexists; eauto. + - eapply senv_preserved. +Qed. + +End BTL_SIMULATES_RTL. |