diff options
Diffstat (limited to 'scheduling/BTL_SEsimuref.v')
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 9 |
1 files changed, 3 insertions, 6 deletions
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. |