diff options
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 96 |
1 files changed, 93 insertions, 3 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 710b8d76..509697de 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -597,6 +597,8 @@ Proof. explore; try congruence. Qed. +(* TODO MOVE EXPANSIONS BELOW ELSEWHERE *) + Definition is_inv_cmp_int (cmp: comparison) : bool := match cmp with | Cle | Cgt => true | _ => false end. @@ -988,6 +990,93 @@ Proof. (* TODO Global Opaque hslocal_set_sreg. Local Hint Resolve hslocal_set_sreg_correct: wlp. +(* TODO MOVE ELSEWHERE Branch expansion *) + +(* XXX NOT SURE IF THIS DEF IS NEEDED + * SHOULD WE TAKE THE PREV STATE INTO ACCOUNT HERE? +Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : ?? list_hsval := + if is_inv then + hlist_args prev*) + +Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeqw optR0 + | Cne => CEbnew optR0 + | Clt => CEbltw optR0 + | Cle => CEbgew optR0 + | Cgt => CEbltw optR0 + | Cge => CEbgew optR0 + end. + +Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeqw optR0 + | Cne => CEbnew optR0 + | Clt => CEbltuw optR0 + | Cle => CEbgeuw optR0 + | Cgt => CEbltuw optR0 + | Cge => CEbgeuw optR0 + end. + +Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeql optR0 + | Cne => CEbnel optR0 + | Clt => CEbltl optR0 + | Cle => CEbgel optR0 + | Cgt => CEbltl optR0 + | Cge => CEbgel optR0 + end. + +Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := + match cmp with + | Ceq => CEbeql optR0 + | Cne => CEbnel optR0 + | Clt => CEbltul optR0 + | Cle => CEbgeul optR0 + | Cgt => CEbltul optR0 + | Cge => CEbgeul optR0 + end. + +Definition cbranch_expanse (prev: hsistate_local) (i: instruction) : ?? (condition * list_hsval) := + match i with + | Icond (Ccomp c) (a1 :: a2 :: nil) _ _ _ => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + | Icond (Ccompu c) (a1 :: a2 :: nil) _ _ _ => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + | Icond (Ccompl c) (a1 :: a2 :: nil) _ _ _ => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + | Icond (Ccomplu c) (a1 :: a2 :: nil) _ _ _ => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in + DO hv1 <~ hsi_sreg_get prev a1;; + DO hv2 <~ hsi_sreg_get prev a2;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + RET (cond, lhsv) + (* | Icond (Ccompimm c n) (a1 :: nil) _ _ _ => + let cond := transl_cbranch_int32s c (make_optR0 c) in + RET (cond, a1 :: a1 :: nil)*) + | Icond cond args _ _ _ => + DO vargs <~ hlist_args prev args;; + RET (cond, vargs) + | _ => FAILWITH "cbranch_expanse: not an Icond" + end. + (** ** Execution of one instruction *) Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := @@ -1005,7 +1094,8 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) : RET (Some (hsist_set_local hst pc' next)) | Icond cond args ifso ifnot _ => let prev := hst.(hsi_local) in - DO vargs <~ hlist_args prev args ;; + DO res <~ cbranch_expanse prev i;; + let (cond, vargs) := res in let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}) | _ => RET None (* TODO jumptable ? *) @@ -1044,7 +1134,7 @@ Lemma hsiexec_inst_correct i hst: exists st', siexec_inst i st = Some st' /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st') /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st'). -Proof. +Proof. Admitted. (* destruct i; simpl; wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. - (* refines_dyn Iop *) eapply hsist_set_local_correct_dyn; eauto. @@ -1068,7 +1158,7 @@ Proof. + split; simpl; auto. destruct NEST as [|st0 se lse TOP NEST]; econstructor; simpl; auto; constructor; auto. -Qed. + Qed.*) Global Opaque hsiexec_inst. Local Hint Resolve hsiexec_inst_correct: wlp. |