diff options
| -rw-r--r-- | riscV/ExpansionOracle.ml | 8 | ||||
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 111 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 171 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 61 |
4 files changed, 180 insertions, 171 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 9a3518c0..d3805738 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order = | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." let expanse (sb : superblock) code pm = - (*debug_flag := true;*) + debug_flag := true; let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -388,7 +388,7 @@ let expanse (sb : superblock) code pm = debug "Iop/Ccomp\n"; exp := cond_int32s false c a1 a2 dest succ []; was_exp := true - | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> + (*| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompu\n"; exp := cond_int32u false c a1 a2 dest succ []; was_exp := true @@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm = debug "Icond/Cnotcompfs\n"; exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; was_branch := true; - was_exp := true + was_exp := true*) | _ -> new_order := n :: !new_order); if !was_exp then ( node := !node + 1; @@ -510,7 +510,7 @@ let expanse (sb : superblock) code pm = sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; - (*debug_flag := false;*) + debug_flag := false; (!code', !pm') let rec find_last_node_reg = function diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 4fadcfdc..b9fe504e 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -1,9 +1,114 @@ +Require Import Integers. Require Import Op Registers. Require Import RTLpathSE_theory. Require Import RTLpathSE_simu_specs. +(* Useful functions for conditions/branches expansion *) + +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. + +(* Functions to manage lists of "fake" values *) + +Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval := + let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in + let lhsv := fScons hvfirst fSnil in + fScons hvsec lhsv. + +Definition make_lhsv_single (hvs: hsval) : list_hsval := + fScons hvs fSnil. + +(* Expansion functions *) + +Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := + match cmp with + | Ceq => fSop (OEseqw optR0) lhsv + | Cne => fSop (OEsnew optR0) lhsv + | Clt | Cgt => fSop (OEsltw optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltw optR0) lhsv) in + let hl := make_lhsv_single hvs in + fSop (OExoriw Int.one) hl + end. + +(* Target op simplifications using "fake" values *) + Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := - None. (* default implementation *) + match op, lr with + | Ocmp (Ccomp c), a1 :: a2 :: nil => + let fv1 := fsi_sreg_get hst a1 in + let fv2 := fsi_sreg_get hst a2 in + let is_inv := is_inv_cmp_int c in + let optR0 := make_optR0 false is_inv in + let lhsv := make_lhsv_cmp is_inv fv1 fv2 in + Some (cond_int32s c lhsv optR0) + + (*| Ocmp (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 + | Ocmp (Ccompimm c imm), a1 :: nil => + DO hv1 <~ hsi_sreg_get hst a1;; + expanse_condimm_int32s c hv1 imm + | Ocmp (Ccompuimm c imm), a1 :: nil => + DO hv1 <~ hsi_sreg_get hst a1;; + expanse_condimm_int32u c hv1 imm + | Ocmp (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 + | Ocmp (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 + | Ocmp (Ccomplimm c imm), a1 :: nil => + DO hv1 <~ hsi_sreg_get hst a1;; + expanse_condimm_int64s c hv1 imm + | Ocmp (Ccompluimm c imm), a1 :: nil => + DO hv1 <~ hsi_sreg_get hst a1;; + expanse_condimm_int64u c hv1 imm + | Ocmp (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 + | Ocmp (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 + | Ocmp (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 + | Ocmp (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*) + | _, _ => None + end. + Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall (H: target_op_simplify op lr hst = Some fsv) @@ -12,8 +117,8 @@ Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args) (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m), seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m. -Proof. +Proof. Admitted. (* unfold target_op_simplify; simpl. congruence. -Qed. + Qed.*) Global Opaque target_op_simplify. 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 *) diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index 589cf25f..c6a4d409 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v @@ -12,6 +12,7 @@ Local Open Scope error_monad_scope. Local Open Scope option_monad_scope. Require Export Impure.ImpHCons. +Import HConsing. Import ListNotations. Local Open Scope list_scope. @@ -304,6 +305,66 @@ Inductive hfinal_refines: hsfval -> sfval -> Prop := End HFINAL_REFINES. +(* TODO gourdinl Leave this here ? *) +Section FAKE_HSVAL. +(* 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 ... *) + +End FAKE_HSVAL. + Record hsstate := { hinternal:> hsistate; hfinal: hsfval }. |