diff options
author | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-27 11:22:33 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-27 11:22:33 +0200 |
commit | 70ed73cba9347b398c509488051ae54d193eb875 (patch) | |
tree | 0dfe7586746d4d8acd76ddf28512abc8d94e4188 /scheduling/BTL_SEimpl.v | |
parent | 0b076ef6eb5553be43ce81c27e438f632b17cb32 (diff) | |
parent | b063fb03af84483671833d40491f4fa8d2c8b4c9 (diff) | |
download | compcert-kvx-70ed73cba9347b398c509488051ae54d193eb875.tar.gz compcert-kvx-70ed73cba9347b398c509488051ae54d193eb875.zip |
Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL-SEimpl
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. |