diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-15 11:50:56 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-15 11:50:56 +0200 |
| commit | 3ceff391e0be39cd7a3d5d861fb1f32653579bab (patch) | |
| tree | 07e6a693bac4bd8cc14723c658edd562f899789d /backend/CSE3analysisproof.v | |
| parent | 7c6ce18466ed1de58a0f99c785c777d63a9a6149 (diff) | |
| download | compcert-kvx-3ceff391e0be39cd7a3d5d861fb1f32653579bab.tar.gz compcert-kvx-3ceff391e0be39cd7a3d5d861fb1f32653579bab.zip | |
some more tuning of CSE3
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 0ddaa527..66b199cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -821,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. |