From 75a9af775b8fcc35d2d9218a1311a637db0fc344 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 23 Feb 2021 14:47:42 +0100 Subject: starting an interface for target rewriting rules. --- scheduling/RTLpathSE_impl.v | 139 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 130 insertions(+), 9 deletions(-) (limited to 'scheduling/RTLpathSE_impl.v') diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index bdd4bda8..d5921e51 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -430,6 +430,102 @@ 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 *) + +Fixpoint fsval_proj hsv: ?? hsval := + match hsv with + | HSinput r hc => + DO b <~ phys_eq hc unknown_hid;; + if b + then hSinput r (* was not yet really hash-consed *) + else RET hsv (* already hash-consed *) + | HSop op hl hc => + DO b <~ phys_eq hc unknown_hid;; + if b + then (* was not yet really hash-consed *) + DO hl' <~ fsval_list_proj hl;; + hSop op hl' + else RET hsv (* already hash-consed *) + | HSload hm t chk addr hl _ => RET hsv (* FIXME ? *) + end +with fsval_list_proj hl: ?? list_hsval := + match hl with + | HSnil hc => + DO b <~ phys_eq hc unknown_hid;; + if b + then hSnil() (* was not yet really hash-consed *) + else RET hl (* already hash-consed *) + | HScons hv hl hc => + DO b <~ phys_eq hc unknown_hid;; + if b + then (* was not yet really hash-consed *) + DO hv' <~ fsval_proj hv;; + DO hl' <~ fsval_list_proj hl;; + hScons hv' hl' + else RET hl (* already hash-consed *) + end. + +Lemma fsval_proj_correct hsv: + WHEN fsval_proj hsv ~> hsv' THEN forall ge sp rs0 m0, + seval_hsval ge sp hsv rs0 m0 = seval_hsval ge sp hsv' rs0 m0. +Admitted. +Global Opaque fsval_proj. +Local Hint Resolve fsval_proj_correct: wlp. + +(* END "fake" hsval ... *) + (** ** Assignment of memory *) Definition hslocal_set_smem (hst:hsistate_local) hm := {| hsi_smem := hm; @@ -596,6 +692,23 @@ Proof. explore; try congruence. Qed. + +(* TODO: This function could be defined in a specific file for each target *) +Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := + None. (* default implementation *) + +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) + (REF: hsilocal_refines ge sp rs0 m0 hst st) + (OK0: hsok_local ge sp rs0 m0 hst) + (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. + unfold target_op_simplify; simpl. congruence. +Qed. +Global Opaque target_op_simplify. + (** simplify a symbolic value before assignment to a register *) Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval := match rsv with @@ -603,8 +716,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs match is_move_operation op lr with | Some arg => hsi_sreg_get hst arg (** optimization of Omove *) | None => - DO lhsv <~ hlist_args hst lr;; - hSop op lhsv + match target_op_simplify op lr hst with + | Some fhv => fsval_proj fhv + | None => + DO lhsv <~ hlist_args hst lr;; + hSop op lhsv + end end | Rload _ chunk addr => DO lhsv <~ hlist_args hst lr;; @@ -620,17 +737,21 @@ Lemma simplify_correct rsv lr hst: Proof. destruct rsv; simpl; auto. - (* Rop *) - destruct (is_move_operation _ _) eqn: Hmove; wlp_simplify. - + exploit is_move_operation_correct; eauto. + destruct (is_move_operation _ _) eqn: Hmove. + { wlp_simplify; exploit is_move_operation_correct; eauto. intros (Hop & Hlsv); subst; simpl in *. simplify_SOME z. * erewrite H; eauto. * try_simplify_someHyps; congruence. - * congruence. - + clear Hmove. - generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0. - destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto. - intro H0; clear H0; simplify_SOME z; congruence. (* absurd case *) + * congruence. } + destruct (target_op_simplify _ _ _) eqn: Htarget_op_simp; wlp_simplify. + { destruct (seval_list_sval _ _ _) eqn: OKlist; try congruence. + destruct (seval_smem _ _ _ _ _) eqn: OKmem; try congruence. + rewrite <- H; exploit target_op_simplify_correct; eauto. } + clear Htarget_op_simp. + generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0. + destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto. + intro H0; clear H0; simplify_SOME z; congruence. (* absurd case *) - (* Rload *) destruct trap; wlp_simplify. erewrite H0; eauto. -- cgit