diff options
-rw-r--r-- | backend/CSE3analysis.v | 17 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 34 |
2 files changed, 50 insertions, 1 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 7357a811..cdda2cb7 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -236,6 +236,23 @@ Section OPERATIONS. then kill_reg dst rel else oper2 dst op args rel. + + Definition move (src dst : reg) (rel : RELATION.t) : RELATION.t := + match eq_find {| eq_lhs := dst; + eq_op := SOp Omove; + eq_args:= src::nil |} with + | Some eq_id => PSet.add eq_id (kill_reg dst rel) + | None => kill_reg dst rel + end. + + (* + Definition oper (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + match find_op rel op (forward_move_l rel args) with + | Some r => move r dst rel + | None => oper1 op dst args rel + end. +*) End PER_NODE. End OPERATIONS. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 5eff5e08..96baac77 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -565,5 +565,37 @@ Section SOUNDNESS. unfold oper1. destruct in_dec; auto with cse3. Qed. - + + Lemma move_sound : + forall no : node, + forall rel : RELATION.t, + forall src dst : reg, + forall rs m, + sem_rel rel rs m -> + sem_rel (move (ctx:=ctx) no src dst rel) (rs # dst <- (rs # src)) m. + Proof. + unfold move. + intros until m. + intro REL. + pose proof (eq_find_sound no {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND. + destruct eq_find. + - intros i eq CONTAINS. + destruct (peq i e). + + subst i. + rewrite (EQ_FIND_SOUND e) by trivial. + intro Z. + inv Z. + unfold sem_eq. + simpl. + destruct (peq src dst). + * subst dst. + reflexivity. + * rewrite Regmap.gss. + rewrite Regmap.gso by congruence. + reflexivity. + + intros. + rewrite PSet.gaddo in CONTAINS by congruence. + apply (kill_reg_sound rel rs m dst (rs # src) REL i); auto. + - apply kill_reg_sound; auto. + Qed. End SOUNDNESS. |