diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-13 14:08:49 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-13 14:08:49 +0200 |
| commit | fae36491fa22adaaf447e189988848483eb01dcd (patch) | |
| tree | 285c18919ca5b3d5e728021b21cd44d62d1a9f25 /kvx/lib/RTLpathSchedulerproof.v | |
| parent | 7af1dae4e776b3977fcb16b5a770644e2932d7ca (diff) | |
| download | compcert-kvx-fae36491fa22adaaf447e189988848483eb01dcd.tar.gz compcert-kvx-fae36491fa22adaaf447e189988848483eb01dcd.zip | |
removing useless opt_simu
Diffstat (limited to 'kvx/lib/RTLpathSchedulerproof.v')
| -rw-r--r-- | kvx/lib/RTLpathSchedulerproof.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kvx/lib/RTLpathSchedulerproof.v b/kvx/lib/RTLpathSchedulerproof.v index e2344579..4ba197b0 100644 --- a/kvx/lib/RTLpathSchedulerproof.v +++ b/kvx/lib/RTLpathSchedulerproof.v @@ -155,7 +155,7 @@ Proof. unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *. + rewrite !(seval_preserved ge tge) in *; eauto. destruct (seval_sval _ _ _ _); try congruence. - erewrite SIMU; try congruence. clear SIMU. + erewrite <- SIMU; try congruence. clear SIMU. intros; exploit functions_preserved; eauto. intros (fd' & cunit & (X1 & X2 & X3)). eexists. repeat split; eauto. @@ -217,7 +217,7 @@ Proof. exploit initialize_path. { eapply dupmap_path_entry1; eauto. } intros (path & PATH). eexists; split; econstructor; eauto. - + eapply opt_simu_Some; eauto. + + eapply eq_trans; try eassumption; auto. + simpl. repeat (econstructor; eauto). - (* Stailcall *) exploit s_find_function_preserved; eauto. @@ -225,7 +225,7 @@ Proof. erewrite <- function_sig_preserved; eauto. eexists; split; econstructor; eauto. + erewrite <- preserv_fnstacksize; eauto. - + eapply opt_simu_Some; eauto. + + eapply eq_trans; try eassumption; auto. - (* Sbuiltin *) pose senv_preserved_RTL as SRTL. exploit initialize_path. { eapply dupmap_path_entry1; eauto. } @@ -233,7 +233,7 @@ Proof. eexists; split; econstructor; eauto. + eapply seval_builtin_args_preserved; eauto. eapply seval_list_builtin_sval_correct; eauto. - intro. rewrite <- H0 by assumption. + rewrite H0. erewrite seval_list_builtin_sval_preserved; eauto. + eapply external_call_symbols_preserved; eauto. + eapply eqlive_reg_refl. @@ -242,7 +242,7 @@ Proof. exploit initialize_path. { eapply dupmap_path_entry1; eauto. } intros (path & PATH). eexists; split; econstructor; eauto. - + eapply opt_simu_Some; eauto. + + eapply eq_trans; try eassumption; auto. + eapply eqlive_reg_refl. - (* Sreturn *) eexists; split; econstructor; eauto. @@ -250,7 +250,7 @@ Proof. - (* Sreturn bis *) eexists; split; econstructor; eauto. + erewrite <- preserv_fnstacksize; eauto. - + rewrite H by congruence. erewrite <- seval_preserved; eauto. + + rewrite <- H. erewrite <- seval_preserved; eauto. Qed. (* The main theorem on simulation of symbolic states ! *) |