diff options
Diffstat (limited to 'scheduling/BTL_SEimpl.v')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 305c3cfa..aa27bd19 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -823,11 +823,11 @@ Proof. simpl in *; econstructor; eauto. Qed. -Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs: - WHEN hrs_sreg_set dest args (Rload TRAP chunk addr) hrs ~> rst THEN +Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs trap: + WHEN hrs_sreg_set dest args (Rload trap chunk addr) hrs ~> rst THEN ris_ok ctx rst -> ris_ok ctx hrs. Proof. - wlp_simplify; inv H1; + wlp_simplify; inv H2 || inv H1; simpl in *; econstructor; eauto. Qed. @@ -1071,10 +1071,9 @@ Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := | Bop op args dst _ => DO next <~ hrs_sreg_set dst args (Rop op) hrs;; k next - | Bload TRAP chunk addr args dst _ => - DO next <~ hrs_sreg_set dst args (Rload TRAP chunk addr) hrs;; + | Bload trap chunk addr args dst _ => + DO next <~ hrs_sreg_set dst args (Rload trap chunk addr) hrs;; k next - | Bload NOTRAP chunk addr args dst _ => RET Rabort | Bstore chunk addr args src _ => DO next <~ hrexec_store chunk addr args src hrs;; k next @@ -1122,7 +1121,6 @@ Proof. intros X; apply H0 in X. exploit hrexec_final_sfv_correct; eauto. - (* Bnop *) wlp_simplify; eapply CONT; eauto. - - (* Bload *) destruct trap; wlp_simplify. - (* Bseq *) wlp_simplify. eapply IHib1. 3-7: eauto. @@ -1171,7 +1169,7 @@ Proof. - (* Bop *) wlp_simplify; exploit hrs_ok_op_okpreserv; eauto. - (* Bload *) - destruct trap; wlp_simplify; try_simplify_someHyps. + destruct trap; wlp_simplify; try_simplify_someHyps; exploit hrs_ok_load_okpreserv; eauto. - (* Bstore *) wlp_simplify; exploit hrs_ok_store_okpreserv; eauto. @@ -1207,7 +1205,6 @@ Proof. intros X; apply H0 in X. exploit hrexec_final_sfv_correct; eauto. - (* Bnop *) wlp_simplify; eapply CONT; eauto. - - (* Bload *) destruct trap; wlp_simplify. - (* Bseq *) wlp_simplify. eapply IHib1. 3-6: eauto. |