From b063fb03af84483671833d40491f4fa8d2c8b4c9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 23 Jul 2021 18:25:00 +0200 Subject: non trapping loads --- scheduling/BTL_SEsimuref.v | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'scheduling/BTL_SEsimuref.v') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 7af1af62..d47e53b8 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -348,7 +348,7 @@ Proof. unfold sexec_op. rewrite ok_set_sreg. intuition. Qed. -Lemma si_ok_load_okpreserv ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis. +Lemma si_ok_load_okpreserv ctx chunk addr args dest sis trap: si_ok ctx (sexec_load trap chunk addr args dest sis) -> si_ok ctx sis. Proof. unfold sexec_load. rewrite ok_set_sreg. intuition. Qed. @@ -705,8 +705,7 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := (* basic instructions *) | Bnop _ => k ris | Bop op args res _ => k (rexec_op op args res ris) - | Bload TRAP chunk addr args dst _ => k (rexec_load TRAP chunk addr args dst ris) - | Bload NOTRAP chunk addr args dst _ => Rabort + | Bload trap chunk addr args dst _ => k (rexec_load trap chunk addr args dst ris) | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris) (* composed instructions *) | Bseq ib1 ib2 => @@ -739,7 +738,6 @@ Lemma rexec_rec_correct1 ctx ib: , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st. Proof. induction ib; simpl; try (intros; subst; eauto; fail). - - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. - (* seq *) intros; subst. eapply IHib1. 3-6: eauto. @@ -774,7 +772,7 @@ Proof. unfold rexec_op. rewrite ok_rset_sreg. intuition. Qed. -Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris. +Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris trap: ris_ok ctx (rexec_load trap chunk addr args dest ris) -> ris_ok ctx ris. Proof. unfold rexec_load. rewrite ok_rset_sreg. intuition. Qed. @@ -818,7 +816,6 @@ Lemma rexec_rec_correct2 ctx ib: , rst_refines ctx st (sexec_rec (cf ctx) ib sis k). Proof. induction ib; simpl; try (intros; subst; eauto; fail). - - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. - (* seq *) intros; subst. eapply IHib1. 3-6: eauto. -- cgit