diff options
| -rw-r--r-- | backend/CSE3analysis.v | 31 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 78 |
2 files changed, 98 insertions, 11 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 34df644e..dbf1afe2 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -236,7 +236,30 @@ Section OPERATIONS. | nil => before end. - Definition pick_source (l : list reg) := + Definition pick_source (l : list reg) := (* todo: take min? *) + match l with + | h::t => Some h + | nil => None + end. + + Definition forward_move1 (rel : RELATION.t) (x : reg) : reg := + match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with + | None => x + | Some eqno => + match eq_catalog ctx eqno with + | Some eq => + if is_smove (eq_op eq) && peq x (eq_lhs eq) + then + match eq_args eq with + | src::nil => src + | _ => x + end + else x + | _ => x + end + end. + + Definition pick_min_source (l : list reg) := match l with | h::t => Some (reg_min_rec t h) | nil => None @@ -259,11 +282,13 @@ Section OPERATIONS. end end. - Definition forward_move (rel : RELATION.t) (x : reg) : reg := - match pick_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with + Definition forward_move2 (rel : RELATION.t) (x : reg) : reg := + match pick_min_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with | None => x | Some src => src end. + + Definition forward_move := forward_move1. Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := List.map (forward_move rel). diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 12048010..29254a4f 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -500,9 +500,9 @@ Section SOUNDNESS. destruct (reg_min_sound bef a); auto. Qed. - Lemma pick_source_sound : + Lemma pick_min_source_sound : forall (l : list reg), - match pick_source l with + match pick_min_source l with | Some x => In x l | None => True end. @@ -511,7 +511,7 @@ Section SOUNDNESS. destruct (reg_min_rec_sound l r); auto. Qed. - Hint Resolve pick_source_sound : cse3. + Hint Resolve pick_min_source_sound : cse3. Theorem get_sources_sound : forall l src rs m x, @@ -551,15 +551,15 @@ Section SOUNDNESS. assumption. Qed. - Theorem forward_move_sound : + Theorem forward_move2_sound : forall rel rs m x, (sem_rel rel rs m) -> - rs # (forward_move (ctx := ctx) rel x) = rs # x. + rs # (forward_move2 (ctx := ctx) rel x) = rs # x. Proof. - unfold forward_move. + unfold forward_move2. intros until x; intros REL. - pose proof (pick_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK. - destruct pick_source. + pose proof (pick_min_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK. + destruct pick_min_source. 2: reflexivity. apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m). 2: assumption. @@ -572,6 +572,68 @@ Section SOUNDNESS. apply REL with (i:=i); assumption. Qed. + Hint Resolve forward_move2_sound : cse3. + + + Lemma pick_source_sound : + forall (l : list reg), + match pick_source l with + | Some x => In x l + | None => True + end. + Proof. + unfold pick_source. + destruct l; simpl; trivial. + left; trivial. + Qed. + + Hint Resolve pick_source_sound : cse3. + + Theorem forward_move1_sound : + forall rel rs m x, + (sem_rel rel rs m) -> + rs # (forward_move1 (ctx := ctx) rel x) = rs # x. + Proof. + unfold sem_rel, forward_move1. + intros until x. + intro REL. + pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT. + destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))). + 2: reflexivity. + destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. + 2: reflexivity. + specialize REL with (i := r) (eq0 := eq). + destruct (is_smove (eq_op eq)) as [MOVE | ]. + 2: reflexivity. + destruct (peq x (eq_lhs eq)). + 2: reflexivity. + simpl. + subst x. + rewrite PSet.elements_spec in ELEMENT. + rewrite PSet.ginter in ELEMENT. + rewrite andb_true_iff in ELEMENT. + unfold sem_eq in REL. + rewrite MOVE in REL. + simpl in REL. + destruct (eq_args eq) as [ | h t]. + reflexivity. + destruct t. + 2: reflexivity. + simpl in REL. + intuition congruence. + Qed. + + Hint Resolve forward_move1_sound : cse3. + + Theorem forward_move_sound : + forall rel rs m x, + (sem_rel rel rs m) -> + rs # (forward_move (ctx := ctx) rel x) = rs # x. + Proof. + unfold forward_move. + apply forward_move1_sound. + Qed. + Hint Resolve forward_move_sound : cse3. Theorem forward_move_l_sound : |