diff options
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 171 |
1 files changed, 7 insertions, 164 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 9a50b627..f42a3492 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -432,63 +432,6 @@ Qed. Global Opaque hlist_args. Local Hint Resolve hlist_args_correct: wlp. -(* BEGIN "fake" hsval without real hash-consing *) -(* TODO: - 1) put these definitions elsewhere ? in RTLpathSE_simu_specs.v ? - 2) reuse these definitions in hSinput, hSop, etc - in order to factorize proofs ? -*) - -Definition fSinput (r: reg): hsval := - HSinput r unknown_hid. - -Lemma fSinput_correct r ge sp rs0 m0: (* useless trivial lemma ? *) - sval_refines ge sp rs0 m0 (fSinput r) (Sinput r). -Proof. - auto. -Qed. - -Definition fSop (op:operation) (lhsv: list_hsval): hsval := - HSop op lhsv unknown_hid. - -Lemma fSop_correct op lhsv ge sp rs0 m0 lsv sm m: forall - (MEM: seval_smem ge sp sm rs0 m0 = Some m) - (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) - (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), - sval_refines ge sp rs0 m0 (fSop op lhsv) (Sop op lsv sm). -Proof. - intros; simpl. rewrite <- LR, MEM. - destruct (seval_list_sval _ _ _ _); try congruence. - eapply op_valid_pointer_eq; eauto. -Qed. - -Definition fsi_sreg_get (hst: PTree.t hsval) r: hsval := - match PTree.get r hst with - | None => fSinput r - | Some sv => sv - end. - -Lemma fsi_sreg_get_correct hst r ge sp rs0 m0 (f: reg -> sval): forall - (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0), - sval_refines ge sp rs0 m0 (fsi_sreg_get hst r) (f r). -Proof. - unfold hsi_sreg_eval, hsi_sreg_proj, fsi_sreg_get; intros; simpl. - rewrite <- RR. destruct (hst ! r); simpl; auto. -Qed. - -Definition fSnil: list_hsval := - HSnil unknown_hid. - -(* TODO: Lemma fSnil_correct *) - -Definition fScons (hsv: hsval) (lhsv: list_hsval): list_hsval := - HScons hsv lhsv unknown_hid. - -(* TODO: Lemma fScons_correct *) - -(* END "fake" hsval ... *) - - (** Convert a "fake" hash-consed term into a "real" hash-consed term *) Fixpoint fsval_proj hsv: ?? hsval := @@ -707,15 +650,6 @@ Qed. (* TODO gourdinl MOVE EXPANSIONS BELOW ELSEWHERE *) -Definition is_inv_cmp_int (cmp: comparison) : bool := - match cmp with | Cle | Cgt => true | _ => false end. - -Definition is_inv_cmp_float (cmp: comparison) : bool := - match cmp with | Cge | Cgt => true | _ => false end. - -Definition make_optR0 (is_x0 is_inv: bool) : option bool := - if is_x0 then Some is_inv else None. - (* TODO gourdinl IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval := match l with | nil => hSnil() @@ -724,18 +658,7 @@ Definition make_optR0 (is_x0 is_inv: bool) : option bool := hScons r lhsv end.*) -Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : ?? list_hsval := - DO hnil <~ hSnil();; - let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in - DO lhsv <~ hScons hvfirst hnil;; - DO lhsv <~ hScons hvsec lhsv;; - RET lhsv. - -Definition make_lhsv_single (hvs: hsval) : ?? list_hsval := - DO hnil <~ hSnil();; - DO hl <~ hScons hvs hnil;; - RET hl. - +(* Definition load_hilo32 (hi lo: int) := DO hnil <~ hSnil();; if Int.eq lo Int.zero then @@ -805,16 +728,6 @@ Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril. Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. -Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := - match cmp with - | Ceq => hSop (OEseqw optR0) lhsv - | Cne => hSop (OEsnew optR0) lhsv - | Clt | Cgt => hSop (OEsltw optR0) lhsv - | Cle | Cge => - DO hvs <~ (hSop (OEsltw optR0) lhsv);; - DO hl <~ make_lhsv_single hvs;; - hSop (OExoriw Int.one) hl - end. Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := match cmp with @@ -954,11 +867,12 @@ Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) := DO hl <~ make_lhsv_cmp is_inv hv1 hvs;; cond_int64u cmp hl optR0 end. + *) (** simplify a symbolic value before assignment to a register *) Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval := match rsv with - | Rop (Omove as op) => + | Rop op => match is_move_operation op lr with | Some arg => hsi_sreg_get hst arg (* optimization of Omove *) | None => @@ -969,84 +883,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs hSop op lhsv end end - | Rop ((Ocmp cond) as op) => - match cond, lr with - | (Ccomp c), a1 :: a2 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - DO hv2 <~ hsi_sreg_get hst a2;; - let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - cond_int32s c lhsv optR0 - | (Ccompu c), a1 :: a2 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - DO hv2 <~ hsi_sreg_get hst a2;; - let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - cond_int32u c lhsv optR0 - | (Ccompimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int32s c hv1 imm - | (Ccompuimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int32u c hv1 imm - | (Ccompl c), a1 :: a2 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - DO hv2 <~ hsi_sreg_get hst a2;; - let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - cond_int64s c lhsv optR0 - | (Ccomplu c), a1 :: a2 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - DO hv2 <~ hsi_sreg_get hst a2;; - let is_inv := is_inv_cmp_int c in - let optR0 := make_optR0 false is_inv in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - cond_int64u c lhsv optR0 - | (Ccomplimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int64s c hv1 imm - | (Ccompluimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int64u c hv1 imm - | (Ccompf c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cond_fp false cond_float c lhsv - | (Cnotcompf c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cond_fp true cond_float c lhsv - | (Ccompfs c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cond_fp false cond_single c lhsv - | (Cnotcompfs c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; - let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cond_fp true cond_single c lhsv - | _, _ => - DO lhsv <~ hlist_args hst lr;; - hSop op lhsv - end - | Rop op => - DO lhsv <~ hlist_args hst lr;; - hSop op lhsv | Rload _ chunk addr => DO lhsv <~ hlist_args hst lr;; hSload hst NOTRAP chunk addr lhsv end. +(* Lemma simplify_nothing lr (hst: hsistate_local) op: WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) @@ -1905,7 +1747,7 @@ Proof. 4: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl. 5: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl. all: destruct (Float32.cmp _ _ _); trivial. -Qed. + Qed.*) Lemma simplify_correct rsv lr hst: WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st @@ -2053,6 +1895,7 @@ Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : if is_inv then hlist_args prev*) +(* Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) := match cmp with | Ceq => CEbeqw optR0 @@ -2205,7 +2048,7 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list | _, _ => DO vargs <~ hlist_args prev args;; RET (cond, vargs) - end. + end.*) (** ** Execution of one instruction *) |