diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-07 19:58:02 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-07 19:58:02 +0200 |
commit | 08b39b2025951a9655939c1377f6e53b346c6821 (patch) | |
tree | f6a64ddf1f59404a58405ffdee06d476b7b28fb5 /scheduling | |
parent | 89aececb825a04dbc1982ec9e61331ef3272c228 (diff) | |
download | compcert-kvx-08b39b2025951a9655939c1377f6e53b346c6821.tar.gz compcert-kvx-08b39b2025951a9655939c1377f6e53b346c6821.zip |
Some advance in proof and NOTRAP loads fix
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTL.v | 13 | ||||
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 57 |
2 files changed, 60 insertions, 10 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index fb67d150..c8dfa0af 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -400,9 +400,9 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i | mib_op isfst pc pc' op lr r: cfg!pc = Some (Iop op lr r pc') -> match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc') - | mib_load isfst pc pc' tm m a lr r: - cfg!pc = Some (Iload tm m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload tm m a lr r) (Some pc') + | mib_load isfst pc pc' m a lr r: + cfg!pc = Some (Iload TRAP m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r) (Some pc') | mib_store isfst pc pc' m a lr r: cfg!pc = Some (Istore m a lr r pc') -> match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc') @@ -581,7 +581,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | Bload tm m a lr r => match cfg!pc with | Some (Iload tm' m' a' lr' r' pc') => - if (trapping_mode_eq tm tm') then + if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then if (chunk_eq m m') then if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then @@ -591,7 +591,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "verify_block: different lr in Bload") else Error (msg "verify_block: different addressing in Bload") else Error (msg "verify_block: different mchunk in Bload") - else Error (msg "verify_block: different trapping_mode in Bload") + else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload") | _ => Error (msg "verify_block: incorrect cfg Bload") end | Bstore m a lr r => @@ -691,7 +691,8 @@ Proof. constructor; assumption. - (* Bload *) destruct i; try discriminate. - destruct (trapping_mode_eq _ _); try discriminate. + do 2 (destruct (trapping_mode_eq _ _); try discriminate). + simpl in H. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index f5ea9fdc..023837f9 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -256,9 +256,59 @@ Lemma opt_simu_intro (RTL.State st f sp pcR1 rs m)) (BTL_RUN : iblock_istep_run tge sp (entry ib0) rs0 m0 = iblock_istep_run tge sp ib rs m) - : exists (oib : option iblock), - omeasure oib < omeasure (Some ib) /\ - t = E0 /\ match_states oib s1' (State st' f' sp pcB0 rs0 m0). + : exists (oib' : option iblock), + (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2') + \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). +Proof. + inv MIB. + - (* mib_BF *) + admit. + - (* mib_exit *) + (* destruct t. + 2: { + eexists; left. eexists; split. + + eapply exec_iblock; eauto. + econstructor; repeat eexists. + eapply iblock_istep_run_equiv; eauto. + inv STEP. + eapply exec_Bgoto.*) admit. + - (* mib_seq *) + inv H. + + (* Bnop *) + inversion STEP; subst; try_simplify_someHyps. (* TODO maybe move that for each subcase *) + exists (Some b2); right; repeat (split; auto). + econstructor; eauto. inv RIGHTA; auto; discriminate. + eapply star_right; eauto. + + (* Bop *) + inversion STEP; subst; try_simplify_someHyps. + exists (Some b2); right; repeat (split; auto). + econstructor; eauto. inv RIGHTA; auto; discriminate. + eapply star_right; eauto. + erewrite eval_operation_preserved in H10. + erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + + (* Bload *) + inversion STEP; subst; try_simplify_someHyps. + exists (Some (b2)); right; repeat (split; auto). + econstructor; eauto. inv RIGHTA; auto; discriminate. + eapply star_right; eauto. + erewrite eval_addressing_preserved in H10. + erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + + (* Bstore *) + inversion STEP; subst; try_simplify_someHyps. + exists (Some b2); right; repeat (split; auto). + econstructor; eauto. inv RIGHTA; auto; discriminate. + eapply star_right; eauto. + erewrite eval_addressing_preserved in H10. + erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + + (* Absurd case *) + inv RIGHTA. inv H4. inv H. + + (* Bcond *) + admit. + - (* mib_cond *) + admit. Admitted. Theorem opt_simu s1 t s1' oib s2: @@ -272,7 +322,6 @@ Proof. inversion 2; subst; clear H0. - (* State *) exploit opt_simu_intro; eauto. - intros (oib' & SIMU); exists oib'; right; assumption. - (* Callstate *) inv H. + (* Internal function *) |