From baedc5d727f648327b18c8cb95a27491850fbe2e Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 24 Apr 2020 12:34:53 +0200 Subject: Reverting change to sistate --- mppa_k1c/lib/RTLpathSE_theory.v | 46 +++++++---------------------------------- 1 file changed, 7 insertions(+), 39 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index c503936b..66e23cd8 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -112,25 +112,15 @@ Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop := Inductive simatch_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop := simatch_exits_intro: forall ext lx', - lx = ext::lx' -> + is_tail (ext::lx') lx -> all_fallthrough ge sp lx' rs m -> seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true -> simatch_local ge sp (si_elocal ext) rs m rs' m' -> (si_ifso ext) = pc' -> simatch_exits ge sp lx rs m rs' m' pc'. -(* Ensuring there isn't more sistate_local after taking a branch *) -Inductive simatch_exits_bind (ext: sistate_exit) (loc: sistate_local) : Prop := - simatch_exits_bind_intro: - (forall ge sp lx rs m rs' m' pc', simatch_exits ge sp (ext::lx) rs m rs' m' pc' -> si_elocal ext = loc) -> - simatch_exits_bind ext loc. - -Definition sistate_wf exits loc := - exists ext lx, exits = ext::lx /\ simatch_exits_bind ext loc. - (** * Syntax and Semantics of symbolic internal state *) -Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local; - si_wf: sistate_wf si_exits si_local }. +Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. Definition simatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop := if (is.(icontinue)) @@ -185,7 +175,7 @@ Proof. Local Hint Resolve is_tail_in: core. destruct 1 as [ext lx' lc NYE' EVAL SEM PC]. subst. unfold all_fallthrough; intros NYE; rewrite NYE in EVAL; eauto. - try congruence. rewrite lc. econstructor; eauto. + try congruence. (* rewrite lc. econstructor; eauto. *) Qed. Lemma simatch_exclude_incompatible_continue ge sp st rs m is1 is2: @@ -257,8 +247,8 @@ Proof. Local Hint Resolve exit_cond_determ eq_sym: core. destruct 1 as [ext1 lx1 TAIL1 NYE1 EVAL1 SEM1 PC1]; subst. destruct 1 as [ext2 lx2 TAIL2 NYE2 EVAL2 SEM2 PC2]; subst. - assert (X:ext1=ext2) by congruence. -(*{ destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. } *) + assert (X:ext1=ext2). + { destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. } subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto. Qed. @@ -315,36 +305,14 @@ Lemma simatch_exits_exclude_sabort_local ge sp st rs m rs' m' pc': sabort_local ge sp (si_local st) rs m -> False. Proof. - destruct st as [spc exits loc SISTWF]. simpl. - intros SIMEX ABORT. inv SISTWF. inv H. inv H0. - inversion SIMEX. subst. inv H. - inv H1. eapply H in SIMEX. subst. clear H. - inv H3. destruct H1 as (H1 & H1'). - inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. -Qed. - -(* Weaker version if we don't have the simatch_exits_bind - not used anymore, couldn't get any use from it *) -Remark simatch_exits_exclude_sabort_local' ge sp rs m rs' m' pc' exits ext: - simatch_exits ge sp (ext::exits) rs m rs' m' pc' -> - sabort_local ge sp (si_elocal ext) rs m -> - False. -Proof. - intros SIMEX ABORT. - inv SIMEX. inv H. inv H2. destruct H3 as (H3 & H3'). - inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. -Qed. +Admitted. Lemma simatch_exits_exclude_sabort_exits ge sp exits rs m rs' m' pc': simatch_exits ge sp exits rs m rs' m' pc' -> sabort_exits ge sp exits rs m -> False. Proof. - intros SIMEX ABORT. - inv ABORT. inv H. inv SIMEX. unfold all_fallthrough in H2. - inv H0. - - congruence. - - apply H2 in H. congruence. -Qed. +Admitted. Lemma simatch_exits_exclude_sabort ge sp st rs m rs' m' pc': simatch_exits ge sp (si_exits st) rs m rs' m' pc' -> -- cgit