diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-04-25 03:36:43 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-04-25 03:36:43 +0200 |
| commit | cfcda01c880743abe6eb63e3c1279654b798f2de (patch) | |
| tree | 0853215391beb8867b14c7351d60822714c5f6ee | |
| parent | 811b511dd505065b5fed51cae6fe341a89788acb (diff) | |
| download | compcert-kvx-cfcda01c880743abe6eb63e3c1279654b798f2de.tar.gz compcert-kvx-cfcda01c880743abe6eb63e3c1279654b798f2de.zip | |
a simpler fix ?
| -rw-r--r-- | mppa_k1c/lib/RTLpathSE_theory.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index 210377c8..aa2c6aeb 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -112,6 +112,18 @@ Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop := *) Inductive sabort_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: regset) (m: mem) : Prop := + sabort_exits_on_cond: forall ext, List.In ext lx -> + seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs m = None -> + sabort_exits ge sp lx rs m + | sabort_exits_after_cond: forall ext, List.In ext lx -> + seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true -> + sabort_local ge sp (si_elocal ext) rs m -> + sabort_exits ge sp lx rs m. + +(* VERSION UNNECESSARILY COMPLEX ? + to try only if the above one does not work... + +Inductive sabort_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: regset) (m: mem) : Prop := sabort_exits_on_cond: forall ext lx', is_tail (ext::lx') lx -> all_fallthrough ge sp lx' rs m -> @@ -123,6 +135,9 @@ Inductive sabort_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: reg seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true -> sabort_local ge sp (si_elocal ext) rs m -> sabort_exits ge sp lx rs m. +*) + + Inductive simatch_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop := @@ -299,8 +314,9 @@ Lemma simatch_local_exclude_sabort_exits ge sp st rs m rs' m': sabort_exits ge sp (si_exits st) rs m -> False. Proof. - intros SIML ALLF ABORT. inv ABORT. inv H. - unfold all_fallthrough in ALLF. apply ALLF in H0. congruence. + intros SIML ALLF ABORT. inv ABORT. + - exploit ALLF; eauto. congruence. + - exploit ALLF; eauto. congruence. Qed. Lemma simatch_local_exclude_sabort ge sp st rs m rs' m': |