diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-20 19:56:42 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-20 19:56:42 +0100 |
commit | 4d5b986ff72098466b3a3bb02c20d0ca697243da (patch) | |
tree | 45b93a558fa7b541e0b42bad5f591255020242df /mppa_k1c/PostpassSchedulingproof.v | |
parent | e25099690ddfc45579c318940f3304ab6400135c (diff) | |
download | compcert-kvx-4d5b986ff72098466b3a3bb02c20d0ca697243da.tar.gz compcert-kvx-4d5b986ff72098466b3a3bb02c20d0ca697243da.zip |
one step further...
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 34 |
1 files changed, 28 insertions, 6 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 25bdf244..5b3768af 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -680,9 +680,9 @@ Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Lemma transf_blocks_checks_all_bundles lbb bundles: - transf_blocks (lbb : list bblock) = OK bundles -> - List.Forall (fun bb => verify_par_bblock bb = OK tt) bundles. +Lemma transf_blocks_checks_all_bundles ofs lbb lb bundle: + transf_blocks lbb = OK lb -> + find_bblock (Ptrofs.unsigned ofs) lb = Some bundle -> verify_par_bblock bundle = OK tt. Proof. Admitted. @@ -691,9 +691,31 @@ Lemma all_bundles_are_checked b ofs f bundle: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle -> verify_par_bblock bundle = OK tt. Proof. - unfold match_prog, match_program, match_program_gen in TRANSL. - (* HOW CAN WE PROVE THIS FROM transf_blocks_checks_all_bundles ?? *) -Admitted. + unfold match_prog, match_program in TRANSL. + unfold Genv.find_funct_ptr; simpl; intros 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 (Internal f)) as f2. + destruct H as [ctx' f1 f2 H0|]; try congruence. + inversion Heqf2 as [H2]. subst; clear Heqf2. + unfold transf_fundef, transf_partial_fundef in H. + (* TODO: is there any way to simplify these reasonings in the monad ? *) + destruct f1 as [f1|f1]; try congruence. + remember (transf_function f1) as tf1. + destruct tf1 as [f0|]; simpl in *|-; try congruence. + inversion H as [H1]. subst. clear H. + unfold transf_function in Heqtf1. + remember (transl_function f1) as tf0. + destruct tf0 as [f0|]; simpl in *|-; try congruence. + destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks f0))); simpl in *|-; try congruence. + inversion Heqtf1 as [H]. subst; clear Heqtf1. + unfold transl_function in Heqtf0. + remember (transf_blocks (fn_blocks f1)) as olb. + destruct olb as [lb|]; simpl in *|-; try congruence. + inversion Heqtf0 as [H]. subst; clear Heqtf0. simpl. + intros; exploit transf_blocks_checks_all_bundles; eauto. +Qed. Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' -> |