diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-23 18:25:00 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-23 18:25:00 +0200 |
commit | b063fb03af84483671833d40491f4fa8d2c8b4c9 (patch) | |
tree | 89033ebd4ec906091d31457b0b7f3c8539e11dc1 /scheduling/BTL_SEsimuref.v | |
parent | 8de8dc6616c49018c6151887f76ea08c8f1ff04e (diff) | |
download | compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.tar.gz compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.zip |
non trapping loads
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. |