diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:50:50 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:50:50 +0100 |
| commit | b7bf754fce5e9442c3a5b1e5cec25ed522d0e870 (patch) | |
| tree | 267a432dbd7fe3102b2ce5278d72961b16f82366 /backend/CSE3analysisproof.v | |
| parent | 8c8e6a0528a91420e399ae84ccf293c0d8be285f (diff) | |
| download | compcert-kvx-b7bf754fce5e9442c3a5b1e5cec25ed522d0e870.tar.gz compcert-kvx-b7bf754fce5e9442c3a5b1e5cec25ed522d0e870.zip | |
oper sound
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 96baac77..c0a9be48 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -415,7 +415,7 @@ Section SOUNDNESS. Hint Resolve eq_find_sound : cse3. - Theorem rhs_find_op_sound: + Theorem rhs_find_sound: forall no sop args rel src rs m, sem_rel rel rs m -> rhs_find (ctx := ctx) no sop args rel = Some src -> @@ -441,7 +441,7 @@ Section SOUNDNESS. intuition congruence. Qed. - Hint Resolve rhs_find_op_sound : cse3. + Hint Resolve rhs_find_sound : cse3. Theorem forward_move_rhs_sound : forall sop args rel rs m v, @@ -507,7 +507,7 @@ Section SOUNDNESS. Qed. Lemma sem_rhs_det: - forall sop args rs m v v', + forall {sop} {args} {rs} {m} {v} {v'}, sem_rhs sop args rs m v -> sem_rhs sop args rs m v' -> v = v'. @@ -566,6 +566,8 @@ Section SOUNDNESS. destruct in_dec; auto with cse3. Qed. + Hint Resolve oper1_sound : cse3. + Lemma move_sound : forall no : node, forall rel : RELATION.t, @@ -598,4 +600,26 @@ Section SOUNDNESS. apply (kill_reg_sound rel rs m dst (rs # src) REL i); auto. - apply kill_reg_sound; auto. Qed. + + Hint Resolve move_sound : cse3. + + Theorem oper_sound: + forall no dst sop args rel rs m v, + sem_rel rel rs m -> + sem_rhs sop args rs m v -> + sem_rel (oper (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. + Proof. + intros until v. + intros REL RHS. + unfold oper. + destruct rhs_find as [src |] eqn:RHS_FIND. + - pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. + eapply forward_move_rhs_sound in RHS. + 2: eassumption. + rewrite <- (sem_rhs_det SOUND RHS). + apply move_sound; auto. + - apply oper1_sound; auto. + Qed. + + Hint Resolve oper_sound : cse3. End SOUNDNESS. |