diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 11:43:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-23 11:43:06 +0200 |
| commit | 69447b8515c0bd123c6aa72c5545cf9beda79ec4 (patch) | |
| tree | 80871cb7091ef1a68e6634fc0cffc5c6fb69c024 /backend/CSE3analysisproof.v | |
| parent | dc43cc3371f7837cff5b8d1fd536aba54e99232f (diff) | |
| download | compcert-kvx-69447b8515c0bd123c6aa72c5545cf9beda79ec4.tar.gz compcert-kvx-69447b8515c0bd123c6aa72c5545cf9beda79ec4.zip | |
fix in CSE3 move propagation
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 3ea5e078..116353fa 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -778,15 +778,25 @@ Section SOUNDNESS. intros until v. intros REL RHS. unfold oper. - destruct rhs_find as [src |] eqn:RHS_FIND. - - 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. - eapply forward_move_rhs_sound in RHS. - 2: eassumption. - rewrite <- (sem_rhs_det SOUND RHS). - apply move_sound; auto. + destruct (is_smove sop). + - subst. + simpl in RHS. + destruct args. contradiction. + destruct args. 2: contradiction. + cbn in *. + subst. + rewrite <- (forward_move_sound rel rs m r) by auto. + apply move_sound; auto. + - destruct rhs_find as [src |] eqn:RHS_FIND. + + (* FIXME 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. + eapply forward_move_rhs_sound in RHS. + 2: eassumption. + rewrite <- (sem_rhs_det SOUND RHS). + apply move_sound; auto. + (* FIXME * apply oper1_sound; auto. *) + apply oper1_sound; auto. - - apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. Qed. Hint Resolve oper_sound : cse3. |