diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-30 17:37:03 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-30 17:37:03 +0200 |
commit | 4b370424090ab9e87fdf48ea5b04482728f99b7f (patch) | |
tree | 7eec645a6e5d0893a1c9e09c75b09e1dd1b2babc /scheduling | |
parent | 7bc2a5e6d2694f144e49fe60af6ddfd0e8a0aba0 (diff) | |
download | compcert-kvx-4b370424090ab9e87fdf48ea5b04482728f99b7f.tar.gz compcert-kvx-4b370424090ab9e87fdf48ea5b04482728f99b7f.zip |
cbranch expanse
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTL_SEimpl.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index f01f1cc0..df8cc47f 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -502,6 +502,31 @@ Proof. + erewrite H0; eauto. Qed. +Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) := + (* TODO gourdinl + match target_cbranch_expanse prev cond args with + | Some (cond', vargs) => + DO vargs' <~ fsval_list_proj vargs;; + RET (cond', vargs') + | None =>*) + DO vargs <~ hlist_args prev args ;; + RET (cond, vargs). + (*end.*) + +Lemma cbranch_expanse_correct hrs c l: + WHEN cbranch_expanse hrs c l ~> r THEN forall ctx st + (REF : ris_refines ctx hrs st) + (OK: ris_ok ctx hrs), + eval_scondition ctx (fst r) (snd r) = + eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)). +Proof. + unfold cbranch_expanse. + wlp_simplify; inv REF. + unfold eval_scondition; erewrite <- H; eauto. +Qed. +Local Hint Resolve cbranch_expanse_correct: wlp. +Global Opaque cbranch_expanse. + Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A := match o with | Some x => RET x |