diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:30:57 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:30:57 +0100 |
| commit | 8c8e6a0528a91420e399ae84ccf293c0d8be285f (patch) | |
| tree | 5052d78f49984466103ab1cb41c5354779134f1f /backend/CSE3analysisproof.v | |
| parent | d5bbfed2c8a0a208cf365abb1df249c9d91ff8e4 (diff) | |
| download | compcert-kvx-8c8e6a0528a91420e399ae84ccf293c0d8be285f.tar.gz compcert-kvx-8c8e6a0528a91420e399ae84ccf293c0d8be285f.zip | |
move sound
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 34 |
1 files changed, 33 insertions, 1 deletions
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. |