More efficient implementation of reg_valnum

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1900 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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.