From 6adfc52c130ee73cf6ee2ee8b85ed8b5e5024a4a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 22 Jul 2021 16:43:14 +0200 Subject: branches expansions support --- scheduling/BTL_SEimpl.v | 23 ++++++++++++----------- scheduling/BTL_SEsimuref.v | 10 +++++----- 2 files changed, 17 insertions(+), 16 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 7711c72d..305c3cfa 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -682,12 +682,13 @@ Lemma cbranch_expanse_correct hrs c l: (REF : ris_refines ctx hrs sis) (OK: ris_ok ctx hrs), eval_scondition ctx (fst r) (snd r) = - eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)) - /\ (fst r) = c. + eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)). Proof. unfold cbranch_expanse. - wlp_simplify; inv REF. - unfold eval_scondition; erewrite <- H; eauto. + destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify; + unfold eval_scondition; try erewrite <- H; inversion REF; eauto. + destruct p as [c' l']; simpl. + exploit target_cbranch_expanse_correct; eauto. Qed. Local Hint Resolve cbranch_expanse_correct: wlp. Global Opaque cbranch_expanse. @@ -1133,9 +1134,9 @@ Proof. erewrite <- OK_EQUIV. 2: eauto. eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. } - exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); - exploit H; eauto; intros (SEVAL & EQC); subst; auto. + exploit H; eauto; intros SEVAL; auto. all: simpl in SOUT; generalize SOUT; clear SOUT; inversion_SOME b0; try_simplify_someHyps. @@ -1217,9 +1218,9 @@ Proof. assert (rOK: ris_ok ctx hrs). { simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps. } - exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 + exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1 (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k)); - exploit H; eauto; intros (SEVAL & EQC); subst; auto. + exploit H; eauto; intros SEVAL; auto. all: simpl in H2; generalize H2; clear H2; inversion_SOME b0; try_simplify_someHyps. @@ -1444,11 +1445,11 @@ Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} := hrs_simu_check hrs1 hrs2;; sfval_simu_check sfv1 sfv2 | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 => - struct_check cond1 cond2 "hsstate_simu_check: conditions do not match";; - phys_check lsv1 lsv2 "hsstate_simu_check: args do not match";; + struct_check cond1 cond2 "rst_simu_check: conditions do not match";; + phys_check lsv1 lsv2 "rst_simu_check: args do not match";; rst_simu_check rsL1 rsL2;; rst_simu_check rsR1 rsR2 - | _, _ => FAILWITH "hsstate_simu_check: simu_check failed" + | _, _ => FAILWITH "rst_simu_check: simu_check failed" end. Lemma rst_simu_check_correct rst1: forall rst2, diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index c812c607..7af1af62 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -260,11 +260,11 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop := (RIS: ris_refines ctx ris sis) (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) - | Refcond cond rargs args rifso rifnot ifso ifnot - (RCOND: eval_scondition ctx cond rargs = eval_scondition ctx cond args) - (REFso: eval_scondition ctx cond rargs = Some true -> rst_refines ctx rifso ifso) - (REFnot: eval_scondition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot) - : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot) + | Refcond rcond cond rargs args rifso rifnot ifso ifnot + (RCOND: eval_scondition ctx rcond rargs = eval_scondition ctx cond args) + (REFso: eval_scondition ctx rcond rargs = Some true -> rst_refines ctx rifso ifso) + (REFnot: eval_scondition ctx rcond rargs = Some false -> rst_refines ctx rifnot ifnot) + : rst_refines ctx (Rcond rcond rargs rifso rifnot) (Scond cond args ifso ifnot) | Refabort : rst_refines ctx Rabort Sabort . -- cgit