diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-04-29 15:02:12 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-04-29 15:02:12 +0200 |
| commit | 0fdf888d455526cf23374c26a961d6e06a582c4d (patch) | |
| tree | 84868fe24452ae21d65337ef56ca04c4ad2a8317 | |
| parent | 0e0e169bb8c78da4965c3c301f1d5f5eb58a87b6 (diff) | |
| download | compcert-kvx-0fdf888d455526cf23374c26a961d6e06a582c4d.tar.gz compcert-kvx-0fdf888d455526cf23374c26a961d6e06a582c4d.zip | |
Complete proof of ssem_exclude_sabort
| -rw-r--r-- | mppa_k1c/lib/RTLpathSE_theory.v | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index 8ea4f9a7..f5a19b27 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -317,7 +317,7 @@ Proof. - (* FIXME Problem : if we have a ssem_local, this means we ONLY evaluated the conditions, but we NEVER actually evaluated the si_elocal from the sistate_exit ! So we cannot prove a lack of abort on the si_elocal.. We must change the definitions *) -Admitted. +Abort. Lemma ssem_local_exclude_sabort ge sp st rs m rs' m': ssem_local ge sp (si_local st) rs m rs' m' -> @@ -328,7 +328,10 @@ Proof. intros SIML ALLF ABORT. inv ABORT. - intuition; eapply ssem_local_exclude_sabort_local; eauto. - - destruct H as (ext & lx & ALLFU & SABORT). inv ALLFU. eapply ssem_local_exclude_sabort_exit; eauto. + - destruct H as (ext & lx & ALLFU & SABORT). + destruct ALLFU as (TAIL & _). eapply is_tail_in in TAIL. + eapply ALLF in TAIL. + destruct SABORT as [CONDFAIL | (CONDTRUE & ABORTL)]; congruence. Qed. Lemma ssem_exit_fallthrough_upto_exit ge sp ext ext' lx lx' exits rs m rs' m' pc': @@ -371,9 +374,9 @@ Proof. - destruct H as (ext' & lx' & ALLFU' & ABORT). exploit ssem_exit_fallthrough_upto_exit; eauto. intros ITAIL. destruct ALLFU as (ALLFU1 & ALLFU2). destruct ALLFU' as (ALLFU1' & ALLFU2'). - exploit (is_tail_cons_eq ext' ext lx' lx); eauto. intro. inv H. - + eapply ssem_exit_exclude_sabort_exit; eauto. - + eapply ALLFU2 in H0. destruct ABORT as [ABORT | (ABORT & ABORT')]; congruence. + exploit (is_tail_inv_left ext' ext lx' lx); eauto. intro. inv H. + + inv H0. eapply ssem_exit_exclude_sabort_exit; eauto. + + destruct H0 as (INE & TAIL). eapply ALLFU2 in INE. destruct ABORT as [ABORT | (ABORT & ABORT')]; congruence. Qed. Lemma ssem_exclude_sabort ge sp st rs m is: |