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_SEimpl.v | |
| parent | 8de8dc6616c49018c6151887f76ea08c8f1ff04e (diff) | |
| download | compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.tar.gz compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.zip | |
non trapping loads
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. |