diff options
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index f4e3672d..66b199cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -745,6 +745,25 @@ Section SOUNDNESS. Hint Resolve oper1_sound : cse3. + Lemma rel_idem_replace: + forall rel rs r m, + sem_rel rel rs m -> + sem_rel rel rs # r <- (rs # r) m. + Proof. + intros until m. + intro REL. + unfold sem_rel, sem_eq, sem_rhs in *. + intros. + specialize REL with (i:=i) (eq0:=eq). + rewrite Regmap.gsident. + replace ((rs # r <- (rs # r)) ## (eq_args eq)) with + (rs ## (eq_args eq)). + { apply REL; auto. } + apply list_map_exten. + intros. + apply Regmap.gsident. + Qed. + Lemma move_sound : forall no : node, forall rel : RELATION.t, @@ -756,6 +775,10 @@ Section SOUNDNESS. unfold move. intros until m. intro REL. + destruct (peq src dst). + { subst dst. + apply rel_idem_replace; auto. + } 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. @@ -798,7 +821,11 @@ Section SOUNDNESS. subst. rewrite <- (forward_move_sound rel rs m r) by auto. apply move_sound; auto. - - destruct rhs_find as [src |] eqn:RHS_FIND. + - destruct (is_trivial_sym_op sop). + { + apply kill_reg_sound; auto. + } + destruct rhs_find as [src |] eqn:RHS_FIND. + destruct (Compopts.optim_CSE3_glb tt). * apply sem_rel_glb; split. ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. |