diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-06 22:33:02 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-06 22:33:02 +0200 |
| commit | 6171f6a0880acbf0d007a7715cc37984ac25d851 (patch) | |
| tree | 6d9fdc4e935a6c616623f3dc1529a0945f8d79d2 /backend/CSE3analysisproof.v | |
| parent | f1f535cad98f3db3e586f0f7a2dbc329fc5bff6f (diff) | |
| download | compcert-kvx-6171f6a0880acbf0d007a7715cc37984ac25d851.tar.gz compcert-kvx-6171f6a0880acbf0d007a7715cc37984ac25d851.zip | |
-fcse3-glb
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 0c2aeb8e..f4e3672d 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -799,13 +799,17 @@ Section SOUNDNESS. 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. *) + + 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. + eapply forward_move_rhs_sound in RHS. + 2: eassumption. + rewrite <- (sem_rhs_det SOUND RHS). + apply move_sound; auto. + ** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + * ** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + apply oper1_sound; auto. apply forward_move_rhs_sound; auto. Qed. |