diff options
| -rw-r--r-- | backend/CSE.v | 61 | ||||
| -rw-r--r-- | backend/CSEproof.v | 197 |
2 files changed, 168 insertions, 90 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index ba8dec8..d46afdc 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -80,13 +80,14 @@ Qed. fresh value numbers. *) Record numbering : Type := mknumbering { - num_next: valnum; - num_eqs: list (valnum * rhs); - num_reg: PTree.t valnum + num_next: valnum; (**r first unused value number *) + num_eqs: list (valnum * rhs); (**r valid equations *) + num_reg: PTree.t valnum; (**r mapping register to valnum *) + num_val: PMap.t (list reg) (**r reverse mapping valnum to regs containing it *) }. Definition empty_numbering := - mknumbering 1%positive nil (PTree.empty valnum). + mknumbering 1%positive nil (PTree.empty valnum) (PMap.init nil). (** [valnum_reg n r] returns the value number for the contents of register [r]. If none exists, a fresh value number is returned @@ -97,10 +98,13 @@ Definition empty_numbering := Definition valnum_reg (n: numbering) (r: reg) : numbering * valnum := match PTree.get r n.(num_reg) with | Some v => (n, v) - | None => (mknumbering (Psucc n.(num_next)) - n.(num_eqs) - (PTree.set r n.(num_next) n.(num_reg)), - n.(num_next)) + | None => + let v := n.(num_next) in + (mknumbering (Psucc v) + n.(num_eqs) + (PTree.set r v n.(num_reg)) + (PMap.set v (r :: nil) n.(num_val)), + v) end. Fixpoint valnum_regs (n: numbering) (rl: list reg) @@ -126,6 +130,29 @@ Fixpoint find_valnum_rhs (r: rhs) (eqs: list (valnum * rhs)) if eq_rhs r r' then Some v else find_valnum_rhs r eqs1 end. +(** [find_valnum_num vn eqs] searches the list of equations [eqs] + for an equation of the form [vn = rhs] for some equation [rhs]. + If found, [Some rhs] is returned, otherwise [None] is returned. *) + +Fixpoint find_valnum_num (v: valnum) (eqs: list (valnum * rhs)) + {struct eqs} : option rhs := + match eqs with + | nil => None + | (v', r') :: eqs1 => + if peq v v' then Some r' else find_valnum_num v eqs1 + end. + +(** Update the [num_val] mapping prior to a redefinition of register [r]. *) + +Definition forget_reg (n: numbering) (rd: reg) : PMap.t (list reg) := + match PTree.get rd n.(num_reg) with + | None => n.(num_val) + | Some v => PMap.set v (List.remove peq rd (PMap.get v n.(num_val))) n.(num_val) + end. + +Definition update_reg (n: numbering) (rd: reg) (vn: valnum) : PMap.t (list reg) := + let nv := forget_reg n rd in PMap.set vn (rd :: PMap.get vn nv) nv. + (** [add_rhs n rd rhs] updates the value numbering [n] to reflect the computation of the operation or load represented by [rhs] and the storing of the result in register [rd]. If an equation @@ -138,10 +165,12 @@ Definition add_rhs (n: numbering) (rd: reg) (rh: rhs) : numbering := | Some vres => mknumbering n.(num_next) n.(num_eqs) (PTree.set rd vres n.(num_reg)) + (update_reg n rd vres) | None => mknumbering (Psucc n.(num_next)) ((n.(num_next), rh) :: n.(num_eqs)) (PTree.set rd n.(num_next) n.(num_reg)) + (update_reg n rd n.(num_next)) end. (** [add_op n rd op rs] specializes [add_rhs] for the case of an @@ -164,7 +193,8 @@ Definition add_op (n: numbering) (rd: reg) (op: operation) (rs: list reg) := match is_move_operation op rs with | Some r => let (n1, v) := valnum_reg n r in - mknumbering n1.(num_next) n1.(num_eqs) (PTree.set rd v n1.(num_reg)) + mknumbering n1.(num_next) n1.(num_eqs) + (PTree.set rd v n1.(num_reg)) (update_reg n1 rd v) | None => let (n1, vs) := valnum_regs n rs in add_rhs n1 rd (Op op vs) @@ -188,7 +218,8 @@ Definition add_load (n: numbering) (rd: reg) Definition add_unknown (n: numbering) (rd: reg) := mknumbering (Psucc n.(num_next)) n.(num_eqs) - (PTree.set rd n.(num_next) n.(num_reg)). + (PTree.set rd n.(num_next) n.(num_reg)) + (forget_reg n rd). (** [kill_equations pred n] remove all equations satisfying predicate [pred]. *) @@ -201,7 +232,7 @@ Fixpoint kill_eqs (pred: rhs -> bool) (eqs: list (valnum * rhs)) : list (valnum Definition kill_equations (pred: rhs -> bool) (n: numbering) : numbering := mknumbering n.(num_next) (kill_eqs pred n.(num_eqs)) - n.(num_reg). + n.(num_reg) n.(num_val). (** [kill_loads n] removes all equations involving memory loads, as well as those involving memory-dependent operators. @@ -245,10 +276,10 @@ Definition add_store (n: numbering) (chunk: memory_chunk) (addr: addressing) [vn], or [None] if no such register exists. *) Definition reg_valnum (n: numbering) (vn: valnum) : option reg := - PTree.fold - (fun (res: option reg) (r: reg) (v: valnum) => - if peq v vn then Some r else res) - n.(num_reg) None. + match PMap.get vn n.(num_val) with + | nil => None + | r :: rs => Some r + end. (* [find_rhs] and its specializations [find_op] and [find_load] return a register that already holds the result of the given arithmetic diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 6543826..fa07716 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -48,19 +48,22 @@ Definition wf_rhs (next: valnum) (rh: rhs) : Prop := Definition wf_equation (next: valnum) (vr: valnum) (rh: rhs) : Prop := Plt vr next /\ wf_rhs next rh. -Definition wf_numbering (n: numbering) : Prop := - (forall v rh, - In (v, rh) n.(num_eqs) -> wf_equation n.(num_next) v rh) -/\ - (forall r v, - PTree.get r n.(num_reg) = Some v -> Plt v n.(num_next)). +Inductive wf_numbering (n: numbering) : Prop := + wf_numbering_intro + (EQS: forall v rh, + In (v, rh) n.(num_eqs) -> wf_equation n.(num_next) v rh) + (REG: forall r v, + PTree.get r n.(num_reg) = Some v -> Plt v n.(num_next)) + (VAL: forall r v, + In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v). Lemma wf_empty_numbering: wf_numbering empty_numbering. Proof. unfold empty_numbering; split; simpl; intros. - elim H. + contradiction. rewrite PTree.gempty in H. congruence. + rewrite PMap.gi in H. contradiction. Qed. Lemma wf_rhs_increasing: @@ -76,7 +79,7 @@ Lemma wf_equation_increasing: Ple next1 next2 -> wf_equation next1 vr rh -> wf_equation next2 vr rh. Proof. - intros. elim H0; intros. split. + intros. destruct H0. split. apply Plt_Ple_trans with next1; auto. apply wf_rhs_increasing with next1; auto. Qed. @@ -90,20 +93,21 @@ Lemma wf_valnum_reg: valnum_reg n r = (n', v) -> wf_numbering n' /\ Plt v n'.(num_next) /\ Ple n.(num_next) n'.(num_next). Proof. - intros until v. intros WF. inversion WF. - generalize (H0 r v). - unfold valnum_reg. destruct ((num_reg n)!r). - intros. replace n' with n. split. auto. - split. apply H1. congruence. - apply Ple_refl. - congruence. - intros. inversion H2. simpl. split. - split; simpl; intros. + intros until v. unfold valnum_reg. intros WF VREG. inversion WF. + destruct ((num_reg n)!r) as [v'|]_eqn. +(* found *) + inv VREG. split. auto. split. eauto. apply Ple_refl. +(* not found *) + inv VREG. split. + split; simpl; intros. apply wf_equation_increasing with (num_next n). apply Ple_succ. auto. - rewrite PTree.gsspec in H3. destruct (peq r0 r). - replace v0 with (num_next n). apply Plt_succ. congruence. - apply Plt_trans_succ; eauto. - split. apply Plt_succ. apply Ple_succ. + rewrite PTree.gsspec in H. destruct (peq r0 r). + inv H. apply Plt_succ. + apply Plt_trans_succ; eauto. + rewrite PMap.gsspec in H. destruct (peq v (num_next n)). + subst v. simpl in H. destruct H. subst r0. apply PTree.gss. contradiction. + rewrite PTree.gso. eauto. exploit VAL; eauto. congruence. + simpl. split. apply Plt_succ. apply Ple_succ. Qed. Lemma wf_valnum_regs: @@ -142,6 +146,54 @@ Proof. intro. right. auto. Qed. +Lemma find_valnum_num_correct: + forall rh vn eqs, + find_valnum_num vn eqs = Some rh -> In (vn, rh) eqs. +Proof. + induction eqs; simpl. + congruence. + destruct a as [v' r']. destruct (peq vn v'); intros. + left. congruence. + right. auto. +Qed. + +Remark in_remove: + forall (A: Type) (eq: forall (x y: A), {x=y}+{x<>y}) x y l, + In y (List.remove eq x l) <-> x <> y /\ In y l. +Proof. + induction l; simpl. + tauto. + destruct (eq x a). + subst a. rewrite IHl. tauto. + simpl. rewrite IHl. intuition congruence. +Qed. + +Lemma wf_forget_reg: + forall n rd r v, + wf_numbering n -> + In r (PMap.get v (forget_reg n rd)) -> r <> rd /\ PTree.get r n.(num_reg) = Some v. +Proof. + unfold forget_reg; intros. inversion H. + destruct ((num_reg n)!rd) as [vd|]_eqn. + rewrite PMap.gsspec in H0. destruct (peq v vd). + subst vd. rewrite in_remove in H0. destruct H0. split. auto. eauto. + split; eauto. exploit VAL; eauto. congruence. + split; eauto. exploit VAL; eauto. congruence. +Qed. + +Lemma wf_update_reg: + forall n rd vd r v, + wf_numbering n -> + In r (PMap.get v (update_reg n rd vd)) -> PTree.get r (PTree.set rd vd n.(num_reg)) = Some v. +Proof. + unfold update_reg; intros. inversion H. rewrite PMap.gsspec in H0. + destruct (peq v vd). + subst v; simpl in H0. destruct H0. + subst r. apply PTree.gss. + exploit wf_forget_reg; eauto. intros [A B]. rewrite PTree.gso; eauto. + exploit wf_forget_reg; eauto. intros [A B]. rewrite PTree.gso; eauto. +Qed. + Lemma wf_add_rhs: forall n rd rh, wf_numbering n -> @@ -149,20 +201,24 @@ Lemma wf_add_rhs: wf_numbering (add_rhs n rd rh). Proof. intros. inversion H. unfold add_rhs. - caseEq (find_valnum_rhs rh n.(num_eqs)); intros. - split; simpl. assumption. - intros r v0. rewrite PTree.gsspec. case (peq r rd); intros. - inversion H4. subst v0. - elim (H1 v rh (find_valnum_rhs_correct _ _ _ H3)). auto. - eauto. - split; simpl. - intros v rh0 [A1|A2]. inversion A1. subst rh0. - split. apply Plt_succ. apply wf_rhs_increasing with n.(num_next). - apply Ple_succ. auto. + destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|]_eqn. +(* found *) + exploit find_valnum_rhs_correct; eauto. intros IN. + split; simpl; intros. + auto. + rewrite PTree.gsspec in H1. destruct (peq r rd). + inv H1. exploit EQS; eauto. intros [A B]. auto. + eauto. + eapply wf_update_reg; eauto. +(* not found *) + split; simpl; intros. + destruct H1. + inv H1. split. apply Plt_succ. apply wf_rhs_increasing with n.(num_next). apply Ple_succ. auto. apply wf_equation_increasing with n.(num_next). apply Ple_succ. auto. - intros r v. rewrite PTree.gsspec. case (peq r rd); intro. - intro. inversion H4. apply Plt_succ. - intro. apply Plt_trans_succ. eauto. + rewrite PTree.gsspec in H1. destruct (peq r rd). + inv H1. apply Plt_succ. + apply Plt_trans_succ. eauto. + eapply wf_update_reg; eauto. Qed. Lemma wf_add_op: @@ -170,16 +226,18 @@ Lemma wf_add_op: wf_numbering n -> wf_numbering (add_op n rd op rs). Proof. - intros. unfold add_op. - case (is_move_operation op rs). - intro r. caseEq (valnum_reg n r); intros n' v EQ. - destruct (wf_valnum_reg _ _ _ _ H EQ) as [[A1 A2] [B C]]. - split; simpl. assumption. intros until v0. rewrite PTree.gsspec. - case (peq r0 rd); intros. replace v0 with v. auto. congruence. + intros. unfold add_op. destruct (is_move_operation op rs) as [r|]_eqn. +(* move *) + destruct (valnum_reg n r) as [n' v]_eqn. + exploit wf_valnum_reg; eauto. intros [A [B C]]. inversion A. + constructor; simpl; intros. eauto. - caseEq (valnum_regs n rs). intros n' vl EQ. - generalize (wf_valnum_regs _ _ _ _ H EQ). intros [A [B C]]. - apply wf_add_rhs; auto. + rewrite PTree.gsspec in H0. destruct (peq r0 rd). inv H0. auto. eauto. + eapply wf_update_reg; eauto. +(* not a move *) + destruct (valnum_regs n rs) as [n' vs]_eqn. + exploit wf_valnum_regs; eauto. intros [A [B C]]. + eapply wf_add_rhs; eauto. Qed. Lemma wf_add_load: @@ -198,11 +256,12 @@ Lemma wf_add_unknown: wf_numbering n -> wf_numbering (add_unknown n rd). Proof. - intros. inversion H. unfold add_unknown. constructor; simpl. - intros. eapply wf_equation_increasing; eauto. auto with coqlib. - intros until v. rewrite PTree.gsspec. case (peq r rd); intros. - inversion H2. auto with coqlib. - apply Plt_trans_succ. eauto. + intros. inversion H. unfold add_unknown. constructor; simpl; intros. + eapply wf_equation_increasing; eauto. auto with coqlib. + rewrite PTree.gsspec in H0. destruct (peq r rd). + inv H0. auto with coqlib. + apply Plt_trans_succ; eauto. + exploit wf_forget_reg; eauto. intros [A B]. rewrite PTree.gso; eauto. Qed. Remark kill_eqs_in: @@ -222,6 +281,7 @@ Proof. intros. inversion H. unfold kill_equations; split; simpl; intros. exploit kill_eqs_in; eauto. intros [A B]. auto. eauto. + eauto. Qed. Lemma wf_add_store: @@ -320,15 +380,13 @@ Lemma numbering_holds_exten: numbering_holds valu2 ge sp rs m n. Proof. intros. inversion H0. inversion H1. split; intros. - generalize (H2 _ _ H6). intro WFEQ. - generalize (H4 _ _ H6). + exploit EQS; eauto. intros [A B]. red in B. + generalize (H2 _ _ H4). unfold equation_holds; destruct rh. - elim WFEQ; intros. rewrite (valu_agree_list valu1 valu2 n.(num_next)). - rewrite H. auto. auto. auto. exact H8. - elim WFEQ; intros. + rewrite H. auto. auto. auto. auto. rewrite (valu_agree_list valu1 valu2 n.(num_next)). - rewrite H. auto. auto. auto. exact H8. + rewrite H. auto. auto. auto. auto. rewrite H. auto. eauto. Qed. @@ -643,25 +701,11 @@ Qed. that register correctly maps back to the given value number. *) Lemma reg_valnum_correct: - forall n v r, reg_valnum n v = Some r -> n.(num_reg)!r = Some v. + forall n v r, wf_numbering n -> reg_valnum n v = Some r -> n.(num_reg)!r = Some v. Proof. - intros until r. unfold reg_valnum. rewrite PTree.fold_spec. - assert(forall l acc0, - List.fold_left - (fun (acc: option reg) (p: reg * valnum) => - if peq (snd p) v then Some (fst p) else acc) - l acc0 = Some r -> - In (r, v) l \/ acc0 = Some r). - induction l; simpl. - intros. tauto. - case a; simpl; intros r1 v1 acc0 FL. - generalize (IHl _ FL). - case (peq v1 v); intro. - subst v1. intros [A|B]. tauto. inversion B; subst r1. tauto. - tauto. - intro. elim (H _ _ H0); intro. - apply PTree.elements_complete; auto. - discriminate. + unfold reg_valnum; intros. inv H. + destruct ((num_val n)#v) as [| r1 rl]_eqn; inv H0. + eapply VAL. rewrite Heql. auto with coqlib. Qed. (** Correctness of [find_op] and [find_load]: if successful and in a @@ -670,15 +714,16 @@ Qed. Lemma find_rhs_correct: forall valu rs m n rh r, + wf_numbering n -> numbering_holds valu ge sp rs m n -> find_rhs n rh = Some r -> rhs_evals_to valu rh m rs#r. Proof. - intros until r. intros NH. + intros until r. intros WF NH. unfold find_rhs. caseEq (find_valnum_rhs rh n.(num_eqs)); intros. - generalize (find_valnum_rhs_correct _ _ _ H); intro. - generalize (reg_valnum_correct _ _ _ H0); intro. + exploit find_valnum_rhs_correct; eauto. intros. + exploit reg_valnum_correct; eauto. intros. inversion NH. generalize (H3 _ _ H1). rewrite (H4 _ _ H2). destruct rh; simpl; auto. @@ -694,6 +739,7 @@ Lemma find_op_correct: Proof. intros until r. intros WF [valu NH]. unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND. + assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto). generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR). intros [valu2 [NH2 [EQ AG]]]. rewrite <- EQ. @@ -712,6 +758,7 @@ Lemma find_load_correct: Proof. intros until r. intros WF [valu NH]. unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND. + assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto). generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR). intros [valu2 [NH2 [EQ AG]]]. rewrite <- EQ. |