diff options
| -rw-r--r-- | backend/CSE2.v | 64 | ||||
| -rw-r--r-- | backend/CSE2proof.v | 32 | ||||
| -rw-r--r-- | lib/Maps.v | 121 |
3 files changed, 204 insertions, 13 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index a76104af..1e3bc3b7 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -41,7 +41,8 @@ Definition pset_remove (i : positive) (s : pset) := PTree.remove i s. Record relmap := mkrel { var_to_sym : PTree.t sym_val ; - mem_used : pset + mem_used : pset ; + reg_used : PTree.t pset }. Module RELATION. @@ -51,7 +52,7 @@ Definition t := relmap. Definition eq (r1 r2 : t) := forall x, (PTree.get x (var_to_sym r1)) = (PTree.get x (var_to_sym r2)). -Definition top : t := mkrel (PTree.empty sym_val) pset_empty. +Definition top : t := mkrel (PTree.empty sym_val) pset_empty (PTree.empty pset). Lemma eq_refl: forall x, eq x x. Proof. @@ -131,7 +132,13 @@ Definition lub (r1 r2 : t) := | _, None => None end) (var_to_sym r1) (var_to_sym r2)) - (pset_inter (mem_used r1) (mem_used r2)). + (pset_inter (mem_used r1) (mem_used r2)) + (PTree.combine_null + (fun x y => let r := pset_inter x y in + if PTree.bempty_canon r + then None + else Some r) + (reg_used r1) (reg_used r2)). Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. @@ -275,17 +282,46 @@ End ADD_BOTTOM. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). -Definition kill_sym_val (dst : reg) (sv : sym_val) := +Definition kill_sym_val (dst : reg) (sv : sym_val) : bool := match sv with | SMove src => if peq dst src then true else false | SOp op args => List.existsb (peq dst) args | SLoad chunk addr args => List.existsb (peq dst) args end. - + +Definition referenced_by sv := + match sv with + | SMove src => src :: nil + | SOp op args => args + | SLoad chunk addr args => args + end. + +Definition referenced_by' osv := + match osv with + | None => nil + | Some sv => referenced_by sv + end. + +Definition remove_from_sets + (to_remove : reg) : + list reg -> PTree.t pset -> PTree.t pset := + List.fold_left + (fun sets reg => + match PTree.get reg sets with + | None => sets + | Some xset => + let xset' := PTree.remove to_remove xset in + if PTree.bempty_canon xset' + then PTree.remove reg sets + else PTree.set reg xset' sets + end). + Definition kill_reg (dst : reg) (rel : RELATION.t) : RELATION.t := - mkrel (PTree.filter1 (fun x => negb (kill_sym_val dst x)) - (PTree.remove dst (var_to_sym rel))) - (pset_remove dst (mem_used rel)). + let rel' := PTree.remove dst (var_to_sym rel) in + mkrel (PTree.filter1 (fun x => negb (kill_sym_val dst x)) rel') + (pset_remove dst (mem_used rel)) + (remove_from_sets dst (referenced_by' (PTree.get dst (var_to_sym rel))) + (PTree.remove dst (reg_used rel))). Definition kill_sym_val_mem (sv: sym_val) := match sv with @@ -297,7 +333,8 @@ Definition kill_sym_val_mem (sv: sym_val) := Definition kill_mem (rel : RELATION.t) := mkrel (PTree.remove_t (var_to_sym rel) (mem_used rel)) - pset_empty. + pset_empty + (reg_used rel). (* FIXME *) Definition forward_move (rel : RELATION.t) (x : reg) : reg := @@ -309,7 +346,8 @@ Definition forward_move (rel : RELATION.t) (x : reg) : reg := Definition move (src dst : reg) (rel : RELATION.t) := let rel0 := kill_reg dst rel in mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym rel0)) - (mem_used rel0). + (mem_used rel0) + (reg_used rel0). (* FIXME *) Definition find_op_fold op args (already : option reg) x sv := match already with @@ -350,7 +388,8 @@ Definition oper2 (op: operation) (dst : reg) (args : list reg) let rel' := kill_reg dst rel in mkrel (PTree.set dst (SOp op (List.map (forward_move rel') args)) (var_to_sym rel')) (if op_depends_on_memory op then (pset_add dst (mem_used rel')) - else mem_used rel'). + else mem_used rel') + (reg_used rel'). (* FIXME *) Definition oper1 (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t := @@ -376,7 +415,8 @@ Definition load2 (chunk: memory_chunk) (addr : addressing) (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t := let rel' := kill_reg dst rel in mkrel (PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) (var_to_sym rel')) - (pset_add dst (mem_used rel')). + (pset_add dst (mem_used rel')) + (reg_used rel'). (* FIXME *) Definition load1 (chunk: memory_chunk) (addr : addressing) (dst : reg) (args : list reg) (rel : RELATION.t) := diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 350cdb24..e0244518 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -171,6 +171,38 @@ Proof. Qed. Local Hint Resolve wellformed_mem_kill_reg : wellformed. +Lemma kill_sym_val_referenced: + forall dst, + forall sv, + (kill_sym_val dst sv)=true <-> In dst (referenced_by sv). +Proof. + intros. + destruct sv; simpl. + - destruct peq; intuition congruence. + - rewrite existsb_exists. + split. + + intros [x [IN EQ]]. + destruct peq. + * subst x; trivial. + * discriminate. + + intro. + exists dst. + split; trivial. + destruct peq; trivial. + congruence. + - rewrite existsb_exists. + split. + + intros [x [IN EQ]]. + destruct peq. + * subst x; trivial. + * discriminate. + + intro. + exists dst. + split; trivial. + destruct peq; trivial. + congruence. +Qed. + Lemma wellformed_mem_kill_mem: forall rel, (wellformed_mem rel) -> (wellformed_mem (kill_mem rel)). @@ -164,6 +164,12 @@ Module Type TREE. forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), fold1 f m v = List.fold_left (fun a p => f a (snd p)) (elements m) v. + + Parameter bempty_canon : + forall (A : Type), t A -> bool. + Axiom bempty_canon_correct: + forall (A : Type) (tr : t A) (i : elt), + bempty_canon tr = true -> get i tr = None. End TREE. (** * The abstract signatures of maps *) @@ -274,6 +280,12 @@ Module PTree <: TREE. induction i; simpl; auto. Qed. + Definition bempty_canon (A : Type) (tr : t A) : bool := + match tr with + | Leaf => true + | _ => false + end. + Theorem gss: forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x. Proof. @@ -282,7 +294,16 @@ Module PTree <: TREE. Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None. Proof. exact gempty. Qed. - + + Lemma bempty_canon_correct: + forall (A : Type) (tr : t A) (i : elt), + bempty_canon tr = true -> get i tr = None. + Proof. + destruct tr; intros. + - rewrite gleaf; trivial. + - discriminate. + Qed. + Theorem gso: forall (A: Type) (i j: positive) (x: A) (m: t A), i <> j -> get i (set j x m) = get i m. @@ -1045,6 +1066,104 @@ Module PTree <: TREE. intros. apply fold1_xelements with (l := @nil (positive * A)). Qed. + (* DM + Fixpoint xfind_any (A : Type) (P : elt -> A -> bool) (i : elt) (m : t A): + option elt := + match m with + | Leaf => None + | Node l None r => + match xfind_any P (xO i) l with + | None => xfind_any P (xI i) r + | r => r + end + | Node l (Some x) r => + if P i x + then Some i + else + match xfind_any P (xO i) l with + | None => xfind_any P (xI i) r + | r => r + end + end. + + Definition find_any (A : Type) (P : elt -> A -> bool) (m : t A) := + xfind_any P xH m. + + Fixpoint pos_concat (i : positive) (j : positive) := + match i with + | xI r => xI (pos_concat r j) + | xO r => xO (pos_concat r j) + | xH => j + end. + + Lemma pos_concat_assoc : + forall i j k, + (pos_concat (pos_concat i j) k) = (pos_concat i (pos_concat j k)). + Admitted. + + Lemma pos_concat_eq_l : forall i j, + (pos_concat i j) = i -> j = xH. + Proof. + induction i; simpl; intros j EQ. + - inv EQ. auto. + - inv EQ. auto. + - trivial. + Qed. + + Lemma pos_concat_eq_r : forall i j, + (pos_concat i j) = j -> i = xH. + Admitted. + + Local Hint Resolve pos_concat_eq_r : trees. + + Lemma pos_concat_xH_r: forall i, (pos_concat i xH) = i. + Proof. + induction i; simpl; try rewrite IHi; trivial. + Qed. + + Local Hint Resolve pos_concat_xH_r : trees. + + (* + Fixpoint pos_is_prefix (i j : elt) := + match i, j with + | xI i1, xI j1 => pos_is_prefix i1 j1 + | xO i1, xO j1 => pos_is_prefix i1 j1 + | xH, _ => true + | _, _ => false + end. + *) + + Lemma xfind_any_correct: + forall A P (m : t A) i k, + xfind_any P i m = Some k -> exists j v, k = pos_concat j i + /\ (get j m)=Some v /\ (P k v)=true. + Proof. + induction m; simpl. + { (* leaf *) + discriminate. + } + intros i k FOUND. + destruct o. + { destruct P eqn:Pval in FOUND. + { inv FOUND. + exists xH. exists a. + simpl. + eauto. + } + specialize IHm1 with (i := xO i) (k := k). + specialize IHm2 with (i := xI i) (k := k). + assert (Some k = Some k) as SK by trivial. + destruct (xfind_any P (xO i) m1). + { + inv FOUND. + destruct (IHm1 SK) as [j' [v [EQk [GET PP]]]]. + exists (pos_concat j' (xO xH)). exists v. + rewrite pos_concat_assoc. + simpl. + split; trivial. + split; trivial. + } + *) End PTree. (** * An implementation of maps over type [positive] *) |